Adapt the PowerPC port to the new builtin representation.

__builtin_get_spr() and __builtin_set_spr() work, but horrible error
message if the SPR argument is not a constant.

powerpc/AsmToJSON.ml needs updating.

10 files changed, 285 insertions, 258 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index b7656dc4..a724f932 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -232,6 +232,8 @@ Inductive instruction : Type :=
   | 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 +281,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 +387,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_longofwords 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,10 +862,8 @@ 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 _ _ _
@@ -881,6 +889,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Plhbrx _ _ _
   | Plwzu _ _ _
   | Pmfcr _
+  | Pmfspr _ _
+  | Pmtspr _ _
   | Pstwbrx _ _ _
   | Pstwcx_ _ _ _
   | Pstfdu _ _ _
@@ -954,24 +964,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 +1037,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 +1046,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 +1065,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..3440e16f 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -243,6 +243,8 @@ let p_instruction oc ic =
   | 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 n
+  | Pmtspr(n, ir) -> fprintf oc "{\"Instruction Name\":\"Pmtspr\",\"Args\":[%a,%a]}" p_int 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
   | Pmulhw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pmulhw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
@@ -289,7 +291,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 +301,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 +334,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 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..9f6c5f76 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -44,11 +44,11 @@ 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
@@ -62,34 +62,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 memcpy_small_arg sz arg otherarg tmp1 tmp2 =
+  match arg with
+  | BA (IR r) ->
+      (r, _0)
+  | BA_addrstack ofs ->
+      if Int.eq (Asmgen.high_s ofs) Int.zero
+      && Int.eq (Asmgen.high_s (Int.add ofs (Int.repr (Z.of_uint sz))))
+                Int.zero
+      then (GPR1, ofs)
+      else begin
+        let tmp = if otherarg = BA (IR tmp1) then tmp2 else tmp1 in
+        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 (rsrc, osrc) = memcpy_small_arg sz src dst GPR11 GPR12 in
+  let (rdst, odst) = memcpy_small_arg sz dst src GPR12 GPR11 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 +139,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 +148,129 @@ 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 Int.eq (Asmgen.high_s n') Int.zero 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 *)
-  | _ ->
-      assert false
+  | Mint64, BR_longofwords(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 Int.eq (Asmgen.high_s ofs) Int.zero 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 *)
-  | _ ->
-      assert false
+  | Mint64, BA_longofwords(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 Int.eq (Asmgen.high_s ofs) Int.zero 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 *)
 
@@ -308,43 +327,43 @@ 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 +371,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_longofwords(BA(IR ah), BA(IR al))],
+                      BR_longofwords(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_longofwords(BA(IR ah), BA(IR al));
+                       BA_longofwords(BA(IR bh), BA(IR bl))],
+                      BR_longofwords(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_longofwords(BA(IR ah), BA(IR al));
+                       BA_longofwords(BA(IR bh), BA(IR bl))],
+                      BR_longofwords(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_longofwords(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", [], _ ->
@@ -391,15 +416,25 @@ let expand_builtin_inline name args res =
   | "__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))
+  (* Special registers *)
+  | "__builtin_get_spr", [BA_int n], BR(IR res) ->
+      emit (Pmfspr(res, n))
+  | "__builtin_get_spr", _, _ ->
+      invalid_arg ("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", _, _ ->
+      invalid_arg ("the first argument of __builtin_set_spr must be a constant")
+  (* Catch-all *)
   | _ ->
       invalid_arg ("unrecognized builtin " ^ name)
 
@@ -484,25 +519,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
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..75dbd23d 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -93,7 +93,12 @@ let builtins = {
     "__builtin_dcbi",
       (TVoid [],[TPtr(TVoid [], [])],false);
     "__builtin_icbi",
-      (TVoid [],[TPtr(TVoid [], [])],false)
+      (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..b9af652a 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,23 @@ 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_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 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..31f7e2e4 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_longofwords (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 8610f750..5431d88d 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -599,6 +599,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 +697,8 @@ 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) ->
+              print_annot_stmt oc (extern_atom txt) targs 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 +706,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 +730,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