diff options
| -rw-r--r-- | arm/Asmexpand.ml | 8 | ||||
| -rw-r--r-- | backend/Asmexpandaux.ml | 9 | ||||
| -rw-r--r-- | backend/Asmexpandaux.mli | 36 | ||||
| -rw-r--r-- | ia32/Asmexpand.ml | 4 | ||||
| -rw-r--r-- | powerpc/Asmexpand.ml | 8 |
5 files changed, 55 insertions, 10 deletions
diff --git a/arm/Asmexpand.ml b/arm/Asmexpand.ml index 3283bb09..e114ab28 100644 --- a/arm/Asmexpand.ml +++ b/arm/Asmexpand.ml @@ -267,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)) @@ -363,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; @@ -373,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/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml index 3d1dd754..13aa71d2 100644 --- a/backend/Asmexpandaux.ml +++ b/backend/Asmexpandaux.ml @@ -50,6 +50,15 @@ let new_label () = let set_current_function f = current_function := f; next_label := None; current_code := [] +let get_current_function_args () = + (!current_function).fn_sig.sig_args + +let is_current_function_variadic () = + (!current_function).fn_sig.sig_cc.cc_vararg + +let get_current_function_sig () = + (!current_function).fn_sig + let get_current_function () = let c = List.rev !current_code in let fn = !current_function in diff --git a/backend/Asmexpandaux.mli b/backend/Asmexpandaux.mli new file mode 100644 index 00000000..797eb10c --- /dev/null +++ b/backend/Asmexpandaux.mli @@ -0,0 +1,36 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +open Asm +open AST +open BinNums + +(** Auxiliary functions for builtin expansion *) + +val emit: instruction -> unit + (* Emit an instruction *) +val new_label: unit -> label + (* Compute a fresh label *) +val is_current_function_variadic: unit -> bool + (* Test wether the current function is a variadic function *) +val get_current_function_args: unit -> typ list + (* Get the types of the current function arguments *) +val get_current_function_sig: unit -> signature + (* Get the signature of the current function *) +val set_current_function: coq_function -> unit + (* Set the current function *) +val get_current_function: unit -> coq_function + (* Get the current function *) +val expand_debug: positive -> int -> (preg -> int) -> (instruction -> unit) -> instruction list -> unit + (* Expand builtin debug function. Takes the function id, the register number of the stackpointer, a + function to get the dwarf mapping of varibale names and for the expansion of simple instructions *) diff --git a/ia32/Asmexpand.ml b/ia32/Asmexpand.ml index 3a3548f9..4f2bb937 100644 --- a/ia32/Asmexpand.ml +++ b/ia32/Asmexpand.ml @@ -200,12 +200,12 @@ let expand_builtin_vstore chunk args = (* Handling of varargs *) 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 = coqint_of_camlint Int32.(add (add !PrintAsmaux.current_function_stacksize 4l) (mul 4l (Z.to_int32 (Conventions1.size_arguments - !current_function.fn_sig)))) in + (get_current_function_sig ()))))) in emit (Pmov_mr (linear_addr r _0, ESP)); emit (Padd_mi (linear_addr r _0, ofs)) diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml index 86b74ab1..870b20b3 100644 --- a/powerpc/Asmexpand.ml +++ b/powerpc/Asmexpand.ml @@ -308,10 +308,10 @@ let rec next_arg_locations ir fr ofs = function else next_arg_locations ir fr (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 (ir, fr, ofs) = - next_arg_locations 0 0 0 (!current_function).fn_sig.sig_args in + next_arg_locations 0 0 0 (get_current_function_args ()) in emit_loadimm GPR0 (Z.of_uint ir); emit (Pstb(GPR0, Cint _0, r)); emit_loadimm GPR0 (Z.of_uint fr); @@ -642,7 +642,7 @@ let num_crbit = function let expand_instruction instr = match instr with | Pallocframe(sz, ofs,retofs) -> - let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in + let variadic = is_current_function_variadic () in let sz = camlint_of_coqint sz in assert (ofs = _0); let sz = if variadic then Int32.add sz 96l else sz in @@ -667,7 +667,7 @@ let expand_instruction instr = set_cr6 sg; emit instr | Pfreeframe(sz, ofs) -> - let variadic = (!current_function).fn_sig.sig_cc.cc_vararg in + let variadic = is_current_function_variadic () in let sz = camlint_of_coqint sz in let sz = if variadic then Int32.add sz 96l else sz in if sz < 0x8000l && sz >= 0l then |