diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-04-02 16:25:25 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-04-02 16:25:25 +0200 |
commit | 170284b51766112e29d6bbfe519bad9f6da95269 (patch) | |
tree | 13a163ccee48cee0512a8af484b394623cdce030 /backend/PrintAnnot.ml | |
parent | 2e30ad9698a6f24a8a746f68b30c235913006392 (diff) | |
parent | 959432fa13a899290db5236f93575a8bfdc13bb5 (diff) | |
download | compcert-170284b51766112e29d6bbfe519bad9f6da95269.tar.gz compcert-170284b51766112e29d6bbfe519bad9f6da95269.zip |
Merge branch 'master' into dwarf
Diffstat (limited to 'backend/PrintAnnot.ml')
-rw-r--r-- | backend/PrintAnnot.ml | 65 |
1 files changed, 32 insertions, 33 deletions
diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml index 7b0c1083..995f22dd 100644 --- a/backend/PrintAnnot.ml +++ b/backend/PrintAnnot.ml @@ -97,11 +97,34 @@ let print_file_line_d2 oc pref file line = let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" -type arg_value = - | Reg of preg - | Stack of memory_chunk * Int.int - | Intconst of Int.int - | Floatconst of float +let rec print_annot print_preg sp_reg_name oc = function + | AA_base x -> print_preg oc x + | AA_int n -> fprintf oc "%ld" (camlint_of_coqint n) + | AA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n) + | AA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n) + | AA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n) + | AA_loadstack(chunk, ofs) -> + fprintf oc "mem(%s + %ld, %ld)" + sp_reg_name + (camlint_of_coqint ofs) + (camlint_of_coqint (size_chunk chunk)) + | AA_addrstack ofs -> + fprintf oc "(%s + %ld)" + sp_reg_name + (camlint_of_coqint ofs) + | AA_loadglobal(chunk, id, ofs) -> + fprintf oc "mem(\"%s\" + %ld, %ld)" + (extern_atom id) + (camlint_of_coqint ofs) + (camlint_of_coqint (size_chunk chunk)) + | AA_addrglobal(id, ofs) -> + fprintf oc "(\"%s\" + %ld)" + (extern_atom id) + (camlint_of_coqint ofs) + | AA_longofwords(hi, lo) -> + fprintf oc "(%a * 0x100000000 + %a)" + (print_annot print_preg sp_reg_name) hi + (print_annot print_preg sp_reg_name) lo let print_annot_text print_preg sp_reg_name oc txt args = let print_fragment = function @@ -112,42 +135,18 @@ let print_annot_text print_preg sp_reg_name oc txt args = | Str.Delim s -> let n = int_of_string (String.sub s 1 (String.length s - 1)) in try - match List.nth args (n-1) with - | Reg r -> - print_preg oc r - | Stack(chunk, ofs) -> - fprintf oc "mem(%s + %ld, %ld)" - sp_reg_name - (camlint_of_coqint ofs) - (camlint_of_coqint (size_chunk chunk)) - | Intconst n -> - fprintf oc "%ld" (camlint_of_coqint n) - | Floatconst n -> - fprintf oc "%.18g" (camlfloat_of_coqfloat n) + print_annot print_preg sp_reg_name oc (List.nth args (n-1)) with Failure _ -> fprintf oc "<bad parameter %s>" s in List.iter print_fragment (Str.full_split re_annot_param txt); fprintf oc "\n" -let rec annot_args tmpl args = - match tmpl, args with - | [], _ -> [] - | AA_arg _ :: tmpl', APreg r :: args' -> - Reg r :: annot_args tmpl' args' - | AA_arg _ :: tmpl', APstack(chunk, ofs) :: args' -> - Stack(chunk, ofs) :: annot_args tmpl' args' - | AA_arg _ :: tmpl', [] -> [] (* should never happen *) - | AA_int n :: tmpl', _ -> - Intconst n :: annot_args tmpl' args - | AA_float n :: tmpl', _ -> - Floatconst n :: annot_args tmpl' args - -let print_annot_stmt print_preg sp_reg_name oc txt tmpl args = - print_annot_text print_preg sp_reg_name oc txt (annot_args tmpl args) +let print_annot_stmt print_preg sp_reg_name oc txt tys args = + print_annot_text print_preg sp_reg_name oc txt args let print_annot_val print_preg oc txt args = print_annot_text print_preg "<internal error>" oc txt - (List.map (fun r -> Reg r) args) + (List.map (fun r -> AA_base r) args) (* Print CompCert version and command-line as asm comment *) |