X

Merge branch 'master' into debug_locations

10 files changed, 429 insertions, 280 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index b7656dc4..863ed6a1 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -167,6 +167,10 @@ Inductive instruction : Type :=
   | Pcrxor: crbit -> crbit -> crbit -> instruction            (**r xor between condition bits *)
   | Pdcbf: ireg -> ireg -> instruction                        (**r data cache flush *)
   | Pdcbi: ireg -> ireg -> instruction                        (**r data cache invalidate *)
+  | Pdcbt: int -> ireg -> ireg -> instruction                 (**r data cache block touch *)
+  | Pdcbtst: int -> ireg -> ireg -> instruction               (**r data cache block touch *)
+  | Pdcbtls: int -> ireg -> ireg -> instruction               (**r data cache block touch and lock *)
+  | Pdcbz: ireg -> ireg -> instruction                        (**r data cache block zero *)
   | Pdivw: ireg -> ireg -> ireg -> instruction                (**r signed division *)
   | Pdivwu: ireg -> ireg -> ireg -> instruction               (**r unsigned division *)
   | Peieio: instruction                                       (**r EIEIO barrier *)
@@ -204,6 +208,7 @@ Inductive instruction : Type :=
   | Pfsel: freg -> freg -> freg -> freg -> instruction        (**r FP conditional move *)
   | Pisync: instruction                                       (**r ISYNC barrier *)
   | Picbi: ireg -> ireg -> instruction                        (**r instruction cache invalidate *)
+  | Picbtls: int -> ireg -> ireg -> instruction               (**r instruction cache block touch and lock set *)
   | Plbz: ireg -> constant -> ireg -> instruction             (**r load 8-bit unsigned int *)
   | Plbzx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
   | Plfd: freg -> constant -> ireg -> instruction             (**r load 64-bit float *)
@@ -226,12 +231,15 @@ Inductive instruction : Type :=
   | Plwzx_a: ireg -> ireg -> ireg -> instruction              (**r same, with 2 index regs *)
   | Plwarx: ireg -> ireg -> ireg -> instruction               (**r load with reservation *)
   | Plwbrx: ireg -> ireg -> ireg -> instruction               (**r load 32-bit int and reverse endianness *)
+  | Pmbar: int -> instruction                                 (**r memory barrier *)
   | Pmfcr: ireg -> instruction                                (**r move condition register to reg *)
   | Pmfcrbit: ireg -> crbit -> instruction                    (**r move condition bit to reg (pseudo) *)
   | Pmflr: ireg -> instruction                                (**r move LR to reg *)
   | Pmr: ireg -> ireg -> instruction                          (**r integer move *)
   | Pmtctr: ireg -> instruction                               (**r move ireg to CTR *)
   | Pmtlr: ireg -> instruction                                (**r move ireg to LR *)
+  | Pmfspr: ireg -> int -> instruction                        (**r move from special register *)
+  | Pmtspr: int -> ireg -> instruction                        (**r move to special register *)
   | Pmulli: ireg -> ireg -> constant -> instruction           (**r integer multiply immediate *)
   | Pmullw: ireg -> ireg -> ireg -> instruction               (**r integer multiply *)
   | Pmulhw: ireg -> ireg -> ireg -> instruction               (**r multiply high signed *)
@@ -279,8 +287,7 @@ Inductive instruction : Type :=
   | Pxori: ireg -> ireg -> constant -> instruction            (**r bitwise xor with immediate *)
   | Pxoris: ireg -> ireg -> constant -> instruction           (**r bitwise xor with immediate high *)
   | Plabel: label -> instruction                              (**r define a code label *)
-  | Pbuiltin: external_function -> list preg -> list preg -> instruction (**r built-in function (pseudo) *)
-  | Pannot: external_function -> list (annot_arg preg) -> instruction (**r annotation statement (pseudo) *)
+  | Pbuiltin: external_function -> list (builtin_arg preg) -> builtin_res preg -> instruction (**r built-in function (pseudo) *)
   | Pcfi_adjust: int -> instruction                           (**r .cfi_adjust debug directive *)
   | Pcfi_rel_offset: int -> instruction.                      (**r .cfi_rel_offset lr debug directive *)
 
@@ -386,6 +393,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. *)
@@ -852,16 +868,18 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr rs) m
   | 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. *)
+  (** The following instructions and directives are not generated
+      directly by [Asmgen], so we do not model them. *)
   | Pbdnz _
   | Pcntlzw _ _
   | Pcreqv _ _ _
   | Pcrxor _ _ _
   | Pdcbf _ _
   | Pdcbi _ _
+  | Pdcbt _ _ _
+  | Pdcbtst _ _ _
+  | Pdcbtls _ _ _
+  | Pdcbz _ _
   | Peieio
   | Pfctiw _ _
   | Pfctiwz _ _
@@ -876,11 +894,15 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Plwarx _ _ _
   | Plwbrx _ _ _
   | Picbi _ _
+  | Picbtls _ _ _
   | Pisync
   | Plwsync
   | Plhbrx _ _ _
   | Plwzu _ _ _
+  | Pmbar _
   | Pmfcr _
+  | Pmfspr _ _
+  | Pmtspr _ _
   | Pstwbrx _ _ _
   | Pstwcx_ _ _ _
   | Pstfdu _ _ _
@@ -954,24 +976,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) f.(fn_code) = Some (Pbuiltin ef args res) ->
-      external_call' ef ge (map rs args) m t vl m' ->
+      eval_builtin_args ge rs (rs GPR1) m args vargs ->
+      external_call ef ge vargs m t vres m' ->
       rs' = nextinstr
-              (set_regs res vl
+              (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) f.(fn_code) = Some (Pannot ef args) ->
-      eval_annot_args ge rs (rs GPR1) 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 ->
@@ -1035,12 +1049,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].
@@ -1048,7 +1058,6 @@ Ltac Equalities :=
 (* trace length *)
   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 *)
@@ -1068,4 +1077,4 @@ Definition data_preg (r: preg) : bool :=
   | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false
   | CARRY => false
   | _ => true
