From 0290650b7463088bb228bc96d3143941590b54dd Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 7 Jul 2008 13:55:29 +0000 Subject: Nettoyage du traitement des signatures au return dans LTL et LTLin git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@690 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/LTL.v | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) (limited to 'backend/LTL.v') diff --git a/backend/LTL.v b/backend/LTL.v index e99e016e..a082e122 100644 --- a/backend/LTL.v +++ b/backend/LTL.v @@ -140,7 +140,8 @@ Definition set_result_reg (s: signature) (or: option loc) (ls: locset) := Inductive stackframe : Set := | Stackframe: - forall (res: loc) (**r where to store the result *) + forall (sig: signature) (**r signature of call *) + (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 *) @@ -164,7 +165,6 @@ Inductive state : Set := state | Returnstate: forall (stack: list stackframe) (**r call stack *) - (sig: signature) (**r signature of returning function *) (ls: locset) (**r location state at point of return *) (m: mem), (**r memory state *) state. @@ -172,7 +172,13 @@ Inductive state : Set := Definition parent_locset (stack: list stackframe) : locset := match stack with | nil => Locmap.init Vundef - | Stackframe res f sp ls pc :: stack' => ls + | 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. @@ -261,7 +267,7 @@ Inductive step: state -> trace -> state -> Prop := funsig f' = sig -> let rs1 := parmov args (loc_arguments sig) rs in step (State s f sp pc rs m) - E0 (Callstate (Stackframe res f sp rs1 pc' :: s) f' rs1 m) + E0 (Callstate (Stackframe sig res f sp rs1 pc' :: s) f' rs1 m) | exec_Ltailcall: forall s f stk pc rs m sig ros args f', (fn_code f)!pc = Some(Ltailcall sig ros args) -> @@ -299,7 +305,7 @@ Inductive step: state -> trace -> state -> Prop := 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 f.(fn_sig) rs2 (Mem.free m stk)) + E0 (Returnstate s rs2 (Mem.free m stk)) | exec_function_internal: forall s f rs m m' stk, Mem.alloc m 0 f.(fn_stacksize) = (m', stk) -> @@ -314,12 +320,11 @@ Inductive step: state -> trace -> state -> Prop := let rs1 := Locmap.set (R (Conventions.loc_result ef.(ef_sig))) res rs in step (Callstate s (External ef) rs m) - t (Returnstate s ef.(ef_sig) rs1 m) + t (Returnstate s rs1 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 res f sp rs0 pc :: s) - sig rs m) + step (Returnstate (Stackframe sig res f sp rs0 pc :: s) rs m) E0 (State s f sp pc rs1 m). End RELSEM. @@ -339,9 +344,9 @@ Inductive initial_state (p: program): state -> Prop := initial_state p (Callstate nil f (Locmap.init Vundef) m0). Inductive final_state: state -> int -> Prop := - | final_state_intro: forall sig rs m r, - rs (R (loc_result sig)) = Vint r -> - final_state (Returnstate nil sig rs m) r. + | final_state_intro: forall rs m r, + rs (R (loc_result (mksignature nil (Some Tint)))) = Vint r -> + final_state (Returnstate nil rs m) r. Definition exec_program (p: program) (beh: program_behavior) : Prop := program_behaves step (initial_state p) final_state (Genv.globalenv p) beh. -- cgit