diff options
Diffstat (limited to 'arm/SelectOpproof.v')
-rw-r--r-- | arm/SelectOpproof.v | 22 |
1 files changed, 15 insertions, 7 deletions
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v index ecc758f..a71ead7 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. |