diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Selection.v | 30 | ||||
| -rw-r--r-- | powerpc/Selectionproof.v | 28 |
2 files changed, 58 insertions, 0 deletions
diff --git a/powerpc/Selection.v b/powerpc/Selection.v index f1c5a73..46d8039 100644 --- a/powerpc/Selection.v +++ b/powerpc/Selection.v @@ -802,6 +802,9 @@ Inductive cast8signed_cases: forall (e1: expr), Set := | cast8signed_case1: forall (e2: expr), cast8signed_cases (Eop Ocast8signed (e2 ::: Enil)) + | cast8signed_case2: + forall mode args, + cast8signed_cases (Eload Mint8signed mode args) | cast8signed_default: forall (e1: expr), cast8signed_cases e1. @@ -810,6 +813,8 @@ Definition cast8signed_match (e1: expr) := match e1 as z1 return cast8signed_cases z1 with | Eop Ocast8signed (e2 ::: Enil) => cast8signed_case1 e2 + | Eload Mint8signed mode args => + cast8signed_case2 mode args | e1 => cast8signed_default e1 end. @@ -817,6 +822,7 @@ Definition cast8signed_match (e1: expr) := Definition cast8signed (e: expr) := match cast8signed_match e with | cast8signed_case1 e1 => e + | cast8signed_case2 mode args => e | cast8signed_default e1 => Eop Ocast8signed (e1 ::: Enil) end. @@ -824,6 +830,9 @@ Inductive cast8unsigned_cases: forall (e1: expr), Set := | cast8unsigned_case1: forall (e2: expr), cast8unsigned_cases (Eop Ocast8unsigned (e2 ::: Enil)) + | cast8unsigned_case2: + forall mode args, + cast8unsigned_cases (Eload Mint8unsigned mode args) | cast8unsigned_default: forall (e1: expr), cast8unsigned_cases e1. @@ -832,6 +841,8 @@ Definition cast8unsigned_match (e1: expr) := match e1 as z1 return cast8unsigned_cases z1 with | Eop Ocast8unsigned (e2 ::: Enil) => cast8unsigned_case1 e2 + | Eload Mint8unsigned mode args => + cast8unsigned_case2 mode args | e1 => cast8unsigned_default e1 end. @@ -839,6 +850,7 @@ Definition cast8unsigned_match (e1: expr) := Definition cast8unsigned (e: expr) := match cast8unsigned_match e with | cast8unsigned_case1 e1 => e + | cast8unsigned_case2 mode args => e | cast8unsigned_default e1 => Eop Ocast8unsigned (e1 ::: Enil) end. @@ -846,6 +858,9 @@ Inductive cast16signed_cases: forall (e1: expr), Set := | cast16signed_case1: forall (e2: expr), cast16signed_cases (Eop Ocast16signed (e2 ::: Enil)) + | cast16signed_case2: + forall mode args, + cast16signed_cases (Eload Mint16signed mode args) | cast16signed_default: forall (e1: expr), cast16signed_cases e1. @@ -854,6 +869,8 @@ Definition cast16signed_match (e1: expr) := match e1 as z1 return cast16signed_cases z1 with | Eop Ocast16signed (e2 ::: Enil) => cast16signed_case1 e2 + | Eload Mint16signed mode args => + cast16signed_case2 mode args | e1 => cast16signed_default e1 end. @@ -861,6 +878,7 @@ Definition cast16signed_match (e1: expr) := Definition cast16signed (e: expr) := match cast16signed_match e with | cast16signed_case1 e1 => e + | cast16signed_case2 mode args => e | cast16signed_default e1 => Eop Ocast16signed (e1 ::: Enil) end. @@ -868,6 +886,9 @@ Inductive cast16unsigned_cases: forall (e1: expr), Set := | cast16unsigned_case1: forall (e2: expr), cast16unsigned_cases (Eop Ocast16unsigned (e2 ::: Enil)) + | cast16unsigned_case2: + forall mode args, + cast16unsigned_cases (Eload Mint16unsigned mode args) | cast16unsigned_default: forall (e1: expr), cast16unsigned_cases e1. @@ -876,6 +897,8 @@ Definition cast16unsigned_match (e1: expr) := match e1 as z1 return cast16unsigned_cases z1 with | Eop Ocast16unsigned (e2 ::: Enil) => cast16unsigned_case1 e2 + | Eload Mint16unsigned mode args => + cast16unsigned_case2 mode args | e1 => cast16unsigned_default e1 end. @@ -883,6 +906,7 @@ Definition cast16unsigned_match (e1: expr) := Definition cast16unsigned (e: expr) := match cast16unsigned_match e with | cast16unsigned_case1 e1 => e + | cast16unsigned_case2 mode args => e | cast16unsigned_default e1 => Eop Ocast16unsigned (e1 ::: Enil) end. @@ -890,6 +914,9 @@ Inductive singleoffloat_cases: forall (e1: expr), Set := | singleoffloat_case1: forall (e2: expr), singleoffloat_cases (Eop Osingleoffloat (e2 ::: Enil)) + | singleoffloat_case2: + forall mode args, + singleoffloat_cases (Eload Mfloat32 mode args) | singleoffloat_default: forall (e1: expr), singleoffloat_cases e1. @@ -898,6 +925,8 @@ Definition singleoffloat_match (e1: expr) := match e1 as z1 return singleoffloat_cases z1 with | Eop Osingleoffloat (e2 ::: Enil) => singleoffloat_case1 e2 + | Eload Mfloat32 mode args => + singleoffloat_case2 mode args | e1 => singleoffloat_default e1 end. @@ -905,6 +934,7 @@ Definition singleoffloat_match (e1: expr) := Definition singleoffloat (e: expr) := match singleoffloat_match e with | singleoffloat_case1 e1 => e + | singleoffloat_case2 mode args => e | singleoffloat_default e1 => Eop Osingleoffloat (e1 ::: Enil) end. diff --git a/powerpc/Selectionproof.v b/powerpc/Selectionproof.v index b6e838c..6ffffc1 100644 --- a/powerpc/Selectionproof.v +++ b/powerpc/Selectionproof.v @@ -745,6 +745,29 @@ Proof. intros. EvalOp. Qed. +Lemma loadv_cast: + forall chunk addr v, + 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) + | _ => 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. +Qed. + Theorem eval_cast8signed: forall le a v, eval_expr ge sp e m le a v -> @@ -753,6 +776,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). EvalOp. Qed. @@ -764,6 +788,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). EvalOp. Qed. @@ -775,6 +800,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). EvalOp. Qed. @@ -786,6 +812,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). EvalOp. Qed. @@ -796,6 +823,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). EvalOp. Qed. |