diff options
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/SelectOp.vp | 10 | ||||
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 145 |
2 files changed, 149 insertions, 6 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 0dad482b..65364579 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -62,11 +62,11 @@ Section SELECT. Context {hf: helper_functions}. (** Stuff for select *) -Definition is_zero_expr (vt : expr) : expr := +Definition is_zero (vt : expr) : expr := Eop (Ocmp (Ccomp Ceq)) (vt:::(Eop (Ointconst Int.zero) Enil):::Enil). -Definition is_nonzero_expr (vt : expr) : expr := +Definition is_nonzero (vt : expr) : expr := Eop (Ocmp (Ccomp Cne)) (vt:::(Eop (Ointconst Int.zero) Enil):::Enil). @@ -76,14 +76,14 @@ Definition bool_to_bitmask (et : expr) : expr := Definition not_bool_to_bitmask (et : expr) : expr := Eop Osub (et:::(Eop (Ointconst Int.one) Enil):::Enil). -Definition ternary_expand (et e0 e1 : expr) : expr := +Definition ternary_expand (e0 e1 et : expr) : expr := Eop Oor ((Eop Oand ((not_bool_to_bitmask et):::e1:::Enil))::: (Eop Oand ((bool_to_bitmask et):::e0:::Enil))::: Enil). -Definition select_or_expand (et e0 e1 : expr) : expr := - ternary_expand (is_nonzero_expr et) e0 e1. +Definition select_or_expand (e0 e1 et: expr) : expr := + ternary_expand e0 e1 (is_zero et). (** ** Constants **) diff --git a/mppa_k1c/SelectOpproof.v b/mppa_k1c/SelectOpproof.v index 89af39ee..0637256d 100644 --- a/mppa_k1c/SelectOpproof.v +++ b/mppa_k1c/SelectOpproof.v @@ -92,7 +92,7 @@ Let ge := Genv.globalenv prog. Variable sp: val. Variable e: env. Variable m: mem. - + (* Helper lemmas - from SplitLongproof.v *) Ltac UseHelper := decompose [Logic.and] arith_helpers_correct; eauto. @@ -163,6 +163,149 @@ Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> va eval_expr ge sp e m le b y -> exists v, eval_expr ge sp e m le (cstr a b) v /\ Val.lessdef (sem x y) v. +Definition is_zero_sem (vt : val) : val := + match vt with + | Vint x => Vint (if Int.eq x Int.zero then Int.one else Int.zero) + | _ => Vundef + end. + +Theorem eval_is_zero: unary_constructor_sound is_zero is_zero_sem. +Proof. + red; intros. + unfold is_zero_sem, is_zero; simpl. + TrivialExists. + - constructor. + + exact H. + + constructor; econstructor; constructor. + - simpl. + destruct x; simpl; try congruence. + unfold Vtrue, Vfalse. + predSpec Int.eq Int.eq_spec i Int.zero; reflexivity. +Qed. + +Definition is_nonzero_sem (vt : val) : val := + match vt with + | Vint x => Vint (if Int.eq x Int.zero then Int.zero else Int.one) + | _ => Vundef + end. + +Theorem eval_is_nonzero: unary_constructor_sound is_nonzero is_nonzero_sem. +Proof. + red; intros. + unfold is_zero_sem, is_zero; simpl. + TrivialExists. + - constructor. + + exact H. + + constructor; econstructor; constructor. + - simpl. + destruct x; simpl; try congruence. + unfold Vtrue, Vfalse. + predSpec Int.eq Int.eq_spec i Int.zero; reflexivity. +Qed. + + +Definition ternary_constructor_sound (cstr: expr -> expr -> expr -> expr) (sem: val -> val -> val -> val) : Prop := + forall le a x b y c z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + eval_expr ge sp e m le c z -> + exists v, eval_expr ge sp e m le (cstr a b c) v /\ Val.lessdef (sem x y z) v. + +Lemma int_eq_commut : forall x y, + Int.eq x y = Int.eq y x. +Proof. + unfold Int.eq. + intros. + unfold zeq. + destruct (Z.eq_dec _ _); destruct (Z.eq_dec _ _); congruence. +Qed. + +Theorem eval_select_or_expand : ternary_constructor_sound select_or_expand select. +Proof. + unfold ternary_constructor_sound, ternary_expand. + intros. + TrivialExists. + constructor. + - econstructor. + constructor. + econstructor. + constructor. + unfold is_zero. + econstructor. + constructor. + eassumption. + constructor. + econstructor. + constructor. + simpl. + reflexivity. + constructor. + simpl. + reflexivity. + constructor. + econstructor. + constructor. + simpl. + reflexivity. + constructor. + simpl. + reflexivity. + constructor. + eassumption. + constructor. + simpl. + reflexivity. + - constructor. + econstructor. + constructor. + econstructor. + constructor. + unfold is_zero. + econstructor. + constructor. + eassumption. + constructor. + econstructor. + constructor. + simpl. + reflexivity. + constructor. + simpl. + reflexivity. + constructor. + simpl. + reflexivity. + constructor. + eassumption. + constructor. + simpl. + reflexivity. + constructor. + - simpl. + unfold select. + destruct z; simpl; trivial. + destruct x; simpl; trivial; try (destruct (Int.eq i Int.zero); simpl; rewrite <- (Val.or_commut Vundef); simpl; reflexivity). + destruct y; simpl; trivial; + try (destruct (Int.eq i Int.zero); simpl; reflexivity). + rewrite int_eq_commut. predSpec Int.eq Int.eq_spec Int.zero i. + * simpl. + rewrite Int.sub_idem. + rewrite Int.and_commut. + rewrite Int.and_zero. + rewrite Int.or_commut. + rewrite Int.or_zero. + rewrite Int.and_commut. + rewrite Int.and_mone. + reflexivity. + * simpl. + rewrite Int.and_commut. + rewrite Int.and_mone. + rewrite Int.and_commut. + rewrite Int.and_zero. + rewrite Int.or_zero. + reflexivity. +Qed. + Theorem eval_addrsymbol: forall le id ofs, exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (Genv.symbol_address ge id ofs) v. |