diff options
-rw-r--r-- | arm/TargetPrinter.ml | 11 | ||||
-rw-r--r-- | backend/AisAnnot.ml | 159 | ||||
-rw-r--r-- | backend/AisAnnot.mli | 31 | ||||
-rw-r--r-- | backend/PrintAsm.ml | 24 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 12 | ||||
-rw-r--r-- | cfrontend/C2C.ml | 59 | ||||
-rw-r--r-- | cparser/Cutil.ml | 10 | ||||
-rw-r--r-- | cparser/Cutil.mli | 4 | ||||
-rw-r--r-- | cparser/Diagnostics.ml | 8 | ||||
-rw-r--r-- | cparser/Diagnostics.mli | 1 | ||||
-rw-r--r-- | cparser/Parse.ml | 2 | ||||
-rw-r--r-- | cparser/Rename.ml | 2 | ||||
-rw-r--r-- | powerpc/TargetPrinter.ml | 19 | ||||
-rw-r--r-- | riscV/TargetPrinter.ml | 10 | ||||
-rw-r--r-- | x86/TargetPrinter.ml | 10 |
15 files changed, 289 insertions, 73 deletions
diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 56619cdd..9c1e296b 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -15,6 +15,7 @@ open Printf open Camlcoq open Sections +open AisAnnot open AST open Asm open PrintAsmaux @@ -459,15 +460,15 @@ struct | Pbuiltin(ef, args, res) -> 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 + | 1 -> let annot = annot_text preg_annot "sp" (camlstring_of_coqstring txt) args in + fprintf oc "%s annotation: %S\n" comment annot | 2 -> let lbl = new_label () in fprintf oc "%a: " label lbl; - ais_annot_text lbl preg_annot "sp" (camlstring_of_coqstring txt) args + add_ais_annot lbl preg_annot "sp" (camlstring_of_coqstring txt) args | _ -> assert false - end in - fprintf oc "%s annotation: %S\n" comment annot + end; + 0 | 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/backend/AisAnnot.ml b/backend/AisAnnot.ml new file mode 100644 index 00000000..f4dab4c9 --- /dev/null +++ b/backend/AisAnnot.ml @@ -0,0 +1,159 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +open AST +open Camlcoq +open Diagnostics +open Memdata +open Printf + +type t = + | Label of int + | String of string + | Symbol of ident + +let offset ofs = + let ofs = camlint_of_coqint ofs in + if ofs = 0l then "" else sprintf " + %ld" ofs + +let size_chunk c = + sprintf "%ld" (camlint_of_coqint (size_chunk c)) + +let addr_global id ofs = + let addr_o = "(" + and addr_e = sprintf "%s)" (offset ofs) in + [String addr_o;Symbol id;String addr_e] + +exception Bad_parameter of string +exception Unknown_parameter of string +exception Unknown_type of char + +let ais_expr_arg lval preg_string sp_reg_name arg = + let preg reg = sprintf "reg(\"%s\")" (preg_string reg) + and sp = sprintf "reg(\"%s\")" sp_reg_name + and simple s = [String s] + and lval ty = + if lval then + let msg = sprintf "expected register or memory cell but found %s" ty in + raise (Bad_parameter msg) + in + let rec ais_arg = function + | BA x -> simple (preg x) + | BA_int n -> lval "constant"; simple (sprintf "%ld" (camlint_of_coqint n)) + | BA_long n ->lval "constant"; simple (sprintf "%Ld" (camlint64_of_coqint n)) + | BA_float _ + | BA_single _ -> assert false (* Should never occur and be avoided in C2C *) + | BA_loadstack(chunk, ofs) -> + let loadstack = sprintf "mem(%s%s, %s)" sp + (offset ofs) + (size_chunk chunk) in + simple loadstack + | BA_addrstack ofs -> + lval "stack cell"; + let addrstack = sprintf "(%s%s)" sp (offset ofs) in + simple addrstack + | BA_loadglobal(chunk, id, ofs) -> + let mem_o = "mem(" + and mem_e = sprintf "%s, %s)" + (offset ofs) + (size_chunk chunk) in + [String mem_o;Symbol id;String mem_e] + | BA_addrglobal(id, ofs) -> + lval "global address"; + addr_global id ofs + | BA_splitlong(hi, lo) -> + combine " * 0x100000000 + " hi lo + | BA_addptr(a1, a2) -> + combine " + " a1 a2 + and combine mid arg1 arg2 = + lval "pointer computation"; + let op_br = simple "(" + and mid = simple mid + and cl_br = simple ")" + and arg1 = ais_arg arg1 + and arg2 = ais_arg arg2 in + op_br@arg1@mid@arg2@cl_br in + ais_arg arg + +let ais_annot_list: (t list) list ref = ref [] + +let get_ais_annots () = + let annots = !ais_annot_list in + ais_annot_list := []; + List.rev annots + +let re_loc_param = Str.regexp "# file:\\([^ ]+\\) line:\\([^ ]+\\)" + +let loc_of_txt txt = + try + let pos = String.index txt '\n' in + let txt = String.sub txt 0 (pos -1) in + if Str.string_partial_match re_loc_param txt 0 then + let file = Str.matched_group 1 txt + and line = int_of_string (Str.matched_group 2 txt) in + file,line + else + no_loc + with _ -> + no_loc + +let re_ais_annot_param = Str.regexp "%%\\|%[aelp][1-9][0-9]*\\|%here\\|\007" + +let add_ais_annot lbl preg_string sp_reg_name txt args = + let fragment = function + | Str.Delim "%here" -> + [Label lbl] + | Str.Text s -> + [String s] + | Str.Delim "%%" -> + [String "%"] + | Str.Delim "\007" -> + [String "\007\000"] + | Str.Delim s -> + let typ = String.get s 1 + and n = int_of_string (String.sub s 2 (String.length s - 2)) in + let arg = try + List.nth args (n-1) + with _ -> + raise (Unknown_parameter s) in + begin match typ with + | 'e' -> ais_expr_arg false preg_string sp_reg_name arg + | 'l' -> ais_expr_arg true preg_string sp_reg_name arg + | _ -> raise (Unknown_type typ) + end + in + let loc = loc_of_txt txt in + let warn t s = + warning loc Wrong_ais_parameter "%s %s" t s; [] + in + let annot = + try + List.concat (List.map fragment (Str.full_split re_ais_annot_param txt)) + with + | Bad_parameter s -> + warn "wrong ais parameter" s + | Unknown_parameter s -> + warn "unknown parameter" s + | Unknown_type c -> + warn "unknown format argument" (String.make 1 c) + in + let rec merge acc = function + | [] -> List.rev acc + | (Label _ as lbl):: rest -> merge (lbl::acc) rest + | (Symbol _ as sym) :: rest -> merge (sym::acc) rest + | String s1 :: String s2 :: rest -> + merge acc (String (s1 ^ s2) :: rest) + | String s:: rest -> merge ((String s)::acc) rest + in + let annot = merge [] annot in + if annot <> [] then + ais_annot_list := (annot)::!ais_annot_list diff --git a/backend/AisAnnot.mli b/backend/AisAnnot.mli new file mode 100644 index 00000000..7219369c --- /dev/null +++ b/backend/AisAnnot.mli @@ -0,0 +1,31 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +type t = + | Label of int (** label argument, used for current location*) + | String of string (** text part of the ais annotation *) + | Symbol of AST.ident (** symbol argument, used in variable and function addresses *) + +val add_ais_annot : int -> ('a -> string) -> string -> string -> 'a AST.builtin_arg list -> unit +(** [add_ais_annot lbl preg spreg txt args] adds the ais annotation [txt] were the format + specifiers are replace according to their type: + -a: area definitions + -e: general expressions + -l: l-value expressions + -p: program location + -here: the address of the ais annotation [lbl] + and [preg] is used to get the names of the registers, as well as [spreg] the name of the + stack pointer and [args] the arguments reference in the replacements +*) + +val get_ais_annots: unit -> (t list) list +(** [get_ais_annots ()] return the list of all ais annotations and reset it *) diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 44c6b409..04ecbae3 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -18,6 +18,7 @@ open PrintAsmaux open Printf open Sections open TargetPrinter +open AisAnnot module Printer(Target:TARGET) = struct @@ -148,21 +149,24 @@ module Printer(Target:TARGET) = | Gvar v -> print_var oc name v let print_ais_annot oc = - let annots = List.rev !ais_annot_list in + let annots = get_ais_annots () 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; + let print_addr oc pp_addr addr = + fprintf oc " .byte 7,%d\n" (if Archi.ptr64 then 8 else 4); + fprintf oc " %s %a\n" Target.address pp_addr addr in + let annot_part oc = function + | AisAnnot.Label lbl -> + print_addr oc Target.label lbl + | AisAnnot.Symbol symb -> + print_addr oc Target.symbol symb + | AisAnnot.String a -> fprintf oc " .ascii %S\n" a in + let annot oc str = + List.iter (annot_part oc) str; fprintf oc " .ascii \"\\n\"\n" in List.iter (annot oc) annots - end; - ais_annot_list := [] + end module DwarfTarget: DwarfTypes.DWARF_TARGET = struct diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index d985d5a4..f9ed569f 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -212,18 +212,6 @@ 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 re_annot_quote = Str.regexp "\007" - -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 annot = Str.global_replace re_annot_quote "\007\000" annot 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/cfrontend/C2C.ml b/cfrontend/C2C.ml index b8134599..c18a6e03 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -119,6 +119,10 @@ let currentLocation = ref Cutil.no_loc let updateLoc l = currentLocation := l +let currentFunction = ref "" + +let updateFunction f = currentFunction := f + let error fmt = Diagnostics.error !currentLocation fmt @@ -140,21 +144,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 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 = - (* ais_annot_functions - * @ *) + ais_annot_functions + @ [ (* Integer arithmetic *) "__builtin_bswap", @@ -871,19 +875,25 @@ let rec convertExpr env e = 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 file,line = !currentLocation in - * let loc_string = Printf.sprintf "# file %s, line %d\n" file line in - * let targs1 = convertTypArgs env [] args1 in - * Ebuiltin( - * AST.EF_annot(P.of_int 2,coqstring_of_camlstring (loc_string ^ 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"}}, args) when Configuration.elf_target -> + begin match args with + | {edesc = C.EConst(CStr txt)} :: args1 -> + let file,line = !currentLocation in + let fun_name = !currentFunction in + let loc_string = Printf.sprintf "# file:%s line:%d function:%s\n" file line fun_name in + let targs1 = convertTypArgs env [] args1 in + List.iter (fun exp -> if Cutil.is_float_type env exp.etyp then begin + error "floating point types are not supported in ais annotations" + end else if Cutil.is_volatile_variable env exp then begin + error "access to volatile variables are not supported in ais annotations" + end) args1; + Ebuiltin( + AST.EF_annot(P.of_int 2,coqstring_of_camlstring (loc_string ^ 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_memcpy_aligned"}}, args) -> make_builtin_memcpy (convertExprList env args) @@ -1135,6 +1145,7 @@ and convertSwitch env is_64 = function let convertFundef loc env fd = checkFunctionType env fd.fd_ret (Some fd.fd_params); + updateFunction fd.fd_name.name; if fd.fd_vararg && not !Clflags.option_fvararg_calls then unsupported "variable-argument function (consider adding option [-fvararg-calls])"; let ret = diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 71c253f8..30037049 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -707,6 +707,11 @@ let is_integer_type env t = | TEnum(_, _) -> true | _ -> false +let is_float_type env t = + match unroll env t with + | TFloat (_, _) -> true + | _ -> false + let is_arith_type env t = match unroll env t with | TInt(_, _) -> true @@ -1207,3 +1212,8 @@ let rec subst_stmt phi s = List.map subst_asm_operand inputs, clob) } + +let is_volatile_variable env exp = + match exp.edesc with + | EVar x -> List.mem AVolatile (attributes_of_type env exp.etyp) + | _ -> false diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 79975dcf..87a69f12 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -141,6 +141,8 @@ val is_void_type : Env.t -> typ -> bool (* Is type [void]? *) val is_integer_type : Env.t -> typ -> bool (* Is type integer? *) +val is_float_type : Env.t -> typ -> bool + (* Is type float *) val is_arith_type : Env.t -> typ -> bool (* Is type integer or float? *) val is_pointer_type : Env.t -> typ -> bool @@ -239,6 +241,8 @@ val field_of_arrow_access: Env.t -> typ -> string -> field (* Return the field info for a [x->field] access *) val valid_array_size: Env.t -> typ -> int64 -> bool (* Test whether the array size fits in half of the address space *) +val is_volatile_variable: Env.t -> exp -> bool + (* Test whether the expression is an access to a volatile variable *) (* Constructors *) diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml index fbdc9297..e3258a38 100644 --- a/cparser/Diagnostics.ml +++ b/cparser/Diagnostics.ml @@ -90,6 +90,7 @@ type warning_type = | Inline_asm_sdump | Unused_variable | Unused_parameter + | Wrong_ais_parameter (* List of active warnings *) let active_warnings: warning_type list ref = ref [ @@ -110,6 +111,7 @@ let active_warnings: warning_type list ref = ref [ Return_type; Literal_range; Inline_asm_sdump; + Wrong_ais_parameter; ] (* List of errors treated as warning *) @@ -139,6 +141,7 @@ let string_of_warning = function | Inline_asm_sdump -> "inline-asm-sdump" | Unused_variable -> "unused-variable" | Unused_parameter -> "unused-parameter" + | Wrong_ais_parameter -> "wrong-ais-parameter" (* Activate the given warning *) let activate_warning w () = @@ -184,7 +187,8 @@ let wall () = CompCert_conformance; Inline_asm_sdump; Unused_variable; - Unused_parameter + Unused_parameter; + Wrong_ais_parameter; ] let wnothing () = @@ -214,6 +218,7 @@ let werror () = CompCert_conformance; Inline_asm_sdump; Unused_variable; + Wrong_ais_parameter; ] (* Generate the warning key for the message *) @@ -390,6 +395,7 @@ let warning_options = error_option Inline_asm_sdump @ error_option Unused_variable @ error_option Unused_parameter @ + error_option Wrong_ais_parameter @ [Exact ("-Wfatal-errors"), Set error_fatal; Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *) Exact ("-fno-diagnostics-color"), Unset color_diagnostics; diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli index 82edd9fa..648d537b 100644 --- a/cparser/Diagnostics.mli +++ b/cparser/Diagnostics.mli @@ -47,6 +47,7 @@ type warning_type = | Inline_asm_sdump (** inline assembler used in combination of sdump *) | Unused_variable (** unused local variables *) | Unused_parameter (** unused function parameter *) + | Wrong_ais_parameter (** wrong parameter type for ais replacement *) val warning : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a (** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to diff --git a/cparser/Parse.ml b/cparser/Parse.ml index 8143954b..b2c83698 100644 --- a/cparser/Parse.ml +++ b/cparser/Parse.ml @@ -69,7 +69,7 @@ let preprocessed_file transfs name sourcefile = | Parser.Parser.Inter.Fail_pr -> (* Theoretically impossible : implies inconsistencies between grammars. *) - Diagnostics.fatal_error Diagnostics.no_loc "Internal error while parsing" + Diagnostics.fatal_error Diagnostics.no_loc "Internal error while parsing" | Parser.Parser.Inter.Timeout_pr -> assert false | Parser.Parser.Inter.Parsed_pr (ast, _ ) -> ast) in let p1 = Timing.time "Elaboration" Elab.elab_file ast in diff --git a/cparser/Rename.ml b/cparser/Rename.ml index cdb5751e..d63fa47d 100644 --- a/cparser/Rename.ml +++ b/cparser/Rename.ml @@ -84,7 +84,7 @@ let ident env id = IdentMap.find id env.re_id with Not_found -> Diagnostics.fatal_error Diagnostics.no_loc "internal error: rename: %s__%d unbound" - id.name id.stamp + id.name id.stamp let rec typ env = function | TPtr(ty, a) -> TPtr(typ env ty, a) diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index 01851ac2..9a6840b1 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -20,6 +20,7 @@ open Sections open AST open Asm open PrintAsmaux +open AisAnnot (* Recognition of target ABI and asm syntax *) @@ -834,15 +835,15 @@ module Target (System : SYSTEM):TARGET = | Pbuiltin(ef, args, res) -> 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 + begin match (P.to_int kind) with + | 1 -> let annot = annot_text preg_annot "sp" (camlstring_of_coqstring txt) args in + fprintf oc "%s annotation: %S\n" comment annot + + | 2 -> let lbl = new_label () in + fprintf oc "%a: " label lbl; + add_ais_annot lbl preg_annot "r1" (camlstring_of_coqstring txt) args + | _ -> assert false + end | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg_annot "r1" oc (P.to_int kind) (extern_atom txt) args diff --git a/riscV/TargetPrinter.ml b/riscV/TargetPrinter.ml index 696bc87f..381f4397 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -22,6 +22,7 @@ open Camlcoq open Sections open AST open Asm +open AisAnnot open PrintAsmaux open Fileinfo @@ -566,15 +567,14 @@ module Target : TARGET = | Pbuiltin(ef, args, res) -> 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 + | 1 -> let annot = annot_text preg_annot "sp" (camlstring_of_coqstring txt) args in + fprintf oc "%s annotation: %S\n" comment annot | 2 -> let lbl = new_label () in fprintf oc "%a: " label lbl; - ais_annot_text lbl preg_annot "r1" (camlstring_of_coqstring txt) args + add_ais_annot lbl preg_annot "r1" (camlstring_of_coqstring txt) args | _ -> assert false - end in - fprintf oc "%s annotation: %S\n" comment annot + end | 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/TargetPrinter.ml b/x86/TargetPrinter.ml index 3171847c..12ef6472 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -17,6 +17,7 @@ open Camlcoq open Sections open AST open Asm +open AisAnnot open PrintAsmaux open Fileinfo @@ -792,15 +793,14 @@ module Target(System: SYSTEM):TARGET = | Pbuiltin(ef, args, res) -> 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 + | 1 -> let annot = annot_text preg_annot "sp" (camlstring_of_coqstring txt) args in + fprintf oc "%s annotation: %S\n" comment annot | 2 -> let lbl = new_label () in fprintf oc "%a: " label lbl; - ais_annot_text lbl preg_annot "r1" (camlstring_of_coqstring txt) args + add_ais_annot lbl preg_annot "r1" (camlstring_of_coqstring txt) args | _ -> assert false - end in - fprintf oc "%s annotation: %S\n" comment annot + end | EF_debug(kind, txt, targs) -> print_debug_info comment print_file_line preg_annot "%esp" oc (P.to_int kind) (extern_atom txt) args |