diff options
Diffstat (limited to 'powerpc/SelectOpproof.v')
| -rw-r--r-- | powerpc/SelectOpproof.v | 35 |
1 files changed, 14 insertions, 21 deletions
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v index 2736e9e9..d4a45dab 100644 --- a/powerpc/SelectOpproof.v +++ b/powerpc/SelectOpproof.v @@ -18,7 +18,7 @@ Require Import AST. Require Import Integers. Require Import Floats. Require Import Values. -Require Import Mem. +Require Import Memory. Require Import Events. Require Import Globalenvs. Require Import Smallstep. @@ -657,25 +657,18 @@ Qed. Lemma loadv_cast: forall chunk addr v, - loadv chunk m addr = Some v -> + Mem.loadv chunk m addr = Some v -> match chunk with - | Mint8signed => loadv chunk m addr = Some(Val.sign_ext 8 v) - | Mint8unsigned => loadv chunk m addr = Some(Val.zero_ext 8 v) - | Mint16signed => loadv chunk m addr = Some(Val.sign_ext 16 v) - | Mint16unsigned => loadv chunk m addr = Some(Val.zero_ext 16 v) - | Mfloat32 => loadv chunk m addr = Some(Val.singleoffloat v) + | Mint8signed => v = Val.sign_ext 8 v + | Mint8unsigned => v = Val.zero_ext 8 v + | Mint16signed => v = Val.sign_ext 16 v + | Mint16unsigned => v = Val.zero_ext 16 v + | Mfloat32 => v = Val.singleoffloat v | _ => True end. Proof. - intros. rewrite H. destruct addr; simpl in H; try discriminate. - exploit Mem.load_inv; eauto. - set (v' := (getN (pred_size_chunk chunk) (Int.signed i) (contents (blocks m b)))). - intros [A B]. subst v. destruct chunk; auto; destruct v'; simpl; auto. - rewrite Int.sign_ext_idem; auto. compute; auto. - rewrite Int.zero_ext_idem; auto. compute; auto. - rewrite Int.sign_ext_idem; auto. compute; auto. - rewrite Int.zero_ext_idem; auto. compute; auto. - rewrite Float.singleoffloat_idem; auto. + intros. destruct addr; simpl in H; try discriminate. + eapply Mem.load_cast. eauto. Qed. Theorem eval_cast8signed: @@ -686,7 +679,7 @@ Proof. intros until v; unfold cast8signed; case (cast8signed_match a); intros; InvEval. EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.sign_ext_idem. reflexivity. compute; auto. - inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). + inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). EvalOp. Qed. @@ -698,7 +691,7 @@ Proof. intros until v; unfold cast8unsigned; case (cast8unsigned_match a); intros; InvEval. EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.zero_ext_idem. reflexivity. compute; auto. - inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). + inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). EvalOp. Qed. @@ -710,7 +703,7 @@ Proof. intros until v; unfold cast16signed; case (cast16signed_match a); intros; InvEval. EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.sign_ext_idem. reflexivity. compute; auto. - inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). + inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). EvalOp. Qed. @@ -722,7 +715,7 @@ Proof. intros until v; unfold cast16unsigned; case (cast16unsigned_match a); intros; InvEval. EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Int.zero_ext_idem. reflexivity. compute; auto. - inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). + inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). EvalOp. Qed. @@ -733,7 +726,7 @@ Theorem eval_singleoffloat: Proof. intros until v; unfold singleoffloat; case (singleoffloat_match a); intros; InvEval. EvalOp. simpl. subst v. destruct v1; simpl; auto. rewrite Float.singleoffloat_idem. reflexivity. - inv H. econstructor; eauto. apply (loadv_cast _ _ _ H7). + inv H. econstructor; eauto. rewrite H7. decEq. apply (loadv_cast _ _ _ H7). EvalOp. Qed. |