diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-10-05 15:52:58 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-10-05 15:52:58 +0200 |
commit | 26ddb90280b45e92d90eead89edb237f2922824a (patch) | |
tree | ff18b31abdbb97133f9708ca085467f25758e507 /x86/TargetPrinter.ml | |
parent | e9c738e3bd156f68905968e25c70ec796d3119c4 (diff) | |
download | compcert-26ddb90280b45e92d90eead89edb237f2922824a.tar.gz compcert-26ddb90280b45e92d90eead89edb237f2922824a.zip |
Support Cygwin 64 bits
- Add support for the Win64 ABI to the x86_64 port
- Update vararg support to handle Win64 conventions
- Configure support for x86_64-cygwin64
Diffstat (limited to 'x86/TargetPrinter.ml')
-rw-r--r-- | x86/TargetPrinter.ml | 36 |
1 files changed, 31 insertions, 5 deletions
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index f0a54506..481b09b9 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -239,8 +239,11 @@ module MacOS_System : SYSTEM = module Cygwin_System : SYSTEM = struct + let symbol_prefix = + if Archi.ptr64 then "" else "_" + let raw_symbol oc s = - fprintf oc "_%s" s + fprintf oc "%s%s" symbol_prefix s let symbol oc symb = raw_symbol oc (extern_atom symb) @@ -268,19 +271,39 @@ module Cygwin_System : SYSTEM = | Section_debug_str-> assert false (* Should not be used *) | Section_ais_annotation -> assert false (* Not supported for coff binaries *) - let stack_alignment = 8 (* minimum is 4, 8 is better for perfs *) + let stack_alignment = 8 + (* minimum is 4 for 32 bits, 8 for 64 bits; 8 is better for perfs *) let print_align oc n = fprintf oc " .balign %d\n" n + let indirect_symbols : StringSet.t ref = ref StringSet.empty + let print_mov_rs oc rd id = - fprintf oc " movl $%a, %a\n" symbol id ireg rd + if Archi.ptr64 then begin + let s = extern_atom id in + indirect_symbols := StringSet.add s !indirect_symbols; + fprintf oc " movq .refptr.%s(%%rip), %a\n" s ireg rd + end else begin + fprintf oc " movl $%a, %a\n" symbol id ireg rd + end let print_fun_info _ _ = () let print_var_info _ _ = () - let print_epilogue _ = () + let declare_indirect_symbol oc s = + fprintf oc " .section .rdata$.refptr.%s, \"dr\"\n" s; + fprintf oc " .globl .refptr.%s\n" s; + fprintf oc " .linkonce discard\n"; + fprintf oc ".refptr.%s:\n" s; + fprintf oc " .quad %s\n" s + + let print_epilogue oc = + if Archi.ptr64 then begin + StringSet.iter (declare_indirect_symbol oc) !indirect_symbols; + indirect_symbols := StringSet.empty + end let print_comm_decl oc name sz al = fprintf oc " .comm %a, %s, %d\n" @@ -288,7 +311,8 @@ module Cygwin_System : SYSTEM = let print_lcomm_decl oc name sz al = fprintf oc " .lcomm %a, %s, %d\n" - symbol name (Z.to_string sz) (log2 al) + symbol name (Z.to_string sz) + (if Archi.ptr64 then al else log2 al) end @@ -769,6 +793,8 @@ module Target(System: SYSTEM):TARGET = fprintf oc " minsd %a, %a\n" freg a1 freg res | Pmovb_rm (rd,a) -> fprintf oc " movb %a, %a\n" addressing a ireg8 rd + | Pmovq_rf (rd, r1) -> + fprintf oc " movq %a, %a\n" freg r1 ireg64 rd | Pmovsq_mr(a, rs) -> fprintf oc " movq %a, %a\n" freg rs addressing a | Pmovsq_rm(rd, a) -> |