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.

48 files changed, 1692 insertions, 368 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 919843b5..37b79a1a 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -22,6 +22,7 @@ Require Import Maps.
 Require Import Lattice.
 Require Import AST.
 Require Import Integers.
+Require Import Floats.
 Require Import Memdata.
 Require Import Op.
 Require Import Registers.
@@ -95,8 +96,9 @@ Inductive block_shape: Type :=
   | BSbuiltin (ef: external_function) (args: list reg) (res: reg)
          (mv1: moves) (args': list mreg) (res': list mreg)
          (mv2: moves) (s: node)
-  | BSannot (text: ident) (targs: list annot_arg) (args: list reg) (res: reg)
-         (mv: moves) (args': list loc) (s: node)
+  | BSannot (ef: external_function)
+         (args: list (annot_arg reg)) (args': list (annot_arg loc))
+         (s: node)
   | BScond (cond: condition) (args: list reg)
          (mv: moves) (args': list mreg) (s1 s2: node)
   | BSjumptable (arg: reg)
@@ -276,13 +278,14 @@ Definition pair_instr_block
           assertion (external_function_eq ef ef');
           assertion (check_succ s b3);
           Some(BSbuiltin ef args res mv1 args' res' mv2 s)
-      | Lannot ef' args' :: b2 =>
+      | _ => None
+      end
+  | Iannot ef args s =>
+      match b with
+      | Lannot ef' args' :: b1 =>
           assertion (external_function_eq ef ef');
-          assertion (check_succ s b2);
-          match ef with
-          | EF_annot txt typ => Some(BSannot txt typ args res mv1 args' s)
-          | _ => None
-          end
+          assertion (check_succ s b1);
+          Some(BSannot ef args args' s)
       | _ => None
       end
   | Icond cond args s1 s2 =>
@@ -696,6 +699,57 @@ Definition add_equation_ros (ros: reg + ident) (ros': mreg + ident) (e: eqs) : o
   | _, _ => None
   end.
 
+(** [add_equations_annot_arg] adds the needed equations for annotation
+   arguments. *)
+
+Fixpoint add_equations_annot_arg (env: regenv) (arg: annot_arg reg) (arg': annot_arg loc) (e: eqs) : option eqs :=
+  match arg, arg' with
+  | AA_base r, AA_base l =>
+      Some (add_equation (Eq Full r l) e)
+  | AA_base r, AA_longofwords (AA_base lhi) (AA_base llo) =>
+      assertion (typ_eq (env r) Tlong);
+      Some (add_equation (Eq Low r llo) (add_equation (Eq High r lhi) e))
+  | AA_int n, AA_int n' =>
+      assertion (Int.eq_dec n n'); Some e
+  | AA_long n, AA_long n' =>
+      assertion (Int64.eq_dec n n'); Some e
+  | AA_float f, AA_float f' =>
+      assertion (Float.eq_dec f f'); Some e
+  | AA_single f, AA_single f' =>
+      assertion (Float32.eq_dec f f'); Some e
+  | AA_loadstack chunk ofs, AA_loadstack chunk' ofs' =>
+      assertion (chunk_eq chunk chunk');
+      assertion (Int.eq_dec ofs ofs');
+      Some e
+  | AA_addrstack ofs, AA_addrstack ofs' =>
+      assertion (Int.eq_dec ofs ofs');
+      Some e
+  | AA_loadglobal chunk id ofs, AA_loadglobal chunk' id' ofs' =>
+      assertion (chunk_eq chunk chunk');
+      assertion (ident_eq id id');
+      assertion (Int.eq_dec ofs ofs');
+      Some e
+  | AA_addrglobal id ofs, AA_addrglobal id' ofs' =>
+      assertion (ident_eq id id');
+      assertion (Int.eq_dec ofs ofs');
+      Some e
+  | AA_longofwords hi lo, AA_longofwords hi' lo' =>
+      do e1 <- add_equations_annot_arg env hi hi' e;
+      add_equations_annot_arg env lo lo' e1
+  | _, _ =>
+      None
+  end.
+
+Fixpoint add_equations_annot_args (env: regenv)
+   (args: list(annot_arg reg)) (args': list(annot_arg loc)) (e: eqs) : option eqs :=
+  match args, args' with
+  | nil, nil => Some e
+  | a1 :: al, a1' :: al' =>
+      do e1 <- add_equations_annot_arg env a1 a1' e;
+      add_equations_annot_args env al al' e1
+  | _, _ => None
+  end.
+
 (** [can_undef ml] returns true if all machine registers in [ml] are
   unconstrained and can harmlessly be undefined. *)
 
@@ -926,9 +980,8 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
       assertion (can_undef (destroyed_by_builtin ef) e2);
       do e3 <- add_equations_args args (sig_args (ef_sig ef)) args' e2;
       track_moves env mv1 e3
-  | BSannot txt typ args res mv1 args' s =>
-      do e1 <- add_equations_args args (annot_args_typ typ) args' e;
-      track_moves env mv1 e1
+  | BSannot ef args args' s =>
+      add_equations_annot_args env args args' e
   | BScond cond args mv args' s1 s2 =>
       assertion (can_undef (destroyed_by_cond cond) e);
       do e1 <- add_equations args args' e;
@@ -1099,7 +1152,7 @@ Definition successors_block_shape (bsh: block_shape) : list node :=
   | BScall sg ros args res mv1 ros' mv2 s => s :: nil
   | BStailcall sg ros args mv1 ros' => nil
   | BSbuiltin ef args res mv1 args' res' mv2 s => s :: nil
-  | BSannot txt typ args res mv1 args' s => s :: nil
+  | BSannot ef args args' s => s :: nil
   | BScond cond args mv args' s1 s2 => s1 :: s2 :: nil
   | BSjumptable arg mv arg' tbl => tbl
   | BSreturn optarg mv => nil
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 2612ebf2..875d4929 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -165,12 +165,10 @@ Inductive expand_block_shape: block_shape -> RTL.instruction -> LTL.bblock -> Pr
                          (Ibuiltin ef args res s)
                          (expand_moves mv1
                            (Lbuiltin ef args' res' :: expand_moves mv2 (Lbranch s :: k)))
-  | ebs_annot: forall txt typ args res mv args' s k,
-      wf_moves mv ->
-      expand_block_shape (BSannot txt typ args res mv args' s)
-                         (Ibuiltin (EF_annot txt typ) args res s)
-                         (expand_moves mv
-                           (Lannot (EF_annot txt typ) args' :: Lbranch s :: k))
+  | ebs_annot: forall ef args args' s k,
+      expand_block_shape (BSannot ef args args' s)
+                         (Iannot ef args s)
+                         (Lannot ef args' :: Lbranch s :: k)
   | ebs_cond: forall cond args mv args' s1 s2 k,
       wf_moves mv ->
       expand_block_shape (BScond cond args mv args' s1 s2)
@@ -322,7 +320,8 @@ Proof.
 (* builtin *) 
   destruct b0; MonadInv. destruct i; MonadInv; UseParsingLemmas.
   econstructor; eauto.
-  destruct ef; inv H. econstructor; eauto. 
+(* annot *)
+  destruct b; MonadInv. destruct i; MonadInv. UseParsingLemmas. constructor.  
 (* cond *)
   destruct b0; MonadInv. destruct i; MonadInv; UseParsingLemmas. econstructor; eauto.
 (* jumptable *)
@@ -1348,6 +1347,75 @@ Proof.
   rewrite Int64.hi_ofwords, Int64.lo_ofwords; auto. 
 Qed.
 
+Lemma add_equations_annot_arg_satisf:
+  forall env rs ls arg arg' e e',
+  add_equations_annot_arg env arg arg' e = Some e' ->
+  satisf rs ls e' -> satisf rs ls e.
+Proof.
+  induction arg; destruct arg'; simpl; intros; MonadInv; eauto.
+  eapply add_equation_satisf; eauto.
+  destruct arg'1; MonadInv. destruct arg'2; MonadInv. eauto using add_equation_satisf.
+Qed.
+
+Lemma add_equations_annot_arg_lessdef:
+  forall env (ge: RTL.genv) sp rs ls m arg v,
+  eval_annot_arg ge (fun r => rs#r) sp m arg v ->
+  forall e e' arg',
+  add_equations_annot_arg env arg arg' e = Some e' ->
+  satisf rs ls e' ->
+  wt_regset env rs ->
+  exists v', eval_annot_arg ge ls sp m arg' v' /\ Val.lessdef v v'.
+Proof.
+  induction 1; simpl; intros e e' arg' AE SAT WT; destruct arg'; MonadInv.
+- exploit add_equation_lessdef; eauto. simpl; intros.
+  exists (ls x0); auto with aarg.
+- destruct arg'1; MonadInv. destruct arg'2; MonadInv. 
+  exploit add_equation_lessdef. eauto. simpl; intros LD1.
+  exploit add_equation_lessdef. eapply add_equation_satisf. eauto. simpl; intros LD2.
+  exists (Val.longofwords (ls x0) (ls x1)); split; auto with aarg. 
+  rewrite <- (val_longofwords_eq rs#x). apply Val.longofwords_lessdef; auto.
+  rewrite <- e0; apply WT. 
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- exploit IHeval_annot_arg1; eauto. eapply add_equations_annot_arg_satisf; eauto. 
+  intros (v1 & A & B).
+  exploit IHeval_annot_arg2; eauto. intros (v2 & C & D).
+  exists (Val.longofwords v1 v2); split; auto with aarg. apply Val.longofwords_lessdef; auto.
+Qed.
+
+Lemma add_equations_annot_args_satisf:
+  forall env rs ls arg arg' e e',
+  add_equations_annot_args env arg arg' e = Some e' ->
+  satisf rs ls e' -> satisf rs ls e.
+Proof.
+  induction arg; destruct arg'; simpl; intros; MonadInv; eauto using add_equations_annot_arg_satisf.
+Qed.
+
+Lemma add_equations_annot_args_lessdef:
+  forall env (ge: RTL.genv) sp rs ls m tm arg vl,
+  eval_annot_args ge (fun r => rs#r) sp m arg vl ->
+  forall arg' e e',
+  add_equations_annot_args env arg arg' e = Some e' ->
+  satisf rs ls e' ->
+  wt_regset env rs ->
+  Mem.extends m tm ->
+  exists vl', eval_annot_args ge ls sp tm arg' vl' /\ Val.lessdef_list vl vl'.
+Proof.
+  induction 1; simpl; intros; destruct arg'; MonadInv.
+- exists (@nil val); split; constructor.
+- exploit IHlist_forall2; eauto. intros (vl' & A & B).
+  exploit add_equations_annot_arg_lessdef; eauto. 
+  eapply add_equations_annot_args_satisf; eauto. intros (v1' & C & D).
+  exploit (@eval_annot_arg_lessdef _ ge ls ls); eauto. intros (v1'' & E & F).
+  exists (v1'' :: vl'); split; constructor; auto. eapply Val.lessdef_trans; eauto. 
+Qed.
+
 (** * Properties of the dataflow analysis *)
 
 Lemma analyze_successors:
@@ -2035,27 +2103,21 @@ Proof.
   econstructor; eauto.
  
 (* annot *)
-- exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]]. 
-  exploit external_call_mem_extends; eauto. eapply add_equations_args_lessdef; eauto.
-  inv WTI. simpl in H4. rewrite <- H4. apply wt_regset_list; auto. 
-  intros [v' [m'' [F [G [J K]]]]].
-  assert (v = Vundef). red in H0; inv H0. auto.
+- exploit add_equations_annot_args_lessdef; eauto.
+  intros (vargs' & A & B). 
+  exploit external_call_mem_extends; eauto.
+  intros [vres' [m'' [F [G [J K]]]]].
   econstructor; split.
   eapply plus_left. econstructor; eauto. 
-  eapply star_trans. eexact A1. 
   eapply star_two. econstructor.
-  eapply external_call_symbols_preserved' with (ge1 := ge).
-  econstructor; eauto. 
+  eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved with (ge1 := ge); eauto. 
   exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
-  eauto. constructor. eauto. eauto. traceEq.
+  constructor. eauto. traceEq.
   exploit satisf_successors. eauto. eauto. simpl; eauto. eauto. 
-  eapply satisf_undef_reg with (r := res).
-  eapply add_equations_args_satisf; eauto. 
+  eapply add_equations_annot_args_satisf; eauto. 
   intros [enext [U V]]. 
   econstructor; eauto.
-  change (destroyed_by_builtin (EF_annot txt typ)) with (@nil mreg). 
-  simpl. subst v. assumption.
-  apply wt_regset_assign; auto. subst v. constructor. 
 
 (* cond *)
 - exploit (exec_moves mv); eauto. intros [ls1 [A1 B1]].
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index 3801a4f6..ba7fa3a6 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -358,34 +358,27 @@ Qed.
 
 (** Translation of arguments to annotations. *)
 
-Lemma annot_arg_match:
-  forall ms sp rs m m' p v,
-  agree ms sp rs ->
-  Mem.extends m m' ->
-  Mach.annot_arg ms m sp p v ->
-  exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v'.
+Remark annot_arg_match:
+  forall ge (rs: regset) sp m a v,
+  eval_annot_arg ge (fun r => rs (preg_of r)) sp m a v ->
+  eval_annot_arg ge rs sp m (map_annot_arg preg_of a) v.
 Proof.
-  intros. inv H1; simpl.
-(* reg *)
-  exists (rs (preg_of r)); split. constructor. eapply preg_val; eauto.
-(* stack *)
-  exploit Mem.load_extends; eauto. intros [v' [A B]].
-  exists v'; split; auto. 
-  inv H. econstructor; eauto. 
+  induction 1; simpl; eauto with aarg.
 Qed.
 
-Lemma annot_arguments_match:
-  forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
-  forall pl vl,
-  Mach.annot_arguments ms m sp pl vl ->
-  exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl'
+Lemma annot_args_match:
+  forall ge ms sp rs m m', agree ms sp rs -> Mem.extends m m' ->
+  forall al vl, eval_annot_args ge ms sp m al vl ->
+  exists vl', eval_annot_args ge rs sp m' (map (map_annot_arg preg_of) al) vl'
            /\ Val.lessdef_list vl vl'.
 Proof.
-  induction 3; intros. 
-  exists (@nil val); split. constructor. constructor.
-  exploit annot_arg_match; eauto. intros [v1' [A B]].
+  induction 3; intros; simpl.
+  exists (@nil val); split; constructor.
+  exploit (@eval_annot_arg_lessdef _ ge ms (fun r => rs (preg_of r))); eauto. 
+  intros; eapply preg_val; eauto.
+  intros (v1' & A & B).
   destruct IHlist_forall2 as [vl' [C D]].
-  exists (v1' :: vl'); split; constructor; auto.
+  exists (v1' :: vl'); split; constructor; auto. apply annot_arg_match; auto. 
 Qed.
 
 (** * Correspondence between Mach code and Asm code *)
diff --git a/backend/Bounds.v b/backend/Bounds.v
index bcd28487..249ff796 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -69,7 +69,7 @@ Definition instr_within_bounds (i: instruction) :=
   | Lbuiltin ef args res =>
       forall r, In r res \/ In r (destroyed_by_builtin ef) -> mreg_within_bounds r
   | Lannot ef args =>
-      forall sl ofs ty, In (S sl ofs ty) args -> slot_within_bounds sl ofs ty
+      forall sl ofs ty, In (S sl ofs ty) (params_of_annot_args args) -> slot_within_bounds sl ofs ty
   | _ => True
   end.
 
@@ -121,7 +121,7 @@ Definition slots_of_instr (i: instruction) : list (slot * Z * typ) :=
   match i with
   | Lgetstack sl ofs ty r => (sl, ofs, ty) :: nil
   | Lsetstack r sl ofs ty => (sl, ofs, ty) :: nil
-  | Lannot ef args => slots_of_locs args
+  | Lannot ef args => slots_of_locs (params_of_annot_args args)
   | _ => nil
   end.
 
diff --git a/backend/CSE.v b/backend/CSE.v
index fa229871..2c0c5f33 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -492,6 +492,8 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb
           | EF_vload _ | EF_vload_global _ _ _ | EF_annot _ _ | EF_annot_val _ _ =>
               set_unknown before res
           end
+      | Iannot ef args s =>
+          before
       | Icond cond args ifso ifnot =>
           before
       | Ijumptable arg tbl =>
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index ae8052be..74e3ceca 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -1144,6 +1144,21 @@ Proof.
   + apply CASE1.
 * apply set_reg_lessdef; auto.
 
+- (* Iannot *)
+  exploit (@eval_annot_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto. 
+  intros (vargs' & A & B).
+  exploit external_call_mem_extends; eauto.
+  intros (v' & m1' & P & Q & R & S).
+  econstructor; split.
+  eapply exec_Iannot; eauto.
+  eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  econstructor; eauto.
+  eapply analysis_correct_1; eauto. simpl; auto.
+  unfold transfer; rewrite H. replace m' with m; auto. 
+  destruct ef; try contradiction. inv H2; auto.
+
 - (* Icond *)
   destruct (valnum_regs approx!!pc args) as [n1 vl] eqn:?.
   elim SAT; intros valu1 NH1.
diff --git a/backend/CleanupLabelsproof.v b/backend/CleanupLabelsproof.v
index f952f1ea..d48a0553 100644
--- a/backend/CleanupLabelsproof.v
+++ b/backend/CleanupLabelsproof.v
@@ -296,7 +296,9 @@ Proof.
   econstructor; eauto with coqlib.
 (* Lannot *)
   left; econstructor; split.
-  econstructor; eauto. eapply external_call_symbols_preserved'; eauto.
+  econstructor; eauto. 
+  eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved.  exact public_preserved. exact varinfo_preserved.
   econstructor; eauto with coqlib.
 (* Llabel *)
diff --git a/backend/CminorSel.v b/backend/CminorSel.v
index 03ef0926..668eb808 100644
--- a/backend/CminorSel.v
+++ b/backend/CminorSel.v
@@ -79,6 +79,7 @@ Inductive stmt : Type :=
   | Scall : option ident -> signature -> expr + ident -> exprlist -> stmt
   | Stailcall: signature -> expr + ident -> exprlist -> stmt
   | Sbuiltin : option ident -> external_function -> exprlist -> stmt
+  | Sannot : external_function -> list (annot_arg expr) -> stmt
   | Sseq: stmt -> stmt -> stmt
   | Sifthenelse: condexpr -> stmt -> stmt -> stmt
   | Sloop: stmt -> stmt
@@ -248,6 +249,32 @@ Inductive eval_expr_or_symbol: letenv -> expr + ident -> val -> Prop :=
       Genv.find_symbol ge id = Some b ->
       eval_expr_or_symbol le (inr _ id) (Vptr b Int.zero).
 
+Inductive eval_annot_arg: annot_arg expr -> val -> Prop :=
+  | eval_AA_base: forall a v,
+      eval_expr nil a v ->
+      eval_annot_arg (AA_base a) v
+  | eval_AA_int: forall n,
+      eval_annot_arg (AA_int n) (Vint n)
+  | eval_AA_long: forall n,
+      eval_annot_arg (AA_long n) (Vlong n)
+  | eval_AA_float: forall n,
+      eval_annot_arg (AA_float n) (Vfloat n)
+  | eval_AA_single: forall n,
+      eval_annot_arg (AA_single n) (Vsingle n)
+  | eval_AA_loadstack: forall chunk ofs v,
+      Mem.loadv chunk m (Val.add sp (Vint ofs)) = Some v ->
+      eval_annot_arg (AA_loadstack chunk ofs) v
+  | eval_AA_addrstack: forall ofs,
+      eval_annot_arg (AA_addrstack ofs) (Val.add sp (Vint ofs))
+  | eval_AA_loadglobal: forall chunk id ofs v,
+      Mem.loadv chunk m (Genv.symbol_address ge id ofs) = Some v ->
+      eval_annot_arg (AA_loadglobal chunk id ofs) v
+  | eval_AA_addrglobal: forall id ofs,
+      eval_annot_arg (AA_addrglobal id ofs) (Genv.symbol_address ge id ofs)
+  | eval_AA_longofwords: forall a1 a2 v1 v2,
+      eval_expr nil a1 v1 -> eval_expr nil a2 v2 ->
+      eval_annot_arg (AA_longofwords (AA_base a1) (AA_base a2)) (Val.longofwords v1 v2).
+
 End EVAL_EXPR.
 
 (** Pop continuation until a call or stop *)
@@ -343,6 +370,13 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State f (Sbuiltin optid ef al) k sp e m)
          t (State f Sskip k sp (set_optvar optid v e) m')
 
+  | step_annot: forall f ef al k sp e m vl t v m',
+      match ef with EF_annot _ _ => True | _ => False end ->
+      list_forall2 (eval_annot_arg sp e m) al vl ->
+      external_call ef ge vl m t v m' ->
+      step (State f (Sannot ef al) k sp e m)
+         t (State f Sskip k sp e m')
+
   | step_seq: forall f s1 s2 k sp e m,
       step (State f (Sseq s1 s2) k sp e m)
         E0 (State f s1 (Kseq s2 k) sp e m)
diff --git a/backend/Constprop.v b/backend/Constprop.v
index bdfc4b17..ce56ff62 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -102,23 +102,22 @@ Definition num_iter := 10%nat.
 Definition successor (f: function) (ae: AE.t) (pc: node) : node :=
   successor_rec num_iter f ae pc.
 
-Fixpoint annot_strength_reduction
-     (ae: AE.t) (targs: list annot_arg) (args: list reg) :=
-  match targs, args with
-  | AA_arg ty :: targs', arg :: args' =>
-      let (targs'', args'') := annot_strength_reduction ae targs' args' in
-      match ty, areg ae arg with
-      | Tint, I n => (AA_int n :: targs'', args'')
-      | Tfloat, F n => if Compopts.generate_float_constants tt
-                       then (AA_float n :: targs'', args'')
-                       else (AA_arg ty :: targs'', arg :: args'')
-      | _, _ => (AA_arg ty :: targs'', arg :: args'')
+Fixpoint annot_strength_reduction (ae: AE.t) (a: annot_arg reg) :=
+  match a with
+  | AA_base r =>
+      match areg ae r with
+      | I n => AA_int n
+      | L n => AA_long n
+      | F n => if Compopts.generate_float_constants tt then AA_float n else a
+      | FS n => if Compopts.generate_float_constants tt then AA_single n else a
+      | _ => a
       end
-  | targ :: targs', _ =>
-      let (targs'', args'') := annot_strength_reduction ae targs' args in
-      (targ :: targs'', args'')
-  | _, _ =>
-      (targs, args)
+  | AA_longofwords hi lo =>
+      match annot_strength_reduction ae hi, annot_strength_reduction ae lo with
+      | AA_int nhi, AA_int nlo => AA_long (Int64.ofwords nhi nlo)
+      | hi', lo' => AA_longofwords hi' lo'
+      end
+  | _ => a
   end.
 
 Function builtin_strength_reduction
@@ -134,9 +133,6 @@ Function builtin_strength_reduction
       | Ptr(Gl symb n1) => (EF_vstore_global chunk symb n1, r2 :: nil)
       | _ => (ef, args)
       end
-  | EF_annot text targs, args =>
-      let (targs', args') := annot_strength_reduction ae targs args in
-      (EF_annot text targs', args')
   | _, _ =>
       (ef, args)
   end.
@@ -180,6 +176,8 @@ Definition transf_instr (f: function) (an: PMap.t VA.t) (rm: romem)
       | Ibuiltin ef args res s =>
           let (ef', args') := builtin_strength_reduction ae ef args in
           Ibuiltin ef' args' res s
+      | Iannot ef args s =>
+          Iannot ef (List.map (annot_strength_reduction ae) args) s
       | Icond cond args s1 s2 =>
           let aargs := aregs ae args in
           match resolve_branch (eval_static_condition cond aargs) with
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index 450050de..30bdd674 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -211,83 +211,56 @@ Proof.
   unfold successor; intros. apply match_successor_rec.
 Qed.
 
-Section BUILTIN_STRENGTH_REDUCTION.
-
-Variable bc: block_classification.
-Hypothesis GE: genv_match bc ge.
-Variable ae: AE.t.
-Variable rs: regset.
-Hypothesis MATCH: ematch bc rs ae.
-
 Lemma annot_strength_reduction_correct:
-  forall targs args targs' args' eargs,
-  annot_strength_reduction ae targs args = (targs', args') ->
-  eventval_list_match ge eargs (annot_args_typ targs) rs##args ->
-  exists eargs',
-  eventval_list_match ge eargs' (annot_args_typ targs') rs##args'
-  /\ annot_eventvals targs' eargs' = annot_eventvals targs eargs.
+  forall bc sp m rs ae, ematch bc rs ae ->
+  forall a v,
+  eval_annot_arg ge (fun r => rs#r) sp m a v ->
+  eval_annot_arg ge (fun r => rs#r) sp m (annot_strength_reduction ae a) v.
 Proof.
-  induction targs; simpl; intros.
-- inv H. simpl. exists eargs; auto. 
-- destruct a.
-  + destruct args as [ | arg args0]; simpl in H0; inv H0.
-    destruct (annot_strength_reduction ae targs args0) as [targs'' args''] eqn:E.
-    exploit IHtargs; eauto. intros [eargs'' [A B]].
-    assert (DFL:
-      exists eargs',
-      eventval_list_match ge eargs' (annot_args_typ (AA_arg ty :: targs'')) rs##(arg :: args'')
-      /\ annot_eventvals (AA_arg ty :: targs'') eargs' = ev1 :: annot_eventvals targs evl).
-    {
-      exists (ev1 :: eargs''); split.
-      simpl; constructor; auto. simpl. congruence.
-    }
-    destruct ty; destruct (areg ae arg) as [] eqn:E2; inv H; auto.
-    * exists eargs''; split; auto; simpl; f_equal; auto. 
-      generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM.
-      inv VM. rewrite <- H0 in *. inv H5; auto.
-    * destruct (Compopts.generate_float_constants tt); inv H1; auto. 
-      exists eargs''; split; auto; simpl; f_equal; auto. 
-      generalize (MATCH arg); fold (areg ae arg); rewrite E2; intros VM.
-      inv VM. rewrite <- H0 in *. inv H5; auto.
-  + destruct (annot_strength_reduction ae targs args) as [targs'' args''] eqn:E.
-    inv H.
-    exploit IHtargs; eauto. intros [eargs'' [A B]].
-    exists eargs''; simpl; split; auto. congruence.
-  + destruct (annot_strength_reduction ae targs args) as [targs'' args''] eqn:E.
-    inv H.
-    exploit IHtargs; eauto. intros [eargs'' [A B]].
-    exists eargs''; simpl; split; auto. congruence.
+  induction 2; simpl; eauto with aarg.
+- specialize (H x). unfold areg. destruct (AE.get x ae); try constructor. 
+  + inv H. constructor.
+  + inv H. constructor.
+  + destruct (Compopts.generate_float_constants tt); [inv H|idtac]; constructor.
+  + destruct (Compopts.generate_float_constants tt); [inv H|idtac]; constructor.
+- destruct (annot_strength_reduction ae hi); auto with aarg.
+  destruct (annot_strength_reduction ae lo); auto with aarg.
+  inv IHeval_annot_arg1; inv IHeval_annot_arg2. constructor. 
 Qed.
 
-Lemma vmatch_ptr_gl':
-  forall v id ofs,
-  vmatch bc v (Ptr (Gl id ofs)) ->
-  v = Vundef \/ exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b ofs.
+Lemma annot_strength_reduction_correct_2:
+  forall bc sp m rs ae, ematch bc rs ae ->
+  forall al vl,
+  eval_annot_args ge (fun r => rs#r) sp m al vl ->
+  eval_annot_args ge (fun r => rs#r) sp m (List.map (annot_strength_reduction ae) al) vl.
 Proof.
-  intros. inv H; auto. inv H2. right; exists b; split; auto. eapply GE; eauto.
-Qed. 
+  induction 2; simpl; constructor; auto. eapply annot_strength_reduction_correct; eauto. 
+Qed.
 
 Lemma builtin_strength_reduction_correct:
-  forall ef args m t vres m',
+  forall bc ae rs ef args m t vres m',
+  genv_match bc ge ->
+  ematch bc rs ae ->
   external_call ef ge rs##args m t vres m' ->
   let (ef', args') := builtin_strength_reduction ae ef args in
   external_call ef' ge rs##args' m t vres m'.
 Proof.
-  intros until m'. functional induction (builtin_strength_reduction ae ef args); intros; auto.
+  intros until m'. intros GE MATCH. 
+  assert (M: forall v id ofs,
+             vmatch bc v (Ptr (Gl id ofs)) ->
+             v = Vundef \/ exists b, Genv.find_symbol ge id = Some b /\ v = Vptr b ofs).
+  { intros. inv H; auto. inv H2. right; exists b; split; auto. eapply GE; eauto. }
+  functional induction (builtin_strength_reduction ae ef args); intros; auto.
 + simpl in H. assert (V: vmatch bc (rs#r1) (Ptr (Gl symb n1))) by (rewrite <- e1; apply MATCH). 
-  exploit vmatch_ptr_gl'; eauto. intros [A | [b [A B]]].
+  exploit M; eauto. intros [A | [b [A B]]].
   * simpl in H; rewrite A in H; inv H.
   * simpl; rewrite volatile_load_global_charact; simpl. exists b; split; congruence.
 + simpl in H. assert (V: vmatch bc (rs#r1) (Ptr (Gl symb n1))) by (rewrite <- e1; apply MATCH). 
-  exploit vmatch_ptr_gl'; eauto. intros [A | [b [A B]]].
+  exploit M; eauto. intros [A | [b [A B]]].
   * simpl in H; rewrite A in H; inv H.
   * simpl; rewrite volatile_store_global_charact; simpl. exists b; split; congruence.
-+ inv H. exploit annot_strength_reduction_correct; eauto. intros [eargs' [A B]]. 
-  rewrite <- B. econstructor; eauto. 
 Qed.
 
-End BUILTIN_STRENGTH_REDUCTION.
-
 (** The proof of semantic preservation is a simulation argument
   based on "option" diagrams of the following form:
 <<
@@ -521,6 +494,21 @@ Opaque builtin_strength_reduction.
   eapply match_states_succ; eauto. simpl; auto.
   apply set_reg_lessdef; auto.
 
+  (* Iannot *)
+  rename pc'0 into pc. TransfInstr; intros. 
+  exploit (@eval_annot_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)). 
+    apply REGS. eauto. 
+    eapply annot_strength_reduction_correct_2 with (ae := ae); eauto.
+  intros (vargs' & A & B). 
+  exploit external_call_mem_extends; eauto. 
+  intros (v' & P & Q & R & S & T). 
+  left; econstructor; econstructor; split.
+  eapply exec_Iannot; eauto.
+  eapply eval_annot_args_preserved. eexact symbols_preserved. eauto.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply match_states_succ; eauto.
+
   (* Icond, preserved *)
   rename pc' into pc. TransfInstr.
   set (ac := eval_static_condition cond (aregs ae args)).
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) =>
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index 4d09c5ba..b998c631 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -547,39 +547,77 @@ Proof.
   eapply magree_monotone; eauto. intros; apply B; auto.  
 Qed.
 
-(** Properties of volatile memory accesses *)
-
-(*
-Lemma transf_volatile_load:
-
-  forall s f sp pc e m te r tm nm chunk t v m',
-
-  volatile_load_sem chunk ge (addr :: nil) m t v m' ->
-  Val.lessdef addr taddr ->
+(** Annotation arguments *)
+
+Lemma transfer_annot_arg_sound:
+  forall bc e e' sp m m' a v,
+  eval_annot_arg ge (fun r => e#r) (Vptr sp Int.zero) m a v ->
+  forall ne1 nm1 ne2 nm2,
+  transfer_annot_arg (ne1, nm1) a = (ne2, nm2) ->
+  eagree e e' ne2 ->
+  magree m m' (nlive ge sp nm2) ->
   genv_match bc ge ->
   bc sp = BCstack ->
-  pmatch 
-
-  sound_state prog (State s f (Vptr sp Int.zero) pc e m) ->
-  Val.lessdef e#r te#r ->
-  magree m tm
-        (nlive ge sp
-           (nmem_add nm (aaddr (vanalyze rm f) # pc r) (size_chunk chunk))) ->
-  m' = m /\
-  exists tv, volatile_load_sem chunk ge (te#r :: nil) tm t tv tm /\ Val.lessdef v tv.
+  exists v',
+     eval_annot_arg ge (fun r => e'#r) (Vptr sp Int.zero) m' a  v'
+  /\ Val.lessdef v v'
+  /\ eagree e e' ne1
+  /\ magree m m' (nlive ge sp nm1).
 Proof.
-  intros. inv H2. split; auto. rewrite <- H3 in H0; inv H0. inv H4.
-- (* volatile *)
-  exists (Val.load_result chunk v0); split; auto. 
-  constructor. constructor; auto. 
-- (* not volatile *)
+  induction 1; simpl; intros until nm2; intros TR EA MA GM SPM; inv TR.
+- exists e'#x; intuition auto. constructor. eauto 2 with na. eauto 2 with na.
+- exists (Vint n); intuition auto. constructor.
+- exists (Vlong n); intuition auto. constructor.
+- exists (Vfloat n); intuition auto. constructor.
+- exists (Vsingle n); intuition auto. constructor.
+- simpl in H. exploit magree_load; eauto. 
+  intros. eapply nlive_add; eauto with va. rewrite Int.add_zero_l in H0; auto.
+  intros (v' & A & B).
+  exists v'; intuition auto. constructor; auto.
+  eapply magree_monotone; eauto. intros; eapply incl_nmem_add; eauto. 
+- exists (Vptr sp (Int.add Int.zero ofs)); intuition auto with na. constructor. 
+- unfold Senv.symbol_address in H; simpl in H. 
+  destruct (Genv.find_symbol ge id) as [b|] eqn:FS; simpl in H; try discriminate.
   exploit magree_load; eauto.
-  exploit aaddr_sound; eauto. intros (bc & P & Q & R).
-  intros. eapply nlive_add; eauto.
-  intros (v' & P & Q).
-  exists v'; split. constructor. econstructor; eauto. auto.
+  intros. eapply nlive_add; eauto. constructor. apply GM; auto. 
+  intros (v' & A & B).
+  exists v'; intuition auto.
+  constructor. simpl. unfold Senv.symbol_address; simpl; rewrite FS; auto. 
+  eapply magree_monotone; eauto. intros; eapply incl_nmem_add; eauto.
+- exists (Senv.symbol_address ge id ofs); intuition auto with na. constructor.
+- destruct (transfer_annot_arg (ne1, nm1) hi) as [ne' nm'] eqn:TR.
+  exploit IHeval_annot_arg2; eauto. intros (vlo' & A & B & C & D).
+  exploit IHeval_annot_arg1; eauto. intros (vhi' & P & Q & R & S).
+  exists (Val.longofwords vhi' vlo'); intuition auto.
+  constructor; auto.
+  apply Val.longofwords_lessdef; auto.
+Qed.
+
+Lemma transfer_annot_args_sound:
+  forall e sp m e' m' bc al vl,
+  eval_annot_args ge (fun r => e#r) (Vptr sp Int.zero) m al vl ->
+  forall ne1 nm1 ne2 nm2,
+  List.fold_left transfer_annot_arg al (ne1, nm1) = (ne2, nm2) ->
+  eagree e e' ne2 ->
+  magree m m' (nlive ge sp nm2) ->
+  genv_match bc ge ->
+  bc sp = BCstack ->
+  exists vl',
+     eval_annot_args ge (fun r => e'#r) (Vptr sp Int.zero) m' al vl'
+  /\ Val.lessdef_list vl vl'
+  /\ eagree e e' ne1
+  /\ magree m m' (nlive ge sp nm1).
+Proof.
+Local Opaque transfer_annot_arg.
+  induction 1; simpl; intros.
+- inv H. exists (@nil val); intuition auto. constructor.
+- destruct (transfer_annot_arg (ne1, nm1) a1) as [ne' nm'] eqn:TR.
+  exploit IHlist_forall2; eauto. intros (vs' & A1 & B1 & C1 & D1).
+  exploit transfer_annot_arg_sound; eauto. intros (v1' & A2 & B2 & C2 & D2). 
+  exists (v1' :: vs'); intuition auto. constructor; auto. 
 Qed.
-*)
+
+(** Properties of volatile memory accesses *)
 
 Lemma transf_volatile_store:
   forall v1 v2 v1' v2' m tm chunk sp nm t v m',
@@ -930,6 +968,21 @@ Ltac UseTransfer :=
   apply eagree_update; eauto 3 with na.
   eapply mextends_agree; eauto. 
 
+- (* annot *)
+  TransfInstr; UseTransfer. 
+  destruct (fold_left transfer_annot_arg args (ne, nm)) as [ne1 nm1] eqn:TR; simpl in *.
+  inv SS. exploit transfer_annot_args_sound; eauto. intros (vargs' & A & B & C & D).
+  assert (EC: m' = m /\ external_call ef ge vargs' tm t Vundef tm).
+  { destruct ef; try contradiction. inv H2. split; auto. simpl. constructor. 
+    eapply eventval_list_match_lessdef; eauto. }
+  destruct EC as [EC1 EC2]; subst m'.
+  econstructor; split.
+  eapply exec_Iannot. eauto. auto. 
+  eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved with (ge1 := ge); eauto.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply match_succ_states; eauto. simpl; auto.
+
 - (* conditional *)
   TransfInstr; UseTransfer.
   econstructor; split.
diff --git a/backend/Inlining.v b/backend/Inlining.v
index cd347345..4f17d59c 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -203,6 +203,15 @@ Definition sop (ctx: context) (op: operation) :=
 Definition saddr (ctx: context) (addr: addressing) :=
   shift_stack_addressing (Int.repr ctx.(dstk)) addr.
 
+Fixpoint sannotarg (ctx: context) (a: annot_arg reg) : annot_arg reg :=
+  match a with
+  | AA_base x => AA_base (sreg ctx x)
+  | AA_loadstack chunk ofs => AA_loadstack chunk (Int.add ofs (Int.repr ctx.(dstk)))
+  | AA_addrstack ofs => AA_addrstack (Int.add ofs (Int.repr ctx.(dstk)))
+  | AA_longofwords hi lo => AA_longofwords (sannotarg ctx hi) (sannotarg ctx lo)
+  | _ => a
+  end.
+
 (** The initial context, used to copy the CFG of a toplevel function. *)
 
 Definition initcontext (dpc dreg nreg: positive) (sz: Z) :=
@@ -382,6 +391,9 @@ Definition expand_instr (ctx: context) (pc: node) (i: instruction): mon unit :=
   | Ibuiltin ef args res s =>
       set_instr (spc ctx pc)
                 (Ibuiltin ef (sregs ctx args) (sreg ctx res) (spc ctx s))
+  | Iannot ef args s =>
+      set_instr (spc ctx pc)
+                (Iannot ef (map (sannotarg ctx) args) (spc ctx s))
   | Icond cond args s1 s2 =>
       set_instr (spc ctx pc)
                 (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2))
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index 9b1aec4c..e3c5bf2a 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -400,6 +400,63 @@ Proof.
   eapply function_ptr_translated; eauto.
 Qed.
 
+(** Translation of annotation arguments. *)
+
+Lemma tr_annot_arg:
+  forall F bound ctx rs rs' sp sp' m m',
+  match_globalenvs F bound ->
+  agree_regs F ctx rs rs' ->
+  F sp = Some(sp', ctx.(dstk)) ->
+  Mem.inject F m m' ->
+  forall a v,
+  eval_annot_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v ->
+  exists v', eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (sannotarg ctx a) v'
+          /\ val_inject F v v'.
+Proof.
+  intros until m'; intros MG AG SP MI. induction 1; simpl.
+- exists rs'#(sreg ctx x); split. constructor. eapply agree_val_reg; eauto.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- exploit Mem.loadv_inject; eauto. 
+  instantiate (1 := Vptr sp' (Int.add ofs (Int.repr (dstk ctx)))). 
+  simpl. econstructor; eauto. rewrite Int.add_zero_l; auto.
+  intros (v' & A & B). exists v'; split; auto. constructor. simpl. rewrite Int.add_zero_l; auto. 
+- econstructor; split. constructor. simpl. econstructor; eauto. rewrite ! Int.add_zero_l; auto.
+- assert (val_inject F (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)).
+  { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. 
+    rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
+    inv MG. econstructor. eauto. rewrite Int.add_zero; auto. }
+  exploit Mem.loadv_inject; eauto. intros (v' & A & B).
+  exists v'; eauto with aarg. 
+- econstructor; split. constructor. 
+  unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. 
+  rewrite symbols_preserved. destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
+  inv MG. econstructor. eauto. rewrite Int.add_zero; auto.
+- destruct IHeval_annot_arg1 as (v1 & A1 & B1).
+  destruct IHeval_annot_arg2 as (v2 & A2 & B2).
+  econstructor; split. eauto with aarg. apply val_longofwords_inject; auto. 
+Qed.
+
+Lemma tr_annot_args:
+  forall F bound ctx rs rs' sp sp' m m',
+  match_globalenvs F bound ->
+  agree_regs F ctx rs rs' ->
+  F sp = Some(sp', ctx.(dstk)) ->
+  Mem.inject F m m' ->
+  forall al vl,
+  eval_annot_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl ->
+  exists vl', eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' (map (sannotarg ctx) al) vl'
+          /\ val_list_inject F vl vl'.
+Proof.
+  induction 5; simpl.
+- exists (@nil val); split; constructor.
+- exploit tr_annot_arg; eauto. intros (v1' & A & B).
+  destruct IHlist_forall2 as (vl' & C & D).
+  exists (v1' :: vl'); split; constructor; auto.
+Qed.
+
 (** ** Relating stacks *)
 
 Inductive match_stacks (F: meminj) (m m': mem):
@@ -1030,6 +1087,29 @@ Proof.
   auto. 
   intros. apply SSZ2. eapply external_call_max_perm; eauto. 
 
+(* annot *)
+  exploit tr_funbody_inv; eauto. intros TR; inv TR.
+  exploit match_stacks_inside_globalenvs; eauto. intros [bound MG]. 
+  exploit tr_annot_args; eauto. intros (vargs' & P & Q).
+  exploit external_call_mem_inject; eauto. 
+    eapply match_stacks_inside_globals; eauto.
+  intros [F1 [v1 [m1' [A [B [C [D [E [J K]]]]]]]]].
+  left; econstructor; split.
+  eapply plus_one. eapply exec_Iannot; eauto.
+    eapply external_call_symbols_preserved; eauto. 
+    exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  econstructor.
+    eapply match_stacks_inside_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto.
+    intros; eapply external_call_max_perm; eauto. 
+    intros; eapply external_call_max_perm; eauto. 
+  auto. 
+  eapply agree_regs_incr; eauto. auto. auto. 
+  eapply external_call_valid_block; eauto. 
+  eapply range_private_extcall; eauto. 
+    intros; eapply external_call_max_perm; eauto. 
+  auto. 
+  intros. apply SSZ2. eapply external_call_max_perm; eauto. 
+
 (* cond *)
   exploit tr_funbody_inv; eauto. intros TR; inv TR.
   assert (eval_condition cond rs'##(sregs ctx args) m' = Some b).
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index b5948a22..f7e6c317 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -316,6 +316,9 @@ Inductive tr_instr: context -> node -> instruction -> code -> Prop :=
       Ple res ctx.(mreg) ->
       c!(spc ctx pc) = Some (Ibuiltin ef (sregs ctx args) (sreg ctx res) (spc ctx s)) ->
       tr_instr ctx pc (Ibuiltin ef args res s) c
+  | tr_annot: forall ctx pc c ef args s,
+      c!(spc ctx pc) = Some (Iannot ef (map (sannotarg ctx) args) (spc ctx s)) ->
+      tr_instr ctx pc (Iannot ef args s) c
   | tr_cond: forall ctx pc cond args s1 s2 c,
       c!(spc ctx pc) = Some (Icond cond (sregs ctx args) (spc ctx s1) (spc ctx s2)) ->
       tr_instr ctx pc (Icond cond args s1 s2) c
diff --git a/backend/LTL.v b/backend/LTL.v
index dd79c8e3..8c2749a7 100644
--- a/backend/LTL.v
+++ b/backend/LTL.v
@@ -45,7 +45,7 @@ Inductive instruction: Type :=
   | Lcall (sg: signature) (ros: mreg + ident)
   | Ltailcall (sg: signature) (ros: mreg + ident)
   | Lbuiltin (ef: external_function) (args: list mreg) (res: list mreg)
-  | Lannot (ef: external_function) (args: list loc)
+  | Lannot (ef: external_function) (args: list (annot_arg loc))
   | Lbranch (s: node)
   | Lcond (cond: condition) (args: list mreg) (s1 s2: node)
   | Ljumptable (arg: mreg) (tbl: list node)
@@ -244,8 +244,9 @@ Inductive step: state -> trace -> state -> Prop :=
       rs' = Locmap.setlist (map R res) vl (undef_regs (destroyed_by_builtin ef) rs) ->
       step (Block s f sp (Lbuiltin ef args res :: bb) rs m)
          t (Block s f sp bb rs' m')
-  | exec_Lannot: forall s f sp ef args bb rs m t vl m',
-      external_call' ef ge (map rs args) m t vl m' ->
+  | exec_Lannot: forall s f sp ef args bb rs vl m t v' m',
+      eval_annot_args ge rs sp m args vl ->
+      external_call ef ge vl m t v' m' ->
       step (Block s f sp (Lannot ef args :: bb) rs m)
          t (Block s f sp bb rs m')
   | exec_Lbranch: forall s f sp pc bb rs m,
diff --git a/backend/Linear.v b/backend/Linear.v
index 56d1eb99..5d1fc0d8 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -42,7 +42,7 @@ Inductive instruction: Type :=
   | Lcall: signature -> mreg + ident -> instruction
   | Ltailcall: signature -> mreg + ident -> instruction
   | Lbuiltin: external_function -> list mreg -> list mreg -> instruction
-  | Lannot: external_function -> list loc -> instruction
+  | Lannot: external_function -> list (annot_arg loc) -> instruction
   | Llabel: label -> instruction
   | Lgoto: label -> instruction
   | Lcond: condition -> list mreg -> label -> instruction
@@ -204,8 +204,9 @@ Inductive step: state -> trace -> state -> Prop :=
       step (State s f sp (Lbuiltin ef args res :: b) rs m)
          t (State s f sp b rs' m')
   | exec_Lannot:
-      forall s f sp rs m ef args b t v m',
-      external_call' ef ge (map rs args) m t v m' ->
+      forall s f sp rs m ef args vl b t v m',
+      eval_annot_args ge rs sp m args vl ->
+      external_call ef ge vl m t v m' ->
       step (State s f sp (Lannot ef args :: b) rs m)
          t (State s f sp b rs m')
   | exec_Llabel:
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v
index 63fa6565..08bcd3f3 100644
--- a/backend/Linearizeproof.v
+++ b/backend/Linearizeproof.v
@@ -651,7 +651,8 @@ Proof.
   (* Lannot *)
   left; econstructor; split. simpl.
   apply plus_one. eapply exec_Lannot; eauto.
-  eapply external_call_symbols_preserved'; eauto.
+  eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   econstructor; eauto.
 
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index ccf17e1e..c093b62d 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -76,7 +76,7 @@ Definition wt_instr (i: instruction) : bool :=
   | Lbuiltin ef args res =>
       subtype_list (proj_sig_res' (ef_sig ef)) (map mreg_type res) 
   | Lannot ef args =>
-      forallb loc_valid args
+      forallb loc_valid (params_of_annot_args args)
   | _ =>
       true
   end.
@@ -365,7 +365,7 @@ Qed.
 Lemma wt_state_annot:
   forall s f sp ef args c rs m,
   wt_state (State s f sp (Lannot ef args :: c) rs m) ->
-  forallb (loc_valid f) args = true.
+  forallb (loc_valid f) (params_of_annot_args args) = true.
 Proof.
   intros. inv H. simpl in WTC; InvBooleans. auto. 
 Qed.
diff --git a/backend/Liveness.v b/backend/Liveness.v
index 3a5bde97..ce1a798a 100644
--- a/backend/Liveness.v
+++ b/backend/Liveness.v
@@ -93,6 +93,8 @@ Definition transfer
           reg_list_live args (reg_sum_live ros Regset.empty)
       | Ibuiltin ef args res s =>
           reg_list_live args (reg_dead res after)
+      | Iannot ef args s =>
+          reg_list_live (params_of_annot_args args) after
       | Icond cond args ifso ifnot =>
           reg_list_live args after
       | Ijumptable arg tbl =>
diff --git a/backend/Mach.v b/backend/Mach.v
index ff72a828..fe00d42d 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -61,16 +61,12 @@ Inductive instruction: Type :=
   | Mcall: signature -> mreg + ident -> instruction
   | Mtailcall: signature -> mreg + ident -> instruction
   | Mbuiltin: external_function -> list mreg -> list mreg -> instruction
-  | Mannot: external_function -> list annot_param -> instruction
+  | Mannot: external_function -> list (annot_arg mreg) -> instruction
   | Mlabel: label -> instruction
   | Mgoto: label -> instruction
   | Mcond: condition -> list mreg -> label -> instruction
   | Mjumptable: mreg -> list label -> instruction
-  | Mreturn: instruction
-
-with annot_param: Type :=
-  | APreg: mreg -> annot_param
-  | APstack: memory_chunk -> Z -> annot_param.
+  | Mreturn: instruction.
 
 Definition code := list instruction.
 
@@ -225,19 +221,6 @@ Definition extcall_arguments
     (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop :=
   list_forall2 (extcall_arg rs m sp) (loc_arguments sg) args.
 
-(** Extract the values of the arguments to an annotation. *)
-
-Inductive annot_arg: regset -> mem -> val -> annot_param -> val -> Prop :=
-  | annot_arg_reg: forall rs m sp r,
-      annot_arg rs m sp (APreg r) (rs r)
-  | annot_arg_stack: forall rs m stk base chunk ofs v,
-      Mem.load chunk m stk (Int.unsigned base + ofs) = Some v ->
-      annot_arg rs m (Vptr stk base) (APstack chunk ofs) v.
-
-Definition annot_arguments
-   (rs: regset) (m: mem) (sp: val) (params: list annot_param) (args: list val) : Prop :=
-  list_forall2 (annot_arg rs m sp) params args.
-
 (** Mach execution states. *)
 
 (** Mach execution states. *)
@@ -352,8 +335,8 @@ Inductive step: state -> trace -> state -> Prop :=
          t (State s f sp b rs' m')
   | exec_Mannot:
       forall s f sp rs m ef args b vargs t v m',
-      annot_arguments rs m sp args vargs ->
-      external_call' ef ge vargs m t v m' ->
+      eval_annot_args ge rs sp m args vargs ->
+      external_call ef ge vargs m t v m' ->
       step (State s f sp (Mannot ef args :: b) rs m)
          t (State s f sp b rs m')
   | exec_Mgoto:
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 5c8347cb..ce2275cf 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -74,6 +74,10 @@ let print_instruction pp (pc, i) =
       fprintf pp "%a = %s(%a)\n"
         reg res (name_of_external ef) regs args;
       print_succ pp s (pc - 1)
+  | Iannot(ef, args, s) ->
+      fprintf pp "%s(%a)\n"
+        (name_of_external ef) (print_annot_args reg) args;
+      print_succ pp s (pc - 1)
   | Icond(cond, args, s1, s2) ->
       fprintf pp "if (%a) goto %d else goto %d\n"
         (PrintOp.print_condition reg) (cond, args)
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
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 26f51e3f..8b11022b 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -455,6 +455,56 @@ with transl_condexpr (map: mapping) (a: condexpr) (ntrue nfalse: node)
          transl_expr map b r nc
   end.
 
+(** Translation of arguments to annotations. *)
+
+Fixpoint convert_annot_arg (map: mapping) (a: annot_arg expr) : mon (annot_arg reg) :=
+  match a with
+  | AA_base a => do rd <- alloc_reg map a; ret (AA_base rd)
+  | AA_int n => ret (AA_int n)
+  | AA_long n => ret (AA_long n)
+  | AA_float n => ret (AA_float n)
+  | AA_single n => ret (AA_single n)
+  | AA_loadstack chunk ofs => ret (AA_loadstack chunk ofs)
+  | AA_addrstack ofs => ret (AA_addrstack ofs)
+  | AA_loadglobal chunk id ofs => ret (AA_loadglobal chunk id ofs)
+  | AA_addrglobal id ofs => ret (AA_addrglobal id ofs)
+  | AA_longofwords hi lo =>
+      do hi' <- convert_annot_arg map hi;
+      do lo' <- convert_annot_arg map lo;
+      ret (AA_longofwords hi' lo')
+  end.
+
+Fixpoint convert_annot_args (map: mapping) (al: list (annot_arg expr)) : mon (list (annot_arg reg)) :=
+  match al with
+  | nil => ret nil
+  | a1 :: al =>
+      do a1' <- convert_annot_arg map a1;
+      do al' <- convert_annot_args map al;
+      ret (a1' :: al')
+  end.
+
+Fixpoint transl_annot_arg
+             (map: mapping) (a: annot_arg expr) (d: annot_arg reg) (nd: node) 
+             : mon node :=
+  match a, d with
+  | AA_base a, AA_base r => transl_expr map a r nd
+  | AA_longofwords hi lo, AA_longofwords hi' lo' =>
+      do no <- transl_annot_arg map lo lo' nd;
+      transl_annot_arg map hi hi' no
+  | _, _ => ret nd
+  end.
+
+Fixpoint transl_annot_args
+          (map: mapping) (al: list (annot_arg expr)) (dl: list (annot_arg reg)) (nd: node)
+          : mon node :=
+  match al, dl with
+  | a1 :: al, d1 :: dl =>
+      do no <- transl_annot_args map al dl nd;
+      transl_annot_arg map a1 d1 no
+  | _, _ =>
+      ret nd
+  end.
+
 (** Auxiliary for translating exit expressions. *)
 
 Definition transl_exit (nexits: list node) (n: nat) : mon node :=
@@ -558,6 +608,10 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node)
       do r <- alloc_optreg map optid;
       do n1 <- add_instr (Ibuiltin ef rargs r nd);
          transl_exprlist map al rargs n1
+  | Sannot ef al =>
+      do dl <- convert_annot_args map al;
+      do n1 <- add_instr (Iannot ef dl nd);
+         transl_annot_args map al dl n1
   | Sseq s1 s2 =>
       do ns <- transl_stmt map s2 nd nexits ngoto nret rret;
       transl_stmt map s1 ns nexits ngoto nret rret
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 8acce510..db55c8e8 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -972,6 +972,145 @@ Proof.
   auto.
 Qed.
 
+(** Annotation arguments. *)
+
+(*
+Definition transl_annot_arg_prop (a: annot_arg expr) (v: val): Prop :=
+  forall tm cs f map pr ns nd a' rs
+    (MWF: map_wf map)
+    (TR: tr_annot_arg f.(fn_code) map pr a ns nd a')
+    (ME: match_env map e nil rs)
+    (EXT: Mem.extends m tm),
+  exists rs', exists tm', exists v',
+     star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm')
+  /\ match_env map e nil rs'
+  /\ Events.eval_annot_arg tge (fun r => rs'#r) sp tm' a' v'
+  /\ Val.lessdef v v'
+  /\ (forall r, In r pr -> rs'#r = rs#r)
+  /\ Mem.extends m tm'.
+
+Theorem transl_annot_arg_correct:
+  forall a v,
+  eval_annot_arg ge sp e m a v ->
+  transl_annot_arg_prop a v.
+Proof.
+  induction 1; red; intros; inv TR.
+- exploit transl_expr_correct; eauto. intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1).
+  exists rs1, tm1, rs1#r; intuition eauto. constructor.
+- exists rs, tm, (Vint n); intuition auto using star_refl with aarg.
+- exists rs, tm, (Vlong n); intuition auto using star_refl with aarg.
+- exists rs, tm, (Vfloat n); intuition auto using star_refl with aarg.
+- exists rs, tm, (Vsingle n); intuition auto using star_refl with aarg.
+- exploit Mem.loadv_extends; eauto. intros (v' & P & Q).
+  exists rs, tm, v'; intuition auto using star_refl with aarg.
+- exists rs, tm, (Val.add sp (Vint ofs)); intuition auto using star_refl with aarg.
+- exploit Mem.loadv_extends; eauto. intros (v' & P & Q).
+  replace (Genv.symbol_address ge id ofs) 
+     with (Senv.symbol_address tge id ofs) in P.
+  exists rs, tm, v'; intuition auto using star_refl with aarg.
+  unfold Genv.symbol_address, Senv.symbol_address. simpl.
+  rewrite symbols_preserved; auto.
+- exists rs, tm, (Senv.symbol_address tge id ofs); intuition auto using star_refl with aarg.
+  unfold Genv.symbol_address, Senv.symbol_address. simpl.
+  rewrite symbols_preserved; auto.
+- inv H5. inv H9. simpl in H5. 
+  exploit transl_expr_correct. eexact H. eauto. eauto. eauto. eauto. 
+  intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1).
+  exploit transl_expr_correct. eexact H0. eauto. eauto. eauto. eauto. 
+  intros (rs2 & tm2 & A2 & B2 & C2 & D2 & E2).
+  exists rs2, tm2, (Val.longofwords rs2#r rs2#r0); intuition auto.
+  eapply star_trans; eauto. 
+  constructor. constructor. constructor. 
+  rewrite (D2 r) by auto with coqlib. apply Val.longofwords_lessdef; auto.
+  transitivity rs1#r1; auto with coqlib.
+Qed.
+*)
+
+Definition transl_annot_args_prop (l: list (annot_arg expr)) (vl: list val): Prop :=
+  forall tm cs f map pr ns nd l' rs
+    (MWF: map_wf map)
+    (TR: tr_annot_args f.(fn_code) map pr l ns nd l')
+    (ME: match_env map e nil rs)
+    (EXT: Mem.extends m tm),
+  exists rs', exists tm', exists vl',
+     star step tge (State cs f sp ns rs tm) E0 (State cs f sp nd rs' tm')
+  /\ match_env map e nil rs'
+  /\ eval_annot_args tge (fun r => rs'#r) sp tm' l' vl'
+  /\ Val.lessdef_list vl vl'
+  /\ (forall r, In r pr -> rs'#r = rs#r)
+  /\ Mem.extends m tm'.
+
+Theorem transl_annot_args_correct:
+  forall l vl,
+  list_forall2 (eval_annot_arg ge sp e m) l vl ->
+  transl_annot_args_prop l vl.
+Proof.
+  induction 1; red; intros.
+- inv TR. exists rs, tm, (@nil val). 
+  split. constructor.
+  split. auto.
+  split. constructor.
+  split. constructor.
+  split. auto.
+  auto.
+- inv TR. inv H; inv H5. 
+  + exploit transl_expr_correct; eauto.
+    intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1).
+    exploit (IHlist_forall2 tm1 cs); eauto. 
+    intros (rs2 & tm2 & vl2 & A2 & B2 & C2 & D2 & E2 & F2). simpl in E2.
+    exists rs2, tm2, (rs2#r :: vl2); intuition auto.
+    eapply star_trans; eauto.
+    constructor; auto. constructor.
+    rewrite E2; auto.
+    transitivity rs1#r0; auto.
+  + exploit (IHlist_forall2 tm cs); eauto.
+    intros (rs' & tm' & vl' & A & B & C & D & E & F).
+    exists rs', tm', (Vint n :: vl'); simpl; intuition auto. constructor; auto with aarg.
+  + exploit (IHlist_forall2 tm cs); eauto.
+    intros (rs' & tm' & vl' & A & B & C & D & E & F).
+    exists rs', tm', (Vlong n :: vl'); simpl; intuition auto. constructor; auto with aarg.
+  + exploit (IHlist_forall2 tm cs); eauto.
+    intros (rs' & tm' & vl' & A & B & C & D & E & F).
+    exists rs', tm', (Vfloat n :: vl'); simpl; intuition auto. constructor; auto with aarg.
+  + exploit (IHlist_forall2 tm cs); eauto.
+    intros (rs' & tm' & vl' & A & B & C & D & E & F).
+    exists rs', tm', (Vsingle n :: vl'); simpl; intuition auto. constructor; auto with aarg.
+  + exploit (IHlist_forall2 tm cs); eauto.
+    intros (rs' & tm' & vl' & A & B & C & D & E & F).
+    exploit Mem.loadv_extends; eauto. intros (v1' & P & Q).
+    exists rs', tm', (v1' :: vl'); simpl; intuition auto. constructor; eauto with aarg. 
+  + exploit (IHlist_forall2 tm cs); eauto.
+    intros (rs' & tm' & vl' & A & B & C & D & E & F).
+    exists rs', tm', (Val.add sp (Vint ofs) :: vl'); simpl; intuition auto. constructor; auto with aarg.
+  + exploit (IHlist_forall2 tm cs); eauto.
+    intros (rs' & tm' & vl' & A & B & C & D & E & F).
+    exploit Mem.loadv_extends; eauto. intros (v1' & P & Q).
+    replace (Genv.symbol_address ge id ofs) 
+       with (Senv.symbol_address tge id ofs) in P.
+    exists rs', tm', (v1' :: vl'); simpl; intuition auto. constructor; auto with aarg. 
+    unfold Genv.symbol_address, Senv.symbol_address. simpl.
+    rewrite symbols_preserved; auto. 
+  + exploit (IHlist_forall2 tm cs); eauto.
+    intros (rs' & tm' & vl' & A & B & C & D & E & F).
+    exists rs', tm', (Genv.symbol_address tge id ofs :: vl'); simpl; intuition auto.
+    constructor; auto with aarg. constructor. 
+    unfold Genv.symbol_address. rewrite symbols_preserved; auto.
+  + inv H7. inv H12. 
+    exploit transl_expr_correct. eexact H1. eauto. eauto. eauto. eauto. 
+    intros (rs1 & tm1 & A1 & B1 & C1 & D1 & E1).
+    exploit transl_expr_correct. eexact H2. eauto. eauto. eauto. eexact E1.  
+    intros (rs2 & tm2 & A2 & B2 & C2 & D2 & E2). simpl in D2.
+    exploit (IHlist_forall2 tm2 cs); eauto. 
+    intros (rs3 & tm3 & vl3 & A3 & B3 & C3 & D3 & E3 & F3). simpl in E3.
+    exists rs3, tm3, (Val.longofwords rs3#r rs3#r0 :: vl3); intuition auto.
+    eapply star_trans; eauto. eapply star_trans; eauto.  auto.
+    constructor; auto with aarg. constructor. constructor. constructor.  
+    constructor; auto. apply Val.longofwords_lessdef. 
+    rewrite E3, D2; auto.
+    rewrite E3; auto. 
+    transitivity rs1#r1; auto. transitivity rs2#r1; auto.
+Qed.
+
 End CORRECTNESS_EXPR.
 
 (** ** Measure over CminorSel states *)
@@ -1304,6 +1443,19 @@ Proof.
   econstructor; eauto. constructor.
   eapply match_env_update_dest; eauto.
 
+  (* annot *)
+  inv TS. 
+  exploit transl_annot_args_correct; eauto. 
+  intros [rs' [tm' [vl' [E [F [G [J [K L]]]]]]]].
+  edestruct external_call_mem_extends as [tv [tm'' [A [B [C D]]]]]; eauto.
+  econstructor; split.
+  left. eapply plus_right. eexact E.
+  eapply exec_Iannot; eauto. 
+  eapply external_call_symbols_preserved. eauto.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  traceEq. 
+  econstructor; eauto. constructor.
+ 
   (* seq *)
   inv TS. 
   econstructor; split.
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 32f35bb4..e78c6c59 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -220,6 +220,13 @@ Proof.
   intros; red; intros. elim H1; intro. subst r1; auto. auto.
 Qed.
 
+Lemma regs_valid_app:
+  forall rl1 rl2 s,
+  regs_valid rl1 s -> regs_valid rl2 s -> regs_valid (rl1 ++ rl2) s.
+Proof.
+  intros; red; intros. apply in_app_iff in H1. destruct H1; auto. 
+Qed.
+
 Lemma regs_valid_incr:
   forall s1 s2 rl, state_incr s1 s2 -> regs_valid rl s1 -> regs_valid rl s2.
 Proof.
@@ -800,6 +807,49 @@ Inductive tr_exitexpr (c: code):
       tr_exitexpr c (add_letvar map r) b n1 nexits ->
       tr_exitexpr c map (XElet a b) ns nexits.
 
+(** Translation of arguments to annotations.
+    [tr_annot_args c map pr al ns nd al'] holds if the graph [c],
+    starting at node [ns], contains instructions that evaluate the
+    expressions contained in the built-in argument list [al],
+    then terminate on node [nd].  When [nd] is reached, the registers
+    contained in [al'] hold the values of the corresponding expressions
+    in [al].  Registers in [pr] are not modified. *)
+
+Inductive tr_annot_arg (c: code):
+      mapping -> list reg -> annot_arg expr -> node -> node -> annot_arg reg -> Prop :=
+  | tr_AA_base: forall map pr a ns nd r,
+      tr_expr c map pr a ns nd r None ->
+      tr_annot_arg c map pr (AA_base a) ns nd (AA_base r)
+  | tr_AA_int: forall map pr i n,
+      tr_annot_arg c map pr (AA_int i) n n (AA_int i)
+  | tr_AA_long: forall map pr i n,
+      tr_annot_arg c map pr (AA_long i) n n (AA_long i)
+  | tr_AA_float: forall map pr i n,
+      tr_annot_arg c map pr (AA_float i) n n (AA_float i)
+  | tr_AA_single: forall map pr i n,
+      tr_annot_arg c map pr (AA_single i) n n (AA_single i)
+  | tr_AA_loadstack: forall map pr chunk ofs n,
+      tr_annot_arg c map pr (AA_loadstack chunk ofs) n n (AA_loadstack chunk ofs)
+  | tr_AA_addrstack: forall map pr ofs n,
+      tr_annot_arg c map pr (AA_addrstack ofs) n n (AA_addrstack ofs)
+  | tr_AA_loadglobal: forall map pr chunk id ofs n,
+      tr_annot_arg c map pr (AA_loadglobal chunk id ofs) n n (AA_loadglobal chunk id ofs)
+  | tr_AA_addrglobal: forall map pr id ofs n,
+      tr_annot_arg c map pr (AA_addrglobal id ofs) n n (AA_addrglobal id ofs)
+  | tr_AA_longofwords: forall map pr hi lo ns nd n1 hi' lo',
+      tr_annot_arg c map pr hi ns n1 hi' ->
+      tr_annot_arg c map (params_of_annot_arg hi' ++ pr) lo n1 nd lo' ->
+      tr_annot_arg c map pr (AA_longofwords hi lo) ns nd (AA_longofwords hi' lo').
+
+Inductive tr_annot_args (c: code):
+      mapping -> list reg -> list (annot_arg expr) -> node -> node -> list (annot_arg reg) -> Prop :=
+  | tr_AA_nil: forall map pr n,
+      tr_annot_args c map pr nil n n nil
+  | tr_AA_cons: forall map pr a ns n1 a' al nd al',
+      tr_annot_arg c map pr a ns n1 a' ->
+      tr_annot_args c map (params_of_annot_arg a' ++ pr) al n1 nd al' ->
+      tr_annot_args c map pr (a :: al) ns nd (a' :: al').
+
 (** [tr_stmt c map stmt ns ncont nexits nret rret] holds if the graph [c],
   starting at node [ns], contains instructions that perform the Cminor
   statement [stmt].   These instructions branch to node [ncont] if
@@ -847,6 +897,10 @@ Inductive tr_stmt (c: code) (map: mapping):
      c!n1 = Some (Ibuiltin ef rargs rd nd) ->
      reg_map_ok map rd optid ->
      tr_stmt c map (Sbuiltin optid ef al) ns nd nexits ngoto nret rret
+  | tr_Sannot: forall ef al ns nd nexits ngoto nret rret n1 al',
+     tr_annot_args c map nil al ns n1 al' ->
+     c!n1 = Some (Iannot ef al' nd) ->
+     tr_stmt c map (Sannot ef al) ns nd nexits ngoto nret rret
   | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n,
      tr_stmt c map s2 n nd nexits ngoto nret rret ->
      tr_stmt c map s1 ns n nexits ngoto nret rret ->
@@ -1136,6 +1190,28 @@ Proof.
   induction 1; econstructor; eauto with rtlg.
 Qed.
 
+Lemma tr_annot_arg_incr:
+  forall s1 s2, state_incr s1 s2 ->
+  forall map pr a ns nd a',
+  tr_annot_arg s1.(st_code) map pr a ns nd a' ->
+  tr_annot_arg s2.(st_code) map pr a ns nd a'.
+Proof.
+  intros s1 s2 EXT.
+  generalize tr_expr_incr; intros I1.
+  induction 1; econstructor; eauto with rtlg.
+Qed.
+
+Lemma tr_annot_args_incr:
+  forall s1 s2, state_incr s1 s2 ->
+  forall map pr al ns nd al',
+  tr_annot_args s1.(st_code) map pr al ns nd al' ->
+  tr_annot_args s2.(st_code) map pr al ns nd al'.
+Proof.
+  intros s1 s2 EXT.
+  generalize tr_annot_arg_incr; intros I1.
+  induction 1; econstructor; eauto with rtlg.
+Qed.
+
 Lemma tr_stmt_incr:
   forall s1 s2, state_incr s1 s2 ->
   forall map s ns nd nexits ngoto nret rret,
@@ -1143,7 +1219,7 @@ Lemma tr_stmt_incr:
   tr_stmt s2.(st_code) map s ns nd nexits ngoto nret rret.
 Proof.
   intros s1 s2 EXT.
-  generalize tr_expr_incr tr_condition_incr tr_exprlist_incr tr_exitexpr_incr; intros I1 I2 I3 I4.
+  generalize tr_expr_incr tr_condition_incr tr_exprlist_incr tr_exitexpr_incr tr_annot_args_incr; intros I1 I2 I3 I4 I5.
   pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT).
   induction 1; econstructor; eauto.
 Qed.
@@ -1196,7 +1272,143 @@ Proof.
   apply tr_exitexpr_incr with s1; auto. eapply IHa; eauto with rtlg.
   apply add_letvar_valid; eauto with rtlg.
 Qed.
- 
+
+Lemma convert_annot_arg_valid:
+  forall map a s1 a' s2 i,
+  convert_annot_arg map a s1 = OK a' s2 i ->
+  map_valid map s1 ->
+  regs_valid (params_of_annot_arg a') s2.
+Proof.
+  induction a; simpl; intros; monadInv H; simpl; auto using regs_valid_nil.
+- apply regs_valid_cons. eauto with rtlg. apply regs_valid_nil.
+- apply regs_valid_app. eauto with rtlg. eapply IHa2; eauto with rtlg. 
+Qed.
+
+Lemma convert_annot_args_valid:
+  forall map l s1 l' s2 i,
+  convert_annot_args map l s1 = OK l' s2 i ->
+  map_valid map s1 ->
+  regs_valid (params_of_annot_args l') s2.
+Proof.
+  induction l; simpl; intros.
+- monadInv H. apply regs_valid_nil. 
+- monadInv H. simpl. apply regs_valid_app.
+  + apply regs_valid_incr with s; auto. eapply convert_annot_arg_valid; eauto.
+  + eapply IHl; eauto with rtlg.
+Qed.
+
+Inductive target_annot_arg_ok (map: mapping): list reg -> annot_arg expr -> annot_arg reg -> Prop :=
+  | taa_AA_base: forall pr a r,
+      target_reg_ok map pr a r ->
+      target_annot_arg_ok map pr (AA_base a) (AA_base r)
+  | taa_AA_int: forall pr i,
+      target_annot_arg_ok map pr (AA_int i) (AA_int i)
+  | taa_AA_long: forall pr i,
+      target_annot_arg_ok map pr (AA_long i) (AA_long i)
+  | taa_AA_float: forall pr i,
+      target_annot_arg_ok map pr (AA_float i) (AA_float i)
+  | taa_AA_single: forall pr i,
+      target_annot_arg_ok map pr (AA_single i) (AA_single i)
+  | taa_AA_loadstack: forall pr chunk ofs,
+      target_annot_arg_ok map pr (AA_loadstack chunk ofs) (AA_loadstack chunk ofs)
+  | taa_AA_addrstack: forall pr ofs,
+      target_annot_arg_ok map pr (AA_addrstack ofs) (AA_addrstack ofs)
+  | taa_AA_loadglobal: forall pr chunk id ofs,
+      target_annot_arg_ok map pr (AA_loadglobal chunk id ofs) (AA_loadglobal chunk id ofs)
+  | taa_AA_addrglobal: forall pr id ofs,
+      target_annot_arg_ok map pr (AA_addrglobal id ofs) (AA_addrglobal id ofs)
+  | taa_AA_longofwords: forall pr hi lo hi' lo',
+      target_annot_arg_ok map pr hi hi' ->
+      target_annot_arg_ok map (params_of_annot_arg hi' ++ pr) lo lo' ->
+      target_annot_arg_ok map pr (AA_longofwords hi lo) (AA_longofwords hi' lo').
+
+Lemma convert_annot_arg_ok:
+  forall map a pr s1 a' s2 i,
+  map_valid map s1 ->
+  regs_valid pr s1 ->
+  convert_annot_arg map a s1 = OK a' s2 i ->
+  target_annot_arg_ok map pr a a'.
+Proof.
+  induction a; simpl; intros until i; intros MAP PR CVT; monadInv CVT; try (now constructor).
+- constructor. eauto with rtlg.
+- constructor. 
+  eapply IHa1 with (s1 := s1); eauto. 
+  eapply IHa2 with (s1 := s); eauto with rtlg. 
+  apply regs_valid_app; eauto using convert_annot_arg_valid with rtlg.
+Qed.
+
+Inductive target_annot_args_ok (map: mapping): list reg -> list (annot_arg expr) -> list (annot_arg reg) -> Prop :=
+  | taa_AA_nil: forall pr,
+      target_annot_args_ok map pr nil nil
+  | taa_AA_cons: forall pr a a' l l',
+      target_annot_arg_ok map pr a a' ->
+      target_annot_args_ok map (params_of_annot_arg a' ++ pr) l l' ->
+      target_annot_args_ok map pr (a :: l) (a' :: l').
+
+Lemma convert_annot_args_ok:
+  forall map l pr s1 l' s2 i,
+  map_valid map s1 ->
+  regs_valid pr s1 ->
+  convert_annot_args map l s1 = OK l' s2 i ->
+  target_annot_args_ok map pr l l'.
+Proof.
+  induction l; simpl; intros until i; intros MAP PR CVT; monadInv CVT.
+- constructor.
+- constructor.
+  eapply convert_annot_arg_ok with (s1 := s1); eauto. 
+  eapply IHl with (s1 := s); eauto with rtlg.
+  apply regs_valid_app; eauto using convert_annot_arg_valid with rtlg.
+Qed.
+
+Lemma transl_annot_arg_charact:
+  forall map a a' nd s ns s' i pr
+     (TR: transl_annot_arg map a a' nd s = OK ns s' i) 
+     (WF: map_valid map s)
+     (OK: target_annot_arg_ok map pr a a')
+     (VALID: regs_valid pr s)
+     (VALID2: regs_valid (params_of_annot_arg a') s),
+  tr_annot_arg s'.(st_code) map pr a ns nd a'.
+Proof.
+  induction a; intros; inv OK; simpl in TR; try (monadInv TR); simpl in VALID2.
+- assert (reg_valid r s) by auto with coqlib.
+  constructor. eapply transl_expr_charact; eauto with rtlg. 
+- constructor.
+- constructor.
+- constructor.
+- constructor.
+- constructor.
+- constructor.
+- constructor.
+- constructor.
+- econstructor. 
+  eapply IHa1; eauto with rtlg.
+  red; intros. apply reg_valid_incr with s; auto using in_or_app.
+  apply tr_annot_arg_incr with s0; auto. 
+  eapply IHa2; eauto with rtlg.
+  apply regs_valid_app; auto. red; intros; auto using in_or_app.
+  red; intros; auto using in_or_app.
+Qed.
+
+Lemma transl_annot_args_charact:
+  forall map al al' nd s ns s' i pr
+     (TR: transl_annot_args map al al' nd s = OK ns s' i) 
+     (WF: map_valid map s)
+     (OK: target_annot_args_ok map pr al al')
+     (VALID: regs_valid pr s)
+     (VALID2: regs_valid (params_of_annot_args al') s),
+  tr_annot_args s'.(st_code) map pr al ns nd al'.
+Proof.
+  induction al as [|a al]; intros; inv OK; monadInv TR; simpl in VALID2.
+- constructor.
+- econstructor. 
+  eapply transl_annot_arg_charact; eauto with rtlg.
+  red; intros. apply reg_valid_incr with s; auto using in_or_app.
+  apply tr_annot_args_incr with s0; auto. 
+  eapply IHal; eauto with rtlg.
+  apply regs_valid_app; auto. red; intros; auto using in_or_app.
+  red; intros; auto using in_or_app.
+Qed.
+
 Lemma transl_stmt_charact:
   forall map stmt nd nexits ngoto nret rret s ns s' INCR
     (TR: transl_stmt map stmt nd nexits ngoto nret rret s = OK ns s' INCR)
@@ -1250,6 +1462,11 @@ Proof.
   econstructor; eauto 4 with rtlg.
   eapply transl_exprlist_charact; eauto 3 with rtlg.
   eapply alloc_optreg_map_ok with (s1 := s0); eauto with rtlg.
+  (* Sannot *)
+  econstructor; eauto 4 with rtlg. 
+  eapply transl_annot_args_charact; eauto 3 with rtlg.
+  eapply convert_annot_args_ok; eauto 3 with rtlg.
+  apply regs_valid_incr with s0; auto. eapply convert_annot_args_valid; eauto. 
   (* Sseq *)
   econstructor. 
   apply tr_stmt_incr with s0; auto. 
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 5042c775..8961fc0b 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -65,6 +65,20 @@ Variable env: regenv.
 Definition valid_successor (s: node) : Prop :=
   exists i, funct.(fn_code)!s = Some i.
 
+Definition type_of_annot_arg (a: annot_arg reg) : typ :=
+  match a with
+  | AA_base r => env r
+  | AA_int _ => Tint
+  | AA_long _ => Tlong
+  | AA_float _ => Tfloat
+  | AA_single _ => Tsingle
+  | AA_loadstack chunk ofs => type_of_chunk chunk
+  | AA_addrstack ofs => Tint
+  | AA_loadglobal chunk id ofs => type_of_chunk chunk
+  | AA_addrglobal id ofs => Tint
+  | AA_longofwords hi lo => Tlong
+  end.
+
 Inductive wt_instr : instruction -> Prop :=
   | wt_Inop:
       forall s,
@@ -114,6 +128,11 @@ Inductive wt_instr : instruction -> Prop :=
       env res = proj_sig_res (ef_sig ef) ->
       valid_successor s ->
       wt_instr (Ibuiltin ef args res s)
+  | wt_Iannot:
+      forall ef args s,
+      map type_of_annot_arg args = (ef_sig ef).(sig_args) ->
+      valid_successor s ->
+      wt_instr (Iannot ef args s)
   | wt_Icond:
       forall cond args s1 s2,
       map env args = type_of_condition cond ->
@@ -211,6 +230,32 @@ Definition type_ros (e: S.typenv) (ros: reg + ident) : res S.typenv :=
 Definition is_move (op: operation) : bool :=
   match op with Omove => true | _ => false end.
 
+Definition type_expect (e: S.typenv) (t1 t2: typ) : res S.typenv :=
+  if typ_eq t1 t2 then OK e else Error(msg "unexpected type").
+
+Definition type_annot_arg (e: S.typenv) (a: annot_arg reg) (ty: typ) : res S.typenv :=
+  match a with
+  | AA_base r => S.set e r ty
+  | AA_int _ => type_expect e ty Tint
+  | AA_long _ => type_expect e ty Tlong
+  | AA_float _ => type_expect e ty Tfloat
+  | AA_single _ => type_expect e ty Tsingle
+  | AA_loadstack chunk ofs => type_expect e ty (type_of_chunk chunk)
+  | AA_addrstack ofs => type_expect e ty Tint
+  | AA_loadglobal chunk id ofs => type_expect e ty (type_of_chunk chunk)
+  | AA_addrglobal id ofs => type_expect e ty Tint
+  | AA_longofwords hi lo => type_expect e ty Tlong
+  end.
+
+Fixpoint type_annot_args (e: S.typenv) (al: list (annot_arg reg)) (tyl: list typ) : res S.typenv :=
+  match al, tyl with
+  | nil, nil => OK e
+  | a1 :: al, ty1 :: tyl =>
+      do e1 <- type_annot_arg e a1 ty1; type_annot_args e1 al tyl
+  | _, _ =>
+      Error (msg "annotation arity mismatch")
+  end.
+
 Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
   match i with
   | Inop s =>
@@ -251,6 +296,9 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
       do x <- check_successor s;
       do e1 <- S.set_list e args sig.(sig_args);
       S.set e1 res (proj_sig_res sig)
+  | Iannot ef args s =>
+      do x <- check_successor s;
+      type_annot_args e args (sig_args (ef_sig ef))
  | Icond cond args s1 s2 =>
       do x1 <- check_successor s1;
       do x2 <- check_successor s2;
@@ -332,6 +380,55 @@ Proof.
   monadInv H. destruct H0. subst a; eauto with ty. eauto. 
 Qed.
 
+Remark type_expect_incr:
+  forall e ty1 ty2 e' te, type_expect e ty1 ty2 = OK e' -> S.satisf te e' -> S.satisf te e.
+Proof.
+  unfold type_expect; intros. destruct (typ_eq ty1 ty2); inv H. auto.
+Qed.
+
+Hint Resolve type_expect_incr: ty.
+
+Lemma type_expect_sound:
+  forall e ty1 ty2 e', type_expect e ty1 ty2 = OK e' -> ty1 = ty2.
+Proof.
+  unfold type_expect; intros. destruct (typ_eq ty1 ty2); inv H. auto.
+Qed.
+
+Lemma type_annot_arg_incr:
+  forall e a ty e' te, type_annot_arg e a ty = OK e' -> S.satisf te e' -> S.satisf te e.
+Proof.
+  unfold type_annot_arg; intros; destruct a; eauto with ty.
+Qed.
+
+Lemma type_annot_args_incr:
+  forall a ty e e' te, type_annot_args e a ty = OK e' -> S.satisf te e' -> S.satisf te e.
+Proof.
+  induction a; destruct ty; simpl; intros; try discriminate.
+  inv H; auto.
+  monadInv H. eapply type_annot_arg_incr; eauto. 
+Qed.
+
+Hint Resolve type_annot_args_incr: ty.
+
+Lemma type_annot_arg_sound:
+  forall e a ty e' te,
+  type_annot_arg e a ty = OK e' -> S.satisf te e' -> type_of_annot_arg te a = ty.
+Proof.
+  intros. destruct a; simpl in *; try (symmetry; eapply type_expect_sound; eassumption).
+  eapply S.set_sound; eauto.
+Qed.
+
+Lemma type_annot_args_sound:
+  forall al tyl e e' te,
+  type_annot_args e al tyl = OK e' -> S.satisf te e' -> List.map (type_of_annot_arg te) al = tyl.
+Proof.
+  induction al as [|a al]; destruct tyl as [|ty tyl]; simpl; intros; try discriminate.
+- auto.
+- monadInv H. f_equal.
+  eapply type_annot_arg_sound; eauto with ty.
+  eauto.
+Qed.
+
 Lemma type_instr_incr:
   forall e i e' te,
   type_instr e i = OK e' -> S.satisf te e' -> S.satisf te e.
@@ -403,6 +500,10 @@ Proof.
   eapply S.set_list_sound; eauto with ty.
   eapply S.set_sound; eauto with ty.
   eauto with ty.
+- (* annot *)
+  constructor.
+  eapply type_annot_args_sound; eauto.
+  eauto with ty.
 - (* cond *)
   constructor.
   eapply S.set_list_sound; eauto with ty.
@@ -483,6 +584,33 @@ Proof.
   destruct H as [i EQ]; rewrite EQ; auto.
 Qed.
 
+Lemma type_expect_complete:
+  forall e ty, type_expect e ty ty = OK e.
+Proof.
+  unfold type_expect; intros. rewrite dec_eq_true; auto. 
+Qed.
+
+Lemma type_annot_arg_complete:
+  forall te a e,
+  S.satisf te e ->
+  exists e', type_annot_arg e a (type_of_annot_arg te a) = OK e' /\ S.satisf te e'.
+Proof.
+  intros. destruct a; simpl; try (exists e; split; [apply type_expect_complete|assumption]). 
+  apply S.set_complete; auto.
+Qed.
+
+Lemma type_annot_args_complete:
+  forall te al e,
+  S.satisf te e ->
+  exists e', type_annot_args e al (List.map (type_of_annot_arg te) al) = OK e' /\ S.satisf te e'.
+Proof.
+  induction al; simpl; intros. 
+- exists e; auto.
+- destruct (type_annot_arg_complete te a e) as (e1 & A & B); auto. 
+  destruct (IHal e1) as (e2 & C & D); auto.
+  exists e2; split; auto. rewrite A. auto. 
+Qed.
+
 Lemma type_instr_complete:
   forall te e i,
   S.satisf te e ->
@@ -539,6 +667,10 @@ Proof.
   exists e2; split; auto.
   rewrite check_successor_complete by auto; simpl. 
   rewrite A; simpl; rewrite C; auto.
+- (* annot *)
+  exploit type_annot_args_complete; eauto. intros [e1 [A B]].
+  exists e1; split; auto. rewrite check_successor_complete by auto.
+  simpl; rewrite <- H0; eauto.
 - (* cond *)
   exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]].
   exists e1; split; auto.
@@ -782,6 +914,8 @@ Proof.
   inv WTI. rewrite <- H7. apply wt_regset_list. auto.
   (* Ibuiltin *)
   econstructor; eauto. eapply wt_exec_Ibuiltin; eauto.
+  (* Iannot *)
+  econstructor; eauto. 
   (* Icond *)
   econstructor; eauto.
   (* Ijumptable *)
diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml
index 687cbbd3..6c15e15e 100644
--- a/backend/Regalloc.ml
+++ b/backend/Regalloc.ml
@@ -114,6 +114,22 @@ let xparmove srcs dsts k =
   | [src], [dst] -> move src dst k
   | _, _ -> Xparmove(srcs, dsts, new_temp Tint, new_temp Tfloat) :: k
 
+let convert_annot_arg tyenv = function
+  | AA_base r ->
+      begin match tyenv r with
+      | Tlong -> AA_longofwords(V(r, Tint), V(twin_reg r, Tint))
+      | ty    -> AA_base(V(r, ty))
+      end
+  | AA_int n -> AA_int n
+  | AA_long n -> AA_long n
+  | AA_float n -> AA_float n
+  | AA_single n -> AA_single n
+  | AA_loadstack(chunk, ofs) -> AA_loadstack(chunk, ofs)
+  | AA_addrstack(ofs) -> AA_addrstack(ofs)
+  | AA_loadglobal(chunk, id, ofs) -> AA_loadglobal(chunk, id, ofs)
+  | AA_addrglobal(id, ofs) -> AA_addrglobal(id, ofs)
+  | AA_longofwords(hi, lo) -> AA_longofwords(vreg tyenv hi, vreg tyenv lo)
+ 
 (* Return the XTL basic block corresponding to the given RTL instruction.
    Move and parallel move instructions are introduced to honor calling
    conventions and register constraints on some operations.
@@ -192,6 +208,8 @@ let block_of_RTL_instr funsig tyenv = function
       let args2 = constrain_regs args1 cargs and res2 = constrain_regs res1 cres in
       movelist args1 args2
          (Xbuiltin(ef, args2, res2) :: movelist res2 res1 [Xbranch s])
+  | RTL.Iannot(ef, args, s) ->
+      [Xannot(ef, List.map (convert_annot_arg tyenv) args); Xbranch s]
   | RTL.Icond(cond, args, s1, s2) ->
       [Xcond(cond, vregs tyenv args, s1, s2)]
   | RTL.Ijumptable(arg, tbl) ->
@@ -231,6 +249,11 @@ let vset_removelist vl after = List.fold_right VSet.remove vl after
 let vset_addlist vl after = List.fold_right VSet.add vl after
 let vset_addros vos after =
   match vos with Coq_inl v -> VSet.add v after | Coq_inr id -> after
+let vset_addannot a after =
+  match a with
+  | AA_base v -> VSet.add v after
+  | AA_longofwords(hi, lo) -> VSet.add hi (VSet.add lo after)
+  | _ -> after
 
 let live_before instr after =
   match instr with
@@ -256,6 +279,8 @@ let live_before instr after =
       vset_addlist args (vset_addros ros VSet.empty)
   | Xbuiltin(ef, args, res) ->
       vset_addlist args (vset_removelist res after)
+  | Xannot(ef, args) ->
+      List.fold_right vset_addannot args after
   | Xbranch s ->
       after
   | Xcond(cond, args, s1, s2) ->
@@ -431,16 +456,14 @@ let spill_costs f =
         | EF_vstore _ | EF_vstore_global _ | EF_memcpy _ ->
             (* result is not used but should not be spilled *)
             charge_list 10 1 args; charge_list max_int 0 res
-        | EF_annot _ ->
-            (* arguments are not actually used, so don't charge;
-               result is never used but should not be spilled *)
-            charge_list max_int 0 res
         | EF_annot_val _ ->
             (* like a move *)
             charge_list 1 1 args; charge_list 1 1 res
         | _ ->
             charge_list 10 1 args; charge_list 10 1 res
         end
+    | Xannot(ef, args) ->
+        ()
     | Xbranch _ -> ()
     | Xcond(cond, args, _, _) ->
         charge_list 10 1 args
@@ -556,6 +579,8 @@ let add_interfs_instr g instr live =
       | EF_annot_val _, [arg], [res] -> IRC.add_pref g arg res (* like a move *)
       | _ -> ()
       end
+  | Xannot(ef, args) ->
+      ()
   | Xbranch s ->
       ()
   | Xcond(cond, args, s1, s2) ->
@@ -631,10 +656,9 @@ let tospill_instr alloc instr ts =
   | Xtailcall(sg, vos, args) ->
       addros_tospill alloc vos ts
   | Xbuiltin(ef, args, res) ->
-      begin match ef with
-      | EF_annot _ -> ts
-      |      _     -> addlist_tospill alloc args (addlist_tospill alloc res ts)
-      end
+      addlist_tospill alloc args (addlist_tospill alloc res ts)
+  | Xannot(ef, args) ->
+      ts
   | Xbranch s ->
       ts
   | Xcond(cond, args, s1, s2) ->
@@ -794,14 +818,11 @@ let spill_instr tospill eqs instr =
   | Xtailcall(sg, Coq_inr id, args) ->
       ([instr], [])
   | Xbuiltin(ef, args, res) ->
-      begin match ef with
-      | EF_annot _ ->
-          ([instr], eqs)
-      | _ ->
-          let (args', c1, eqs1) = reload_vars tospill eqs args in
-          let (res', c2, eqs2) = save_vars tospill eqs1 res in
-          (c1 @ Xbuiltin(ef, args', res') :: c2, eqs2)
-      end
+      let (args', c1, eqs1) = reload_vars tospill eqs args in
+      let (res', c2, eqs2) = save_vars tospill eqs1 res in
+      (c1 @ Xbuiltin(ef, args', res') :: c2, eqs2)
+  | Xannot(ef, args) ->
+      ([instr], eqs)
   | Xbranch s ->
       ([instr], eqs)
   | Xcond(cond, args, s1, s2) ->
@@ -911,6 +932,18 @@ let make_parmove srcs dsts itmp ftmp k =
   done;
   List.rev_append !code k
 
+let transl_annot_arg alloc = function
+  | AA_base v -> AA_base (alloc v)
+  | AA_int n -> AA_int n
+  | AA_long n -> AA_long n
+  | AA_float n -> AA_float n
+  | AA_single n -> AA_single n
+  | AA_loadstack(chunk, ofs) -> AA_loadstack(chunk, ofs)
+  | AA_addrstack(ofs) -> AA_addrstack(ofs)
+  | AA_loadglobal(chunk, id, ofs) -> AA_loadglobal(chunk, id, ofs)
+  | AA_addrglobal(id, ofs) -> AA_addrglobal(id, ofs)
+  | AA_longofwords(hi, lo) -> AA_longofwords(alloc hi, alloc lo)
+
 let transl_instr alloc instr k =
   match instr with
   | Xmove(src, dst) | Xreload(src, dst) | Xspill(src, dst) ->
@@ -940,12 +973,9 @@ let transl_instr alloc instr k =
   | Xtailcall(sg, vos, args) ->
       LTL.Ltailcall(sg, mros_of alloc vos) :: []
   | Xbuiltin(ef, args, res) ->
-      begin match ef with
-      | EF_annot _ ->
-          LTL.Lannot(ef, List.map alloc args) :: k
-      | _ ->
-          LTL.Lbuiltin(ef, mregs_of alloc args, mregs_of alloc res) :: k
-      end
+      LTL.Lbuiltin(ef, mregs_of alloc args, mregs_of alloc res) :: k
+  | Xannot(ef, args) ->
+      LTL.Lannot(ef, List.map (transl_annot_arg alloc) args) :: k
   | Xbranch s ->
       LTL.Lbranch s :: []
   | Xcond(cond, args, s1, s2) ->
diff --git a/backend/Renumber.v b/backend/Renumber.v
index 0a2c2f12..634fe56a 100644
--- a/backend/Renumber.v
+++ b/backend/Renumber.v
@@ -48,6 +48,7 @@ Definition renum_instr (i: instruction) : instruction :=
   | Icall sg ros args res s => Icall sg ros args res (renum_pc s)
   | Itailcall sg ros args => i
   | Ibuiltin ef args res s => Ibuiltin ef args res (renum_pc s)
+  | Iannot ef args s => Iannot ef args (renum_pc s)
   | Icond cond args s1 s2 => Icond cond args (renum_pc s1) (renum_pc s2)
   | Ijumptable arg tbl => Ijumptable arg (List.map renum_pc tbl)
   | Ireturn or => i
diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v
index 19c3b680..09faa131 100644
--- a/backend/Renumberproof.v
+++ b/backend/Renumberproof.v
@@ -201,6 +201,13 @@ Proof.
     eapply external_call_symbols_preserved; eauto.
     exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   constructor; auto. eapply reach_succ; eauto. simpl; auto.
+(* annot *)
+  econstructor; split.
+  eapply exec_Iannot; eauto.
+    eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+    eapply external_call_symbols_preserved; eauto.
+    exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  constructor; auto. eapply reach_succ; eauto. simpl; auto.
 (* cond *)
   econstructor; split.
   eapply exec_Icond; eauto. 
diff --git a/backend/Selection.v b/backend/Selection.v
index 11125856..5cec6e00 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -203,6 +203,12 @@ Definition classify_call (ge: Cminor.genv) (e: Cminor.expr) : call_kind :=
       end
   end.
 
+Definition builtin_is_annot (ef: external_function) (optid: option ident) : bool :=
+  match ef, optid with
+  | EF_annot _ _, None => true
+  | _, _ => false
+  end.
+
 (** Conversion of Cminor [switch] statements to decision trees. *)
 
 Parameter compile_switch: Z -> nat -> table -> comptree.
@@ -263,7 +269,9 @@ Fixpoint sel_stmt (ge: Cminor.genv) (s: Cminor.stmt) : res stmt :=
       | Call_builtin ef => Sbuiltin optid ef (sel_exprlist args)
       end)
   | Cminor.Sbuiltin optid ef args =>
-      OK (Sbuiltin optid ef (sel_exprlist args))
+      OK (if builtin_is_annot ef optid
+          then Sannot ef (List.map (fun e => annot_arg (sel_expr e)) args)
+          else Sbuiltin optid ef (sel_exprlist args))
   | Cminor.Stailcall sg fn args => 
       OK (match classify_call ge fn with
       | Call_imm id  => Stailcall sg (inr _ id) (sel_exprlist args)
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index bb9bd592..d755d46d 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -520,6 +520,14 @@ Proof.
   auto.
 Qed.
 
+Lemma set_optvar_lessdef:
+  forall e1 e2 optid v1 v2,
+  env_lessdef e1 e2 -> Val.lessdef v1 v2 ->
+  env_lessdef (set_optvar optid v1 e1) (set_optvar optid v2 e2).
+Proof.
+  unfold set_optvar; intros. destruct optid; auto. apply set_var_lessdef; auto.
+Qed.
+
 Lemma set_params_lessdef:
   forall il vl1 vl2, 
   Val.lessdef_list vl1 vl2 ->
@@ -590,6 +598,25 @@ Proof.
   exists (v1' :: vl'); split; auto. constructor; eauto.
 Qed.
 
+Lemma sel_annot_args_correct:
+  forall sp e e' m m',
+  env_lessdef e e' -> Mem.extends m m' ->
+  forall al vl,
+  Cminor.eval_exprlist ge sp e m al vl ->
+  exists vl',
+     list_forall2 (CminorSel.eval_annot_arg tge sp e' m')
+                  (List.map (fun a => annot_arg (sel_expr a)) al)
+                  vl'
+  /\ Val.lessdef_list vl vl'.
+Proof.
+  induction 3; simpl.
+- exists (@nil val); split; constructor. 
+- exploit sel_expr_correct; eauto. intros (v1' & A & B).
+  destruct IHeval_exprlist as (vl' & C & D).
+  exists (v1' :: vl'); split; auto.
+  constructor; auto. eapply eval_annot_arg; eauto. 
+Qed.
+
 (** Semantic preservation for functions and statements. *)
 
 Inductive match_cont: Cminor.cont -> CminorSel.cont -> Prop :=
@@ -675,6 +702,8 @@ Proof.
   destruct (classify_call ge e); simpl; auto.
 (* tailcall *)
   destruct (classify_call ge e); simpl; auto.
+(* builtin *)
+  destruct (builtin_is_annot e); simpl; auto.
 (* seq *)
   exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto.  
   destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ];
@@ -776,14 +805,33 @@ Proof.
   econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto.
   constructor; auto. apply call_cont_commut; auto.
 - (* Sbuiltin *)
+  destruct (builtin_is_annot ef optid) eqn:ISANNOT.
++ (* annotation *)
+  assert (X: exists text targs, ef = EF_annot text targs). 
+  { destruct ef; try discriminate. econstructor; econstructor; eauto. }
+  destruct X as (text & targs & EQ). 
+  assert (Y: optid = None).
+  { destruct ef; try discriminate. destruct optid; try discriminate. auto. }
+  exploit sel_annot_args_correct; eauto. 
+  set (bl' := map (fun e => annot_arg (sel_expr e)) bl).
+  intros (vargs' & P & Q).
+  exploit external_call_mem_extends; eauto. 
+  intros [vres' [m2 [A [B [C D]]]]].
+  left; econstructor; split.
+  econstructor.
+  rewrite EQ; auto.
+  eauto.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  rewrite Y. constructor; auto.
++ (* other builtin *)
   exploit sel_exprlist_correct; eauto. intros [vargs' [P Q]].
   exploit external_call_mem_extends; eauto. 
   intros [vres' [m2 [A [B [C D]]]]].
   left; econstructor; split.
   econstructor. eauto. eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
-  constructor; auto.
-  destruct optid; simpl; auto. apply set_var_lessdef; auto.
+  constructor; auto. apply set_optvar_lessdef; auto. 
 - (* Seq *)
   left; econstructor; split.
   constructor. constructor; auto. constructor; auto.
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 4ee43bb1..c17dc038 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -130,14 +130,26 @@ Definition transl_addr (fe: frame_env) (addr: addressing) :=
 
 (** Translation of an annotation argument. *)
 
-Definition transl_annot_param (fe: frame_env) (l: loc) : annot_param :=
-  match l with
-  | R r => APreg r
-  | S Local ofs ty => APstack (chunk_of_type ty) (offset_of_index fe (FI_local ofs ty))
-  | S _ _ _ => APstack Mint32 (-1)     (**r never happens *)
+Fixpoint transl_annot_arg (fe: frame_env) (a: annot_arg loc) : annot_arg mreg :=
+  match a with
+  | AA_base (R r) => AA_base r
+  | AA_base (S Local ofs ty) =>
+      AA_loadstack (chunk_of_type ty) (Int.repr (offset_of_index fe (FI_local ofs ty)))
+  | AA_base (S _ _ __) => AA_int Int.zero  (**r never happens *)
+  | AA_int n => AA_int n
+  | AA_long n => AA_long n
+  | AA_float n => AA_float n
+  | AA_single n => AA_single n
+  | AA_loadstack chunk ofs =>
+      AA_loadstack chunk (Int.add ofs (Int.repr fe.(fe_stack_data)))
+  | AA_addrstack ofs =>
+      AA_addrstack (Int.add ofs (Int.repr fe.(fe_stack_data)))
+  | AA_loadglobal chunk id ofs => AA_loadglobal chunk id ofs
+  | AA_addrglobal id ofs => AA_addrglobal id ofs
+  | AA_longofwords hi lo => 
+      AA_longofwords (transl_annot_arg fe hi) (transl_annot_arg fe lo)
   end.
 
-
 (** Translation of a Linear instruction.  Prepends the corresponding
   Mach instructions to the given list of instructions.
   [Lgetstack] and [Lsetstack] moves between registers and stack slots
@@ -182,7 +194,7 @@ Definition transl_instr
   | Lbuiltin ef args dst =>
       Mbuiltin ef args dst :: k
   | Lannot ef args =>
-      Mannot ef (map (transl_annot_param fe) args) :: k
+      Mannot ef (map (transl_annot_arg fe) args) :: k
   | Llabel lbl =>
       Mlabel lbl :: k
   | Lgoto lbl =>
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index e3e3a0d0..f4a1935f 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -2382,6 +2382,8 @@ Section ANNOT_ARGUMENTS.
 Variable f: Linear.function.
 Let b := function_bounds f.
 Let fe := make_env b.
+Variable tf: Mach.function.
+Hypothesis TRANSF_F: transf_function f = OK tf.
 Variable j: meminj.
 Variables m m': mem.
 Variables ls ls0: locset.
@@ -2390,39 +2392,67 @@ Variables sp sp': block.
 Variables parent retaddr: val.
 Hypothesis AGR: agree_regs j ls rs.
 Hypothesis AGF: agree_frame f j ls ls0 m sp m' sp' parent retaddr.
-
-Lemma transl_annot_param_correct:
-  forall l,
-  loc_valid f l = true ->
-  match l with S sl ofs ty => slot_within_bounds b sl ofs ty | _ => True end ->
-  exists v, annot_arg rs m' (Vptr sp' Int.zero) (transl_annot_param fe l) v
-         /\ val_inject j (ls l) v.
-Proof.
-  intros. destruct l; simpl in H.
-(* reg *)
-  exists (rs r); split. constructor. auto.
-(* stack *) 
-  destruct sl; try discriminate. 
-  exploit agree_locals; eauto. intros [v [A B]]. inv A. 
-  exists v; split. constructor. rewrite Zplus_0_l. auto. auto.
-Qed.
-
-Lemma transl_annot_params_correct:
-  forall ll,
-  forallb (loc_valid f) ll = true ->
-  (forall sl ofs ty, In (S sl ofs ty) ll -> slot_within_bounds b sl ofs ty) ->
-  exists vl,
-     annot_arguments rs m' (Vptr sp' Int.zero) (map (transl_annot_param fe) ll) vl
-  /\ val_list_inject j (map ls ll) vl.
-Proof.
-  induction ll; simpl; intros. 
-  exists (@nil val); split; constructor.
-  InvBooleans. 
-  exploit (transl_annot_param_correct a). auto. destruct a; auto. 
-  intros [v1 [A B]].
-  exploit IHll. auto. auto. 
-  intros [vl [C D]].
-  exists (v1 :: vl); split; constructor; auto.
+Hypothesis MINJ: Mem.inject j m m'.
+Hypothesis GINJ: meminj_preserves_globals ge j.
+
+Lemma transl_annot_arg_correct:
+  forall a v,
+  eval_annot_arg ge ls (Vptr sp Int.zero) m a v ->
+  (forall l, In l (params_of_annot_arg a) -> loc_valid f l = true) ->
+  (forall sl ofs ty, In (S sl ofs ty) (params_of_annot_arg a) -> slot_within_bounds b sl ofs ty) ->
+  exists v',
+     eval_annot_arg ge rs (Vptr sp' Int.zero) m' (transl_annot_arg fe a) v'
+  /\ val_inject j v v'.
+Proof.
+Local Opaque fe offset_of_index.
+  induction 1; simpl; intros VALID BOUNDS.
+- assert (loc_valid f x = true) by auto.
+  destruct x as [r | [] ofs ty]; try discriminate.
+  + exists (rs r); auto with aarg.
+  + exploit agree_locals; eauto. intros [v [A B]]. inv A. 
+    exists v; split; auto. constructor. simpl. rewrite Int.add_zero_l.
+Local Transparent fe.
+    unfold fe, b. erewrite offset_of_index_no_overflow by eauto.  exact H1. 
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- simpl in H. exploit Mem.load_inject; eauto. eapply agree_inj; eauto. 
+  intros (v' & A & B). exists v'; split; auto. constructor.
+  unfold Mem.loadv, Val.add. rewrite <- Int.add_assoc.
+  unfold fe, b; erewrite shifted_stack_offset_no_overflow; eauto.
+  eapply agree_bounds; eauto. eapply Mem.valid_access_perm. eapply Mem.load_valid_access; eauto. 
+- econstructor; split; eauto with aarg.
+  unfold Val.add. rewrite ! Int.add_zero_l. econstructor. eapply agree_inj; eauto. auto.
+- assert (val_inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address ge id ofs)).
+  { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. 
+    destruct (Genv.find_symbol ge id) eqn:FS; auto.
+    econstructor. eapply (proj1 GINJ); eauto. rewrite Int.add_zero; auto. }
+  exploit Mem.loadv_inject; eauto. intros (v' & A & B). exists v'; auto with aarg.
+- econstructor; split; eauto with aarg. 
+  unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. 
+  destruct (Genv.find_symbol ge id) eqn:FS; auto.
+  econstructor. eapply (proj1 GINJ); eauto. rewrite Int.add_zero; auto.
+- destruct IHeval_annot_arg1 as (v1 & A1 & B1); auto using in_or_app.
+  destruct IHeval_annot_arg2 as (v2 & A2 & B2); auto using in_or_app.
+  exists (Val.longofwords v1 v2); split; auto with aarg. 
+  apply val_longofwords_inject; auto. 
+Qed.
+
+Lemma transl_annot_args_correct:
+  forall al vl,
+  eval_annot_args ge ls (Vptr sp Int.zero) m al vl ->
+  (forall l, In l (params_of_annot_args al) -> loc_valid f l = true) ->
+  (forall sl ofs ty, In (S sl ofs ty) (params_of_annot_args al) -> slot_within_bounds b sl ofs ty) ->
+  exists vl',
+     eval_annot_args ge rs (Vptr sp' Int.zero) m' (List.map (transl_annot_arg fe) al) vl'
+  /\ val_list_inject j vl vl'.
+Proof.
+  induction 1; simpl; intros VALID BOUNDS.
+- exists (@nil val); split; constructor.
+- exploit transl_annot_arg_correct; eauto using in_or_app. intros (v1' & A & B).
+  exploit IHlist_forall2; eauto using in_or_app. intros (vl' & C & D).
+  exists (v1'::vl'); split; constructor; auto. 
 Qed.
 
 End ANNOT_ARGUMENTS.
@@ -2705,25 +2735,28 @@ Proof.
   eapply agree_valid_mach; eauto.
 
 - (* Lannot *)
-  exploit transl_annot_params_correct; eauto. eapply wt_state_annot; eauto.
+  exploit transl_annot_args_correct; eauto.
+  eapply match_stacks_preserves_globals; eauto.
+  rewrite <- forallb_forall. eapply wt_state_annot; eauto.
   intros [vargs' [P Q]]. 
-  exploit external_call_mem_inject'; eauto. 
+  exploit external_call_mem_inject; eauto. 
     eapply match_stacks_preserves_globals; eauto.
   intros [j' [res' [m1' [A [B [C [D [E [F G]]]]]]]]].
   econstructor; split.
-  apply plus_one. econstructor; eauto. 
-  eapply external_call_symbols_preserved'; eauto.
+  apply plus_one. econstructor; eauto.
+  eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   econstructor; eauto with coqlib.
-  inv H; inv A. eapply match_stack_change_extcall; eauto.
+  eapply match_stack_change_extcall; eauto.
   apply Plt_Ple. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto.
   apply Plt_Ple. change (Mem.valid_block m'0 sp'). eapply agree_valid_mach; eauto.
   eapply agree_regs_inject_incr; eauto.
   eapply agree_frame_inject_incr; eauto. 
   apply agree_frame_extcall_invariant with m m'0; auto.
-  eapply external_call_valid_block'; eauto.
-  intros. inv H; eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto.
-  eapply external_call_valid_block'; eauto.
+  eapply external_call_valid_block; eauto.
+  intros. eapply external_call_max_perm; eauto. eapply agree_valid_linear; eauto.
+  eapply external_call_valid_block; eauto.
   eapply agree_valid_mach; eauto.
 
 - (* Llabel *)
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 5ee7ccc1..bd9b227f 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -513,6 +513,19 @@ Proof.
   exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   econstructor; eauto. apply regset_set; auto.
 
+(* annot *)
+  TransfInstr.
+  exploit (@eval_annot_args_lessdef _ ge (fun r => rs#r) (fun r => rs'#r)); eauto.
+  intros (vargs' & P & Q).
+  exploit external_call_mem_extends; eauto.
+  intros [v' [m'1 [A [B [C D]]]]].
+  left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) pc' rs' m'1); split.
+  eapply exec_Iannot; eauto.
+  eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  econstructor; eauto.
+
 (* cond *)
   TransfInstr. 
   left. exists (State s' (transf_function f) (Vptr sp0 Int.zero) (if b then ifso else ifnot) rs' m'); split.
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index e6588938..52318ede 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -344,8 +344,9 @@ Proof.
   econstructor; eauto.
   (* Lannot *)
   left; simpl; econstructor; split.
-  eapply exec_Lannot; eauto. 
-  eapply external_call_symbols_preserved'; eauto.
+  eapply exec_Lannot; eauto.
+  eapply eval_annot_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   econstructor; eauto.
 
diff --git a/backend/Unusedglob.v b/backend/Unusedglob.v
index 55a093a4..400c19d9 100644
--- a/backend/Unusedglob.v
+++ b/backend/Unusedglob.v
@@ -60,6 +60,7 @@ Definition ref_instruction (i: instruction) : list ident :=
   | Itailcall _ (inl r) _ => nil
   | Itailcall _ (inr id) _ => id :: nil
   | Ibuiltin ef _ _ _ => globals_external ef
+  | Iannot _ args _ => globals_of_annot_args args
   | Icond cond _ _ _ => nil
   | Ijumptable _ _ => nil
   | Ireturn _ => nil
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index fbf43866..90d7f270 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -741,6 +741,64 @@ Proof.
   auto.
 Qed.
 
+Lemma eval_annot_arg_inject:
+  forall rs sp m j rs' sp' m' a v,
+  eval_annot_arg ge (fun r => rs#r) (Vptr sp Int.zero) m a v ->
+  j sp = Some(sp', 0) ->
+  meminj_preserves_globals j ->
+  regset_inject j rs rs' ->
+  Mem.inject j m m' ->
+  (forall id, In id (globals_of_annot_arg a) -> kept id) ->
+  exists v',
+     eval_annot_arg tge (fun r => rs'#r) (Vptr sp' Int.zero) m' a v'
+  /\ val_inject j v v'.
+Proof.
+  induction 1; intros SP GL RS MI K; simpl in K.
+- exists rs'#x; split; auto. constructor. 
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- simpl in H. exploit Mem.load_inject; eauto. rewrite Zplus_0_r. 
+  intros (v' & A & B). exists v'; auto with aarg.
+- econstructor; split; eauto with aarg. simpl. econstructor; eauto. rewrite Int.add_zero; auto.
+- assert (val_inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)).
+  { unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. 
+    destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
+    exploit symbols_inject_2; eauto. intros (b' & A & B). rewrite A. 
+    econstructor; eauto. rewrite Int.add_zero; auto. }
+  exploit Mem.loadv_inject; eauto. intros (v' & A & B). exists v'; auto with aarg.
+- econstructor; split; eauto with aarg.
+  unfold Senv.symbol_address; simpl; unfold Genv.symbol_address. 
+  destruct (Genv.find_symbol ge id) as [b|] eqn:FS; auto.
+  exploit symbols_inject_2; eauto. intros (b' & A & B). rewrite A. 
+  econstructor; eauto. rewrite Int.add_zero; auto.
+- destruct IHeval_annot_arg1 as (v1' & A1 & B1); eauto using in_or_app.
+  destruct IHeval_annot_arg2 as (v2' & A2 & B2); eauto using in_or_app.
+  exists (Val.longofwords v1' v2'); split; auto with aarg. 
+  apply val_longofwords_inject; auto.
+Qed.
+
+Lemma eval_annot_args_inject:
+  forall rs sp m j rs' sp' m' al vl,
+  eval_annot_args ge (fun r => rs#r) (Vptr sp Int.zero) m al vl ->
+  j sp = Some(sp', 0) ->
+  meminj_preserves_globals j ->
+  regset_inject j rs rs' ->
+  Mem.inject j m m' ->
+  (forall id, In id (globals_of_annot_args al) -> kept id) ->
+  exists vl',
+     eval_annot_args tge (fun r => rs'#r) (Vptr sp' Int.zero) m' al vl'
+  /\ val_list_inject j vl vl'.
+Proof.
+  induction 1; intros. 
+- exists (@nil val); split; constructor.
+- simpl in H5. 
+  exploit eval_annot_arg_inject; eauto using in_or_app. intros (v1' & A & B).
+  destruct IHlist_forall2 as (vl' & C & D); eauto using in_or_app. 
+  exists (v1' :: vl'); split; constructor; auto.
+Qed.
+
 Theorem step_simulation:
   forall S1 t S2, step ge S1 t S2 ->
   forall S1' (MS: match_states S1 S1'),
@@ -845,6 +903,25 @@ Proof.
   unfold Mem.valid_block in *; xomega.
   apply set_reg_inject; auto. apply regset_inject_incr with j; auto.
 
+- (* annot *)
+  exploit eval_annot_args_inject; eauto. 
+  eapply match_stacks_preserves_globals; eauto.
+  intros. apply KEPT. red. econstructor; econstructor; eauto. 
+  intros (vargs' & P & Q).
+  exploit external_call_inject; eauto. 
+  eapply match_stacks_preserves_globals; eauto.
+  destruct ef; contradiction.
+  intros (j' & tv & tm' & A & B & C & D & E & F & G).
+  econstructor; split.
+  eapply exec_Iannot; eauto.
+  eapply match_states_regular with (j := j'); eauto. 
+  apply match_stacks_incr with j; auto. 
+  intros. exploit G; eauto. intros [U V].
+  assert (Mem.valid_block m sp0) by (eapply Mem.valid_block_inject_1; eauto).
+  assert (Mem.valid_block tm tsp) by (eapply Mem.valid_block_inject_2; eauto).
+  unfold Mem.valid_block in *; xomega.
+  apply regset_inject_incr with j; auto.
+
 - (* cond *)
   assert (C: eval_condition cond trs##args tm = Some b).
   { eapply eval_condition_inject; eauto. apply regs_inject; auto. }
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 4249a8da..8720ce50 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -55,7 +55,6 @@ Inductive builtin_kind : Type :=
   | Builtin_vload (chunk: memory_chunk) (aaddr: aval)
   | Builtin_vstore (chunk: memory_chunk) (aaddr av: aval)
   | Builtin_memcpy (sz al: Z) (adst asrc: aval)
-  | Builtin_annot
   | Builtin_annot_val (av: aval)
   | Builtin_default.
 
@@ -66,7 +65,6 @@ Definition classify_builtin (ef: external_function) (args: list reg) (ae: aenv)
   | EF_vstore chunk, a1::a2::nil => Builtin_vstore chunk (areg ae a1) (areg ae a2)
   | EF_vstore_global chunk id ofs, a1::nil => Builtin_vstore chunk (Ptr (Gl id ofs)) (areg ae a1)
   | EF_memcpy sz al, a1::a2::nil => Builtin_memcpy sz al (areg ae a1) (areg ae a2)
-  | EF_annot _ _, _ => Builtin_annot
   | EF_annot_val _ _, a1::nil => Builtin_annot_val (areg ae a1)
   | _, _ => Builtin_default
   end.
@@ -86,8 +84,6 @@ Definition transfer_builtin (ae: aenv) (am: amem) (rm: romem) (ef: external_func
       let p := loadbytes am rm (aptr_of_aval asrc) in
       let am' := storebytes am (aptr_of_aval adst) sz p in
       VA.State (AE.set res itop ae) am'
-  | Builtin_annot =>
-      VA.State (AE.set res itop ae) am
   | Builtin_annot_val av =>
       VA.State (AE.set res av ae) am
   | Builtin_default =>
@@ -115,6 +111,8 @@ Definition transfer (f: function) (rm: romem) (pc: node) (ae: aenv) (am: amem) :
       VA.Bot
   | Some(Ibuiltin ef args res s) =>
       transfer_builtin ae am rm ef args res
+  | Some(Iannot ef args s) =>
+      VA.State ae am
   | Some(Icond cond args s1 s2) =>
       VA.State ae am
   | Some(Ijumptable arg tbl) =>
@@ -306,7 +304,6 @@ Lemma classify_builtin_sound:
       exists dst, exists src,
       extcall_memcpy_sem sz al ge (dst::src::nil) m t res m'
       /\ vmatch bc dst adst /\ vmatch bc src asrc
-  | Builtin_annot => m' = m /\ res = Vundef
   | Builtin_annot_val av => m' = m /\ vmatch bc res av
   | Builtin_default => True
   end.
@@ -329,8 +326,6 @@ Proof.
 - (* memcpy *)
   destruct args; auto. destruct args; auto. destruct args; auto.
   exists (e#p), (e#p0); eauto.
-- (* annot *)
-  simpl in H1. inv H1. auto.
 - (* annot val *)
   destruct args; auto. destruct args; auto.
   simpl in H1. inv H1. eauto.
@@ -1303,10 +1298,6 @@ Proof.
   intros. eapply loadbytes_sound; eauto. apply match_aptr_of_aval; auto. 
   eapply romatch_storebytes; eauto. 
   eapply sound_stack_storebytes; eauto. 
-+ (* annot *)
-  intros (A & B); subst. 
-  eapply sound_succ_state; eauto. simpl; auto. 
-  apply ematch_update; auto. constructor.
 + (* annot val *)
   intros (A & B); subst. 
   eapply sound_succ_state; eauto. simpl; auto. 
@@ -1359,6 +1350,11 @@ Proof.
   rewrite C; auto.
   exact AA.
 
+- (* annot *)
+  destruct ef; try contradiction. inv H2. 
+  eapply sound_succ_state; eauto. simpl; auto. 
+  unfold transfer; rewrite H; eauto. 
+
 - (* cond *)
   eapply sound_succ_state; eauto. 
   simpl. destruct b; auto. 
diff --git a/backend/XTL.ml b/backend/XTL.ml
index 9cb8e0a1..30c09fdf 100644
--- a/backend/XTL.ml
+++ b/backend/XTL.ml
@@ -35,6 +35,7 @@ type instruction =
   | Xcall of signature * (var, ident) sum * var list * var list
   | Xtailcall of signature * (var, ident) sum * var list
   | Xbuiltin of external_function * var list * var list
+  | Xannot of external_function * var annot_arg list
   | Xbranch of node
   | Xcond of condition * var list * node * node
   | Xjumptable of var * node list
@@ -124,6 +125,12 @@ let rec set_vars_type vl tyl =
 let unify_var_type v1 v2 =
   if typeof v1 <> typeof v2 then raise Type_error
 
+let type_annot_arg a ty =
+  match a with
+  | AA_base v -> set_var_type v ty
+  | AA_longofwords(v1, v2) -> set_var_type v1 Tint; set_var_type v2 Tint
+  | _ -> ()
+
 let type_instr = function
   | Xmove(src, dst) | Xspill(src, dst) | Xreload(src, dst) ->
       unify_var_type src dst
@@ -153,6 +160,11 @@ let type_instr = function
       let sg = ef_sig ef in
       set_vars_type args sg.sig_args;
       set_vars_type res (Events.proj_sig_res' sg)
+  | Xannot(ef, args) ->
+      let sg = ef_sig ef in
+      if List.length args = List.length sg.sig_args
+      then List.iter2 type_annot_arg args sg.sig_args
+      else raise Type_error
   | Xbranch s ->
       ()
   | Xcond(cond, args, s1, s2) ->
diff --git a/common/AST.v b/common/AST.v
index 9c29a374..d2926178 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -576,7 +576,7 @@ Inductive external_function : Type :=
          Produces no observable event. *)
   | EF_memcpy (sz: Z) (al: Z)
      (** Block copy, of [sz] bytes, between addresses that are [al]-aligned. *)
-  | EF_annot (text: ident) (targs: list annot_arg)
+  | EF_annot (text: ident) (targs: list typ)
      (** A programmer-supplied annotation.  Takes zero, one or several arguments,
          produces an event carrying the text and the values of these arguments,
          and returns no value. *)
@@ -584,27 +584,15 @@ Inductive external_function : Type :=
      (** Another form of annotation that takes one argument, produces
          an event carrying the text and the value of this argument,
          and returns the value of the argument. *)
-  | EF_inline_asm (text: ident)
+  | EF_inline_asm (text: ident).
      (** Inline [asm] statements.  Semantically, treated like an
          annotation with no parameters ([EF_annot text nil]).  To be
          used with caution, as it can invalidate the semantic
          preservation theorem.  Generated only if [-finline-asm] is
          given. *)
 
-with annot_arg : Type :=
-  | AA_arg (ty: typ)
-  | AA_int (n: int)
-  | AA_float (n: float).
-
 (** The type signature of an external function. *)
 
-Fixpoint annot_args_typ (targs: list annot_arg) : list typ :=
-  match targs with
-  | nil => nil
-  | AA_arg ty :: targs' => ty :: annot_args_typ targs'
-  | _ :: targs' => annot_args_typ targs'
-  end.
-
 Definition ef_sig (ef: external_function): signature :=
   match ef with
   | EF_external name sg => sg
@@ -616,7 +604,7 @@ Definition ef_sig (ef: external_function): signature :=
   | EF_malloc => mksignature (Tint :: nil) (Some Tint) cc_default
   | EF_free => mksignature (Tint :: nil) None cc_default
   | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None cc_default
-  | EF_annot text targs => mksignature (annot_args_typ targs) None cc_default
+  | EF_annot text targs => mksignature targs None cc_default
   | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default
   | EF_inline_asm text => mksignature nil None cc_default
   end.
@@ -653,7 +641,7 @@ Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2}
 Proof.
   generalize ident_eq signature_eq chunk_eq typ_eq zeq Int.eq_dec; intros.
   decide equality.
-  apply list_eq_dec. decide equality. apply Float.eq_dec. 
+  apply list_eq_dec. auto.
 Defined.
 Global Opaque external_function_eq.
 
@@ -699,3 +687,56 @@ Definition transf_partial_fundef (fd: fundef A): res (fundef B) :=
   end.
 
 End TRANSF_PARTIAL_FUNDEF.
+
+(** * Arguments to annotations *)
+
+Set Contextual Implicit. 
+
+Inductive annot_arg (A: Type) : Type :=
+  | AA_base (x: A)
+  | AA_int (n: int)
+  | AA_long (n: int64)
+  | AA_float (f: float)
+  | AA_single (f: float32)
+  | AA_loadstack (chunk: memory_chunk) (ofs: int)
+  | AA_addrstack (ofs: int)
+  | AA_loadglobal (chunk: memory_chunk) (id: ident) (ofs: int)
+  | AA_addrglobal (id: ident) (ofs: int)
+  | AA_longofwords (hi lo: annot_arg A).
+
+Fixpoint globals_of_annot_arg (A: Type) (a: annot_arg A) : list ident :=
+  match a with
+  | AA_loadglobal chunk id ofs => id :: nil
+  | AA_addrglobal id ofs => id :: nil
+  | AA_longofwords hi lo => globals_of_annot_arg hi ++ globals_of_annot_arg lo
+  | _ => nil
+  end.
+
+Definition globals_of_annot_args (A: Type) (al: list (annot_arg A)) : list ident :=
+  List.fold_right (fun a l => globals_of_annot_arg a ++ l) nil al.
+
+Fixpoint params_of_annot_arg (A: Type) (a: annot_arg A) : list A :=
+  match a with
+  | AA_base x => x :: nil
+  | AA_longofwords hi lo => params_of_annot_arg hi ++ params_of_annot_arg lo
+  | _ => nil
+  end.
+
+Definition params_of_annot_args (A: Type) (al: list (annot_arg A)) : list A :=
+  List.fold_right (fun a l => params_of_annot_arg a ++ l) nil al.
+
+Fixpoint map_annot_arg (A B: Type) (f: A -> B) (a: annot_arg A) : annot_arg B :=
+  match a with
+  | AA_base x => AA_base (f x)
+  | AA_int n => AA_int n
+  | AA_long n => AA_long n
+  | AA_float n => AA_float n
+  | AA_single n => AA_single n
+  | AA_loadstack chunk ofs => AA_loadstack chunk ofs
+  | AA_addrstack ofs => AA_addrstack ofs
+  | AA_loadglobal chunk id ofs => AA_loadglobal chunk id ofs
+  | AA_addrglobal id ofs => AA_addrglobal id ofs
+  | AA_longofwords hi lo => 
+      AA_longofwords (map_annot_arg f hi) (map_annot_arg f lo)
+  end.
+
diff --git a/common/Events.v b/common/Events.v
index 3fb58806..ad59ece9 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1344,25 +1344,16 @@ Qed.
 
 (** ** Semantics of annotations. *)
 
-Fixpoint annot_eventvals (targs: list annot_arg) (vargs: list eventval) : list eventval :=
-  match targs, vargs with
-  | AA_arg ty :: targs', varg :: vargs' => varg :: annot_eventvals targs' vargs'
-  | AA_int n :: targs', _ => EVint n :: annot_eventvals targs' vargs
-  | AA_float n :: targs', _ => EVfloat n :: annot_eventvals targs' vargs
-  | _, _ => vargs
-  end.
-
-Inductive extcall_annot_sem (text: ident) (targs: list annot_arg) (ge: Senv.t):
+Inductive extcall_annot_sem (text: ident) (targs: list typ) (ge: Senv.t):
               list val -> mem -> trace -> val -> mem -> Prop :=
   | extcall_annot_sem_intro: forall vargs m args,
-      eventval_list_match ge args (annot_args_typ targs) vargs ->
-      extcall_annot_sem text targs ge vargs m
-           (Event_annot text (annot_eventvals targs args) :: E0) Vundef m.
+      eventval_list_match ge args targs vargs ->
+      extcall_annot_sem text targs ge vargs m (Event_annot text args :: E0) Vundef m.
 
 Lemma extcall_annot_ok:
   forall text targs,
   extcall_properties (extcall_annot_sem text targs)
-                     (mksignature (annot_args_typ targs) None cc_default)
+                     (mksignature targs None cc_default)
                      nil.
 Proof.
   intros; constructor; intros.
@@ -1794,9 +1785,167 @@ Proof.
   split; congruence.
 Qed.
 
+(** * Evaluation of annotation arguments *)
+
+Section EVAL_ANNOT_ARG.
+
+Variable A: Type.
+Variable ge: Senv.t.
+Variable e: A -> val.
+Variable sp: val.
+Variable m: mem.
+
+Inductive eval_annot_arg: annot_arg A -> val -> Prop :=
+  | eval_AA_base: forall x,
+      eval_annot_arg (AA_base x) (e x)
+  | eval_AA_int: forall n,
+      eval_annot_arg (AA_int n) (Vint n)
+  | eval_AA_long: forall n,
+      eval_annot_arg (AA_long n) (Vlong n)
+  | eval_AA_float: forall n,
+      eval_annot_arg (AA_float n) (Vfloat n)
+  | eval_AA_single: forall n,
+      eval_annot_arg (AA_single n) (Vsingle n)
+  | eval_AA_loadstack: forall chunk ofs v,
+      Mem.loadv chunk m (Val.add sp (Vint ofs)) = Some v ->
+      eval_annot_arg (AA_loadstack chunk ofs) v
+  | eval_AA_addrstack: forall ofs,
+      eval_annot_arg (AA_addrstack ofs) (Val.add sp (Vint ofs))
+  | eval_AA_loadglobal: forall chunk id ofs v,
+      Mem.loadv chunk m (Senv.symbol_address ge id ofs) = Some v ->
+      eval_annot_arg (AA_loadglobal chunk id ofs) v
+  | eval_AA_addrglobal: forall id ofs,
+      eval_annot_arg (AA_addrglobal id ofs) (Senv.symbol_address ge id ofs)
+  | eval_AA_longofwords: forall hi lo vhi vlo,
+      eval_annot_arg hi vhi -> eval_annot_arg lo vlo ->
+      eval_annot_arg (AA_longofwords hi lo) (Val.longofwords vhi vlo).
+
+Definition eval_annot_args (al: list (annot_arg A)) (vl: list val) : Prop :=
+  list_forall2 eval_annot_arg al vl.
+
+Lemma eval_annot_arg_determ:
+  forall a v, eval_annot_arg a v -> forall v', eval_annot_arg a v' -> v' = v.
+Proof.
+  induction 1; intros v' EV; inv EV; try congruence.
+  f_equal; eauto.
+Qed.
+
+Lemma eval_annot_args_determ:
+  forall al vl, eval_annot_args al vl -> forall vl', eval_annot_args al vl' -> vl' = vl.
+Proof.
+  induction 1; intros v' EV; inv EV; f_equal; eauto using eval_annot_arg_determ.
+Qed.
+
+End EVAL_ANNOT_ARG.
+
+Hint Constructors eval_annot_arg: aarg.
+
+(** Invariance by change of global environment. *)
+
+Section EVAL_ANNOT_ARG_PRESERVED.
+
+Variables A F1 V1 F2 V2: Type.
+Variable ge1: Genv.t F1 V1.
+Variable ge2: Genv.t F2 V2.
+Variable e: A -> val.
+Variable sp: val.
+Variable m: mem.
+
+Hypothesis symbols_preserved:
+  forall id, Genv.find_symbol ge2 id = Genv.find_symbol ge1 id.
+
+Lemma eval_annot_arg_preserved:
+  forall a v, eval_annot_arg ge1 e sp m a v -> eval_annot_arg ge2 e sp m a v.
+Proof.
+  assert (EQ: forall id ofs, Senv.symbol_address ge2 id ofs = Senv.symbol_address ge1 id ofs).
+  { unfold Senv.symbol_address; simpl; intros. rewrite symbols_preserved; auto. }
+  induction 1; eauto with aarg. rewrite <- EQ in H; eauto with aarg. rewrite <- EQ; eauto with aarg. 
+Qed. 
+
+Lemma eval_annot_args_preserved:
+  forall al vl, eval_annot_args ge1 e sp m al vl -> eval_annot_args ge2 e sp m al vl.
+Proof.
+  induction 1; constructor; auto; eapply eval_annot_arg_preserved; eauto. 
+Qed.
+
+End EVAL_ANNOT_ARG_PRESERVED.
+
+(** Compatibility with the "is less defined than" relation. *)
+
+Section EVAL_ANNOT_ARG_LESSDEF.
+
+Variable A: Type.
+Variable ge: Senv.t.
+Variables e1 e2: A -> val.
+Variable sp: val.
+Variables m1 m2: mem.
 
+Hypothesis env_lessdef: forall x, Val.lessdef (e1 x) (e2 x).
+Hypothesis mem_extends: Mem.extends m1 m2.
 
+Lemma eval_annot_arg_lessdef:
+  forall a v1, eval_annot_arg ge e1 sp m1 a v1 ->
+  exists v2, eval_annot_arg ge e2 sp m2 a v2 /\ Val.lessdef v1 v2.
+Proof.
+  induction 1.
+- exists (e2 x); auto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- econstructor; eauto with aarg.
+- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with aarg. 
+- econstructor; eauto with aarg.
+- exploit Mem.loadv_extends; eauto. intros (v' & P & Q). exists v'; eauto with aarg.
+- econstructor; eauto with aarg.
+- destruct IHeval_annot_arg1 as (vhi' & P & Q).
+  destruct IHeval_annot_arg2 as (vlo' & R & S).
+  econstructor; split; eauto with aarg. apply Val.longofwords_lessdef; auto. 
+Qed.
+
+Lemma eval_annot_args_lessdef:
+  forall al vl1, eval_annot_args ge e1 sp m1 al vl1 ->
+  exists vl2, eval_annot_args ge e2 sp m2 al vl2 /\ Val.lessdef_list vl1 vl2.
+Proof.
+  induction 1.
+- econstructor; split. constructor. auto.
+- exploit eval_annot_arg_lessdef; eauto. intros (v1' & P & Q). 
+  destruct IHlist_forall2 as (vl' & U & V).
+  exists (v1'::vl'); split; constructor; auto.
+Qed.
+
+End EVAL_ANNOT_ARG_LESSDEF.
+
+(** Extensionality *)
+
+Section EVAL_ANNOT_ARG_EXTEN.
+
+Variable A: Type.
+Variable ge: Senv.t.
+Variables e1 e2: A -> val.
+Variable sp: val.
+Variable m: mem.
+
+Lemma eval_annot_arg_exten:
+  forall a v, eval_annot_arg ge e1 sp m a v ->
+  (forall x, In x (params_of_annot_arg a) -> e2 x = e1 x) ->
+  eval_annot_arg ge e2 sp m a v.
+Proof.
+  induction 1; simpl; intros EXT; try (now constructor).
+- rewrite <- EXT by auto. constructor.
+- constructor; eauto using in_or_app. 
+Qed.
+
+Lemma eval_annot_args_exten:
+  forall a v, eval_annot_args ge e1 sp m a v ->
+  (forall x, In x (params_of_annot_args a) -> e2 x = e1 x) ->
+  eval_annot_args ge e2 sp m a v.
+Proof.
+  induction 1; simpl; intros EXT; constructor.
+  eapply eval_annot_arg_exten; eauto using in_or_app.
+  eapply IHlist_forall2; eauto using in_or_app.
+Qed.
 
+End EVAL_ANNOT_ARG_EXTEN.
 
 
 
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index c0eab04f..e4d79c3e 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -54,3 +54,26 @@ let name_of_external = function
   | EF_annot(text, targs) -> sprintf "annot %S" (extern_atom text)
   | EF_annot_val(text, targ) ->  sprintf "annot_val %S" (extern_atom text)
   | EF_inline_asm text -> sprintf "inline_asm %S" (extern_atom text)
+
+let print_annot_arg px oc = function
+  | AA_base x -> px oc x
+  | AA_int n -> fprintf oc "int %ld" (camlint_of_coqint n)
+  | AA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n)
+  | AA_float n -> fprintf oc "float %F" (camlfloat_of_coqfloat n)
+  | AA_single n -> fprintf oc "single %F" (camlfloat_of_coqfloat32 n)
+  | AA_loadstack(chunk, ofs) -> 
+      fprintf oc "%s[sp + %ld]" (name_of_chunk chunk) (camlint_of_coqint ofs)
+  | AA_addrstack(ofs) ->
+      fprintf oc "sp + %ld" (camlint_of_coqint ofs)
+  | AA_loadglobal(chunk, id, ofs) -> 
+      fprintf oc "%s[&%s + %ld]"
+              (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs)
+  | AA_addrglobal(id, ofs) ->
+      fprintf oc "&%s + %ld" (extern_atom id) (camlint_of_coqint ofs)
+  | AA_longofwords(hi, lo) -> fprintf oc "longofwords %a %a" px hi px lo
+
+let rec print_annot_args px oc = function
+  | [] -> ()
+  | [a] -> print_annot_arg px oc a
+  | a1 :: al ->
+      fprintf oc "%a, %a" (print_annot_arg px) a1 (print_annot_args px) al
diff --git a/ia32/Asm.v b/ia32/Asm.v
index 15f80e42..b67c3cc5 100644
--- a/ia32/Asm.v
+++ b/ia32/Asm.v
@@ -212,11 +212,7 @@ Inductive instruction: Type :=
   | Pallocframe(sz: Z)(ofs_ra ofs_link: int)
   | Pfreeframe(sz: Z)(ofs_ra ofs_link: int)
   | Pbuiltin(ef: external_function)(args: list preg)(res: list preg)
-  | Pannot(ef: external_function)(args: list annot_param)
-
-with annot_param : Type :=
-  | APreg: preg -> annot_param
-  | APstack: memory_chunk -> Z -> annot_param.
+  | Pannot(ef: external_function)(args: list (annot_arg preg)).
 
 Definition code := list instruction.
 Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
@@ -798,20 +794,6 @@ Definition extcall_arguments
 Definition loc_external_result (sg: signature) : list preg :=
   map preg_of (loc_result sg).
 
-(** Extract the values of the arguments of an annotation. *)
-
-Inductive annot_arg (rs: regset) (m: mem): annot_param -> val -> Prop :=
-  | annot_arg_reg: forall r,
-      annot_arg rs m (APreg r) (rs r)
-  | annot_arg_stack: forall chunk ofs stk base v,
-      rs (IR ESP) = Vptr stk base ->
-      Mem.load chunk m stk (Int.unsigned base + ofs) = Some v ->
-      annot_arg rs m (APstack chunk ofs) v.
-
-Definition annot_arguments
-    (rs: regset) (m: mem) (params: list annot_param) (args: list val) : Prop :=
-  list_forall2 (annot_arg rs m) params args.
-
 (** Execution of the instruction at [rs#PC]. *)
 
 Inductive state: Type :=
@@ -840,8 +822,8 @@ Inductive step: state -> trace -> state -> Prop :=
       rs PC = Vptr b ofs ->
       Genv.find_funct_ptr ge b = Some (Internal f) ->
       find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pannot ef args) ->
-      annot_arguments rs m args vargs ->
-      external_call' ef ge vargs m t v m' ->
+      eval_annot_args ge rs (rs ESP) m args vargs ->
+      external_call ef ge vargs m t v m' ->
       step (State rs m) t
            (State (nextinstr rs) m')
   | exec_step_external:
@@ -893,16 +875,6 @@ Proof.
   intros. red in H0; red in H1. eauto. 
 Qed.
 
-Remark annot_arguments_determ:
-  forall rs m params args1 args2,
-  annot_arguments rs m params args1 -> annot_arguments rs m params args2 -> args1 = args2.
-Proof.
-  unfold annot_arguments. intros. revert params args1 H args2 H0. 
-  induction 1; intros. 
-  inv H0; auto.
-  inv H1. decEq; eauto. inv H; inv H4. auto. congruence. 
-Qed.
-
 Lemma semantics_determinate: forall p, determinate (semantics p).
 Proof.
 Ltac Equalities :=
@@ -912,32 +884,32 @@ Ltac Equalities :=
   | _ => idtac
   end.
   intros; constructor; simpl; intros.
-(* determ *)
+- (* determ *)
   inv H; inv H0; Equalities.
-  split. constructor. auto.
-  discriminate.
-  discriminate.
-  inv H11. 
-  exploit external_call_determ'. eexact H4. eexact H9. intros [A B].
++ split. constructor. auto.
++ discriminate.
++ discriminate.
++ inv H11. 
++ exploit external_call_determ'. eexact H4. eexact H9. intros [A B].
   split. auto. intros. destruct B; auto. subst. auto.
-  inv H12.
-  assert (vargs0 = vargs) by (eapply annot_arguments_determ; eauto). subst vargs0.
-  exploit external_call_determ'. eexact H5. eexact H13. intros [A B].
++ inv H12.
++ assert (vargs0 = vargs) by (eapply eval_annot_args_determ; eauto). subst vargs0.
+  exploit external_call_determ. eexact H5. eexact H13. intros [A B].
   split. auto. intros. destruct B; auto. subst. auto.
-  assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
++ assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
   exploit external_call_determ'. eexact H4. eexact H9. intros [A B].
   split. auto. intros. destruct B; auto. subst. auto.
-(* trace length *)
+- (* trace length *)
   red; intros; inv H; simpl.
   omega.
   inv H3. eapply external_call_trace_length; eauto.
-  inv H4. eapply external_call_trace_length; eauto.
+  eapply external_call_trace_length; eauto.
   inv H3. eapply external_call_trace_length; eauto.
-(* initial states *)
+- (* initial states *)
   inv H; inv H0. f_equal. congruence.
-(* final no step *)
+- (* final no step *)
   inv H. unfold Vzero in H0. red; intros; red; intros. inv H; congruence.
-(* final states *)
+- (* final states *)
   inv H; inv H0. congruence.
 Qed.
 
diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v
index 9c0a76e0..2c1afc11 100644
--- a/ia32/Asmgen.v
+++ b/ia32/Asmgen.v
@@ -492,14 +492,6 @@ Definition transl_store (chunk: memory_chunk)
       Error (msg "Asmgen.transl_store")
   end.
 
-(** Translation of arguments to annotations *)
-
-Definition transl_annot_param (p: Mach.annot_param) : Asm.annot_param :=
-  match p with
-  | Mach.APreg r => APreg (preg_of r)
-  | Mach.APstack chunk ofs => APstack chunk ofs
-  end.
-
 (** Translation of a Mach instruction. *)
 
 Definition transl_instr (f: Mach.function) (i: Mach.instruction)
@@ -546,7 +538,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
   | Mbuiltin ef args res =>
       OK (Pbuiltin ef (List.map preg_of args) (List.map preg_of res) :: k)
   | Mannot ef args =>
-      OK (Pannot ef (map transl_annot_param args) :: k)
+      OK (Pannot ef (List.map (map_annot_arg preg_of) args) :: k)
   end.
 
 (** Translation of a code sequence *)
diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v
index 57d7de4a..3570da2e 100644
--- a/ia32/Asmgenproof.v
+++ b/ia32/Asmgenproof.v
@@ -700,13 +700,16 @@ Opaque loadind.
   inv AT. monadInv H4. 
   exploit functions_transl; eauto. intro FN.
   generalize (transf_function_no_overflow _ _ H3); intro NOOV.
-  exploit annot_arguments_match; eauto. intros [vargs' [P Q]]. 
-  exploit external_call_mem_extends'; eauto.
+  exploit annot_args_match; eauto. intros [vargs' [P Q]]. 
+  exploit external_call_mem_extends; eauto.
   intros [vres' [m2' [A [B [C D]]]]].
   left. econstructor; split. apply plus_one. 
   eapply exec_step_annot. eauto. eauto.
   eapply find_instr_tail; eauto. eauto.
-  eapply external_call_symbols_preserved'; eauto.
+  erewrite <- sp_val by eauto. 
+  eapply eval_annot_args_preserved with (ge1 := ge); eauto.
+  exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   eapply match_states_intro with (ep := false); eauto with coqlib.
   unfold nextinstr. rewrite Pregmap.gss. 
diff --git a/ia32/SelectOp.vp b/ia32/SelectOp.vp
index b6aef725..74e3fbd7 100644
--- a/ia32/SelectOp.vp
+++ b/ia32/SelectOp.vp
@@ -507,3 +507,17 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   | _ => (Aindexed Int.zero, e:::Enil)
   end.
 
+(** ** Arguments of annotations *)
+
+Nondetfunction annot_arg (e: expr) :=
+  match e with
+  | Eop (Ointconst n) Enil => AA_int n
+  | Eop (Olea (Aglobal id ofs)) Enil => AA_addrglobal id ofs
+  | Eop (Olea (Ainstack ofs)) Enil => AA_addrstack ofs
+  | Eop Omakelong (Eop (Ointconst h) Enil ::: Eop (Ointconst l) Enil ::: Enil) =>
+        AA_long (Int64.ofwords h l)
+  | Eop Omakelong (h ::: l ::: Enil) => AA_longofwords (AA_base h) (AA_base l)
+  | Eload chunk (Aglobal id ofs) Enil => AA_loadglobal chunk id ofs
+  | Eload chunk (Ainstack ofs) Enil => AA_loadstack chunk ofs
+  | _ => AA_base e
+  end.
diff --git a/ia32/SelectOpproof.v b/ia32/SelectOpproof.v
index 50688621..50f0d9b6 100644
--- a/ia32/SelectOpproof.v
+++ b/ia32/SelectOpproof.v
@@ -898,4 +898,20 @@ Proof.
   exists (v :: nil); split. constructor; auto. constructor. subst; simpl. rewrite Int.add_zero; auto. 
 Qed.
 
+Theorem eval_annot_arg:
+  forall a v,
+  eval_expr ge sp e m nil a v ->
+  CminorSel.eval_annot_arg ge sp e m (annot_arg a) v.
+Proof.
+  intros until v. unfold annot_arg; case (annot_arg_match a); intros; InvEval.
+- constructor.
+- constructor.
+- constructor. 
+- simpl in H5. inv H5. constructor.
+- subst v. constructor; auto.
+- inv H. InvEval. simpl in H6; inv H6. constructor; auto.
+- inv H. InvEval. simpl in H6. inv H6. constructor; auto.
+- constructor; auto.
+Qed.
+
 End CMCONSTR.