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/RTL.v | 46 ++++++++++++++++++++++++++++++---------------- 1 file changed, 30 insertions(+), 16 deletions(-) (limited to 'backend/RTL.v') diff --git a/backend/RTL.v b/backend/RTL.v index 7471997..b1afc94 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 v1.2.3