Revised handling of annotation statements, and more generally built-in functions, and more generally external functions

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1672 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

22 files changed, 231 insertions, 76 deletions

diff --git a/backend/Bounds.v b/backend/Bounds.v
index 0415670..23fa3b5 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -75,6 +75,7 @@ Definition instr_within_bounds (i: instruction) :=
   | Lload chunk addr args dst => mreg_within_bounds dst
   | Lcall sig ros => size_arguments sig <= bound_outgoing b
   | Lbuiltin ef args res => mreg_within_bounds res
+  | Lannot ef args => forall s, In (S s) args -> slot_within_bounds s
   | _ => True
   end.
 
@@ -107,6 +108,7 @@ Definition regs_of_instr (i: instruction) : list mreg :=
   | Lcall sig ros => nil
   | Ltailcall sig ros => nil
   | Lbuiltin ef args res => res :: nil
+  | Lannot ef args => nil
   | Llabel lbl => nil
   | Lgoto lbl => nil
   | Lcond cond args lbl => nil
@@ -114,10 +116,18 @@ Definition regs_of_instr (i: instruction) : list mreg :=
   | Lreturn => nil
   end.
 
+Fixpoint slots_of_locs (l: list loc) : list slot :=
+  match l with
+  | nil => nil
+  | S s :: l' => s :: slots_of_locs l'
+  | R r :: l' => slots_of_locs l'
+  end.
+
 Definition slots_of_instr (i: instruction) : list slot :=
   match i with
   | Lgetstack s r => s :: nil
   | Lsetstack r s => s :: nil
+  | Lannot ef args => slots_of_locs args
   | _ => nil
   end.
 
@@ -343,6 +353,14 @@ Proof.
   split. simpl in H1. exact H1. eapply outgoing_slot_bound; eauto.
 Qed.
 
+Lemma slots_of_locs_charact:
+  forall s l, In s (slots_of_locs l) <-> In (S s) l.
+Proof.
+  induction l; simpl; intros. 
+  tauto.
+  destruct a; simpl; intuition congruence.
+Qed.
+
 (** It follows that every instruction in the function is within bounds, 
     in the sense of the [instr_within_bounds] predicate. *)
 
@@ -356,9 +374,16 @@ Proof.
   destruct i;
   generalize (mreg_is_within_bounds _ H); generalize (slot_is_within_bounds _ H); 
   simpl; intros; auto.
+(* getstack *)
   inv H0. split; auto.
+(* setstack *)
   inv H0; auto.
+(* call *)
   eapply size_arguments_bound; eauto.
+(* annot *)
+  inv H0. apply H1. rewrite slots_of_locs_charact; auto. 
+  generalize (H8 _ H3). unfold loc_acceptable, slot_valid. 
+  destruct s; (contradiction || omega).
 Qed.
 
 Lemma function_is_within_bounds:
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index 1cd245e..0b48c0f 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -352,7 +352,7 @@ proc:
                    fn_stackspace = $8;
                    fn_body = $10 }) }
   | EXTERN STRINGLIT COLON signature 
-      { Coq_pair($2, External({ef_id = $2; ef_sig = $4; ef_inline = false})) }
+      { Coq_pair($2, External(EF_external($2, $4))) }
 ;
 
 signature:
diff --git a/backend/LTLintyping.v b/backend/LTLintyping.v
index c928f3f..1a20f73 100644
--- a/backend/LTLintyping.v
+++ b/backend/LTLintyping.v
@@ -73,7 +73,7 @@ Inductive wt_instr : instruction -> Prop :=
       forall ef args res,
       List.map Loc.type args = (ef_sig ef).(sig_args) ->
       Loc.type res = proj_sig_res (ef_sig ef) ->
-      arity_ok (ef_sig ef).(sig_args) = true ->
+      arity_ok (ef_sig ef).(sig_args) = true \/ ef_reloads ef = false ->
       locs_acceptable args -> loc_acceptable res ->
        wt_instr (Lbuiltin ef args res)
   | wt_Llabel: forall lbl,
