diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/Bounds.v | 7 | ||||
-rw-r--r-- | backend/PrintAnnot.ml | 182 | ||||
-rw-r--r-- | backend/PrintAsm.ml | 6 | ||||
-rw-r--r-- | backend/PrintAsmaux.ml | 160 | ||||
-rw-r--r-- | backend/Regalloc.ml | 6 |
5 files changed, 166 insertions, 195 deletions
diff --git a/backend/Bounds.v b/backend/Bounds.v index 7528b66e..04c1328d 100644 --- a/backend/Bounds.v +++ b/backend/Bounds.v @@ -87,8 +87,6 @@ Section BOUNDS. Variable f: function. -Parameter mregs_of_clobber: list ident -> list mreg. - (** In the proof of the [Stacking] pass, we only need to bound the registers written by an instruction. Therefore, this function returns these registers, ignoring registers used only as @@ -103,7 +101,6 @@ Definition regs_of_instr (i: instruction) : list mreg := | Lstore chunk addr args src => nil | Lcall sig ros => nil | Ltailcall sig ros => nil - | Lbuiltin (EF_inline_asm txt typs clob) args res => res ++ mregs_of_clobber clob | Lbuiltin ef args res => res ++ destroyed_by_builtin ef | Lannot ef args => nil | Llabel lbl => nil @@ -354,9 +351,7 @@ Proof. (* call *) eapply size_arguments_bound; eauto. (* builtin *) - apply H1. destruct e; apply in_or_app; auto. - change (destroyed_by_builtin (EF_inline_asm text sg clobbers)) with (@nil mreg) in H2. - simpl in H2; tauto. + apply H1. apply in_or_app; auto. (* annot *) apply H0. rewrite slots_of_locs_charact; auto. Qed. diff --git a/backend/PrintAnnot.ml b/backend/PrintAnnot.ml deleted file mode 100644 index 88f5d8d6..00000000 --- a/backend/PrintAnnot.ml +++ /dev/null @@ -1,182 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - -(* Printing annotations in asm syntax *) - -open Printf -open Datatypes -open Integers -open Floats -open Camlcoq -open AST -open Memdata -open Asm - -(** All files used in the debug entries *) -module StringSet = Set.Make(String) -let all_files : StringSet.t ref = ref StringSet.empty -let add_file file = - all_files := StringSet.add file !all_files - - -(** Line number annotations *) - -let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t - = Hashtbl.create 7 - -let last_file = ref "" - -let reset_filenames () = - Hashtbl.clear filename_info; last_file := "" - -let close_filenames () = - Hashtbl.iter - (fun file (num, fb) -> - match fb with Some b -> Printlines.close b | None -> ()) - filename_info; - reset_filenames() - -let enter_filename f = - let num = Hashtbl.length filename_info + 1 in - let filebuf = - if !Clflags.option_S || !Clflags.option_dasm then begin - try Some (Printlines.openfile f) - with Sys_error _ -> None - end else None in - Hashtbl.add filename_info f (num, filebuf); - (num, filebuf) - -(* Add file and line debug location, using GNU assembler-style DWARF2 - directives *) - -let print_file_line oc pref file line = - if !Clflags.option_g && file <> "" then begin - let (filenum, filebuf) = - try - Hashtbl.find filename_info file - with Not_found -> - let (filenum, filebuf as res) = enter_filename file in - fprintf oc " .file %d %S\n" filenum file; - res in - fprintf oc " .loc %d %d\n" filenum line; - match filebuf with - | None -> () - | Some fb -> Printlines.copy oc pref fb line line - end - -(* Add file and line debug location, using DWARF2 directives in the style - of Diab C 5 *) - -let print_file_line_d2 oc pref file line = - if !Clflags.option_g && file <> "" then begin - let (_, filebuf) = - try - Hashtbl.find filename_info file - with Not_found -> - enter_filename file in - if file <> !last_file then begin - fprintf oc " .d2file %S\n" file; - last_file := file - end; - fprintf oc " .d2line %d\n" line; - match filebuf with - | None -> () - | Some fb -> Printlines.copy oc pref fb line line - end - -(** "True" annotations *) - -let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" - -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 - | Str.Text s -> - output_string oc 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)) - with Failure _ -> - fprintf oc "<bad parameter %s>" s in - List.iter print_fragment (Str.full_split re_annot_param txt); - fprintf oc "\n" - -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 -> AA_base r) args) - -(** Inline assembly *) - -let re_asm_param = Str.regexp "%%\\|%[0-9]+" - -let print_inline_asm print_preg oc txt sg args res = - let operands = - if sg.sig_res = None then args else res @ args in - let print_fragment = function - | Str.Text s -> - output_string oc 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_preg oc (List.nth operands n) - with Failure _ -> - fprintf oc "<bad parameter %s>" s in - List.iter print_fragment (Str.full_split re_asm_param txt); - fprintf oc "\n" - - -(** Print CompCert version and command-line as asm comment *) - -let print_version_and_options oc comment = - fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version; - fprintf oc "%s Command line:" comment; - for i = 1 to Array.length Sys.argv - 1 do - fprintf oc " %s" Sys.argv.(i) - done; - fprintf oc "\n" - diff --git a/backend/PrintAsm.ml b/backend/PrintAsm.ml index 0438a40f..e91b4e03 100644 --- a/backend/PrintAsm.ml +++ b/backend/PrintAsm.ml @@ -130,12 +130,12 @@ module Printer(Target:TARGET) = let print_program oc p db = let module Target = (val (sel_target ()):TARGET) in let module Printer = Printer(Target) in - PrintAnnot.reset_filenames (); - PrintAnnot.print_version_and_options oc Target.comment; + reset_filenames (); + print_version_and_options oc Target.comment; Target.print_prologue oc; List.iter (Printer.print_globdef oc) p.prog_defs; Target.print_epilogue oc; - PrintAnnot.close_filenames (); + close_filenames (); if !Clflags.option_g && Configuration.advanced_debug then begin match db with diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 8bc961ef..497760c1 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -16,6 +16,7 @@ open Asm open Camlcoq open DwarfTypes open Datatypes +open Memdata open Printf open Sections @@ -140,3 +141,162 @@ let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$" (* Basic printing functions *) let coqint oc n = fprintf oc "%ld" (camlint_of_coqint n) + +(* Printing annotations in asm syntax *) +(** All files used in the debug entries *) +module StringSet = Set.Make(String) +let all_files : StringSet.t ref = ref StringSet.empty +let add_file file = + all_files := StringSet.add file !all_files + + +let filename_info : (string, int * Printlines.filebuf option) Hashtbl.t + = Hashtbl.create 7 + +let last_file = ref "" + +let reset_filenames () = + Hashtbl.clear filename_info; last_file := "" + +let close_filenames () = + Hashtbl.iter + (fun file (num, fb) -> + match fb with Some b -> Printlines.close b | None -> ()) + filename_info; + reset_filenames() + +let enter_filename f = + let num = Hashtbl.length filename_info + 1 in + let filebuf = + if !Clflags.option_S || !Clflags.option_dasm then begin + try Some (Printlines.openfile f) + with Sys_error _ -> None + end else None in + Hashtbl.add filename_info f (num, filebuf); + (num, filebuf) + +(* Add file and line debug location, using GNU assembler-style DWARF2 + directives *) + +let print_file_line oc pref file line = + if !Clflags.option_g && file <> "" then begin + let (filenum, filebuf) = + try + Hashtbl.find filename_info file + with Not_found -> + let (filenum, filebuf as res) = enter_filename file in + fprintf oc " .file %d %S\n" filenum file; + res in + fprintf oc " .loc %d %d\n" filenum line; + match filebuf with + | None -> () + | Some fb -> Printlines.copy oc pref fb line line + end + +(* Add file and line debug location, using DWARF2 directives in the style + of Diab C 5 *) + +let print_file_line_d2 oc pref file line = + if !Clflags.option_g && file <> "" then begin + let (_, filebuf) = + try + Hashtbl.find filename_info file + with Not_found -> + enter_filename file in + if file <> !last_file then begin + fprintf oc " .d2file %S\n" file; + last_file := file + end; + fprintf oc " .d2line %d\n" line; + match filebuf with + | None -> () + | Some fb -> Printlines.copy oc pref fb line line + end + + +(** "True" annotations *) + +let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" + +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 + | Str.Text s -> + output_string oc 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)) + with Failure _ -> + fprintf oc "<bad parameter %s>" s in + List.iter print_fragment (Str.full_split re_annot_param txt); + fprintf oc "\n" + +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 -> AA_base r) args) + +(** Inline assembly *) + +let re_asm_param = Str.regexp "%%\\|%[0-9]+" + +let print_inline_asm print_preg oc txt sg args res = + let operands = + if sg.sig_res = None then args else res @ args in + let print_fragment = function + | Str.Text s -> + output_string oc 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_preg oc (List.nth operands n) + with Failure _ -> + fprintf oc "<bad parameter %s>" s in + List.iter print_fragment (Str.full_split re_asm_param txt); + fprintf oc "\n" + + +(** Print CompCert version and command-line as asm comment *) + +let print_version_and_options oc comment = + fprintf oc "%s File generated by CompCert %s\n" comment Configuration.version; + fprintf oc "%s Command line:" comment; + for i = 1 to Array.length Sys.argv - 1 do + fprintf oc " %s" Sys.argv.(i) + done; + fprintf oc "\n" diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index c286e946..aa4efc53 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -585,13 +585,11 @@ let add_interfs_instr g instr live = (* like a move *) IRC.add_pref g arg res | EF_inline_asm(txt, sg, clob), _, _ -> - (* clobbered regs interfere with live set - and also with res and args for GCC compatibility *) + (* clobbered regs interfere with res and args for GCC compatibility *) List.iter (fun c -> - match Machregsaux.register_by_name (extern_atom c) with + match Machregs.register_by_name c with | None -> () | Some mr -> - add_interfs_destroyed g across [mr]; add_interfs_list_mreg g args mr; if sg.sig_res <> None then add_interfs_list_mreg g res mr) clob |