summaryrefslogtreecommitdiff
path: root/powerpc/Asmgenproof.v
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc/Asmgenproof.v')
-rw-r--r--powerpc/Asmgenproof.v84
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