Documentation

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

6 files changed, 126 insertions, 119 deletions

diff --git a/backend/LTL.v b/backend/LTL.v
index edb8ecc5..db996ba4 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -124,43 +124,37 @@ Definition set_result_reg (s: signature) (or: option loc) (ls: locset) :=
   | None => ls
   end.
 
-(** The components of an LTL execution state are:
-
-- [State cs f sp pc ls m]: [f] is the function currently executing.
-  [sp] is the stack pointer (as in RTL).  [pc] is the current
-  program point (CFG node) within the code of [f].
-  [ls] maps locations to their current values. [m] is the current
-  memory state.
-- [Callstate cs f ls m]:
-  [f] is the function definition that we are calling.
-  [ls] is the values of locations just before the call.
-  [m] is the current memory state.
-- [Returnstate cs sig ls m]:
-  [sig] is the signature of the function that just returned.
-  [ls] is the values of locations just before the return.
-  [m] is the current memory state.
-
-[cs] is a list of stack frames [Stackframe res f sp ls pc],
-where [res] is the location that will receive the result of the call,
-[f] is the calling function, [sp] its stack pointer,
-[ls] the values of locations just before the call,
-and [pc] the program point within [f] of the successor of the
-[Lcall] instruction. *)
+(** LTL execution states. *)
 
 Inductive stackframe : Set :=
   | Stackframe:
-      forall (res: loc) (f: function) (sp: val) (ls: locset) (pc: node), 
+      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 *)
+             (pc: node),        (**r program point in calling function *)
       stackframe.
 
 Inductive state : Set :=
   | State:
-      forall (stack: list stackframe) (f: function) (sp: val)
-             (pc: node) (ls: locset) (m: mem), state
+      forall (stack: list stackframe) (**r call stack *)
+             (f: function)            (**r function currently executing *)
+             (sp: val)                (**r stack pointer *)
+             (pc: node)               (**r current program point *)
+             (ls: locset)             (**r location state *)
+             (m: mem),                (**r memory state *)
+      state
   | Callstate:
-      forall (stack: list stackframe) (f: fundef) (ls: locset) (m: mem),
+      forall (stack: list stackframe) (**r call stack *)
+             (f: fundef)              (**r function to call *)
+             (ls: locset)             (**r location state at point of call *)
+             (m: mem),                (**r memory state *)
       state
   | Returnstate:
-      forall (stack: list stackframe) (sig: signature) (ls: locset) (m: mem),
+      forall (stack: list stackframe) (**r call stack *)
+             (sig: signature)         (**r signature of returning function *)
+             (ls: locset)             (**r location state at point of return *)
+             (m: mem),                (**r memory state *)
       state.
 
 Definition parent_locset (stack: list stackframe) : locset :=
diff --git a/backend/LTLin.v b/backend/LTLin.v
index 368c13cd..da8719ac 100644
--- a/backend/LTLin.v
+++ b/backend/LTLin.v
@@ -100,18 +100,33 @@ Fixpoint find_label (lbl: label) (c: code) {struct c} : option code :=
 
 Inductive stackframe : Set :=
   | Stackframe:
-      forall (res: loc) (f: function) (sp: val) (ls: locset) (c: code), 
+      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 *)
+             (c: code),       (**r program point in calling function *)
       stackframe.
 
 Inductive state : Set :=
   | State:
-      forall (stack: list stackframe) (f: function) (sp: val)
-             (c: code) (ls: locset) (m: mem), state
+      forall (stack: list stackframe) (**r call stack *)
+             (f: function)            (**r function currently executing *)
+             (sp: val)                (**r stack pointer *)
+             (c: code)                (**r current program point *)
+             (ls: locset)             (**r location state *)
+             (m: mem),                (**r memory state *)
+      state
   | Callstate:
-      forall (stack: list stackframe) (f: fundef) (ls: locset) (m: mem),
+      forall (stack: list stackframe) (**r call stack *)
+             (f: fundef)              (**r function to call *)
+             (ls: locset)             (**r location state at point of call *)
+             (m: mem),                (**r memory state *)
       state
   | Returnstate:
-      forall (stack: list stackframe) (sig: signature) (ls: locset) (m: mem),
+      forall (stack: list stackframe) (**r call stack *)
+             (sig: signature)         (**r signature of returning function *)
+             (ls: locset)             (**r location state at point of return *)
+             (m: mem),                (**r memory state *)
       state.
 
 Definition parent_locset (stack: list stackframe) : locset :=
diff --git a/backend/Linear.v b/backend/Linear.v
index 65803710..a6e31fb6 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -104,44 +104,35 @@ Definition find_function (ros: mreg + ident) (rs: locset) : option fundef :=
 Definition reglist (rs: locset) (rl: list mreg) : list val :=
   List.map (fun r => rs (R r)) rl.
 
