diff options
Diffstat (limited to 'x86/SelectOpproof.v')
| -rw-r--r-- | x86/SelectOpproof.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/x86/SelectOpproof.v b/x86/SelectOpproof.v index 1728c39d..e2e0b830 100644 --- a/x86/SelectOpproof.v +++ b/x86/SelectOpproof.v @@ -115,7 +115,7 @@ Lemma eval_Olea_ptr: forall a el m, eval_operation ge sp (Olea_ptr a) el m = eval_addressing ge sp a el. Proof. - unfold Olea_ptr, eval_addressing; intros. destruct Archi.ptr64; auto. + unfold Olea_ptr, eval_addressing; intros. destruct Archi.ptr64; auto. Qed. Theorem eval_addrsymbol: @@ -162,7 +162,7 @@ Proof. + TrivialExists; simpl. rewrite Int.add_commut. auto. + inv H0. simpl in H6. TrivialExists. simpl. erewrite eval_offset_addressing_total_32 by eauto. rewrite Int.repr_signed; auto. -+ TrivialExists. simpl. rewrite Int.repr_signed; auto. ++ TrivialExists. simpl. rewrite Int.repr_signed; auto. Qed. Theorem eval_add: binary_constructor_sound add Val.add. @@ -172,7 +172,7 @@ Proof. assert (B: forall id ofs n, Archi.ptr64 = false -> Genv.symbol_address ge id (Ptrofs.add ofs (Ptrofs.repr n)) = Val.add (Genv.symbol_address ge id ofs) (Vint (Int.repr n))). - { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int (Int.repr n)) by auto with ptrofs. + { intros. replace (Ptrofs.repr n) with (Ptrofs.of_int (Int.repr n)) by auto with ptrofs. apply Genv.shift_symbol_address_32; auto. } red; intros until y. unfold add; case (add_match a b); intros; InvEval. @@ -193,7 +193,7 @@ Proof. - TrivialExists. - TrivialExists. simpl. repeat rewrite Val.add_assoc. decEq; decEq. apply Val.add_commut. - TrivialExists. simpl. rewrite Val.add_assoc; auto. -- TrivialExists. simpl. +- TrivialExists. simpl. unfold Val.add; destruct Archi.ptr64, x, y; auto. + rewrite Int.add_zero; auto. + rewrite Int.add_zero; auto. @@ -324,7 +324,7 @@ Proof. exploit (eval_shlimm j (x :: le) (Eletvar 0) x). constructor; auto. intros [v2 [A2 B2]]. exploit eval_add. eexact A1. eexact A2. intros [v3 [A3 B3]]. exists v3; split. econstructor; eauto. - rewrite D; simpl; rewrite Int.add_zero. + rewrite D; simpl; rewrite Int.add_zero. replace (Vint (Int.add (Int.shl Int.one i) (Int.shl Int.one j))) with (Val.add (Val.shl Vone (Vint i)) (Val.shl Vone (Vint j))). rewrite Val.mul_add_distr_r. @@ -936,12 +936,12 @@ Proof. /\ eval_addressing ge sp (Aindexed 0) vl = Some v). { intros. exists (v :: nil); split. constructor; auto. constructor. auto. } unfold addressing; case (addressing_match a); intros. -- destruct (negb Archi.ptr64 && addressing_valid addr) eqn:E. -+ inv H. InvBooleans. apply negb_true_iff in H. unfold eval_addressing; rewrite H. +- destruct (negb Archi.ptr64 && addressing_valid addr) eqn:E. ++ inv H. InvBooleans. apply negb_true_iff in H. unfold eval_addressing; rewrite H. exists vl; auto. + apply D; auto. -- destruct (Archi.ptr64 && addressing_valid addr) eqn:E. -+ inv H. InvBooleans. unfold eval_addressing; rewrite H. +- destruct (Archi.ptr64 && addressing_valid addr) eqn:E. ++ inv H. InvBooleans. unfold eval_addressing; rewrite H. exists vl; auto. + apply D; auto. - apply D; auto. |