From b5325808cb1d36d4ff500d2fb754fe7a424e8329 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 25 Jul 2008 16:24:06 +0000 Subject: Simplification de la semantique de LTL et LTLin. Les details lies aux conventions d'appel sont maintenant geres de maniere plus locale dans la passe Reload. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@701 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/LTL.v | 144 ++++++++++++++++++++-------------------------------------- 1 file changed, 48 insertions(+), 96 deletions(-) (limited to 'backend/LTL.v') diff --git a/backend/LTL.v b/backend/LTL.v index a082e122..e39a4ecf 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -72,53 +72,20 @@ Definition funsig (fd: fundef) := Definition genv := Genv.t fundef. Definition locset := Locmap.t. -Section RELSEM. - -(** Calling conventions are reflected at the level of location sets - (environments mapping locations to values) by the following two - functions. +Definition locmap_optget (ol: option loc) (dfl: val) (ls: locset) : val := + match ol with + | None => dfl + | Some l => ls l + end. - [call_regs caller] returns the location set at function entry, - as a function of the location set [caller] of the calling function. -- Machine registers have the same values as in the caller. -- Incoming stack slots (used for parameter passing) have the same - values as the corresponding outgoing stack slots (used for argument - passing) in the caller. -- Local and outgoing stack slots are initialized to undefined values. -*) +Fixpoint init_locs (vl: list val) (rl: list loc) {struct rl} : locset := + match rl, vl with + | r1 :: rs, v1 :: vs => Locmap.set r1 v1 (init_locs vs rs) + | _, _ => Locmap.init Vundef + end. -Definition call_regs (caller: locset) : locset := - fun (l: loc) => - match l with - | R r => caller (R r) - | S (Local ofs ty) => Vundef - | S (Incoming ofs ty) => caller (S (Outgoing ofs ty)) - | S (Outgoing ofs ty) => Vundef - end. -(** [return_regs caller callee] returns the location set after - a call instruction, as a function of the location set [caller] - of the caller before the call instruction and of the location - set [callee] of the callee at the return instruction. -- Callee-save machine registers have the same values as in the caller - before the call. -- Caller-save machine registers have the same values - as in the callee at the return point. -- Stack slots have the same values as in the caller before the call. -*) - -Definition return_regs (caller callee: locset) : locset := - fun (l: loc) => - match l with - | R r => - if In_dec Loc.eq (R r) Conventions.temporaries then - callee (R r) - else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then - callee (R r) - else - caller (R r) - | S s => caller (S s) - end. +Section RELSEM. (** [parmov srcs dsts ls] performs the parallel assignment of locations [dsts] to the values of the corresponding locations @@ -130,18 +97,29 @@ Fixpoint parmov (srcs dsts: list loc) (ls: locset) {struct srcs} : locset := | _, _ => ls end. -Definition set_result_reg (s: signature) (or: option loc) (ls: locset) := - match or with - | Some r => Locmap.set (R (loc_result s)) (ls r) ls - | None => ls - end. +(** [postcall_regs ls] returns the location set [ls] after a function + call. Caller-save registers and temporary registers + are set to [undef], reflecting the fact that the called + function can modify them freely. *) + +Definition postcall_regs (ls: locset) : locset := + fun (l: loc) => + match l with + | R r => + if In_dec Loc.eq (R r) Conventions.temporaries then + Vundef + else if In_dec Loc.eq (R r) Conventions.destroyed_at_call then + Vundef + else + ls (R r) + | S s => ls (S s) + end. (** LTL execution states. *) Inductive stackframe : Set := | Stackframe: - forall (sig: signature) (**r signature of call *) - (res: loc) (**r where to store the result *) + forall (res: loc) (**r where to store the result *) (f: function) (**r calling function *) (sp: val) (**r stack pointer in calling function *) (ls: locset) (**r location state in calling function *) @@ -160,27 +138,15 @@ Inductive state : Set := | Callstate: forall (stack: list stackframe) (**r call stack *) (f: fundef) (**r function to call *) - (ls: locset) (**r location state at point of call *) + (args: list val) (**r arguments to the call *) (m: mem), (**r memory state *) state | Returnstate: forall (stack: list stackframe) (**r call stack *) - (ls: locset) (**r location state at point of return *) + (v: val) (**r return value for the call *) (m: mem), (**r memory state *) state. -Definition parent_locset (stack: list stackframe) : locset := - match stack with - | nil => Locmap.init Vundef - | Stackframe sg res f sp ls pc :: stack' => ls - end. - -Definition parent_callsig (stack: list stackframe) : signature := - match stack with - | nil => mksignature nil (Some Tint) - | Stackframe sg res f sp ls pc :: stack' => sg - end. - Variable ge: genv. Definition find_function (los: loc + ident) (rs: locset) : option fundef := @@ -265,28 +231,23 @@ Inductive step: state -> trace -> state -> Prop := (fn_code f)!pc = Some(Lcall sig ros args res pc') -> find_function ros rs = Some f' -> funsig f' = sig -> - let rs1 := parmov args (loc_arguments sig) rs in step (State s f sp pc rs m) - E0 (Callstate (Stackframe sig res f sp rs1 pc' :: s) f' rs1 m) + E0 (Callstate (Stackframe res f sp (postcall_regs rs) pc' :: s) + f' (List.map rs args) m) | exec_Ltailcall: forall s f stk pc rs m sig ros args f', (fn_code f)!pc = Some(Ltailcall sig ros args) -> find_function ros rs = Some f' -> funsig f' = sig -> - let rs1 := parmov args (loc_arguments sig) rs in - let rs2 := return_regs (parent_locset s) rs1 in step (State s f (Vptr stk Int.zero) pc rs m) - E0 (Callstate s f' rs2 (Mem.free m stk)) + E0 (Callstate s f' (List.map rs args) (Mem.free m stk)) | exec_Lalloc: forall s f sp pc rs m pc' arg res sz m' b, (fn_code f)!pc = Some(Lalloc arg res pc') -> rs arg = Vint sz -> Mem.alloc m 0 (Int.signed sz) = (m', b) -> - let rs1 := Locmap.set (R loc_alloc_argument) (rs arg) rs in - let rs2 := Locmap.set (R loc_alloc_result) (Vptr b Int.zero) rs1 in - let rs3 := Locmap.set res (rs2 (R loc_alloc_result)) rs2 in step (State s f sp pc rs m) - E0 (State s f sp pc' rs3 m') + E0 (State s f sp pc' (Locmap.set res (Vptr b Int.zero) (postcall_regs rs)) m') | exec_Lcond_true: forall s f sp pc rs m cond args ifso ifnot, (fn_code f)!pc = Some(Lcond cond args ifso ifnot) -> @@ -302,30 +263,22 @@ Inductive step: state -> trace -> state -> Prop := | exec_Lreturn: forall s f stk pc rs m or, (fn_code f)!pc = Some(Lreturn or) -> - let rs1 := set_result_reg f.(fn_sig) or rs in - let rs2 := return_regs (parent_locset s) rs1 in step (State s f (Vptr stk Int.zero) pc rs m) - E0 (Returnstate s rs2 (Mem.free m stk)) + E0 (Returnstate s (locmap_optget or Vundef rs) (Mem.free m stk)) | exec_function_internal: - forall s f rs m m' stk, + forall s f args m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> - let rs1 := call_regs rs in - let rs2 := parmov (loc_parameters f.(fn_sig)) f.(fn_params) rs1 in - step (Callstate s (Internal f) rs m) - E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) rs2 m') + step (Callstate s (Internal f) args m) + E0 (State s f (Vptr stk Int.zero) f.(fn_entrypoint) (init_locs args f.(fn_params)) m') | exec_function_external: - forall s ef t res rs m, - let args := map rs (Conventions.loc_arguments ef.(ef_sig)) in + forall s ef t args res m, event_match ef args t res -> - let rs1 := - Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in - step (Callstate s (External ef) rs m) - t (Returnstate s rs1 m) + step (Callstate s (External ef) args m) + t (Returnstate s res m) | exec_return: - forall res f sp rs0 pc s sig rs m, - let rs1 := Locmap.set res (rs (R (loc_result sig))) rs in - step (Returnstate (Stackframe sig res f sp rs0 pc :: s) rs m) - E0 (State s f sp pc rs1 m). + forall res f sp rs pc s vres m, + step (Returnstate (Stackframe res f sp rs pc :: s) vres m) + E0 (State s f sp pc (Locmap.set res vres rs) m). End RELSEM. @@ -341,12 +294,11 @@ Inductive initial_state (p: program): state -> Prop := Genv.find_symbol ge p.(prog_main) = Some b -> Genv.find_funct_ptr ge b = Some f -> funsig f = mksignature nil (Some Tint) -> - initial_state p (Callstate nil f (Locmap.init Vundef) m0). + initial_state p (Callstate nil f nil m0). Inductive final_state: state -> int -> Prop := - | final_state_intro: forall rs m r, - rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r -> - final_state (Returnstate nil rs m) r. + | final_state_intro: forall n m, + final_state (Returnstate nil (Vint n) m) n. Definition exec_program (p: program) (beh: program_behavior) : Prop := program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. -- cgit