-(** The components of a Linear execution state are:
-
-- [State cs f sp c rs m]: [f] is the function currently executing.
-  [sp] is the stack pointer.  [c] is the sequence of instructions
-  that remain to be executed.
-  [rs] maps locations to their current values. [m] is the current
-  memory state.
-
-- [Callstate cs f rs m]:
-  [f] is the function definition that we are calling.
-  [rs] is the values of locations just before the call.
-  [m] is the current memory state.
-
-- [Returnstate cs rs m]:
-  [rs] is the values of locations just before the return.
-  [m] is the current memory state.
-
-[cs] is a list of stack frames [Stackframe res f rs pc].
-[f] is the calling function, [sp] its stack pointer.
-[rs] the values of locations just before the call.
-[c] is the sequence of instructions following the call in the code of [f].
-*)
+(** Linear execution states. *)
 
 Inductive stackframe: Set :=
   | Stackframe:
-      forall (f: function) (sp: val) (rs: locset) (c: code),
+      forall (f: function)         (**r calling function *)
+             (sp: val)             (**r stack pointer in calling function *)
+             (rs: locset)          (**r location state in calling function *)
+             (c: code),            (**r program point in calling function *)
       stackframe.
 
 Inductive state: Set :=
   | State:
-      forall (stack: list stackframe) (f: function) (sp: val)
-             (c: code) (rs: locset) (m: mem),
+      forall (stack: list stackframe) (**r call stack *)
+             (f: function)            (**r function currently executing *)
+             (sp: val)                (**r stack pointer *)
+             (c: code)                (**r current program point *)
+             (rs: locset)             (**r location state *)
+             (m: mem),                (**r memory state *)
       state
   | Callstate:
-      forall (stack: list stackframe) (f: fundef) (rs: locset) (m: mem),
+      forall (stack: list stackframe) (**r call stack *)
+             (f: fundef)              (**r function to call *)
+             (rs: locset)             (**r location state at point of call *)
+             (m: mem),                (**r memory state *)
       state
   | Returnstate:
