Simplification de la semantique de LTL et LTLin. Les details lies aux conventions d'appel sont maintenant geres de maniere plus locale dans la passe Reload.

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

1 files changed, 48 insertions, 96 deletions

diff --git a/backend/LTL.v b/backend/LTL.v
index a082e12..e39a4ec 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -72,53 +72,20 @@ Definition funsig (fd: fundef) :=
 Definition genv := Genv.t fundef.
 Definition locset := Locmap.t.
 
-Section RELSEM.
-
-(** Calling conventions are reflected at the level of location sets
-  (environments mapping locations to values) by the following two 
-  functions.  
+Definition locmap_optget (ol: option loc) (dfl: val) (ls: locset) : val :=
+  match ol with
+  | None => dfl
+  | Some l => ls l
+  end.
 
-  [call_regs caller] returns the location set at function entry,
-  as a function of the location set [caller] of the calling function.
-- Machine registers have the same values as in the caller.
-- Incoming stack slots (used for parameter passing) have the same
-  values as the corresponding outgoing stack slots (used for argument
-  passing) in the caller.
-- Local and outgoing stack slots are initialized to undefined values.
-*) 
+Fixpoint init_locs (vl: list val) (rl: list loc) {struct rl} : locset :=
+  match rl, vl with
+  | r1 :: rs, v1 :: vs => Locmap.set r1 v1 (init_locs vs rs)
+  | _, _ => Locmap.init Vundef
+  end.
 
-Definition call_regs (caller: locset) : locset :=
-  fun (l: loc) =>
-    match l with
-    | R r => caller (R r)
-    | S (Local ofs ty) => Vundef
-    | S (Incoming ofs ty) => caller (S (Outgoing ofs ty))
-    | S (Outgoing ofs ty) => Vundef
-    end.
 
