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, 13 insertions, 0 deletions

diff --git a/backend/Deadcode.v b/backend/Deadcode.v
index 98bc14a8..9a8f85d2 100644
--- a/backend/Deadcode.v
+++ b/backend/Deadcode.v
@@ -70,6 +70,17 @@ Definition is_dead (v: nval) :=
 Definition is_int_zero (v: nval) :=
   match v with I n => Int.eq n Int.zero | _ => false end.
 
+Fixpoint transfer_annot_arg (na: NA.t) (a: annot_arg reg) : NA.t :=
+  let (ne, nm) := na in
+  match a with
+  | AA_base r => (add_need_all r ne, nm)
+  | AA_int _ | AA_long _ | AA_float _ | AA_single _
+  | AA_addrstack _ | AA_addrglobal _ _ => (ne, nm)
+  | AA_loadstack chunk ofs => (ne, nmem_add nm (Stk ofs) (size_chunk chunk))
+  | AA_loadglobal chunk id ofs => (ne, nmem_add nm (Gl id ofs) (size_chunk chunk))
+  | AA_longofwords hi lo => transfer_annot_arg (transfer_annot_arg na hi) lo
+  end.
+
 Function transfer_builtin (app: VA.t) (ef: external_function) (args: list reg) (res: reg)
                           (ne: NE.t) (nm: nmem) : NA.t :=
   match ef, args with
@@ -128,6 +139,8 @@ Definition transfer (f: function) (approx: PMap.t VA.t)
        nmem_dead_stack f.(fn_stacksize))
   | Some(Ibuiltin ef args res s) =>
       transfer_builtin approx!!pc ef args res ne nm
+  | Some(Iannot ef args s) =>
+      List.fold_left transfer_annot_arg args after
   | Some(Icond cond args s1 s2) =>
       (add_needs args (needs_of_condition cond) ne, nm)
   | Some(Ijumptable arg tbl) =>