From 68a6d0dd0ea5774529d823fb9a9ca981c1ecebb0 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 4 Jun 2019 22:58:34 +0200 Subject: osel imm --- mppa_k1c/Asmblockgen.v | 43 ++++++++++++++++++++++++++++++++ mppa_k1c/Asmblockgenproof1.v | 48 ++++++++++++++++++++++++++++++++++++ mppa_k1c/Machregs.v | 2 +- mppa_k1c/Op.v | 12 ++++----- mppa_k1c/PostpassSchedulingOracle.ml | 2 +- mppa_k1c/SelectOp.vp | 10 ++++++-- mppa_k1c/SelectOpproof.v | 19 ++++++-------- mppa_k1c/ValueAOp.v | 4 +-- 8 files changed, 117 insertions(+), 23 deletions(-) (limited to 'mppa_k1c') diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 04ce13e7..e5b9b35a 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -375,6 +375,34 @@ Definition conditional_move (cond0 : condition0) (rc rd rs : ireg) : OK (PArith (Pcmoveu bt rd rc rs)) end). +Definition conditional_move_imm32 (cond0 : condition0) (rc rd : ireg) (imm : int) : res basic := + match cond0 with + | Ccomp0 cmp => + OK (PArith (Pcmoveiw (btest_for_cmpswz cmp) rd rc imm)) + | Ccompu0 cmp => + do bt <- btest_for_cmpuwz cmp; + OK (PArith (Pcmoveuiw bt rd rc imm)) + | Ccompl0 cmp => + OK (PArith (Pcmoveiw (btest_for_cmpsdz cmp) rd rc imm)) + | Ccomplu0 cmp => + do bt <- btest_for_cmpudz cmp; + OK (PArith (Pcmoveuiw bt rd rc imm)) + end. + +Definition conditional_move_imm64 (cond0 : condition0) (rc rd : ireg) (imm : int64) : res basic := + match cond0 with + | Ccomp0 cmp => + OK (PArith (Pcmoveil (btest_for_cmpswz cmp) rd rc imm)) + | Ccompu0 cmp => + do bt <- btest_for_cmpuwz cmp; + OK (PArith (Pcmoveuil bt rd rc imm)) + | Ccompl0 cmp => + OK (PArith (Pcmoveil (btest_for_cmpsdz cmp) rd rc imm)) + | Ccomplu0 cmp => + do bt <- btest_for_cmpudz cmp; + OK (PArith (Pcmoveuil bt rd rc imm)) + end. + Definition transl_cond_op (cond: condition) (rd: ireg) (args: list mreg) (k: bcode) := match cond, args with @@ -847,6 +875,21 @@ Definition transl_op do rC <- ireg_of aC; do op <- conditional_move (negate_condition0 cond0) rC rT rF; OK (op ::i k) + + | Oselimm cond0 imm, aT :: aC :: nil => + assertion (mreg_eq aT res); + do rT <- ireg_of aT; + do rC <- ireg_of aC; + do op <- conditional_move_imm32 (negate_condition0 cond0) rC rT imm; + OK (op ::i k) + + + | Osellimm cond0 imm, aT :: aC :: nil => + assertion (mreg_eq aT res); + do rT <- ireg_of aT; + do rC <- ireg_of aC; + do op <- conditional_move_imm64 (negate_condition0 cond0) rC rT imm; + OK (op ::i k) | _, _ => Error(msg "Asmgenblock.transl_op") diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v index 8939cc30..bc549b4a 100644 --- a/mppa_k1c/Asmblockgenproof1.v +++ b/mppa_k1c/Asmblockgenproof1.v @@ -1799,6 +1799,54 @@ Opaque Int.eq. try destruct (_ || _); trivial; try apply Val.lessdef_normalize. + +- (* Oselimm *) + unfold conditional_move_imm32 in *. + destruct c0; simpl in *. + + all: + destruct c; simpl in *; inv EQ0; + econstructor; split; try (apply exec_straight_one; constructor); + split; try (simpl; intros; rewrite Pregmap.gso; trivial; assumption); + unfold Val.select; simpl; + unfold cmove, cmoveu; + rewrite Pregmap.gss; + destruct (rs x0); simpl; trivial; + try rewrite int_ltu_to_neq; + try rewrite int64_ltu_to_neq; + try change (Int64.eq Int64.zero Int64.zero) with true; + try destruct Archi.ptr64; + repeat rewrite if_neg; + simpl; + trivial; + try destruct (_ || _); + trivial; + try apply Val.lessdef_normalize. + + +- (* Osellimm *) + unfold conditional_move_imm64 in *. + destruct c0; simpl in *. + + all: + destruct c; simpl in *; inv EQ0; + econstructor; split; try (apply exec_straight_one; constructor); + split; try (simpl; intros; rewrite Pregmap.gso; trivial; assumption); + unfold Val.select; simpl; + unfold cmove, cmoveu; + rewrite Pregmap.gss; + destruct (rs x0); simpl; trivial; + try rewrite int_ltu_to_neq; + try rewrite int64_ltu_to_neq; + try change (Int64.eq Int64.zero Int64.zero) with true; + try destruct Archi.ptr64; + repeat rewrite if_neg; + simpl; + trivial; + try destruct (_ || _); + trivial; + try apply Val.lessdef_normalize. + Qed. (** Memory accesses *) diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index ee3a63c7..5a7d42b4 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -216,7 +216,7 @@ Definition two_address_op (op: operation) : bool := | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Omsub | Omsubl - | Osel _ _ + | Osel _ _ | Oselimm _ _ | Osellimm _ _ | Oinsf _ _ | Oinsfl _ _ => true | _ => false end. diff --git a/mppa_k1c/Op.v b/mppa_k1c/Op.v index 1b3a839f..35fbb596 100644 --- a/mppa_k1c/Op.v +++ b/mppa_k1c/Op.v @@ -456,8 +456,8 @@ Definition eval_operation | (Oinsf stop start), v0::v1::nil => Some (insf stop start v0 v1) | (Oinsfl stop start), v0::v1::nil => Some (insfl stop start v0 v1) | Osel c ty, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 v2 ty) - | Oselimm c imm, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vint imm) Tint) - | Osellimm c imm, v1::v2::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vlong imm) Tlong) + | Oselimm c imm, v1::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vint imm) Tint) + | Osellimm c imm, v1::vc::nil => Some(Val.select (eval_condition0 c vc m) v1 (Vlong imm) Tlong) | _, _ => None end. @@ -662,8 +662,8 @@ Definition type_of_operation (op: operation) : list typ * typ := | Oinsf _ _ => (Tint :: Tint :: nil, Tint) | Oinsfl _ _ => (Tlong :: Tlong :: nil, Tlong) | Osel c ty => (ty :: ty :: arg_type_of_condition0 c :: nil, ty) - | Oselimm c ty => (Tint :: Tint :: arg_type_of_condition0 c :: nil, Tint) - | Osellimm c ty => (Tlong :: Tlong :: arg_type_of_condition0 c :: nil, Tlong) + | Oselimm c ty => (Tint :: arg_type_of_condition0 c :: nil, Tint) + | Osellimm c ty => (Tlong :: arg_type_of_condition0 c :: nil, Tlong) end. (* FIXME: two Tptr ?! *) @@ -1614,7 +1614,7 @@ Proof. (* Oselimm *) - apply Val.select_inject; trivial. - destruct (eval_condition0 c0 v2 m1) eqn:Hcond. + destruct (eval_condition0 _ _ _) eqn:Hcond. + right. symmetry. eapply eval_condition0_inj; eassumption. @@ -1622,7 +1622,7 @@ Proof. (* Osellimm *) - apply Val.select_inject; trivial. - destruct (eval_condition0 c0 v2 m1) eqn:Hcond. + destruct (eval_condition0 _ _ _) eqn:Hcond. + right. symmetry. eapply eval_condition0_inj; eassumption. diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index 78af896a..6ccc4e97 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -551,7 +551,7 @@ let ab_inst_to_real = function | "Pfixedudrzz" -> Fixedudz | "Pfixeddrzz_i32" -> Fixeddz | "Pfixedudrzz_i32" -> Fixedudz - | "Pcmove" | "Pcmoveu" -> Cmoved + | "Pcmove" | "Pcmoveu" | "Pcmoveiw" | "Pcmoveuiw" | "Pcmoveil" | "Pcmoveuil" -> Cmoved | "Plb" -> Lbs | "Plbu" -> Lbz diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 01985060..2618983b 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -91,8 +91,14 @@ Nondetfunction cond_to_condition0 (cond : condition) (args : exprlist) := end. (** Ternary operator *) -Definition select0 (ty : typ) (cond0 : condition0) (e1 e2 eC: expr) := - (Eop (Osel cond0 ty) (e1 ::: e2 ::: eC ::: Enil)). +Nondetfunction select0 (ty : typ) (cond0 : condition0) (e1 e2 e3: expr) := + match ty, cond0, e1, e2, e3 with + | Tint, cond0, e1, (Eop (Ointconst imm) Enil), e3 => + (Eop (Oselimm cond0 imm) (e1 ::: e3 ::: Enil)) + | Tlong, cond0, e1, (Eop (Olongconst imm) Enil), e3 => + (Eop (Osellimm cond0 imm) (e1 ::: e3 ::: Enil)) + | _, _, _ => (Eop (Osel cond0 ty) (e1 ::: e2 ::: e3 ::: Enil)) + end. Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr) : option expr := Some( diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 4047048c..39ad763e 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -1451,12 +1451,10 @@ Lemma eval_select0: /\ Val.lessdef (Val.select (eval_condition0 cond0 vc m) v1 v2 ty) v. Proof. intros. - econstructor; split. - { - unfold select0. - repeat (try econstructor; try eassumption). - } - constructor. + unfold select0. + destruct (select0_match ty cond0 a1 a2 ac). + all: InvEval; econstructor; split; + repeat (try econstructor; try eassumption). Qed. Lemma bool_cond0_ne: @@ -1578,12 +1576,11 @@ Proof. erewrite <- (bool_cond0_ne (Val.cmplu_bool (Mem.valid_pointer m) c v0 (Vlong x))). eapply eval_select0; repeat (try econstructor; try eassumption). } - TrivialExists. - repeat (try econstructor; try eassumption). + erewrite <- (bool_cond0_ne (Some b)). + eapply eval_select0; repeat (try econstructor; try eassumption). + rewrite <- HeC. simpl. - f_equal. - rewrite HeC. - destruct b; simpl; reflexivity. + reflexivity. Qed. (* floating-point division *) diff --git a/mppa_k1c/ValueAOp.v b/mppa_k1c/ValueAOp.v index daceab8b..439138da 100644 --- a/mppa_k1c/ValueAOp.v +++ b/mppa_k1c/ValueAOp.v @@ -265,8 +265,8 @@ Definition eval_static_operation (op: operation) (vl: list aval): aval := | (Oinsf stop start), v0::v1::nil => eval_static_insf stop start v0 v1 | (Oinsfl stop start), v0::v1::nil => eval_static_insfl stop start v0 v1 | Osel c ty, v1::v2::vc::nil => select (eval_static_condition0 c vc) v1 v2 - | Oselimm c imm, v1::v2::vc::nil => select (eval_static_condition0 c vc) v1 (I imm) - | Osellimm c imm, v1::v2::vc::nil => select (eval_static_condition0 c vc) v1 (L imm) + | Oselimm c imm, v1::vc::nil => select (eval_static_condition0 c vc) v1 (I imm) + | Osellimm c imm, v1::vc::nil => select (eval_static_condition0 c vc) v1 (L imm) | _, _ => Vbot end. -- cgit