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 --- arm/SelectOpproof.v | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) (limited to 'arm/SelectOpproof.v') diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index ecc758fe..a71ead78 100644 --- a/arm/SelectOpproof.v +++ b/arm/SelectOpproof.v @@ -27,13 +27,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 @@ -81,6 +74,13 @@ Ltac TrivialExists := (** * 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 [Selection.notint] behaves as expected. Continuing the [notint] example, we show that if the expression [e] @@ -172,6 +172,8 @@ Proof. subst. rewrite <- Val.add_assoc. apply eval_addimm. EvalOp. subst. rewrite Val.add_commut. TrivialExists. subst. TrivialExists. + subst. TrivialExists. + subst. rewrite Val.add_commut. TrivialExists. TrivialExists. Qed. @@ -325,6 +327,9 @@ Proof. 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. + predSpec Int.eq Int.eq_spec n Int.mone. + intros. exists x; split; auto. + subst. destruct x; simpl; auto. rewrite Int.and_mone; 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. @@ -352,6 +357,9 @@ Proof. predSpec Int.eq Int.eq_spec n Int.zero. intros. subst. exists x; split; auto. destruct x; simpl; auto. rewrite Int.or_zero; auto. + predSpec Int.eq Int.eq_spec n Int.mone. + intros. exists (Vint Int.mone); split. EvalOp. + destruct x; simpl; auto. subst n. rewrite Int.or_mone. 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. -- cgit