From a82c9c0e4a0b8e37c9c3ea5ae99714982563606f Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 14 Jan 2012 14:23:26 +0000 Subject: Merge of the nonstrict-ops branch: - Most RTL operators now evaluate to Some Vundef instead of None when undefined behavior occurs. - More aggressive instruction selection. - "Bertotization" of pattern-matchings now implemented by a proper preprocessor. - Cast optimization moved to cfrontend/Cminorgen; removed backend/CastOptim. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1790 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/SelectOpproof.v | 1261 ++++++++++++++++++++------------------------------- 1 file changed, 503 insertions(+), 758 deletions(-) (limited to 'arm/SelectOpproof.v') diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index 9ecf1de8..fa416820 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -44,8 +44,6 @@ Variable m: mem. Ltac EvalOp := eapply eval_Eop; eauto with evalexpr. -Ltac TrivialOp cstr := unfold cstr; intros; EvalOp. - Ltac InvEval1 := match goal with | [ H: (eval_expr _ _ _ _ _ (Eop _ Enil) _) |- _ ] => @@ -78,6 +76,11 @@ Ltac InvEval2 := Ltac InvEval := InvEval1; InvEval2; InvEval2. +Ltac TrivialExists := + match goal with + | [ |- exists v, _ /\ Val.lessdef ?a v ] => exists a; split; [EvalOp | auto] + end. + (** * Correctness of the smart constructors *) (** We now show that the code generated by "smart constructor" functions @@ -100,440 +103,373 @@ Ltac InvEval := InvEval1; InvEval2; InvEval2. by the smart constructor. *) +Definition unary_constructor_sound (cstr: expr -> expr) (sem: val -> val) : Prop := + forall le a x, + eval_expr ge sp e m le a x -> + exists v, eval_expr ge sp e m le (cstr a) v /\ Val.lessdef (sem x) v. + +Definition binary_constructor_sound (cstr: expr -> expr -> expr) (sem: val -> val -> val) : Prop := + forall le a x b y, + eval_expr ge sp e m le a x -> + 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. + Theorem eval_addrsymbol: - forall le id ofs b, - Genv.find_symbol ge id = Some b -> - eval_expr ge sp e m le (addrsymbol id ofs) (Vptr b ofs). + forall le id ofs, + exists v, eval_expr ge sp e m le (addrsymbol id ofs) v /\ Val.lessdef (symbol_address ge id ofs) v. Proof. - intros. unfold addrsymbol. econstructor. constructor. - simpl. rewrite H. auto. + intros. unfold addrsymbol. econstructor; split. + EvalOp. simpl; eauto. + auto. Qed. Theorem eval_addrstack: - forall le ofs b n, - sp = Vptr b n -> - eval_expr ge sp e m le (addrstack ofs) (Vptr b (Int.add n ofs)). + forall le ofs, + exists v, eval_expr ge sp e m le (addrstack ofs) v /\ Val.lessdef (Val.add sp (Vint ofs)) v. Proof. - intros. unfold addrstack. econstructor. constructor. - simpl. unfold offset_sp. rewrite H. auto. + intros. unfold addrstack. econstructor; split. + EvalOp. simpl; eauto. + auto. Qed. -Theorem eval_notint: - forall le a x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (notint a) (Vint (Int.not x)). +Theorem eval_notint: unary_constructor_sound notint Val.notint. Proof. - unfold notint; intros until x; case (notint_match a); intros; InvEval. - EvalOp. simpl. congruence. - subst x. rewrite Int.not_involutive. auto. - EvalOp. simpl. subst x. rewrite Int.not_involutive. auto. - EvalOp. + unfold notint; red; intros until x; case (notint_match a); intros; InvEval. + subst x. TrivialExists. + exists v1; split; auto. subst. destruct v1; simpl; auto. rewrite Int.not_involutive; auto. + exists (eval_shift s v1); split. EvalOp. subst x. destruct (eval_shift s v1); simpl; auto. rewrite Int.not_involutive; auto. + TrivialExists. Qed. -Lemma eval_notbool_base: - forall le a v b, - eval_expr ge sp e m le a v -> - Val.bool_of_val v b -> - eval_expr ge sp e m le (notbool_base a) (Val.of_bool (negb b)). -Proof. - TrivialOp notbool_base. simpl. - inv H0. - rewrite Int.eq_false; auto. - rewrite Int.eq_true; auto. - reflexivity. -Qed. - -Hint Resolve Val.bool_of_true_val Val.bool_of_false_val - Val.bool_of_true_val_inv Val.bool_of_false_val_inv: valboolof. - -Theorem eval_notbool: - forall le a v b, - eval_expr ge sp e m le a v -> - Val.bool_of_val v b -> - eval_expr ge sp e m le (notbool a) (Val.of_bool (negb b)). +Theorem eval_notbool: unary_constructor_sound notbool Val.notbool. Proof. - induction a; simpl; intros; try (eapply eval_notbool_base; eauto). - destruct o; try (eapply eval_notbool_base; eauto). + assert (DFL: + forall le a x, + eval_expr ge sp e m le a x -> + exists v, eval_expr ge sp e m le (Eop (Ocmp (Ccompuimm Ceq Int.zero)) (a ::: Enil)) v + /\ Val.lessdef (Val.notbool x) v). + intros. TrivialExists. simpl. destruct x; simpl; auto. - destruct e0. InvEval. - inv H0. rewrite Int.eq_false; auto. - simpl; eauto with evalexpr. - rewrite Int.eq_true; simpl; eauto with evalexpr. - eapply eval_notbool_base; eauto. - - inv H. eapply eval_Eop; eauto. - simpl. assert (eval_condition c vl m = Some b). - generalize H6. simpl. - case (eval_condition c vl); intros. - destruct b0; inv H1; inversion H0; auto; congruence. - congruence. - rewrite (Op.eval_negate_condition _ _ _ H). - destruct b; reflexivity. - - inv H. eapply eval_Econdition; eauto. - destruct v1; eauto. + red. induction a; simpl; intros; eauto. destruct o; eauto. +(* intconst *) + destruct e0; eauto. InvEval. TrivialExists. simpl. destruct (Int.eq i Int.zero); auto. +(* cmp *) + inv H. simpl in H5. + destruct (eval_condition c vl m) as []_eqn. + TrivialExists. simpl. rewrite (eval_negate_condition _ _ _ Heqo). destruct b; inv H5; auto. + inv H5. simpl. + destruct (eval_condition (negate_condition c) vl m) as []_eqn. + destruct b; [exists Vtrue | exists Vfalse]; split; auto; EvalOp; simpl. rewrite Heqo0; auto. rewrite Heqo0; auto. + exists Vundef; split; auto; EvalOp; simpl. rewrite Heqo0; auto. +(* condition *) + inv H. destruct v1. + exploit IHa1; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. + exploit IHa2; eauto. intros [v [A B]]. exists v; split; auto. eapply eval_Econdition; eauto. Qed. Theorem eval_addimm: - forall le n a x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (addimm n a) (Vint (Int.add x n)). -Proof. - unfold addimm; intros until x. - generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro. - subst n. rewrite Int.add_zero. auto. - case (addimm_match a); intros; InvEval; EvalOp; simpl. + forall n, unary_constructor_sound (addimm n) (fun x => Val.add x (Vint n)). +Proof. + red; unfold addimm; intros until x. + predSpec Int.eq Int.eq_spec n Int.zero. + subst n. intros. exists x; split; auto. + destruct x; simpl; auto. rewrite Int.add_zero. auto. rewrite Int.add_zero. auto. + case (addimm_match a); intros; InvEval; simpl; TrivialExists; simpl. rewrite Int.add_commut. auto. - destruct (Genv.find_symbol ge s); discriminate. - destruct sp; simpl in H1; discriminate. - subst x. rewrite Int.add_assoc. decEq; decEq; decEq. apply Int.add_commut. + unfold symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. rewrite Int.add_commut; auto. + rewrite Val.add_assoc. rewrite Int.add_commut. auto. + subst x. rewrite Val.add_assoc. rewrite Int.add_commut. auto. Qed. -Theorem eval_addimm_ptr: - forall le n a b ofs, - eval_expr ge sp e m le a (Vptr b ofs) -> - eval_expr ge sp e m le (addimm n a) (Vptr b (Int.add ofs n)). -Proof. - unfold addimm; intros until ofs. - generalize (Int.eq_spec n Int.zero). case (Int.eq n Int.zero); intro. - subst n. rewrite Int.add_zero. auto. - case (addimm_match a); intros; InvEval; EvalOp; simpl. - destruct (Genv.find_symbol ge s). - rewrite Int.add_commut. congruence. - discriminate. - destruct sp; simpl in H1; try discriminate. - inv H1. simpl. decEq. decEq. - rewrite Int.add_assoc. decEq. apply Int.add_commut. - subst. rewrite (Int.add_commut n m0). rewrite Int.add_assoc. auto. -Qed. - -Theorem eval_add: - forall le a b x y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (add a b) (Vint (Int.add x y)). +Theorem eval_add: binary_constructor_sound add Val.add. Proof. - intros until y. + red; intros until y. unfold add; case (add_match a b); intros; InvEval. - rewrite Int.add_commut. apply eval_addimm. auto. - replace (Int.add x y) with (Int.add (Int.add i0 i) (Int.add n1 n2)). - apply eval_addimm. EvalOp. - subst x; subst y. - repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. - replace (Int.add x y) with (Int.add (Int.add i y) n1). - apply eval_addimm. EvalOp. - subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - apply eval_addimm. auto. - replace (Int.add x y) with (Int.add (Int.add x i) n2). - apply eval_addimm. EvalOp. - subst y. rewrite Int.add_assoc. auto. - EvalOp. simpl. subst x. rewrite Int.add_commut. auto. - EvalOp. simpl. congruence. - EvalOp. -Qed. - -Theorem eval_add_ptr: - forall le a b p x y, - eval_expr ge sp e m le a (Vptr p x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (add a b) (Vptr p (Int.add x y)). -Proof. - intros until y. unfold add; case (add_match a b); intros; InvEval. - replace (Int.add x y) with (Int.add (Int.add i0 i) (Int.add n1 n2)). - apply eval_addimm_ptr. subst b0. EvalOp. - subst x; subst y. - repeat rewrite Int.add_assoc. decEq. apply Int.add_permut. - replace (Int.add x y) with (Int.add (Int.add i y) n1). - apply eval_addimm_ptr. subst b0. EvalOp. - subst x. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - apply eval_addimm_ptr. auto. - replace (Int.add x y) with (Int.add (Int.add x i) n2). - apply eval_addimm_ptr. EvalOp. - subst y. rewrite Int.add_assoc. auto. - EvalOp. simpl. congruence. - EvalOp. -Qed. - -Theorem eval_add_ptr_2: - forall le a b x p y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vptr p y) -> - eval_expr ge sp e m le (add a b) (Vptr p (Int.add y x)). -Proof. - intros until y. unfold add; case (add_match a b); intros; InvEval. - apply eval_addimm_ptr. auto. - replace (Int.add y x) with (Int.add (Int.add i i0) (Int.add n1 n2)). - apply eval_addimm_ptr. subst b0. EvalOp. - subst x; subst y. - repeat rewrite Int.add_assoc. decEq. - rewrite (Int.add_commut n1 n2). apply Int.add_permut. - replace (Int.add y x) with (Int.add (Int.add y i) n1). - apply eval_addimm_ptr. EvalOp. - subst x. repeat rewrite Int.add_assoc. auto. - replace (Int.add y x) with (Int.add (Int.add i x) n2). - apply eval_addimm_ptr. EvalOp. subst b0; reflexivity. - subst y. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut. - EvalOp. simpl. congruence. - EvalOp. -Qed. - -Theorem eval_sub: - forall le a b x y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)). -Proof. - intros until y. - unfold sub; case (sub_match a b); intros; InvEval. - rewrite Int.sub_add_opp. - apply eval_addimm. assumption. - replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). - apply eval_addimm. EvalOp. - subst x; subst y. - repeat rewrite Int.sub_add_opp. - repeat rewrite Int.add_assoc. decEq. - rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. - replace (Int.sub x y) with (Int.add (Int.sub i y) n1). - apply eval_addimm. EvalOp. - subst x. rewrite Int.sub_add_l. auto. - replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). - apply eval_addimm. EvalOp. - subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. - EvalOp. - EvalOp. simpl. congruence. - EvalOp. simpl. congruence. - EvalOp. -Qed. - -Theorem eval_sub_ptr_int: - forall le a b p x y, - eval_expr ge sp e m le a (Vptr p x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (sub a b) (Vptr p (Int.sub x y)). -Proof. - intros until y. + rewrite Val.add_commut. apply eval_addimm; auto. + subst. + replace (Val.add (Val.add v1 (Vint n1)) (Val.add v0 (Vint n2))) + with (Val.add (Val.add v1 v0) (Val.add (Vint n1) (Vint n2))). + apply eval_addimm. EvalOp. + repeat rewrite Val.add_assoc. decEq. apply Val.add_permut. + subst. + replace (Val.add (Val.add v1 (Vint n1)) y) + with (Val.add (Val.add v1 y) (Vint n1)). + apply eval_addimm. EvalOp. + repeat rewrite Val.add_assoc. decEq. apply Val.add_commut. + apply eval_addimm; auto. + subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp. + subst. rewrite Val.add_commut. TrivialExists. + subst. TrivialExists. + TrivialExists. +Qed. + +Theorem eval_sub: binary_constructor_sound sub Val.sub. +Proof. + red; intros until y. unfold sub; case (sub_match a b); intros; InvEval. - rewrite Int.sub_add_opp. - apply eval_addimm_ptr. assumption. - subst b0. replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). - apply eval_addimm_ptr. EvalOp. - subst x; subst y. - repeat rewrite Int.sub_add_opp. - repeat rewrite Int.add_assoc. decEq. - rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. - subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1). - apply eval_addimm_ptr. EvalOp. - subst x. rewrite Int.sub_add_l. auto. - replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). - apply eval_addimm_ptr. EvalOp. - subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. - EvalOp. simpl. congruence. - EvalOp. + rewrite Val.sub_add_opp. apply eval_addimm; auto. + subst. rewrite Val.sub_add_l. rewrite Val.sub_add_r. + rewrite Val.add_assoc. simpl. rewrite Int.add_commut. rewrite <- Int.sub_add_opp. + apply eval_addimm; EvalOp. + subst. rewrite Val.sub_add_l. apply eval_addimm; EvalOp. + subst. rewrite Val.sub_add_r. apply eval_addimm; EvalOp. + TrivialExists. + subst. TrivialExists. + subst. TrivialExists. + TrivialExists. Qed. -Theorem eval_sub_ptr_ptr: - forall le a b p x y, - eval_expr ge sp e m le a (Vptr p x) -> - eval_expr ge sp e m le b (Vptr p y) -> - eval_expr ge sp e m le (sub a b) (Vint (Int.sub x y)). +Theorem eval_negint: unary_constructor_sound negint (fun v => Val.sub Vzero v). Proof. - intros until y. - unfold sub; case (sub_match a b); intros; InvEval. - replace (Int.sub x y) with (Int.add (Int.sub i0 i) (Int.sub n1 n2)). - apply eval_addimm. EvalOp. - simpl; unfold eq_block. subst b0; subst b1; rewrite zeq_true. auto. - subst x; subst y. - repeat rewrite Int.sub_add_opp. - repeat rewrite Int.add_assoc. decEq. - rewrite Int.add_permut. decEq. symmetry. apply Int.neg_add_distr. - subst b0. replace (Int.sub x y) with (Int.add (Int.sub i y) n1). - apply eval_addimm. EvalOp. - simpl. unfold eq_block. rewrite zeq_true. auto. - subst x. rewrite Int.sub_add_l. auto. - subst b0. replace (Int.sub x y) with (Int.add (Int.sub x i) (Int.neg n2)). - apply eval_addimm. EvalOp. - simpl. unfold eq_block. rewrite zeq_true. auto. - subst y. rewrite (Int.add_commut i n2). symmetry. apply Int.sub_add_r. - EvalOp. simpl. unfold eq_block. rewrite zeq_true. auto. + red; intros. unfold negint. TrivialExists. Qed. Theorem eval_shlimm: - forall le a n x, - eval_expr ge sp e m le a (Vint x) -> - Int.ltu n Int.iwordsize = true -> - eval_expr ge sp e m le (shlimm a n) (Vint (Int.shl x n)). -Proof. - intros until x. unfold shlimm, is_shift_amount. - generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. - intros. subst n. rewrite Int.shl_zero. auto. - destruct (is_shift_amount_aux n). simpl. - case (shlimm_match a); intros; InvEval. - EvalOp. - destruct (is_shift_amount_aux (Int.add n (s_amount n1))). - EvalOp. simpl. subst x. - decEq. decEq. symmetry. rewrite Int.add_commut. apply Int.shl_shl. - apply s_amount_ltu. auto. - rewrite Int.add_commut. auto. - EvalOp. econstructor. EvalOp. simpl. reflexivity. constructor. - simpl. congruence. - EvalOp. - congruence. + forall n, unary_constructor_sound (fun a => shlimm a n) + (fun x => Val.shl x (Vint n)). +Proof. +Opaque mk_shift_amount. + red; intros until x. unfold shlimm. + predSpec Int.eq Int.eq_spec n Int.zero. + intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shl_zero; auto. + destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl. + destruct (shlimm_match a); intros. + InvEval. simpl; rewrite Heqb. TrivialExists. + destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn. + InvEval. subst x. exists (Val.shl v1 (Vint (Int.add n n1))); split. EvalOp. + simpl. rewrite mk_shift_amount_eq; auto. + destruct v1; simpl; auto. rewrite s_range. simpl. rewrite Heqb. rewrite Heqb0. + rewrite Int.add_commut. rewrite Int.shl_shl; auto. apply s_range. rewrite Int.add_commut; auto. + TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. + TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. + intros; TrivialExists. simpl. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto. +Qed. + + Theorem eval_shrimm: + forall n, unary_constructor_sound (fun a => shrimm a n) + (fun x => Val.shr x (Vint n)). +Proof. + red; intros until x. unfold shrimm. + predSpec Int.eq Int.eq_spec n Int.zero. + intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shr_zero; auto. + destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl. + destruct (shrimm_match a); intros. + InvEval. simpl; rewrite Heqb. TrivialExists. + destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn. + InvEval. subst x. exists (Val.shr v1 (Vint (Int.add n n1))); split. EvalOp. + simpl. rewrite mk_shift_amount_eq; auto. + destruct v1; simpl; auto. rewrite s_range. simpl. rewrite Heqb. rewrite Heqb0. + rewrite Int.add_commut. rewrite Int.shr_shr; auto. apply s_range. rewrite Int.add_commut; auto. + TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. + TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. + intros; TrivialExists. simpl. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto. Qed. Theorem eval_shruimm: - forall le a n x, - eval_expr ge sp e m le a (Vint x) -> - Int.ltu n Int.iwordsize = true -> - eval_expr ge sp e m le (shruimm a n) (Vint (Int.shru x n)). -Proof. - intros until x. unfold shruimm, is_shift_amount. - generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. - intros. subst n. rewrite Int.shru_zero. auto. - destruct (is_shift_amount_aux n). simpl. - case (shruimm_match a); intros; InvEval. - EvalOp. - destruct (is_shift_amount_aux (Int.add n (s_amount n1))). - EvalOp. simpl. subst x. - decEq. decEq. symmetry. rewrite Int.add_commut. apply Int.shru_shru. - apply s_amount_ltu. auto. - rewrite Int.add_commut. auto. - EvalOp. econstructor. EvalOp. simpl. reflexivity. constructor. - simpl. congruence. - EvalOp. - congruence. -Qed. - -Theorem eval_shrimm: - forall le a n x, - eval_expr ge sp e m le a (Vint x) -> - Int.ltu n Int.iwordsize = true -> - eval_expr ge sp e m le (shrimm a n) (Vint (Int.shr x n)). -Proof. - intros until x. unfold shrimm, is_shift_amount. - generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. - intros. subst n. rewrite Int.shr_zero. auto. - destruct (is_shift_amount_aux n). simpl. - case (shrimm_match a); intros; InvEval. - EvalOp. - destruct (is_shift_amount_aux (Int.add n (s_amount n1))). - EvalOp. simpl. subst x. - decEq. decEq. symmetry. rewrite Int.add_commut. apply Int.shr_shr. - apply s_amount_ltu. auto. - rewrite Int.add_commut. auto. - EvalOp. econstructor. EvalOp. simpl. reflexivity. constructor. - simpl. congruence. - EvalOp. - congruence. + forall n, unary_constructor_sound (fun a => shruimm a n) + (fun x => Val.shru x (Vint n)). +Proof. + red; intros until x. unfold shruimm. + predSpec Int.eq Int.eq_spec n Int.zero. + intros; subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.shru_zero; auto. + destruct (Int.ltu n Int.iwordsize) as []_eqn; simpl. + destruct (shruimm_match a); intros. + InvEval. simpl; rewrite Heqb. TrivialExists. + destruct (Int.ltu (Int.add n n1) Int.iwordsize) as []_eqn. + InvEval. subst x. exists (Val.shru v1 (Vint (Int.add n n1))); split. EvalOp. + simpl. rewrite mk_shift_amount_eq; auto. + destruct v1; simpl; auto. destruct (Int.ltu n1 Int.iwordsize) as []_eqn; simpl; auto. + rewrite Heqb; rewrite Heqb0. rewrite Int.add_commut. rewrite Int.shru_shru; auto. rewrite Int.add_commut; auto. + TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. + TrivialExists. simpl. rewrite mk_shift_amount_eq; auto. + intros; TrivialExists. simpl. constructor. eauto. constructor. EvalOp. simpl; eauto. constructor. auto. Qed. Lemma eval_mulimm_base: - forall le a n x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (mulimm_base n a) (Vint (Int.mul x n)). + forall n, unary_constructor_sound (mulimm_base n) (fun x => Val.mul x (Vint n)). Proof. - intros; unfold mulimm_base. + intros; red; intros; unfold mulimm_base. + assert (DFL: exists v, eval_expr ge sp e m le (Eop Omul (Eop (Ointconst n) Enil ::: a ::: Enil)) v /\ Val.lessdef (Val.mul x (Vint n)) v). + TrivialExists. econstructor. EvalOp. simpl; eauto. econstructor. eauto. constructor. + rewrite Val.mul_commut. auto. generalize (Int.one_bits_decomp n). generalize (Int.one_bits_range n). - change (Z_of_nat Int.wordsize) with 32. destruct (Int.one_bits n). - intros. EvalOp. constructor. EvalOp. simpl; reflexivity. - constructor. eauto. constructor. simpl. rewrite Int.mul_commut. auto. + intros. auto. destruct l. intros. rewrite H1. simpl. - rewrite Int.add_zero. rewrite <- Int.shl_mul. - apply eval_shlimm. auto. auto with coqlib. + rewrite Int.add_zero. + replace (Vint (Int.shl Int.one i)) with (Val.shl Vone (Vint i)). rewrite Val.shl_mul. + apply eval_shlimm. auto. simpl. rewrite H0; auto with coqlib. destruct l. - intros. apply eval_Elet with (Vint x). auto. - rewrite H1. simpl. rewrite Int.add_zero. - rewrite Int.mul_add_distr_r. - rewrite <- Int.shl_mul. - rewrite <- Int.shl_mul. - apply eval_add. - apply eval_shlimm. apply eval_Eletvar. simpl. reflexivity. - auto with coqlib. - apply eval_shlimm. apply eval_Eletvar. simpl. reflexivity. - auto with coqlib. - intros. EvalOp. constructor. EvalOp. simpl; reflexivity. - constructor. eauto. constructor. simpl. rewrite Int.mul_commut. auto. + intros. rewrite H1. simpl. + exploit (eval_shlimm i (x :: le) (Eletvar 0) x). constructor; auto. intros [v1 [A1 B1]]. + exploit (eval_shlimm i0 (x :: le) (Eletvar 0) x). constructor; auto. intros [v2 [A2 B2]]. + exploit (eval_add (x :: le)). eexact A1. eexact A2. intros [v [A B]]. + exists v; split. econstructor; eauto. + rewrite Int.add_zero. + replace (Vint (Int.add (Int.shl Int.one i) (Int.shl Int.one i0))) + with (Val.add (Val.shl Vone (Vint i)) (Val.shl Vone (Vint i0))). + rewrite Val.mul_add_distr_r. + repeat rewrite Val.shl_mul. eapply Val.lessdef_trans. 2: eauto. apply Val.add_lessdef; auto. + simpl. repeat rewrite H0; auto with coqlib. + intros. auto. Qed. + Theorem eval_mulimm: - forall le a n x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (mulimm n a) (Vint (Int.mul x n)). -Proof. - intros until x; unfold mulimm. - generalize (Int.eq_spec n Int.zero); case (Int.eq n Int.zero); intro. - subst n. rewrite Int.mul_zero. - intro. EvalOp. - generalize (Int.eq_spec n Int.one); case (Int.eq n Int.one); intro. - subst n. rewrite Int.mul_one. auto. + forall n, unary_constructor_sound (mulimm n) (fun x => Val.mul x (Vint n)). +Proof. + intros; red; intros until x; unfold mulimm. + predSpec Int.eq Int.eq_spec n Int.zero. + intros. exists (Vint Int.zero); split. EvalOp. + destruct x; simpl; auto. subst n. rewrite Int.mul_zero. auto. + predSpec Int.eq Int.eq_spec n Int.one. + intros. exists x; split; auto. + destruct x; simpl; auto. subst n. rewrite Int.mul_one. auto. case (mulimm_match a); intros; InvEval. - EvalOp. rewrite Int.mul_commut. reflexivity. - replace (Int.mul x n) with (Int.add (Int.mul i n) (Int.mul n n2)). - apply eval_addimm. apply eval_mulimm_base. auto. - subst x. rewrite Int.mul_add_distr_l. decEq. apply Int.mul_commut. - apply eval_mulimm_base. assumption. + TrivialExists. simpl. rewrite Int.mul_commut; auto. + subst. rewrite Val.mul_add_distr_l. + exploit eval_mulimm_base; eauto. instantiate (1 := n). intros [v' [A1 B1]]. + exploit (eval_addimm (Int.mul n n2) le (mulimm_base n t2) v'). auto. intros [v'' [A2 B2]]. + exists v''; split; auto. eapply Val.lessdef_trans. eapply Val.add_lessdef; eauto. + rewrite Val.mul_commut; auto. + apply eval_mulimm_base; auto. Qed. -Theorem eval_mul: - forall le a b x y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (mul a b) (Vint (Int.mul x y)). +Theorem eval_mul: binary_constructor_sound mul Val.mul. Proof. - intros until y. + red; intros until y. unfold mul; case (mul_match a b); intros; InvEval. - rewrite Int.mul_commut. apply eval_mulimm. auto. + rewrite Val.mul_commut. apply eval_mulimm. auto. apply eval_mulimm. auto. - EvalOp. + TrivialExists. Qed. -Theorem eval_divs_base: - forall le a b x y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (Eop Odiv (a ::: b ::: Enil)) (Vint (Int.divs x y)). +Theorem eval_andimm: + forall n, unary_constructor_sound (andimm n) (fun x => Val.and x (Vint n)). Proof. - intros. EvalOp; simpl. - predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. + intros; red; intros until x. unfold andimm. + predSpec Int.eq Int.eq_spec n Int.zero. + intros. exists (Vint Int.zero); split. EvalOp. + destruct x; simpl; auto. subst n. rewrite Int.and_zero. auto. + case (andimm_match a); intros. + InvEval. TrivialExists. simpl. rewrite Int.and_commut; auto. + InvEval. subst. rewrite Val.and_assoc. simpl. rewrite Int.and_commut. TrivialExists. + TrivialExists. Qed. -Theorem eval_divs: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (divs a b) (Vint (Int.divs x y)). -Proof. - intros until y. - unfold divs; case (divu_match b); intros; InvEval. - caseEq (Int.is_power2 y); intros. - caseEq (Int.ltu i (Int.repr 31)); intros. - EvalOp. simpl. unfold Int.ltu. rewrite zlt_true. - rewrite (Int.divs_pow2 x y i H0). auto. - exploit Int.ltu_inv; eauto. - change (Int.unsigned (Int.repr 31)) with 31. - change (Int.unsigned Int.iwordsize) with 32. - omega. - apply eval_divs_base. auto. EvalOp. auto. - apply eval_divs_base. auto. EvalOp. auto. - apply eval_divs_base; auto. +Theorem eval_and: binary_constructor_sound and Val.and. +Proof. + red; intros until y; unfold and; case (and_match a b); intros; InvEval. + rewrite Val.and_commut. apply eval_andimm; auto. + apply eval_andimm; auto. + subst. rewrite Val.and_commut. TrivialExists. + subst. TrivialExists. + subst. rewrite Val.and_commut. TrivialExists. + subst. TrivialExists. + subst. rewrite Val.and_commut. TrivialExists. + subst. TrivialExists. + TrivialExists. +Qed. + +Theorem eval_orimm: + forall n, unary_constructor_sound (orimm n) (fun x => Val.or x (Vint n)). +Proof. + intros; red; intros until x. unfold orimm. + predSpec Int.eq Int.eq_spec n Int.zero. + intros. subst. exists x; split; auto. + destruct x; simpl; auto. rewrite Int.or_zero; auto. + destruct (orimm_match a); intros; InvEval. + TrivialExists. simpl. rewrite Int.or_commut; auto. + subst. rewrite Val.or_assoc. simpl. rewrite Int.or_commut. TrivialExists. + TrivialExists. +Qed. + +Remark eval_same_expr: + forall a1 a2 le v1 v2, + same_expr_pure a1 a2 = true -> + eval_expr ge sp e m le a1 v1 -> + eval_expr ge sp e m le a2 v2 -> + a1 = a2 /\ v1 = v2. +Proof. + intros until v2. + destruct a1; simpl; try (intros; discriminate). + destruct a2; simpl; try (intros; discriminate). + case (ident_eq i i0); intros. + subst i0. inversion H0. inversion H1. split. auto. congruence. + discriminate. +Qed. + +Theorem eval_or: binary_constructor_sound or Val.or. +Proof. + red; intros until y; unfold or; case (or_match a b); intros; InvEval. + rewrite Val.or_commut. apply eval_orimm; auto. + apply eval_orimm; auto. +(* shl - shru *) + destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) as []_eqn. + destruct (andb_prop _ _ Heqb0). + generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros. + exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst. + exists (Val.ror v0 (Vint n2)); split. EvalOp. + destruct v0; simpl; auto. + destruct (Int.ltu n1 Int.iwordsize) as []_eqn; auto. + destruct (Int.ltu n2 Int.iwordsize) as []_eqn; auto. + simpl. rewrite <- Int.or_ror; auto. + subst. TrivialExists. + econstructor. EvalOp. simpl; eauto. econstructor; eauto. constructor. + simpl. auto. +(* shru - shr *) + destruct (Int.eq (Int.add n2 n1) Int.iwordsize && same_expr_pure t1 t2) as []_eqn. + destruct (andb_prop _ _ Heqb0). + generalize (Int.eq_spec (Int.add n2 n1) Int.iwordsize); rewrite H1; intros. + exploit eval_same_expr; eauto. intros [EQ1 EQ2]. subst. + exists (Val.ror v0 (Vint n1)); split. EvalOp. + destruct v0; simpl; auto. + destruct (Int.ltu n1 Int.iwordsize) as []_eqn; auto. + destruct (Int.ltu n2 Int.iwordsize) as []_eqn; auto. + simpl. rewrite Int.or_commut. rewrite <- Int.or_ror; auto. + subst. TrivialExists. + econstructor. EvalOp. simpl; eauto. econstructor; eauto. constructor. + simpl. auto. +(* orshift *) + subst. rewrite Val.or_commut. TrivialExists. + subst. TrivialExists. +(* default *) + TrivialExists. +Qed. + +Theorem eval_xorimm: + forall n, unary_constructor_sound (xorimm n) (fun x => Val.xor x (Vint n)). +Proof. + intros; red; intros until x. unfold xorimm. + predSpec Int.eq Int.eq_spec n Int.zero. + intros. exists x; split. auto. + destruct x; simpl; auto. subst n. rewrite Int.xor_zero. auto. + destruct (xorimm_match a); intros; InvEval. + TrivialExists. simpl. rewrite Int.xor_commut; auto. + subst. rewrite Val.xor_assoc. simpl. rewrite Int.xor_commut. TrivialExists. + TrivialExists. +Qed. + +Theorem eval_xor: binary_constructor_sound xor Val.xor. +Proof. + red; intros until y; unfold xor; case (xor_match a b); intros; InvEval. + rewrite Val.xor_commut. apply eval_xorimm; auto. + apply eval_xorimm; auto. + subst. rewrite Val.xor_commut. TrivialExists. + subst. TrivialExists. + TrivialExists. Qed. Lemma eval_mod_aux: forall divop semdivop, - (forall sp x y m, - y <> Int.zero -> - eval_operation ge sp divop (Vint x :: Vint y :: nil) m = - Some (Vint (semdivop x y))) -> - forall le a b x y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (mod_aux divop a b) - (Vint (Int.sub x (Int.mul (semdivop x y) y))). + (forall sp x y m, eval_operation ge sp divop (x :: y :: nil) m = semdivop x y) -> + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + semdivop x y = Some z -> + eval_expr ge sp e m le (mod_aux divop a b) (Val.sub x (Val.mul z y)). Proof. intros; unfold mod_aux. eapply eval_Elet. eexact H0. eapply eval_Elet. @@ -545,424 +481,246 @@ Proof. eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. apply eval_Enil. - apply H. assumption. + rewrite H. eauto. eapply eval_Econs. apply eval_Eletvar. simpl; reflexivity. apply eval_Enil. simpl; reflexivity. apply eval_Enil. reflexivity. Qed. -Theorem eval_mods: - forall le a b x y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (mods a b) (Vint (Int.mods x y)). +Theorem eval_divs: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.divs x y = Some z -> + exists v, eval_expr ge sp e m le (divs a b) v /\ Val.lessdef z v. Proof. - intros; unfold mods. - rewrite Int.mods_divs. - eapply eval_mod_aux; eauto. - intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. - contradiction. auto. + intros. unfold divs. exists z; split. EvalOp. auto. Qed. -Lemma eval_divu_base: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (Eop Odivu (a ::: b ::: Enil)) (Vint (Int.divu x y)). +Theorem eval_mods: + forall le a b x y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.mods x y = Some z -> + exists v, eval_expr ge sp e m le (mods a b) v /\ Val.lessdef z v. Proof. - intros. EvalOp. simpl. - predSpec Int.eq Int.eq_spec y Int.zero. contradiction. auto. + intros; unfold mods. + exploit Val.mods_divs; eauto. intros [v [A B]]. + subst. econstructor; split; eauto. + apply eval_mod_aux with (semdivop := Val.divs); auto. Qed. -Theorem eval_divu: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (divu a b) (Vint (Int.divu x y)). +Theorem eval_divuimm: + forall le n a x z, + eval_expr ge sp e m le a x -> + Val.divu x (Vint n) = Some z -> + exists v, eval_expr ge sp e m le (divuimm a n) v /\ Val.lessdef z v. Proof. - intros until y. - unfold divu; case (divu_match b); intros; InvEval. - caseEq (Int.is_power2 y). - intros. rewrite (Int.divu_pow2 x y i H0). - apply eval_shruimm. auto. - apply Int.is_power2_range with y. auto. - intros. apply eval_divu_base. auto. EvalOp. auto. - eapply eval_divu_base; eauto. + intros; unfold divuimm. + destruct (Int.is_power2 n) as []_eqn. + replace z with (Val.shru x (Vint i)). apply eval_shruimm; auto. + eapply Val.divu_pow2; eauto. + TrivialExists. + econstructor. eauto. econstructor. EvalOp. simpl; eauto. constructor. auto. Qed. -Theorem eval_modu: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - y <> Int.zero -> - eval_expr ge sp e m le (modu a b) (Vint (Int.modu x y)). -Proof. - intros until y; unfold modu; case (divu_match b); intros; InvEval. - caseEq (Int.is_power2 y). - intros. rewrite (Int.modu_and x y i H0). - EvalOp. - intro. rewrite Int.modu_divu. eapply eval_mod_aux. - intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. - contradiction. auto. - auto. EvalOp. auto. auto. - rewrite Int.modu_divu. eapply eval_mod_aux. - intros. simpl. predSpec Int.eq Int.eq_spec y0 Int.zero. - contradiction. auto. auto. auto. auto. auto. -Qed. - -Theorem eval_and: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (and a b) (Vint (Int.and x y)). -Proof. - intros until y; unfold and; case (and_match a b); intros; InvEval. - rewrite Int.and_commut. EvalOp. simpl. congruence. - EvalOp. simpl. congruence. - rewrite Int.and_commut. EvalOp. simpl. congruence. - EvalOp. simpl. congruence. - rewrite Int.and_commut. EvalOp. simpl. congruence. - EvalOp. simpl. congruence. +Theorem eval_divu: + forall le a x b y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.divu x y = Some z -> + exists v, eval_expr ge sp e m le (divu a b) v /\ Val.lessdef z v. +Proof. + intros until z. unfold divu; destruct (divu_match b); intros; InvEval. + eapply eval_divuimm; eauto. + TrivialExists. +Qed. + +Theorem eval_moduimm: + forall le n a x z, + eval_expr ge sp e m le a x -> + Val.modu x (Vint n) = Some z -> + exists v, eval_expr ge sp e m le (moduimm a n) v /\ Val.lessdef z v. +Proof. + intros; unfold moduimm. + destruct (Int.is_power2 n) as []_eqn. + replace z with (Val.and x (Vint (Int.sub n Int.one))). TrivialExists. + eapply Val.modu_pow2; eauto. + exploit Val.modu_divu; eauto. intros [v [A B]]. + subst. econstructor; split; eauto. + apply eval_mod_aux with (semdivop := Val.divu); auto. EvalOp. Qed. -Remark eval_same_expr: - forall a1 a2 le v1 v2, - same_expr_pure a1 a2 = true -> - eval_expr ge sp e m le a1 v1 -> - eval_expr ge sp e m le a2 v2 -> - a1 = a2 /\ v1 = v2. +Theorem eval_modu: + forall le a x b y z, + eval_expr ge sp e m le a x -> + eval_expr ge sp e m le b y -> + Val.modu x y = Some z -> + exists v, eval_expr ge sp e m le (modu a b) v /\ Val.lessdef z v. Proof. - intros until v2. - destruct a1; simpl; try (intros; discriminate). - destruct a2; simpl; try (intros; discriminate). - case (ident_eq i i0); intros. - subst i0. inversion H0. inversion H1. split. auto. congruence. - discriminate. + intros until y; unfold modu; case (modu_match b); intros; InvEval. + eapply eval_moduimm; eauto. + exploit Val.modu_divu; eauto. intros [v [A B]]. + subst. econstructor; split; eauto. + apply eval_mod_aux with (semdivop := Val.divu); auto. Qed. -Lemma eval_or: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (or a b) (Vint (Int.or x y)). -Proof. - intros until y; unfold or; case (or_match a b); intros; InvEval. - caseEq (Int.eq (Int.add (s_amount n1) (s_amount n2)) Int.iwordsize - && same_expr_pure t1 t2); intro. - destruct (andb_prop _ _ H1). - generalize (Int.eq_spec (Int.add (s_amount n1) (s_amount n2)) Int.iwordsize). - rewrite H4. intro. - exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. - simpl. EvalOp. simpl. decEq. decEq. apply Int.or_ror. - destruct n1; auto. destruct n2; auto. auto. - EvalOp. econstructor. EvalOp. simpl. reflexivity. - econstructor; eauto with evalexpr. - simpl. congruence. - caseEq (Int.eq (Int.add (s_amount n2) (s_amount n1)) Int.iwordsize - && same_expr_pure t1 t2); intro. - destruct (andb_prop _ _ H1). - generalize (Int.eq_spec (Int.add (s_amount n2) (s_amount n1)) Int.iwordsize). - rewrite H4. intro. - exploit eval_same_expr; eauto. intros [EQ1 EQ2]. inv EQ1. inv EQ2. - simpl. EvalOp. simpl. decEq. decEq. rewrite Int.or_commut. apply Int.or_ror. - destruct n2; auto. destruct n1; auto. auto. - EvalOp. econstructor. EvalOp. simpl. reflexivity. - econstructor; eauto with evalexpr. - simpl. congruence. - EvalOp. simpl. rewrite Int.or_commut. congruence. - EvalOp. simpl. congruence. - EvalOp. -Qed. - -Theorem eval_xor: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (xor a b) (Vint (Int.xor x y)). +Theorem eval_shl: binary_constructor_sound shl Val.shl. Proof. - intros until y; unfold xor; case (xor_match a b); intros; InvEval. - rewrite Int.xor_commut. EvalOp. simpl. congruence. - EvalOp. simpl. congruence. - EvalOp. + red; intros until y; unfold shl; case (shl_match b); intros. + InvEval. apply eval_shlimm; auto. + TrivialExists. Qed. -Theorem eval_shl: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - Int.ltu y Int.iwordsize = true -> - eval_expr ge sp e m le (shl a b) (Vint (Int.shl x y)). +Theorem eval_shr: binary_constructor_sound shr Val.shr. Proof. - intros until y; unfold shl; case (shift_match b); intros. - InvEval. apply eval_shlimm; auto. - EvalOp. simpl. rewrite H1. auto. + red; intros until y; unfold shr; case (shr_match b); intros. + InvEval. apply eval_shrimm; auto. + TrivialExists. Qed. -Theorem eval_shru: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - Int.ltu y Int.iwordsize = true -> - eval_expr ge sp e m le (shru a b) (Vint (Int.shru x y)). +Theorem eval_shru: binary_constructor_sound shru Val.shru. Proof. - intros until y; unfold shru; case (shift_match b); intros. + red; intros until y; unfold shru; case (shru_match b); intros. InvEval. apply eval_shruimm; auto. - EvalOp. simpl. rewrite H1. auto. + TrivialExists. Qed. -Theorem eval_shr: - forall le a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - Int.ltu y Int.iwordsize = true -> - eval_expr ge sp e m le (shr a b) (Vint (Int.shr x y)). + +Theorem eval_negf: unary_constructor_sound negf Val.negf. Proof. - intros until y; unfold shr; case (shift_match b); intros. - InvEval. apply eval_shrimm; auto. - EvalOp. simpl. rewrite H1. auto. + red; intros. TrivialExists. Qed. -Theorem eval_cast8signed: - forall le a v, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m le (cast8signed a) (Val.sign_ext 8 v). -Proof. TrivialOp cast8signed. Qed. - -Theorem eval_cast8unsigned: - forall le a v, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m le (cast8unsigned a) (Val.zero_ext 8 v). -Proof. TrivialOp cast8unsigned. Qed. +Theorem eval_absf: unary_constructor_sound absf Val.absf. +Proof. + red; intros. TrivialExists. +Qed. -Theorem eval_cast16signed: - forall le a v, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m le (cast16signed a) (Val.sign_ext 16 v). -Proof. TrivialOp cast16signed. Qed. +Theorem eval_addf: binary_constructor_sound addf Val.addf. +Proof. + red; intros; TrivialExists. +Qed. + +Theorem eval_subf: binary_constructor_sound subf Val.subf. +Proof. + red; intros; TrivialExists. +Qed. -Theorem eval_cast16unsigned: - forall le a v, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m le (cast16unsigned a) (Val.zero_ext 16 v). -Proof. TrivialOp cast16unsigned. Qed. +Theorem eval_mulf: binary_constructor_sound mulf Val.mulf. +Proof. + red; intros; TrivialExists. +Qed. -Theorem eval_singleoffloat: - forall le a v, - eval_expr ge sp e m le a v -> - eval_expr ge sp e m le (singleoffloat a) (Val.singleoffloat v). -Proof. TrivialOp singleoffloat. Qed. +Theorem eval_divf: binary_constructor_sound divf Val.divf. +Proof. + red; intros; TrivialExists. +Qed. Theorem eval_comp: - forall le c a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (comp c a b) (Val.of_bool(Int.cmp c x y)). -Proof. - intros until y. - unfold comp; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite Int.swap_cmp. destruct (Int.cmp c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. - EvalOp. simpl. rewrite H. rewrite Int.swap_cmp. destruct (Int.cmp c x y); reflexivity. - EvalOp. simpl. rewrite H0. destruct (Int.cmp c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmp c x y); reflexivity. -Qed. - -Theorem eval_compu_int: - forall le c a x b y, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vint y) -> - eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x y)). -Proof. - intros until y. - unfold compu; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite Int.swap_cmpu. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. rewrite Int.swap_cmpu. rewrite H. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. rewrite H0. destruct (Int.cmpu c x y); reflexivity. - EvalOp. simpl. destruct (Int.cmpu c x y); reflexivity. -Qed. - -Remark eval_compare_null_trans: - forall c x v, - (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> - match eval_compare_null c x with - | Some true => Some Vtrue - | Some false => Some Vfalse - | None => None (A:=val) - end = Some v. -Proof. - unfold Cminor.eval_compare_mismatch, eval_compare_null; intros. - destruct (Int.eq x Int.zero); try discriminate. - destruct c; try discriminate; auto. -Qed. - -Theorem eval_compu_ptr_int: - forall le c a x1 x2 b y v, - eval_expr ge sp e m le a (Vptr x1 x2) -> - eval_expr ge sp e m le b (Vint y) -> - (if Int.eq y Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> - eval_expr ge sp e m le (compu c a b) v. -Proof. - intros until v. - unfold compu; case (comp_match a b); intros; InvEval. - EvalOp. simpl. apply eval_compare_null_trans; auto. - EvalOp. simpl. rewrite H0. apply eval_compare_null_trans; auto. - EvalOp. simpl. apply eval_compare_null_trans; auto. -Qed. - -Remark eval_swap_compare_null_trans: - forall c x v, - (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> - match eval_compare_null (swap_comparison c) x with - | Some true => Some Vtrue - | Some false => Some Vfalse - | None => None (A:=val) - end = Some v. -Proof. - unfold Cminor.eval_compare_mismatch, eval_compare_null; intros. - destruct (Int.eq x Int.zero); try discriminate. - destruct c; simpl; try discriminate; auto. -Qed. - -Theorem eval_compu_int_ptr: - forall le c a x b y1 y2 v, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le b (Vptr y1 y2) -> - (if Int.eq x Int.zero then Cminor.eval_compare_mismatch c else None) = Some v -> - eval_expr ge sp e m le (compu c a b) v. -Proof. - intros until v. - unfold compu; case (comp_match a b); intros; InvEval. - EvalOp. simpl. apply eval_swap_compare_null_trans; auto. - EvalOp. simpl. rewrite H. apply eval_swap_compare_null_trans; auto. - EvalOp. simpl. apply eval_compare_null_trans; auto. -Qed. - -Theorem eval_compu_ptr_ptr: - forall le c a x1 x2 b y1 y2, - eval_expr ge sp e m le a (Vptr x1 x2) -> - eval_expr ge sp e m le b (Vptr y1 y2) -> - Mem.valid_pointer m x1 (Int.unsigned x2) - && Mem.valid_pointer m y1 (Int.unsigned y2) = true -> - x1 = y1 -> - eval_expr ge sp e m le (compu c a b) (Val.of_bool(Int.cmpu c x2 y2)). -Proof. - intros until y2. - unfold compu; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite H1. subst y1. rewrite dec_eq_true. - destruct (Int.cmpu c x2 y2); reflexivity. -Qed. - -Theorem eval_compu_ptr_ptr_2: - forall le c a x1 x2 b y1 y2 v, - eval_expr ge sp e m le a (Vptr x1 x2) -> - eval_expr ge sp e m le b (Vptr y1 y2) -> - Mem.valid_pointer m x1 (Int.unsigned x2) - && Mem.valid_pointer m y1 (Int.unsigned y2) = true -> - x1 <> y1 -> - Cminor.eval_compare_mismatch c = Some v -> - eval_expr ge sp e m le (compu c a b) v. -Proof. - intros until y2. - unfold compu; case (comp_match a b); intros; InvEval. - EvalOp. simpl. rewrite H1. rewrite dec_eq_false; auto. - destruct c; simpl in H3; inv H3; auto. + forall c, binary_constructor_sound (comp c) (Val.cmp c). +Proof. + intros; red; intros until y. unfold comp; case (comp_match a b); intros; InvEval. + TrivialExists. simpl. rewrite Val.swap_cmp_bool. auto. + TrivialExists. + subst. TrivialExists. simpl. rewrite Val.swap_cmp_bool. auto. + subst. TrivialExists. + TrivialExists. Qed. -Theorem eval_compf: - forall le c a x b y, - eval_expr ge sp e m le a (Vfloat x) -> - eval_expr ge sp e m le b (Vfloat y) -> - eval_expr ge sp e m le (compf c a b) (Val.of_bool(Float.cmp c x y)). +Theorem eval_compu: + forall c, binary_constructor_sound (compu c) (Val.cmpu (Mem.valid_pointer m) c). Proof. - intros. unfold compf. EvalOp. simpl. - destruct (Float.cmp c x y); reflexivity. + intros; red; intros until y. unfold compu; case (compu_match a b); intros; InvEval. + TrivialExists. simpl. rewrite Val.swap_cmpu_bool. auto. + TrivialExists. + subst. TrivialExists. simpl. rewrite Val.swap_cmpu_bool. auto. + subst. TrivialExists. + TrivialExists. Qed. -Theorem eval_negint: - forall le a x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (negint a) (Vint (Int.neg x)). -Proof. intros; unfold negint; EvalOp. Qed. - -Theorem eval_negf: - forall le a x, - eval_expr ge sp e m le a (Vfloat x) -> - eval_expr ge sp e m le (negf a) (Vfloat (Float.neg x)). -Proof. intros; unfold negf; EvalOp. Qed. +Theorem eval_compf: + forall c, binary_constructor_sound (compf c) (Val.cmpf c). +Proof. + intros; red; intros. unfold compf. TrivialExists. +Qed. -Theorem eval_absf: - forall le a x, - eval_expr ge sp e m le a (Vfloat x) -> - eval_expr ge sp e m le (absf a) (Vfloat (Float.abs x)). -Proof. intros; unfold absf; EvalOp. Qed. +Theorem eval_cast8signed: unary_constructor_sound cast8signed (Val.sign_ext 8). +Proof. + red; intros. unfold cast8signed. + exploit (eval_shlimm (Int.repr 24)); eauto. intros [v1 [A1 B1]]. + exploit (eval_shrimm (Int.repr 24)). eexact A1. intros [v2 [A2 B2]]. + exists v2; split; auto. + destruct x; simpl; auto. simpl in *. inv B1. simpl in *. inv B2. + rewrite Int.sign_ext_shr_shl. auto. compute; auto. +Qed. -Theorem eval_addf: - forall le a x b y, - eval_expr ge sp e m le a (Vfloat x) -> - eval_expr ge sp e m le b (Vfloat y) -> - eval_expr ge sp e m le (addf a b) (Vfloat (Float.add x y)). -Proof. intros; unfold addf; EvalOp. Qed. +Theorem eval_cast8unsigned: unary_constructor_sound cast8unsigned (Val.zero_ext 8). +Proof. + red; intros until x. unfold cast8unsigned. + rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. +Qed. -Theorem eval_subf: - forall le a x b y, - eval_expr ge sp e m le a (Vfloat x) -> - eval_expr ge sp e m le b (Vfloat y) -> - eval_expr ge sp e m le (subf a b) (Vfloat (Float.sub x y)). -Proof. intros; unfold subf; EvalOp. Qed. +Theorem eval_cast16signed: unary_constructor_sound cast16signed (Val.sign_ext 16). +Proof. + red; intros. unfold cast16signed. + exploit (eval_shlimm (Int.repr 16)); eauto. intros [v1 [A1 B1]]. + exploit (eval_shrimm (Int.repr 16)). eexact A1. intros [v2 [A2 B2]]. + exists v2; split; auto. + destruct x; simpl; auto. simpl in *. inv B1. simpl in *. inv B2. + rewrite Int.sign_ext_shr_shl. auto. compute; auto. +Qed. -Theorem eval_mulf: - forall le a x b y, - eval_expr ge sp e m le a (Vfloat x) -> - eval_expr ge sp e m le b (Vfloat y) -> - eval_expr ge sp e m le (mulf a b) (Vfloat (Float.mul x y)). -Proof. intros; unfold mulf; EvalOp. Qed. +Theorem eval_cast16unsigned: unary_constructor_sound cast16unsigned (Val.zero_ext 16). +Proof. + red; intros until x. unfold cast8unsigned. + rewrite Val.zero_ext_and. apply eval_andimm. compute; auto. +Qed. -Theorem eval_divf: - forall le a x b y, - eval_expr ge sp e m le a (Vfloat x) -> - eval_expr ge sp e m le b (Vfloat y) -> - eval_expr ge sp e m le (divf a b) (Vfloat (Float.div x y)). -Proof. intros; unfold divf; EvalOp. Qed. +Theorem eval_singleoffloat: unary_constructor_sound singleoffloat Val.singleoffloat. +Proof. + red; intros. unfold singleoffloat. TrivialExists. +Qed. Theorem eval_intoffloat: - forall le a x n, - eval_expr ge sp e m le a (Vfloat x) -> - Float.intoffloat x = Some n -> - eval_expr ge sp e m le (intoffloat a) (Vint n). + forall le a x y, + eval_expr ge sp e m le a x -> + Val.intoffloat x = Some y -> + exists v, eval_expr ge sp e m le (intoffloat a) v /\ Val.lessdef y v. Proof. - intros; unfold intoffloat; EvalOp. - simpl. rewrite H0. auto. + intros; unfold intoffloat. TrivialExists. Qed. -Theorem eval_intuoffloat: - forall le a x n, - eval_expr ge sp e m le a (Vfloat x) -> - Float.intuoffloat x = Some n -> - eval_expr ge sp e m le (intuoffloat a) (Vint n). +Theorem eval_floatofint: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.floatofint x = Some y -> + exists v, eval_expr ge sp e m le (floatofint a) v /\ Val.lessdef y v. Proof. - intros; unfold intuoffloat; EvalOp. - simpl. rewrite H0. auto. + intros; unfold floatofint. TrivialExists. Qed. -Theorem eval_floatofint: - forall le a x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (floatofint a) (Vfloat (Float.floatofint x)). -Proof. intros; unfold floatofint; EvalOp. Qed. +Theorem eval_intuoffloat: + forall le a x y, + eval_expr ge sp e m le a x -> + Val.intuoffloat x = Some y -> + exists v, eval_expr ge sp e m le (intuoffloat a) v /\ Val.lessdef y v. +Proof. + intros; unfold intuoffloat. TrivialExists. +Qed. Theorem eval_floatofintu: - forall le a x, - eval_expr ge sp e m le a (Vint x) -> - eval_expr ge sp e m le (floatofintu a) (Vfloat (Float.floatofintu x)). -Proof. intros; unfold floatofintu; EvalOp. Qed. + forall le a x y, + eval_expr ge sp e m le a x -> + Val.floatofintu x = Some y -> + exists v, eval_expr ge sp e m le (floatofintu a) v /\ Val.lessdef y v. +Proof. + intros; unfold floatofintu. TrivialExists. +Qed. -Lemma eval_addressing: +Theorem eval_addressing: forall le chunk a v b ofs, eval_expr ge sp e m le a v -> v = Vptr b ofs -> @@ -974,29 +732,16 @@ Lemma eval_addressing: Proof. intros until v. unfold addressing; case (addressing_match a); intros; InvEval. exists (@nil val). split. eauto with evalexpr. simpl. auto. - exists (Vptr b0 i :: nil). split. eauto with evalexpr. - simpl. congruence. - destruct (can_use_Aindexed2 chunk). - exists (Vptr b0 i :: Vint i0 :: nil). - split. eauto with evalexpr. simpl. congruence. - exists (Vptr b0 ofs :: nil). - split. constructor. econstructor. eauto with evalexpr. simpl. congruence. constructor. - simpl. rewrite Int.add_zero. congruence. - destruct (can_use_Aindexed chunk). - exists (Vint i :: Vptr b0 i0 :: nil). - split. eauto with evalexpr. simpl. - rewrite Int.add_commut. congruence. - exists (Vptr b0 ofs :: nil). - split. constructor. econstructor. eauto with evalexpr. simpl. congruence. constructor. - simpl. rewrite Int.add_zero. congruence. - destruct (can_use_Aindexed chunk). - exists (Vptr b0 i :: Vint i0 :: nil). - split. eauto with evalexpr. simpl. congruence. - exists (Vptr b0 ofs :: nil). - split. constructor. econstructor. eauto with evalexpr. simpl. congruence. constructor. - simpl. rewrite Int.add_zero. congruence. - exists (v :: nil). split. eauto with evalexpr. - subst v. simpl. rewrite Int.add_zero. auto. + exists (v1 :: nil); split. eauto with evalexpr. simpl. congruence. + destruct (can_use_Aindexed2shift chunk); simpl. + exists (v1 :: v0 :: nil); split. eauto with evalexpr. congruence. + exists (Vptr b ofs :: nil); split. constructor. EvalOp. simpl. congruence. constructor. + simpl. rewrite Int.add_zero; auto. + destruct (can_use_Aindexed2 chunk); simpl. + exists (v1 :: v0 :: nil); split. eauto with evalexpr. congruence. + exists (Vptr b ofs :: nil); split. constructor. EvalOp. simpl. congruence. constructor. + simpl. rewrite Int.add_zero; auto. + exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Int.add_zero; auto. Qed. End CMCONSTR. -- cgit