From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/SelectOpproof.v | 36 ++++++++++++++++++++++-------------- 1 file changed, 22 insertions(+), 14 deletions(-) (limited to 'ia32/SelectOpproof.v') diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v index 18deca6..1569ad6 100644 --- a/ia32/SelectOpproof.v +++ b/ia32/SelectOpproof.v @@ -26,13 +26,6 @@ Require Import SelectOp. Open Local Scope cminorsel_scope. -Section CMCONSTR. - -Variable ge: genv. -Variable sp: val. -Variable e: env. -Variable m: mem. - (** * Useful lemmas and tactics *) (** The following are trivial lemmas and custom tactics that help @@ -78,9 +71,15 @@ Ltac TrivialExists := | [ |- exists v, _ /\ Val.lessdef ?a v ] => exists a; split; [EvalOp | auto] end. - (** * Correctness of the smart constructors *) +Section CMCONSTR. + +Variable ge: genv. +Variable sp: val. +Variable e: env. +Variable m: mem. + (** We now show that the code generated by "smart constructor" functions such as [SelectOp.notint] behaves as expected. Continuing the [notint] example, we show that if the expression [e] @@ -410,6 +409,12 @@ Proof. discriminate. Qed. +Remark int_add_sub_eq: + forall x y z, Int.add x y = z -> Int.sub z x = y. +Proof. + intros. subst z. rewrite Int.sub_add_l. rewrite Int.sub_idem. apply Int.add_zero_l. +Qed. + Lemma eval_or: binary_constructor_sound or Val.or. Proof. red; intros until y; unfold or; case (or_match a b); intros. @@ -417,26 +422,29 @@ Proof. InvEval. rewrite Val.or_commut. apply eval_orimm; auto. InvEval. apply eval_orimm; auto. (* shlimm - shruimm *) - destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) eqn:?. - destruct (andb_prop _ _ Heqb0). - generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros EQ. + predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize. + destruct (same_expr_pure t1 t2) eqn:?. InvEval. 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) eqn:?; auto. destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto. simpl. rewrite <- Int.or_ror; auto. + InvEval. exists (Val.or x y); split. EvalOp. + simpl. erewrite int_add_sub_eq; eauto. rewrite H0; rewrite H; auto. auto. TrivialExists. (* shruimm - shlimm *) - destruct (Int.eq (Int.add n1 n2) Int.iwordsize && same_expr_pure t1 t2) eqn:?. - destruct (andb_prop _ _ Heqb0). - generalize (Int.eq_spec (Int.add n1 n2) Int.iwordsize); rewrite H1; intros EQ. + predSpec Int.eq Int.eq_spec (Int.add n1 n2) Int.iwordsize. + destruct (same_expr_pure t1 t2) eqn:?. InvEval. exploit eval_same_expr; eauto. intros [EQ1 EQ2]; subst. exists (Val.ror v1 (Vint n2)); split. EvalOp. destruct v1; simpl; auto. destruct (Int.ltu n2 Int.iwordsize) eqn:?; auto. destruct (Int.ltu n1 Int.iwordsize) eqn:?; auto. simpl. rewrite Int.or_commut. rewrite <- Int.or_ror; auto. + InvEval. exists (Val.or y x); split. EvalOp. + simpl. erewrite int_add_sub_eq; eauto. rewrite H0; rewrite H; auto. + rewrite Val.or_commut; auto. TrivialExists. (* default *) TrivialExists. -- cgit v1.2.3