Constant propagation within __builtin_annot.

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

15 files changed, 250 insertions, 124 deletions

diff --git a/Changelog b/Changelog
index 243cdff7..cfb516d9 100644
--- a/Changelog
+++ b/Changelog
@@ -10,6 +10,10 @@ Development version
 - Comparisons involving pointers "one past" the end of a block are
   now defined.  (They used to be undefined behavior.)
   (Contributed by Robbert Krebbers).
+- Arguments to __builtin_annot() that are compile-time constants
+  are now replaced by their (integer or float) value in the annotation
+  generated in the assembly file.
+
 
 Release 1.12.1, 2013-01-29
 ==========================
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index d90d7b64..186e327d 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -226,33 +226,13 @@ let call_helper oc fn dst arg1 arg2 =
 
 (* Handling of annotations *)
 
-let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
-
-let print_annot_text print_arg oc txt args =
-  fprintf oc "%s annotation: " comment;
-  let print_fragment = function
-  | Str.Text s ->
-      output_string oc s
-  | Str.Delim "%%" ->
-      output_char oc '%'
-  | Str.Delim s ->
-      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
-      try
-        print_arg oc (List.nth args (n-1))
-      with Failure _ ->
-        fprintf oc "<bad parameter %s>" s in
-  List.iter print_fragment (Str.full_split re_annot_param txt);
-  fprintf oc "\n"
-
 let print_annot_stmt oc txt args =
-  let print_annot_param oc = function
-  | APreg r -> preg oc r
-  | APstack(chunk, ofs) ->
-      fprintf oc "mem(R1 + %a, %a)" coqint ofs coqint (size_chunk chunk) in
-  print_annot_text print_annot_param oc txt args
+  fprintf oc "%s annotation: " comment;
+  PrintAnnot.print_annot_stmt preg "sp" oc txt args
 
 let print_annot_val oc txt args res =
-  print_annot_text preg oc txt args;
+  fprintf oc "%s annotation: " comment;
+  PrintAnnot.print_annot_val preg oc txt args;
   match args, res with
   | IR src :: _, IR dst ->
       if dst = src then 0 else (fprintf oc "	mov	%a, %a\n" ireg dst ireg src; 1)
diff --git a/backend/CMparser.mly b/backend/CMparser.mly
index eb3b9ab9..273d572a 100644
--- a/backend/CMparser.mly
+++ b/backend/CMparser.mly
@@ -55,7 +55,8 @@ let mkef sg toks =
   | [EFT_tok "memcpy"; EFT_tok "size"; EFT_int sz; EFT_tok "align"; EFT_int al] ->
       EF_memcpy(Z.of_sint32 sz, Z.of_sint32 al)
   | [EFT_tok "annot"; EFT_string txt] ->
-      EF_annot(intern_string txt, sg.sig_args)
+      EF_annot(intern_string txt,
+               List.map (fun t -> AA_arg t) sg.sig_args)
   | [EFT_tok "annot_val"; EFT_string txt] ->
       if sg.sig_args = [] then raise Parsing.Parse_error;
       EF_annot_val(intern_string txt, List.hd sg.sig_args)
diff --git a/backend/Constprop.v b/backend/Constprop.v
index fe16240e..8fa0691a 100644
--- a/backend/Constprop.v
+++ b/backend/Constprop.v
@@ -296,6 +296,43 @@ Definition num_iter := 10%nat.
 Definition successor (f: function) (app: D.t) (pc: node) : node :=
   successor_rec num_iter f app pc.
 
+Function annot_strength_reduction
+     (app: D.t) (targs: list annot_arg) (args: list reg) :=
+  match targs, args with
+  | AA_arg ty :: targs', arg :: args' =>
+      let (targs'', args'') := annot_strength_reduction app targs' args' in
+      match ty, approx_reg app arg with
+      | Tint, I n => (AA_int n :: targs'', args'')
+      | Tfloat, F n => (AA_float n :: targs'', args'')
+      | _, _ => (AA_arg ty :: targs'', arg :: args'')
+      end
+  | targ :: targs', _ =>
+      let (targs'', args'') := annot_strength_reduction app targs' args in
+      (targ :: targs'', args'')
+  | _, _ =>
+      (targs, args)
+  end.
+
+Function builtin_strength_reduction
+      (app: D.t) (ef: external_function) (args: list reg) :=
+  match ef, args with
+  | EF_vload chunk, r1 :: nil =>
+      match approx_reg app r1 with
+      | G symb n1 => (EF_vload_global chunk symb n1, nil)
+      | _ => (ef, args)
+      end
+  | EF_vstore chunk, r1 :: r2 :: nil =>
+      match approx_reg app r1 with
+      | G symb n1 => (EF_vstore_global chunk symb n1, r2 :: nil)
+      | _ => (ef, args)
+      end
+  | EF_annot text targs, args =>
+      let (targs', args') := annot_strength_reduction app targs args in
+      (EF_annot text targs', args')
+  | _, _ =>
+      (ef, args)
+  end.
+
 Definition transf_instr (gapp: global_approx) (f: function) (apps: PMap.t D.t)
                        (pc: node) (instr: instruction) :=
   let app := apps!!pc in