diff --git a/backend/LTLtyping.v b/backend/LTLtyping.v
index 791c755..40a584f 100644
--- a/backend/LTLtyping.v
+++ b/backend/LTLtyping.v
@@ -94,7 +94,7 @@ Inductive wt_instr : instruction -> Prop :=
       forall ef args res s,
       List.map Loc.type args = (ef_sig ef).(sig_args) ->
       Loc.type res = proj_sig_res (ef_sig ef) ->
-      arity_ok (ef_sig ef).(sig_args) = true ->
+      arity_ok (ef_sig ef).(sig_args) = true \/ ef_reloads ef = false ->
       locs_acceptable args -> loc_acceptable res ->
       valid_successor s ->
       wt_instr (Lbuiltin ef args res s)
diff --git a/backend/Linear.v b/backend/Linear.v
index 31c3fed..23f0324 100644
--- a/backend/Linear.v
+++ b/backend/Linear.v
@@ -44,6 +44,7 @@ Inductive instruction: Type :=
   | Lcall: signature -> mreg + ident -> instruction
   | Ltailcall: signature -> mreg + ident -> instruction
   | Lbuiltin: external_function -> list mreg -> mreg -> instruction
+  | Lannot: external_function -> list loc -> instruction
   | Llabel: label -> instruction
   | Lgoto: label -> instruction
   | Lcond: condition -> list mreg -> label -> instruction
