Upgrade the ARM port to the new builtins.

8 files changed, 256 insertions, 209 deletions

diff --git a/arm/Asm.v b/arm/Asm.v
index 4e8a411a..1fd792b8 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -205,14 +205,13 @@ Inductive instruction : Type :=
   | Ploadsymbol: ireg -> ident -> int -> instruction (**r load the address of a symbol *)
   | Pmovite: testcond -> ireg -> shift_op -> shift_op -> instruction (**r integer conditional move *)
   | Pbtbl: ireg -> list label -> instruction       (**r N-way branch through a jump table *)
-  | Pbuiltin: external_function -> list preg -> list preg -> instruction  (**r built-in function *)
-  | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement *)
+  | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *)
   | Padc: ireg -> ireg -> shift_op -> instruction     (**r add with carry *)
   | Pcfi_adjust: int -> instruction                   (**r .cfi_adjust debug directive *)
-  | Pclz: preg -> preg -> instruction                 (**r count leading zeros. *)
+  | Pclz: ireg -> ireg -> instruction                 (**r count leading zeros. *)
   | Pfsqrt: freg -> freg -> instruction               (**r floating-point square root. *)
-  | Prev: preg -> preg -> instruction                 (**r reverse bytes and reverse bits. *)
-  | Prev16: preg -> preg -> instruction               (**r reverse bytes and reverse bits. *)
+  | Prev: ireg -> ireg -> instruction                 (**r reverse bytes and reverse bits. *)
+  | Prev16: ireg -> ireg -> instruction               (**r reverse bytes and reverse bits. *)
   | Prsc: ireg -> ireg -> shift_op -> instruction     (**r reverse subtract without carry. *)
   | Psbc: ireg -> ireg -> shift_op -> instruction     (**r add with carry *)
   (* Add, sub, rsb versions with s suffix *)
@@ -319,6 +318,15 @@ Fixpoint set_regs (rl: list preg) (vl: list val) (rs: regset) : regset :=
   | _, _ => rs
   end.
 
+(** Assigning the result of a builtin *)
+
+Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
+  match res with
+  | BR r => rs#r <- v
+  | BR_none => rs
+  | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
+  end.
+
 Section RELSEM.
 
 (** Looking up instructions in a code sequence by position. *)
@@ -748,7 +756,6 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       | _ => Stuck
       end
   | Pbuiltin ef args res => Stuck    (**r treated specially below *)
-  | Pannot ef args => Stuck          (**r treated specially below *)
   (** The following instructions and directives are not generated directly by Asmgen,
       so we do not model them. *)
   | Ppush _
@@ -827,23 +834,16 @@ Inductive step: state -> trace -> state -> Prop :=
       exec_instr f i rs m = Next rs' m' ->
       step (State rs m) E0 (State rs' m')
   | exec_step_builtin:
-      forall b ofs f ef args res rs m t vl rs' m',
+      forall b ofs f ef args res rs m vargs t vres rs' m',
       rs PC = Vptr b ofs ->
       Genv.find_funct_ptr ge b = Some (Internal f) ->