-  end.
\ No newline at end of file
+  end.
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index d66dd163..5f875ebf 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -158,7 +158,7 @@ let p_instruction oc ic =
   | Pandi_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandi_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c
   | Pandis_ (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pandis_\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c
   | Pb l -> fprintf oc "{\"Instruction Name\":\"Pb\",\"Args\":[%a]}" p_label l
-  | Pbctr s -> assert false (* Should not occur *)
+  | Pbctr s -> fprintf oc  "{\"Instruction Name\":\"Pbctr\",\"Args\":[]}"
   | Pbctrl s -> fprintf oc "{\"Instruction Name\":\"Pbctrl\",\"Args\":[]}"
   | Pbdnz l -> fprintf oc "{\"Instruction Name\":\"Pbdnz\",\"Args\":[%a]}" p_label l 
   | Pbf (c,l) -> fprintf oc "{\"Instruction Name\":\"Pbf\",\"Args\":[%a,%a]}" p_crbit c p_label l
@@ -177,6 +177,10 @@ let p_instruction oc ic =
   | Pcrxor (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcrxor\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3
   | Pdcbf (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbf\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pdcbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
+  | Pdcbt (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbt\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2
+  | Pdcbtst (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbtst\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2
+  | Pdcbtls (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbtls\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2
+  | Pdcbz (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbz\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pdivw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pdivwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Peieio -> fprintf oc "{\"Instruction Name\":\"Peieio,\"Args\":[]}"
@@ -213,10 +217,11 @@ let p_instruction oc ic =
   | Pfres (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfres\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2
   | Pfsel (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfsel\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4
   | Picbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
+  | Picbtls (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbtls\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2
   | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}"
   | Plwsync -> fprintf oc "{\"Instruction Name\":\"Plwsync\",\"Args\":[]}"
   | Plbz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2
-  | Plbzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pblzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
+  | Plbzx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plbzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Plfd (fr,c,ir)
   | Plfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Plfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir
   | Plfdx (fr,ir1,ir2)
@@ -237,14 +242,17 @@ let p_instruction oc ic =
   | Plwzx_a (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwzx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Plwarx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwarx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Plwbrx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Plwbrx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
+  | Pmbar c -> fprintf oc "{\"Instruction Name\":\"Pmbar\",\"Args\":[%a]}" p_int_constant c
   | Pmfcr ir -> fprintf oc "{\"Instruction Name\":\"Pmfcr\",\"Args\":[%a]}" p_ireg ir
   | Pmfcrbit (ir,crb) -> assert false (* Should not occur *)
   | Pmflr ir -> fprintf oc "{\"Instruction Name\":\"Pmflr\",\"Args\":[%a]}" p_ireg ir
   | Pmr (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pmr\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pmtctr ir -> fprintf oc "{\"Instruction Name\":\"Pmtctr\",\"Args\":[%a]}" p_ireg ir
   | Pmtlr ir -> fprintf oc "{\"Instruction Name\":\"Pmtlr\",\"Args\":[%a]}" p_ireg ir
+  | Pmfspr(ir, n) -> fprintf oc "{\"Instruction Name\":\"Pmfspr\",\"Args\":[%a,%a]}" p_ireg ir p_int_constant n
+  | Pmtspr(n, ir) -> fprintf oc "{\"Instruction Name\":\"Pmtspr\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir
   | Pmulli (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pmulli\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c
-  | Pmullw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
+  | Pmullw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmullw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pmulhw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulhw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pmulhwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulhwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pnand (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pnand\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
@@ -263,7 +271,7 @@ let p_instruction oc ic =
   | Pstbx (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pstbx\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pstfd (fr,c,ir)
   | Pstfd_a (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfd\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir
-  | Pstfdu (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstdu\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir
+  | Pstfdu (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfdu\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir
   | Pstfdx (fr,ir1,ir2)
   | Pstfdx_a (fr,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pstfdx\",\"Args\":[%a,%a,%a]}" p_freg fr p_ireg ir1 p_ireg ir2
   | Pstfs (fr,c,ir) -> fprintf oc "{\"Instruction Name\":\"Pstfs\",\"Args\":[%a,%a,%a]}" p_freg fr p_constant c p_ireg ir
@@ -289,7 +297,9 @@ let p_instruction oc ic =
   | Pxori (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pxori\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c
   | Pxoris (ir1,ir2,c) -> fprintf oc "{\"Instruction Name\":\"Pxoris\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_constant c
   | Plabel l -> fprintf oc "{\"Instruction Name\":\"Plabel\",\"Args\":[%a]}" p_label l
-  | Pbuiltin (ef,args1,args2) ->
+  | Pbuiltin (ef,args1,args2) -> ()
+(* FIXME *)
+(*
       begin match ef with
       | EF_inline_asm (i,s,il) ->
           fprintf oc "{\"Instruction Name\":\"Inline_asm\",\"Args\":[%a%a%a%a]}" p_atom_constant i  (p_list_cont p_char_list) il
@@ -297,7 +307,8 @@ let p_instruction oc ic =
       | _ -> (* Should all be folded away *)
           assert false
       end
-  | Pannot _  (* We do not check the annotations *)
+*)
+(* END FIXME *)
   | Pcfi_adjust _  (* Only debug relevant *)
   | Pcfi_rel_offset _ ->  () (* Only debug relevant *)
 
@@ -329,7 +340,7 @@ let p_fundef oc (name,f) =
   let alignment = atom_alignof name
   and inline = atom_is_inline name
   and static = atom_is_static name
-  and instr = List.filter (function Pannot _ | Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in
+  and instr = List.filter (function Pbuiltin _| Pcfi_adjust _ | Pcfi_rel_offset _ -> false | _ -> true) f.fn_code in
   let c_section,l_section,j_section = match (atom_sections name) with [a;b;c] -> a,b,c | _ -> assert false in
   fprintf oc "{\"Fun Name\":%a,\n\"Fun Storage Class\":%a,\n\"Fun Alignment\":%a,\n\"Fun Section Code\":%a,\"Fun Section Literals\":%a,\"Fun Section Jumptable\":%a,\n\"Fun Inline\":%B,\n\"Fun Code\":%a}\n"
     p_atom name  p_storage static p_int_opt alignment  
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index ae4d694a..3e57cdbf 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -21,6 +21,7 @@ open Memdata
 open Asm
 open Asmexpandaux
 
+exception Error of string
 
 (* Useful constants and helper functions *)
 
@@ -44,14 +45,14 @@ let emit_addimm rd rs n =
 (* 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));
   begin match args, res with
-  | [IR src], [IR dst] ->
+  | [BA(IR src)], BR(IR dst) ->
       if dst <> src then emit (Pmr(dst, src))
-  | [FR src], [FR dst] ->
+  | [BA(FR src)], BR(FR dst) ->
       if dst <> src then emit (Pfmr(dst, src))
   | _, _ ->
-      assert false
+      raise (Error "ill-formed __builtin_annot_val")
   end
 
 (* Handling of memcpy *)
@@ -62,34 +63,64 @@ let expand_annot_val txt targ args res =
    So, use 64-bit accesses only if alignment >= 4.
    Note that lfd and stfd cannot trap on ill-formed floats. *)
 
+let offset_in_range ofs =
+  Int.eq (Asmgen.high_s ofs) Int.zero
+
+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 (GPR1, ofs)
+      else begin emit_addimm tmp GPR1 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 GPR11) then (GPR11, GPR12) else (GPR12, GPR11) 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 (Plfd(FPR13, Cint ofs, src));
-      emit (Pstfd(FPR13, Cint ofs, dst));
-      copy (Int.add ofs _8) (sz - 8)
+      emit (Plfd(FPR13, Cint osrc, rsrc));
+      emit (Pstfd(FPR13, Cint odst, rdst));
+      copy (Int.add osrc _8) (Int.add odst _8) (sz - 8)
     end else if sz >= 4 then begin
-      emit (Plwz(GPR0, Cint ofs, src));
-      emit (Pstw(GPR0, Cint ofs, dst));
-      copy (Int.add ofs _4) (sz - 4)
+      emit (Plwz(GPR0, Cint osrc, rsrc));
+      emit (Pstw(GPR0, Cint odst, rdst));
+      copy (Int.add osrc _4) (Int.add odst _4) (sz - 4)
     end else if sz >= 2 then begin
-      emit (Plhz(GPR0, Cint ofs, src));
-      emit (Psth(GPR0, Cint ofs, dst));
-      copy (Int.add ofs _2) (sz - 2)
+      emit (Plhz(GPR0, Cint osrc, rsrc));
+      emit (Psth(GPR0, Cint odst, rdst));
+      copy (Int.add osrc _2) (Int.add odst _2) (sz - 2)
     end else if sz >= 1 then begin
-      emit (Plbz(GPR0, Cint ofs, src));
-      emit (Pstb(GPR0, Cint ofs, dst));
-      copy (Int.add ofs _1) (sz - 1)
+      emit (Plbz(GPR0, Cint osrc, rsrc));
+      emit (Pstb(GPR0, Cint odst, rdst));
+      copy (Int.add osrc _1) (Int.add odst _1) (sz - 1)
     end in
-  copy _0 sz
+  copy osrc odst sz
+
+let memcpy_big_arg arg tmp =
+  (* Set [tmp] to the value of [arg] minus 4 *)
+  match arg with
+  | BA (IR r) ->
+      emit (Paddi(tmp, r, Cint _m4))
+  | BA_addrstack ofs ->
+      emit_addimm tmp GPR1 (Int.add ofs _m4)
+  | _ ->
+      assert false
 
 let expand_builtin_memcpy_big sz al src dst =
   assert (sz >= 4);
   emit_loadimm GPR0 (Z.of_uint (sz / 4));
   emit (Pmtctr GPR0);
-  let (s,d) = if dst <> GPR11 then (GPR11, GPR12) else (GPR12, GPR11) in
-  emit (Paddi(s, src, Cint _m4));
-  emit (Paddi(d, dst, Cint _m4));
+  let (s, d) = 
+    if dst <> BA (IR GPR11) then (GPR11, GPR12) else (GPR12, GPR11) in
+  memcpy_big_arg src s;
+  memcpy_big_arg dst d;
   let lbl = new_label() in
   emit (Plabel lbl);
   emit (Plwzu(GPR0, Cint _4, s));
@@ -109,7 +140,7 @@ 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 <= (if !Clflags.option_ffpu && al >= 4
             then if !Clflags.option_Osize then 35 else 51
 	    else if !Clflags.option_Osize then 19 else 27)
@@ -118,140 +149,131 @@ let expand_builtin_memcpy sz al args =
 
 (* Handling of volatile reads and writes *)
 
-let expand_builtin_vload_common chunk base offset res =
+let offset_constant cst delta =
+  match cst with
+  | Cint n ->
+      let n' = Int.add n delta in
+      if offset_in_range n' then Some (Cint n') else None
+  | Csymbol_sda(id, ofs) ->
+      Some (Csymbol_sda(id, Int.add ofs delta))
+  | _ -> None
+
+let rec expand_builtin_vload_common chunk base offset res =
   match chunk, res with
-  | Mint8unsigned, IR res ->
+  | Mint8unsigned, BR(IR res) ->
       emit (Plbz(res, offset, base))
-  | Mint8signed, IR res ->
+  | Mint8signed, BR(IR res) ->
       emit (Plbz(res, offset, base));
       emit (Pextsb(res, res))
-  | Mint16unsigned, IR res ->
+  | Mint16unsigned, BR(IR res) ->
       emit (Plhz(res, offset, base))
-  | Mint16signed, IR res ->
+  | Mint16signed, BR(IR res) ->
       emit (Plha(res, offset, base))
-  | (Mint32 | Many32), IR res ->
+  | (Mint32 | Many32), BR(IR res) ->
       emit (Plwz(res, offset, base))
-  | Mfloat32, FR res ->
+  | Mfloat32, BR(FR res) ->
       emit (Plfs(res, offset, base))
-  | (Mfloat64 | Many64), FR res ->
+  | (Mfloat64 | Many64), BR(FR res) ->
       emit (Plfd(res, offset, base))
-  (* Mint64 is special-cased below *)
-  | _ ->
+  | Mint64, BR_splitlong(BR(IR hi), BR(IR lo)) ->
+      begin match offset_constant offset _4 with
+      | Some offset' ->
+          if hi <> base then begin
+            emit (Plwz(hi, offset, base));
+            emit (Plwz(lo, offset', base))
+          end else begin
+            emit (Plwz(lo, offset', base));
+            emit (Plwz(hi, offset, base))
+          end
+      | None ->      
+          emit (Paddi(GPR11, base, offset));
+          expand_builtin_vload_common chunk GPR11 (Cint _0) res
+      end
+  | _, _ ->
       assert false
 
 let expand_builtin_vload chunk args res =
-  begin match args, res with
-  | [IR addr], [res] when chunk <> Mint64 ->
+  match args with
+  | [BA(IR addr)] ->
       expand_builtin_vload_common chunk addr (Cint _0) res
-  | [IR addr], [IR res1; IR res2] when chunk = Mint64 ->
-      if addr <> res1 then begin
-        emit (Plwz(res1, Cint _0, addr));
-        emit (Plwz(res2, Cint _4, addr))
+  | [BA_addrstack ofs] ->
+      if offset_in_range ofs then
+        expand_builtin_vload_common chunk GPR1 (Cint ofs) res
+      else begin
+        emit_addimm GPR11 GPR1 ofs;
+        expand_builtin_vload_common chunk GPR11 (Cint _0) res
+      end
+  | [BA_addrglobal(id, ofs)] ->
+      if symbol_is_small_data id ofs then
+        expand_builtin_vload_common chunk GPR0 (Csymbol_sda(id, ofs)) res
+      else if symbol_is_rel_data id ofs then begin
+        emit (Paddis(GPR11, GPR0, Csymbol_rel_high(id, ofs)));
+        expand_builtin_vload_common chunk GPR11 (Csymbol_rel_low(id, ofs)) res
       end else begin
-        emit (Plwz(res2, Cint _4, addr));
-        emit (Plwz(res1, Cint _0, addr))
+        emit (Paddis(GPR11, GPR0, Csymbol_high(id, ofs)));
+        expand_builtin_vload_common chunk GPR11 (Csymbol_low(id, ofs)) res
       end
   | _ ->
       assert false
-  end
-
-let expand_builtin_vload_global chunk id ofs args res =
-  begin match res with
-  | [res] when chunk <> Mint64 ->
-      emit (Paddis(GPR11, GPR0, Csymbol_high(id, ofs)));
-      expand_builtin_vload_common chunk GPR11 (Csymbol_low(id, ofs)) res
-  | [IR res1; IR res2] when chunk = Mint64 ->
-      emit (Paddis(res1, GPR0, Csymbol_high(id, ofs)));
-      emit (Plwz(res1, Csymbol_low(id, ofs), res1));
-      let ofs = Int.add ofs _4 in
-      emit (Paddis(res2, GPR0, Csymbol_high(id, ofs)));
-      emit (Plwz(res2, Csymbol_low(id, ofs), res2))
-  | _ ->
-      assert false
-  end
-
-let expand_builtin_vload_sda chunk id ofs args res =
-  begin match res with
-  | [res] when chunk <> Mint64 ->
-      expand_builtin_vload_common chunk GPR0 (Csymbol_sda(id, ofs)) res
-  | [IR res1; IR res2] when chunk = Mint64 ->
-      emit (Plwz(res1, Csymbol_sda(id, ofs), GPR0));
-      let ofs = Int.add ofs _4 in
-      emit (Plwz(res2, Csymbol_sda(id, ofs), GPR0))
-  | _ ->
-      assert false
-  end
 
-let expand_builtin_vload_rel chunk id ofs args res =
-  emit (Paddis(GPR11, GPR0, Csymbol_rel_high(id, ofs)));
-  emit (Paddi(GPR11, GPR11, Csymbol_rel_low(id, ofs)));
-  expand_builtin_vload chunk [IR GPR11] res
+let temp_for_vstore src =
+  let rl = AST.params_of_builtin_arg src in
+  if not (List.mem (IR GPR11) rl) then GPR11
+  else if not (List.mem (IR GPR12) rl) then GPR12
+  else GPR10
 
 let expand_builtin_vstore_common chunk base offset src =
   match chunk, src with
-  | (Mint8signed | Mint8unsigned), IR src ->
+  | (Mint8signed | Mint8unsigned), BA(IR src) ->
       emit (Pstb(src, offset, base))
-  | (Mint16signed | Mint16unsigned), IR src ->
+  | (Mint16signed | Mint16unsigned), BA(IR src) ->
       emit (Psth(src, offset, base))
-  | (Mint32 | Many32), IR src ->
+  | (Mint32 | Many32), BA(IR src) ->
       emit (Pstw(src, offset, base))
-  | Mfloat32, FR src ->
+  | Mfloat32, BA(FR src) ->
       emit (Pstfs(src, offset, base))
-  | (Mfloat64 | Many64), FR src ->
+  | (Mfloat64 | Many64), BA(FR src) ->
       emit (Pstfd(src, offset, base))
-  (* Mint64 is special-cased below *)
-  | _ ->
+  | Mint64, BA_splitlong(BA(IR hi), BA(IR lo)) ->
+      begin match offset_constant offset _4 with
+      | Some offset' ->
+          emit (Pstw(hi, offset, base));
+          emit (Pstw(lo, offset', base))
+      | None ->      
+          let tmp = temp_for_vstore src in
+          emit (Paddi(tmp, base, offset));
+          emit (Pstw(hi, Cint _0, tmp));
+          emit (Pstw(lo, Cint _4, tmp))
+      end
+  | _, _ ->
       assert false
 
 let expand_builtin_vstore chunk args =
-  begin match args with
-  | [IR addr; src] when chunk <> Mint64 ->
+  match args with
+  | [BA(IR addr); src] ->
       expand_builtin_vstore_common chunk addr (Cint _0) src
-  | [IR addr; IR src1; IR src2] when chunk = Mint64 ->
-      emit (Pstw(src1, Cint _0, addr));
-      emit (Pstw(src2, Cint _4, addr))
-  | _ ->
-      assert false
-  end
-
-let expand_builtin_vstore_global chunk id ofs args =
-  begin match args with
-  | [src] when chunk <> Mint64 ->
-      let tmp = if src = IR GPR11 then GPR12 else GPR11 in
-      emit (Paddis(tmp, GPR0, Csymbol_high(id, ofs)));
-      expand_builtin_vstore_common chunk tmp (Csymbol_low(id, ofs)) src
-  | [IR src1; IR src2] when chunk = Mint64 ->
-      let tmp =
-        if not (List.mem GPR12 [src1; src2]) then GPR12 else
-        if not (List.mem GPR11 [src1; src2]) then GPR11 else GPR10 in
-      emit (Paddis(tmp, GPR0, Csymbol_high(id, ofs)));
-      emit (Pstw(src1, Csymbol_low(id, ofs), tmp));
-      let ofs = Int.add ofs _4 in
-      emit (Paddis(tmp, GPR0, Csymbol_high(id, ofs)));
-      emit (Pstw(src2, Csymbol_low(id, ofs), tmp))
-  | _ ->
-      assert false
-  end
-
-let expand_builtin_vstore_sda chunk id ofs args =
-  begin match args with
-  | [src] when chunk <> Mint64 ->
-      expand_builtin_vstore_common chunk GPR0 (Csymbol_sda(id, ofs)) src
-  | [IR src1; IR src2] when chunk = Mint64 ->
-      emit (Pstw(src1, Csymbol_sda(id, ofs), GPR0));
-      let ofs = Int.add ofs _4 in
-      emit (Pstw(src2, Csymbol_sda(id, ofs), GPR0))
+  | [BA_addrstack ofs; src] ->
+      if offset_in_range ofs then
+        expand_builtin_vstore_common chunk GPR1 (Cint ofs) src
+      else begin
+        let tmp = temp_for_vstore src in
+        emit_addimm tmp GPR1 ofs;
+        expand_builtin_vstore_common chunk tmp (Cint _0) src
+      end
+  | [BA_addrglobal(id, ofs); src] ->
+      if symbol_is_small_data id ofs then
+        expand_builtin_vstore_common chunk GPR0 (Csymbol_sda(id, ofs)) src
+      else if symbol_is_rel_data id ofs then begin
+        let tmp = temp_for_vstore src in
+        emit (Paddis(tmp, GPR0, Csymbol_rel_high(id, ofs)));
+        expand_builtin_vstore_common chunk tmp (Csymbol_rel_low(id, ofs)) src
+      end else begin
+        let tmp = temp_for_vstore src in
+        emit (Paddis(tmp, GPR0, Csymbol_high(id, ofs)));
+        expand_builtin_vstore_common chunk tmp (Csymbol_low(id, ofs)) src
+      end
   | _ ->
       assert false
-  end
-
-let expand_builtin_vstore_rel chunk id ofs args =
-  let tmp =
-    if not (List.mem (IR GPR12) args) then GPR12 else
-    if not (List.mem (IR GPR11) args) then GPR11 else GPR10 in
-  emit (Paddis(tmp, GPR0, Csymbol_rel_high(id, ofs)));
-  emit (Paddi(tmp, tmp, Csymbol_rel_low(id, ofs)));
-  expand_builtin_vstore chunk (IR tmp :: args)
 
 (* Handling of varargs *)
 
@@ -302,49 +324,99 @@ let expand_builtin_va_start r =
 let expand_int64_arith conflict rl fn =
   if conflict then (fn GPR0; emit (Pmr(rl, GPR0))) else fn rl
 
+(* Handling of cache instructions *)
+
+(* Auxiliary function to generate address for the cache function *)
+let expand_builtin_cache_common addr f =
+  let add = match addr with
+  | BA (IR a1) -> a1
+  | BA_addrstack ofs ->
+      emit_addimm GPR11 GPR1 ofs;
+      GPR11
+  | BA_addrglobal(id, ofs) ->
+      if symbol_is_small_data id ofs then begin
+        emit (Paddi (GPR11, GPR0, Csymbol_sda(id, ofs)));
+        GPR11
+      end else if symbol_is_rel_data id ofs then begin
+        emit (Paddis(GPR11, GPR0, Csymbol_rel_high(id, ofs)));
+        emit (Paddi(GPR11, GPR11, Csymbol_rel_low(id, ofs)));
+        GPR11
+      end else begin
+        emit (Paddis(GPR11, GPR0, Csymbol_high(id, ofs)));
+        emit (Paddi (GPR11, GPR11, Csymbol_low(id, ofs)));
+        GPR11
+      end 
+  | _ -> raise (Error "Argument is not an address") in
+  f add
+ 
+let expand_builtin_prefetch addr rw loc =
+  if not ((loc >= _0) && (loc <= _2)) then
+    raise (Error "the last argument of __builtin_prefetch must be a constant between 0 and 2");
+  let emit_prefetch_instr addr =
+    if Int.eq rw _0 then begin
+      emit (Pdcbt (loc,GPR0,addr));
+    end else if Int.eq rw _1 then begin
+      emit (Pdcbtst (loc,GPR0,addr));
+    end else
+      raise (Error "the second argument of __builtin_prefetch must be either 0 or 1")
+  in
+  expand_builtin_cache_common addr emit_prefetch_instr
+
+let expand_builtin_dcbtls addr loc =
+  if not ((loc == _0) || (loc = _2)) then
+    raise (Error "the second argument of __builtin_dcbtls must be a constant between 0 and 2");
+  let emit_inst addr = emit (Pdcbtls (loc,GPR0,addr)) in
+  expand_builtin_cache_common addr emit_inst
+
+let expand_builtin_icbtls addr loc =
+  if not ((loc == _0) || (loc = _2)) then
+    raise (Error "the second argument of __builtin_icbtls must be a constant between 0 and 2");
+  let emit_inst addr = emit (Picbtls (loc,GPR0,addr)) in
+  expand_builtin_cache_common addr emit_inst
+
 (* Handling of compiler-inlined builtins *)
 
 let expand_builtin_inline name args res =
   (* Can use as temporaries: GPR0, FPR13 *)
   match name, args, res with
   (* Integer arithmetic *)
-  | "__builtin_mulhw", [IR a1; IR a2], [IR res] ->
+  | "__builtin_mulhw", [BA(IR a1); BA(IR a2)], BR(IR res) ->
       emit (Pmulhw(res, a1, a2))
-  | "__builtin_mulhwu", [IR a1; IR a2], [IR res] ->
+  | "__builtin_mulhwu", [BA(IR a1); BA(IR a2)], BR(IR res) ->
       emit (Pmulhwu(res, a1, a2))
-  | "__builtin_clz", [IR a1], [IR res] ->
+  | "__builtin_clz", [BA(IR a1)], BR(IR res) ->
       emit (Pcntlzw(res, a1))
-  | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] ->
+  | ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
       emit (Pstwu(a1, Cint _m8, GPR1));
       emit (Pcfi_adjust _8);
       emit (Plwbrx(res, GPR0, GPR1));
       emit (Paddi(GPR1, GPR1, Cint _8));
       emit (Pcfi_adjust _m8)
-  | "__builtin_bswap16", [IR a1], [IR res] ->
+  | "__builtin_bswap16", [BA(IR a1)], BR(IR res) ->
       emit (Prlwinm(GPR0, a1, _8, coqint_of_camlint 0x0000FF00l));
       emit (Prlwinm(res, a1, coqint_of_camlint 24l,
                                   coqint_of_camlint 0x000000FFl));
       emit (Por(res, GPR0, res))
   (* Float arithmetic *)
-  | "__builtin_fmadd", [FR a1; FR a2; FR a3], [FR res] ->
+  | "__builtin_fmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) ->
       emit (Pfmadd(res, a1, a2, a3))
-  | "__builtin_fmsub", [FR a1; FR a2; FR a3], [FR res] ->
+  | "__builtin_fmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) ->
       emit (Pfmsub(res, a1, a2, a3))
-  | "__builtin_fnmadd", [FR a1; FR a2; FR a3], [FR res] ->
+  | "__builtin_fnmadd", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) ->
       emit (Pfnmadd(res, a1, a2, a3))
-  | "__builtin_fnmsub", [FR a1; FR a2; FR a3], [FR res] ->
+  | "__builtin_fnmsub", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) ->
       emit (Pfnmsub(res, a1, a2, a3))
-  | "__builtin_fabs", [FR a1], [FR res] ->
+  | "__builtin_fabs", [BA(FR a1)], BR(FR res) ->
       emit (Pfabs(res, a1))
-  | "__builtin_fsqrt", [FR a1], [FR res] ->
+  | "__builtin_fsqrt", [BA(FR a1)], BR(FR res) ->
       emit (Pfsqrt(res, a1))
-  | "__builtin_frsqrte", [FR a1], [FR res] ->
+  | "__builtin_frsqrte", [BA(FR a1)], BR(FR res) ->
       emit (Pfrsqrte(res, a1))
-  | "__builtin_fres", [FR a1], [FR res] ->
+  | "__builtin_fres", [BA(FR a1)], BR(FR res) ->
       emit (Pfres(res, a1))
-  | "__builtin_fsel", [FR a1; FR a2; FR a3], [FR res] ->
+  | "__builtin_fsel", [BA(FR a1); BA(FR a2); BA(FR a3)], BR(FR res) ->
       emit (Pfsel(res, a1, a2, a3))
-  | "__builtin_fcti", [FR a1], [IR res] ->
+  | "__builtin_fcti", [BA(FR a1)], BR(IR res) ->
       emit (Pfctiw(FPR13, a1));
       emit (Pstfdu(FPR13, Cint _m8, GPR1));
       emit (Pcfi_adjust _8);
@@ -352,30 +424,36 @@ let expand_builtin_inline name args res =
       emit (Paddi(GPR1, GPR1, Cint _8));
       emit (Pcfi_adjust _m8)
   (* 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 (Psubfic(rl, al, Cint _0));
         emit (Psubfze(rh, ah)))
-  | "__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 (Paddc(rl, al, bl));
         emit (Padde(rh, ah, 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 (Psubfc(rl, bl, al));
         emit (Psubfe(rh, bh, ah)))
-  | "__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)) ->
       expand_int64_arith (rl = a || rl = b) rl (fun rl ->
         emit (Pmullw(rl, a, b));
         emit (Pmulhwu(rh, a, b)))
   (* Memory accesses *)
-  | "__builtin_read16_reversed", [IR a1], [IR res] ->
+  | "__builtin_read16_reversed", [BA(IR a1)], BR(IR res) ->
       emit (Plhbrx(res, GPR0, a1))
-  | "__builtin_read32_reversed", [IR a1], [IR res] ->
+  | "__builtin_read32_reversed", [BA(IR a1)], BR(IR res) ->
       emit (Plwbrx(res, GPR0, a1))
-  | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
+  | "__builtin_write16_reversed", [BA(IR a1); BA(IR a2)], _ ->
       emit (Psthbrx(a2, GPR0, a1))
-  | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
+  | "__builtin_write32_reversed", [BA(IR a1); BA(IR a2)], _ ->
       emit (Pstwbrx(a2, GPR0, a1))
   (* Synchronization *)
   | "__builtin_membar", [], _ ->
@@ -388,20 +466,50 @@ let expand_builtin_inline name args res =
       emit (Pisync)
   | "__builtin_lwsync", [], _ ->
       emit (Plwsync)
+  | "__builtin_mbar",  [BA_int mo], _ ->
+      if not (mo = _0 || mo = _1) then
+        raise (Error "the argument of __builtin_mbar must be either 0 or 1");
+      emit (Pmbar mo)
+  | "__builin_mbar",_, _ ->
+      raise (Error "the argument of __builtin_mbar must be a constant");
   | "__builtin_trap", [], _ ->
       emit (Ptrap)
   (* Vararg stuff *)
-  | "__builtin_va_start", [IR a], _ ->
+  | "__builtin_va_start", [BA(IR a)], _ ->
       expand_builtin_va_start a
-  (* Catch-all *)
-  | "__builtin_dcbf", [IR a1],_ ->
+  (* Cache control *)
+  | "__builtin_dcbf", [BA(IR a1)],_ ->
       emit (Pdcbf (GPR0,a1))
-  | "__builtin_dcbi", [IR a1],_ ->
+  | "__builtin_dcbi", [BA(IR a1)],_ ->
       emit (Pdcbi (GPR0,a1))
-  | "__builtin_icbi", [IR a1],_ ->
+  | "__builtin_icbi", [BA(IR a1)],_ ->
       emit (Picbi(GPR0,a1))
+  | "__builtin_dcbtls", [a; BA_int loc],_ ->
+     expand_builtin_dcbtls a loc
+  | "__builtin_dcbtls",_,_ ->
+      raise (Error "the second argument of __builtin_dcbtls must be a constant")
+  | "__builtin_icbtls", [a; BA_int loc],_ ->
+     expand_builtin_icbtls a loc
+  | "__builtin_icbtls",_,_ ->
+      raise (Error "the second argument of __builtin_icbtls must be a constant")
+  | "__builtin_prefetch" , [a1 ;BA_int rw; BA_int loc],_ ->
+      expand_builtin_prefetch a1 rw loc
+  | "__builtin_prefetch" ,_,_ ->
+      raise (Error "the second and third argument of __builtin_prefetch must be a constant")
+  | "__builtin_dcbz",[BA (IR a1)],_ ->
+      emit (Pdcbz (GPR0,a1))
+  (* Special registers *)
+  | "__builtin_get_spr", [BA_int n], BR(IR res) ->
+      emit (Pmfspr(res, n))
+  | "__builtin_get_spr", _, _ ->
+      raise (Error "the argument of __builtin_get_spr must be a constant")
+  | "__builtin_set_spr", [BA_int n; BA(IR a1)], _ ->
+      emit (Pmtspr(n, a1))
+  | "__builtin_set_spr", _, _ ->
+      raise (Error "the first argument of __builtin_set_spr must be a constant")
+  (* Catch-all *)
   | _ ->
-      invalid_arg ("unrecognized builtin " ^ name)
+      raise (Error ("unrecognized builtin " ^ name))
 
 (* Calls to variadic functions: condition bit 6 must be set
    if at least one argument is a float; clear otherwise.
@@ -484,25 +592,11 @@ let expand_instruction instr =
           expand_builtin_vload chunk args res
       | EF_vstore chunk ->
           expand_builtin_vstore chunk args
-      | EF_vload_global(chunk, id, ofs) ->
-          if symbol_is_small_data id ofs then
-             expand_builtin_vload_sda chunk id ofs args res
-          else if symbol_is_rel_data id ofs then
-             expand_builtin_vload_rel chunk id ofs args res
-          else
-             expand_builtin_vload_global chunk id ofs args res
-      | EF_vstore_global(chunk, id, ofs) ->
-          if symbol_is_small_data id ofs then
-            expand_builtin_vstore_sda chunk id ofs args
-          else if symbol_is_rel_data id ofs then
-            expand_builtin_vstore_rel chunk id ofs args
-          else
-            expand_builtin_vstore_global chunk id ofs args
       | EF_memcpy(sz, al) ->
           expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args
       | EF_annot_val(txt, targ) ->
           expand_annot_val txt targ args res
-      | EF_inline_asm(txt, sg, clob) ->
+       | EF_annot _ | EF_debug _ | EF_inline_asm _ ->
           emit instr
       | _ ->
           assert false
@@ -511,13 +605,21 @@ let expand_instruction instr =
       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
+  | 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 =
-  AST.transform_program expand_fundef p
+let expand_program (p: Asm.program) : Asm.program Errors.res =
+  AST.transform_partial_program expand_fundef p
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v
index 7ee6c770..541fe7c6 100644
--- a/powerpc/Asmgen.v
+++ b/powerpc/Asmgen.v
@@ -648,9 +648,7 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction)
           Pfreeframe f.(fn_stacksize) f.(fn_link_ofs) :: 
           Pbs 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/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index 27b32ba1..ece6af1a 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -754,48 +754,32 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen.
   unfold rs5; auto 10 with asmgen.
 
 - (* 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/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 06a7e395..e18fdb2d 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -85,6 +85,8 @@ let builtins = {
       (TVoid [], [], false);
     "__builtin_lwsync",
       (TVoid [], [], false);
+    "__builtin_mbar",
+      (TVoid [], [TInt(IInt, [])], false);
     "__builtin_trap",
       (TVoid [], [], false);
     (* Cache isntructions *)
@@ -93,7 +95,20 @@ let builtins = {
     "__builtin_dcbi",
       (TVoid [],[TPtr(TVoid [], [])],false);
     "__builtin_icbi",
-      (TVoid [],[TPtr(TVoid [], [])],false)
+      (TVoid [],[TPtr(TVoid [], [])],false);
+    "__builtin_prefetch",
+      (TVoid [], [TPtr (TVoid [],[]);TInt (IInt, []);TInt (IInt,[])],false);
+    "__builtin_dcbtls",
+      (TVoid[], [TPtr (TVoid [],[]);TInt (IInt,[])],false);
+    "__builtin_icbtls",
+      (TVoid[], [TPtr (TVoid [],[]);TInt (IInt,[])],false);
+    "__builtin_dcbz",
+      (TVoid[], [TPtr (TVoid [],[])],false);
+    (* Access to special registers *)
+    "__builtin_get_spr",
+      (TInt(IUInt, []), [TInt(IInt, [])], false);
+    "__builtin_set_spr",
+      (TVoid [], [TInt(IInt, []); TInt(IUInt, [])], false)
   ]
 }
 
diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v
index 3b7cbb76..402f07d1 100644
--- a/powerpc/Machregs.v
+++ b/powerpc/Machregs.v
@@ -163,11 +163,9 @@ Fixpoint destroyed_by_clobber (cl: list string): list mreg :=
 Definition destroyed_by_builtin (ef: external_function): list mreg :=
   match ef with
   | EF_builtin _ _ => F13 :: nil
-  | EF_vload _ => nil
-  | EF_vstore _ => nil
-  | EF_vload_global _ _ _ => R11 :: nil
-  | EF_vstore_global Mint64 _ _ => R10 :: R11 :: R12 :: nil
-  | EF_vstore_global _ _ _ => R11 :: R12 :: nil
+  | EF_vload _ => R11 :: nil
+  | EF_vstore Mint64 => R10 :: R11 :: R12 :: nil
+  | EF_vstore _ => R11 :: R12 :: nil
   | EF_memcpy _ _ => R11 :: R12 :: F13 :: nil
   | EF_inline_asm txt sg clob => destroyed_by_clobber clob
   | _ => nil
@@ -203,3 +201,31 @@ Definition two_address_op (op: operation) : bool :=
   | Oroli _ _ => true
   | _ => false
   end.
+
+(* Constraints on constant propagation for builtins *)
+
+Definition builtin_get_spr := ident_of_string "__builtin_get_spr".
+Definition builtin_set_spr := ident_of_string "__builtin_set_spr".
+Definition builtin_prefetch := ident_of_string "__builtin_prefetch".
+Definition builtin_dcbtls := ident_of_string "__builtin_dcbtls".
+Definition builtin_icbtls := ident_of_string "__builtin_icbtls".
+Definition builtin_mbar := ident_of_string "__builtin_mbar".
+
+Definition builtin_constraints (ef: external_function) :
+                                       list builtin_arg_constraint :=
+  match ef with
+  | EF_builtin id sg =>
+      if ident_eq id builtin_get_spr then OK_const :: nil
+      else if ident_eq id builtin_set_spr then OK_const :: OK_default :: nil
+      else if ident_eq id builtin_prefetch then OK_addrany :: OK_const :: OK_const :: nil
+      else if ident_eq id builtin_dcbtls then OK_addrany::OK_const::nil
+      else if ident_eq id builtin_icbtls then OK_addrany::OK_const::nil
+      else if ident_eq id builtin_mbar then OK_const::nil
+      else nil
+  | 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/powerpc/SelectOp.vp b/powerpc/SelectOp.vp
index 618643b8..6d39569e 100644
--- a/powerpc/SelectOp.vp
+++ b/powerpc/SelectOp.vp
@@ -524,17 +524,17 @@ 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 (Aglobal id ofs) Enil => AA_loadglobal chunk id ofs
-  | 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 (Aglobal id ofs) Enil => BA_loadglobal chunk id ofs
+  | Eload chunk (Ainstack ofs) Enil => BA_loadstack chunk ofs
+  | _ => BA e
   end.
diff --git a/powerpc/SelectOpproof.v b/powerpc/SelectOpproof.v
index c51b650b..147132dd 100644
--- a/powerpc/SelectOpproof.v
+++ b/powerpc/SelectOpproof.v
@@ -999,12 +999,12 @@ Proof.
   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. 
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 1e78f038..409f2cc0 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -358,17 +358,6 @@ module Target (System : SYSTEM):TARGET =
       assert (!count = 2 || (!count = 0 && !last));
       (!mb, !me-1)
 
-    (* 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_annot "R1" oc txt targs args
-      end
-
     (* Determine if the displacement of a conditional branch fits the short form *)
 
     let short_cond_branch tbl pc lbl_dest =
@@ -473,6 +462,14 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	dcbf	%a, %a\n" ireg r1 ireg r2
       | Pdcbi (r1,r2) ->
           fprintf oc "	dcbi	%a, %a\n" ireg r1 ireg r2
+      | Pdcbt (c,r1,r2) ->
+          fprintf oc "	dcbt	%ld, %a, %a\n" (camlint_of_coqint c) ireg r1  ireg r2
+      | Pdcbtst (c,r1,r2) ->
+          fprintf oc "	dcbtst	%ld, %a, %a\n"  (camlint_of_coqint c) ireg r1 ireg r2
+      | Pdcbtls (c,r1,r2) ->
+          fprintf oc "	dcbtls	%ld, %a, %a\n" (camlint_of_coqint c) ireg r1 ireg r2
+      | Pdcbz (r1,r2) ->
+          fprintf oc "	dcbz	%a, %a\n" ireg r1 ireg r2
       | Pdivw(r1, r2, r3) ->
           fprintf oc "	divw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
       | Pdivwu(r1, r2, r3) ->
@@ -541,6 +538,8 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fsel	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
       | Picbi (r1,r2) ->
           fprintf oc "	icbi	%a,%a\n" ireg r1 ireg r2
+      | Picbtls (n,r1,r2) ->
+          fprintf oc "	icbtls	%ld, %a, %a\n" (camlint_of_coqint n) ireg r1 ireg r2
       | Pisync ->
           fprintf oc "	isync\n"
       | Plwsync ->
@@ -587,6 +586,8 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	lwzu	%a, %a(%a)\n" ireg r1 constant c ireg r2
       | Plwzx(r1, r2, r3) | Plwzx_a(r1, r2, r3) ->
           fprintf oc "	lwzx	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
+      | Pmbar mo ->
+          fprintf oc "	mbar	%ld\n" (camlint_of_coqint mo)
       | Pmfcr(r1) ->
           fprintf oc "	mfcr	%a\n" ireg r1
       | Pmfcrbit(r1, bit) ->
@@ -599,6 +600,10 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	mtctr	%a\n" ireg r1
       | Pmtlr(r1) ->
           fprintf oc "	mtlr	%a\n" ireg r1
+      | Pmfspr(rd, spr) ->
+          fprintf oc "	mfspr	%a, %ld\n" ireg rd (camlint_of_coqint spr)
+      | Pmtspr(spr, rs) ->
+          fprintf oc "	mtspr	%ld, %a\n" (camlint_of_coqint spr) ireg rs
       | Pmulli(r1, r2, c) ->
           fprintf oc "	mulli	%a, %a, %a\n" ireg r1 ireg r2 constant c
       | Pmullw(r1, r2, r3) ->
@@ -693,6 +698,12 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "%a:\n" label (transl_label lbl)
       | Pbuiltin(ef, args, res) ->
           begin match ef with
+          | EF_annot(txt, targs) ->
+              fprintf oc "%s annotation: " comment;
+              print_annot_text preg_annot "r1" oc (extern_atom txt) args
+          | EF_debug(kind, txt, targs) ->
+              print_debug_info comment print_file_line preg_annot "r1" oc
+                               (P.to_int kind) (extern_atom txt) args
           | 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;
@@ -700,13 +711,6 @@ module Target (System : SYSTEM):TARGET =
           | _ ->
               assert false
           end
-      | Pannot(ef, args) ->
-          begin match ef with
-          | EF_annot(txt, targs) ->
-              print_annot_stmt oc (extern_atom txt) targs args
-          | _ ->
-              assert false
-          end
       | Pcfi_adjust n ->
           cfi_adjust oc (camlint_of_coqint n)
       | Pcfi_rel_offset n ->
@@ -731,8 +735,8 @@ module Target (System : SYSTEM):TARGET =
       | Plfi(r1, c) -> 2
       | Plfis(r1, c) -> 2
       | Plabel lbl -> 0
-      | Pbuiltin(ef, args, res) -> 0
-      | Pannot(ef, args) -> 0
+      | Pbuiltin((EF_annot _ | EF_debug _), args, res) -> 0
+      | Pbuiltin(ef, args, res) -> 3
       | Pcfi_adjust _ | Pcfi_rel_offset _ -> 0
       | _ -> 1