diff options
Diffstat (limited to 'backend')
| -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 |
4 files changed, 204 insertions, 22 deletions
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]*\\)$" |