aboutsummaryrefslogtreecommitdiffstats
path: root/arm/PrintAsm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'arm/PrintAsm.ml')
-rw-r--r--arm/PrintAsm.ml1176
1 files changed, 0 insertions, 1176 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
deleted file mode 100644
index 9558348a..00000000
--- a/arm/PrintAsm.ml
+++ /dev/null
@@ -1,1176 +0,0 @@
-(* *********************************************************************)
-(* *)
-(* The Compcert verified compiler *)
-(* *)
-(* Xavier Leroy, INRIA Paris-Rocquencourt *)
-(* *)
-(* Copyright Institut National de Recherche en Informatique et en *)
-(* Automatique. All rights reserved. This file is distributed *)
-(* under the terms of the INRIA Non-Commercial License Agreement. *)
-(* *)
-(* *********************************************************************)
-
-(* Printing ARM assembly code in asm syntax *)
-
-open Printf
-open Datatypes
-open Camlcoq
-open Sections
-open AST
-open Memdata
-open Asm
-open PrintAsmaux
-
-(* Type for the ABI versions *)
-type float_abi_type =
- | Hard
- | Soft
-
-(* Module type for the options *)
-module type PRINTER_OPTIONS =
- sig
- val float_abi: float_abi_type
- val vfpv3: bool
- val hardware_idiv: bool
- end
-
-(* Module containing the printing functions *)
-
-module AsmPrinter (Opt: PRINTER_OPTIONS) =
- (struct
-(* Code generation options. *)
-
-let literals_in_code = ref true (* to be turned into a proper option *)
-
-(* Basic printing functions *)
-
-let print_label oc lbl = label oc (transl_label lbl)
-
-let comment = "@"
-
-let symbol_offset oc (symb, ofs) =
- symbol oc symb;
- let ofs = camlint_of_coqint ofs in
- if ofs <> 0l then fprintf oc " + %ld" ofs
-
-let int_reg_name = function
- | IR0 -> "r0" | IR1 -> "r1" | IR2 -> "r2" | IR3 -> "r3"
- | IR4 -> "r4" | IR5 -> "r5" | IR6 -> "r6" | IR7 -> "r7"
- | IR8 -> "r8" | IR9 -> "r9" | IR10 -> "r10" | IR11 -> "r11"
- | IR12 -> "r12" | IR13 -> "sp" | IR14 -> "lr"
-
-let float_reg_name = function
- | FR0 -> "d0" | FR1 -> "d1" | FR2 -> "d2" | FR3 -> "d3"
- | FR4 -> "d4" | FR5 -> "d5" | FR6 -> "d6" | FR7 -> "d7"
- | FR8 -> "d8" | FR9 -> "d9" | FR10 -> "d10" | FR11 -> "d11"
- | FR12 -> "d12" | FR13 -> "d13" | FR14 -> "d14" | FR15 -> "d15"
-
-let single_float_reg_index = function
- | FR0 -> 0 | FR1 -> 2 | FR2 -> 4 | FR3 -> 6
- | FR4 -> 8 | FR5 -> 10 | FR6 -> 12 | FR7 -> 14
- | FR8 -> 16 | FR9 -> 18 | FR10 -> 20 | FR11 -> 22
- | FR12 -> 24 | FR13 -> 26 | FR14 -> 28 | FR15 -> 30
-
-let single_float_reg_name = function
- | FR0 -> "s0" | FR1 -> "s2" | FR2 -> "s4" | FR3 -> "s6"
- | FR4 -> "s8" | FR5 -> "s10" | FR6 -> "s12" | FR7 -> "s14"
- | FR8 -> "s16" | FR9 -> "s18" | FR10 -> "s20" | FR11 -> "s22"
- | FR12 -> "s24" | FR13 -> "s26" | FR14 -> "s28" | FR15 -> "s30"
-
-let ireg oc r = output_string oc (int_reg_name r)
-let freg oc r = output_string oc (float_reg_name r)
-let freg_single oc r = output_string oc (single_float_reg_name r)
-
-let preg oc = function
- | IR r -> ireg oc r
- | FR r -> freg oc r
- | _ -> assert false
-
-let condition_name = function
- | TCeq -> "eq"
- | TCne -> "ne"
- | TChs -> "hs"
- | TClo -> "lo"
- | TCmi -> "mi"
- | TCpl -> "pl"
- | TChi -> "hi"
- | TCls -> "ls"
- | TCge -> "ge"
- | TClt -> "lt"
- | TCgt -> "gt"
- | TCle -> "le"
-
-let neg_condition_name = function
- | TCeq -> "ne"
- | TCne -> "eq"
- | TChs -> "lo"
- | TClo -> "hs"
- | TCmi -> "pl"
- | TCpl -> "mi"
- | TChi -> "ls"
- | TCls -> "hi"
- | TCge -> "lt"
- | TClt -> "ge"
- | TCgt -> "le"
- | TCle -> "gt"
-
-(* In Thumb2 mode, some arithmetic instructions have shorter encodings
- if they carry the "S" flag (update condition flags):
- add (but not sp + imm)
- and
- asr
- bic
- eor
- lsl
- lsr
- mov
- mvn
- orr
- rsb
- sub (but not sp - imm)
- The proof of Asmgen shows that CompCert-generated code behaves the
- same whether flags are updated or not by those instructions. The
- following printing function adds a "S" suffix if we are in Thumb2
- mode. *)
-
-let thumbS oc =
- if !Clflags.option_mthumb then output_char oc 's'
-
-(* Names of sections *)
-
-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 .rodata" else "COMM"
- | Section_string -> ".section .rodata"
- | Section_literal -> ".text"
- | Section_jumptable -> ".text"
- | Section_user(s, wr, ex) ->
- sprintf ".section \"%s\",\"a%s%s\",%%progbits"
- s (if wr then "w" else "") (if ex then "x" else "")
-
-let section oc sec =
- fprintf oc " %s\n" (name_of_section sec)
-
-(* Record current code position and latest position at which to
- emit float and symbol constants. *)
-
-let currpos = ref 0
-let size_constants = ref 0
-let max_pos_constants = ref max_int
-
-let distance_to_emit_constants () =
- if !literals_in_code
- then !max_pos_constants - (!currpos + !size_constants)
- else max_int
-
-(* Associate labels to floating-point constants and to symbols *)
-
-let float_labels = (Hashtbl.create 39 : (int64, int) Hashtbl.t)
-let float32_labels = (Hashtbl.create 39 : (int32, int) Hashtbl.t)
-
-let label_float bf =
- try
- Hashtbl.find float_labels bf
- with Not_found ->
- let lbl' = new_label() in
- Hashtbl.add float_labels bf lbl';
- size_constants := !size_constants + 8;
- max_pos_constants := min !max_pos_constants (!currpos + 1024);
- lbl'
-
-let label_float32 bf =
- try
- Hashtbl.find float32_labels bf
- with Not_found ->
- let lbl' = new_label() in
- Hashtbl.add float32_labels bf lbl';
- size_constants := !size_constants + 4;
- max_pos_constants := min !max_pos_constants (!currpos + 1024);
- lbl'
-
-let symbol_labels =
- (Hashtbl.create 39 : (ident * Integers.Int.int, int) Hashtbl.t)
-
-let label_symbol id ofs =
- try
- Hashtbl.find symbol_labels (id, ofs)
- with Not_found ->
- let lbl' = new_label() in
- Hashtbl.add symbol_labels (id, ofs) lbl';
- size_constants := !size_constants + 4;
- max_pos_constants := min !max_pos_constants (!currpos + 4096);
- lbl'
-
-let reset_constants () =
- Hashtbl.clear float_labels;
- Hashtbl.clear float32_labels;
- Hashtbl.clear symbol_labels;
- size_constants := 0;
- max_pos_constants := max_int
-
-let emit_constants oc =
- fprintf oc " .balign 4\n";
- Hashtbl.iter
- (fun bf lbl ->
- (* Little-endian floats *)
- let bfhi = Int64.shift_right_logical bf 32
- and bflo = Int64.logand bf 0xFFFF_FFFFL in
- fprintf oc ".L%d: .word 0x%Lx, 0x%Lx\n" lbl bflo bfhi)
- float_labels;
- Hashtbl.iter
- (fun bf lbl ->
- fprintf oc ".L%d: .word 0x%lx\n" lbl bf)
- float32_labels;
- Hashtbl.iter
- (fun (id, ofs) lbl ->
- fprintf oc ".L%d: .word %a\n"
- lbl symbol_offset (id, ofs))
- symbol_labels;
- reset_constants ()
-
-(* Generate code to load the address of id + ofs in register r *)
-
-let loadsymbol oc r id ofs =
- if !Clflags.option_mthumb then begin
- fprintf oc " movw %a, #:lower16:%a\n"
- ireg r symbol_offset (id, ofs);
- fprintf oc " movt %a, #:upper16:%a\n"
- ireg r symbol_offset (id, ofs); 2
- end else begin
- let lbl = label_symbol id ofs in
- fprintf oc " ldr %a, .L%d @ %a\n"
- ireg r lbl symbol_offset (id, ofs); 1
- end
-
-(* Emit instruction sequences that set or offset a register by a constant. *)
-(* No S suffix because they are applied to SP most of the time. *)
-
-let movimm oc dst n =
- match Asmgen.decompose_int n with
- | [] -> assert false
- | hd::tl as l ->
- fprintf oc " mov %s, #%a\n" dst coqint hd;
- List.iter
- (fun n -> fprintf oc " orr %s, %s, #%a\n" dst dst coqint n)
- tl;
- List.length l
-
-let addimm oc dst src n =
- match Asmgen.decompose_int n with
- | [] -> assert false
- | hd::tl as l ->
- fprintf oc " add %s, %s, #%a\n" dst src coqint hd;
- List.iter
- (fun n -> fprintf oc " add %s, %s, #%a\n" dst dst coqint n)
- tl;
- List.length l
-
-let subimm oc dst src n =
- match Asmgen.decompose_int n with
- | [] -> assert false
- | hd::tl as l ->
- fprintf oc " sub %s, %s, #%a\n" dst src coqint hd;
- List.iter
- (fun n -> fprintf oc " sub %s, %s, #%a\n" dst dst coqint n)
- tl;
- List.length l
-
-(* Recognition of float constants appropriate for VMOV.
- "a normalized binary floating point encoding with 1 sign bit, 4
- bits of fraction and a 3-bit exponent" *)
-
-let is_immediate_float64 bits =
- let exp = (Int64.(to_int (shift_right_logical bits 52)) land 0x7FF) - 1023 in
- let mant = Int64.logand bits 0xF_FFFF_FFFF_FFFFL in
- exp >= -3 && exp <= 4 && Int64.logand mant 0xF_0000_0000_0000L = mant
-
-let is_immediate_float32 bits =
- let exp = (Int32.(to_int (shift_right_logical bits 23)) land 0xFF) - 127 in
- let mant = Int32.logand bits 0x7F_FFFFl in
- exp >= -3 && exp <= 4 && Int32.logand mant 0x78_0000l = mant
-
-(* Emit .file / .loc debugging directives *)
-
-let print_file_line oc file line =
- PrintAnnot.print_file_line oc comment file line
-
-let print_location oc loc =
- if loc <> Cutil.no_loc then print_file_line oc (fst loc) (snd loc)
-
-(* 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
- registers.
-*)
-
-(* Handling of annotations *)
-
-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)
- (int_of_string (Str.matched_group 2 txt))
- end else begin
- fprintf oc "%s annotation: " comment;
- PrintAnnot.print_annot_stmt preg "sp" oc txt targs args
- end
-
-let print_annot_val oc txt args res =
- fprintf oc "%s annotation: " comment;
- PrintAnnot.print_annot_val preg oc txt args;
- match args, res with
- | [IR src], [IR dst] ->
- if dst = src then 0 else (fprintf oc " mov %a, %a\n" ireg dst ireg src; 1)
- | [FR src], [FR dst] ->
- if dst = src then 0 else (fprintf oc " vmov.f64 %a, %a\n" freg dst freg src; 1)
- | _, _ -> assert false
-
-(* Handling of memcpy *)
-
-(* The ARM has strict alignment constraints for 2 and 4 byte accesses.
- 8-byte accesses must be 4-aligned. *)
-
-let print_builtin_memcpy_small oc sz al src dst =
- let rec copy ofs sz ninstr =
- if sz >= 8 && al >= 4 && !Clflags.option_ffpu then begin
- fprintf oc " vldr %a, [%a, #%d]\n" freg FR7 ireg src ofs;
- fprintf oc " vstr %a, [%a, #%d]\n" freg FR7 ireg dst ofs;
- copy (ofs + 8) (sz - 8) (ninstr + 2)
- end else if sz >= 4 && al >= 4 then begin
- fprintf oc " ldr %a, [%a, #%d]\n" ireg IR14 ireg src ofs;
- fprintf oc " str %a, [%a, #%d]\n" ireg IR14 ireg dst ofs;
- copy (ofs + 4) (sz - 4) (ninstr + 2)
- end else if sz >= 2 && al >= 2 then begin
- fprintf oc " ldrh %a, [%a, #%d]\n" ireg IR14 ireg src ofs;
- fprintf oc " strh %a, [%a, #%d]\n" ireg IR14 ireg dst ofs;
- copy (ofs + 2) (sz - 2) (ninstr + 2)
- end else if sz >= 1 then begin
- fprintf oc " ldrb %a, [%a, #%d]\n" ireg IR14 ireg src ofs;
- fprintf oc " strb %a, [%a, #%d]\n" ireg IR14 ireg dst ofs;
- copy (ofs + 1) (sz - 1) (ninstr + 2)
- end else
- ninstr in
- copy 0 sz 0
-
-let print_builtin_memcpy_big oc sz al src dst =
- assert (sz >= al);
- assert (sz mod al = 0);
- assert (src = IR2);
- assert (dst = IR3);
- let (load, store, chunksize) =
- if al >= 4 then ("ldr", "str", 4)
- else if al = 2 then ("ldrh", "strh", 2)
- else ("ldrb", "strb", 1) in
- let n = movimm oc "r14" (coqint_of_camlint (Int32.of_int (sz / chunksize))) in
- let lbl = new_label() in
- fprintf oc ".L%d: %s %a, [%a], #%d\n" lbl load ireg IR12 ireg src chunksize;
- fprintf oc " subs %a, %a, #1\n" ireg IR14 ireg IR14;
- fprintf oc " %s %a, [%a], #%d\n" store ireg IR12 ireg dst chunksize;
- fprintf oc " bne .L%d\n" lbl;
- n + 4
-
-let print_builtin_memcpy oc sz al args =
- let (dst, src) =
- match args with [IR d; IR s] -> (d, s) | _ -> assert false in
- fprintf oc "%s begin builtin __builtin_memcpy_aligned, size = %d, alignment = %d\n"
- comment sz al;
- let n =
- if sz <= 32
- then print_builtin_memcpy_small oc sz al src dst
- else print_builtin_memcpy_big oc sz al src dst in
- fprintf oc "%s end builtin __builtin_memcpy_aligned\n" comment; n
-
-(* Handling of volatile reads and writes *)
-
-let print_builtin_vload_common oc chunk args res =
- match chunk, args, res with
- | Mint8unsigned, [IR addr], [IR res] ->
- fprintf oc " ldrb %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mint8signed, [IR addr], [IR res] ->
- fprintf oc " ldrsb %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mint16unsigned, [IR addr], [IR res] ->
- fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mint16signed, [IR addr], [IR res] ->
- fprintf oc " ldrsh %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mint32, [IR addr], [IR res] ->
- fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg addr; 1
- | Mint64, [IR addr], [IR res1; IR res2] ->
- if addr <> res2 then begin
- fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr;
- fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr
- end else begin
- fprintf oc " ldr %a, [%a, #4]\n" ireg res1 ireg addr;
- fprintf oc " ldr %a, [%a, #0]\n" ireg res2 ireg addr
- end; 2
- | Mfloat32, [IR addr], [FR res] ->
- fprintf oc " vldr %a, [%a, #0]\n" freg_single res ireg addr; 1
- | Mfloat64, [IR addr], [FR res] ->
- fprintf oc " vldr %a, [%a, #0]\n" freg res ireg addr; 1
- | _ ->
- assert false
-
-let print_builtin_vload oc chunk args res =
- fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
- let n = print_builtin_vload_common oc chunk args res in
- fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n
-
-let print_builtin_vload_global oc chunk id ofs args res =
- fprintf oc "%s begin builtin __builtin_volatile_read\n" comment;
- let n1 = loadsymbol oc IR14 id ofs in
- let n2 = print_builtin_vload_common oc chunk [IR IR14] res in
- fprintf oc "%s end builtin __builtin_volatile_read\n" comment; n1 + n2
-
-let print_builtin_vstore_common oc chunk args =
- match chunk, args with
- | (Mint8signed | Mint8unsigned), [IR addr; IR src] ->
- fprintf oc " strb %a, [%a, #0]\n" ireg src ireg addr; 1
- | (Mint16signed | Mint16unsigned), [IR addr; IR src] ->
- fprintf oc " strh %a, [%a, #0]\n" ireg src ireg addr; 1
- | Mint32, [IR addr; IR src] ->
- fprintf oc " str %a, [%a, #0]\n" ireg src ireg addr; 1
- | Mint64, [IR addr; IR src1; IR src2] ->
- fprintf oc " str %a, [%a, #0]\n" ireg src2 ireg addr;
- fprintf oc " str %a, [%a, #4]\n" ireg src1 ireg addr; 2
- | Mfloat32, [IR addr; FR src] ->
- fprintf oc " vstr %a, [%a, #0]\n" freg_single src ireg addr; 1
- | Mfloat64, [IR addr; FR src] ->
- fprintf oc " vstr %a, [%a, #0]\n" freg src ireg addr; 1
- | _ ->
- assert false
-
-let print_builtin_vstore oc chunk args =
- fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
- let n = print_builtin_vstore_common oc chunk args in
- fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n
-
-let print_builtin_vstore_global oc chunk id ofs args =
- fprintf oc "%s begin builtin __builtin_volatile_write\n" comment;
- let n1 = loadsymbol oc IR14 id ofs in
- let n2 = print_builtin_vstore_common oc chunk (IR IR14 :: args) in
- fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n1 + n2
-
-(* Handling of varargs *)
-
-let align n a = (n + a - 1) land (-a)
-
-let rec next_arg_location ir ofs = function
- | [] ->
- Int32.of_int (ir * 4 + ofs)
- | (Tint | Tsingle | Tany32) :: l ->
- if ir < 4
- then next_arg_location (ir + 1) ofs l
- else next_arg_location ir (ofs + 4) l
- | (Tfloat | Tlong | Tany64) :: l ->
- if ir < 3
- then next_arg_location (align ir 2 + 2) ofs l
- else next_arg_location ir (align ofs 8 + 8) l
-
-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";
- let ofs =
- Int32.add
- (next_arg_location 0 0 (!current_function_sig).sig_args)
- !current_function_stacksize in
- let n = addimm oc "r14" "sp" (coqint_of_camlint ofs) in
- fprintf oc " str r14, [%a, #0]\n" ireg r;
- n + 1
-
-(* Auxiliary for 64-bit integer arithmetic built-ins. They expand to
- two instructions, one computing the low 32 bits of the result,
- followed by another computing the high 32 bits. In cases where
- the first instruction would overwrite arguments to the second
- instruction, we must go through IR14 to hold the low 32 bits of the result.
-*)
-
-let print_int64_arith oc conflict rl fn =
- if conflict then begin
- let n = fn IR14 in
- fprintf oc " mov%t %a, %a\n" thumbS ireg rl ireg IR14;
- n + 1
- end else
- fn rl
-
-(* Handling of compiler-inlined builtins *)
-
-let print_builtin_inline oc name args res =
- fprintf oc "%s begin %s\n" comment name;
- let n = match name, args, res with
- (* Integer arithmetic *)
- | ("__builtin_bswap" | "__builtin_bswap32"), [IR a1], [IR res] ->
- fprintf oc " rev %a, %a\n" ireg res ireg a1; 1
- | "__builtin_bswap16", [IR a1], [IR res] ->
- fprintf oc " rev16 %a, %a\n" ireg res ireg a1; 1
- | "__builtin_clz", [IR a1], [IR res] ->
- fprintf oc " clz %a, %a\n" ireg res ireg a1; 1
- (* Float arithmetic *)
- | "__builtin_fabs", [FR a1], [FR res] ->
- fprintf oc " vabs.f64 %a, %a\n" freg res freg a1; 1
- | "__builtin_fsqrt", [FR a1], [FR res] ->
- fprintf oc " vsqrt.f64 %a, %a\n" freg res freg a1; 1
- (* 64-bit integer arithmetic *)
- | "__builtin_negl", [IR ah; IR al], [IR rh; IR rl] ->
- print_int64_arith oc (rl = ah) rl (fun rl ->
- fprintf oc " rsbs %a, %a, #0\n" ireg rl ireg al;
- (* No "rsc" instruction in Thumb2. Emulate based on
- rsc a, b, #0 == a <- AddWithCarry(~b, 0, carry)
- == mvn a, b; adc a, a, #0 *)
- if !Clflags.option_mthumb then begin
- fprintf oc " mvn %a, %a\n" ireg rh ireg ah;
- fprintf oc " adc %a, %a, #0\n" ireg rh ireg rh; 3
- end else begin
- fprintf oc " rsc %a, %a, #0\n" ireg rh ireg ah; 2
- end)
- | "__builtin_addl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
- print_int64_arith oc (rl = ah || rl = bh) rl (fun rl ->
- fprintf oc " adds %a, %a, %a\n" ireg rl ireg al ireg bl;
- fprintf oc " adc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2)
- | "__builtin_subl", [IR ah; IR al; IR bh; IR bl], [IR rh; IR rl] ->
- print_int64_arith oc (rl = ah || rl = bh) rl (fun rl ->
- fprintf oc " subs %a, %a, %a\n" ireg rl ireg al ireg bl;
- fprintf oc " sbc %a, %a, %a\n" ireg rh ireg ah ireg bh; 2)
- | "__builtin_mull", [IR a; IR b], [IR rh; IR rl] ->
- fprintf oc " umull %a, %a, %a, %a\n" ireg rl ireg rh ireg a ireg b; 1
- (* Memory accesses *)
- | "__builtin_read16_reversed", [IR a1], [IR res] ->
- fprintf oc " ldrh %a, [%a, #0]\n" ireg res ireg a1;
- fprintf oc " rev16 %a, %a\n" ireg res ireg res; 2
- | "__builtin_read32_reversed", [IR a1], [IR res] ->
- fprintf oc " ldr %a, [%a, #0]\n" ireg res ireg a1;
- fprintf oc " rev %a, %a\n" ireg res ireg res; 2
- | "__builtin_write16_reversed", [IR a1; IR a2], _ ->
- fprintf oc " rev16 %a, %a\n" ireg IR14 ireg a2;
- fprintf oc " strh %a, [%a, #0]\n" ireg IR14 ireg a1; 2
- | "__builtin_write32_reversed", [IR a1; IR a2], _ ->
- fprintf oc " rev %a, %a\n" ireg IR14 ireg a2;
- fprintf oc " str %a, [%a, #0]\n" ireg IR14 ireg a1; 2
- (* Synchronization *)
- | "__builtin_membar", [], _ ->
- 0
- | "__builtin_dmb", [], _ ->
- fprintf oc " dmb\n"; 1
- | "__builtin_dsb", [], _ ->
- fprintf oc " dsb\n"; 1
- | "__builtin_isb", [], _ ->
- fprintf oc " isb\n"; 1
-
- (* Vararg stuff *)
- | "__builtin_va_start", [IR a], _ ->
- print_builtin_va_start oc a
- (* Catch-all *)
- | _ ->
- invalid_arg ("unrecognized builtin " ^ name)
- in
- fprintf oc "%s end %s\n" comment name;
- n
-
-(* Fixing up calling conventions *)
-
-type direction = Incoming | Outgoing
-
-module FixupEABI = struct
-
- let ireg_param = function
- | 0 -> IR0 | 1 -> IR1 | 2 -> IR2 | 3 -> IR3 | _ -> assert false
-
- let freg_param = function
- | 0 -> FR0 | 1 -> FR1 | 2 -> FR2 | 3 -> FR3 | _ -> assert false
-
- let fixup_double oc dir f i1 i2 =
- match dir with
- | Incoming -> (* f <- (i1, i2) *)
- fprintf oc " vmov %a, %a, %a\n" freg f ireg i1 ireg i2
- | Outgoing -> (* (i1, i2) <- f *)
- fprintf oc " vmov %a, %a, %a\n" ireg i1 ireg i2 freg f
-
- let fixup_single oc dir f i =
- match dir with
- | Incoming -> (* f <- i *)
- fprintf oc " vmov %a, %a\n" freg_single f ireg i
- | Outgoing -> (* i <- f *)
- fprintf oc " vmov %a, %a\n" ireg i freg_single f
-
- let fixup_conventions oc dir tyl =
- let rec fixup i tyl =
- if i >= 4 then 0 else
- match tyl with
- | [] -> 0
- | (Tint | Tany32) :: tyl' ->
- fixup (i+1) tyl'
- | Tlong :: tyl' ->
- fixup (((i + 1) land (-2)) + 2) tyl'
- | (Tfloat | Tany64) :: tyl' ->
- let i = (i + 1) land (-2) in
- if i >= 4 then 0 else begin
- fixup_double oc dir (freg_param i) (ireg_param i) (ireg_param (i+1));
- 1 + fixup (i+2) tyl'
- end
- | Tsingle :: tyl' ->
- fixup_single oc dir (freg_param i) (ireg_param i);
- 1 + fixup (i+1) tyl'
- in fixup 0 tyl
-
- let fixup_arguments oc dir sg =
- fixup_conventions oc dir sg.sig_args
-
- let fixup_result oc dir sg =
- fixup_conventions oc dir (proj_sig_res sg :: [])
-
-end
-
-module FixupHF = struct
-
- type fsize = Single | Double
-
- let rec find_single used pos =
- if pos >= Array.length used then pos
- else if used.(pos) then find_single used (pos + 1)
- else begin used.(pos) <- true; pos end
-
- let rec find_double used pos =
- if pos + 1 >= Array.length used then pos
- else if used.(pos) || used.(pos + 1) then find_double used (pos + 2)
- else begin used.(pos) <- true; used.(pos + 1) <- true; pos / 2 end
-
- let rec fixup_actions used fr tyl =
- match tyl with
- | [] -> []
- | (Tint | Tlong | Tany32) :: tyl' -> fixup_actions used fr tyl'
- | (Tfloat | Tany64) :: tyl' ->
- if fr >= 8 then [] else begin
- let dr = find_double used 0 in
- assert (dr < 8);
- (fr, Double, dr) :: fixup_actions used (fr + 1) tyl'
- end
- | Tsingle :: tyl' ->
- if fr >= 8 then [] else begin
- let sr = find_single used 0 in
- assert (sr < 16);
- (fr, Single, sr) :: fixup_actions used (fr + 1) tyl'
- end
-
- let rec fixup_outgoing oc = function
- | [] -> 0
- | (fr, Double, dr) :: act ->
- if fr = dr then fixup_outgoing oc act else begin
- fprintf oc " vmov.f64 d%d, d%d\n" dr fr;
- 1 + fixup_outgoing oc act
- end
- | (fr, Single, sr) :: act ->
- fprintf oc " vmov.f32 s%d, s%d\n" sr (2*fr);
- 1 + fixup_outgoing oc act
-
- let rec fixup_incoming oc = function
- | [] -> 0
- | (fr, Double, dr) :: act ->
- let n = fixup_incoming oc act in
- if fr = dr then n else begin
- fprintf oc " vmov.f64 d%d, d%d\n" fr dr;
- 1 + n
- end
- | (fr, Single, sr) :: act ->
- let n = fixup_incoming oc act in
- if fr = sr then n else begin
- fprintf oc " vmov.f32 s%d, s%d\n" (2*fr) sr;
- 1 + n
- end
-
- let fixup_arguments oc dir sg =
- if sg.sig_cc.cc_vararg then
- FixupEABI.fixup_arguments oc dir sg
- else begin
- let act = fixup_actions (Array.make 16 false) 0 sg.sig_args in
- match dir with
- | Outgoing -> fixup_outgoing oc act
- | Incoming -> fixup_incoming oc act
- end
-
- let fixup_result oc dir sg =
- if sg.sig_cc.cc_vararg then
- FixupEABI.fixup_result oc dir sg
- else
- 0
-end
-
-let (fixup_arguments, fixup_result) =
- match Opt.float_abi with
- | Soft -> (FixupEABI.fixup_arguments, FixupEABI.fixup_result)
- | Hard -> (FixupHF.fixup_arguments, FixupHF.fixup_result)
-
-(* Printing of instructions *)
-
-let shift_op oc = function
- | SOimm n -> fprintf oc "#%a" coqint n
- | SOreg r -> ireg oc r
- | SOlsl(r, n) -> fprintf oc "%a, lsl #%a" ireg r coqint n
- | SOlsr(r, n) -> fprintf oc "%a, lsr #%a" ireg r coqint n
- | SOasr(r, n) -> fprintf oc "%a, asr #%a" ireg r coqint n
- | SOror(r, n) -> fprintf oc "%a, ror #%a" ireg r coqint n
-
-let print_instruction oc = function
- (* Core instructions *)
- | Padd(r1, r2, so) ->
- fprintf oc " add%s %a, %a, %a\n"
- (if !Clflags.option_mthumb && r2 <> IR14 then "s" else "")
- ireg r1 ireg r2 shift_op so; 1
- | Pand(r1, r2, so) ->
- fprintf oc " and%t %a, %a, %a\n"
- thumbS ireg r1 ireg r2 shift_op so; 1
- | Pasr(r1, r2, r3) ->
- fprintf oc " asr%t %a, %a, %a\n"
- thumbS ireg r1 ireg r2 ireg r3; 1
- | Pb lbl ->
- fprintf oc " b %a\n" print_label lbl; 1
- | Pbc(bit, lbl) ->
- fprintf oc " b%s %a\n" (condition_name bit) print_label lbl; 1
- | Pbsymb(id, sg) ->
- let n = fixup_arguments oc Outgoing sg in
- fprintf oc " b %a\n" symbol id;
- n + 1
- | Pbreg(r, sg) ->
- let n =
- if r = IR14
- then fixup_result oc Outgoing sg
- else fixup_arguments oc Outgoing sg in
- fprintf oc " bx %a\n" ireg r;
- n + 1
- | Pblsymb(id, sg) ->
- let n1 = fixup_arguments oc Outgoing sg in
- fprintf oc " bl %a\n" symbol id;
- let n2 = fixup_result oc Incoming sg in
- n1 + 1 + n2
- | Pblreg(r, sg) ->
- let n1 = fixup_arguments oc Outgoing sg in
- fprintf oc " blx %a\n" ireg r;
- let n2 = fixup_result oc Incoming sg in
- n1 + 1 + n2
- | Pbic(r1, r2, so) ->
- fprintf oc " bic%t %a, %a, %a\n"
- thumbS ireg r1 ireg r2 shift_op so; 1
- | Pcmp(r1, so) ->
- fprintf oc " cmp %a, %a\n" ireg r1 shift_op so; 1
- | Peor(r1, r2, so) ->
- fprintf oc " eor%t %a, %a, %a\n"
- thumbS ireg r1 ireg r2 shift_op so; 1
- | Pldr(r1, r2, sa) | Pldr_a(r1, r2, sa) ->
- fprintf oc " ldr %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
- | Pldrb(r1, r2, sa) ->
- fprintf oc " ldrb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
- | Pldrh(r1, r2, sa) ->
- fprintf oc " ldrh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
- | Pldrsb(r1, r2, sa) ->
- fprintf oc " ldrsb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
- | Pldrsh(r1, r2, sa) ->
- fprintf oc " ldrsh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
- | Plsl(r1, r2, r3) ->
- fprintf oc " lsl%t %a, %a, %a\n"
- thumbS ireg r1 ireg r2 ireg r3; 1
- | Plsr(r1, r2, r3) ->
- fprintf oc " lsr%t %a, %a, %a\n"
- thumbS ireg r1 ireg r2 ireg r3; 1
- | Pmla(r1, r2, r3, r4) ->
- fprintf oc " mla %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1
- | Pmov(r1, so) ->
- fprintf oc " mov%t %a, %a\n" thumbS ireg r1 shift_op so; 1
- | Pmovw(r1, n) ->
- fprintf oc " movw %a, #%a\n" ireg r1 coqint n; 1
- | Pmovt(r1, n) ->
- fprintf oc " movt %a, #%a\n" ireg r1 coqint n; 1
- | Pmul(r1, r2, r3) ->
- fprintf oc " mul %a, %a, %a\n" ireg r1 ireg r2 ireg r3; 1
- | Pmvn(r1, so) ->
- fprintf oc " mvn%t %a, %a\n" thumbS ireg r1 shift_op so; 1
- | Porr(r1, r2, so) ->
- fprintf oc " orr%t %a, %a, %a\n"
- thumbS ireg r1 ireg r2 shift_op so; 1
- | Prsb(r1, r2, so) ->
- fprintf oc " rsb%t %a, %a, %a\n"
- thumbS ireg r1 ireg r2 shift_op so; 1
- | 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 -> cfi_rel_offset oc "lr" (camlint_of_coqint n)
- | _ -> ()
- end;
- 1
- | Pstrb(r1, r2, sa) ->
- fprintf oc " strb %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
- | Pstrh(r1, r2, sa) ->
- fprintf oc " strh %a, [%a, %a]\n" ireg r1 ireg r2 shift_op sa; 1
- | Psdiv ->
- if Opt.hardware_idiv then begin
- fprintf oc " sdiv r0, r0, r1\n"; 1
- end else begin
- fprintf oc " bl __aeabi_idiv\n"; 1
- end
- | Psbfx(r1, r2, lsb, sz) ->
- fprintf oc " sbfx %a, %a, #%a, #%a\n" ireg r1 ireg r2 coqint lsb coqint sz; 1
- | Psmull(r1, r2, r3, r4) ->
- fprintf oc " smull %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1
- | Psub(r1, r2, so) ->
- fprintf oc " sub%t %a, %a, %a\n"
- thumbS ireg r1 ireg r2 shift_op so; 1
- | Pudiv ->
- if Opt.hardware_idiv then begin
- fprintf oc " udiv r0, r0, r1\n"; 1
- end else begin
- fprintf oc " bl __aeabi_uidiv\n"; 1
- end
- | Pumull(r1, r2, r3, r4) ->
- fprintf oc " umull %a, %a, %a, %a\n" ireg r1 ireg r2 ireg r3 ireg r4; 1
- (* Floating-point VFD instructions *)
- | Pfcpyd(r1, r2) ->
- fprintf oc " vmov.f64 %a, %a\n" freg r1 freg r2; 1
- | Pfabsd(r1, r2) ->
- fprintf oc " vabs.f64 %a, %a\n" freg r1 freg r2; 1
- | Pfnegd(r1, r2) ->
- fprintf oc " vneg.f64 %a, %a\n" freg r1 freg r2; 1
- | Pfaddd(r1, r2, r3) ->
- fprintf oc " vadd.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1
- | Pfdivd(r1, r2, r3) ->
- fprintf oc " vdiv.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1
- | Pfmuld(r1, r2, r3) ->
- fprintf oc " vmul.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1
- | Pfsubd(r1, r2, r3) ->
- fprintf oc " vsub.f64 %a, %a, %a\n" freg r1 freg r2 freg r3; 1
- | Pflid(r1, f) ->
- let f = camlint64_of_coqint(Floats.Float.to_bits f) in
- if Opt.vfpv3 && is_immediate_float64 f then begin
- fprintf oc " vmov.f64 %a, #%F\n"
- freg r1 (Int64.float_of_bits f); 1
- (* immediate floats have at most 4 bits of fraction, so they
- should print exactly with OCaml's F decimal format. *)
- end else if !literals_in_code then begin
- let lbl = label_float f in
- fprintf oc " vldr %a, .L%d @ %.12g\n"
- freg r1 lbl (Int64.float_of_bits f); 1
- end else begin
- let lbl = label_float f in
- fprintf oc " movw r14, #:lower16:.L%d\n" lbl;
- fprintf oc " movt r14, #:upper16:.L%d\n" lbl;
- fprintf oc " vldr %a, [r14, #0] @ %.12g\n"
- freg r1 (Int64.float_of_bits f); 3
- end
- | Pfcmpd(r1, r2) ->
- fprintf oc " vcmp.f64 %a, %a\n" freg r1 freg r2;
- fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2
- | Pfcmpzd(r1) ->
- fprintf oc " vcmp.f64 %a, #0\n" freg r1;
- fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2
- | Pfsitod(r1, r2) ->
- fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2;
- fprintf oc " vcvt.f64.s32 %a, %a\n" freg r1 freg_single r1; 2
- | Pfuitod(r1, r2) ->
- fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2;
- fprintf oc " vcvt.f64.u32 %a, %a\n" freg r1 freg_single r1; 2
- | Pftosizd(r1, r2) ->
- fprintf oc " vcvt.s32.f64 %a, %a\n" freg_single FR6 freg r2;
- fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6; 2
- | Pftouizd(r1, r2) ->
- fprintf oc " vcvt.u32.f64 %a, %a\n" freg_single FR6 freg r2;
- fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6; 2
- | Pfabss(r1, r2) ->
- fprintf oc " vabs.f32 %a, %a\n" freg_single r1 freg_single r2; 1
- | Pfnegs(r1, r2) ->
- fprintf oc " vneg.f32 %a, %a\n" freg_single r1 freg_single r2; 1
- | Pfadds(r1, r2, r3) ->
- fprintf oc " vadd.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
- | Pfdivs(r1, r2, r3) ->
- fprintf oc " vdiv.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
- | Pfmuls(r1, r2, r3) ->
- fprintf oc " vmul.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
- | Pfsubs(r1, r2, r3) ->
- fprintf oc " vsub.f32 %a, %a, %a\n" freg_single r1 freg_single r2 freg_single r3; 1
- | Pflis(r1, f) ->
- let f = camlint_of_coqint(Floats.Float32.to_bits f) in
- if Opt.vfpv3 && is_immediate_float32 f then begin
- fprintf oc " vmov.f32 %a, #%F\n"
- freg_single r1 (Int32.float_of_bits f); 1
- (* immediate floats have at most 4 bits of fraction, so they
- should print exactly with OCaml's F decimal format. *)
- end else if !literals_in_code then begin
- let lbl = label_float32 f in
- fprintf oc " vldr %a, .L%d @ %.12g\n"
- freg_single r1 lbl (Int32.float_of_bits f); 1
- end else begin
- fprintf oc " movw r14, #%ld\n" (Int32.logand f 0xFFFFl);
- fprintf oc " movt r14, #%ld\n" (Int32.shift_right_logical f 16);
- fprintf oc " vmov %a, r14 @ %.12g\n"
- freg_single r1 (Int32.float_of_bits f); 3
- end
- | Pfcmps(r1, r2) ->
- fprintf oc " vcmp.f32 %a, %a\n" freg_single r1 freg_single r2;
- fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2
- | Pfcmpzs(r1) ->
- fprintf oc " vcmp.f32 %a, #0\n" freg_single r1;
- fprintf oc " vmrs APSR_nzcv, FPSCR\n"; 2
- | Pfsitos(r1, r2) ->
- fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2;
- fprintf oc " vcvt.f32.s32 %a, %a\n" freg_single r1 freg_single r1; 2
- | Pfuitos(r1, r2) ->
- fprintf oc " vmov %a, %a\n" freg_single r1 ireg r2;
- fprintf oc " vcvt.f32.u32 %a, %a\n" freg_single r1 freg_single r1; 2
- | Pftosizs(r1, r2) ->
- fprintf oc " vcvt.s32.f32 %a, %a\n" freg_single FR6 freg_single r2;
- fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6; 2
- | Pftouizs(r1, r2) ->
- fprintf oc " vcvt.u32.f32 %a, %a\n" freg_single FR6 freg_single r2;
- fprintf oc " vmov %a, %a\n" ireg r1 freg_single FR6; 2
- | Pfcvtsd(r1, r2) ->
- fprintf oc " vcvt.f32.f64 %a, %a\n" freg_single r1 freg r2; 1
- | Pfcvtds(r1, r2) ->
- fprintf oc " vcvt.f64.f32 %a, %a\n" freg r1 freg_single r2; 1
- | Pfldd(r1, r2, n) | Pfldd_a(r1, r2, n) ->
- fprintf oc " vldr %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1
- | Pflds(r1, r2, n) ->
- fprintf oc " vldr %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1
- | Pfstd(r1, r2, n) | Pfstd_a(r1, r2, n) ->
- fprintf oc " vstr %a, [%a, #%a]\n" freg r1 ireg r2 coqint n; 1
- | Pfsts(r1, r2, n) ->
- fprintf oc " vstr %a, [%a, #%a]\n" freg_single r1 ireg r2 coqint n; 1
- (* Pseudo-instructions *)
- | Pallocframe(sz, ofs) ->
- fprintf oc " mov r12, sp\n";
- if (!current_function_sig).sig_cc.cc_vararg then begin
- fprintf oc " push {r0, r1, r2, r3}\n";
- cfi_adjust oc 16l
- end;
- let sz' = camlint_of_coqint sz in
- let ninstr = subimm oc "sp" "sp" sz in
- 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)
- | Pfreeframe(sz, ofs) ->
- let sz =
- if (!current_function_sig).sig_cc.cc_vararg
- then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz))
- else sz in
- if Asmgen.is_immed_arith sz
- then fprintf oc " add sp, sp, #%a\n" coqint sz
- else fprintf oc " ldr sp, [sp, #%a]\n" coqint ofs; 1
- | Plabel lbl ->
- fprintf oc "%a:\n" print_label lbl; 0
- | Ploadsymbol(r1, id, ofs) ->
- loadsymbol oc r1 id ofs
- | Pmovite(cond, r1, ifso, ifnot) ->
- fprintf oc " ite %s\n" (condition_name cond);
- fprintf oc " mov%s %a, %a\n"
- (condition_name cond) ireg r1 shift_op ifso;
- fprintf oc " mov%s %a, %a\n"
- (neg_condition_name cond) ireg r1 shift_op ifnot; 2
- | Pbtbl(r, tbl) ->
- if !Clflags.option_mthumb then begin
- let lbl = new_label() in
- fprintf oc " adr r14, .L%d\n" lbl;
- fprintf oc " add r14, r14, %a, lsl #2\n" ireg r;
- fprintf oc " mov pc, r14\n";
- fprintf oc ".L%d:\n" lbl;
- List.iter
- (fun l -> fprintf oc " b.w %a\n" print_label l)
- tbl;
- 3 + List.length tbl
- end else begin
- fprintf oc " add pc, pc, %a, lsl #2\n" ireg r;
- fprintf oc " nop\n";
- List.iter
- (fun l -> fprintf oc " b %a\n" print_label l)
- tbl;
- 2 + List.length tbl
- end
- | Pbuiltin(ef, args, res) ->
- begin match ef with
- | EF_builtin(name, sg) ->
- print_builtin_inline oc (extern_atom name) args res
- | EF_vload chunk ->
- print_builtin_vload oc chunk args res
- | EF_vstore chunk ->
- print_builtin_vstore oc chunk args
- | EF_vload_global(chunk, id, ofs) ->
- print_builtin_vload_global oc chunk id ofs args res
- | EF_vstore_global(chunk, id, ofs) ->
- print_builtin_vstore_global oc chunk id ofs args
- | EF_memcpy(sz, al) ->
- print_builtin_memcpy oc (Int32.to_int (camlint_of_coqint sz))
- (Int32.to_int (camlint_of_coqint al)) args
- | EF_annot_val(txt, targ) ->
- print_annot_val oc (extern_atom txt) args res
- | EF_inline_asm txt ->
- fprintf oc "%s begin inline assembly\n" comment;
- fprintf oc " %s\n" (extern_atom txt);
- fprintf oc "%s end inline assembly\n" comment;
- 5 (* hoping this is an upper bound... *)
- | _ ->
- assert false
- end
- | Pannot(ef, args) ->
- begin match ef with
- | EF_annot(txt, targs) ->
- print_annot_stmt oc (extern_atom txt) targs args; 0
- | _ ->
- assert false
- end
-
-let no_fallthrough = function
- | Pb _ -> true
- | Pbsymb _ -> true
- | Pbreg _ -> true
- | _ -> false
-
-let rec print_instructions oc instrs =
- match instrs with
- | [] -> ()
- | i :: il ->
- let n = print_instruction oc i in
- currpos := !currpos + n * 4;
- let d = distance_to_emit_constants() in
- if d < 256 && no_fallthrough i then
- emit_constants oc
- else if d < 16 then begin
- let lbl = new_label() in
- fprintf oc " b .L%d\n" lbl;
- emit_constants oc;
- fprintf oc ".L%d:\n" lbl
- end;
- print_instructions oc il
-
-let print_function oc name fn =
- Hashtbl.clear current_function_labels;
- reset_constants();
- current_function_sig := fn.fn_sig;
- currpos := 0;
- let (text, lit) =
- match C2C.atom_sections name with
- | t :: l :: _ -> (t, l)
- | _ -> (Section_text, Section_literal) in
- section oc text;
- let alignment =
- match !Clflags.option_falignfunctions with Some n -> n | None -> 4 in
- fprintf oc " .balign %d\n" alignment;
- if not (C2C.atom_is_static name) then
- fprintf oc " .global %a\n" symbol name;
- if !Clflags.option_mthumb then
- fprintf oc " .thumb_func\n";
- fprintf oc "%a:\n" symbol name;
- print_location oc (C2C.atom_location name);
- 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;
- cfi_endproc oc;
- print_fun_info oc name;
- if not !literals_in_code && !size_constants > 0 then begin
- section oc lit;
- emit_constants oc
- end
-
-(* Data *)
-
-let print_init oc = function
- | Init_int8 n ->
- fprintf oc " .byte %ld\n" (camlint_of_coqint n)
- | Init_int16 n ->
- fprintf oc " .short %ld\n" (camlint_of_coqint n)
- | Init_int32 n ->
- fprintf oc " .word %ld\n" (camlint_of_coqint n)
- | Init_int64 n ->
- fprintf oc " .quad %Ld\n" (camlint64_of_coqint n)
- | Init_float32 n ->
- fprintf oc " .word 0x%lx %s %.15g \n" (camlint_of_coqint (Floats.Float32.to_bits n))
- comment (camlfloat_of_coqfloat n)
- | Init_float64 n ->
- fprintf oc " .quad %Ld %s %.18g\n" (camlint64_of_coqint (Floats.Float.to_bits n))
- comment (camlfloat_of_coqfloat n)
- | Init_space n ->
- if Z.gt n Z.zero then
- fprintf oc " .space %s\n" (Z.to_string n)
- | Init_addrof(symb, ofs) ->
- fprintf oc " .word %a\n" symbol_offset (symb, ofs)
-
-let print_init_data oc name id =
- if Str.string_match PrintCsyntax.re_string_literal (extern_atom name) 0
- && List.for_all (function Init_int8 _ -> true | _ -> false) id
- then
- fprintf oc " .ascii \"%s\"\n" (PrintCsyntax.string_of_init id)
- else
- List.iter (print_init oc) id
-
-let print_var oc name v =
- match v.gvar_init with
- | [] -> ()
- | _ ->
- let sec =
- match C2C.atom_sections name with
- | [s] -> s
- | _ -> Section_data true
- and align =
- match C2C.atom_alignof name with
- | Some a -> a
- | None -> 8 (* 8-alignment is a safe default *)
- in
- let name_sec =
- name_of_section sec in
- if name_sec <> "COMM" then begin
- fprintf oc " %s\n" name_sec;
- fprintf oc " .balign %d\n" align;
- if not (C2C.atom_is_static name) then
- fprintf oc " .global %a\n" symbol name;
- fprintf oc "%a:\n" symbol name;
- print_init_data oc name v.gvar_init;
- print_var_info oc name
- end else begin
- let sz =
- match v.gvar_init with [Init_space sz] -> sz | _ -> assert false in
- if C2C.atom_is_static name then
- fprintf oc " .local %a\n" symbol name;
- fprintf oc " .comm %a, %s, %d\n"
- symbol name
- (Z.to_string sz)
- align
- end
-
-let print_globdef oc (name, gdef) =
- match gdef with
- | Gfun(Internal f) -> print_function oc name f
- | Gfun(External ef) -> ()
- | Gvar v -> print_var oc name v
-
- end)
-
-let print_program oc p =
- let module Opt : PRINTER_OPTIONS = struct
-
- let vfpv3 = Configuration.model >= "armv7"
-
- let float_abi = match Configuration.abi with
- | "eabi" -> Soft
- | "hardfloat" -> Hard
- | _ -> assert false
-
- let hardware_idiv =
- match Configuration.model with
- | "armv7r" | "armv7m" -> !Clflags.option_mthumb
- | _ -> false
-
-
- end in
- let module Printer = AsmPrinter(Opt) in
- PrintAnnot.reset_filenames();
- PrintAnnot.print_version_and_options oc Printer.comment;
- fprintf oc " .syntax unified\n";
- fprintf oc " .arch %s\n"
- (match Configuration.model with
- | "armv6" -> "armv6"
- | "armv7a" -> "armv7-a"
- | "armv7r" -> "armv7-r"
- | "armv7m" -> "armv7-m"
- | _ -> "armv7");
- fprintf oc " .fpu %s\n"
- (if Opt.vfpv3 then "vfpv3-d16" else "vfpv2");
- fprintf oc " .%s\n" (if !Clflags.option_mthumb then "thumb" else "arm");
- List.iter (Printer.print_globdef oc) p.prog_defs;
- PrintAnnot.close_filenames()
-
generated by cgit (git 2.34.1) at 2024-07-01 03:16:02 +0000