From 6a010b47b216c5a6b6e85abcfbba5339bab15dd6 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Thu, 19 Oct 2017 13:08:13 +0200 Subject: New support for inserting ais-annotations. The ais annotations can be inserted via the new ais variants of the builtin annotation. They mainly differe in that they have an address format specifier '%addr' which will be replaced by the adress in the binary. The implementation simply prints a label for the builtin call alongside a the text of the annotation as comment and inserts the annotation together as acii string in a separate section 'ais_annotations' and replaces the usages of the address format specifiers by the address of the label of the builtin call. --- arm/Asmexpand.ml | 8 ++++---- arm/Machregs.v | 2 +- arm/TargetPrinter.ml | 14 +++++++++++--- backend/CSE.v | 2 +- backend/Deadcode.v | 2 +- backend/Deadcodeproof.v | 4 ++-- backend/PrintAsm.ml | 18 ++++++++++++++++++ backend/PrintAsmaux.ml | 10 ++++++++++ backend/RTLtyping.v | 6 +++--- backend/ValueAnalysis.v | 4 ++-- cfrontend/C2C.ml | 43 ++++++++++++++++++++++++++++++++++++++++--- cfrontend/Cexec.v | 4 ++-- cfrontend/PrintCsyntax.ml | 4 ++-- common/AST.v | 14 +++++++------- common/Events.v | 4 ++-- common/PrintAST.ml | 4 ++-- common/Sections.ml | 1 + common/Sections.mli | 1 + driver/Configuration.ml | 2 ++ driver/Configuration.mli | 3 +++ exportclight/ExportClight.ml | 4 ++-- powerpc/AsmToJSON.ml | 11 ++++++++--- powerpc/Asmexpand.ml | 8 ++++---- powerpc/Machregs.v | 2 +- powerpc/TargetPrinter.ml | 21 ++++++++++++++++----- riscV/Asmexpand.ml | 8 ++++---- riscV/Machregs.v | 2 +- riscV/TargetPrinter.ml | 14 +++++++++++--- x86/Asmexpand.ml | 8 ++++---- x86/Machregs.v | 2 +- x86/TargetPrinter.ml | 16 +++++++++++++--- 31 files changed, 180 insertions(+), 66 deletions(-) diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 04b4152d..b65007df 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -81,8 +81,8 @@ let expand_int64_arith conflict rl fn = (* Handling of annotations *) -let expand_annot_val txt targ args res = - emit (Pbuiltin (EF_annot(txt,[targ]), args, BR_none)); +let expand_annot_val kind txt targ args res = + emit (Pbuiltin (EF_annot(kind,txt,[targ]), args, BR_none)); match args, res with | [BA(IR src)], BR(IR dst) -> if dst <> src then emit (Pmov (dst,SOreg src)) @@ -453,8 +453,8 @@ let expand_instruction instr = expand_builtin_vload chunk args res | EF_vstore chunk -> expand_builtin_vstore chunk args - | EF_annot_val (txt,targ) -> - expand_annot_val txt targ args res + | EF_annot_val (kind,txt,targ) -> + expand_annot_val kind txt targ args res | EF_memcpy(sz, al) -> expand_builtin_memcpy (Int32.to_int (camlint_of_coqint sz)) (Int32.to_int (camlint_of_coqint al)) args diff --git a/arm/Machregs.v b/arm/Machregs.v index ba3bda7c..ae0ff6bf 100644 --- a/arm/Machregs.v +++ b/arm/Machregs.v @@ -200,7 +200,7 @@ Definition builtin_constraints (ef: external_function) : | EF_vload _ => OK_addressing :: nil | EF_vstore _ => OK_addressing :: OK_default :: nil | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil - | EF_annot txt targs => map (fun _ => OK_all) targs + | EF_annot kind txt targs => map (fun _ => OK_all) targs | EF_debug kind txt targs => map (fun _ => OK_all) targs | _ => nil end. diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index fa612047..67bc5d8b 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -159,6 +159,7 @@ struct | Section_debug_line _ -> ".section .debug_line,\"\",%progbits" | Section_debug_ranges -> ".section .debug_ranges,\"\",%progbits" | Section_debug_str -> ".section .debug_str,\"MS\",%progbits,1" + | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",\"\",%%note" let section oc sec = fprintf oc " %s\n" (name_of_section sec) @@ -722,9 +723,16 @@ struct end | Pbuiltin(ef, args, res) -> begin match ef with - | EF_annot(txt, targs) -> - fprintf oc "%s annotation: %s\n" comment - (annot_text preg_annot "sp" (camlstring_of_coqstring txt) args); + | EF_annot(kind,txt, targs) -> + let annot = + begin match (P.to_int kind) with + | 1 -> annot_text preg_annot "sp" (camlstring_of_coqstring txt) args + | 2 -> let lbl = new_label () in + fprintf oc "%a: " elf_label lbl; + ais_annot_text lbl preg_annot "r1" (camlstring_of_coqstring txt) args + | _ -> assert false + end in + fprintf oc "%s annotation: %S\n" comment annot; 0 | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg_annot "sp" oc diff --git a/backend/CSE.v b/backend/CSE.v index bc3fdba5..6d3f6f33 100644 --- a/backend/CSE.v +++ b/backend/CSE.v @@ -486,7 +486,7 @@ Definition transfer (f: function) (approx: PMap.t VA.t) (pc: node) (before: numb | _ => empty_numbering end - | EF_vload _ | EF_annot _ _ | EF_annot_val _ _ | EF_debug _ _ _ => + | EF_vload _ | EF_annot _ _ _ | EF_annot_val _ _ _ | EF_debug _ _ _ => set_res_unknown before res end | Icond cond args ifso ifnot => diff --git a/backend/Deadcode.v b/backend/Deadcode.v index 9cbe5054..2286876e 100644 --- a/backend/Deadcode.v +++ b/backend/Deadcode.v @@ -102,7 +102,7 @@ Function transfer_builtin (app: VA.t) (ef: external_function) nmem_add (nmem_remove nm (aaddr_arg app dst) sz) (aaddr_arg app src) sz) args else (ne, nm) - | (EF_annot _ _ | EF_annot_val _ _), _ => + | (EF_annot _ _ _ | EF_annot_val _ _ _), _ => transfer_builtin_args (kill_builtin_res res ne, nm) args | EF_debug _ _ _, _ => (kill_builtin_res res ne, nm) diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index ca6ad649..12c05cc3 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -994,7 +994,7 @@ Ltac UseTransfer := erewrite Mem.loadbytes_length in H0 by eauto. rewrite nat_of_Z_eq in H0 by omega. auto. + (* annot *) - destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x1) as (ne1, nm1) eqn:TR. + destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x2) as (ne1, nm1) eqn:TR. InvSoundState. exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). inv H1. @@ -1006,7 +1006,7 @@ Ltac UseTransfer := eapply match_succ_states; eauto. simpl; auto. apply eagree_set_res; auto. + (* annot val *) - destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x1) as (ne1, nm1) eqn:TR. + destruct (transfer_builtin_args (kill_builtin_res res ne, nm) _x2) as (ne1, nm1) eqn:TR. InvSoundState. exploit transfer_builtin_args_sound; eauto. intros (tvl & A & B & C & D). inv H1. inv B. inv H6. diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 0e9eadcb..465b8791 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -108,6 +108,23 @@ module Printer(Target:TARGET) = | Gfun (External ef) -> () | Gvar v -> print_var oc name v + let print_ais_annot oc = + let annots = List.rev !ais_annot_list in + if annots <> [] then begin + Target.section oc Section_ais_annotation; + let annot_part oc lbl = function + | Str.Delim _ -> + fprintf oc " .byte 7,%d\n" (if Archi.ptr64 then 8 else 4) ; + fprintf oc " %s %a\n" Target.address Target.label lbl + | Str.Text a -> fprintf oc " .ascii %S\n" a in + let annot oc (lbl,str) = + List.iter (annot_part oc lbl) str; + fprintf oc " .ascii \"\\n\"\n" + in + List.iter (annot oc) annots + end; + ais_annot_list := [] + module DwarfTarget: DwarfTypes.DWARF_TARGET = struct let label = Target.label @@ -128,6 +145,7 @@ let print_program oc p = Target.print_prologue oc; List.iter (Printer.print_globdef oc) p.prog_defs; Target.print_epilogue oc; + Printer.print_ais_annot oc; if !Clflags.option_g then begin let atom_to_s s = diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index df3445ea..07ab4bed 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -197,6 +197,16 @@ let annot_text preg_string sp_reg_name txt args = sprintf "" s in String.concat "" (List.map fragment (Str.full_split re_annot_param txt)) +let ais_annot_list: (int * Str.split_result list) list ref = ref [] + +let re_annot_addr = Str.regexp "%addr" + +let ais_annot_text lbl preg_string sp_reg_name txt args = + let annot = annot_text preg_string sp_reg_name txt args in + let annots = Str.full_split re_annot_addr annot in + ais_annot_list := (lbl,annots)::!ais_annot_list; + annot + (* Printing of [EF_debug] info. To be completed. *) let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index fef74706..8336d1bf 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -132,7 +132,7 @@ Inductive wt_instr : instruction -> Prop := | wt_Ibuiltin: forall ef args res s, match ef with - | EF_annot _ _ | EF_debug _ _ _ => True + | EF_annot _ _ _ | EF_debug _ _ _ => True | _ => map type_of_builtin_arg args = (ef_sig ef).(sig_args) end -> type_of_builtin_res res = proj_sig_res (ef_sig ef) -> @@ -308,7 +308,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := do x <- check_successor s; do e1 <- match ef with - | EF_annot _ _ | EF_debug _ _ _ => OK e + | EF_annot _ _ _ | EF_debug _ _ _ => OK e | _ => type_builtin_args e args sig.(sig_args) end; type_builtin_res e1 res (proj_sig_res sig) @@ -702,7 +702,7 @@ Proof. exploit type_builtin_res_complete; eauto. instantiate (1 := res). intros [e2 [C D]]. exploit type_builtin_res_complete. eexact H. instantiate (1 := res). intros [e3 [E F]]. rewrite check_successor_complete by auto. simpl. - exists (match ef with EF_annot _ _ | EF_debug _ _ _ => e3 | _ => e2 end); split. + exists (match ef with EF_annot _ _ _ | EF_debug _ _ _ => e3 | _ => e2 end); split. rewrite H1 in C, E. destruct ef; try (rewrite <- H0; rewrite A); simpl; auto. destruct ef; auto. diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v index 8aa4878a..674bc065 100644 --- a/backend/ValueAnalysis.v +++ b/backend/ValueAnalysis.v @@ -99,9 +99,9 @@ Definition transfer_builtin let p := loadbytes am rm (aptr_of_aval asrc) in let am' := storebytes am (aptr_of_aval adst) sz p in VA.State (set_builtin_res res ntop ae) am' - | (EF_annot _ _ | EF_debug _ _ _), _ => + | (EF_annot _ _ _ | EF_debug _ _ _), _ => VA.State (set_builtin_res res ntop ae) am - | EF_annot_val _ _, v :: nil => + | EF_annot_val _ _ _, v :: nil => let av := abuiltin_arg ae am rm v in VA.State (set_builtin_res res av ae) am | _, _ => diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 4dbd6c05..a7ee353a 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -132,9 +132,21 @@ let string_of_errmsg msg = (** ** The builtin environment *) +let ais_annot_functions = + if Configuration.elf_target then + [(* Ais Annotations, only available for ELF targets *) + "__builtin_ais_annot", + (TVoid [], + [TPtr(TInt(IChar, [AConst]), [])], + true);] + else + [] + let builtins_generic = { Builtins.typedefs = []; - Builtins.functions = [ + Builtins.functions = + ais_annot_functions + @[ (* Integer arithmetic *) "__builtin_bswap", (TInt(IUInt, []), [TInt(IUInt, [])], false); @@ -828,7 +840,7 @@ let rec convertExpr env e = | {edesc = C.EConst(CStr txt)} :: args1 -> let targs1 = convertTypArgs env [] args1 in Ebuiltin( - AST.EF_annot(coqstring_of_camlstring txt, typlist_of_typelist targs1), + AST.EF_annot(P.of_int 1,coqstring_of_camlstring txt, typlist_of_typelist targs1), targs1, convertExprList env args1, convertTyp env e.etyp) | _ -> error "argument 1 of '__builtin_annot' must be a string literal"; @@ -840,7 +852,32 @@ let rec convertExpr env e = | [ {edesc = C.EConst(CStr txt)}; arg ] -> let targ = convertTyp env (Cutil.default_argument_conversion env arg.etyp) in - Ebuiltin(AST.EF_annot_val(coqstring_of_camlstring txt, typ_of_type targ), + Ebuiltin(AST.EF_annot_val(P.of_int 1,coqstring_of_camlstring txt, typ_of_type targ), + Tcons(targ, Tnil), convertExprList env [arg], + convertTyp env e.etyp) + | _ -> + error "argument 1 of '__builtin_annot_intval' must be a string literal"; + ezero + end + + | C.ECall({edesc = C.EVar {name = "__builtin_ais_annot"}}, args) when Configuration.elf_target -> + begin match args with + | {edesc = C.EConst(CStr txt)} :: args1 -> + let targs1 = convertTypArgs env [] args1 in + Ebuiltin( + AST.EF_annot(P.of_int 2,coqstring_of_camlstring txt, typlist_of_typelist targs1), + targs1, convertExprList env args1, convertTyp env e.etyp) + | _ -> + error "argument 1 of '__builtin_ais_annot' must be a string literal"; + ezero + end + + | C.ECall({edesc = C.EVar {name = "__builtin_ais_annot_intval"}}, args) when Configuration.elf_target -> + begin match args with + | [ {edesc = C.EConst(CStr txt)}; arg ] -> + let targ = convertTyp env + (Cutil.default_argument_conversion env arg.etyp) in + Ebuiltin(AST.EF_annot_val(P.of_int 2,coqstring_of_camlstring txt, typ_of_type targ), Tcons(targ, Tnil), convertExprList env [arg], convertTyp env e.etyp) | _ -> diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v index 15818317..bea579fc 100644 --- a/cfrontend/Cexec.v +++ b/cfrontend/Cexec.v @@ -512,8 +512,8 @@ Definition do_external (ef: external_function): | EF_malloc => do_ef_malloc | EF_free => do_ef_free | EF_memcpy sz al => do_ef_memcpy sz al - | EF_annot text targs => do_ef_annot text targs - | EF_annot_val text targ => do_ef_annot_val text targ + | EF_annot kind text targs => do_ef_annot text targs + | EF_annot_val kind text targ => do_ef_annot_val text targ | EF_inline_asm text sg clob => do_inline_assembly text sg ge | EF_debug kind text targs => do_ef_debug kind text targs end. diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml index 6366906a..6e016cb3 100644 --- a/cfrontend/PrintCsyntax.ml +++ b/cfrontend/PrintCsyntax.ml @@ -253,10 +253,10 @@ let rec expr p (prec, e) = fprintf p "__builtin_memcpy_aligned@[(%ld,@ %ld,@ %a)@]" (camlint_of_coqint sz) (camlint_of_coqint al) exprlist (true, args) - | Ebuiltin(EF_annot(txt, _), _, args, _) -> + | Ebuiltin(EF_annot(_,txt, _), _, args, _) -> fprintf p "__builtin_annot@[(%S%a)@]" (camlstring_of_coqstring txt) exprlist (false, args) - | Ebuiltin(EF_annot_val(txt, _), _, args, _) -> + | Ebuiltin(EF_annot_val(_,txt, _), _, args, _) -> fprintf p "__builtin_annot_intval@[(%S%a)@]" (camlstring_of_coqstring txt) exprlist (false, args) | Ebuiltin(EF_external(id, sg), _, args, _) -> diff --git a/common/AST.v b/common/AST.v index a072ef29..145f4919 100644 --- a/common/AST.v +++ b/common/AST.v @@ -451,11 +451,11 @@ 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: string) (targs: list typ) + | EF_annot (kind: positive) (text: string) (targs: list typ) (** 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. *) - | EF_annot_val (text: string) (targ: typ) + | EF_annot_val (kind: positive) (text: string) (targ: typ) (** 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. *) @@ -482,8 +482,8 @@ Definition ef_sig (ef: external_function): signature := | EF_malloc => mksignature (Tptr :: nil) (Some Tptr) cc_default | EF_free => mksignature (Tptr :: nil) None cc_default | EF_memcpy sz al => mksignature (Tptr :: Tptr :: nil) None cc_default - | EF_annot text targs => mksignature targs None cc_default - | EF_annot_val text targ => mksignature (targ :: nil) (Some targ) cc_default + | EF_annot kind text targs => mksignature targs None cc_default + | EF_annot_val kind text targ => mksignature (targ :: nil) (Some targ) cc_default | EF_inline_asm text sg clob => sg | EF_debug kind text targs => mksignature targs None cc_default end. @@ -500,8 +500,8 @@ Definition ef_inline (ef: external_function) : bool := | EF_malloc => false | EF_free => false | EF_memcpy sz al => true - | EF_annot text targs => true - | EF_annot_val text targ => true + | EF_annot kind text targs => true + | EF_annot_val kind Text rg => true | EF_inline_asm text sg clob => true | EF_debug kind text targs => true end. @@ -510,7 +510,7 @@ Definition ef_inline (ef: external_function) : bool := Definition ef_reloads (ef: external_function) : bool := match ef with - | EF_annot text targs => false + | EF_annot kind text targs => false | EF_debug kind text targs => false | _ => true end. diff --git a/common/Events.v b/common/Events.v index 63922bc5..b2335b96 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1419,8 +1419,8 @@ Definition external_call (ef: external_function): extcall_sem := | EF_malloc => extcall_malloc_sem | EF_free => extcall_free_sem | EF_memcpy sz al => extcall_memcpy_sem sz al - | EF_annot txt targs => extcall_annot_sem txt targs - | EF_annot_val txt targ => extcall_annot_val_sem txt targ + | EF_annot kind txt targs => extcall_annot_sem txt targs + | EF_annot_val kind txt targ => extcall_annot_val_sem txt targ | EF_inline_asm txt sg clb => inline_assembly_sem txt sg | EF_debug kind txt targs => extcall_debug_sem end. diff --git a/common/PrintAST.ml b/common/PrintAST.ml index ac7d2276..883d101a 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -46,8 +46,8 @@ let name_of_external = function | EF_free -> "free" | EF_memcpy(sz, al) -> sprintf "memcpy size %s align %s " (Z.to_string sz) (Z.to_string al) - | EF_annot(text, targs) -> sprintf "annot %S" (camlstring_of_coqstring text) - | EF_annot_val(text, targ) -> sprintf "annot_val %S" (camlstring_of_coqstring text) + | EF_annot(kind,text, targs) -> sprintf "annot %S" (camlstring_of_coqstring text) + | EF_annot_val(kind,text, targ) -> sprintf "annot_val %S" (camlstring_of_coqstring text) | EF_inline_asm(text, sg, clob) -> sprintf "inline_asm %S" (camlstring_of_coqstring text) | EF_debug(kind, text, targs) -> sprintf "debug%d %S" (P.to_int kind) (extern_atom text) diff --git a/common/Sections.ml b/common/Sections.ml index 1c2e8291..30be9e69 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -31,6 +31,7 @@ type section_name = | Section_debug_line of string option | Section_debug_ranges | Section_debug_str + | Section_ais_annotation type access_mode = | Access_default diff --git a/common/Sections.mli b/common/Sections.mli index b83b0bb4..bc97814d 100644 --- a/common/Sections.mli +++ b/common/Sections.mli @@ -32,6 +32,7 @@ type section_name = | Section_debug_line of string option | Section_debug_ranges | Section_debug_str + | Section_ais_annotation type access_mode = | Access_default diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 58583330..48f8abde 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -184,3 +184,5 @@ let response_file_style = | v -> bad_config "response_file_style" [v] let gnu_toolchain = system <> "diab" + +let elf_target = system <> "macosx" && system <> "cygwin" diff --git a/driver/Configuration.mli b/driver/Configuration.mli index f0bb8f83..b918c169 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -77,3 +77,6 @@ val response_file_style: response_file_style val gnu_toolchain: bool (** Does the targeted system use the gnu toolchain *) + +val elf_target: bool + (** Is the target binary format ELF? *) diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 16aac9ab..f5b8150d 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -250,10 +250,10 @@ let external_function p = function | EF_free -> fprintf p "EF_free" | EF_memcpy(sz, al) -> fprintf p "(EF_memcpy %ld %ld)" (Z.to_int32 sz) (Z.to_int32 al) - | EF_annot(text, targs) -> + | EF_annot(kind,text, targs) -> assertions := (camlstring_of_coqstring text, targs) :: !assertions; fprintf p "(EF_annot %a %a)" coqstring text (print_list asttype) targs - | EF_annot_val(text, targ) -> + | EF_annot_val(kind,text, targ) -> assertions := (camlstring_of_coqstring text, [targ]) :: !assertions; fprintf p "(EF_annot_val %a %a)" coqstring text asttype targ | EF_debug(kind, text, targs) -> diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml index b542d7a7..a3e57e51 100644 --- a/powerpc/AsmToJSON.ml +++ b/powerpc/AsmToJSON.ml @@ -367,7 +367,7 @@ let pp_instructions pp ic = | EF_inline_asm _ -> instruction pp "Pinlineasm" [Id]; Cerrors.warning ("",-10) Cerrors.Inline_asm_sdump "inline assembler is not supported in sdump" - | EF_annot (txt,targs) -> + | EF_annot (kind,txt,targs) -> let annot_string = PrintAsmaux.annot_text preg_annot "r1" (camlstring_of_coqstring txt) args in let len = String.length annot_string in let buf = Buffer.create len in @@ -376,7 +376,11 @@ let pp_instructions pp ic = | _ -> () end; Buffer.add_char buf c) annot_string; let annot_string = Buffer.contents buf in - instruction pp "Pannot" [String annot_string] + let kind = match P.to_int kind with + | 1 -> "normal" + | 2 -> "ais" + | _ -> assert false in + instruction pp "Pannot" [String kind;String annot_string] | EF_annot_val _ | EF_builtin _ | EF_debug _ @@ -423,7 +427,8 @@ let pp_section pp sec = | Section_debug_line _ | Section_debug_loc | Section_debug_ranges - | Section_debug_str -> () (* There should be no info in the debug sections *) + | Section_debug_str + | Section_ais_annotation -> () (* There should be no info in the debug sections *) let pp_int_opt pp = function | None -> fprintf pp "0" diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index deab7703..96b11056 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -58,8 +58,8 @@ let emit_addimm rd rs n = (* Handling of annotations *) -let expand_annot_val txt targ args res = - emit (Pbuiltin(EF_annot(txt, [targ]), args, BR_none)); +let expand_annot_val kind txt targ args res = + emit (Pbuiltin(EF_annot(kind,txt, [targ]), args, BR_none)); begin match args, res with | [BA(IR src)], BR(IR dst) -> if dst <> src then emit (Pmr(dst, src)) @@ -869,8 +869,8 @@ let expand_instruction instr = expand_builtin_vstore chunk 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_annot_val(kind,txt, targ) -> + expand_annot_val kind txt targ args res | EF_annot _ | EF_debug _ | EF_inline_asm _ -> emit instr | _ -> diff --git a/powerpc/Machregs.v b/powerpc/Machregs.v index 8442bb52..53d99e2f 100644 --- a/powerpc/Machregs.v +++ b/powerpc/Machregs.v @@ -279,7 +279,7 @@ Definition builtin_constraints (ef: external_function) : | EF_vload _ => OK_addressing :: nil | EF_vstore _ => OK_addressing :: OK_default :: nil | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil - | EF_annot txt targs => map (fun _ => OK_all) targs + | EF_annot kind txt targs => map (fun _ => OK_all) targs | EF_debug kind txt targs => map (fun _ => OK_all) targs | _ => nil end. diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index bff2a7fa..9c07b086 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -136,6 +136,7 @@ module Linux_System : SYSTEM = | Section_debug_line _ -> ".section .debug_line,\"\",@progbits" | Section_debug_ranges -> ".section .debug_ranges,\"\",@progbits" | Section_debug_str -> ".section .debug_str,\"MS\",@progbits,1" + | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",\"\",@note" let section oc sec = @@ -234,6 +235,7 @@ module Diab_System : SYSTEM = sprintf ".section .debug_line,,n\n" | Section_debug_ranges | Section_debug_str -> assert false (* Should not be used *) + | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",,n" let section oc sec = let name = name_of_section sec in @@ -832,10 +834,17 @@ module Target (System : SYSTEM):TARGET = fprintf oc " .balign %d\n" !Clflags.option_falignbranchtargets; fprintf oc "%a:\n" label (transl_label lbl) | Pbuiltin(ef, args, res) -> - begin match ef with - | EF_annot(txt, targs) -> - fprintf oc "%s annotation: %s\n" comment - (annot_text preg_annot "r1" (camlstring_of_coqstring txt) args) + begin match ef with + | EF_annot(kind,txt, targs) -> + let annot = + begin match (P.to_int kind) with + | 1 -> annot_text preg_annot "sp" (camlstring_of_coqstring txt) args + | 2 -> let lbl = new_label () in + fprintf oc "%a: " label lbl; + ais_annot_text lbl preg_annot "r1" (camlstring_of_coqstring txt) args + | _ -> assert false + end in + fprintf oc "%s annotation: %S\n" comment annot | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg_annot "r1" oc (P.to_int kind) (extern_atom txt) args @@ -990,7 +999,9 @@ module Target (System : SYSTEM):TARGET = let section oc sec = section oc sec; - debug_section oc sec + match sec with + | Section_ais_annotation -> () + | _ -> debug_section oc sec end let sel_target () = diff --git a/riscV/Asmexpand.ml b/riscV/Asmexpand.ml index d42f4d13..945974e0 100644 --- a/riscV/Asmexpand.ml +++ b/riscV/Asmexpand.ml @@ -104,8 +104,8 @@ let fixup_call sg = (* Handling of annotations *) -let expand_annot_val txt targ args res = - emit (Pbuiltin (EF_annot(txt,[targ]), args, BR_none)); +let expand_annot_val kind txt targ args res = + emit (Pbuiltin (EF_annot(kind,txt,[targ]), args, BR_none)); match args, res with | [BA(IR src)], BR(IR dst) -> if dst <> src then emit (Pmv (dst, src)) @@ -556,8 +556,8 @@ let expand_instruction instr = expand_builtin_vload chunk args res | EF_vstore chunk -> expand_builtin_vstore chunk args - | EF_annot_val (txt,targ) -> - expand_annot_val txt targ args res + | EF_annot_val (kind,txt,targ) -> + expand_annot_val kind txt targ args res | EF_memcpy(sz, al) -> expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args | EF_annot _ | EF_debug _ | EF_inline_asm _ -> diff --git a/riscV/Machregs.v b/riscV/Machregs.v index c21ea97a..d8bb4a4b 100644 --- a/riscV/Machregs.v +++ b/riscV/Machregs.v @@ -247,7 +247,7 @@ Definition builtin_constraints (ef: external_function) : | EF_vload _ => OK_addressing :: nil | EF_vstore _ => OK_addressing :: OK_default :: nil | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil - | EF_annot txt targs => map (fun _ => OK_all) targs + | EF_annot kind txt targs => map (fun _ => OK_all) targs | EF_debug kind txt targs => map (fun _ => OK_all) targs | _ => nil end. diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 65339d35..b363b2b7 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -122,6 +122,7 @@ module Target : TARGET = | Section_user(s, wr, ex) -> sprintf ".section \"%s\",\"a%s%s\",%%progbits" s (if wr then "w" else "") (if ex then "x" else "") + | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",\"\",@note" let section oc sec = fprintf oc " %s\n" (name_of_section sec) @@ -589,9 +590,16 @@ module Target : TARGET = fprintf oc "%s end pseudoinstr btbl\n" comment | Pbuiltin(ef, args, res) -> begin match ef with - | EF_annot(txt, targs) -> - fprintf oc "%s annotation: %s\n" comment - (annot_text preg_annot "sp" (camlstring_of_coqstring txt) args) + | EF_annot(kind,txt, targs) -> + let annot = + begin match (P.to_int kind) with + | 1 -> annot_text preg_annot "sp" (camlstring_of_coqstring txt) args + | 2 -> let lbl = new_label () in + fprintf oc "%a: " label lbl; + ais_annot_text lbl preg_annot "r1" (camlstring_of_coqstring txt) args + | _ -> assert false + end in + fprintf oc "%s annotation: %S\n" comment annot | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg_annot "sp" oc (P.to_int kind) (extern_atom txt) args diff --git a/x86/Asmexpand.ml b/x86/Asmexpand.ml index 1b716165..9927d2fb 100644 --- a/x86/Asmexpand.ml +++ b/x86/Asmexpand.ml @@ -81,8 +81,8 @@ let sp_adjustment_64 sz = (* Handling of annotations *) -let expand_annot_val txt targ args res = - emit (Pbuiltin (EF_annot(txt,[targ]), args, BR_none)); +let expand_annot_val kind txt targ args res = + emit (Pbuiltin (EF_annot(kind,txt,[targ]), args, BR_none)); match args, res with | [BA(IR src)], BR(IR dst) -> if dst <> src then emit (Pmov_rr (dst,src)) @@ -537,8 +537,8 @@ let expand_instruction instr = expand_builtin_vstore chunk 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_annot_val(kind,txt, targ) -> + expand_annot_val kind txt targ args res | EF_annot _ | EF_debug _ | EF_inline_asm _ -> emit instr | _ -> diff --git a/x86/Machregs.v b/x86/Machregs.v index 5d1b4515..bdf492ed 100644 --- a/x86/Machregs.v +++ b/x86/Machregs.v @@ -361,7 +361,7 @@ Definition builtin_constraints (ef: external_function) : | EF_vload _ => OK_addressing :: nil | EF_vstore _ => OK_addressing :: OK_default :: nil | EF_memcpy _ _ => OK_addrstack :: OK_addrstack :: nil - | EF_annot txt targs => map (fun _ => OK_all) targs + | EF_annot kind txt targs => map (fun _ => OK_all) targs | EF_debug kind txt targs => map (fun _ => OK_all) targs | _ => nil end. diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index d55618db..c19359fa 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -131,6 +131,7 @@ module ELF_System : SYSTEM = | Section_debug_abbrev -> ".section .debug_abbrev,\"\",@progbits" | Section_debug_ranges -> ".section .debug_ranges,\"\",@progbits" | Section_debug_str -> ".section .debug_str,\"MS\",@progbits,1" + | Section_ais_annotation -> sprintf ".section \"__compcert_ais_annotations\",\"\",@note" let stack_alignment = 16 @@ -189,6 +190,7 @@ module MacOS_System : SYSTEM = | Section_debug_str -> ".section __DWARF,__debug_str,regular,debug" | Section_debug_ranges -> ".section __DWARF,__debug_ranges,regular,debug" | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" + | Section_ais_annotation -> assert false (* Not supported under MacOS *) let stack_alignment = 16 (* mandatory *) @@ -264,6 +266,7 @@ module Cygwin_System : SYSTEM = | Section_debug_abbrev -> ".section .debug_abbrev,\"dr\"" | Section_debug_ranges -> ".section .debug_ranges,\"dr\"" | Section_debug_str-> assert false (* Should not be used *) + | Section_ais_annotation -> assert false (* Not supported for coff binaries *) let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) @@ -796,9 +799,16 @@ module Target(System: SYSTEM):TARGET = assert false | Pbuiltin(ef, args, res) -> begin match ef with - | EF_annot(txt, targs) -> - fprintf oc "%s annotation: %s\n" comment - (annot_text preg_annot "%esp" (camlstring_of_coqstring txt) args) + | EF_annot(kind,txt, targs) -> + let annot = + begin match (P.to_int kind) with + | 1 -> annot_text preg_annot "sp" (camlstring_of_coqstring txt) args + | 2 -> let lbl = new_label () in + fprintf oc "%a: " label lbl; + ais_annot_text lbl preg_annot "r1" (camlstring_of_coqstring txt) args + | _ -> assert false + end in + fprintf oc "%s annotation: %S\n" comment annot | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg_annot "%esp" oc (P.to_int kind) (extern_atom txt) args -- cgit