From 32d25a371fc0e1aaea2a94459363b21e9841d637 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Wed, 19 Jul 2017 12:39:17 +0200 Subject: Print_annot should produce a string. --- arm/TargetPrinter.ml | 11 ++++++++--- backend/PrintAsmaux.ml | 51 ++++++++++++++++++++++++------------------------ powerpc/TargetPrinter.ml | 10 +++++----- riscV/TargetPrinter.ml | 11 ++++++++--- x86/TargetPrinter.ml | 11 ++++++++--- 5 files changed, 54 insertions(+), 40 deletions(-) diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 6f1cb6c1..0626a371 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -81,6 +81,11 @@ struct | FR r -> freg oc r | _ -> assert false + let preg_annot = function + | IR r -> int_reg_name r + | FR r -> float_reg_name r + | _ -> assert false + let condition_name = function | TCeq -> "eq" | TCne -> "ne" @@ -730,11 +735,11 @@ struct | Pbuiltin(ef, args, res) -> begin match ef with | EF_annot(txt, targs) -> - fprintf oc "%s annotation: " comment; - print_annot_text preg "sp" oc (camlstring_of_coqstring txt) args; + fprintf oc "%s annotation: %s\n" comment + (annot_text preg_annot "sp" (camlstring_of_coqstring txt) args); 0 | EF_debug(kind, txt, targs) -> - print_debug_info comment print_file_line preg "sp" oc + print_debug_info comment print_file_line preg_annot "sp" oc (P.to_int kind) (extern_atom txt) args; 0 | EF_inline_asm(txt, sg, clob) -> diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index f54c8698..df3445ea 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -150,62 +150,61 @@ let ptrofs oc n = let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" -let rec print_annot print_preg sp_reg_name oc = function - | BA x -> print_preg oc x - | BA_int n -> fprintf oc "%ld" (camlint_of_coqint n) - | BA_long n -> fprintf oc "%Ld" (camlint64_of_coqint n) - | BA_float n -> fprintf oc "%.18g" (camlfloat_of_coqfloat n) - | BA_single n -> fprintf oc "%.18g" (camlfloat_of_coqfloat32 n) +let rec annot_arg preg_string sp_reg_name = function + | BA x -> preg_string x + | BA_int n -> sprintf "%ld" (camlint_of_coqint n) + | BA_long n -> sprintf "%Ld" (camlint64_of_coqint n) + | BA_float n -> sprintf "%.18g" (camlfloat_of_coqfloat n) + | BA_single n -> sprintf "%.18g" (camlfloat_of_coqfloat32 n) | BA_loadstack(chunk, ofs) -> - fprintf oc "mem(%s + %ld, %ld)" + sprintf "mem(%s + %ld, %ld)" sp_reg_name (camlint_of_coqint ofs) (camlint_of_coqint (size_chunk chunk)) | BA_addrstack ofs -> - fprintf oc "(%s + %ld)" + sprintf "(%s + %ld)" sp_reg_name (camlint_of_coqint ofs) | BA_loadglobal(chunk, id, ofs) -> - fprintf oc "mem(\"%s\" + %ld, %ld)" + sprintf "mem(\"%s\" + %ld, %ld)" (extern_atom id) (camlint_of_coqint ofs) (camlint_of_coqint (size_chunk chunk)) | BA_addrglobal(id, ofs) -> - fprintf oc "(\"%s\" + %ld)" + sprintf "(\"%s\" + %ld)" (extern_atom id) (camlint_of_coqint ofs) | BA_splitlong(hi, lo) -> - fprintf oc "(%a * 0x100000000 + %a)" - (print_annot print_preg sp_reg_name) hi - (print_annot print_preg sp_reg_name) lo + sprintf "(%s * 0x100000000 + %s)" + (annot_arg preg_string sp_reg_name hi) + (annot_arg preg_string sp_reg_name lo) | BA_addptr(a1, a2) -> - fprintf oc "(%a + %a)" - (print_annot print_preg sp_reg_name) a1 - (print_annot print_preg sp_reg_name) a2 + sprintf "(%s + %s)" + (annot_arg preg_string sp_reg_name a1) + (annot_arg preg_string sp_reg_name a2) -let print_annot_text print_preg sp_reg_name oc txt args = - let print_fragment = function +let annot_text preg_string sp_reg_name txt args = + let fragment = function | Str.Text s -> - output_string oc s + s | Str.Delim "%%" -> - output_char oc '%' + "%" | Str.Delim s -> let n = int_of_string (String.sub s 1 (String.length s - 1)) in try - print_annot print_preg sp_reg_name oc (List.nth args (n-1)) + annot_arg preg_string sp_reg_name (List.nth args (n-1)) with Failure _ -> - fprintf oc "" s in - List.iter print_fragment (Str.full_split re_annot_param txt); - fprintf oc "\n" + sprintf "" s in + String.concat "" (List.map fragment (Str.full_split re_annot_param txt)) (* Printing of [EF_debug] info. To be completed. *) let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" -let print_debug_info comment print_line print_preg sp_name oc kind txt args = +let print_debug_info comment print_line preg_string sp_name oc kind txt args = let print_debug_args oc args = List.iter - (fun a -> fprintf oc " %a" (print_annot print_preg sp_name) a) + (fun a -> fprintf oc " %s" (annot_arg preg_string sp_name a)) args in match kind with | 1 -> (* line number *) diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml index cb5f2304..bff2a7fa 100644 --- a/powerpc/TargetPrinter.ml +++ b/powerpc/TargetPrinter.ml @@ -335,9 +335,9 @@ module Target (System : SYSTEM):TARGET = (* For printing annotations, use the full register names [rN] and [fN] to avoid ambiguity with constants. *) - let preg_annot oc = function - | IR r -> fprintf oc "r%s" (int_reg_name r) - | FR r -> fprintf oc "f%s" (float_reg_name r) + let preg_annot = function + | IR r -> sprintf "r%s" (int_reg_name r) + | FR r -> sprintf "f%s" (float_reg_name r) | _ -> assert false (* Encoding masks for rlwinm instructions *) @@ -834,8 +834,8 @@ module Target (System : SYSTEM):TARGET = | Pbuiltin(ef, args, res) -> begin match ef with | EF_annot(txt, targs) -> - fprintf oc "%s annotation: " comment; - print_annot_text preg_annot "r1" oc (camlstring_of_coqstring txt) args + fprintf oc "%s annotation: %s\n" comment + (annot_text preg_annot "r1" (camlstring_of_coqstring txt) args) | 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 7a369832..65339d35 100644 --- a/riscV/TargetPrinter.ml +++ b/riscV/TargetPrinter.ml @@ -97,6 +97,11 @@ module Target : TARGET = | FR r -> freg oc r | _ -> assert false + let preg_annot = function + | IR r -> int_reg_name r + | FR r -> float_reg_name r + | _ -> assert false + (* Names of sections *) let name_of_section = function @@ -585,10 +590,10 @@ module Target : TARGET = | Pbuiltin(ef, args, res) -> begin match ef with | EF_annot(txt, targs) -> - fprintf oc "%s annotation: " comment; - print_annot_text preg "sp" oc (camlstring_of_coqstring txt) args + fprintf oc "%s annotation: %s\n" comment + (annot_text preg_annot "sp" (camlstring_of_coqstring txt) args) | EF_debug(kind, txt, targs) -> - print_debug_info comment print_file_line preg "sp" oc + print_debug_info comment print_file_line preg_annot "sp" oc (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index 4a576df3..f61d7686 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -66,6 +66,11 @@ let preg oc = function | FR r -> freg oc r | _ -> assert false +let preg_annot = function + | IR r -> if Archi.ptr64 then int64_reg_name r else int32_reg_name r + | FR r -> float_reg_name r + | _ -> assert false + let z oc n = output_string oc (Z.to_string n) (* 32/64 bit dependencies *) @@ -736,10 +741,10 @@ module Target(System: SYSTEM):TARGET = | Pbuiltin(ef, args, res) -> begin match ef with | EF_annot(txt, targs) -> - fprintf oc "%s annotation: " comment; - print_annot_text preg "%esp" oc (camlstring_of_coqstring txt) args + fprintf oc "%s annotation: %s\n" comment + (annot_text preg_annot "%esp" (camlstring_of_coqstring txt) args) | EF_debug(kind, txt, targs) -> - print_debug_info comment print_file_line preg "%esp" oc + print_debug_info comment print_file_line preg_annot "%esp" oc (P.to_int kind) (extern_atom txt) args | EF_inline_asm(txt, sg, clob) -> fprintf oc "%s begin inline assembly\n\t" comment; -- cgit