From 4622f49fd089ae47d0c853343cb0a05f986c962a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 27 Mar 2015 08:55:05 +0100 Subject: Extend annotations so that they can keep track of global variables and local variables whose address is taken. - CminorSel, RTL: add "annot" instructions. - CminorSel to Asm: use type "annot_arg" for arguments of "annot" instructions. - AST, Events: simplify EF_annot because constants are now part of the arguments. Implementation is not complete yet. --- backend/RTL.v | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'backend/RTL.v') diff --git a/backend/RTL.v b/backend/RTL.v index e8ec1391..83761c42 100644 --- a/backend/RTL.v +++ b/backend/RTL.v @@ -74,6 +74,9 @@ Inductive instruction: Type := (** [Ibuiltin ef args dest succ] calls the built-in function identified by [ef], giving it the values of [args] as arguments. It stores the return value in [dest] and branches to [succ]. *) + | Iannot: external_function -> list (annot_arg reg) -> node -> instruction + (** [Iannot ef args succ] is similar to [Ibuiltin] but specialized + to annotations. *) | Icond: condition -> list reg -> node -> node -> instruction (** [Icond cond args ifso ifnot] evaluates the boolean condition [cond] over the values of registers [args]. If the condition @@ -255,6 +258,14 @@ Inductive step: state -> trace -> state -> Prop := external_call ef ge rs##args m t v m' -> step (State s f sp pc rs m) t (State s f sp pc' (rs#res <- v) m') + | exec_Iannot: + forall s f sp pc rs m ef args pc' vargs vres t m', + (fn_code f)!pc = Some(Iannot ef args pc') -> + match ef with EF_annot _ _ => True | _ => False end -> + eval_annot_args ge (fun r => rs#r) sp m args vargs -> + external_call ef ge vargs m t vres m' -> + step (State s f sp pc rs m) + t (State s f sp pc' rs m') | exec_Icond: forall s f sp pc rs m cond args ifso ifnot b pc', (fn_code f)!pc = Some(Icond cond args ifso ifnot) -> @@ -358,11 +369,14 @@ Proof. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (State s0 f sp pc' (rs#res <- vres2) m2). eapply exec_Ibuiltin; eauto. exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. + exists (State s0 f sp pc' rs m2). eapply exec_Iannot; eauto. + exploit external_call_receptive; eauto. intros [vres2 [m2 EC2]]. exists (Returnstate s0 vres2 m2). econstructor; eauto. (* trace length *) red; intros; inv H; simpl; try omega. eapply external_call_trace_length; eauto. eapply external_call_trace_length; eauto. + eapply external_call_trace_length; eauto. Qed. (** * Operations on RTL abstract syntax *) @@ -397,6 +411,7 @@ Definition successors_instr (i: instruction) : list node := | Icall sig ros args res s => s :: nil | Itailcall sig ros args => nil | Ibuiltin ef args res s => s :: nil + | Iannot ef args s => s :: nil | Icond cond args ifso ifnot => ifso :: ifnot :: nil | Ijumptable arg tbl => tbl | Ireturn optarg => nil @@ -418,6 +433,7 @@ Definition instr_uses (i: instruction) : list reg := | Itailcall sig (inl r) args => r :: args | Itailcall sig (inr id) args => args | Ibuiltin ef args res s => args + | Iannot ef args s => params_of_annot_args args | Icond cond args ifso ifnot => args | Ijumptable arg tbl => arg :: nil | Ireturn None => nil @@ -435,6 +451,7 @@ Definition instr_defs (i: instruction) : option reg := | Icall sig ros args res s => Some res | Itailcall sig ros args => None | Ibuiltin ef args res s => Some res + | Iannot ef args s => None | Icond cond args ifso ifnot => None | Ijumptable arg tbl => None | Ireturn optarg => None @@ -476,6 +493,7 @@ Definition max_reg_instr (m: positive) (pc: node) (i: instruction) := | Itailcall sig (inl r) args => fold_left Pmax args (Pmax r m) | Itailcall sig (inr id) args => fold_left Pmax args m | Ibuiltin ef args res s => fold_left Pmax args (Pmax res m) + | Iannot ef args s => fold_left Pmax (params_of_annot_args args) m | Icond cond args ifso ifnot => fold_left Pmax args m | Ijumptable arg tbl => Pmax arg m | Ireturn None => m -- cgit