diff options
Diffstat (limited to 'ia32')
-rw-r--r-- | ia32/Asmexpand.ml | 30 | ||||
-rw-r--r-- | ia32/CBuiltins.ml | 8 | ||||
-rw-r--r-- | ia32/TargetPrinter.ml | 84 |
3 files changed, 61 insertions, 61 deletions
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index 4f02e633..871599d1 100644 --- a/ia32/Asmexpand.ml +++ b/ia32/Asmexpand.ml @@ -21,7 +21,7 @@ open AST open Camlcoq open Datatypes open Integers - + exception Error of string (* Useful constants and helper functions *) @@ -35,14 +35,14 @@ let _8 = coqint_of_camlint 8l let stack_alignment () = if Configuration.system = "macoxs" then 16 else 8 - + (* SP adjustment to allocate or free a stack frame *) - + let int32_align n a = if n >= 0l then Int32.logand (Int32.add n (Int32.of_int (a-1))) (Int32.of_int (-a)) else Int32.logand n (Int32.of_int (-a)) - + let sp_adjustment sz = let sz = camlint_of_coqint sz in (* Preserve proper alignment of the stack *) @@ -50,9 +50,9 @@ let sp_adjustment sz = (* The top 4 bytes have already been allocated by the "call" instruction. *) let sz = Int32.sub sz 4l in sz - - -(* Built-ins. They come in two flavors: + + +(* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; - inlined by the compiler: take their arguments in arbitrary @@ -88,7 +88,7 @@ let offset_addressing (Addrmode(base, ofs, cst)) delta = let linear_addr reg ofs = Addrmode(Some reg, None, Coq_inl ofs) let global_addr id ofs = Addrmode(None, None, Coq_inr(id, ofs)) - + (* Handling of memcpy *) (* Unaligned memory accesses are quite fast on IA32, so use large @@ -128,7 +128,7 @@ let expand_builtin_memcpy sz al args = if sz <= 32 then expand_builtin_memcpy_small sz al src dst else expand_builtin_memcpy_big sz al src dst - + (* Handling of volatile reads and writes *) let expand_builtin_vload_common chunk addr res = @@ -197,9 +197,9 @@ let expand_builtin_vstore chunk args = expand_builtin_vstore_common chunk addr src (if Asmgen.addressing_mentions addr EAX then ECX else EAX) | _ -> assert false - + (* Handling of varargs *) - + let expand_builtin_va_start r = if not !current_function.fn_sig.sig_cc.cc_vararg then invalid_arg "Fatal error: va_start used in non-vararg function"; @@ -231,7 +231,7 @@ let expand_fma args res i132 i213 i231 = end | _ -> invalid_arg ("ill-formed fma builtin") - + (* Handling of compiler-inlined builtins *) let expand_builtin_inline name args res = @@ -348,7 +348,7 @@ let expand_builtin_inline name args res = raise (Error ("unrecognized builtin " ^ name)) (* Expansion of instructions *) - + let expand_instruction instr = match instr with | Pallocframe (sz, ofs_ra, ofs_link) -> @@ -379,14 +379,14 @@ let expand_instruction instr = (Int32.to_int (camlint_of_coqint al)) args | EF_annot_val(txt, targ) -> - expand_annot_val txt targ args res + expand_annot_val txt targ args res | EF_annot _ | EF_debug _ | EF_inline_asm _ -> emit instr | _ -> assert false end | _ -> emit instr - + let int_reg_to_dwarf = function | EAX -> 0 | EBX -> 3 diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml index b1be612b..125e71d5 100644 --- a/ia32/CBuiltins.ml +++ b/ia32/CBuiltins.ml @@ -41,19 +41,19 @@ let builtins = { "__builtin_fmin", (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, [])], false); "__builtin_fmadd", - (TFloat(FDouble, []), + (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false); "__builtin_fmsub", - (TFloat(FDouble, []), + (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false); "__builtin_fnmadd", - (TFloat(FDouble, []), + (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false); "__builtin_fnmsub", - (TFloat(FDouble, []), + (TFloat(FDouble, []), [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], false); (* Memory accesses *) diff --git a/ia32/TargetPrinter.ml b/ia32/TargetPrinter.ml index 32e55ec1..1ccfdcba 100644 --- a/ia32/TargetPrinter.ml +++ b/ia32/TargetPrinter.ml @@ -83,13 +83,13 @@ module Cygwin_System : SYSTEM = let raw_symbol oc s = fprintf oc "_%s" s - + let symbol oc symb = raw_symbol oc (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 -> @@ -106,18 +106,18 @@ module Cygwin_System : SYSTEM = | Section_debug_loc -> ".section .debug_loc,\"dr\"" | Section_debug_line _ -> ".section .debug_line,\"dr\"" | Section_debug_abbrev -> ".section .debug_abbrev,\"dr\"" - | Section_debug_str-> assert false (* Should not be used *) - + | Section_debug_str-> assert false (* Should not be used *) + 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 = + + 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 _ = () @@ -134,10 +134,10 @@ module Cygwin_System : SYSTEM = (* Printer functions for ELF *) module ELF_System : SYSTEM = struct - + let raw_symbol oc s = fprintf oc "%s" s - + let symbol = elf_symbol let label = elf_label @@ -159,19 +159,19 @@ module ELF_System : SYSTEM = | Section_debug_line _ -> ".section .debug_line,\"\",@progbits" | Section_debug_abbrev -> ".section .debug_abbrev,\"\",@progbits" | Section_debug_str -> ".section .debug_str,\"MS\",@progbits,1" - + 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 = + + let print_mov_ra oc rd id = fprintf oc " movl $%a, %a\n" symbol id ireg rd let print_fun_info = elf_print_fun_info - + let print_var_info = elf_print_var_info - + let print_epilogue _ = () let print_comm_decl oc name sz al = @@ -186,7 +186,7 @@ module ELF_System : SYSTEM = (* Printer functions for MacOS *) module MacOS_System : SYSTEM = struct - + let raw_symbol oc s = fprintf oc "_%s" s @@ -214,30 +214,30 @@ module MacOS_System : SYSTEM = | Section_debug_line _ -> ".section __DWARF,__debug_line,regular,debug" | Section_debug_str -> ".section __DWARF,__debug_str,regular,debug" | Section_debug_abbrev -> ".section __DWARF,__debug_abbrev,regular,debug" (* Dummy value *) - - + + let stack_alignment = 16 (* mandatory *) - - (* Base-2 log of a Caml integer *) + + (* Base-2 log of a Caml integer *) let rec log2 n = assert (n > 0); if n = 1 then 0 else 1 + log2 (n lsr 1) let print_align oc n = fprintf oc " .align %d\n" (log2 n) - + let indirect_symbols : StringSet.t ref = ref StringSet.empty - let print_mov_ra oc rd id = + let print_mov_ra oc rd id = let id = extern_atom id in indirect_symbols := StringSet.add id !indirect_symbols; fprintf oc " movl L%a$non_lazy_ptr, %a\n" raw_symbol id ireg rd let print_fun_info _ _ = () - + let print_var_info _ _ = () - - let print_epilogue oc = + + let print_epilogue oc = fprintf oc " .section __IMPORT,__pointers,non_lazy_symbol_pointers\n"; StringSet.iter (fun s -> @@ -275,7 +275,7 @@ module Target(System: SYSTEM):TARGET = | Coq_inl n -> let n = camlint_of_coqint n in fprintf oc "%ld" n - | Coq_inr(id, ofs) -> + | Coq_inr(id, ofs) -> let ofs = camlint_of_coqint ofs in if ofs = 0l then symbol oc id @@ -292,13 +292,13 @@ module Target(System: SYSTEM):TARGET = | Cond_e -> "e" | Cond_ne -> "ne" | Cond_b -> "b" | Cond_be -> "be" | Cond_ae -> "ae" | Cond_a -> "a" | Cond_l -> "l" | Cond_le -> "le" | Cond_ge -> "ge" | Cond_g -> "g" - | Cond_p -> "p" | Cond_np -> "np" + | Cond_p -> "p" | Cond_np -> "np" let name_of_neg_condition = function | Cond_e -> "ne" | Cond_ne -> "e" | Cond_b -> "ae" | Cond_be -> "a" | Cond_ae -> "b" | Cond_a -> "be" | Cond_l -> "ge" | Cond_le -> "g" | Cond_ge -> "l" | Cond_g -> "le" - | Cond_p -> "np" | Cond_np -> "p" + | Cond_p -> "np" | Cond_np -> "p" (* Names of sections *) @@ -342,7 +342,7 @@ module Target(System: SYSTEM):TARGET = (* Built-in functions *) -(* Built-ins. They come in two flavors: +(* Built-ins. They come in two flavors: - annotation statements: take their arguments in registers or stack locations; generate no code; - inlined by the compiler: take their arguments in arbitrary @@ -652,7 +652,7 @@ module Target(System: SYSTEM):TARGET = (** Pseudo-instructions *) | Plabel(l) -> fprintf oc "%a:\n" label (transl_label l) - | Pallocframe(sz, ofs_ra, ofs_link) + | Pallocframe(sz, ofs_ra, ofs_link) | Pfreeframe(sz, ofs_ra, ofs_link) -> assert false | Pbuiltin(ef, args, res) -> @@ -670,13 +670,13 @@ module Target(System: SYSTEM):TARGET = | _ -> assert false end - + let print_literal64 oc (lbl, n) = fprintf oc "%a: .quad 0x%Lx\n" label lbl n let print_literal32 oc (lbl, n) = fprintf oc "%a: .long 0x%lx\n" label lbl n - - let print_jumptable oc jmptbl = + + let print_jumptable oc jmptbl = let print_jumptable oc (lbl, tbl) = fprintf oc "%a:" label lbl; List.iter @@ -688,7 +688,7 @@ module Target(System: SYSTEM):TARGET = List.iter (print_jumptable oc) !jumptables; jumptables := [] end - + let print_init oc = function | Init_int8 n -> fprintf oc " .byte %ld\n" (camlint_of_coqint n) @@ -710,7 +710,7 @@ module Target(System: SYSTEM):TARGET = if Z.gt n Z.zero then fprintf oc " .space %s\n" (Z.to_string n) | Init_addrof(symb, ofs) -> - fprintf oc " .long %a\n" + fprintf oc " .long %a\n" symbol_offset (symb, camlint_of_coqint ofs) let print_align = print_align @@ -741,7 +741,7 @@ module Target(System: SYSTEM):TARGET = let print_optional_fun_info _ = () - let get_section_names name = + let get_section_names name = match C2C.atom_sections name with | [t;l;j] -> (t, l, j) | _ -> (Section_text, Section_literal, Section_jumptable) @@ -749,10 +749,10 @@ module Target(System: SYSTEM):TARGET = let reset_constants = reset_constants let print_fun_info = print_fun_info - + let print_var_info = print_var_info - let print_prologue oc = + let print_prologue oc = need_masks := false; if !Clflags.option_g then begin section oc Section_text; @@ -762,7 +762,7 @@ module Target(System: SYSTEM):TARGET = fprintf oc " .cfi_sections .debug_frame\n" end - let print_epilogue oc = + let print_epilogue oc = if !need_masks then begin section oc (Section_const true); (* not Section_literal because not 8-bytes *) @@ -784,13 +784,13 @@ module Target(System: SYSTEM):TARGET = section oc Section_text; fprintf oc "%a:\n" elf_label high_pc end - + let comment = comment let default_falignment = 16 let label = label - + let new_label = new_label end @@ -798,7 +798,7 @@ end let sel_target () = let module S = (val (match Configuration.system with | "macosx" -> (module MacOS_System:SYSTEM) - | "linux" + | "linux" | "bsd" -> (module ELF_System:SYSTEM) | "cygwin" -> (module Cygwin_System:SYSTEM) | _ -> invalid_arg ("System " ^ Configuration.system ^ " not supported") ):SYSTEM) in |