diff options
-rw-r--r-- | Changelog | 4 | ||||
-rw-r--r-- | arm/PrintAsm.ml | 28 | ||||
-rw-r--r-- | backend/CMparser.mly | 3 | ||||
-rw-r--r-- | backend/Constprop.v | 39 | ||||
-rw-r--r-- | backend/Constpropproof.v | 74 | ||||
-rw-r--r-- | backend/PrintAnnot.ml | 76 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 6 | ||||
-rw-r--r-- | cfrontend/Cexec.v | 9 | ||||
-rw-r--r-- | common/AST.v | 18 | ||||
-rw-r--r-- | common/Events.v | 21 | ||||
-rw-r--r-- | ia32/ConstpropOp.vp | 11 | ||||
-rw-r--r-- | ia32/ConstpropOpproof.v | 18 | ||||
-rw-r--r-- | ia32/PrintAsm.ml | 30 | ||||
-rw-r--r-- | powerpc/PrintAsm.ml | 28 | ||||
-rw-r--r-- | test/regression/annot1.c | 9 |
15 files changed, 250 insertions, 124 deletions
@@ -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"); |