@@ -296,6 +297,11 @@ Inductive step: state -> trace -> state -> Prop :=
       external_call ef ge (reglist rs args) m t v m' ->
       step (State s f sp (Lbuiltin ef args res :: b) rs m)
          t (State s f sp b (Locmap.set (R res) v (undef_temps 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' ->
+      step (State s f sp (Lannot ef args :: b) rs m)
+         t (State s f sp b rs m')
   | exec_Llabel:
       forall s f sp lbl b rs m,
       step (State s f sp (Llabel lbl :: b) rs m)
diff --git a/backend/Lineartyping.v b/backend/Lineartyping.v
index ef6194c..390b630 100644
--- a/backend/Lineartyping.v
+++ b/backend/Lineartyping.v
@@ -93,6 +93,12 @@ Inductive wt_instr : instruction -> Prop :=
       mreg_type res = proj_sig_res (ef_sig ef) ->
       arity_ok (ef_sig ef).(sig_args) = true ->
       wt_instr (Lbuiltin ef args res)
+  | wt_Lannot:
+      forall ef args,
+      List.map Loc.type args = (ef_sig ef).(sig_args) ->
+      ef_reloads ef = false ->
+      locs_acceptable args ->
+      wt_instr (Lannot ef args)
   | wt_Llabel:
       forall lbl,
       wt_instr (Llabel lbl)
diff --git a/backend/Mach.v b/backend/Mach.v
index 223d5ab..3210a9e 100644
--- a/backend/Mach.v
+++ b/backend/Mach.v
@@ -60,11 +60,16 @@ Inductive instruction: Type :=
   | Mcall: signature -> mreg + ident -> instruction
   | Mtailcall: signature -> mreg + ident -> instruction
   | Mbuiltin: external_function -> list mreg -> mreg -> instruction
+  | Mannot: external_function -> list annot_param -> instruction
   | Mlabel: label -> instruction
   | Mgoto: label -> instruction
   | Mcond: condition -> list mreg -> label -> instruction
   | Mjumptable: mreg -> list label -> instruction
-  | Mreturn: instruction.
+  | Mreturn: instruction
+
+with annot_param: Type :=
+  | APreg: mreg -> annot_param
+  | APstack: memory_chunk -> Z -> annot_param.
 
 Definition code := list instruction.
 
@@ -87,7 +92,12 @@ Definition funsig (fd: fundef) :=
 
 Definition genv := Genv.t fundef unit.
 
-(** * Dynamic semantics *)
+(** * Elements of dynamic semantics *)
+
+(** The operational semantics is in module [Machsem]. *)
+
+Definition chunk_of_type (ty: typ) :=
+  match ty with Tint => Mint32 | Tfloat => Mfloat64 end.
 
 Module RegEq.
   Definition t := mreg.
diff --git a/backend/Machsem.v b/backend/Machsem.v
index 1a167a9..fe0ec37 100644
--- a/backend/Machsem.v
+++ b/backend/Machsem.v
@@ -56,16 +56,13 @@ function.  The [return_address_offset] predicate from module
 the Asm code generated later will store in the reserved location.
 *)
 
-Definition chunk_of_type (ty: typ) :=
-  match ty with Tint => Mint32 | Tfloat => Mfloat64 end.
-
 Definition load_stack (m: mem) (sp: val) (ty: typ) (ofs: int) :=
   Mem.loadv (chunk_of_type ty) m (Val.add sp (Vint ofs)).
 
 Definition store_stack (m: mem) (sp: val) (ty: typ) (ofs: int) (v: val) :=
   Mem.storev (chunk_of_type ty) m (Val.add sp (Vint ofs)) v.
 
-(** Extract the values of the arguments of an external call. *)
+(** Extract the values of the arguments to an external call. *)
 
 Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop :=
   | extcall_arg_reg: forall rs m sp r,
@@ -74,16 +71,22 @@ Inductive extcall_arg: regset -> mem -> val -> loc -> val -> Prop :=
       load_stack m sp ty (Int.repr (Stacklayout.fe_ofs_arg + 4 * ofs)) = Some v ->
       extcall_arg rs m sp (S (Outgoing ofs ty)) v.
 
-Inductive extcall_args: regset -> mem -> val -> list loc -> list val -> Prop :=
-  | extcall_args_nil: forall rs m sp,
-      extcall_args rs m sp nil nil
-  | extcall_args_cons: forall rs m sp l1 ll v1 vl,
-      extcall_arg rs m sp l1 v1 -> extcall_args rs m sp ll vl ->
-      extcall_args rs m sp (l1 :: ll) (v1 :: vl).
-
 Definition extcall_arguments
-   (rs: regset) (m: mem) (sp: val) (sg: signature) (args: list val) : Prop :=
-  extcall_args rs m sp (loc_arguments sg) args.
+    (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. *)
 
@@ -193,6 +196,12 @@ Inductive step: state -> trace -> state -> Prop :=
       external_call ef ge rs##args m t v m' ->
       step (State s f sp (Mbuiltin ef args res :: b) rs m)
          t (State s f sp b ((undef_temps rs)#res <- v) 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' ->
+      step (State s f sp (Mannot ef args :: b) rs m)
+         t (State s f sp b rs m')
   | exec_Mgoto:
       forall s fb f sp lbl c rs m c',
       Genv.find_funct_ptr ge fb = Some (Internal f) ->
diff --git a/backend/Machtyping.v b/backend/Machtyping.v
index 95ceafe..2d8c83d 100644
--- a/backend/Machtyping.v
+++ b/backend/Machtyping.v
@@ -77,6 +77,10 @@ Inductive wt_instr : instruction -> Prop :=
       List.map mreg_type args = (ef_sig ef).(sig_args) ->
       mreg_type res = proj_sig_res (ef_sig ef) ->
       wt_instr (Mbuiltin ef args res)
+  | wt_Mannot:
+      forall ef args,
+      ef_reloads ef = false ->
+      wt_instr (Mannot ef args)
   | wt_Mgoto:
       forall lbl,
       wt_instr (Mgoto lbl)
diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml
index cce00f6..3bfd803 100644
--- a/backend/PrintLTL.ml
+++ b/backend/PrintLTL.ml
@@ -20,11 +20,10 @@ open AST
 open Integers
 open Locations
 open LTL
+open PrintAST
 open PrintOp
 open PrintRTL
 
-let name_of_typ = function Tint -> "int" | Tfloat -> "float"
-
 let loc pp l =
   match l with
   | R r ->
@@ -78,6 +77,10 @@ let print_instruction pp (pc, i) =
   | Ltailcall(sg, fn, args) ->
       fprintf pp "tailcall %a(%a)@ "
         ros fn locs args
+  | Lbuiltin(ef, args, res, s) ->
+      fprintf pp "%a = builtin %s(%a)@ "
+        loc res (name_of_external ef) locs args;
+      print_succ pp s (Int32.pred pc)
   | Lcond(cond, args, s1, s2) ->
       fprintf pp "if (%a) goto %ld else goto %ld@ "
         (print_condition loc) (cond, args)
diff --git a/backend/PrintLTLin.ml b/backend/PrintLTLin.ml
index e0a3204..adff483 100644
--- a/backend/PrintLTLin.ml
+++ b/backend/PrintLTLin.ml
@@ -21,21 +21,9 @@ open Integers
 open Locations
 open Machregsaux
 open LTLin
+open PrintAST
 open PrintOp
 
-let name_of_chunk = function
-  | Mint8signed -> "int8signed"
-  | Mint8unsigned -> "int8unsigned"
-  | Mint16signed -> "int16signed"
-  | Mint16unsigned -> "int16unsigned"
-  | Mint32 -> "int32"
-  | Mfloat32 -> "float32"
-  | Mfloat64 -> "float64"
-
-let name_of_type = function
-  | Tint -> "int"
-  | Tfloat -> "float"
-
 let reg pp loc =
   match loc with
   | R r ->
@@ -80,8 +68,8 @@ let print_instruction pp i =
       fprintf pp "tailcall %a(%a)@ "
         ros fn regs args
   | Lbuiltin(ef, args, res) ->
-      fprintf pp "%a = builtin \"%s\"(%a)@ "
-        reg res (extern_atom ef.ef_id) regs args
+      fprintf pp "%a = builtin %s(%a)@ "
+        reg res (name_of_external ef) regs args
   | Llabel lbl ->
       fprintf pp "%ld:@ " (camlint_of_positive lbl)
   | Lgoto lbl ->
diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml
index 5b4887e..a6a1cc5 100644
--- a/backend/PrintMach.ml
+++ b/backend/PrintMach.ml
@@ -21,21 +21,9 @@ open Integers
 open Locations
 open Machregsaux
 open Mach
+open PrintAST
 open PrintOp
 
-let name_of_chunk = function
-  | Mint8signed -> "int8signed"
-  | Mint8unsigned -> "int8unsigned"
-  | Mint16signed -> "int16signed"
-  | Mint16unsigned -> "int16unsigned"
-  | Mint32 -> "int32"
-  | Mfloat32 -> "float32"
-  | Mfloat64 -> "float64"
-
-let name_of_type = function
-  | Tint -> "int"
-  | Tfloat -> "float"
-
 let reg pp r =
   match name_of_register r with
   | Some s -> fprintf pp "%s" s
@@ -46,6 +34,15 @@ let rec regs pp = function
   | [r] -> reg pp r
   | r1::rl -> fprintf pp "%a, %a" reg r1 regs rl
 
+let annot_param pp = function
+  | APreg r -> reg pp r
+  | APstack(chunk, ofs) -> fprintf pp "stack(%s,%ld)" (name_of_chunk chunk) (camlint_of_coqint ofs)
+
+let rec annot_params pp = function
+  | [] -> ()
+  | [r] -> annot_param pp r
+  | r1::rl -> fprintf pp "%a, %a" annot_param r1 annot_params rl
+
 let ros pp = function
   | Coq_inl r -> reg pp r
   | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
@@ -78,8 +75,10 @@ let print_instruction pp i =
   | Mtailcall(sg, fn) ->
       fprintf pp "tailcall %a@ " ros fn
   | Mbuiltin(ef, args, res) ->
-      fprintf pp "%a = builtin \"%s\"(%a)@ "
-        reg res (extern_atom ef.ef_id) regs args
+      fprintf pp "%a = builtin %s(%a)@ "
+        reg res (name_of_external ef) regs args
+  | Mannot(ef, args) ->
+      fprintf pp "%s(%a)@ " (name_of_external ef) annot_params args
   | Mlabel lbl ->
       fprintf pp "%ld:@ " (camlint_of_positive lbl)
   | Mgoto lbl ->
diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml
index 62ee2c9..620a949 100644
--- a/backend/PrintRTL.ml
+++ b/backend/PrintRTL.ml
@@ -19,19 +19,11 @@ open Maps
 open AST
 open Integers
 open RTL
+open PrintAST
 open PrintOp
 
 (* Printing of RTL code *)
 
-let name_of_chunk = function
-  | Mint8signed -> "int8signed"
-  | Mint8unsigned -> "int8unsigned"
-  | Mint16signed -> "int16signed"
-  | Mint16unsigned -> "int16unsigned"
-  | Mint32 -> "int32"
-  | Mfloat32 -> "float32"
-  | Mfloat64 -> "float64"
-
 let reg pp r =
   fprintf pp "x%ld" (camlint_of_positive r)
 
@@ -79,8 +71,8 @@ let print_instruction pp (pc, i) =
       fprintf pp "tailcall %a(%a)@ "
         ros fn regs args
   | Ibuiltin(ef, args, res, s) ->
-      fprintf pp "%a = builtin \"%s\"(%a)@ "
-        reg res (extern_atom ef.ef_id) regs args;
+      fprintf pp "%a = builtin %s(%a)@ "
+        reg res (name_of_external ef) regs args;
       print_succ pp s (Int32.pred pc)
   | Icond(cond, args, s1, s2) ->
       fprintf pp "if (%a) goto %ld else goto %ld@ "
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 49f339d..02359b9 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -110,7 +110,7 @@ Inductive wt_instr : instruction -> Prop :=
       forall ef args res s,
       List.map env args = (ef_sig ef).(sig_args) ->
       env res = proj_sig_res (ef_sig ef) ->
-      arity_ok (ef_sig ef).(sig_args) = true ->
+      arity_ok (ef_sig ef).(sig_args) = true \/ ef_reloads ef = false ->
       valid_successor s ->
       wt_instr (Ibuiltin ef args res s)
   | wt_Icond:
@@ -236,7 +236,7 @@ Definition check_instr (i: instruction) : bool :=
   | Ibuiltin ef args res s =>
       check_regs args (ef_sig ef).(sig_args)
       && check_reg res (proj_sig_res (ef_sig ef))
-      && arity_ok (ef_sig ef).(sig_args)
+      && (if ef_reloads ef then arity_ok (ef_sig ef).(sig_args) else true)
       && check_successor s
   | Icond cond args s1 s2 =>
       check_regs args (type_of_condition cond)
@@ -349,6 +349,7 @@ Proof.
   apply check_regs_correct; auto.
   apply check_reg_correct; auto.
   auto.
+  destruct (ef_reloads e); auto. 
   apply check_successor_correct; auto.
   (* cond *)
   constructor. apply check_regs_correct; auto.
diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml
index 7549ff4..17acbc6 100644
--- a/backend/RTLtypingaux.ml
+++ b/backend/RTLtypingaux.ml
@@ -20,6 +20,7 @@ open Memdata
 open Op
 open Registers
 open RTL
+open PrintAST
 
 exception Type_error of string
 
@@ -93,11 +94,11 @@ let type_instr retty (Coq_pair(pc, i)) =
         let sg = ef_sig ef in
         set_types args sg.sig_args;
         set_type res (match sg.sig_res with None -> Tint | Some ty -> ty);
-        if not (Conventions.arity_ok sg.sig_args) then
+        if ef_reloads ef && not (Conventions.arity_ok sg.sig_args) then
           raise(Type_error "wrong arity")
       with Type_error msg ->
         raise(Type_error (Printf.sprintf "type mismatch in Ibuiltin(%s): %s"
-                                         (extern_atom ef.ef_id) msg))
+                                         (name_of_external ef) msg))
       end
   | Icond(cond, args, _, _) ->
       set_types args (type_of_condition cond)
diff --git a/backend/Reload.v b/backend/Reload.v
index 81b6199..0ad53e6 100644
--- a/backend/Reload.v
+++ b/backend/Reload.v
@@ -236,10 +236,13 @@ Definition transf_instr
             (Ltailcall sig (inr _ id) :: k)
       end
   | LTLin.Lbuiltin ef args dst =>
-      let rargs := regs_for args in
-      let rdst := reg_for dst in
-      add_reloads args rargs
-        (Lbuiltin ef rargs rdst :: add_spill rdst dst k)
+      if ef_reloads ef then
+       (let rargs := regs_for args in
+        let rdst := reg_for dst in
+        add_reloads args rargs
+          (Lbuiltin ef rargs rdst :: add_spill rdst dst k))
+      else
+        Lannot ef args :: k
   | LTLin.Llabel lbl =>
       Llabel lbl :: k
   | LTLin.Lgoto lbl =>
diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v
index 09a9101..49640a3 100644
--- a/backend/Reloadproof.v
+++ b/backend/Reloadproof.v
@@ -799,7 +799,7 @@ Proof.
     FL. FL. 
   destruct s0; FL; FL; FL.
   destruct s0; FL; FL; FL.
-  FL.
+  destruct (ef_reloads e). FL. FL. FL.
   destruct o; FL.
 Qed.
 
@@ -1254,8 +1254,9 @@ Proof.
 
   (* Lbuiltin *)
   ExploitWT; inv WTI.
+  case_eq (ef_reloads ef); intro RELOADS.
   exploit add_reloads_correct.
-    instantiate (1 := args). apply arity_ok_enough. rewrite H3. auto. auto.
+    instantiate (1 := args). apply arity_ok_enough. rewrite H3. destruct H5. auto. congruence. auto.
   intros [ls2 [A [B C]]].
   exploit external_call_mem_extends; eauto. 
   apply agree_locs; eauto. 
@@ -1273,6 +1274,19 @@ Proof.
   rewrite E. rewrite Locmap.gss. auto.
   intros. rewrite F; auto. rewrite Locmap.gso. rewrite undef_temps_others; auto. 
   apply reg_for_diff; auto.
+  (* no reload *)
+  exploit external_call_mem_extends; eauto. 
+  apply agree_locs; eauto. 
+  intros [v' [tm' [P [Q [R S]]]]].
+  assert (EQ: v = Vundef).
+    destruct ef; simpl in RELOADS; try congruence. simpl in H; inv H. auto.
+  subst v.
+  left; econstructor; split.
+  apply plus_one. eapply exec_Lannot.
+  eapply external_call_symbols_preserved; eauto.
+  exact symbols_preserved. exact varinfo_preserved.
+  econstructor; eauto with coqlib.
+  apply agree_set with ls; auto.
 
   (* Llabel *)
   left; econstructor; split.
diff --git a/backend/Reloadtyping.v b/backend/Reloadtyping.v
index 60be59b..eba5ad6 100644
--- a/backend/Reloadtyping.v
+++ b/backend/Reloadtyping.v
@@ -33,9 +33,7 @@ Require Import Reloadproof.
   generate well-typed instruction sequences,
   given sufficient typing and well-formedness hypotheses over the locations involved. *)
 
-Hint Resolve wt_Lgetstack wt_Lsetstack wt_Lopmove
-             wt_Lop wt_Lload wt_Lstore wt_Lcall wt_Ltailcall wt_Lbuiltin
-             wt_Llabel wt_Lgoto wt_Lcond wt_Ljumptable wt_Lreturn: reloadty.
+Hint Constructors wt_instr: reloadty.
 
 Remark wt_code_cons:
   forall f i c, wt_instr f i -> wt_code f c -> wt_code f (i :: c).
@@ -292,9 +290,12 @@ Proof.
   destruct ros. destruct H2 as [A [B C]]. auto 10 with reloadty. 
   auto 10 with reloadty.
 
+  destruct (ef_reloads ef) as [] _eqn.
+  assert (arity_ok (sig_args (ef_sig ef)) = true) by intuition congruence.
   assert (map mreg_type (regs_for args) = map Loc.type args).
     apply wt_regs_for. apply arity_ok_enough. congruence.
   assert (mreg_type (reg_for res) = Loc.type res). eauto with reloadty.
+  auto 10 with reloadty.
   auto with reloadty.
 
 
diff --git a/backend/Selection.v b/backend/Selection.v
index 9e11bc3..9c037b8 100644
--- a/backend/Selection.v
+++ b/backend/Selection.v
@@ -184,7 +184,7 @@ Definition expr_is_addrof_builtin (ge: Cminor.genv) (e: Cminor.expr) : option ex
       | None => None
       | Some b =>
           match Genv.find_funct_ptr ge b with
-          | Some(External ef) => if ef.(ef_inline) then Some ef else None
+          | Some(External ef) => if ef_inline ef then Some ef else None
           | _ => None
           end
       end
diff --git a/backend/Stacking.v b/backend/Stacking.v
index 09d98d6..23a112c 100644
--- a/backend/Stacking.v
+++ b/backend/Stacking.v
@@ -130,6 +130,16 @@ Definition transl_op (fe: frame_env) (op: operation) :=
 Definition transl_addr (fe: frame_env) (addr: addressing) :=
   shift_stack_addressing (Int.repr fe.(fe_stack_data)) addr.
 
+(** 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 *)
+  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
@@ -173,6 +183,8 @@ Definition transl_instr
         (Mtailcall sig ros :: k)
   | Lbuiltin ef args dst =>
       Mbuiltin ef args dst :: k
+  | Lannot ef args =>
+      Mannot ef (map (transl_annot_param fe) args) :: k
   | Llabel lbl =>
       Mlabel lbl :: k
   | Lgoto lbl =>
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index d651220..fbe8882 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -2172,7 +2172,7 @@ Lemma transl_external_arguments_rec:
   forall locs,
   incl locs (loc_arguments sg) ->
   exists vl,
-  extcall_args rs m' (parent_sp cs') locs vl /\ val_list_inject j ls##locs vl.
+  list_forall2 (extcall_arg rs m' (parent_sp cs')) locs vl /\ val_list_inject j ls##locs vl.
 Proof.
   induction locs; simpl; intros.
   exists (@nil val); split. constructor. constructor.
