aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-02-04 14:26:37 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-02-04 14:26:37 +0100
commitf6b9815685741a76fee78dfb58e8fb8dd70db8f0 (patch)
tree58d28fbf4e12939e05a4861f16a6bd47d4ab6d34
parent7cbc68a8056ace840ef187156461a361554d5fef (diff)
downloadcompcert-f6b9815685741a76fee78dfb58e8fb8dd70db8f0.tar.gz
compcert-f6b9815685741a76fee78dfb58e8fb8dd70db8f0.zip
Moved more common functions into a seperate file.
-rw-r--r--arm/PrintAsm.ml53
-rw-r--r--backend/PrintAsmaux.ml48
-rw-r--r--ia32/PrintAsm.ml65
-rw-r--r--powerpc/PrintAsm.ml40
4 files changed, 69 insertions, 137 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 41a815d6..9558348a 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -32,10 +32,6 @@ module type PRINTER_OPTIONS =
val float_abi: float_abi_type
val vfpv3: bool
val hardware_idiv: bool
- val cfi_startproc: out_channel -> unit
- val cfi_endproc: out_channel -> unit
- val cfi_adjust: out_channel -> int32 -> unit
- val cfi_rel_offset: out_channel -> string -> int32 -> unit
end
(* Module containing the printing functions *)
@@ -48,11 +44,7 @@ let literals_in_code = ref true (* to be turned into a proper option *)
(* Basic printing functions *)
-let print_label oc lbl =
- fprintf oc ".L%d" (transl_label lbl)
-
-let coqint oc n =
- fprintf oc "%ld" (camlint_of_coqint n)
+let print_label oc lbl = label oc (transl_label lbl)
let comment = "@"
@@ -317,8 +309,6 @@ let print_location oc loc =
(* Handling of annotations *)
-let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
-
let print_annot_stmt oc txt targs args =
if Str.string_match re_file_line txt 0 then begin
print_file_line oc (Str.matched_group 1 txt)
@@ -802,7 +792,7 @@ let print_instruction oc = function
| Pstr(r1, r2, sa) | Pstr_a(r1, r2, sa) ->
fprintf oc " str %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa;
begin match r1, r2, sa with
- | IR14, IR13, SOimm n -> Opt.cfi_rel_offset oc "lr" (camlint_of_coqint n)
+ | IR14, IR13, SOimm n -> cfi_rel_offset oc "lr" (camlint_of_coqint n)
| _ -> ()
end;
1
@@ -946,11 +936,11 @@ let print_instruction oc = function
fprintf oc " mov r12, sp\n";
if (!current_function_sig).sig_cc.cc_vararg then begin
fprintf oc " push {r0, r1, r2, r3}\n";
- Opt.cfi_adjust oc 16l
+ cfi_adjust oc 16l
end;
let sz' = camlint_of_coqint sz in
let ninstr = subimm oc "sp" "sp" sz in
- Opt.cfi_adjust oc sz';
+ cfi_adjust oc sz';
fprintf oc " str r12, [sp, #%a]\n" coqint ofs;
current_function_stacksize := sz';
ninstr + (if (!current_function_sig).sig_cc.cc_vararg then 3 else 2)
@@ -1066,13 +1056,12 @@ let print_function oc name fn =
fprintf oc " .thumb_func\n";
fprintf oc "%a:\n" symbol name;
print_location oc (C2C.atom_location name);
- Opt.cfi_startproc oc;
+ cfi_startproc oc;
ignore (fixup_arguments oc Incoming fn.fn_sig);
print_instructions oc fn.fn_code;
if !literals_in_code then emit_constants oc;
- Opt.cfi_endproc oc;
- fprintf oc " .type %a, %%function\n" symbol name;
- fprintf oc " .size %a, . - %a\n" symbol name symbol name;
+ cfi_endproc oc;
+ print_fun_info oc name;
if not !literals_in_code && !size_constants > 0 then begin
section oc lit;
emit_constants oc
@@ -1131,8 +1120,7 @@ let print_var oc name v =
fprintf oc " .global %a\n" symbol name;
fprintf oc "%a:\n" symbol name;
print_init_data oc name v.gvar_init;
- fprintf oc " .type %a, %%object\n" symbol name;
- fprintf oc " .size %a, . - %a\n" symbol name symbol name
+ print_var_info oc name
end else begin
let sz =
match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
@@ -1167,31 +1155,6 @@ let print_program oc p =
| "armv7r" | "armv7m" -> !Clflags.option_mthumb
| _ -> false
-
- (* Emit .cfi directives *)
- let cfi_startproc =
- if Configuration.asm_supports_cfi then
- (fun oc -> fprintf oc " .cfi_startproc\n")
- else
- (fun _ -> ())
-
- let cfi_endproc =
- if Configuration.asm_supports_cfi then
- (fun oc ->fprintf oc " .cfi_endproc\n")
- else
- (fun _ -> ())
-
- let cfi_adjust =
- if Configuration.asm_supports_cfi then
- (fun oc delta -> fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta)
- else
- (fun _ _ -> ())
-
- let cfi_rel_offset =
- if Configuration.asm_supports_cfi then
- (fun oc reg ofs -> fprintf oc " .cfi_rel_offset %s, %ld\n" reg ofs)
- else
- (fun _ _ _ -> ())
end in
let module Printer = AsmPrinter(Opt) in
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 3493e912..75ecfa40 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -26,8 +26,8 @@ module type TARGET =
val print_epilogue: out_channel -> unit
val print_align: out_channel -> int -> unit
val print_comm_symb: out_channel -> P.t -> int -> unit
- val print_var_info: out_channel -> P.t -> unit
- val print_fun_info: out_channel -> P.t -> unit
+ val print_var_info: bool
+ val print_fun_info: bool
val print_init: out_channel -> init_data -> unit
val reset_constants: unit -> unit
val get_section_names: unit -> section_name * section_name * section_name
@@ -58,6 +58,8 @@ let transl_label lbl =
Hashtbl.add current_function_labels lbl lbl';
lbl'
+let label oc lbl =
+ fprintf oc ".L%d" lbl
(* List of literals and jumptables used in the code *)
@@ -82,3 +84,45 @@ let symbol_offset oc (symb, ofs) =
(* The comment deliminiter *)
let comment = "#"
+
+(* Functions for fun and var info *)
+let print_fun_info oc name =
+ fprintf oc " .type %a, @function\n" symbol name;
+ fprintf oc " .size %a, . - %a\n" symbol name symbol name
+
+let print_var_info oc name =
+ fprintf oc " .type %a, @object\n" symbol name;
+ fprintf oc " .size %a, . - %a\n" symbol name symbol name
+
+(* Emit .cfi directives *)
+let cfi_startproc =
+ if Configuration.asm_supports_cfi then
+ (fun oc -> fprintf oc " .cfi_startproc\n")
+ else
+ (fun _ -> ())
+
+let cfi_endproc =
+ if Configuration.asm_supports_cfi then
+ (fun oc -> fprintf oc " .cfi_endproc\n")
+ else
+ (fun _ -> ())
+
+
+let cfi_adjust =
+ if Configuration.asm_supports_cfi then
+ (fun oc delta -> fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta)
+ else
+ (fun _ _ -> ())
+
+let cfi_rel_offset =
+ if Configuration.asm_supports_cfi then
+ (fun oc reg ofs -> fprintf oc " .cfi_rel_offset %s, %ld\n" reg ofs)
+ else
+ (fun _ _ _ -> ())
+
+(* For handling of annotations *)
+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)
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index b0ef0180..4c845b92 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -19,6 +19,7 @@ open Sections
open AST
open Memdata
open Asm
+open PrintAsmaux
module StringSet = Set.Make(String)
@@ -80,8 +81,7 @@ module Cygwin_System =
let raw_symbol oc s =
fprintf oc "_%s" s
- let symbol oc symb =
- fprintf oc "%s" (extern_atom symb)
+ let symbol = symbol
let label oc lbl =
fprintf oc "L%d" lbl
@@ -129,11 +129,9 @@ module ELF_System =
let raw_symbol oc s =
fprintf oc "%s" s
- let symbol oc symb =
- fprintf oc "%s" (extern_atom symb)
+ let symbol = symbol
- let label oc lbl =
- fprintf oc ".L%d" lbl
+ let label = label
let name_of_section = function
| Section_text -> ".text"
@@ -156,14 +154,10 @@ module ELF_System =
let print_mov_ra oc rd id =
fprintf oc " movl $%a, %a\n" symbol id ireg rd
- let print_fun_info oc name =
- fprintf oc " .type %a, @function\n" symbol name;
- fprintf oc " .size %a, . - %a\n" symbol name symbol name
-
- let print_var_info oc name =
- fprintf oc " .type %a, @object\n" symbol name;
- fprintf oc " .size %a, . - %a\n" symbol name symbol name
-
+ let print_fun_info = print_fun_info
+
+ let print_var_info = print_var_info
+
let print_epilogue _ = ()
let print_comm_decl oc name sz al =
@@ -247,33 +241,13 @@ module MacOS_System =
module AsmPrinter(Target: SYSTEM) =
(struct
open Target
-(* On-the-fly label renaming *)
-
-let next_label = ref 100
-
-let new_label() =
- let lbl = !next_label in incr next_label; lbl
-
-let current_function_labels = (Hashtbl.create 39 : (label, int) Hashtbl.t)
-
-let transl_label lbl =
- try
- Hashtbl.find current_function_labels lbl
- with Not_found ->
- let lbl' = new_label() in
- Hashtbl.add current_function_labels lbl lbl';
- lbl'
(* Basic printing functions *)
-let comment = "#"
-
let symbol_offset oc (symb, ofs) =
symbol oc symb;
if ofs <> 0l then fprintf oc " + %ld" ofs
-let coqint oc n =
- fprintf oc "%ld" (camlint_of_coqint n)
let addressing oc (Addrmode(base, shift, cst)) =
begin match cst with
@@ -344,17 +318,6 @@ let print_file_line oc file line =
let print_location oc loc =
if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
-(* Emit .cfi directives *)
-
-let cfi_startproc oc =
- if Configuration.asm_supports_cfi then fprintf oc " .cfi_startproc\n"
-
-let cfi_endproc oc =
- if Configuration.asm_supports_cfi then fprintf oc " .cfi_endproc\n"
-
-let cfi_adjust oc delta =
- if Configuration.asm_supports_cfi then
- fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta
(* Built-in functions *)
@@ -366,8 +329,6 @@ let cfi_adjust oc delta =
(* Handling of annotations *)
-let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
-
let print_annot_stmt oc txt targs args =
if Str.string_match re_file_line txt 0 then begin
print_file_line oc (Str.matched_group 1 txt)
@@ -528,10 +489,6 @@ let print_builtin_vstore_global oc chunk id ofs args =
(* Handling of varargs *)
-let current_function_stacksize = ref 0l
-let current_function_sig =
- ref { sig_args = []; sig_res = None; sig_cc = cc_default }
-
let print_builtin_va_start oc r =
if not (!current_function_sig).sig_cc.cc_vararg then
invalid_arg "Fatal error: va_start used in non-vararg function";
@@ -656,10 +613,6 @@ let print_builtin_inline oc name args res =
(* Printing of instructions *)
-let float64_literals : (int * int64) list ref = ref []
-let float32_literals : (int * int32) list ref = ref []
-let jumptables : (int * label list) list ref = ref []
-
(* Reminder on AT&T syntax: op source, dest *)
let print_instruction oc = function
@@ -1043,7 +996,7 @@ let print_program oc p =
| ELF -> (module ELF_System:SYSTEM)
| Cygwin -> (module Cygwin_System:SYSTEM)):SYSTEM) in
let module Printer = AsmPrinter(Target) in
- PrintAnnot.print_version_and_options oc Printer.comment;
+ PrintAnnot.print_version_and_options oc comment;
PrintAnnot.reset_filenames();
Printer.need_masks := false;
List.iter (Printer.print_globdef oc) p.prog_defs;
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 6e9e1a4f..d733c514 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -115,31 +115,13 @@ module Linux_System : SYSTEM =
PrintAnnot.print_file_line oc comment file line
(* Emit .cfi directives *)
- let cfi_startproc =
- if Configuration.asm_supports_cfi then
- (fun oc -> fprintf oc " .cfi_startproc\n")
- else
- (fun _ -> ())
-
- let cfi_endproc =
- if Configuration.asm_supports_cfi then
- (fun oc -> fprintf oc " .cfi_endproc\n")
- else
- (fun _ -> ())
+ let cfi_startproc = cfi_startproc
+ let cfi_endproc = cfi_endproc
- let cfi_adjust =
- if Configuration.asm_supports_cfi then
- (fun oc delta -> fprintf oc " .cfi_adjust_cfa_offset %ld\n" delta)
- else
- (fun _ _ -> ())
+ let cfi_adjust = cfi_adjust
- let cfi_rel_offset =
- if Configuration.asm_supports_cfi then
- (fun oc reg ofs -> fprintf oc " .cfi_rel_offset %s, %ld\n" reg ofs)
- else
- (fun _ _ _ -> ())
-
+ let cfi_rel_offset = cfi_rel_offset
let print_prologue oc = ()
@@ -217,15 +199,9 @@ module AsmPrinter (Target : SYSTEM) =
(* Basic printing functions *)
-let coqint oc n =
- fprintf oc "%ld" (camlint_of_coqint n)
-
let raw_symbol oc s =
fprintf oc "%s" s
-let label oc lbl =
- fprintf oc ".L%d" lbl
-
let label_low oc lbl =
fprintf oc ".L%d@l" lbl
@@ -280,8 +256,6 @@ let rolm_mask n =
(* Handling of annotations *)
-let re_file_line = Str.regexp "#line:\\(.*\\):\\([1-9][0-9]*\\)$"
-
let print_annot_stmt oc txt targs args =
if Str.string_match re_file_line txt 0 then begin
print_file_line oc (Str.matched_group 1 txt)
@@ -703,8 +677,7 @@ let print_function oc name fn =
print_instructions oc (label_positions PTree.empty 0 fn.fn_code)
0 true fn.fn_code;
cfi_endproc oc;
- fprintf oc " .type %a, @function\n" symbol name;
- fprintf oc " .size %a, . - %a\n" symbol name symbol name;
+ print_fun_info oc name;
if !float64_literals <> [] || !float32_literals <> [] then begin
section oc lit;
fprintf oc " .balign 8\n";
@@ -777,8 +750,7 @@ let print_var oc name v =
fprintf oc " .globl %a\n" symbol name;
fprintf oc "%a:\n" symbol name;
print_init_data oc name v.gvar_init;
- fprintf oc " .type %a, @object\n" symbol name;
- fprintf oc " .size %a, . - %a\n" symbol name symbol name
+ print_var_info oc name
end else begin
let sz =
match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in