From a7c6cf8d4d59e29ed73f9eb8bfc015b0384672a1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:33:05 +0000 Subject: Revu la repartition des sources Coq en sous-repertoires git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@73 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csharpminor.v | 563 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 563 insertions(+) create mode 100644 cfrontend/Csharpminor.v (limited to 'cfrontend/Csharpminor.v') diff --git a/cfrontend/Csharpminor.v b/cfrontend/Csharpminor.v new file mode 100644 index 00000000..246ebf53 --- /dev/null +++ b/cfrontend/Csharpminor.v @@ -0,0 +1,563 @@ +(** Abstract syntax and semantics for the Csharpminor language. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import Mem. +Require Import Events. +Require Import Globalenvs. + +(** Abstract syntax *) + +(** Csharpminor is a low-level imperative language structured in expressions, + statements, functions and programs. Expressions include + reading global or local variables, reading store locations, + arithmetic operations, function calls, and conditional expressions + (similar to [e1 ? e2 : e3] in C). The [Elet] and [Eletvar] constructs + enable sharing the computations of subexpressions. De Bruijn notation + is used: [Eletvar n] refers to the value bound by then [n+1]-th enclosing + [Elet] construct. + + Unlike in Cminor (the next intermediate language of the back-end), + Csharpminor local variables reside in memory, and their address can + be taken using [Eaddrof] expressions. + + Another difference with Cminor is that Csharpminor is entirely + processor-neutral. In particular, Csharpminor uses a standard set of + operations: it does not reflect processor-specific operations nor + addressing modes. *) + +Inductive operation : Set := + | Ointconst: int -> operation (**r integer constant *) + | Ofloatconst: float -> operation (**r floating-point constant *) + | Ocast8unsigned: operation (**r 8-bit zero extension *) + | Ocast8signed: operation (**r 8-bit sign extension *) + | Ocast16unsigned: operation (**r 16-bit zero extension *) + | Ocast16signed: operation (**r 16-bit sign extension *) + | Onotint: operation (**r bitwise complement *) + | Oadd: operation (**r integer addition *) + | Osub: operation (**r integer subtraction *) + | Omul: operation (**r integer multiplication *) + | Odiv: operation (**r integer signed division *) + | Odivu: operation (**r integer unsigned division *) + | Omod: operation (**r integer signed modulus *) + | Omodu: operation (**r integer unsigned modulus *) + | Oand: operation (**r bitwise ``and'' *) + | Oor: operation (**r bitwise ``or'' *) + | Oxor: operation (**r bitwise ``xor'' *) + | Oshl: operation (**r left shift *) + | Oshr: operation (**r right signed shift *) + | Oshru: operation (**r right unsigned shift *) + | Onegf: operation (**r float opposite *) + | Oabsf: operation (**r float absolute value *) + | Oaddf: operation (**r float addition *) + | Osubf: operation (**r float subtraction *) + | Omulf: operation (**r float multiplication *) + | Odivf: operation (**r float division *) + | Osingleoffloat: operation (**r float truncation *) + | Ointoffloat: operation (**r integer to float *) + | Ofloatofint: operation (**r float to signed integer *) + | Ofloatofintu: operation (**r float to unsigned integer *) + | Ocmp: comparison -> operation (**r integer signed comparison *) + | Ocmpu: comparison -> operation (**r integer unsigned comparison *) + | Ocmpf: comparison -> operation. (**r float comparison *) + +Inductive expr : Set := + | Evar : ident -> expr (**r reading a scalar variable *) + | Eaddrof : ident -> expr (**r taking the address of a variable *) + | Eop : operation -> exprlist -> expr (**r arithmetic 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 *) + | Elet : expr -> expr -> expr (**r let binding *) + | Eletvar : nat -> expr (**r reference to a let-bound variable *) + | Ealloc : expr -> expr (**r memory allocation *) + +with exprlist : Set := + | Enil: exprlist + | Econs: expr -> exprlist -> exprlist. + +(** Statements include expression evaluation, variable assignment, + memory stores, an if/then/else conditional, + infinite loops, blocks and early block exits, and early function returns. + [Sexit n] terminates prematurely the execution of the [n+1] enclosing + [Sblock] statements. *) + +Inductive stmt : Set := + | Sskip: stmt + | Sexpr: expr -> stmt + | Sassign : ident -> expr -> stmt + | Sstore : memory_chunk -> expr -> expr -> stmt + | Sseq: stmt -> stmt -> stmt + | Sifthenelse: expr -> stmt -> stmt -> stmt + | Sloop: stmt -> stmt + | Sblock: stmt -> stmt + | Sexit: nat -> stmt + | Sswitch: expr -> list (int * nat) -> nat -> stmt + | Sreturn: option expr -> stmt. + +(** The variables can be either scalar variables + (whose type, size and signedness are given by a [memory_chunk] + or array variables (of the indicated sizes). The only operation + permitted on an array variable is taking its address. *) + +Inductive var_kind : Set := + | Vscalar: memory_chunk -> var_kind + | Varray: Z -> var_kind. + +(** Functions are composed of a signature, a list of parameter names + with associated memory chunks (parameters must be scalar), a list of + local variables with associated [var_kind] description, and a + statement representing the function body. *) + +Record function : Set := mkfunction { + fn_sig: signature; + fn_params: list (ident * memory_chunk); + fn_vars: list (ident * var_kind); + fn_body: stmt +}. + +Definition fundef := AST.fundef function. + +Record program : Set := mkprogram { + prog_funct: list (ident * fundef); + prog_main: ident; + prog_vars: list (ident * var_kind * list init_data) +}. + +Definition funsig (fd: fundef) := + match fd with + | Internal f => f.(fn_sig) + | External ef => ef.(ef_sig) + end. + +(** * Operational semantics *) + +(** The operational semantics for Csharpminor is given in big-step operational + style. Expressions evaluate to values, and statements evaluate to + ``outcomes'' indicating how execution should proceed afterwards. *) + +Inductive outcome: Set := + | Out_normal: outcome (**r continue in sequence *) + | Out_exit: nat -> outcome (**r terminate [n+1] enclosing blocks *) + | Out_return: option val -> outcome. (**r return immediately to caller *) + +Definition outcome_result_value + (out: outcome) (ot: option typ) (v: val) : Prop := + match out, ot with + | Out_normal, None => v = Vundef + | Out_return None, None => v = Vundef + | Out_return (Some v'), Some ty => v = v' + | _, _ => False + end. + +Definition outcome_block (out: outcome) : outcome := + match out with + | Out_normal => Out_normal + | Out_exit O => Out_normal + | Out_exit (S n) => Out_exit n + | Out_return optv => Out_return optv + end. + +Fixpoint switch_target (n: int) (dfl: nat) (cases: list (int * nat)) + {struct cases} : nat := + match cases with + | nil => dfl + | (n1, lbl1) :: rem => if Int.eq n n1 then lbl1 else switch_target n dfl rem + end. + +(** 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; +- [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). +Definition empty_env : env := PTree.empty (block * var_kind). +Definition letenv := list val. + +Definition sizeof (lv: var_kind) : Z := + match lv with + | Vscalar chunk => size_chunk chunk + | Varray sz => Zmax 0 sz + end. + +Definition program_of_program (p: program): AST.program fundef := + AST.mkprogram + p.(prog_funct) + p.(prog_main) + (List.map (fun x => match x with (id, k, init) => (id, init) end) p.(prog_vars)). + +Definition fn_variables (f: function) := + List.map + (fun id_chunk => (fst id_chunk, Vscalar (snd id_chunk))) f.(fn_params) + ++ f.(fn_vars). + +Definition fn_params_names (f: function) := + List.map (@fst ident memory_chunk) f.(fn_params). + +Definition fn_vars_names (f: function) := + List.map (@fst ident var_kind) f.(fn_vars). + +Definition global_var_env (p: program): gvarenv := + List.fold_left + (fun gve x => match x with (id, k, init) => PTree.set id k gve end) + p.(prog_vars) (PTree.empty var_kind). + +(** Evaluation of operator applications. *) + +Definition eval_compare_null (c: comparison) (n: int) : option val := + if Int.eq n Int.zero + then match c with Ceq => Some Vfalse | Cne => Some Vtrue | _ => None end + else None. + +Definition eval_operation (op: operation) (vl: list val) (m: mem): option val := + match op, vl with + | Ointconst n, nil => Some (Vint n) + | Ofloatconst n, nil => Some (Vfloat n) + | Ocast8unsigned, Vint n1 :: nil => Some (Vint (Int.cast8unsigned n1)) + | Ocast8signed, Vint n1 :: nil => Some (Vint (Int.cast8signed n1)) + | Ocast16unsigned, Vint n1 :: nil => Some (Vint (Int.cast16unsigned n1)) + | Ocast16signed, Vint n1 :: nil => Some (Vint (Int.cast16signed n1)) + | Onotint, Vint n1 :: nil => Some (Vint (Int.not n1)) + | Oadd, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.add n1 n2)) + | Oadd, Vint n1 :: Vptr b2 n2 :: nil => Some (Vptr b2 (Int.add n2 n1)) + | Oadd, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.add n1 n2)) + | Osub, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.sub n1 n2)) + | Osub, Vptr b1 n1 :: Vint n2 :: nil => Some (Vptr b1 (Int.sub n1 n2)) + | Osub, Vptr b1 n1 :: Vptr b2 n2 :: nil => + if eq_block b1 b2 then Some (Vint (Int.sub n1 n2)) else None + | Omul, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.mul n1 n2)) + | Odiv, Vint n1 :: Vint n2 :: nil => + if Int.eq n2 Int.zero then None else Some (Vint (Int.divs n1 n2)) + | Odivu, Vint n1 :: Vint n2 :: nil => + if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2)) + | Omod, Vint n1 :: Vint n2 :: nil => + if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2)) + | Omodu, Vint n1 :: Vint n2 :: nil => + if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2)) + | Oand, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.and n1 n2)) + | Oor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.or n1 n2)) + | Oxor, Vint n1 :: Vint n2 :: nil => Some (Vint (Int.xor n1 n2)) + | Oshl, Vint n1 :: Vint n2 :: nil => + if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shl n1 n2)) else None + | Oshr, Vint n1 :: Vint n2 :: nil => + if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None + | Oshru, Vint n1 :: Vint n2 :: nil => + if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None + | Onegf, Vfloat f1 :: nil => Some (Vfloat (Float.neg f1)) + | Oabsf, Vfloat f1 :: nil => Some (Vfloat (Float.abs f1)) + | Oaddf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.add f1 f2)) + | Osubf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.sub f1 f2)) + | Omulf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.mul f1 f2)) + | Odivf, Vfloat f1 :: Vfloat f2 :: nil => Some (Vfloat (Float.div f1 f2)) + | Osingleoffloat, Vfloat f1 :: nil => + Some (Vfloat (Float.singleoffloat f1)) + | Ointoffloat, Vfloat f1 :: nil => + Some (Vint (Float.intoffloat f1)) + | Ofloatofint, Vint n1 :: nil => + Some (Vfloat (Float.floatofint n1)) + | Ofloatofintu, Vint n1 :: nil => + Some (Vfloat (Float.floatofintu n1)) + | Ocmp c, Vint n1 :: Vint n2 :: nil => + Some (Val.of_bool(Int.cmp c n1 n2)) + | Ocmp c, Vptr b1 n1 :: Vptr b2 n2 :: nil => + if valid_pointer m b1 (Int.signed n1) + && valid_pointer m b2 (Int.signed n2) then + if eq_block b1 b2 then Some(Val.of_bool(Int.cmp c n1 n2)) else None + else + None + | Ocmp c, Vptr b1 n1 :: Vint n2 :: nil => eval_compare_null c n2 + | Ocmp c, Vint n1 :: Vptr b2 n2 :: nil => eval_compare_null c n1 + | Ocmpu c, Vint n1 :: Vint n2 :: nil => + Some (Val.of_bool(Int.cmpu c n1 n2)) + | Ocmpf c, Vfloat f1 :: Vfloat f2 :: nil => + Some (Val.of_bool (Float.cmp c f1 f2)) + | _, _ => None + end. + +(** Allocation of local variables at function entry. Each variable is + bound to the reference to a fresh block of the appropriate size. *) + +Inductive alloc_variables: env -> mem -> + list (ident * var_kind) -> + env -> mem -> list block -> Prop := + | alloc_variables_nil: + forall e m, + alloc_variables e m nil e m nil + | alloc_variables_cons: + forall e m id lv vars m1 b1 m2 e2 lb, + Mem.alloc m 0 (sizeof lv) = (m1, b1) -> + alloc_variables (PTree.set id (b1, lv) e) m1 vars e2 m2 lb -> + alloc_variables e m ((id, lv) :: vars) e2 m2 (b1 :: lb). + +(** Initialization of local variables that are parameters. The value + of the corresponding argument is stored into the memory block + bound to the parameter. *) + +Inductive bind_parameters: env -> + mem -> list (ident * memory_chunk) -> list val -> + mem -> Prop := + | bind_parameters_nil: + forall e m, + bind_parameters e m nil nil m + | bind_parameters_cons: + forall e m id chunk params v1 vl b m1 m2, + PTree.get id e = Some (b, Vscalar chunk) -> + Mem.store chunk m b 0 v1 = Some m1 -> + bind_parameters e m1 params vl m2 -> + bind_parameters e m ((id, chunk) :: params) (v1 :: vl) m2. + +Section RELSEM. + +Variable prg: program. +Let ge := Genv.globalenv (program_of_program prg). + +(* Evaluation of the address of a variable: + [eval_var_addr prg ge e id b] states that variable [id] + in environment [e] evaluates to block [b]. *) + +Inductive eval_var_addr: env -> ident -> block -> Prop := + | eval_var_addr_local: + forall e id b vi, + PTree.get id e = Some (b, vi) -> + eval_var_addr e id b + | eval_var_addr_global: + forall e id b, + PTree.get id e = None -> + Genv.find_symbol ge id = Some b -> + eval_var_addr e id b. + +(* Evaluation of a reference to a scalar variable: + [eval_var_ref prg ge e id b chunk] states + that variable [id] in environment [e] evaluates to block [b] + and is associated with the memory chunk [chunk]. *) + +Inductive eval_var_ref: env -> ident -> block -> memory_chunk -> Prop := + | eval_var_ref_local: + forall e id b chunk, + PTree.get id e = Some (b, Vscalar chunk) -> + eval_var_ref e id b chunk + | eval_var_ref_global: + forall e id b chunk, + PTree.get id e = None -> + Genv.find_symbol ge id = Some b -> + 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 + 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. *) + +Inductive eval_expr: + letenv -> env -> + mem -> expr -> trace -> mem -> val -> Prop := + | eval_Evar: + forall le e m id b chunk v, + eval_var_ref e id b chunk -> + Mem.load chunk m b 0 = Some v -> + eval_expr le e m (Evar id) E0 m v + | eval_Eaddrof: + forall le e m id b, + eval_var_addr e id b -> + eval_expr le e m (Eaddrof id) E0 m (Vptr b Int.zero) + | eval_Eop: + forall le e m op al t m1 vl v, + eval_exprlist le e m al t m1 vl -> + eval_operation op vl m1 = Some v -> + eval_expr le e m (Eop op al) t m1 v + | eval_Eload: + forall le e m chunk a t m1 v1 v, + eval_expr le e m a t m1 v1 -> + Mem.loadv chunk m1 v1 = Some v -> + eval_expr le e m (Eload chunk a) t m1 v + | eval_Ecall: + forall le e m sig a bl t1 m1 t2 m2 t3 m3 vf vargs vres f t, + eval_expr le e m a t1 m1 vf -> + eval_exprlist le e m1 bl t2 m2 vargs -> + Genv.find_funct ge vf = Some f -> + funsig f = sig -> + eval_funcall m2 f vargs t3 m3 vres -> + t = t1 ** t2 ** t3 -> + eval_expr le e m (Ecall sig a bl) t m3 vres + | eval_Econdition_true: + forall le e m a b c t1 m1 v1 t2 m2 v2 t, + eval_expr le e m a t1 m1 v1 -> + Val.is_true v1 -> + eval_expr le e m1 b t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr le e m (Econdition a b c) t m2 v2 + | eval_Econdition_false: + forall le e m a b c t1 m1 v1 t2 m2 v2 t, + eval_expr le e m a t1 m1 v1 -> + Val.is_false v1 -> + eval_expr le e m1 c t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr le e m (Econdition a b c) t m2 v2 + | eval_Elet: + forall le e m a b t1 m1 v1 t2 m2 v2 t, + eval_expr le e m a t1 m1 v1 -> + eval_expr (v1::le) e m1 b t2 m2 v2 -> + t = t1 ** t2 -> + eval_expr le e m (Elet a b) t m2 v2 + | eval_Eletvar: + forall le e m n v, + nth_error le n = Some v -> + eval_expr le e m (Eletvar n) E0 m v + | eval_Ealloc: + forall le e m a t m1 n m2 b, + eval_expr le e m a t m1 (Vint n) -> + Mem.alloc m1 0 (Int.signed n) = (m2, b) -> + 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] + states that the list [al] of expressions evaluate + to the list [vl] of values. + The other parameters are as in [eval_expr]. +*) + +with eval_exprlist: + letenv -> env -> + mem -> exprlist -> trace -> + mem -> list val -> Prop := + | eval_Enil: + forall le e m, + eval_exprlist le e m Enil E0 m nil + | eval_Econs: + forall le e m a bl t1 m1 v t2 m2 vl t, + eval_expr le e m a t1 m1 v -> + eval_exprlist le e m1 bl t2 m2 vl -> + 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] + means that the function [f], applied to the arguments [args] in + memory state [m], returns the value [res] in modified memory state [m']. +*) +with eval_funcall: + mem -> fundef -> list val -> trace -> + mem -> val -> Prop := + | eval_funcall_internal: + forall m f vargs e m1 lb m2 t m3 out vres, + list_norepet (fn_params_names f ++ fn_vars_names f) -> + alloc_variables empty_env m (fn_variables f) e m1 lb -> + bind_parameters e m1 f.(fn_params) vargs m2 -> + exec_stmt e m2 f.(fn_body) t m3 out -> + outcome_result_value out f.(fn_sig).(sig_res) vres -> + eval_funcall m (Internal f) vargs t (Mem.free_list m3 lb) vres + | eval_funcall_external: + forall m ef vargs t vres, + 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] + means that statement [s] executes with outcome [out]. + The other parameters are as in [eval_expr]. *) + +with exec_stmt: + env -> + mem -> stmt -> trace -> + mem -> outcome -> Prop := + | exec_Sskip: + forall e m, + exec_stmt e m Sskip E0 m Out_normal + | exec_Sexpr: + forall e m a t m1 v, + eval_expr nil e m a t m1 v -> + exec_stmt e m (Sexpr a) t m1 Out_normal + | eval_Sassign: + forall e m id a t m1 b chunk v m2, + eval_expr nil e m a t m1 v -> + eval_var_ref e id b chunk -> + Mem.store chunk m1 b 0 v = Some m2 -> + exec_stmt e m (Sassign id a) t m2 Out_normal + | eval_Sstore: + forall e m chunk a b t1 m1 v1 t2 m2 v2 t3 m3, + eval_expr nil e m a t1 m1 v1 -> + eval_expr nil e m1 b t2 m2 v2 -> + Mem.storev chunk m2 v1 v2 = Some m3 -> + t3 = t1 ** t2 -> + exec_stmt e m (Sstore chunk a b) t3 m3 Out_normal + | exec_Sseq_continue: + forall e m s1 s2 t1 t2 m1 m2 t out, + exec_stmt e m s1 t1 m1 Out_normal -> + exec_stmt e m1 s2 t2 m2 out -> + t = t1 ** t2 -> + exec_stmt e m (Sseq s1 s2) t m2 out + | exec_Sseq_stop: + forall e m s1 s2 t1 m1 out, + exec_stmt e m s1 t1 m1 out -> + out <> Out_normal -> + exec_stmt e m (Sseq s1 s2) t1 m1 out + | exec_Sifthenelse_true: + forall e m a sl1 sl2 t1 m1 v1 t2 m2 out t, + eval_expr nil e m a t1 m1 v1 -> + Val.is_true v1 -> + exec_stmt e m1 sl1 t2 m2 out -> + t = t1 ** t2 -> + exec_stmt e m (Sifthenelse a sl1 sl2) t m2 out + | exec_Sifthenelse_false: + forall e m a sl1 sl2 t1 m1 v1 t2 m2 out t, + eval_expr nil e m a t1 m1 v1 -> + Val.is_false v1 -> + exec_stmt e m1 sl2 t2 m2 out -> + t = t1 ** t2 -> + exec_stmt e m (Sifthenelse a sl1 sl2) t m2 out + | exec_Sloop_loop: + forall e m sl t1 m1 t2 m2 out t, + exec_stmt e m sl t1 m1 Out_normal -> + exec_stmt e m1 (Sloop sl) t2 m2 out -> + t = t1 ** t2 -> + exec_stmt e m (Sloop sl) t m2 out + | exec_Sloop_stop: + forall e m sl t1 m1 out, + exec_stmt e m sl t1 m1 out -> + out <> Out_normal -> + exec_stmt e m (Sloop sl) t1 m1 out + | exec_Sblock: + forall e m sl t1 m1 out, + exec_stmt e m sl t1 m1 out -> + exec_stmt e m (Sblock sl) t1 m1 (outcome_block out) + | exec_Sexit: + forall e m n, + exec_stmt e m (Sexit n) E0 m (Out_exit n) + | exec_Sswitch: + forall e m a cases default t1 m1 n, + eval_expr nil e m a t1 m1 (Vint n) -> + exec_stmt e m (Sswitch a cases default) + t1 m1 (Out_exit (switch_target n default cases)) + | exec_Sreturn_none: + forall e m, + exec_stmt e m (Sreturn None) E0 m (Out_return None) + | exec_Sreturn_some: + forall e m a t1 m1 v, + eval_expr nil e m a t1 m1 v -> + exec_stmt e m (Sreturn (Some a)) t1 m1 (Out_return (Some v)). + +Scheme eval_expr_ind4 := Minimality for eval_expr Sort Prop + with eval_exprlist_ind4 := Minimality for eval_exprlist Sort Prop + with eval_funcall_ind4 := Minimality for eval_funcall Sort Prop + with exec_stmt_ind4 := Minimality for exec_stmt Sort Prop. + +End RELSEM. + +(** Execution of a whole program: [exec_program p r] + holds if the application of [p]'s main function to no arguments + in the initial memory state for [p] eventually returns value [r]. *) + +Definition exec_program (p: program) (t: trace) (r: val) : Prop := + let ge := Genv.globalenv (program_of_program p) in + let m0 := Genv.init_mem (program_of_program p) in + exists b, exists f, exists m, + Genv.find_symbol ge p.(prog_main) = Some b /\ + Genv.find_funct_ptr ge b = Some f /\ + funsig f = mksignature nil (Some Tint) /\ + eval_funcall p m0 f nil t m r. -- cgit