-      find_instr (Int.unsigned ofs) (fn_code f) = Some (Pbuiltin ef args res) ->
-      external_call' ef ge (map rs args) m t vl m' ->
-      rs' = nextinstr 
-              (set_regs res vl
+      find_instr (Int.unsigned ofs) f.(fn_code) = Some (Pbuiltin ef args res) ->
+      eval_builtin_args ge rs (rs SP) m args vargs ->
+      external_call ef ge vargs m t vres m' ->
+      rs' = nextinstr
+              (set_res res vres
                 (undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) ->
       step (State rs m) t (State rs' m')
-  | exec_step_annot:
-      forall b ofs f ef args rs m vargs t v m',
-      rs PC = Vptr b ofs ->
-      Genv.find_funct_ptr ge b = Some (Internal f) ->
-      find_instr (Int.unsigned ofs) (fn_code f) = Some (Pannot ef args) ->
-      eval_annot_args ge rs (rs SP) m args vargs ->
-      external_call ef ge vargs m t v m' ->
-      step (State rs m) t (State (nextinstr rs) m')
   | exec_step_external:
       forall b ef args res rs m t rs' m',
       rs PC = Vptr b Int.zero ->
@@ -907,12 +907,8 @@ Ltac Equalities :=
   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 eval_annot_args_determ; eauto). subst vargs0.
-  exploit external_call_determ. eexact H5. eexact H13. intros [A B].
+  assert (vargs0 = vargs) by (eapply eval_builtin_args_determ; eauto). subst vargs0.
+  exploit external_call_determ. eexact H5. eexact H11. intros [A B].
   split. auto. intros. destruct B; auto. subst. auto.
   assert (args0 = args) by (eapply extcall_arguments_determ; eauto). subst args0.
   exploit external_call_determ'. eexact H3. eexact H8. intros [A B].
@@ -921,7 +917,6 @@ Ltac Equalities :=
   red; intros; inv H; simpl.
   omega.
   inv H3; eapply external_call_trace_length; eauto.
-  eapply external_call_trace_length; eauto.
   inv H2; eapply external_call_trace_length; eauto.
 (* initial states *)
   inv H; inv H0. f_equal. congruence.
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml
index ca30924c..d13015ff 100644
--- a/arm/Asmexpand.ml
+++ b/arm/Asmexpand.ml
@@ -21,6 +21,8 @@ open AST
 open Camlcoq
 open Integers
 
+exception Error of string
+
 (* Useful constants and helper functions *)
 
 let _0 = Integers.Int.zero
@@ -74,51 +76,83 @@ let expand_int64_arith conflict rl fn =
 (* Handling of annotations *)
 
 let expand_annot_val txt targ args res =
-  emit (Pannot (EF_annot(txt,[targ]), List.map (fun r -> AA_base r) args));
+  emit (Pbuiltin (EF_annot(txt,[targ]), args, BR_none));
   match args, res with
-  | [IR src], [IR dst] ->
+  | [BA(IR src)], BR(IR dst) ->
      if dst <> src then emit (Pmov (dst,SOreg src))
-  | [FR src], [FR dst] ->
+  | [BA(FR src)], BR(FR dst) ->
      if dst <> src then emit (Pfcpyd (dst,src))
-  | _, _ -> assert false
-
+  | _, _ ->
+     raise (Error "ill-formed __builtin_annot_val")
 
 (* Handling of memcpy *)
 
 (* The ARM has strict alignment constraints for 2 and 4 byte accesses.
    8-byte accesses must be 4-aligned. *)
 
+let offset_in_range ofs =
+  let n = camlint_of_coqint ofs in n <= 128l && n >= -128l
+
+let memcpy_small_arg sz arg tmp =
+  match arg with
+  | BA (IR r) ->
+      (r, _0)
+  | BA_addrstack ofs ->
+      if offset_in_range ofs
+      && offset_in_range (Int.add ofs (Int.repr (Z.of_uint sz)))
+      then (IR13, ofs)
+      else begin expand_addimm tmp IR13 ofs; (tmp, _0) end
+  | _ ->
+      assert false
+
 let expand_builtin_memcpy_small sz al src dst =
-  let rec copy ofs sz  =
+  let (tsrc, tdst) = 
+    if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in
+  let (rsrc, osrc) = memcpy_small_arg sz src tsrc in
+  let (rdst, odst) = memcpy_small_arg sz dst tdst in
+  let rec copy osrc odst sz  =
     if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin
-      emit (Pfldd (FR7,src,ofs));
-      emit (Pfstd (FR7,dst,ofs));
-      copy (Int.add ofs _8) (sz - 8)
+      emit (Pfldd (FR7,rsrc,osrc));
+      emit (Pfstd (FR7,rdst,odst));
+      copy (Int.add osrc _8) (Int.add odst _8) (sz - 8)
     end else if sz >= 4 && al >= 4 then begin
-      emit (Pldr (IR14,src,SOimm ofs));
-      emit (Pstr (IR14,dst,SOimm ofs));
-      copy (Int.add ofs _4) (sz - 4)
+      emit (Pldr (IR14,rsrc,SOimm osrc));
+      emit (Pstr (IR14,rdst,SOimm odst));
+      copy (Int.add osrc _4) (Int.add odst _4) (sz - 4)
     end else if sz >= 2 && al >= 2 then begin
-      emit (Pldrh (IR14,src,SOimm ofs));
-      emit (Pstrh (IR14,dst,SOimm ofs));
-      copy (Int.add ofs _2) (sz - 2)
+      emit (Pldrh (IR14,rsrc,SOimm osrc));
+      emit (Pstrh (IR14,rdst,SOimm odst));
+      copy (Int.add osrc _2) (Int.add odst _2) (sz - 2)
     end else if sz >= 1 then begin
-      emit (Pldrb (IR14,src,SOimm ofs));
-      emit (Pstrb (IR14,dst,SOimm ofs));
-      copy (Int.add ofs _1) (sz - 1)
-    end else
-      () in
-  copy _0 sz
+      emit (Pldrb (IR14,rsrc,SOimm osrc));
+      emit (Pstrb (IR14,rdst,SOimm odst));
+      copy (Int.add osrc _1) (Int.add odst _1) (sz - 1)
+    end in
+  copy osrc odst sz
+
+let memcpy_big_arg arg tmp =
+  match arg with
+  | BA (IR r) ->
+      if r <> tmp then emit (Pmov(tmp, SOreg r))
+  | BA_addrstack ofs ->
+      expand_addimm tmp IR13 ofs
+  | _ ->
+      assert false
 
 let expand_builtin_memcpy_big sz al src dst =
   assert (sz >= al);
   assert (sz mod al = 0);
-  assert (src = IR2);
-  assert (dst = IR3);
+  let (s, d) = 
+    if dst <> BA (IR IR2) then (IR2, IR3) else (IR3, IR2) in
+  memcpy_big_arg src s;
+  memcpy_big_arg dst d;
   let (load, store, chunksize) =
-    if al >= 4 then (Pldr_p (IR12,src,SOimm _4), Pstr_p (IR12,dst,SOimm _4) , 4)
-    else if al = 2 then (Pldrh_p (IR12,src,SOimm _2), Pstrh_p (IR12,dst,SOimm _2), 2)
-    else (Pldrb_p (IR12,src,SOimm _1), Pstrb_p (IR12,dst,SOimm _1), 1) in
+    if al >= 4 then
+      (Pldr_p (IR12,s,SOimm _4), Pstr_p (IR12,d,SOimm _4) , 4)
+    else if al = 2 then
+       (Pldrh_p (IR12,s,SOimm _2), Pstrh_p (IR12,d,SOimm _2), 2)
+    else
+       (Pldrb_p (IR12,s,SOimm _1), Pstrb_p (IR12,d,SOimm _1), 1) in
   expand_movimm IR14 (coqint_of_camlint (Int32.of_int (sz / chunksize)));
   let lbl = new_label () in
   emit (Plabel lbl);
@@ -129,71 +163,93 @@ let expand_builtin_memcpy_big sz al src dst =
 
 let expand_builtin_memcpy  sz al args =
   let (dst, src) =
-    match args with [IR d; IR s] -> (d, s) | _ -> assert false in
+    match args with [d; s] -> (d, s) | _ -> assert false in
   if sz <= 32
   then expand_builtin_memcpy_small sz al src dst
   else expand_builtin_memcpy_big sz al src dst
 
 (* Handling of volatile reads and writes *)
 
-let expand_builtin_vload_common chunk args res =
-  match chunk, args, res with
-  | Mint8unsigned, [IR addr], [IR res] ->
-     emit (Pldrb (res, addr,SOimm _0))
-  | Mint8signed, [IR addr], [IR res] ->
-     emit (Pldrsb (res, addr,SOimm _0))
-  | Mint16unsigned, [IR addr], [IR res] ->
-     emit (Pldrh (res, addr, SOimm _0))
-  | Mint16signed, [IR addr], [IR res] ->
-     emit (Pldrsh (res, addr, SOimm _0))
-  | Mint32, [IR addr], [IR res] ->
-     emit (Pldr (res,addr, SOimm _0))
-  | Mint64, [IR addr], [IR res1; IR res2] ->
-     if addr <> res2 then begin
-	 emit (Pldr (res2, addr, SOimm _0));
-	 emit (Pldr (res1, addr, SOimm _4))
+let expand_builtin_vload_common chunk base ofs res =
+  match chunk, res with
+  | Mint8unsigned, BR(IR res) ->
+     emit (Pldrb (res, base, SOimm ofs))
+  | Mint8signed, BR(IR res) ->
+     emit (Pldrsb (res, base, SOimm ofs))
+  | Mint16unsigned, BR(IR res) ->
+     emit (Pldrh (res, base, SOimm ofs))
+  | Mint16signed, BR(IR res) ->
+     emit (Pldrsh (res, base, SOimm ofs))
+  | Mint32, BR(IR res) ->
+     emit (Pldr (res, base, SOimm ofs))
+  | Mint64, BR_splitlong(BR(IR res1), BR(IR res2)) ->
+     let ofs' = Int.add ofs _4 in
+     if base <> res2 then begin
+	 emit (Pldr (res2, base, SOimm ofs));
+	 emit (Pldr (res1, base, SOimm ofs'))
        end else begin
-	 emit (Pldr (res1,addr, SOimm _4));
-	 emit (Pldr (res2,addr, SOimm _0))
+	 emit (Pldr (res1, base, SOimm ofs'));
+	 emit (Pldr (res2, base, SOimm ofs))
        end
-  | Mfloat32, [IR addr], [FR res] ->
-     emit (Pflds (res, addr, _0))
-  | Mfloat64, [IR addr], [FR res] ->
-     emit (Pfldd (res,addr, _0))
+  | Mfloat32, BR(FR res) ->
+     emit (Pflds (res, base, ofs))
+  | Mfloat64, BR(FR res) ->
+     emit (Pfldd (res, base, ofs))
   | _ ->
      assert false
 
 let expand_builtin_vload chunk args res =
-  expand_builtin_vload_common chunk args res
-
-let expand_builtin_vload_global chunk id ofs args res =
-  emit (Ploadsymbol (IR14,id,ofs));
-  expand_builtin_vload_common chunk (IR IR14 :: args) res
-
-let expand_builtin_vstore_common chunk args =
-  match chunk, args with
-  | (Mint8signed | Mint8unsigned), [IR  addr; IR src] ->
-     emit (Pstrb (src,addr, SOimm _0))
-  | (Mint16signed | Mint16unsigned), [IR  addr; IR src] ->
-     emit (Pstrh (src,addr, SOimm _0))
-  | Mint32, [IR  addr; IR src] ->
-     emit (Pstr (src,addr, SOimm _0))
-  | Mint64, [IR  addr; IR src1; IR src2] ->
-     emit (Pstr (src2,addr,SOimm _0));
-     emit (Pstr (src1,addr,SOimm _4))
-  | Mfloat32, [IR  addr; FR src] ->
-     emit (Pfsts (src,addr,_0))
-  | Mfloat64, [IR  addr; FR src] ->
-     emit (Pfstd (src,addr,_0));
+  match args with
+  | [BA(IR addr)] ->
+      expand_builtin_vload_common chunk addr _0 res
+  | [BA_addrstack ofs] ->
+      if offset_in_range (Int.add ofs (Memdata.size_chunk chunk)) then
+        expand_builtin_vload_common chunk IR13 ofs res
+      else begin
+        expand_addimm IR14 IR13 ofs;
+        expand_builtin_vload_common chunk IR14 _0 res
+      end
+  | [BA_addrglobal(id, ofs)] ->
+      emit (Ploadsymbol (IR14,id,ofs));
+      expand_builtin_vload_common chunk IR14 _0 res
+  | _ ->
+      assert false
+
+let expand_builtin_vstore_common chunk base ofs src =
+  match chunk, src with
+  | (Mint8signed | Mint8unsigned), BA(IR src) ->
+     emit (Pstrb (src, base, SOimm ofs))
+  | (Mint16signed | Mint16unsigned), BA(IR src) ->
+     emit (Pstrh (src, base, SOimm ofs))
+  | Mint32, BA(IR src) ->
+     emit (Pstr (src, base, SOimm ofs))
+  | Mint64, BA_splitlong(BA(IR src1), BA(IR src2)) ->
+     let ofs' = Int.add ofs _4 in
+     emit (Pstr (src2, base, SOimm ofs));
+     emit (Pstr (src1, base, SOimm ofs'))
+  | Mfloat32, BA(FR src) ->
+     emit (Pfsts (src, base, ofs))
+  | Mfloat64, BA(FR src) ->
+     emit (Pfstd (src, base, ofs))
   | _ ->
      assert false
 
 let expand_builtin_vstore chunk args =
-  expand_builtin_vstore_common chunk args
-
-let expand_builtin_vstore_global chunk id ofs args =
-  emit (Ploadsymbol (IR14,id,ofs));
-  expand_builtin_vstore_common chunk (IR IR14 :: args)
+  match args with
+  | [BA(IR addr); src] ->
+      expand_builtin_vstore_common chunk addr _0 src
+  | [BA_addrstack ofs; src] ->
+      if offset_in_range (Int.add ofs (Memdata.size_chunk chunk)) then
+        expand_builtin_vstore_common chunk IR13 ofs src
+      else begin
+        expand_addimm IR14 IR13 ofs;
+        expand_builtin_vstore_common chunk IR14 _0 src
+      end
+  | [BA_addrglobal(id, ofs); src] ->
+      emit (Ploadsymbol (IR14,id,ofs));
+      expand_builtin_vstore_common chunk IR14 _0 src
+  | _ ->
+      assert false
 
 (* Handling of varargs *)
 
@@ -223,22 +279,24 @@ let expand_builtin_va_start r =
 
 
 (* Handling of compiler-inlined builtins *)
+
 let expand_builtin_inline name args res =
   match name, args, res with
   (* Integer arithmetic *)
-  | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] ->
-     emit (Prev (IR res,IR a1))
-  | "__builtin_bswap16", [IR a1], [IR res] ->
-     emit (Prev16 (IR res,IR a1))
-  | "__builtin_clz", [IR a1], [IR res] ->
-     emit (Pclz (IR res, IR a1))
+  | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
+     emit (Prev (res, a1))
+  | "__builtin_bswap16", [BA(IR a1)], BR(IR res) ->
+     emit (Prev16 (res, a1))
+  | "__builtin_clz", [BA(IR a1)], BR(IR res) ->
+     emit (Pclz (res, a1))
   (* Float arithmetic *)
-  | "__builtin_fabs",  [FR a1], [FR res] ->
+  | "__builtin_fabs",  [BA(FR a1)], BR(FR res) ->
      emit (Pfabsd (res,a1))
-  | "__builtin_fsqrt", [FR a1], [FR res] ->
+  | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) ->
      emit (Pfsqrt (res,a1))
   (* 64-bit integer arithmetic *)
-  | "__builtin_negl", [IR ah;IR al], [IR rh; IR rl] ->
+  | "__builtin_negl", [BA_splitlong(BA(IR ah), BA(IR al))],
+                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
       expand_int64_arith (rl = ah ) rl (fun rl ->
         emit (Prsbs (rl,al,SOimm _0));
         (* No "rsc" instruction in Thumb2.  Emulate based on
@@ -250,30 +308,35 @@ let expand_builtin_inline name args res =
         end else begin
 	  emit (Prsc (rh,ah,SOimm _0))
         end)
-  | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+  | "__builtin_addl", [BA_splitlong(BA(IR ah), BA(IR al));
+                       BA_splitlong(BA(IR bh), BA(IR bl))],
+                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
      expand_int64_arith (rl = ah || rl = bh) rl
 			(fun rl ->
 			 emit (Padds (rl,al,SOreg bl));
 			 emit (Padc (rh,ah,SOreg bh)))
-  | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
+  | "__builtin_subl", [BA_splitlong(BA(IR ah), BA(IR al));
+                       BA_splitlong(BA(IR bh), BA(IR bl))],
+                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
      expand_int64_arith (rl = ah || rl = bh) rl
 		       (fun rl ->
 			emit (Psubs (rl,al,SOreg bl));
 			emit (Psbc (rh,ah,SOreg bh)))
-  | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
+  | "__builtin_mull", [BA(IR a); BA(IR b)],
+                      BR_splitlong(BR(IR rh), BR(IR rl)) ->
      emit (Pumull (rl,rh,a,b))
   (* Memory accesses *)
-  | "__builtin_read16_reversed", [IR a1], [IR res] ->
+  | "__builtin_read16_reversed", [BA(IR a1)], BR(IR res) ->
      emit (Pldrh (res,a1,SOimm _0));
-     emit (Prev16 (IR res,IR res));
-  | "__builtin_read32_reversed", [IR a1], [IR res] ->
+     emit (Prev16 (res, res));
+  | "__builtin_read32_reversed", [BA(IR a1)], BR(IR res) ->
      emit (Pldr (res,a1,SOimm _0));
-     emit (Prev (IR res,IR res));
-  | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
-     emit (Prev16 (IR IR14, IR a2));
+     emit (Prev (res, res));
+  | "__builtin_write16_reversed", [BA(IR a1); BA(IR a2)], _ ->
+     emit (Prev16 (IR14, a2));
      emit (Pstrh (IR14, a1, SOimm _0))
-  | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
-     emit (Prev (IR IR14, IR a2));
+  | "__builtin_write32_reversed", [BA(IR a1); BA(IR a2)], _ ->
+     emit (Prev (IR14, a2));
      emit (Pstr (IR14, a1, SOimm _0))
   (* Synchronization *)
   | "__builtin_membar",[], _ ->
@@ -285,11 +348,11 @@ let expand_builtin_inline name args res =
   | "__builtin_isb", [], _ ->
      emit Pisb
   (* Vararg stuff *)
-  | "__builtin_va_start", [IR a], _ ->
+  | "__builtin_va_start", [BA(IR a)], _ ->
      expand_builtin_va_start a
   (* Catch-all *)
   | _ ->
-      invalid_arg ("unrecognized builtin " ^ name)
+      raise (Error ("unrecognized builtin " ^ name))
 
 let expand_instruction instr =
   match instr with
@@ -319,30 +382,35 @@ let expand_instruction instr =
 	      expand_builtin_vload chunk args res
 	   | EF_vstore chunk ->
 	      expand_builtin_vstore chunk args
-	   | EF_vload_global(chunk, id, ofs) ->
-	      expand_builtin_vload_global chunk id ofs args res
-	   | EF_vstore_global(chunk, id, ofs) ->
-	      expand_builtin_vstore_global chunk id ofs args
 	   | EF_annot_val (txt,targ) ->
 	      expand_annot_val txt targ args res
 	   | EF_memcpy(sz, al) ->
 	      expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz))
 		(Int32.to_int (camlint_of_coqint al)) args
-	   | EF_inline_asm(txt, sg, clob) ->
+	   | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
               emit instr
-	   | _ -> assert false
+	   | _ ->
+              assert false
      end
   | _ ->
      emit instr
 
 let expand_function fn =
-  set_current_function fn;
-  List.iter expand_instruction fn.fn_code;
-  get_current_function ()
+  try
+    set_current_function fn;
+    List.iter expand_instruction fn.fn_code;
+    Errors.OK (get_current_function ())
+  with Error s ->
+    Errors.Error (Errors.msg (coqstring_of_camlstring s))
 
 let expand_fundef = function
-  | Internal f -> Internal (expand_function f)
-  | External ef -> External ef
-
-let expand_program (p: Asm.program) : Asm.program =
-  AST.transform_program expand_fundef p
+  | Internal f ->
+      begin match expand_function f with
+      | Errors.OK tf -> Errors.OK (Internal tf)
+      | Errors.Error msg -> Errors.Error msg
+      end
+  | External ef ->
+      Errors.OK (External ef)
+
+let expand_program (p: Asm.program) : Asm.program Errors.res =
+  AST.transform_partial_program expand_fundef p
diff --git a/arm/Asmgen.v b/arm/Asmgen.v
index 5a3a48e1..2365d1d2 100644
--- a/arm/Asmgen.v
+++ b/arm/Asmgen.v
@@ -727,9 +727,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
       OK (loadind_int IR13 f.(fn_retaddr_ofs) IR14
            (Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: Pbsymb symb sig :: k))
   | Mbuiltin ef args res =>
-      OK (Pbuiltin ef (map preg_of args) (map preg_of res) :: k)
-  | Mannot ef args =>
-      OK (Pannot ef (List.map (map_annot_arg preg_of) args) :: k)
+      OK (Pbuiltin ef (List.map (map_builtin_arg preg_of) args) (map_builtin_res preg_of res) :: k)
   | Mlabel lbl =>
       OK (Plabel lbl :: k)
   | Mgoto lbl =>
diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v
index 6d9b134f..93c50bfb 100644
--- a/arm/Asmgenproof.v
+++ b/arm/Asmgenproof.v
@@ -747,48 +747,32 @@ Opaque loadind.
   intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. 
 
 - (* Mbuiltin *)
-  inv AT. monadInv H3. 
+  inv AT. monadInv H4. 
   exploit functions_transl; eauto. intro FN.
-  generalize (transf_function_no_overflow _ _ H2); intro NOOV.
-  exploit external_call_mem_extends'; eauto. eapply preg_vals; eauto.
+  generalize (transf_function_no_overflow _ _ H3); intro NOOV.
+  exploit builtin_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_builtin. eauto. eauto.
   eapply find_instr_tail; eauto.
-  eapply external_call_symbols_preserved'; eauto.
+  erewrite <- sp_val by eauto. 
+  eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
+  eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
   eauto.
   econstructor; eauto.
-  Simpl. rewrite set_pregs_other_2. rewrite undef_regs_other_2. rewrite <- H0. simpl. econstructor; eauto.
+  instantiate (2 := tf); instantiate (1 := x).
+  unfold nextinstr. rewrite Pregmap.gss.
+  rewrite set_res_other. rewrite undef_regs_other_2.
+  rewrite <- H1. simpl. econstructor; eauto.
   eapply code_tail_next_int; eauto.
-  apply preg_notin_charact. auto with asmgen.
-  apply preg_notin_charact. auto with asmgen.
-  apply agree_nextinstr. eapply agree_set_mregs; auto.
+  rewrite preg_notin_charact. intros. auto with asmgen.
+  auto with asmgen.
+  apply agree_nextinstr. eapply agree_set_res; auto.
   eapply agree_undef_regs; eauto. intros; apply undef_regs_other_2; auto. 
   congruence.
 
-- (* Mannot *)
-  inv AT. monadInv H4. 
-  exploit functions_transl; eauto. intro FN.
-  generalize (transf_function_no_overflow _ _ H3); intro NOOV.
-  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.
-  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. 
-  rewrite <- H1; simpl. econstructor; eauto.
-  eapply code_tail_next_int; eauto. 
-  apply agree_nextinstr. auto.
-  congruence.
-
 - (* Mgoto *)
   assert (f0 = f) by congruence. subst f0.
   inv AT. monadInv H4. 
diff --git a/arm/Machregs.v b/arm/Machregs.v
index f46f2904..f4bd4613 100644
--- a/arm/Machregs.v
+++ b/arm/Machregs.v
@@ -130,7 +130,7 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
 
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
-  | EF_memcpy sz al => if zle sz 32 then F7 :: nil else R2 :: R3 :: R12 :: nil
+  | EF_memcpy sz al => R2 :: R3 :: R12 :: F7 :: nil
   | EF_inline_asm txt sg clob => destroyed_by_clobber clob
   | _ => nil
   end.
@@ -150,11 +150,7 @@ Definition mregs_for_operation (op: operation): list (option mreg) * option mreg
   end.
 
 Definition mregs_for_builtin (ef: external_function): list (option mreg) * list(option mreg) :=
-  match ef with
-  | EF_memcpy sz al =>
-      if zle sz 32 then (nil, nil) else (Some R3 :: Some R2 :: nil, nil)
-  | _ => (nil, nil)
-  end.
+  (nil, nil).
 
 Global Opaque
     destroyed_by_op destroyed_by_load destroyed_by_store
@@ -171,3 +167,15 @@ Definition two_address_op (op: operation) : bool :=
 
 Global Opaque two_address_op.
 
+(* Constraints on constant propagation for builtins *)
+
+Definition builtin_constraints (ef: external_function) :
+                                       list builtin_arg_constraint :=
+  match ef with
+  | EF_vload _ => OK_addrany :: nil
+  | EF_vstore _ => OK_addrany :: OK_default :: nil
+  | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil
+  | EF_annot txt targs => map (fun _ => OK_all) targs
+  | EF_debug kind txt targs => map (fun _ => OK_all) targs
+  | _ => nil
+  end.
diff --git a/arm/SelectOp.vp b/arm/SelectOp.vp
index fea99ef5..aec737ad 100644
--- a/arm/SelectOp.vp
+++ b/arm/SelectOp.vp
@@ -489,16 +489,18 @@ Nondetfunction addressing (chunk: memory_chunk) (e: expr) :=
   | _ => (Aindexed Int.zero, e:::Enil)
   end.
 
-(** ** Arguments of annotations *)
+(** ** Arguments of builtins *)
 
-Nondetfunction annot_arg (e: expr) :=
+Nondetfunction builtin_arg (e: expr) :=
   match e with
-  | Eop (Ointconst n) Enil => AA_int n
-  | Eop (Oaddrsymbol id ofs) Enil => AA_addrglobal id ofs
-  | Eop (Oaddrstack ofs) Enil => AA_addrstack ofs
+  | Eop (Ointconst n) Enil => BA_int n
+  | Eop (Oaddrsymbol id ofs) Enil => BA_addrglobal id ofs
+  | Eop (Oaddrstack ofs) Enil => BA_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 (Ainstack ofs) Enil => AA_loadstack chunk ofs
-  | _ => AA_base e
+        BA_long (Int64.ofwords h l)
+  | Eop Omakelong (h ::: l ::: Enil) => BA_splitlong (BA h) (BA l)
+  | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
+  | Eload chunk (Aindexed ofs1) (Eop (Oaddrsymbol id ofs) Enil ::: Enil) =>
+       BA_loadglobal chunk id (Int.add ofs ofs1)
+  | _ => BA e
   end.
diff --git a/arm/SelectOpproof.v b/arm/SelectOpproof.v
index d3c3239a..5f41e754 100644
--- a/arm/SelectOpproof.v
+++ b/arm/SelectOpproof.v
@@ -864,18 +864,20 @@ Proof.
   exists (v :: nil); split. eauto with evalexpr. subst. simpl. rewrite Int.add_zero; auto.
 Qed.
 
-Theorem eval_annot_arg:
+Theorem eval_builtin_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.
+  CminorSel.eval_builtin_arg ge sp e m (builtin_arg a) v.
 Proof.
-  intros until v. unfold annot_arg; case (annot_arg_match a); intros; InvEval.
+  intros until v. unfold builtin_arg; case (builtin_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. rewrite <- Genv.shift_symbol_address in H6.
+  inv H6. constructor; auto.  
 - constructor; auto.
 Qed.
 
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml
index f8d72836..f7f0d313 100644
--- a/arm/TargetPrinter.ml
+++ b/arm/TargetPrinter.ml
@@ -305,17 +305,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
     let print_location oc loc =
       if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
 
-(* Handling of annotations *)
-
-    let print_annot_stmt oc txt targs args =
-      if Str.string_match re_file_line txt 0 then begin
-        print_file_line oc (Str.matched_group 1 txt)
-          (int_of_string (Str.matched_group 2 txt))
-      end else begin
-        fprintf oc "%s annotation: " comment;
-        print_annot_stmt preg "sp" oc txt targs args
-      end
-
 (* Auxiliary for 64-bit integer arithmetic built-ins.  They expand to
    two instructions, one computing the low 32 bits of the result,
    followed by another computing the high 32 bits.  In cases where
@@ -521,7 +510,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           fprintf oc "	bic%t	%a, %a, %a\n"
             thumbS ireg r1 ireg r2 shift_op so; 1
       | Pclz (r1,r2) ->
-	 fprintf oc "	clz	%a, %a\n" preg r1 preg r2; 1
+	 fprintf oc "	clz	%a, %a\n" ireg r1 ireg r2; 1
       | Pcmp(r1, so) ->
           fprintf oc "	cmp	%a, %a\n" ireg r1 shift_op so; 1
       | Pdmb ->
@@ -571,9 +560,9 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           fprintf oc "	orr%t	%a, %a, %a\n"
             thumbS ireg r1 ireg r2 shift_op so; 1
       | Prev (r1,r2) ->
-	 fprintf oc "	rev	%a, %a\n" preg r1 preg r2; 1
+	 fprintf oc "	rev	%a, %a\n" ireg r1 ireg r2; 1
       | Prev16 (r1,r2) ->
-	 fprintf oc "	rev16	%a, %a\n" preg r1 preg r2; 1
+	 fprintf oc "	rev16	%a, %a\n" ireg r1 ireg r2; 1
       | Prsb(r1, r2, so) ->
          fprintf oc "	rsb%t	%a, %a, %a\n"
 		 thumbS ireg r1 ireg r2 shift_op so; 1
@@ -782,6 +771,14 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           end
       | Pbuiltin(ef, args, res) ->
           begin match ef with
+          | EF_annot(txt, targs) ->
+              fprintf oc "%s annotation: " comment;
+              print_annot_text preg "sp" oc (extern_atom txt) args;
+              0
+          | EF_debug(kind, txt, targs) ->
+              print_debug_info comment print_file_line preg "sp" oc
+                               (P.to_int kind) (extern_atom txt) args;
+              0
           | EF_inline_asm(txt, sg, clob) ->
               fprintf oc "%s begin inline assembly\n\t" comment;
               print_inline_asm preg oc (extern_atom txt) sg args res;
@@ -790,13 +787,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET =
           | _ ->
               assert false
           end
-      | Pannot(ef, args) ->
-          begin match ef with
-          | EF_annot(txt, targs) ->
-              print_annot_stmt oc (extern_atom txt) targs args; 0
-          | _ ->
-              assert false
-          end
       | Pcfi_adjust sz -> cfi_adjust oc (camlint_of_coqint sz); 0
 
     let no_fallthrough = function