diff options
Diffstat (limited to 'backend/AisAnnot.ml')
-rw-r--r-- | backend/AisAnnot.ml | 159 |
1 files changed, 159 insertions, 0 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 |