- 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, 7 insertions, 14 deletions

diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index e145c896..25819f72 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -94,8 +94,9 @@ Section FRAME_ACCESSES.
 Variable f: function.
 
 (** A slot [(ty, ofs)] within a frame is valid in function [f] if it lies
-  within the bounds of [f]'s frame, and it does not overlap with
-  the slots reserved for the return address and the back link. *)
+  within the bounds of [f]'s frame, it does not overlap with
+  the slots reserved for the return address and the back link,
+  and it is aligned on a 4-byte boundary. *)
 
 Inductive slot_valid: typ -> Z -> Prop :=
   slot_valid_intro:
@@ -106,6 +107,7 @@ Inductive slot_valid: typ -> Z -> Prop :=
        \/ Int.signed f.(fn_link_ofs) + 4 <= ofs) ->
     (ofs + AST.typesize ty <= Int.signed f.(fn_retaddr_ofs)
        \/ Int.signed f.(fn_retaddr_ofs) + 4 <= ofs) ->
+    (4 | ofs) ->
     slot_valid ty ofs.
 
 (** [get_slot f fr ty ofs v] holds if the frame [fr] contains value [v]
@@ -239,7 +241,7 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f sp c (rs#dst <- v) fr m)
   | exec_Mop:
       forall s f sp op args res c rs fr m v,
-      eval_operation ge sp op rs##args m = Some v ->
+      eval_operation ge sp op rs##args = Some v ->
       step (State s f sp (Mop op args res :: c) rs fr m)
         E0 (State s f sp c (rs#res <- v) fr m)
   | exec_Mload:
@@ -264,15 +266,6 @@ Inductive step: state -> trace -> state -> Prop :=
       find_function ros rs = Some f' ->
       step (State s f (Vptr stk soff) (Mtailcall sig ros :: c) rs fr m)
         E0 (Callstate s f' rs (Mem.free m stk))
-
-  | exec_Malloc:
-      forall s f sp c rs fr m sz m' blk,
-      rs (Conventions.loc_alloc_argument) = Vint sz ->
-      Mem.alloc m 0 (Int.signed sz) = (m', blk) ->
-      step (State s f sp (Malloc :: c) rs fr m)
-        E0 (State s f sp c
-                   (rs#Conventions.loc_alloc_result <- (Vptr blk Int.zero))
-                    fr m')
   | exec_Mgoto:
       forall s f sp lbl c rs fr m c',
       find_label lbl f.(fn_code) = Some c' ->
@@ -280,13 +273,13 @@ Inductive step: state -> trace -> state -> Prop :=
         E0 (State s f sp c' rs fr m)
   | exec_Mcond_true:
       forall s f sp cond args lbl c rs fr m c',
-      eval_condition cond rs##args m = Some true ->
+      eval_condition cond rs##args = Some true ->
       find_label lbl f.(fn_code) = Some c' ->
       step (State s f sp (Mcond cond args lbl :: c) rs fr m)
         E0 (State s f sp c' rs fr m)
   | exec_Mcond_false:
       forall s f sp cond args lbl c rs fr m,
-      eval_condition cond rs##args m = Some false ->
+      eval_condition cond rs##args = Some false ->
       step (State s f sp (Mcond cond args lbl :: c) rs fr m)
         E0 (State s f sp c rs fr m)
   | exec_Mreturn: