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 --- backend/Linear.v | 97 +++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 61 insertions(+), 36 deletions(-) (limited to 'backend/Linear.v') diff --git a/backend/Linear.v b/backend/Linear.v index f4ed0454..2520f5bf 100644 --- a/backend/Linear.v +++ b/backend/Linear.v @@ -11,6 +11,7 @@ Require Import AST. Require Import Integers. Require Import Values. Require Import Mem. +Require Import Events. Require Import Globalenvs. Require Import Op. Require Import Locations. @@ -37,6 +38,7 @@ Inductive instruction: Set := | Lload: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Lstore: memory_chunk -> addressing -> list mreg -> mreg -> instruction | Lcall: signature -> mreg + ident -> instruction + | Lalloc: instruction | Llabel: label -> instruction | Lgoto: label -> instruction | Lcond: condition -> list mreg -> label -> instruction @@ -50,9 +52,17 @@ Record function: Set := mkfunction { fn_code: code }. -Definition program := AST.program function. +Definition fundef := AST.fundef function. -Definition genv := Genv.t function. +Definition program := AST.program fundef. + +Definition funsig (fd: fundef) := + match fd with + | Internal f => f.(fn_sig) + | External ef => ef.(ef_sig) + end. + +Definition genv := Genv.t fundef. Definition locset := Locmap.t. (** * Operational semantics *) @@ -88,7 +98,7 @@ Section RELSEM. Variable ge: genv. -Definition find_function (ros: mreg + ident) (rs: locset) : option function := +Definition find_function (ros: mreg + ident) (rs: locset) : option fundef := match ros with | inl r => Genv.find_funct ge (rs (R r)) | inr symb => @@ -106,84 +116,99 @@ Definition find_function (ros: mreg + ident) (rs: locset) : option function := [ls'] and [m'] are the final location state and memory state. *) Inductive exec_instr: function -> val -> - code -> locset -> mem -> + code -> locset -> mem -> trace -> code -> locset -> mem -> Prop := | exec_Lgetstack: forall f sp sl r b rs m, exec_instr f sp (Lgetstack sl r :: b) rs m - b (Locmap.set (R r) (rs (S sl)) rs) m + E0 b (Locmap.set (R r) (rs (S sl)) rs) m | exec_Lsetstack: forall f sp r sl b rs m, exec_instr f sp (Lsetstack r sl :: b) rs m - b (Locmap.set (S sl) (rs (R r)) rs) m + E0 b (Locmap.set (S sl) (rs (R r)) rs) m | exec_Lop: forall f sp op args res b rs m v, eval_operation ge sp op (reglist args rs) = Some v -> exec_instr f sp (Lop op args res :: b) rs m - b (Locmap.set (R res) v rs) m + E0 b (Locmap.set (R res) v rs) m | exec_Lload: forall f sp chunk addr args dst b rs m a v, eval_addressing ge sp addr (reglist args rs) = Some a -> loadv chunk m a = Some v -> exec_instr f sp (Lload chunk addr args dst :: b) rs m - b (Locmap.set (R dst) v rs) m + E0 b (Locmap.set (R dst) v rs) m | exec_Lstore: forall f sp chunk addr args src b rs m m' a, eval_addressing ge sp addr (reglist args rs) = Some a -> storev chunk m a (rs (R src)) = Some m' -> exec_instr f sp (Lstore chunk addr args src :: b) rs m - b rs m' + E0 b rs m' | exec_Lcall: - forall f sp sig ros b rs m f' rs' m', + forall f sp sig ros b rs m t f' rs' m', find_function ros rs = Some f' -> - sig = f'.(fn_sig) -> - exec_function f' rs m rs' m' -> + sig = funsig f' -> + exec_function f' rs m t rs' m' -> exec_instr f sp (Lcall sig ros :: b) rs m - b (return_regs rs rs') m' + t b (return_regs rs rs') m' + | exec_Lalloc: + forall f sp b rs m sz m' blk, + rs (R Conventions.loc_alloc_argument) = Vint sz -> + Mem.alloc m 0 (Int.signed sz) = (m', blk) -> + exec_instr f sp (Lalloc :: b) rs m + E0 b (Locmap.set (R Conventions.loc_alloc_result) + (Vptr blk Int.zero) rs) m' | exec_Llabel: forall f sp lbl b rs m, exec_instr f sp (Llabel lbl :: b) rs m - b rs m + E0 b rs m | exec_Lgoto: forall f sp lbl b rs m b', find_label lbl f.(fn_code) = Some b' -> exec_instr f sp (Lgoto lbl :: b) rs m - b' rs m + E0 b' rs m | exec_Lcond_true: forall f sp cond args lbl b rs m b', eval_condition cond (reglist args rs) = Some true -> find_label lbl f.(fn_code) = Some b' -> exec_instr f sp (Lcond cond args lbl :: b) rs m - b' rs m + E0 b' rs m | exec_Lcond_false: forall f sp cond args lbl b rs m, eval_condition cond (reglist args rs) = Some false -> exec_instr f sp (Lcond cond args lbl :: b) rs m - b rs m + E0 b rs m with exec_instrs: function -> val -> - code -> locset -> mem -> + code -> locset -> mem -> trace -> code -> locset -> mem -> Prop := | exec_refl: forall f sp b rs m, - exec_instrs f sp b rs m b rs m + exec_instrs f sp b rs m E0 b rs m | exec_one: - forall f sp b1 rs1 m1 b2 rs2 m2, - exec_instr f sp b1 rs1 m1 b2 rs2 m2 -> - exec_instrs f sp b1 rs1 m1 b2 rs2 m2 + forall f sp b1 rs1 m1 t b2 rs2 m2, + exec_instr f sp b1 rs1 m1 t b2 rs2 m2 -> + exec_instrs f sp b1 rs1 m1 t b2 rs2 m2 | exec_trans: - forall f sp b1 rs1 m1 b2 rs2 m2 b3 rs3 m3, - exec_instrs f sp b1 rs1 m1 b2 rs2 m2 -> - exec_instrs f sp b2 rs2 m2 b3 rs3 m3 -> - exec_instrs f sp b1 rs1 m1 b3 rs3 m3 - -with exec_function: function -> locset -> mem -> locset -> mem -> Prop := - | exec_funct: - forall f rs m m1 stk rs2 m2 b, + forall f sp b1 rs1 m1 t1 b2 rs2 m2 t2 b3 rs3 m3 t, + exec_instrs f sp b1 rs1 m1 t1 b2 rs2 m2 -> + exec_instrs f sp b2 rs2 m2 t2 b3 rs3 m3 -> + t = t1 ** t2 -> + exec_instrs f sp b1 rs1 m1 t b3 rs3 m3 + +with exec_function: fundef -> locset -> mem -> trace -> locset -> mem -> Prop := + | exec_funct_internal: + forall f rs m t m1 stk rs2 m2 b, alloc m 0 f.(fn_stacksize) = (m1, stk) -> exec_instrs f (Vptr stk Int.zero) - f.(fn_code) (call_regs rs) m1 (Lreturn :: b) rs2 m2 -> - exec_function f rs m rs2 (free m2 stk). + f.(fn_code) (call_regs rs) m1 + t (Lreturn :: b) rs2 m2 -> + exec_function (Internal f) rs m t rs2 (free m2 stk) + | exec_funct_external: + forall ef args res rs1 rs2 m t, + event_match ef args t res -> + args = List.map rs1 (Conventions.loc_arguments ef.(ef_sig)) -> + rs2 = Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs1 -> + exec_function (External ef) rs1 m t rs2 m. Scheme exec_instr_ind3 := Minimality for exec_instr Sort Prop with exec_instrs_ind3 := Minimality for exec_instrs Sort Prop @@ -191,13 +216,13 @@ Scheme exec_instr_ind3 := Minimality for exec_instr Sort Prop End RELSEM. -Definition exec_program (p: program) (r: val) : Prop := +Definition exec_program (p: program) (t: trace) (r: val) : Prop := let ge := Genv.globalenv p in let m0 := Genv.init_mem p in exists b, exists f, exists rs, exists m, Genv.find_symbol ge p.(prog_main) = Some b /\ Genv.find_funct_ptr ge b = Some f /\ - f.(fn_sig) = mksignature nil (Some Tint) /\ - exec_function ge f (Locmap.init Vundef) m0 rs m /\ - rs (R (Conventions.loc_result f.(fn_sig))) = r. + funsig f = mksignature nil (Some Tint) /\ + exec_function ge f (Locmap.init Vundef) m0 t rs m /\ + rs (R (Conventions.loc_result (funsig f))) = r. -- cgit