@@ -328,7 +365,7 @@ Definition transf_instr (gapp: global_approx) (f: function) (apps: PMap.t D.t)
   | Itailcall sig ros args =>
       Itailcall sig (transf_ros app ros) args
   | Ibuiltin ef args res s =>
-      let (ef', args') := builtin_strength_reduction ef args (approx_regs app args) in
+      let (ef', args') := builtin_strength_reduction app ef args in
       Ibuiltin ef' args' res s
   | Icond cond args s1 s2 =>
       match eval_static_condition cond (approx_regs app args) with
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index cd757cdf..b223e892 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -469,6 +469,70 @@ Proof.
   unfold successor; intros. apply match_successor_rec.
 Qed.
 
+Section BUILTIN_STRENGTH_REDUCTION.
+Variable app: D.t.
+Variable sp: val.
+Variable rs: regset.
+Hypothesis MATCH: forall r, val_match_approx ge sp (approx_reg app r) rs#r.
+
+Lemma annot_strength_reduction_correct:
+  forall targs args targs' args' eargs,
+  annot_strength_reduction app targs args = (targs', args') ->
+  eventval_list_match ge eargs (annot_args_typ targs) rs##args ->
+  exists eargs',
+  eventval_list_match ge eargs' (annot_args_typ targs') rs##args'
+  /\ annot_eventvals targs' eargs' = annot_eventvals targs eargs.
+Proof.
+  induction targs; simpl; intros.
+- inv H. simpl. exists eargs; auto. 
+- destruct a.
+  + destruct args as [ | arg args0]; simpl in H0; inv H0.
+    destruct (annot_strength_reduction app targs args0) as [targs'' args''] eqn:E.
+    exploit IHtargs; eauto. intros [eargs'' [A B]].
+    assert (DFL:
+      exists eargs',
+      eventval_list_match ge eargs' (annot_args_typ (AA_arg ty :: targs'')) rs##(arg :: args'')
+      /\ annot_eventvals (AA_arg ty :: targs'') eargs' = ev1 :: annot_eventvals targs evl).
+    {
+      exists (ev1 :: eargs''); split.
+      simpl; constructor; auto. simpl. congruence.
+    }
+    destruct ty; destruct (approx_reg app arg) as [] eqn:E2; inv H; auto;
+    exists eargs''; split; auto; simpl; f_equal; auto;
+    generalize (MATCH arg); rewrite E2; simpl; intros E3;
+    rewrite E3 in H5; inv H5; auto.
+  + destruct (annot_strength_reduction app targs args) as [targs'' args''] eqn:E.
+    inv H.
+    exploit IHtargs; eauto. intros [eargs'' [A B]].
+    exists eargs''; simpl; split; auto. congruence.
+  + destruct (annot_strength_reduction app targs args) as [targs'' args''] eqn:E.
+    inv H.
+    exploit IHtargs; eauto. intros [eargs'' [A B]].
+    exists eargs''; simpl; split; auto. congruence.
+Qed.
+
+Lemma builtin_strength_reduction_correct:
+  forall ef args m t vres m',
+  external_call ef ge rs##args m t vres m' ->
+  let (ef', args') := builtin_strength_reduction app ef args in
+  external_call ef' ge rs##args' m t vres m'.
+Proof.
+  intros until m'. functional induction (builtin_strength_reduction app ef args); intros; auto.
++ generalize (MATCH r1); rewrite e1; simpl; intros E. simpl in H.
+  unfold symbol_address in E. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite E in H.
+  rewrite volatile_load_global_charact. exists b; auto. 
+  inv H.
++ generalize (MATCH r1); rewrite e1; simpl; intros E. simpl in H.
+  unfold symbol_address in E. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite E in H.
+  rewrite volatile_store_global_charact. exists b; auto. 
+  inv H.
++ inv H. exploit annot_strength_reduction_correct; eauto.
+  intros [eargs' [A B]]. 
+  rewrite <- B. econstructor; eauto. 
+Qed.
+
+End BUILTIN_STRENGTH_REDUCTION.
+
 (** The proof of semantic preservation is a simulation argument
   based on "option" diagrams of the following form:
 <<
@@ -708,15 +772,15 @@ Proof.
   (* Ibuiltin *)
   rename pc'0 into pc.
 Opaque builtin_strength_reduction.
-  destruct (builtin_strength_reduction ef args (approx_regs (analyze gapp f)#pc args)) as [ef' args'] eqn:?.
-  generalize (builtin_strength_reduction_correct ge sp (analyze gapp f)!!pc rs
-                  MATCH2 ef args (approx_regs (analyze gapp f) # pc args) _ _ _ _ (refl_equal _) H0).
-  rewrite Heqp. intros P.
+  exploit builtin_strength_reduction_correct; eauto. 
+  TransfInstr.
+  destruct (builtin_strength_reduction (analyze gapp f)#pc ef args) as [ef' args'].
+  intros P Q.
   exploit external_call_mem_extends; eauto. 
   instantiate (1 := rs'##args'). apply regs_lessdef_regs; auto.
   intros [v' [m2' [A [B [C D]]]]].
   left; econstructor; econstructor; split.
-  eapply exec_Ibuiltin. TransfInstr. rewrite Heqp. eauto.
+  eapply exec_Ibuiltin. eauto. 
   eapply external_call_symbols_preserved; eauto.
   exact symbols_preserved. exact varinfo_preserved.
   eapply match_states_succ; eauto. simpl; auto.
diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml
new file mode 100644
index 00000000..1ebb51f5
--- /dev/null
+++ b/backend/PrintAnnot.ml
@@ -0,0 +1,76 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              The Compcert verified compiler                         *)
+(*                                                                     *)
+(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
+(*                                                                     *)
+(*  Copyright Institut National de Recherche en Informatique et en     *)
+(*  Automatique.  All rights reserved.  This file is distributed       *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Printing annotations in asm syntax *)
+
+open Printf
+open Datatypes
+open Integers
+open Floats
+open Camlcoq
+open AST
+open Memdata
+open Asm
+
+let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
+
+type arg_value =
+  | Reg of preg
+  | Stack of memory_chunk * Int.int
+  | Intconst of Int.int
+  | Floatconst of float
+
+let print_annot_text print_preg sp_reg_name oc txt args =
+  let print_fragment = function
+  | Str.Text s ->
+      output_string oc s
+  | Str.Delim "%%" ->
+      output_char oc '%'
+  | Str.Delim s ->
+      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
+      try
+        match List.nth args (n-1) with
+        | Reg r ->
+            print_preg oc r
+        | Stack(chunk, ofs) ->
+            fprintf oc "mem(%s + %ld, %ld)"
+               sp_reg_name
+               (camlint_of_coqint ofs)
+               (camlint_of_coqint (size_chunk chunk))
+        | Intconst n ->
+            fprintf oc "%ld" (camlint_of_coqint n)
+        | Floatconst n ->
+            fprintf oc "%.18g" (camlfloat_of_coqfloat n)
+      with Failure _ ->
+        fprintf oc "<bad parameter %s>" s in
+  List.iter print_fragment (Str.full_split re_annot_param txt);
+  fprintf oc "\n"
+
+let rec annot_args tmpl args =
+  match tmpl, args with
+  | [], _ -> []
+  | AA_arg _ :: tmpl', APreg r :: args' ->
+      Reg r :: annot_args tmpl' args'
+  | AA_arg _ :: tmpl', APstack(chunk, ofs) :: args' ->
+      Stack(chunk, ofs) :: annot_args tmpl' args'
+  | AA_arg _ :: tmpl', [] -> []         (* should never happen *)
+  | AA_int n :: tmpl', _ ->
+      Intconst n :: annot_args tmpl' args
+  | AA_float n :: tmpl', _ ->
+      Floatconst n :: annot_args tmpl' args
+
+let print_annot_stmt print_preg sp_reg_name oc txt tmpl args =
+  print_annot_text print_preg sp_reg_name oc txt (annot_args tmpl args)
+
+let print_annot_val print_preg oc txt args =
+  print_annot_text print_preg "<internal error>" oc txt
+    (List.map (fun r -> Reg r) args)
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 4233af99..f34c396f 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -511,8 +511,10 @@ let rec convertExpr env e =
       begin match args with
       | {edesc = C.EConst(CStr txt)} :: args1 ->
           let targs1 = convertTypList env (List.map (fun e -> e.etyp) args1) in
-          Ebuiltin(EF_annot(intern_string txt, typlist_of_typelist targs1),
-                   targs1, convertExprList env args1, ty)
+          Ebuiltin(
+            EF_annot(intern_string txt,
+                     List.map (fun t -> AA_arg t) (typlist_of_typelist targs1)),
+            targs1, convertExprList env args1, ty)
       | _ ->
           error "ill-formed __builtin_annot (first argument must be string literal)";
           ezero
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index ded6b721..c638259b 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -478,10 +478,10 @@ Definition do_ef_memcpy (sz al: Z)
   | _ => None
   end.
 
-Definition do_ef_annot (text: ident) (targs: list typ)
+Definition do_ef_annot (text: ident) (targs: list annot_arg)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
-  do args <- list_eventval_of_val vargs targs;
-  Some(w, Event_annot text args :: E0, Vundef, m).
+  do args <- list_eventval_of_val vargs (annot_args_typ targs);
+  Some(w, Event_annot text (annot_eventvals targs args) :: E0, Vundef, m).
 
 Definition do_ef_annot_val (text: ident) (targ: typ)
        (w: world) (vargs: list val) (m: mem) : option (world * trace * val * mem) :=
@@ -578,7 +578,8 @@ Proof with try congruence.
   econstructor. constructor; eauto. constructor.
 (* EF_inline_asm *)
   unfold do_ef_annot. destruct vargs; simpl... mydestr. 
-  split. constructor. constructor. 
+  split. change (Event_annot text nil) with (Event_annot text (annot_eventvals nil nil)).
+  constructor. constructor. 
   econstructor. constructor; eauto. constructor.
 Qed.
 
diff --git a/common/AST.v b/common/AST.v
index d2065d6b..44811b2b 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -443,7 +443,7 @@ Inductive external_function : Type :=
          Produces no observable event. *)
   | EF_memcpy (sz: Z) (al: Z)
      (** Block copy, of [sz] bytes, between addresses that are [al]-aligned. *)
-  | EF_annot (text: ident) (targs: list typ)
+  | EF_annot (text: ident) (targs: list annot_arg)
      (** A programmer-supplied annotation.  Takes zero, one or several arguments,
          produces an event carrying the text and the values of these arguments,
          and returns no value. *)
@@ -451,15 +451,27 @@ Inductive external_function : Type :=
      (** Another form of annotation that takes one argument, produces
          an event carrying the text and the value of this argument,
          and returns the value of the argument. *)
-  | EF_inline_asm (text: ident).
+  | EF_inline_asm (text: ident)
      (** Inline [asm] statements.  Semantically, treated like an
          annotation with no parameters ([EF_annot text nil]).  To be
          used with caution, as it can invalidate the semantic
          preservation theorem.  Generated only if [-finline-asm] is
          given. *)
 
+with annot_arg : Type :=
+  | AA_arg (ty: typ)
+  | AA_int (n: int)
+  | AA_float (n: float).
+
 (** The type signature of an external function. *)
 
+Fixpoint annot_args_typ (targs: list annot_arg) : list typ :=
+  match targs with
+  | nil => nil
+  | AA_arg ty :: targs' => ty :: annot_args_typ targs'
+  | _ :: targs' => annot_args_typ targs'
+  end.
+
 Definition ef_sig (ef: external_function): signature :=
   match ef with
   | EF_external name sg => sg
@@ -471,7 +483,7 @@ Definition ef_sig (ef: external_function): signature :=
   | EF_malloc => mksignature (Tint :: nil) (Some Tint)
   | EF_free => mksignature (Tint :: nil) None
   | EF_memcpy sz al => mksignature (Tint :: Tint :: nil) None
-  | EF_annot text targs => mksignature targs None
+  | EF_annot text targs => mksignature (annot_args_typ targs) None
   | EF_annot_val text targ => mksignature (targ :: nil) (Some targ)
   | EF_inline_asm text => mksignature nil None
   end.
diff --git a/common/Events.v b/common/Events.v
index 3f81e60e..e310bfed 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -1456,23 +1456,32 @@ Proof.
   intros EQ; inv EQ. split; auto. eapply eventval_match_determ_1; eauto.
 Qed.
 
-(** ** Semantics of annotation. *)
+(** ** Semantics of annotations. *)
+
+Fixpoint annot_eventvals (targs: list annot_arg) (vargs: list eventval) : list eventval :=
+  match targs, vargs with
+  | AA_arg ty :: targs', varg :: vargs' => varg :: annot_eventvals targs' vargs'
+  | AA_int n :: targs', _ => EVint n :: annot_eventvals targs' vargs
+  | AA_float n :: targs', _ => EVfloat n :: annot_eventvals targs' vargs
+  | _, _ => vargs
+  end.
 
-Inductive extcall_annot_sem (text: ident) (targs: list typ) (F V: Type) (ge: Genv.t F V):
+Inductive extcall_annot_sem (text: ident) (targs: list annot_arg) (F V: Type) (ge: Genv.t F V):
               list val -> mem -> trace -> val -> mem -> Prop :=
   | extcall_annot_sem_intro: forall vargs m args,
-      eventval_list_match ge args targs vargs ->
-      extcall_annot_sem text targs ge vargs m (Event_annot text args :: E0) Vundef m.
+      eventval_list_match ge args (annot_args_typ targs) vargs ->
+      extcall_annot_sem text targs ge vargs m
+           (Event_annot text (annot_eventvals targs args) :: E0) Vundef m.
 
 Lemma extcall_annot_ok:
   forall text targs,
-  extcall_properties (extcall_annot_sem text targs) (mksignature targs None).
+  extcall_properties (extcall_annot_sem text targs) (mksignature (annot_args_typ targs) None).
 Proof.
   intros; constructor; intros.
 (* well typed *)
   inv H. simpl. auto.
 (* arity *)
-  inv H. eapply eventval_list_match_length; eauto.
+  inv H. simpl. eapply eventval_list_match_length; eauto.
 (* symbols *)
   inv H1. econstructor; eauto. 
   eapply eventval_list_match_preserved; eauto.
diff --git a/ia32/ConstpropOp.vp b/ia32/ConstpropOp.vp
index 8a612f06..e6ba98a9 100644
--- a/ia32/ConstpropOp.vp
+++ b/ia32/ConstpropOp.vp
@@ -307,15 +307,4 @@ Nondetfunction op_strength_reduction
   | _, _, _ => (op, args)
   end.
 
-Nondetfunction builtin_strength_reduction
-               (ef: external_function) (args: list reg) (vl: list approx) :=
-  match ef, args, vl with
-  | EF_vload chunk, r1 :: nil, G symb n1 :: nil =>
-      (EF_vload_global chunk symb n1, nil)
-  | EF_vstore chunk, r1 :: r2 :: nil, G symb n1 :: v2 :: nil =>
-      (EF_vstore_global chunk symb n1, r2 :: nil)
-  | _, _, _ =>
-      (ef, args)
-  end.
-
 End STRENGTH_REDUCTION.
diff --git a/ia32/ConstpropOpproof.v b/ia32/ConstpropOpproof.v
index 90037435..d792d8a5 100644
--- a/ia32/ConstpropOpproof.v
+++ b/ia32/ConstpropOpproof.v
@@ -421,24 +421,6 @@ Proof.
   exists v; auto.
 Qed.
 
-Lemma builtin_strength_reduction_correct:
-  forall ef args vl m t vres m',
-  vl = approx_regs app args ->
-  external_call ef ge rs##args m t vres m' ->
-  let (ef', args') := builtin_strength_reduction ef args vl in
-  external_call ef' ge rs##args' m t vres m'.
-Proof.
-  intros until m'. unfold builtin_strength_reduction.
-  destruct (builtin_strength_reduction_match ef args vl); simpl; intros; InvApproxRegs; SimplVMA.
-  unfold symbol_address in H. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H in H0.
-  rewrite volatile_load_global_charact. exists b; auto. 
-  inv H0.
-  unfold symbol_address in H1. destruct (Genv.find_symbol ge symb) as [b|] eqn:?; rewrite H1 in H0.
-  rewrite volatile_store_global_charact. exists b; auto. 
-  inv H0.
-  auto.
-Qed.
-
 End STRENGTH_REDUCTION.
 
 End ANALYSIS.
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index 00744055..4f626405 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -231,33 +231,13 @@ let need_masks = ref false
 
 (* Handling of annotations *)
 
-let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
-
-let print_annot_text print_arg oc txt args =
-  fprintf oc "%s annotation: " comment;
-  let print_fragment = function
-  | Str.Text s ->
-      output_string oc s
-  | Str.Delim "%%" ->
-      output_char oc '%'
-  | Str.Delim s ->
-      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
-      try
-        print_arg oc (List.nth args (n-1))
-      with Failure _ ->
-        fprintf oc "<bad parameter %s>" s in
-  List.iter print_fragment (Str.full_split re_annot_param txt);
-  fprintf oc "\n"
-
 let print_annot_stmt oc txt args =
-  let print_annot_param oc = function
-  | APreg r -> preg oc r
-  | APstack(chunk, ofs) ->
-      fprintf oc "mem(ESP + %a, %a)" coqint ofs coqint (size_chunk chunk) in
-  print_annot_text print_annot_param oc txt args
+  fprintf oc "%s annotation: " comment;
+  PrintAnnot.print_annot_stmt preg "ESP" oc txt args
 
 let print_annot_val oc txt args res =
-  print_annot_text preg oc txt args;
+  fprintf oc "%s annotation: " comment;
+  PrintAnnot.print_annot_val preg oc txt args;
   match args, res with
   | IR src :: _, IR dst ->
       if dst <> src then fprintf oc "	movl	%a, %a\n" ireg src ireg dst
@@ -723,7 +703,7 @@ let print_instruction oc = function
   | Pannot(ef, args) ->
       begin match ef with
       | EF_annot(txt, targs) ->
-          print_annot_stmt oc (extern_atom txt) args
+          print_annot_stmt oc (extern_atom txt) targs args
       | _ ->
           assert false
       end
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 2ba3cfeb..9c0f471d 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -231,33 +231,13 @@ let rolm_mask n =
 
 (* Handling of annotations *)
 
-let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*"
-
-let print_annot_text print_arg oc txt args =
-  fprintf oc "%s annotation: " comment;
-  let print_fragment = function
-  | Str.Text s ->
-      output_string oc s
-  | Str.Delim "%%" ->
-      output_char oc '%'
-  | Str.Delim s ->
-      let n = int_of_string (String.sub s 1 (String.length s - 1)) in
-      try
-        print_arg oc (List.nth args (n-1))
-      with Failure _ ->
-        fprintf oc "<bad parameter %s>" s in
-  List.iter print_fragment (Str.full_split re_annot_param txt);
-  fprintf oc "\n"
-
 let print_annot_stmt oc txt args =
-  let print_annot_param oc = function
-  | APreg r -> preg oc r
-  | APstack(chunk, ofs) ->
-      fprintf oc "mem(R1 + %a, %a)" coqint ofs coqint (size_chunk chunk) in
-  print_annot_text print_annot_param oc txt args
+  fprintf oc "%s annotation: " comment;
+  PrintAnnot.print_annot_stmt preg "R1" oc txt args
 
 let print_annot_val oc txt args res =
-  print_annot_text preg oc txt args;
+  fprintf oc "%s annotation: " comment;
+  PrintAnnot.print_annot_val preg oc txt args;
   match args, res with
   | IR src :: _, IR dst ->
       if dst <> src then fprintf oc "	mr	%a, %a\n" ireg dst ireg src 
diff --git a/test/regression/annot1.c b/test/regression/annot1.c
index 2763a8cf..9bdf14eb 100644
--- a/test/regression/annot1.c
+++ b/test/regression/annot1.c
@@ -49,6 +49,15 @@ int h(int a)
   return dd;
 }
 
+const int C1 = 42;
+const double C2 = 3.14;
+
+void k(int arg)
+{
+  __builtin_annot("C1 + 1 is %1 and arg is %2 and C2 * 2 is %3",
+                  C1 + 1, arg, C2 * 2);
+}
+
 int main()
 {
   __builtin_annot("calling f");