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 --- cfrontend/Csharpminor.v | 32 ++++++++++++++++++-------------- 1 file changed, 18 insertions(+), 14 deletions(-) (limited to 'cfrontend/Csharpminor.v') diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v index 729814e..7d805c3 100644 --- a/cfrontend/Csharpminor.v +++ b/cfrontend/Csharpminor.v @@ -23,7 +23,7 @@ Require Cminor. [Elet] construct. Unlike in Cminor (the next intermediate language of the back-end), - Csharpminor local variables reside in memory, and their address can + Csharpminor local variables reside in memory, and their addresses can be taken using [Eaddrof] expressions. *) @@ -37,9 +37,9 @@ Definition binary_operation : Set := Cminor.binary_operation. Inductive expr : Set := | Evar : ident -> expr (**r reading a scalar variable *) | Eaddrof : ident -> expr (**r taking the address of a variable *) - | Econst : constant -> expr - | Eunop : unary_operation -> expr -> expr - | Ebinop : binary_operation -> expr -> expr -> expr + | Econst : constant -> expr (**r constants *) + | Eunop : unary_operation -> expr -> expr (**r unary operation *) + | Ebinop : binary_operation -> expr -> expr -> expr (**r binary operation *) | Eload : memory_chunk -> expr -> expr (**r memory read *) | Ecall : signature -> expr -> exprlist -> expr (**r function call *) | Econdition : expr -> expr -> expr -> expr (**r conditional expression *) @@ -138,10 +138,12 @@ Fixpoint switch_target (n: int) (dfl: nat) (cases: list (int * nat)) (** Four kinds of evaluation environments are involved: - [genv]: global environments, define symbols and functions; -- [gvarenv]: map global variables to var info; -- [env]: local environments, map local variables to memory blocks + var info; +- [gvarenv]: map global variables to variable informations (type [var_kind]); +- [env]: local environments, map local variables + to memory blocks and variable informations; - [lenv]: let environments, map de Bruijn indices to values. *) + Definition genv := Genv.t fundef. Definition gvarenv := PTree.t var_kind. Definition env := PTree.t (block * var_kind). @@ -250,11 +252,12 @@ Inductive eval_var_ref: env -> ident -> block -> memory_chunk -> Prop := PTree.get id (global_var_env prg) = Some (Vscalar chunk) -> eval_var_ref e id b chunk. -(** Evaluation of an expression: [eval_expr prg le e m a m' v] states +(** Evaluation of an expression: [eval_expr prg le e m a t m' v] states that expression [a], in initial memory state [m], evaluates to value [v]. [m'] is the final memory state, respectively, reflecting - memory stores possibly performed by [a]. [e] and [le] are the - local environment and let environment respectively. *) + memory stores possibly performed by [a]. [t] is the trace of input/output + events generated during the evaluation. + [e] and [le] are the local environment and let environment respectively. *) Inductive eval_expr: letenv -> env -> @@ -329,7 +332,7 @@ Inductive eval_expr: eval_expr le e m (Ealloc a) t m2 (Vptr b Int.zero) (** Evaluation of a list of expressions: - [eval_exprlist prg le al m a m' vl] + [eval_exprlist prg le al m a t m' vl] states that the list [al] of expressions evaluate to the list [vl] of values. The other parameters are as in [eval_expr]. @@ -349,7 +352,7 @@ with eval_exprlist: t = t1 ** t2 -> eval_exprlist le e m (Econs a bl) t m2 (v :: vl) -(** Evaluation of a function invocation: [eval_funcall prg m f args m' res] +(** Evaluation of a function invocation: [eval_funcall prg m f args t m' res] means that the function [f], applied to the arguments [args] in memory state [m], returns the value [res] in modified memory state [m']. *) @@ -369,7 +372,7 @@ with eval_funcall: event_match ef vargs t vres -> eval_funcall m (External ef) vargs t m vres -(** Execution of a statement: [exec_stmt prg e m s m' out] +(** Execution of a statement: [exec_stmt prg e m s t m' out] means that statement [s] executes with outcome [out]. The other parameters are as in [eval_expr]. *) @@ -460,9 +463,10 @@ Scheme eval_expr_ind4 := Minimality for eval_expr Sort Prop End RELSEM. -(** Execution of a whole program: [exec_program p r] +(** Execution of a whole program: [exec_program p t r] holds if the application of [p]'s main function to no arguments - in the initial memory state for [p] eventually returns value [r]. *) + in the initial memory state for [p] performs the events described + in trace [t] and eventually returns value [r]. *) Definition exec_program (p: program) (t: trace) (r: val) : Prop := let ge := Genv.globalenv p in -- cgit v1.2.3