From c0bc146622528e3d52534909f5ae5cd2e375da8f Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 5 Aug 2007 13:41:45 +0000 Subject: Documentation git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@386 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/LTL.v | 48 +++++++++++++++++++++--------------------------- backend/LTLin.v | 25 ++++++++++++++++++++----- backend/Linear.v | 45 ++++++++++++++++++--------------------------- backend/Machabstr.v | 40 +++++++++++++++++++--------------------- backend/Machconcr.v | 41 ++++++++++++++++++----------------------- backend/RTL.v | 46 ++++++++++++++++++++++++++++++---------------- 6 files changed, 126 insertions(+), 119 deletions(-) (limited to 'backend') 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. -- cgit