-      forall (stack: list stackframe) (rs: locset) (m: mem),
+      forall (stack: list stackframe) (**r call stack *)
+             (rs: locset)             (**r location state at point of return *)
+             (m: mem),                (**r memory state *)
       state.
 
 (** [parent_locset cs] returns the mapping of values for locations
diff --git a/backend/Machabstr.v b/backend/Machabstr.v
index ad4e8e1a..0abdd1e1 100644
--- a/backend/Machabstr.v
+++ b/backend/Machabstr.v
@@ -102,38 +102,36 @@ Definition extcall_arguments
    (rs: regset) (fr: frame) (sg: signature) (args: list val) : Prop :=
   extcall_args rs fr (Conventions.loc_arguments sg) args.
     
-(** The components of an execution state are:
-
-- [State cs f sp c rs fr m]: [f] is the function currently executing.
-  [sp] is the stack pointer.  [c] is the list of instructions that
-  remain to be executed.  [rs] assigns values to registers. 
-  [fr] is the current frame, as described above.  [m] is the memory state.
-- [Callstate cs f rs m]: [f] is the function definition being called.
-  [rs] is the current values of registers,
-  and [m] the current memory state.
-- [Returnstate cs rs m]: [rs] is the current values of registers,
-  and [m] the current memory state.
-
-[cs] is a list of stack frames [Stackframe f sp c fr],
-where [f] is the block reference for the calling function,
-[c] the code within this function that follows the call instruction,
-[sp] its stack pointer, and [fr] its private frame. *)
+(** Mach execution states. *)
 
 Inductive stackframe: Set :=
   | Stackframe:
-      forall (f: function) (sp: val) (c: code) (fr: frame),
+      forall (f: function)      (**r calling function *)
+             (sp: val)          (**r stack pointer in calling function *)
+             (c: code)          (**r program point in calling function *)
+             (fr: frame),       (**r frame state in calling function *)
       stackframe.
 
 Inductive state: Set :=
   | State:
-      forall (stack: list stackframe) (f: function) (sp: val)
-             (c: code) (rs: regset) (fr: frame) (m: mem),
+      forall (stack: list stackframe) (**r call stack *)
+             (f: function)            (**r function currently executing *)
+             (sp: val)                (**r stack pointer *)
+             (c: code)                (**r current program point *)
+             (rs: regset)             (**r register state *)
+             (fr: frame)              (**r frame state *)
+             (m: mem),                (**r memory state *)
       state
   | Callstate:
-      forall (stack: list stackframe) (f: fundef) (rs: regset) (m: mem),
+      forall (stack: list stackframe) (**r call stack *)
+             (f: fundef)              (**r function to call *)
+             (rs: regset)             (**r register state *)
+             (m: mem),                (**r memory state *)
       state
   | Returnstate:
-      forall (stack: list stackframe) (rs: regset) (m: mem),
+      forall (stack: list stackframe) (**r call stack *)
+             (rs: regset)             (**r register state *)
+             (m: mem),                (**r memory state *)
       state.
 
 (** [parent_frame s] returns the frame of the calling function.
diff --git a/backend/Machconcr.v b/backend/Machconcr.v
index fe9a7d90..5a095d79 100644
--- a/backend/Machconcr.v
+++ b/backend/Machconcr.v
@@ -71,40 +71,35 @@ Definition extcall_arguments
    (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop :=
   extcall_args rs m sp (Conventions.loc_arguments sg) args.
 
-(** The components of an execution state are:
-
-- [State cs f sp c rs m]: [f] is the block reference corresponding
-  to the function currently executing.  [sp] is the stack pointer.
-  [c] is the list of instructions that remain to be executed.
-  [rs] assigns values to registers.  [m] is the memory state.
-- [Callstate cs f rs m]: [f] is the block reference corresponding
-  to the function being called. [rs] is the current values of registers,
-  and [m] the current memory state.
-- [Returnstate cs rs m]: [rs] is the current values of registers,
-  and [m] the current memory state.
-
-[cs] is a list of stack frames [Stackframe f sp retaddr c],
-where [f] is the block reference for the calling function,
-[c] the code within this function that follows the call instruction,
-[sp] its stack pointer, and [retaddr] the return address predicted
-by [PPCgenretaddr.return_address_offset].
-*)
+(** Mach execution states. *)
 
 Inductive stackframe: Set :=
   | Stackframe:
-      forall (f: block) (sp retaddr: val) (c: code),
+      forall (f: block)       (**r pointer to calling function *)
+             (sp: val)        (**r stack pointer in calling function *)
+             (retaddr: val)   (**r PPC return address in calling function *)
+             (c: code),       (**r program point in calling function *)
       stackframe.
 
 Inductive state: Set :=
   | State:
-      forall (stack: list stackframe) (f: block) (sp: val)
-             (c: code) (rs: regset) (m: mem),
+      forall (stack: list stackframe)  (**r call stack *)
+             (f: block)                (**r pointer to current function *)
+             (sp: val)                 (**r stack pointer *)
+             (c: code)                 (**r current program point *)
+             (rs: regset)              (**r register state *)
+             (m: mem),                 (**r memory state *)
       state
   | Callstate:
-      forall (stack: list stackframe) (f: block) (rs: regset) (m: mem),
+      forall (stack: list stackframe)  (**r call stack *)
+             (f: block)                (**r pointer to function to call *)
+             (rs: regset)              (**r register state *)
+             (m: mem),                 (**r memory state *)
       state
   | Returnstate:
-      forall (stack: list stackframe) (rs: regset) (m: mem),
+      forall (stack: list stackframe)  (**r call stack *)
+             (rs: regset)              (**r register state *)
+             (m: mem),                 (**r memory state *)
       state.
 
 Definition parent_sp (s: list stackframe) : val :=
diff --git a/backend/RTL.v b/backend/RTL.v
index 74719977..b1afc94a 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -112,22 +112,6 @@ Fixpoint init_regs (vl: list val) (rl: list reg) {struct rl} : regset :=
   | _, _ => Regmap.init Vundef
   end.
 
-Inductive stackframe : Set :=
-  | Stackframe:
-      forall (res: reg) (c: code) (sp: val) (pc: node) (rs: regset), 
-      stackframe.
-
-Inductive state : Set :=
-  | State:
-      forall (stack: list stackframe) (c: code) (sp: val) (pc: node)
-             (rs: regset) (m: mem), state
-  | Callstate:
-      forall (stack: list stackframe) (f: fundef) (args: list val) (m: mem),
-      state
-  | Returnstate:
-      forall (stack: list stackframe) (v: val) (m: mem),
-      state.
-
 (** The dynamic semantics of RTL is given in small-step style, as a 
   set of transitions between states.  A state captures the current
   point in the execution.  Three kinds of states appear in the transitions:
@@ -158,6 +142,36 @@ a function call in progress.
 [rs] is the state of registers in the calling function.
 *)
 
+Inductive stackframe : Set :=
+  | Stackframe:
+      forall (res: reg)            (**r where to store the result *)
+             (c: code)             (**r code of calling function *)
+             (sp: val)             (**r stack pointer in calling function *)
+             (pc: node)            (**r program point in calling function *)
+             (rs: regset),         (**r register state in calling function *)
+      stackframe.
+
+Inductive state : Set :=
+  | State:
+      forall (stack: list stackframe) (**r call stack *)
+             (c: code)                (**r current code *)
+             (sp: val)                (**r stack pointer *)
+             (pc: node)               (**r current program point in [c] *)
+             (rs: regset)             (**r register state *)
+             (m: mem),                (**r memory state *)
+      state
+  | Callstate:
+      forall (stack: list stackframe) (**r call stack *)
+             (f: fundef)              (**r function to call *)
+             (args: list val)         (**r arguments to the call *)
+             (m: mem),                (**r memory state *)
+      state
+  | Returnstate:
+      forall (stack: list stackframe) (**r call stack *)
+             (v: val)                 (**r return value for the call *)
+             (m: mem),                (**r memory state *)
+      state.
+
 Section RELSEM.
 
 Variable ge: genv.