diff options
Diffstat (limited to 'mppa_k1c/SelectOpproof.v')
-rw-r--r-- | mppa_k1c/SelectOpproof.v | 145 |
1 files changed, 144 insertions, 1 deletions
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. |