diff options
Diffstat (limited to 'powerpc/Asmgenproof.v')
| -rw-r--r-- | powerpc/Asmgenproof.v | 84 |
1 files changed, 3 insertions, 81 deletions
diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 980925b..a96125a 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -537,68 +537,6 @@ Proof. intros. apply Pregmap.gso; auto. Qed. -(** * Memory properties *) - -(** The PowerPC has no instruction for ``load 8-bit signed integer''. - We show that it can be synthesized as a ``load 8-bit unsigned integer'' - followed by a sign extension. *) - -Remark valid_access_equiv: - forall chunk1 chunk2 m b ofs, - size_chunk chunk1 = size_chunk chunk2 -> - valid_access m chunk1 b ofs -> - valid_access m chunk2 b ofs. -Proof. - intros. inv H0. rewrite H in H3. constructor; auto. -Qed. - -Remark in_bounds_equiv: - forall chunk1 chunk2 m b ofs (A: Set) (a1 a2: A), - size_chunk chunk1 = size_chunk chunk2 -> - (if in_bounds m chunk1 b ofs then a1 else a2) = - (if in_bounds m chunk2 b ofs then a1 else a2). -Proof. - intros. destruct (in_bounds m chunk1 b ofs). - rewrite in_bounds_true. auto. eapply valid_access_equiv; eauto. - destruct (in_bounds m chunk2 b ofs); auto. - elim n. eapply valid_access_equiv with (chunk1 := chunk2); eauto. -Qed. - -Lemma loadv_8_signed_unsigned: - forall m a, - Mem.loadv Mint8signed m a = - option_map (Val.sign_ext 8) (Mem.loadv Mint8unsigned m a). -Proof. - intros. unfold Mem.loadv. destruct a; try reflexivity. - unfold load. rewrite (in_bounds_equiv Mint8signed Mint8unsigned). - destruct (in_bounds m Mint8unsigned b (Int.signed i)); auto. - simpl. - destruct (getN 0 (Int.signed i) (contents (blocks m b))); auto. - simpl. rewrite Int.sign_ext_zero_ext. auto. compute; auto. - auto. -Qed. - -(** Similarly, we show that signed 8- and 16-bit stores can be performed - like unsigned stores. *) - -Lemma storev_8_signed_unsigned: - forall m a v, - Mem.storev Mint8signed m a v = Mem.storev Mint8unsigned m a v. -Proof. - intros. unfold storev. destruct a; auto. - unfold store. rewrite (in_bounds_equiv Mint8signed Mint8unsigned). - auto. auto. -Qed. - -Lemma storev_16_signed_unsigned: - forall m a v, - Mem.storev Mint16signed m a v = Mem.storev Mint16unsigned m a v. -Proof. - intros. unfold storev. destruct a; auto. - unfold store. rewrite (in_bounds_equiv Mint16signed Mint16unsigned). - auto. auto. -Qed. - (** * Proof of semantic preservation *) (** Semantic preservation is proved using simulation diagrams @@ -805,7 +743,7 @@ Lemma exec_Mop_prop: forall (s : list stackframe) (fb : block) (sp : val) (op : operation) (args : list mreg) (res : mreg) (c : list Mach.instruction) (ms : mreg -> val) (m : mem) (v : val), - eval_operation ge sp op ms ## args m = Some v -> + eval_operation ge sp op ms ## args = Some v -> exec_instr_prop (Machconcr.State s fb sp (Mop op args res :: c) ms m) E0 (Machconcr.State s fb sp c (Regmap.set res v ms) m). Proof. @@ -1069,21 +1007,6 @@ Proof. unfold rs5; auto with ppcgen. Qed. -Lemma exec_Malloc_prop: - forall (s : list stackframe) (fb : block) (sp : val) - (c : list Mach.instruction) (ms : mreg -> val) (m : mem) (sz : int) - (m' : mem) (blk : block), - ms Conventions.loc_alloc_argument = Vint sz -> - alloc m 0 (Int.signed sz) = (m', blk) -> - exec_instr_prop (Machconcr.State s fb sp (Malloc :: c) ms m) E0 - (Machconcr.State s fb sp c - (Regmap.set (Conventions.loc_alloc_result) (Vptr blk Int.zero) ms) m'). -Proof. - intros; red; intros; inv MS. - left; eapply exec_straight_steps; eauto with coqlib. - simpl. eapply transl_alloc_correct; eauto. -Qed. - Lemma exec_Mgoto_prop: forall (s : list stackframe) (fb : block) (f : function) (sp : val) (lbl : Mach.label) (c : list Mach.instruction) (ms : Mach.regset) @@ -1113,7 +1036,7 @@ Lemma exec_Mcond_true_prop: (cond : condition) (args : list mreg) (lbl : Mach.label) (c : list Mach.instruction) (ms : mreg -> val) (m : mem) (c' : Mach.code), - eval_condition cond ms ## args m = Some true -> + eval_condition cond ms ## args = Some true -> Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl (fn_code f) = Some c' -> exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 @@ -1156,7 +1079,7 @@ Lemma exec_Mcond_false_prop: forall (s : list stackframe) (fb : block) (sp : val) (cond : condition) (args : list mreg) (lbl : Mach.label) (c : list Mach.instruction) (ms : mreg -> val) (m : mem), - eval_condition cond ms ## args m = Some false -> + eval_condition cond ms ## args = Some false -> exec_instr_prop (Machconcr.State s fb sp (Mcond cond args lbl :: c) ms m) E0 (Machconcr.State s fb sp c ms m). Proof. @@ -1345,7 +1268,6 @@ Proof exec_Mstore_prop exec_Mcall_prop exec_Mtailcall_prop - exec_Malloc_prop exec_Mgoto_prop exec_Mcond_true_prop exec_Mcond_false_prop |