@@ -2193,6 +2193,61 @@ Qed.
 
 End EXTERNAL_ARGUMENTS.
 
+(** Preservation of the arguments to an annotation. *)
+
+Section ANNOT_ARGUMENTS.
+
+Variable f: Linear.function.
+Let b := function_bounds f.
+Let fe := make_env b.
+Variable j: meminj.
+Variables m m': mem.
+Variables ls ls0: locset.
+Variable rs: regset.
+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_acceptable l -> 
+  match l with S s => slot_within_bounds f b s | _ => 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; red in H. 
+(* reg *)
+  exists (rs m0); split. constructor. auto.
+(* stack *) 
+  destruct s; try contradiction.
+  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,
+  locs_acceptable ll ->
+  (forall s, In (S s) ll -> slot_within_bounds f b s) ->
+  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; intros. 
+  exists (@nil val); split; constructor.
+  exploit (transl_annot_param_correct a). 
+    apply H; auto with coqlib.
+    destruct a; auto with coqlib.
+  intros [v1 [A B]].
+  exploit IHll.
+    red; intros; apply H; auto with coqlib.
+    intros; apply H0; auto with coqlib.
+  intros [vl [C D]].
+  exists (v1 :: vl); split; constructor; auto.
+Qed.
+
+End ANNOT_ARGUMENTS.
+
 (** The proof of semantic preservation relies on simulation diagrams
   of the following form:
 <<
@@ -2466,6 +2521,29 @@ Proof.
   eapply agree_valid_mach; eauto.
   inv WTI. simpl; rewrite H4. eapply external_call_well_typed; eauto.
 
+  (* Lannot *)
+  inv WTI.
+  exploit transl_annot_params_correct; eauto.
+  intros [vargs' [P Q]]. 
+  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.
+  exact symbols_preserved. exact varinfo_preserved.
+  econstructor; eauto with coqlib.
+  eapply match_stack_change_extcall; eauto.
+  apply Zlt_le_weak. change (Mem.valid_block m sp0). eapply agree_valid_linear; eauto.
+  apply Zlt_le_weak. 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.
+  eapply external_call_bounds; eauto. eapply agree_valid_linear; eauto.
+  eapply external_call_valid_block; eauto.
+  eapply agree_valid_mach; eauto.
+
   (* Llabel *)
   econstructor; split.
   apply plus_one; apply exec_Mlabel.
diff --git a/backend/Stackingtyping.v b/backend/Stackingtyping.v
index d00d1b2..27de557 100644
--- a/backend/Stackingtyping.v
+++ b/backend/Stackingtyping.v
@@ -179,6 +179,9 @@ Proof.
   (* builtin *)
   apply wt_instrs_cons; auto.
   constructor; auto.
+  (* annot *)
+  apply wt_instrs_cons; auto.
+  constructor; auto.
   (* label *)
   apply wt_instrs_cons; auto.
   constructor.