-(** [return_regs caller callee] returns the location set after
-  a call instruction, as a function of the location set [caller]
-  of the caller before the call instruction and of the location
-  set [callee] of the callee at the return instruction.
-- Callee-save machine registers have the same values as in the caller
-  before the call.
-- Caller-save machine registers have the same values
-  as in the callee at the return point.
-- Stack slots have the same values as in the caller before the call.
-*)
-
-Definition return_regs (caller callee: locset) : locset :=
-  fun (l: loc) =>
-    match l with
-    | R r =>
-        if In_dec Loc.eq (R r) Conventions.temporaries then
-          callee (R r)
-        else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then
-          callee (R r)
-        else
-          caller (R r)
-    | S s => caller (S s)
-    end.
+Section RELSEM.
 
 (** [parmov srcs dsts ls] performs the parallel assignment
   of locations [dsts] to the values of the corresponding locations
@@ -130,18 +97,29 @@ Fixpoint parmov (srcs dsts: list loc) (ls: locset) {struct srcs} : locset :=
   | _, _ => ls
   end.
 
-Definition set_result_reg (s: signature) (or: option loc) (ls: locset) :=
-  match or with 
-  | Some r => Locmap.set (R (loc_result s)) (ls r) ls
-  | None => ls
-  end.
+(** [postcall_regs ls] returns the location set [ls] after a function
+  call.  Caller-save registers and temporary registers
+  are set to [undef], reflecting the fact that the called
+  function can modify them freely. *)
+
+Definition postcall_regs (ls: locset) : locset :=
+  fun (l: loc) =>
+    match l with
+    | R r =>
+        if In_dec Loc.eq (R r) Conventions.temporaries then
+          Vundef
+        else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then
+          Vundef
+        else
+          ls (R r)
+    | S s => ls (S s)
+    end.
 
 (** LTL execution states. *)
 
 Inductive stackframe : Set :=
   | Stackframe:
-      forall (sig: signature)   (**r signature of call *)
-             (res: loc)         (**r where to store the result *)
+      forall (res: loc)         (**r where to store the result *)
              (f: function)      (**r calling function *)
              (sp: val)          (**r stack pointer in calling function *)
              (ls: locset)       (**r location state in calling function *)
@@ -160,27 +138,15 @@ Inductive state : Set :=
   | Callstate:
       forall (stack: list stackframe) (**r call stack *)
              (f: fundef)              (**r function to call *)
-             (ls: locset)             (**r location state at point of call *)
+             (args: list val)         (**r arguments to the call *)
              (m: mem),                (**r memory state *)
       state
   | Returnstate:
       forall (stack: list stackframe) (**r call stack *)
-             (ls: locset)             (**r location state at point of return *)
+             (v: val)                 (**r return value for the call *)
              (m: mem),                (**r memory state *)
       state.
 
-Definition parent_locset (stack: list stackframe) : locset :=
-  match stack with
-  | nil => Locmap.init Vundef
-  | Stackframe sg res f sp ls pc :: stack' => ls
-  end.
-
-Definition parent_callsig (stack: list stackframe) : signature :=
-  match stack with
-  | nil => mksignature nil (Some Tint)
-  | Stackframe sg res f sp ls pc :: stack' => sg
-  end.
-
 Variable ge: genv.
 
 Definition find_function (los: loc + ident) (rs: locset) : option fundef :=
@@ -265,28 +231,23 @@ Inductive step: state -> trace -> state -> Prop :=
       (fn_code f)!pc = Some(Lcall sig ros args res pc') ->
       find_function ros rs = Some f' ->
       funsig f' = sig ->
-      let rs1 := parmov args (loc_arguments sig) rs in
       step (State s f sp pc rs m)
-        E0 (Callstate (Stackframe sig res f sp rs1 pc' :: s) f' rs1 m)
+        E0 (Callstate (Stackframe res f sp (postcall_regs rs) pc' :: s)
+                      f' (List.map rs args) m)
   | exec_Ltailcall:
       forall s f stk pc rs m sig ros args f',
       (fn_code f)!pc = Some(Ltailcall sig ros args) ->
       find_function ros rs = Some f' ->
       funsig f' = sig ->
-      let rs1 := parmov args (loc_arguments sig) rs in
-      let rs2 := return_regs (parent_locset s) rs1 in
       step (State s f (Vptr stk Int.zero) pc rs m)
-        E0 (Callstate s f' rs2 (Mem.free m stk))
+        E0 (Callstate s f' (List.map rs args) (Mem.free m stk))
   | exec_Lalloc:
       forall s f sp pc rs m pc' arg res sz m' b,
       (fn_code f)!pc = Some(Lalloc arg res pc') ->
       rs arg = Vint sz ->
       Mem.alloc m 0 (Int.signed sz) = (m', b) ->
-      let rs1 := Locmap.set (R loc_alloc_argument) (rs arg) rs in
-      let rs2 := Locmap.set (R loc_alloc_result) (Vptr b Int.zero) rs1 in
-      let rs3 := Locmap.set res (rs2 (R loc_alloc_result)) rs2 in
       step (State s f sp pc rs m)
-        E0 (State s f sp pc' rs3 m')
+        E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_regs rs)) m')
   | exec_Lcond_true:
       forall s f sp pc rs m cond args ifso ifnot,
       (fn_code f)!pc = Some(Lcond cond args ifso ifnot) ->
@@ -302,30 +263,22 @@ Inductive step: state -> trace -> state -> Prop :=
   | exec_Lreturn:
       forall s f stk pc rs m or,
       (fn_code f)!pc = Some(Lreturn or) ->
-      let rs1 := set_result_reg f.(fn_sig) or rs in
-      let rs2 := return_regs (parent_locset s) rs1 in
       step (State s f (Vptr stk Int.zero) pc rs m)
-        E0 (Returnstate s rs2 (Mem.free m stk))
+        E0 (Returnstate s (locmap_optget or Vundef rs) (Mem.free m stk))
   | exec_function_internal:
-      forall s f rs m m' stk,
+      forall s f args m m' stk,
       Mem.alloc m 0 f.(fn_stacksize) = (m', stk) ->
-      let rs1 := call_regs rs in
-      let rs2 := parmov (loc_parameters f.(fn_sig)) f.(fn_params) rs1 in
-      step (Callstate s (Internal f) rs m)
-        E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) rs2 m')
+      step (Callstate s (Internal f) args m)
+        E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) (init_locs args f.(fn_params)) m')
   | exec_function_external:
-      forall s ef t res rs m,
-      let args := map rs (Conventions.loc_arguments ef.(ef_sig)) in
+      forall s ef t args res m,
       event_match ef args t res ->
-      let rs1 :=
-        Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in
-      step (Callstate s (External ef) rs m)
-         t (Returnstate s rs1 m)
+      step (Callstate s (External ef) args m)
+         t (Returnstate s res m)
   | exec_return:
-      forall res f sp rs0 pc s sig rs m,
-      let rs1 := Locmap.set res (rs (R (loc_result sig))) rs in
-      step (Returnstate (Stackframe sig res f sp rs0 pc :: s) rs m)
-        E0 (State s f sp pc rs1 m).
+      forall res f sp rs pc s vres m,
+      step (Returnstate (Stackframe res f sp rs pc :: s) vres m)
+        E0 (State s f sp pc (Locmap.set res vres rs) m).
 
 End RELSEM.
 
@@ -341,12 +294,11 @@ Inductive initial_state (p: program): state -> Prop :=
       Genv.find_symbol ge p.(prog_main) = Some b ->
       Genv.find_funct_ptr ge b = Some f ->
       funsig f = mksignature nil (Some Tint) ->
-      initial_state p (Callstate nil f (Locmap.init Vundef) m0).
+      initial_state p (Callstate nil f nil m0).
 
 Inductive final_state: state -> int -> Prop :=
-  | final_state_intro: forall rs m r,
-      rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r ->
-      final_state (Returnstate nil rs m) r.
+  | final_state_intro: forall n m,
+      final_state (Returnstate nil (Vint n) m) n.
 
 Definition exec_program (p: program) (beh: program_behavior) : Prop :=
   program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.