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 --- backend/Csharpminor.v | 563 -------------------------------------------------- 1 file changed, 563 deletions(-) delete mode 100644 backend/Csharpminor.v (limited to 'backend/Csharpminor.v') diff --git a/backend/Csharpminor.v b/backend/Csharpminor.v deleted file mode 100644 index 246ebf53..00000000 --- a/backend/Csharpminor.v +++ /dev/null @@ -1,563 +0,0 @@ -(** 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