diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 22:15:21 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 22:15:21 +0200 |
commit | 524678ff9a521433ff0b5af2a3986c1e385e699e (patch) | |
tree | fc1f2e2a5f085f2bffede2530f02402839d30ca4 | |
parent | 4518486a771055e633aa050141d9721353d542d7 (diff) | |
download | compcert-kvx-524678ff9a521433ff0b5af2a3986c1e385e699e.tar.gz compcert-kvx-524678ff9a521433ff0b5af2a3986c1e385e699e.zip |
for floats and doubles, asmgen support
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 12 | ||||
-rw-r--r-- | mppa_k1c/Op.v | 54 | ||||
-rw-r--r-- | mppa_k1c/ValueAOp.v | 41 |
3 files changed, 92 insertions, 15 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index a7e3c8ef..ad01ff89 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -729,14 +729,10 @@ Definition transl_op do rd <- ireg_of res; transl_cond_op cmp rd args k - | Oselect, a0 :: a1 :: aS :: nil => - assertion (mreg_eq a0 res); - do r0 <- ireg_of a0; - do r1 <- ireg_of a1; - do rS <- ireg_of aS; - OK (Pcmove BTwnez r0 rS r1 ::i k) - - | Oselectl, a0 :: a1 :: aS :: nil => + | Oselect, a0 :: a1 :: aS :: nil + | Oselectl, a0 :: a1 :: aS :: nil + | Oselectf, a0 :: a1 :: aS :: nil + | Oselectfs, a0 :: a1 :: aS :: nil => assertion (mreg_eq a0 res); do r0 <- ireg_of a0; do r1 <- ireg_of a1; diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 74788387..5afd0cb9 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -183,7 +183,9 @@ Inductive operation : Type := (*c Boolean tests: *) | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) | Oselect (**r [rd = if r3 then r2 else r1] *) - | Oselectl. (**r [rd = if r3 then r2 else r1] *) + | Oselectl (**r [rd = if r3 then r2 else r1] *) + | Oselectf (**r [rd = if r3 then r2 else r1] *) + | Oselectfs. (**r [rd = if r3 then r2 else r1] *) (** Addressing modes. [r1], [r2], etc, are the arguments to the addressing. *) @@ -287,6 +289,40 @@ Definition selectl (v0 : val) (v1 : val) (vselect : val) : val := | _ => Vundef end. +Definition selectf (v0 : val) (v1 : val) (vselect : val) : val := + match vselect with + | Vint iselect => + match v0 with + | Vfloat i0 => + match v1 with + | Vfloat i1 => + Vfloat (if Int.cmp Ceq Int.zero iselect + then i0 + else i1) + | _ => Vundef + end + | _ => Vundef + end + | _ => Vundef + end. + +Definition selectfs (v0 : val) (v1 : val) (vselect : val) : val := + match vselect with + | Vint iselect => + match v0 with + | Vsingle i0 => + match v1 with + | Vsingle i1 => + Vsingle (if Int.cmp Ceq Int.zero iselect + then i0 + else i1) + | _ => Vundef + end + | _ => Vundef + end + | _ => Vundef + end. + Definition eval_operation (F V: Type) (genv: Genv.t F V) (sp: val) (op: operation) (vl: list val) (m: mem): option val := @@ -417,6 +453,8 @@ Definition eval_operation | Ocmp c, _ => Some (Val.of_optbool (eval_condition c vl m)) | Oselect, v0::v1::vselect::nil => Some (select v0 v1 vselect) | Oselectl, v0::v1::vselect::nil => Some (selectl v0 v1 vselect) + | Oselectf, v0::v1::vselect::nil => Some (selectf v0 v1 vselect) + | Oselectfs, v0::v1::vselect::nil => Some (selectfs v0 v1 vselect) | _, _ => None end. @@ -608,6 +646,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oselect => (Tint :: Tint :: Tint :: nil, Tint) | Oselectl => (Tlong :: Tlong :: Tint :: nil, Tlong) + | Oselectf => (Tfloat :: Tfloat :: Tint :: nil, Tfloat) + | Oselectfs => (Tsingle :: Tsingle :: Tint :: nil, Tsingle) end. Definition type_of_addressing (addr: addressing) : list typ := @@ -847,6 +887,10 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type). - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial. (* selectl *) - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial. + (* selectf *) + - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial. + (* selectfs *) + - destruct v0; destruct v1; destruct v2; simpl in *; try discriminate; trivial. Qed. End SOUNDNESS. @@ -1381,6 +1425,14 @@ Proof. - inv H3; simpl; try constructor. inv H4; simpl; try constructor. inv H2; simpl; constructor. + (* selectf *) + - inv H3; simpl; try constructor. + inv H4; simpl; try constructor. + inv H2; simpl; constructor. + (* selectfs *) + - inv H3; simpl; try constructor. + inv H4; simpl; try constructor. + inv H2; simpl; constructor. Qed. Lemma eval_addressing_inj: diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index da108ada..122249a4 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -59,6 +59,24 @@ Definition selectl (v0 v1 vselect : aval) : aval := else binop_long (fun x0 x1 => x1) v0 v1 | _ => Vtop end. + +Definition selectf (v0 v1 vselect : aval) : aval := + match vselect with + | I iselect => + if Int.eq Int.zero iselect + then binop_float (fun x0 x1 => x0) v0 v1 + else binop_float (fun x0 x1 => x1) v0 v1 + | _ => Vtop + end. + +Definition selectfs (v0 v1 vselect : aval) : aval := + match vselect with + | I iselect => + if Int.eq Int.zero iselect + then binop_single (fun x0 x1 => x0) v0 v1 + else binop_single (fun x0 x1 => x1) v0 v1 + | _ => Vtop + end. Definition eval_static_operation (op: operation) (vl: list aval): aval := match op, vl with @@ -186,6 +204,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | Ocmp c, _ => of_optbool (eval_static_condition c vl) | Oselect, v0::v1::vselect::nil => select v0 v1 vselect | Oselectl, v0::v1::vselect::nil => selectl v0 v1 vselect + | Oselectf, v0::v1::vselect::nil => selectf v0 v1 vselect + | Oselectfs, v0::v1::vselect::nil => selectfs v0 v1 vselect | _, _ => Vbot end. @@ -265,18 +285,27 @@ Proof. (* select *) - inv H2; simpl; try constructor. + destruct (Int.eq _ _); apply binop_int_sound; trivial. - + destruct (Int.eq _ _); - destruct a1; destruct a0; eauto; constructor. - + destruct (Int.eq _ _); - destruct a1; destruct a0; eauto; constructor. - + destruct (Int.eq _ _); - destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. (* selectl *) - inv H2; simpl; try constructor. + destruct (Int.eq _ _); apply binop_long_sound; trivial. + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + (* selectf *) + - inv H2; simpl; try constructor. + + destruct (Int.eq _ _); apply binop_float_sound; trivial. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + (* selectfs *) + - inv H2; simpl; try constructor. + + destruct (Int.eq _ _); apply binop_single_sound; trivial. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. + + destruct (Int.eq _ _); destruct a1; destruct a0; eauto; constructor. Qed. End SOUNDNESS. |