diff options
author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
---|---|---|
committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
commit | 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f (patch) | |
tree | 1961b41815fc6e392cc0bd2beeb0fb504bc160ce /ia32/Asmexpand.ml | |
parent | 7a6bb90048db7a254e959b1e3c308bac5fe6c418 (diff) | |
download | compcert-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.tar.gz compcert-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.zip |
Updated PR by removing whitespaces. Bug 17450.
Diffstat (limited to 'ia32/Asmexpand.ml')
-rw-r--r-- | ia32/Asmexpand.ml | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index 99babeb4..d11d9d23 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 |