aboutsummaryrefslogtreecommitdiffstats
path: root/ia32
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2015-02-10 14:33:47 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2015-02-10 14:33:47 +0100
commita7f49e1e55cdf648e7778c1fc12fbc3ac9782c1a (patch)
tree5e07dae89efdc5884160124ce1113c6d0152e6bb /ia32
parentf2b1c25aa56a27836652aef3feeee0856c04235c (diff)
downloadcompcert-a7f49e1e55cdf648e7778c1fc12fbc3ac9782c1a.tar.gz
compcert-a7f49e1e55cdf648e7778c1fc12fbc3ac9782c1a.zip
Added new Mingw Printer. Currently the only difference to the Cygwin printer is that every symbol must start with an "_".
Diffstat (limited to 'ia32')
-rw-r--r--ia32/PrintAsm.ml68
1 files changed, 55 insertions, 13 deletions
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index b0ef0180..94d728e2 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -122,6 +122,55 @@ module Cygwin_System =
end:SYSTEM)
+(* Printer functions for cygwin *)
+module Mingw_System =
+ (struct
+
+ let raw_symbol oc s =
+ fprintf oc "_%s" s
+
+ let symbol oc symb =
+ fprintf oc "_%s" (extern_atom symb)
+
+ let label oc lbl =
+ fprintf oc "L%d" lbl
+
+ let name_of_section = function
+ | Section_text -> ".text"
+ | Section_data i | Section_small_data i ->
+ if i then ".data" else "COMM"
+ | Section_const i | Section_small_const i ->
+ if i then ".section .rdata,\"dr\"" else "COMM"
+ | Section_string -> ".section .rdata,\"dr\""
+ | Section_literal -> ".section .rdata,\"dr\""
+ | Section_jumptable -> ".text"
+ | Section_user(s, wr, ex) ->
+ sprintf ".section \"%s\", \"%s\"\n"
+ s (if ex then "xr" else if wr then "d" else "dr")
+
+ let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *)
+
+ let print_align oc n =
+ fprintf oc " .align %d\n" n
+
+ let print_mov_ra oc rd id =
+ fprintf oc " movl $%a, %a\n" symbol id ireg rd
+
+ let print_fun_info _ _ = ()
+
+ let print_var_info _ _ = ()
+
+ let print_epilogue _ = ()
+
+ let print_comm_decl oc name sz al =
+ fprintf oc " .comm %a, %s, %d\n" symbol name (Z.to_string sz) al
+
+ let print_lcomm_decl oc name sz al =
+ fprintf oc " .local %a\n" symbol name;
+ print_comm_decl oc name sz al
+
+ end:SYSTEM)
+
(* Printer functions for ELF *)
module ELF_System =
(struct
@@ -1028,20 +1077,13 @@ let print_globdef oc (name, gdef) =
| Gvar v -> print_var oc name v
end)
-type target = ELF | MacOS | Cygwin
-
let print_program oc p =
- let target =
- match Configuration.system with
- | "macosx" -> MacOS
- | "linux" -> ELF
- | "bsd" -> ELF
- | "cygwin" -> Cygwin
- | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") in
- let module Target = (val (match target with
- | MacOS -> (module MacOS_System:SYSTEM)
- | ELF -> (module ELF_System:SYSTEM)
- | Cygwin -> (module Cygwin_System:SYSTEM)):SYSTEM) in
+ let module Target = (val (match Configuration.system with
+ | "macosx" -> (module MacOS_System:SYSTEM)
+ | "linux" | "bsd" -> (module ELF_System:SYSTEM)
+ | "cygwin" -> (module Cygwin_System:SYSTEM)
+ | "mingw" -> (module Mingw_System:SYSTEM)
+ | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported")):SYSTEM) in
let module Printer = AsmPrinter(Target) in
PrintAnnot.print_version_and_options oc Printer.comment;
PrintAnnot.reset_filenames();