- Added alignment constraints to memory loads and stores.

- In Cminor and below, removed pointer validity check in semantics of 
  comparisons, so that evaluation of expressions is independent of
  memory state.
- In Cminor and below, removed "alloc" instruction.
- Cleaned up commented-away parts.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

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