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.

1 files changed, 18 insertions, 0 deletions

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