From 73729d23ac13275c0d28d23bc1b1f6056104e5d9 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Sep 2006 15:08:29 +0000 Subject: Fusion de la branche "traces": - Ajout de traces d'evenements d'E/S dans les semantiques - Ajout constructions switch et allocation dynamique - Initialisation des variables globales - Portage Coq 8.1 beta Debut d'integration du front-end C: - Traduction Clight -> Csharpminor dans cfrontend/ - Modifications de Csharpminor et Globalenvs en consequence. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- cfrontend/Csem.v | 752 +++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 752 insertions(+) create mode 100644 cfrontend/Csem.v (limited to 'cfrontend/Csem.v') diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v new file mode 100644 index 0000000..b73e83c --- /dev/null +++ b/cfrontend/Csem.v @@ -0,0 +1,752 @@ +(** * Dynamic semantics for the Clight language *) + +Require Import Coqlib. +Require Import Maps. +Require Import Integers. +Require Import Floats. +Require Import Values. +Require Import AST. +Require Import Mem. +Require Import Events. +Require Import Globalenvs. +Require Import Csyntax. + +(** ** Semantics of type-dependent operations *) + +Inductive is_false: val -> type -> Prop := + | is_false_int: forall sz sg, + is_false (Vint Int.zero) (Tint sz sg) + | is_false_pointer: forall t, + is_false (Vint Int.zero) (Tpointer t) + | is_false_float: forall sz, + is_false (Vfloat Float.zero) (Tfloat sz). + +Inductive is_true: val -> type -> Prop := + | is_true_int_int: forall n sz sg, + n <> Int.zero -> + is_true (Vint n) (Tint sz sg) + | is_true_pointer_int: forall b ofs sz sg, + is_true (Vptr b ofs) (Tint sz sg) + | is_true_int_pointer: forall n t, + n <> Int.zero -> + is_true (Vint n) (Tpointer t) + | is_true_pointer_pointer: forall b ofs t, + is_true (Vptr b ofs) (Tpointer t) + | is_true_float: forall f sz, + f <> Float.zero -> + is_true (Vfloat f) (Tfloat sz). + +Inductive bool_of_val : val -> type -> val -> Prop := + | bool_of_val_true: forall v ty, + is_true v ty -> + bool_of_val v ty Vtrue + | bool_of_val_false: forall v ty, + is_false v ty -> + bool_of_val v ty Vfalse. + +Function sem_neg (v: val) (ty: type) : option val := + match ty with + | Tint _ _ => + match v with + | Vint n => Some (Vint (Int.neg n)) + | _ => None + end + | Tfloat _ => + match v with + | Vfloat f => Some (Vfloat (Float.neg f)) + | _ => None + end + | _ => None + end. + +Function sem_notint (v: val) : option val := + match v with + | Vint n => Some (Vint (Int.xor n Int.mone)) + | _ => None + end. + +Function sem_notbool (v: val) (ty: type) : option val := + match ty with + | Tint _ _ => + match v with + | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) + | Vptr _ _ => Some Vfalse + | _ => None + end + | Tpointer _ => + match v with + | Vint n => Some (Val.of_bool (Int.eq n Int.zero)) + | Vptr _ _ => Some Vfalse + | _ => None + end + | Tfloat _ => + match v with + | Vfloat f => Some (Val.of_bool (Float.cmp Ceq f Float.zero)) + | _ => None + end + | _ => None + end. + +Function sem_add (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_add t1 t2 with + | add_case_ii => + match v1, v2 with + | Vint n1, Vint n2 => Some (Vint (Int.add n1 n2)) + | _, _ => None + end + | add_case_ff => + match v1, v2 with + | Vfloat n1, Vfloat n2 => Some (Vfloat (Float.add n1 n2)) + | _, _ => None + end + | add_case_pi ty=> + match v1,v2 with + | Vptr b1 ofs1, Vint n2 => + Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) + | _, _ => None + end + | add_default => None +end. + +Function sem_sub (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_sub t1 t2 with + | sub_case_ii => (* integer subtraction *) + match v1,v2 with + | Vint n1, Vint n2 => Some (Vint (Int.sub n1 n2)) + | _, _ => None + end + | sub_case_ff => (* float subtraction *) + match v1,v2 with + | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.sub f1 f2)) + | _, _ => None + end + | sub_case_pi ty => (*array| pointer - offset *) + match v1,v2 with + | Vptr b1 ofs1, Vint n2 => + Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof ty)) n2))) + | _, _ => None + end + | sub_case_pp ty => (* array|pointer - array|pointer *) + match v1,v2 with + | Vptr b1 ofs1, Vptr b2 ofs2 => + if zeq b1 b2 then + if Int.eq (Int.repr (sizeof ty)) Int.zero then None + else Some (Vint (Int.divu (Int.sub ofs1 ofs2) (Int.repr (sizeof ty)))) + else None + | _, _ => None + end + | sub_default => None + end. + +Function sem_mul (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_mul t1 t2 with + | mul_case_ii => + match v1,v2 with + | Vint n1, Vint n2 => Some (Vint (Int.mul n1 n2)) + | _, _ => None + end + | mul_case_ff => + match v1,v2 with + | Vfloat f1, Vfloat f2 => Some (Vfloat (Float.mul f1 f2)) + | _, _ => None + end + | mul_default => + None +end. + +Function sem_div (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_div t1 t2 with + | div_case_I32unsi => + match v1,v2 with + | Vint n1, Vint n2 => + if Int.eq n2 Int.zero then None else Some (Vint (Int.divu n1 n2)) + | _,_ => None + end + | div_case_ii => + match v1,v2 with + | Vint n1, Vint n2 => + if Int.eq n2 Int.zero then None else Some (Vint(Int.divs n1 n2)) + | _,_ => None + end + | div_case_ff => + match v1,v2 with + | Vfloat f1, Vfloat f2 => Some (Vfloat(Float.div f1 f2)) + | _, _ => None + end + | div_default => + None +end. + +Function sem_mod (v1:val) (t1:type) (v2: val) (t2:type) : option val := + match classify_mod t1 t2 with + | mod_case_I32unsi => + match v1, v2 with + | Vint n1, Vint n2 => + if Int.eq n2 Int.zero then None else Some (Vint (Int.modu n1 n2)) + | _, _ => None + end + | mod_case_ii => + match v1,v2 with + | Vint n1, Vint n2 => + if Int.eq n2 Int.zero then None else Some (Vint (Int.mods n1 n2)) + | _, _ => None + end + | mod_default => + None + end. + +Function sem_and (v1 v2: val) : option val := + match v1, v2 with + | Vint n1, Vint n2 => Some (Vint(Int.and n1 n2)) + | _, _ => None + end . + +Function sem_or (v1 v2: val) : option val := + match v1, v2 with + | Vint n1, Vint n2 => Some (Vint(Int.or n1 n2)) + | _, _ => None + end. + +Function sem_xor (v1 v2: val): option val := + match v1, v2 with + | Vint n1, Vint n2 => Some (Vint(Int.xor n1 n2)) + | _, _ => None + end. + +Function sem_shl (v1 v2: val): option val := + match v1, v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 (Int.repr 32) then Some (Vint(Int.shl n1 n2)) else None + | _, _ => None + end. + +Function sem_shr (v1: val) (t1: type) (v2: val) (t2: type): option val := + match classify_shr t1 t2 with + | shr_case_I32unsi => + match v1,v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shru n1 n2)) else None + | _,_ => None + end + | shr_case_ii => + match v1,v2 with + | Vint n1, Vint n2 => + if Int.ltu n2 (Int.repr 32) then Some (Vint (Int.shr n1 n2)) else None + | _, _ => None + end + | shr_default=> + None + end. + +Function sem_cmp_mismatch (c: comparison): option val := + match c with + | Ceq => Some Vfalse + | Cne => Some Vtrue + | _ => None + end. + +Function sem_cmp (c:comparison) + (v1: val) (t1: type) (v2: val) (t2: type) + (m: mem): option val := + match classify_cmp t1 t2 with + | cmp_case_I32unsi => + match v1,v2 with + | Vint n1, Vint n2 =>Some (Val.of_bool (Int.cmpu c n1 n2)) + | _, _ => None + end + | cmp_case_ii => + match v1,v2 with + | Vint n1, Vint n2 =>Some (Val.of_bool (Int.cmp c n1 n2)) + | _, _ => None + end + | cmp_case_ff => + match v1,v2 with + | Vfloat f1, Vfloat f2 =>Some (Val.of_bool (Float.cmp c f1 f2)) + | _, _ => None + end + | cmp_case_pi => + match v1,v2 with + | Vptr b ofs, Vint n2 => + if Int.eq n2 Int.zero then sem_cmp_mismatch c else None + | _, _ => None + end + | cmp_case_pp => + match v1,v2 with + | Vptr b1 ofs1, Vptr b2 ofs2 => + if valid_pointer m b1 (Int.signed ofs1) && valid_pointer m b2 (Int.signed ofs2) then + if zeq b1 b2 + then Some (Val.of_bool (Int.cmp c ofs1 ofs2)) + else None + else None + | _, _ => None + end + | cmp_default => None + end. + +Definition sem_unary_operation + (op: unary_operation) (v: val) (ty: type): option val := + match op with + | Onotbool => sem_notbool v ty + | Onotint => sem_notint v + | Oneg => sem_neg v ty + end. + +Definition sem_binary_operation + (op: binary_operation) + (v1: val) (t1: type) (v2: val) (t2:type) + (m: mem): option val := + match op with + | Oadd => sem_add v1 t1 v2 t2 + | Osub => sem_sub v1 t1 v2 t2 + | Omul => sem_mul v1 t1 v2 t2 + | Omod => sem_mod v1 t1 v2 t2 + | Odiv => sem_div v1 t1 v2 t2 + | Oand => sem_and v1 v2 + | Oor => sem_or v1 v2 + | Oxor => sem_xor v1 v2 + | Oshl => sem_shl v1 v2 + | Oshr => sem_shr v1 t1 v2 t2 + | Oeq => sem_cmp Ceq v1 t1 v2 t2 m + | One => sem_cmp Cne v1 t1 v2 t2 m + | Olt => sem_cmp Clt v1 t1 v2 t2 m + | Ogt => sem_cmp Cgt v1 t1 v2 t2 m + | Ole => sem_cmp Cle v1 t1 v2 t2 m + | Oge => sem_cmp Cge v1 t1 v2 t2 m + end. + +Definition cast_int_int (sz: intsize) (sg: signedness) (i: int) : int := + match sz, sg with + | I8, Signed => Int.cast8signed i + | I8, Unsigned => Int.cast8unsigned i + | I16, Signed => Int.cast16signed i + | I16, Unsigned => Int.cast16unsigned i + | I32 , _ => i + end. + +Definition cast_int_float (si : signedness) (i: int) : float := + match si with + | Signed => Float.floatofint i + | Unsigned => Float.floatofintu i + end. + +Definition cast_float_float (sz: floatsize) (f: float) : float := + match sz with + | F32 => Float.singleoffloat f + | F64 => f + end. + +Inductive cast : val -> type -> type -> val -> Prop := + | cast_ii: forall i sz2 sz1 si1 si2, + cast (Vint i) (Tint sz1 si1) (Tint sz2 si2) + (Vint (cast_int_int sz2 si2 i)) + | cast_fi: forall f sz1 sz2 si2, + cast (Vfloat f) (Tfloat sz1) (Tint sz2 si2) + (Vint (cast_int_int sz2 si2 (Float.intoffloat f))) + | cast_if: forall i sz1 sz2 si1, + cast (Vint i) (Tint sz1 si1) (Tfloat sz2) + (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) + | cast_ff: forall f sz1 sz2, + cast (Vfloat f) (Tfloat sz1) (Tfloat sz2) + (Vfloat (cast_float_float sz2 f)) + | cast_ip_p: forall b ofs t1 si2, + cast (Vptr b ofs) (Tint I32 si2) (Tpointer t1) (Vptr b ofs) + | cast_pi_p: forall b ofs t1 si2, + cast (Vptr b ofs) (Tpointer t1) (Tint I32 si2) (Vptr b ofs) + | cast_pp_p: forall b ofs t1 t2, + cast (Vptr b ofs) (Tpointer t1) (Tpointer t2) (Vptr b ofs) + | cast_ip_i: forall n t1 si2, + cast (Vint n) (Tint I32 si2) (Tpointer t1) (Vint n) + | cast_pi_i: forall n t1 si2, + cast (Vint n) (Tpointer t1) (Tint I32 si2) (Vint n) + | cast_pp_i: forall n t1 t2, + cast (Vint n) (Tpointer t1) (Tpointer t2) (Vint n). + +(** ** Operational semantics *) + +(** Global environment *) + +Definition genv := Genv.t fundef. + +Definition globalenv (p: program) : genv := + Genv.globalenv (program_of_program p). + +Definition init_mem (p: program) : mem := + Genv.init_mem (program_of_program p). + +(** Local environment *) + +Definition env := PTree.t block. (* map variable -> location *) + +Definition empty_env: env := (PTree.empty block). + +(** Outcomes for statements *) + +Inductive outcome: Set := + | Out_break: outcome + | Out_continue: outcome + | Out_normal: outcome + | Out_return: option val -> outcome. + +Inductive out_normal_or_continue : outcome -> Prop := + | Out_normal_or_continue_N: out_normal_or_continue Out_normal + | Out_normal_or_continue_C: out_normal_or_continue Out_continue. + +Inductive out_break_or_return : outcome -> outcome -> Prop := + | Out_break_or_return_B: out_break_or_return Out_break Out_normal + | Out_break_or_return_R: forall ov, + out_break_or_return (Out_return ov) (Out_return ov). + +Definition outcome_switch (out: outcome) : outcome := + match out with + | Out_break => Out_normal + | o => o + end. + +Definition outcome_result_value (out: outcome) (t: type) (v: val) : Prop := + match out, t with + | Out_normal, Tvoid => v = Vundef + | Out_return None, Tvoid => v = Vundef + | Out_return (Some v'), ty => ty <> Tvoid /\ v'=v + | _, _ => False + end. + +(** Selection of the appropriate case of a [switch] *) + +Fixpoint select_switch (n: int) (sl: labeled_statements) + {struct sl}: labeled_statements := + match sl with + | LSdefault _ => sl + | LScase c s sl' => if Int.eq c n then sl else select_switch n sl' + end. + +(** Loads and stores by type *) + +Definition load_value_of_type (ty: type) (m: mem) (b: block) (ofs: int) : option val := + match access_mode ty with + | By_value chunk => Mem.loadv chunk m (Vptr b ofs) + | By_reference => Some (Vptr b ofs) + | By_nothing => None + end. + +Definition store_value_of_type (ty_dest: type) (m: mem) (loc: block) (ofs: int) (v: val) : option mem := + match access_mode ty_dest with + | By_value chunk => Mem.storev chunk m (Vptr loc ofs) v + | By_reference => None + | By_nothing => None + end. + +(** Allocation and initialization of function-local variables *) + +Inductive alloc_variables: env -> mem -> + list (ident * type) -> + 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 ty vars m1 b1 m2 e2 lb, + Mem.alloc m 0 (sizeof ty) = (m1, b1) -> + alloc_variables (PTree.set id b1 e) m1 vars e2 m2 lb -> + alloc_variables e m ((id, ty) :: vars) e2 m2 (b1 :: lb). + +Inductive bind_parameters: env -> + mem -> list (ident * type) -> list val -> + mem -> Prop := + | bind_parameters_nil: + forall e m, + bind_parameters e m nil nil m + | bind_parameters_cons: + forall e m id ty params v1 vl b m1 m2, + PTree.get id e = Some b -> + store_value_of_type ty m b Int.zero v1 = Some m1 -> + bind_parameters e m1 params vl m2 -> + bind_parameters e m ((id, ty) :: params) (v1 :: vl) m2. + +Section RELSEM. + +Variable ge: genv. + +(** Evaluation of an expression in r-value position *) + +Inductive eval_expr: env -> mem -> expr -> trace -> mem -> val -> Prop := + | eval_Econst_int: forall e m i ty, + eval_expr e m (Expr (Econst_int i) ty) + E0 m (Vint i) + | eval_Econst_float: forall e m f ty, + eval_expr e m (Expr (Econst_float f) ty) + E0 m (Vfloat f) + | eval_Elvalue: forall e m a ty t m1 loc ofs v, + eval_lvalue e m (Expr a ty) t m1 loc ofs -> + load_value_of_type ty m1 loc ofs = Some v -> + eval_expr e m (Expr a ty) + t m1 v + | eval_Eaddrof: forall e m a t m1 loc ofs ty, + eval_lvalue e m a t m1 loc ofs -> + eval_expr e m (Expr (Eaddrof a) ty) + t m1 (Vptr loc ofs) + | eval_Esizeof: forall e m ty' ty, + eval_expr e m (Expr (Esizeof ty') ty) + E0 m (Vint (Int.repr (sizeof ty'))) + | eval_Eunop: forall e m op a ty t m1 v1 v, + eval_expr e m a t m1 v1 -> + sem_unary_operation op v1 (typeof a) = Some v -> + eval_expr e m (Expr (Eunop op a) ty) + t m1 v + | eval_Ebinop: forall e m op a1 a2 ty t1 m1 v1 t2 m2 v2 v, + eval_expr e m a1 t1 m1 v1 -> + eval_expr e m1 a2 t2 m2 v2 -> + sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m2 = Some v -> + eval_expr e m (Expr (Ebinop op a1 a2) ty) + (t1 ** t2) m2 v + | eval_Eorbool_1: forall e m a1 a2 t m1 v1 ty, + eval_expr e m a1 t m1 v1 -> + is_true v1 (typeof a1) -> + eval_expr e m (Expr (Eorbool a1 a2) ty) + t m1 Vtrue + | eval_Eorbool_2: forall e m a1 a2 ty t1 m1 v1 t2 m2 v2 v, + eval_expr e m a1 t1 m1 v1 -> + is_false v1 (typeof a1) -> + eval_expr e m1 a2 t2 m2 v2 -> + bool_of_val v2 (typeof a2) v -> + eval_expr e m (Expr (Eorbool a1 a2) ty) + (t1 ** t2) m2 v + | eval_Eandbool_1: forall e m a1 a2 t m1 v1 ty, + eval_expr e m a1 t m1 v1 -> + is_false v1 (typeof a1) -> + eval_expr e m (Expr (Eandbool a1 a2) ty) + t m1 Vfalse + | eval_Eandbool_2: forall e m a1 a2 ty t1 m1 v1 t2 m2 v2 v, + eval_expr e m a1 t1 m1 v1 -> + is_true v1 (typeof a1) -> + eval_expr e m1 a2 t2 m2 v2 -> + bool_of_val v2 (typeof a2) v -> + eval_expr e m (Expr (Eandbool a1 a2) ty) + (t1 ** t2) m2 v + | eval_Ecast: forall e m a ty t m1 v1 v, + eval_expr e m a t m1 v1 -> + cast v1 (typeof a) ty v -> + eval_expr e m (Expr (Ecast ty a) ty) + t m1 v + | eval_Ecall: forall e m a bl ty m3 vres t1 m1 vf t2 m2 vargs f t3, + eval_expr e m a t1 m1 vf -> + eval_exprlist e m1 bl t2 m2 vargs -> + Genv.find_funct ge vf = Some f -> + type_of_fundef f = typeof a -> + eval_funcall m2 f vargs t3 m3 vres -> + eval_expr e m (Expr (Ecall a bl) ty) + (t1 ** t2 ** t3) m3 vres + +(** Evaluation of an expression in l-value position *) + +with eval_lvalue: env -> mem -> expr -> trace -> mem -> block -> int -> Prop := + | eval_Evar_local: forall e m id l ty, + e!id = Some l -> + eval_lvalue e m (Expr (Evar id) ty) + E0 m l Int.zero + | eval_Evar_global: forall e m id l ty, + e!id = None -> + Genv.find_symbol ge id = Some l -> + eval_lvalue e m (Expr (Evar id) ty) + E0 m l Int.zero + | eval_Ederef: forall e m m1 a t ofs ty l, + eval_expr e m a t m1 (Vptr l ofs) -> + eval_lvalue e m (Expr (Ederef a) ty) + t m1 l ofs + | eval_Eindex: forall e m a1 t1 m1 v1 a2 t2 m2 v2 l ofs ty, + eval_expr e m a1 t1 m1 v1 -> + eval_expr e m1 a2 t2 m2 v2 -> + sem_add v1 (typeof a1) v2 (typeof a2) = Some (Vptr l ofs) -> + eval_lvalue e m (Expr (Eindex a1 a2) ty) + (t1 ** t2) m2 l ofs + | eval_Efield_struct: forall e m a t m1 l ofs fList i ty delta, + eval_lvalue e m a t m1 l ofs -> + typeof a = Tstruct fList -> + field_offset i fList = Some delta -> + eval_lvalue e m (Expr (Efield a i) ty) + t m1 l (Int.add ofs (Int.repr delta)) + | eval_Efield_union: forall e m a t m1 l ofs fList i ty, + eval_lvalue e m a t m1 l ofs -> + typeof a = Tunion fList -> + eval_lvalue e m (Expr (Efield a i) ty) + t m1 l ofs + +(** Evaluation of a list of expressions *) + +with eval_exprlist: env -> mem -> exprlist -> trace -> mem -> list val -> Prop := + | eval_Enil: forall e m, + eval_exprlist e m Enil E0 m nil + | eval_Econs: forall e m a bl t1 m1 v t2 m2 vl, + eval_expr e m a t1 m1 v -> + eval_exprlist e m1 bl t2 m2 vl -> + eval_exprlist e m (Econs a bl) + (t1 ** t2) m2 (v :: vl) + +(** Execution of a statement *) + +with exec_stmt: env -> mem -> statement -> 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 e m a t m1 v -> + exec_stmt e m (Sexpr a) + t m1 Out_normal + | exec_Sassign: forall e m a1 a2 t1 m1 loc ofs t2 m2 v2 m3, + eval_lvalue e m a1 t1 m1 loc ofs -> + eval_expr e m1 a2 t2 m2 v2 -> + store_value_of_type (typeof a1) m2 loc ofs v2 = Some m3 -> + exec_stmt e m (Sassign a1 a2) + (t1 ** t2) m3 Out_normal + | exec_Sseq_1: forall e m s1 s2 t1 m1 t2 m2 out, + exec_stmt e m s1 t1 m1 Out_normal -> + exec_stmt e m1 s2 t2 m2 out -> + exec_stmt e m (Ssequence s1 s2) + (t1 ** t2) m2 out + | exec_Sseq_2: forall e m s1 s2 t1 m1 out, + exec_stmt e m s1 t1 m1 out -> + out <> Out_normal -> + exec_stmt e m (Ssequence s1 s2) + t1 m1 out + | exec_Sifthenelse_true: forall e m a s1 s2 t1 m1 v1 t2 m2 out, + eval_expr e m a t1 m1 v1 -> + is_true v1 (typeof a) -> + exec_stmt e m1 s1 t2 m2 out -> + exec_stmt e m (Sifthenelse a s1 s2) + (t1 ** t2) m2 out + | exec_Sifthenelse_false: forall e m a s1 s2 t1 m1 v1 t2 m2 out, + eval_expr e m a t1 m1 v1 -> + is_false v1 (typeof a) -> + exec_stmt e m1 s2 t2 m2 out -> + exec_stmt e m (Sifthenelse a s1 s2) + (t1 ** t2) m2 out + | exec_Sreturn_none: forall e m, + exec_stmt e m (Sreturn None) + E0 m (Out_return None) + | exec_Sreturn_some: forall e m a t m1 v, + eval_expr e m a t m1 v -> + exec_stmt e m (Sreturn (Some a)) + t m1 (Out_return (Some v)) + | exec_Sbreak: forall e m, + exec_stmt e m Sbreak + E0 m Out_break + | exec_Scontinue: forall e m, + exec_stmt e m Scontinue + E0 m Out_continue + | exec_Swhile_false: forall e m s a t v m1, + eval_expr e m a t m1 v -> + is_false v (typeof a) -> + exec_stmt e m (Swhile a s) + t m1 Out_normal + | exec_Swhile_stop: forall e m a t1 m1 v s m2 t2 out2 out, + eval_expr e m a t1 m1 v -> + is_true v (typeof a) -> + exec_stmt e m1 s t2 m2 out2 -> + out_break_or_return out2 out -> + exec_stmt e m (Swhile a s) + (t1 ** t2) m2 out + | exec_Swhile_loop: forall e m a t1 m1 v s out2 out t2 m2 t3 m3, + eval_expr e m a t1 m1 v -> + is_true v (typeof a) -> + exec_stmt e m1 s t2 m2 out2 -> + out_normal_or_continue out2 -> + exec_stmt e m2 (Swhile a s) t3 m3 out -> + exec_stmt e m (Swhile a s) + (t1 ** t2 ** t3) m3 out + | exec_Sdowhile_false: forall e m s a t1 m1 out1 v t2 m2, + exec_stmt e m s t1 m1 out1 -> + out_normal_or_continue out1 -> + eval_expr e m1 a t2 m2 v -> + is_false v (typeof a) -> + exec_stmt e m (Sdowhile a s) + (t1 ** t2) m2 Out_normal + | exec_Sdowhile_stop: forall e m s a t m1 out1 out, + exec_stmt e m s t m1 out1 -> + out_break_or_return out1 out -> + exec_stmt e m (Sdowhile a s) + t m1 out + | exec_Sdowhile_loop: forall e m s a m1 m2 m3 t1 t2 t3 out out1 v, + exec_stmt e m s t1 m1 out1 -> + out_normal_or_continue out1 -> + eval_expr e m1 a t2 m2 v -> + is_true v (typeof a) -> + exec_stmt e m2 (Sdowhile a s) t3 m3 out -> + exec_stmt e m (Sdowhile a s) + (t1 ** t2 ** t3) m3 out + | exec_Sfor_start: forall e m s a1 a2 a3 out m1 m2 t1 t2, + exec_stmt e m a1 t1 m1 Out_normal -> + exec_stmt e m1 (Sfor Sskip a2 a3 s) t2 m2 out -> + exec_stmt e m (Sfor a1 a2 a3 s) + (t1 ** t2) m2 out + | exec_Sfor_false: forall e m s a2 a3 t v m1, + eval_expr e m a2 t m1 v -> + is_false v (typeof a2) -> + exec_stmt e m (Sfor Sskip a2 a3 s) + t m1 Out_normal + | exec_Sfor_stop: forall e m s a2 a3 v m1 m2 t1 t2 out2 out, + eval_expr e m a2 t1 m1 v -> + is_true v (typeof a2) -> + exec_stmt e m1 s t2 m2 out2 -> + out_break_or_return out2 out -> + exec_stmt e m (Sfor Sskip a2 a3 s) + (t1 ** t2) m2 out + | exec_Sfor_loop: forall e m s a2 a3 v m1 m2 m3 m4 t1 t2 t3 t4 out2 out, + eval_expr e m a2 t1 m1 v -> + is_true v (typeof a2) -> + exec_stmt e m1 s t2 m2 out2 -> + out_normal_or_continue out2 -> + exec_stmt e m2 a3 t3 m3 Out_normal -> + exec_stmt e m3 (Sfor Sskip a2 a3 s) t4 m4 out -> + exec_stmt e m (Sfor Sskip a2 a3 s) + (t1 ** t2 ** t3 ** t4) m4 out + | exec_Sswitch: forall e m a t1 m1 n sl t2 m2 out, + eval_expr e m a t1 m1 (Vint n) -> + exec_lblstmts e m1 (select_switch n sl) t2 m2 out -> + exec_stmt e m (Sswitch a sl) + (t1 ** t2) m2 (outcome_switch out) + +(** Execution of a list of labeled statements *) + +with exec_lblstmts: env -> mem -> labeled_statements -> trace -> mem -> outcome -> Prop := + | exec_LSdefault: forall e m s t m1 out, + exec_stmt e m s t m1 out -> + exec_lblstmts e m (LSdefault s) t m1 out + | exec_LScase_fallthrough: forall e m n s ls t1 m1 t2 m2 out, + exec_stmt e m s t1 m1 Out_normal -> + exec_lblstmts e m1 ls t2 m2 out -> + exec_lblstmts e m (LScase n s ls) (t1 ** t2) m2 out + | exec_LScase_stop: forall e m n s ls t m1 out, + exec_stmt e m s t m1 out -> out <> Out_normal -> + exec_lblstmts e m (LScase n s ls) t m1 out + +(** Evaluation of a function invocation *) + +with eval_funcall: mem -> fundef -> list val -> trace -> mem -> val -> Prop := + | eval_funcall_internal: forall m f vargs t e m1 lb m2 m3 out vres, + alloc_variables empty_env m (f.(fn_params) ++ f.(fn_vars)) 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_return) vres -> + eval_funcall m (Internal f) vargs t (Mem.free_list m3 lb) vres + | eval_funcall_external: forall m id targs tres vargs t vres, + event_match (external_function id targs tres) vargs t vres -> + eval_funcall m (External id targs tres) vargs t m vres. + +Scheme eval_expr_ind6 := Minimality for eval_expr Sort Prop + with eval_lvalue_ind6 := Minimality for eval_lvalue Sort Prop + with eval_exprlist_ind6 := Minimality for eval_exprlist Sort Prop + with exec_stmt_ind6 := Minimality for exec_stmt Sort Prop + with exec_lblstmts_ind6 := Minimality for exec_lblstmts Sort Prop + with eval_funcall_ind6 := Minimality for eval_funcall Sort Prop. + +End RELSEM. + +(** Execution of a whole program *) + +Definition exec_program (p: program) (t: trace) (r: val) : Prop := + let ge := globalenv p in + let m0 := init_mem p in + exists b, exists f, exists m1, + Genv.find_symbol ge p.(prog_main) = Some b /\ + Genv.find_funct_ptr ge b = Some f /\ + type_of_fundef f = Tfunction Tnil (Tint I32 Signed) /\ + eval_funcall ge m0 f nil t m1 r. -- cgit v1.2.3