aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/Asmexpand.ml8
-rw-r--r--arm/Machregs.v2
-rw-r--r--arm/TargetPrinter.ml14
-rw-r--r--backend/CSE.v2
-rw-r--r--backend/Deadcode.v2
-rw-r--r--backend/Deadcodeproof.v4
-rw-r--r--backend/PrintAsm.ml18
-rw-r--r--backend/PrintAsmaux.ml10
-rw-r--r--backend/RTLtyping.v6
-rw-r--r--backend/ValueAnalysis.v4
-rw-r--r--cfrontend/C2C.ml43
-rw-r--r--cfrontend/Cexec.v4
-rw-r--r--cfrontend/PrintCsyntax.ml4
-rw-r--r--common/AST.v14
-rw-r--r--common/Events.v4
-rw-r--r--common/PrintAST.ml4
-rw-r--r--common/Sections.ml1
-rw-r--r--common/Sections.mli1
-rw-r--r--driver/Configuration.ml2
-rw-r--r--driver/Configuration.mli3
-rw-r--r--exportclight/ExportClight.ml4
-rw-r--r--powerpc/AsmToJSON.ml11
-rw-r--r--powerpc/Asmexpand.ml8
-rw-r--r--powerpc/Machregs.v2
-rw-r--r--powerpc/TargetPrinter.ml21
-rw-r--r--riscV/Asmexpand.ml8
-rw-r--r--riscV/Machregs.v2
-rw-r--r--riscV/TargetPrinter.ml14
-rw-r--r--x86/Asmexpand.ml8
-rw-r--r--x86/Machregs.v2
-rw-r--r--x86/TargetPrinter.ml16
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 "<bad parameter %s>" 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@[<hov 1>(%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@[<hov 1>(%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@[<hov 1>(%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
generated by cgit (git 2.34.1) at 2024-05-20 09:21:27 +0000