diff options
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/AsmToJSON.mli | 13 | ||||
| -rw-r--r-- | arm/Asmexpand.ml | 9 | ||||
| -rw-r--r-- | arm/TargetPrinter.ml | 61 |
3 files changed, 19 insertions, 64 deletions
diff --git a/arm/AsmToJSON.mli b/arm/AsmToJSON.mli new file mode 100644 index 00000000..20bcba5e --- /dev/null +++ b/arm/AsmToJSON.mli @@ -0,0 +1,13 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* AbsInt Angewandte Informatik GmbH. All rights reserved. This file *) +(* is distributed under the terms of the INRIA Non-Commercial *) +(* License Agreement. *) +(* *) +(* *********************************************************************) + +val p_program: out_channel -> (Asm.coq_function AST.fundef, 'a) AST.program -> unit diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 47269f8f..79f06991 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -16,7 +16,6 @@ open Asm open Asmexpandaux -open Asmgen open AST open Camlcoq open Integers @@ -268,11 +267,11 @@ let rec next_arg_location ir ofs = function else next_arg_location 4 (align ofs 8 + 8) l let expand_builtin_va_start r = - if not !current_function.fn_sig.sig_cc.cc_vararg then + if not (is_current_function_variadic ()) then invalid_arg "Fatal error: va_start used in non-vararg function"; let ofs = Int32.add - (next_arg_location 0 0 !current_function.fn_sig.sig_args) + (next_arg_location 0 0 (get_current_function_args ())) !PrintAsmaux.current_function_stacksize in expand_addimm IR14 IR13 (coqint_of_camlint ofs); emit (Pstr (IR14,r,SOimm _0)) @@ -364,7 +363,7 @@ let expand_instruction instr = match instr with | Pallocframe (sz, ofs) -> emit (Pmov (IR12,SOreg IR13)); - if (!current_function).fn_sig.sig_cc.cc_vararg then begin + if (is_current_function_variadic ()) then begin emit (Ppush [IR0;IR1;IR2;IR3]); emit (Pcfi_adjust _16); end; @@ -374,7 +373,7 @@ let expand_instruction instr = PrintAsmaux.current_function_stacksize := camlint_of_coqint sz | Pfreeframe (sz, ofs) -> let sz = - if (!current_function).fn_sig.sig_cc.cc_vararg + if (is_current_function_variadic ()) then coqint_of_camlint (Int32.add 16l (camlint_of_coqint sz)) else sz in if Asmgen.is_immed_arith sz diff --git a/arm/TargetPrinter.ml b/arm/TargetPrinter.ml index 3ca90ce9..bfe11555 100644 --- a/arm/TargetPrinter.ml +++ b/arm/TargetPrinter.ml @@ -13,11 +13,10 @@ (* Printing ARM assembly code in asm syntax *) open Printf -open Datatypes +open !Datatypes open Camlcoq open Sections open AST -open Memdata open Asm open PrintAsmaux open Fileinfo @@ -68,12 +67,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = | 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" @@ -130,7 +123,7 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = orr rsb sub (but not sp - imm) - On the other hand, "mov rd, rs" and "mov rd, #imm" have shorter + On the other hand, "mov rd, rs" and "mov rd, #imm" have shorter encodings if they do not have the "S" flag. Moreover, the "S" flag is not supported if rd or rs is sp. @@ -257,39 +250,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = 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 *) @@ -310,23 +270,6 @@ module Target (Opt: PRINTER_OPTIONS) : TARGET = let print_file_line oc file line = 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) - -(* 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 %a, %a\n" ireg rl ireg IR14; - n + 1 - end else - fn rl (* Fixing up calling conventions *) |