From 7e4e9417b6bfaf9f6a0f36e2fc040c12f8530889 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 1 Jan 2014 16:43:37 +0000 Subject: Experimental support for , the GCC way. Works on IA32. To be tested on PowerPC and ARM. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2394 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/CBuiltins.ml | 5 +- arm/PrintAsm.ml | 98 +++++++++++++++++++----- cfrontend/C2C.ml | 87 +++++++++++++++++++-- cparser/Elab.ml | 12 ++- ia32/CBuiltins.ml | 6 +- ia32/PrintAsm.ml | 23 +++++- powerpc/CBuiltins.ml | 7 +- powerpc/PrintAsm.ml | 57 +++++++++++++- runtime/Makefile | 3 +- runtime/arm/vararg.S | 83 ++++++++++++++++++++ runtime/ia32/vararg.S | 69 +++++++++++++++++ runtime/powerpc/vararg.s | 156 +++++++++++++++++++++++++++++++++++++ test/regression/Makefile | 5 +- test/regression/Results/varargs1 | 1 + test/regression/Results/varargs2 | 11 +++ test/regression/varargs1.c | 7 ++ test/regression/varargs2.c | 161 +++++++++++++++++++++++++++++++++++++++ 17 files changed, 755 insertions(+), 36 deletions(-) create mode 100644 runtime/arm/vararg.S create mode 100644 runtime/ia32/vararg.S create mode 100644 runtime/powerpc/vararg.s create mode 100644 test/regression/Results/varargs1 create mode 100644 test/regression/Results/varargs2 create mode 100644 test/regression/varargs2.c diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml index ad739f1..a8583c8 100644 --- a/arm/CBuiltins.ml +++ b/arm/CBuiltins.ml @@ -18,7 +18,9 @@ open C let builtins = { - Builtins.typedefs = []; + Builtins.typedefs = [ + "__builtin_va_list", TPtr(TVoid [], []) + ]; Builtins.functions = [ (* Integer arithmetic *) "__builtin_bswap", @@ -44,3 +46,4 @@ let builtins = { ] } +let size_va_list = 4 diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 7007467..81c8c38 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -102,6 +102,36 @@ let condition_name = function | TCgt -> "gt" | TCle -> "le" +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" 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" 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" dst dst coqint n) + tl; + List.length l + (* Names of sections *) let name_of_section_ELF = function @@ -276,22 +306,13 @@ let print_builtin_memcpy_big oc sz al src dst = if al >= 4 then ("ldr", "str", 4) else if al = 2 then ("ldrh", "strh", 2) else ("ldrb", "strb", 1) in - begin match Asmgen.decompose_int - (coqint_of_camlint (Int32.of_int (sz / chunksize))) with - | [] -> assert false - | hd::tl -> - fprintf oc " mov %a, #%a\n" ireg IR14 coqint hd; - List.iter - (fun n -> - fprintf oc " orr %a, %a, #%a\n" ireg IR14 ireg IR14 coqint n) - tl - end; + 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; - 8 + n + 4 let print_builtin_memcpy oc sz al args = let (dst, src) = @@ -377,6 +398,37 @@ let print_builtin_vstore_global oc chunk id ofs args = let n = print_builtin_vstore_common oc chunk (IR IR14 :: args) in fprintf oc "%s end builtin __builtin_volatile_write\n" comment; n + 1 +(* Handling of varargs *) + +let current_function_stacksize = ref 0l +let current_function_sig = + ref { sig_args = []; sig_res = None; sig_cc = cc_default } + +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) :: l -> + if ir < 4 + then next_arg_location (ir + 1) ofs l + else next_arg_location ir (ofs + 4) l + | (Tfloat | Tlong) :: 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); + fprintf oc " str r14, [%a, #0]\n" ireg r; + n + 1 + (* Handling of compiler-inlined builtins *) let print_builtin_inline oc name args res = @@ -442,6 +494,9 @@ let print_builtin_inline oc name args res = | "__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 + (* Vararg stuff *) + | "__builtin_va_start", [IR a], _ -> + print_builtin_va_start oc a (* Catch-all *) | _ -> invalid_arg ("unrecognized builtin " ^ name) @@ -659,16 +714,21 @@ let print_instruction oc = function (* Pseudo-instructions *) | Pallocframe(sz, ofs) -> fprintf oc " mov r12, sp\n"; - let ninstr = ref 0 in - List.iter - (fun n -> - fprintf oc " sub sp, sp, #%a\n" coqint n; - incr ninstr) - (Asmgen.decompose_int sz); - cfi_adjust oc (camlint_of_coqint sz); + if (!current_function_sig).sig_cc.cc_vararg then begin + fprintf oc " push {r0, r1, r2, r3}\n"; + cfi_adjust oc 16 + end; + let sz' = camlint_of_coqint sz in + let ninstr = subimm "sp" "sp" sz in + cfi_adjust oc sz'; fprintf oc " str r12, [sp, #%a]\n" coqint ofs; - 2 + !ninstr + current_function_stacksize := rsz; + 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 diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index ba599da..5f99e48 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -70,10 +70,7 @@ let warning msg = (** ** The builtin environment *) let builtins_generic = { - typedefs = [ - (* keeps GCC-specific headers happy, harmless for others *) - "__builtin_va_list", C.TPtr(C.TVoid [], []) - ]; + typedefs = []; functions = [ (* Floating-point absolute value *) "__builtin_fabs", @@ -94,6 +91,41 @@ let builtins_generic = { "__builtin_annot_intval", (TInt(IInt, []), [TPtr(TInt(IChar, [AConst]), []); TInt(IInt, [])], + false); + (* Variable arguments *) +(* va_start(ap,n) + (preprocessing) --> __builtin_va_start(ap, arg) + (elaboration) --> __builtin_va_start(ap) *) + "__builtin_va_start", + (TVoid [], + [TPtr(TVoid [], [])], + false); +(* va_arg(ap, ty) + (preprocessing) --> __builtin_va_arg(ap, ty) + (parsing) --> __builtin_va_arg(ap, sizeof(ty)) *) + "__builtin_va_arg", + (TVoid [], + [TPtr(TVoid [], []); TInt(IUInt, [])], + false); + "__builtin_va_copy", + (TVoid [], + [TPtr(TVoid [], []); TPtr(TVoid [], [])], + false); + "__builtin_va_end", + (TVoid [], + [TPtr(TVoid [], [])], + false); + "__compcert_va_int32", + (TInt(IUInt, []), + [TPtr(TVoid [], [])], + false); + "__compcert_va_int64", + (TInt(IULongLong, []), + [TPtr(TVoid [], [])], + false); + "__compcert_va_int64", + (TFloat(FDouble, []), + [TPtr(TVoid [], [])], false) ] } @@ -165,6 +197,31 @@ a constant)"; Integers.Int.one in | _ -> assert false +(** ** Translation of [va_arg] for variadic functions. *) + +let eaddrof e = Eaddrof(e, Tpointer(typeof e, noattr)) + +let make_builtin_va_arg env ty e = + let (helper, ty_ret) = + match ty with + | Tint _ | Tpointer _ | Tcomp_ptr _ -> + ("__compcert_va_int32", Tint(I32, Unsigned, noattr)) + | Tlong _ -> + ("__compcert_va_int64", Tlong(Unsigned, noattr)) + | Tfloat _ -> + ("__compcert_va_float64", Tfloat(F64, noattr)) + | _ -> + unsupported "va_arg at this type"; + ("", Tvoid) + in + Ecast + (Ecall(Evar (intern_string helper, + Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, + cc_default)), + Econs(eaddrof e, Enil), + ty_ret), + ty) + (** ** Translation functions *) (** Constants *) @@ -555,6 +612,24 @@ let rec convertExpr env e = | C.ECall({edesc = C.EVar {name = "__builtin_fabs"}}, [arg]) -> Eunop(Oabsfloat, convertExpr env arg, ty) + | C.ECall({edesc = C.EVar {name = "__builtin_va_start"}} as fn, [arg]) -> + Ecall(convertExpr env fn, Econs(eaddrof(convertExpr env arg), Enil), ty) + + | C.ECall({edesc = C.EVar {name = "__builtin_va_arg"}}, [arg1; arg2]) -> + make_builtin_va_arg env ty (convertExpr env arg1) + + | C.ECall({edesc = C.EVar {name = "__builtin_va_end"}}, _) -> + Ecast (ezero, Tvoid) + + | C.ECall({edesc = C.EVar {name = "__builtin_va_copy"}}, [arg1; arg2]) -> + let dst = convertExpr env arg1 in + let src = convertExpr env arg2 in + Ebuiltin(EF_memcpy(Z.of_uint CBuiltins.size_va_list, Z.of_uint 4), + Tcons(Tpointer(Tvoid, noattr), + Tcons(Tpointer(Tvoid, noattr), Tnil)), + Econs(eaddrof dst, Econs(eaddrof src, Enil)), + Tvoid) + | C.ECall({edesc = C.EVar {name = "printf"}}, args) when !Clflags.option_interp -> let targs = @@ -769,6 +844,8 @@ let convertFundef loc env fd = (** External function declaration *) +let re_builtin = Str.regexp "__builtin_" + let convertFundecl env (sto, id, ty, optinit) = let (args, res, cconv) = match convertTyp env ty with @@ -779,7 +856,7 @@ let convertFundecl env (sto, id, ty, optinit) = let ef = if id.name = "malloc" then EF_malloc else if id.name = "free" then EF_free else - if List.mem_assoc id.name builtins.functions + if Str.string_match re_builtin id.name 0 then EF_builtin(id', sg) else EF_external(id', sg) in (id', Gfun(External(ef, args, res, cconv))) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index e1276d6..b99c9af 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -828,20 +828,24 @@ let elab_expr loc env a = (* Hack to treat vararg.h functions the GCC way. Helps with testing. va_start(ap,n) (preprocessing) --> __builtin_va_start(ap, arg) - (elaboration) --> __builtin_va_start(ap, &arg) + (elaboration) --> __builtin_va_start(ap) va_arg(ap, ty) (preprocessing) --> __builtin_va_arg(ap, ty) (parsing) --> __builtin_va_arg(ap, sizeof(ty)) *) | CALL((VARIABLE "__builtin_va_start" as a1), [a2; a3]) -> - let b1 = elab a1 and b2 = elab a2 and b3 = elab a3 in - { edesc = ECall(b1, [b2; {edesc = EUnop(Oaddrof, b3); - etyp = TPtr(b3.etyp, [])}]); + let b1 = elab a1 and b2 = elab a2 and _b3 = elab a3 in + { edesc = ECall(b1, [b2]); etyp = TVoid [] } | CALL((VARIABLE "__builtin_va_arg" as a1), [a2; (TYPE_SIZEOF _) as a3]) -> let b1 = elab a1 and b2 = elab a2 and b3 = elab a3 in let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in + let ty' = default_argument_conversion env ty in + if not (compatible_types env ty ty') then + warning "'%a' is promoted to '%a' when passed through '...'.@ You should pass '%a', not '%a', to 'va_arg'" + Cprint.typ ty Cprint.typ ty' + Cprint.typ ty' Cprint.typ ty; { edesc = ECall(b1, [b2; b3]); etyp = ty } | CALL(a1, al) -> diff --git a/ia32/CBuiltins.ml b/ia32/CBuiltins.ml index cbd5998..b594c65 100644 --- a/ia32/CBuiltins.ml +++ b/ia32/CBuiltins.ml @@ -18,7 +18,9 @@ open C let builtins = { - Builtins.typedefs = []; + Builtins.typedefs = [ + "__builtin_va_list", TPtr(TVoid [], []) + ]; Builtins.functions = [ (* Integer arithmetic *) "__builtin_bswap", @@ -45,3 +47,5 @@ let builtins = { (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false); ] } + +let size_va_list = 4 diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index 1e65ee8..0a666cb 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -419,6 +419,22 @@ let print_builtin_vstore_global oc chunk id ofs args = (Addrmode(None, None, Coq_inr(id,ofs))) args EAX; fprintf oc "%s end builtin __builtin_volatile_write\n" comment +(* Handling of varargs *) + +let current_function_stacksize = ref 0l +let current_function_sig = + ref { sig_args = []; sig_res = None; sig_cc = cc_default } + +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 (add !current_function_stacksize 4l) + (mul 4l (Z.to_int32 (Conventions1.size_arguments + !current_function_sig)))) in + fprintf oc " movl %%esp, 0(%a)\n" ireg r; + fprintf oc " addl $%ld, 0(%a)\n" ofs ireg r + (* Handling of compiler-inlined builtins *) let print_builtin_inline oc name args res = @@ -495,6 +511,9 @@ let print_builtin_inline oc name args res = fprintf oc " movl %a, %a\n" ireg a2 ireg tmp; fprintf oc " bswap %a\n" ireg tmp; fprintf oc " movl %a, 0(%a)\n" ireg tmp ireg a1 + (* Vararg stuff *) + | "__builtin_va_start", [IR a], _ -> + print_builtin_va_start oc a (* Catch-all *) | _ -> invalid_arg ("unrecognized builtin " ^ name) @@ -708,7 +727,8 @@ let print_instruction oc = function fprintf oc " subl $%ld, %%esp\n" sz; cfi_adjust oc sz; fprintf oc " leal %ld(%%esp), %%edx\n" (Int32.add sz 4l); - fprintf oc " movl %%edx, %ld(%%esp)\n" ofs_link + fprintf oc " movl %%edx, %ld(%%esp)\n" ofs_link; + current_function_stacksize := sz | Pfreeframe(sz, ofs_ra, ofs_link) -> let sz = sp_adjustment sz in fprintf oc " addl $%ld, %%esp\n" sz @@ -757,6 +777,7 @@ let print_function oc name fn = Hashtbl.clear current_function_labels; float_literals := []; jumptables := []; + current_function_sig := fn.fn_sig; let (text, lit, jmptbl) = match C2C.atom_sections name with | [t;l;j] -> (t, l, j) diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 060e2b7..8405c4f 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -18,7 +18,10 @@ open C let builtins = { - Builtins.typedefs = []; + Builtins.typedefs = [ + "__builtin_va_list", + TArray(TInt(IUInt, []), Some 3L, []) + ]; Builtins.functions = [ (* Integer arithmetic *) "__builtin_mulhw", @@ -84,3 +87,5 @@ let builtins = { (TVoid [], [], false) ] } + +let size_va_list = 12 diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 830a502..4aa88e8 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -501,6 +501,44 @@ let print_builtin_vstore_global oc chunk id ofs args = end; fprintf oc "%s end builtin __builtin_volatile_write\n" comment +(* Handling of varargs *) + +let current_function_sig = + ref { sig_args = []; sig_res = None; sig_cc = cc_default } + +let align n a = (n + a - 1) land (-a) + +let rec next_arg_locations ir fr ofs = function + | [] -> + (ir, fr, ofs) + | Tint :: l -> + if ir < 8 + then next_arg_locations (ir + 1) fr ofs l + else next_arg_locations ir fr (ofs + 4) l + | (Tfloat | Tsingle) :: l -> + if fr < 8 + then next_arg_locations ir (fr + 1) ofs l + else next_arg_locations ir fr (align ofs 8 + 8) l + | Tlong :: l -> + if ir < 7 + then next_arg_locations (align ir 2 + 2) fr ofs l + else next_arg_locations ir fr (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 (ir, fr, ofs) = + next_arg_locations 0 0 0 (!current_function_sig).sig_args in + fprintf oc " li %a, %d\n" ireg GPR0 ir; + fprintf oc " stb %a, 0(%a)\n" ireg GPR0 ireg r; + fprintf oc " li %a, %d\n" ireg GPR0 fr; + fprintf oc " stb %a, 1(%a)\n" ireg GPR0 ireg r; + fprintf oc " lwz %a, 0(%a)\n" ireg GPR0 ireg GPR1; + fprintf oc " addi %a, %a, -96\n" ireg GPR0 ireg GPR0; + fprintf oc " stw %a, 8(%a)\n" ireg GPR0 ireg r; + fprintf oc " addi %a, %a, %d\n" ireg GPR0 ireg GPR0 (96 + 8 + ofs); + fprintf oc " stw %a, 4(%a)\n" ireg GPR0 ireg r + (* Handling of compiler-inlined builtins *) let print_builtin_inline oc name args res = @@ -605,6 +643,9 @@ let print_builtin_inline oc name args res = fprintf oc " isync\n" | "__builtin_trap", [], _ -> fprintf oc " trap\n" + (* Vararg stuff *) + | "__builtin_va_start", [IR a], _ -> + print_builtin_va_start oc a (* Catch-all *) | _ -> invalid_arg ("unrecognized builtin " ^ name) @@ -651,6 +692,10 @@ let print_instruction oc tbl pc fallthrough = function let sz = camlint_of_coqint sz and ofs = camlint_of_coqint ofs in assert (ofs = 0l); + let sz = + if (!current_function_sig).sig_cc.cc_vararg + then Int32.add sz 96l + else sz in let adj = Int32.neg sz in if adj >= -0x8000l then fprintf oc " stwu %a, %ld(%a)\n" ireg GPR1 adj ireg GPR1 @@ -659,7 +704,12 @@ let print_instruction oc tbl pc fallthrough = function fprintf oc " ori %a, %a, %ld\n" ireg GPR0 ireg GPR0 (Int32.logand adj 0xFFFFl); fprintf oc " stwux %a, %a, %a\n" ireg GPR1 ireg GPR1 ireg GPR0 end; - cfi_adjust oc sz + cfi_adjust oc sz; + if (!current_function_sig).sig_cc.cc_vararg then begin + fprintf oc " mflr %a\n" ireg GPR0; + fprintf oc " blr __compcert_va_saveregs\n"; + fprintf oc " mtlr %a\n" ireg GPR0 + end | Pand_(r1, r2, r3) -> fprintf oc " and. %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Pandc(r1, r2, r3) -> @@ -742,6 +792,10 @@ let print_instruction oc tbl pc fallthrough = function | Pfreeframe(sz, ofs) -> let sz = camlint_of_coqint sz and ofs = camlint_of_coqint ofs in + let sz = + if (!current_function_sig).sig_cc.cc_vararg + then Int32.add sz 96l + else sz in if sz < 0x8000l then fprintf oc " addi %a, %a, %ld\n" ireg GPR1 ireg GPR1 sz else @@ -1018,6 +1072,7 @@ let print_function oc name fn = Hashtbl.clear current_function_labels; float_literals := []; jumptables := []; + current_function_sig := fn.fn_sig; let (text, lit, jmptbl) = match C2C.atom_sections name with | [t;l;j] -> (t, l, j) diff --git a/runtime/Makefile b/runtime/Makefile index 668e365..0cdfd3b 100644 --- a/runtime/Makefile +++ b/runtime/Makefile @@ -4,7 +4,8 @@ CFLAGS=-O1 -g -Wall INCLUDES= OBJS=i64_dtos.o i64_dtou.o i64_sar.o i64_sdiv.o i64_shl.o \ i64_shr.o i64_smod.o i64_stod.o i64_stof.o \ - i64_udivmod.o i64_udiv.o i64_umod.o i64_utod.o i64_utof.o + i64_udivmod.o i64_udiv.o i64_umod.o i64_utod.o i64_utof.o \ + vararg.o LIB=libcompcert.a ifeq ($(strip $(HAS_RUNTIME_LIB)),true) diff --git a/runtime/arm/vararg.S b/runtime/arm/vararg.S new file mode 100644 index 0000000..8d431d3 --- /dev/null +++ b/runtime/arm/vararg.S @@ -0,0 +1,83 @@ +@ ***************************************************************** +@ +@ The Compcert verified compiler +@ +@ Xavier Leroy, INRIA Paris-Rocquencourt +@ +@ Copyright (c) 2013 Institut National de Recherche en Informatique et +@ en Automatique. +@ +@ Redistribution and use in source and binary forms, with or without +@ modification, are permitted provided that the following conditions are met: +@ * Redistributions of source code must retain the above copyright +@ notice, this list of conditions and the following disclaimer. +@ * Redistributions in binary form must reproduce the above copyright +@ notice, this list of conditions and the following disclaimer in the +@ documentation and/or other materials provided with the distribution. +@ * Neither the name of the nor the +@ names of its contributors may be used to endorse or promote products +@ derived from this software without specific prior written permission. +@ +@ THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +@ "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +@ LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +@ A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +@ EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +@ PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +@ PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +@ LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +@ NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +@ SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +@ +@ ********************************************************************* + +@ Helper functions for variadic functions . ARM version + + .text + +@ typedef void * va_list; +@ unsigned int __compcert_va_int32(va_list * ap); +@ unsigned long long __compcert_va_int64(va_list * ap); +@ double __compcert_va_float64(va_list * ap); + + .global __compcert_va_int32 +__compcert_va_int32: + @ r0 = ap parameter + ldr r1, [r0, #0] @ r1 = pointer to next argument + add r1, r1, #4 @ advance ap by 4 + str r1, [r0, #0] + ldr r0, [r1, #-4] @ load next argument and return it in r0 + bx lr + .type __compcert_va_int32, %function + .size __compcert_va_int32, . - __compcert_va_int32 + + .global __compcert_va_int64 +__compcert_va_int64: + @ r0 = ap parameter + ldr r1, [r0, #0] @ r1 = pointer to next argument + add r1, r1, #15 @ 8-align and advance by 8 + bic r1, r1, #7 + str r1, [r0, #0] @ update ap + ldr r0, [r1, #-8] @ load next argument and return it in r0,r1 + ldr r1, [r1, #-4] + bx lr + .type __compcert_va_int64, %function + .size __compcert_va_int64, . - __compcert_va_int64 + + .global __compcert_va_float64 +__compcert_va_float64: + @ r0 = ap parameter + ldr r1, [r0, #0] @ r1 = pointer to next argument + add r1, r1, #15 @ 8-align and advance by 8 + bic r1, r1, #7 + str r1, [r0, #0] @ update ap +#ifdef VARIANT_hardfloat + fldd d0, [r1, #-8] @ load next argument and return it in d0 +#else + ldr r0, [r1, #-8] @ load next argument and return it in r0,r1 + ldr r1, [r1, #-4] +#endif + bx lr + .type __compcert_va_float64, %function + .size __compcert_va_float64, . - __compcert_va_float64 diff --git a/runtime/ia32/vararg.S b/runtime/ia32/vararg.S new file mode 100644 index 0000000..ec55a45 --- /dev/null +++ b/runtime/ia32/vararg.S @@ -0,0 +1,69 @@ +// ***************************************************************** +// +// The Compcert verified compiler +// +// Xavier Leroy, INRIA Paris-Rocquencourt +// +// Copyright (c) 2013 Institut National de Recherche en Informatique et +// en Automatique. +// +// Redistribution and use in source and binary forms, with or without +// modification, are permitted provided that the following conditions are met: +// * Redistributions of source code must retain the above copyright +// notice, this list of conditions and the following disclaimer. +// * Redistributions in binary form must reproduce the above copyright +// notice, this list of conditions and the following disclaimer in the +// documentation and/or other materials provided with the distribution. +// * Neither the name of the nor the +// names of its contributors may be used to endorse or promote products +// derived from this software without specific prior written permission. +// +// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +// EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +// PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +// PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +// LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +// NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +// SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +// +// ********************************************************************* + +// Helper functions for variadic functions . IA32 version + +#include "sysdeps.h" + +// typedef void * va_list; +// unsigned int __compcert_va_int32(va_list * ap); +// unsigned long long __compcert_va_int64(va_list * ap); +// double __compcert_va_float64(va_list * ap); + +FUNCTION(__compcert_va_int32) + movl 4(%esp), %ecx // %ecx = ap parameter + movl 0(%ecx), %edx // %edx = current argument pointer + movl 0(%edx), %eax // load the int32 value there + addl $4, %edx // increment argument pointer by 4 + movl %edx, 0(%ecx) + ret +ENDFUNCTION(__compcert_va_int32) + +FUNCTION(__compcert_va_int64) + movl 4(%esp), %ecx // %ecx = ap parameter + movl 0(%ecx), %edx // %edx = current argument pointer + movl 0(%edx), %eax // load the int64 value there + movl 4(%edx), %edx + addl $8, 0(%ecx) // increment argument pointer by 8 + ret +ENDFUNCTION(__compcert_va_int64) + +FUNCTION(__compcert_va_float64) + movl 4(%esp), %ecx // %ecx = ap parameter + movl 0(%ecx), %edx // %edx = current argument pointer + fldl 0(%edx) // load the float64 value there + addl $8, %edx // increment argument pointer by 8 + movl %edx, 0(%ecx) + ret +ENDFUNCTION(__compcert_va_float64) diff --git a/runtime/powerpc/vararg.s b/runtime/powerpc/vararg.s new file mode 100644 index 0000000..98de6c8 --- /dev/null +++ b/runtime/powerpc/vararg.s @@ -0,0 +1,156 @@ +# ***************************************************************** +# +# The Compcert verified compiler +# +# Xavier Leroy, INRIA Paris-Rocquencourt +# +# Copyright (c) 2013 Institut National de Recherche en Informatique et +# en Automatique. +# +# Redistribution and use in source and binary forms, with or without +# modification, are permitted provided that the following conditions are met: +# * Redistributions of source code must retain the above copyright +# notice, this list of conditions and the following disclaimer. +# * Redistributions in binary form must reproduce the above copyright +# notice, this list of conditions and the following disclaimer in the +# documentation and/or other materials provided with the distribution. +# * Neither the name of the nor the +# names of its contributors may be used to endorse or promote products +# derived from this software without specific prior written permission. +# +# THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +# "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +# LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +# A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +# EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +# PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +# LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +# NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +# SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. +# +# ********************************************************************* + +# Helper functions for variadic functions . IA32 version + +# typedef struct { +# unsigned char ireg; // index of next integer register +# unsigned char freg; // index of next FP register +# char * stk; // pointer to next argument in stack +# struct { +# int iregs[8]; +# double fregs[8]; +# } * regs; // pointer to saved register area +# } va_list[1]; +# +# unsigned int __compcert_va_int32(va_list * ap); +# unsigned long long __compcert_va_int64(va_list * ap); +# double __compcert_va_float64(va_list * ap); + + .text + + .balign 16 + .globl __compcert_va_int32 +__compcert_va_int32: + # r3 = ap = address of va_list structure + lbz r4, 0(r3) # r4 = ap->ireg = next integer register + cmplwi r4, 8 + bge 1f + # Next argument was passed in an integer register + lwz r5, 8(r3) # r5 = ap->regs = base of saved register area + rlwinm r6, r4, 2, 0, 29 # r6 = r4 * 4 + lwzx r3, r5, r6 # load argument in r3 + addi r4, r4, 1 # increment ap->ireg + stb r4, 0(r3) + blr + # Next argument was passed on stack +1: lwz r5, 4(r3) # r5 = ap->stk = next argument passed on stack + lwz r3, 0(r5) # load argument in r3 + addi r5, r5, 4 # advance ap->stk by 4 + stw r5, 4(r3) + blr + .type __compcert_va_int32, @function + .size __compcert_va_int32, .-__compcert_va_int32 + + .balign 16 + .globl __compcert_va_int64 +__compcert_va_int64: + # r3 = ap = address of va_list structure + lbz r4, 0(r3) # r4 = ap->ireg = next integer register + cmplwi r4, 7 + bge 1f + # Next argument was passed in two consecutive integer register + lwz r5, 8(r3) # r5 = ap->regs = base of saved register area + addi r4, r4, 3 # round r4 up to an even number and add 2 + rlwinm r4, r4, 0, 0, 30 + rlwinm r6, r4, 2, 0, 29 # r6 = r4 * 4 + add r5, r5, r6 # r5 = address of argument + 8 + stb r4, 8(r3) # update ap->ireg + lwz r3, -8(r5) # load argument in r3:r4 + lwz r4, -4(r5) + blr + # Next argument was passed on stack +1: lwz r5, 4(r3) # r5 = ap->stk = next argument passed on stack + li r4, 8 + stb r4, 8(r3) # set ap->ireg = 8 so that no ireg is left + addi r5, r5, 15 # round r5 to a multiple of 8 and add 8 + rlwinm r5, r5, 0, 0, 28 + lwz r3, -8(r5) # load argument in r3:r4 + lwz r4, -4(r5) + stw r5, 4(r3) # update ap->stk + blr + .type __compcert_va_int64, @function + .size __compcert_va_int64, .-__compcert_va_int64 + + .balign 16 + .globl __compcert_va_float64 +__compcert_va_float64: + # r3 = ap = address of va_list structure + lbz r4, 1(r3) # r4 = ap->freg = next float register + cmplwi r4, 8 + bge 1f + # Next argument was passed in a FP register + lwz r5, 8(r3) # r5 = ap->regs = base of saved register area + rlwinm r6, r4, 3, 0, 28 # r6 = r4 * 8 + add r5, r5, r6 + lfd f1, 32(r5) # load argument in f1 + addi r4, r4, 1 # increment ap->freg + stb r4, 1(r3) + blr + # Next argument was passed on stack +1: lwz r5, 4(r3) # r5 = ap->stk = next argument passed on stack + addi r5, r5, 15 # round r5 to a multiple of 8 and add 8 + rlwinm r5, r5, 0, 0, 28 + lfd f1, -8(r5) # load argument in f1 + stw r5, 4(r3) # update ap->stk + blr + .type __compcert_va_float64, @function + .size __compcert_va_float64, .-__compcert_va_int64 + +# Save integer and FP registers at beginning of vararg function + + .balign 16 + .globl __compcert_va_saveregs +__compcert_va_saveregs: + lwz r11, 0(r1) # r11 point to top of our frame + stwu r3, -96(r11) # register save area is 96 bytes below + stw r4, 4(r11) + stw r5, 8(r11) + stw r6, 12(r11) + stw r7, 16(r11) + stw r8, 20(r11) + stw r9, 24(r11) + stw r10, 28(r11) + bf 6, 1f # don't save FP regs if CR6 bit is clear + stfd f1, 32(r11) + stfd f2, 40(r11) + stfd f3, 48(r11) + stfd f4, 56(r11) + stfd f5, 64(r11) + stfd f6, 72(r11) + stfd f7, 80(r11) + stfd f8, 88(r11) +1: blr + .type __compcert_va_saveregs, @function + .size __compcert_va_saveregs, .-__compcert_va_saveregs diff --git a/test/regression/Makefile b/test/regression/Makefile index 8dc7678..c653a01 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -17,7 +17,8 @@ TESTS=int32 int64 floats floats-basics \ TESTS_COMP=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \ bitfields5 bitfields6 bitfields7 bitfields8 \ - builtins-$(ARCH) packedstruct1 packedstruct2 alignas + builtins-$(ARCH) packedstruct1 packedstruct2 alignas \ + varargs1 varargs2 # Can run, both in compiled mode and in interpreter mode, # but produce processor-dependent results, so no reference output in Results @@ -31,7 +32,7 @@ EXTRAS=annot1 commaprec expr2 expr3 expr4 extern1 funct2 funptr1 init1 \ struct4 struct5 struct6 struct9 struct10 types1 seqops # Test known to fail -FAILURES=funct1 varargs1 +FAILURES=funct1 all: $(TESTS:%=%.compcert) $(TESTS_COMP:%=%.compcert) $(TESTS_DIFF:%=%.compcert) $(EXTRAS:%=%.s) diff --git a/test/regression/Results/varargs1 b/test/regression/Results/varargs1 new file mode 100644 index 0000000..00c4b5d --- /dev/null +++ b/test/regression/Results/varargs1 @@ -0,0 +1 @@ +Sum is 55 diff --git a/test/regression/Results/varargs2 b/test/regression/Results/varargs2 new file mode 100644 index 0000000..35728be --- /dev/null +++ b/test/regression/Results/varargs2 @@ -0,0 +1,11 @@ +An int: 42 +A long long: 123456789012345 +A string: Hello world +A double: 3.141592654 +A char: x and A string: Hello, world! and An int: 42 and A long: 123456789012345 and A double: 3.141592654 and A float: 2.718281746 +Twice: -1 1.23 +Twice: -1 1.23 +With va_copy: -1 1.23 +With va_copy: -1 1.23 +With extra args: A char: x and A string: Hello, world! and An int: 42 and A long: 123456789012345 and A double: 3.141592654 and A float: 2.718281746 +va_list compatibility: A char: x and A string: Hello, world! and An int: 42 and A long: 123456789012345 and A double: 3.141592654 and A float: 2.718281746 diff --git a/test/regression/varargs1.c b/test/regression/varargs1.c index 99dba39..2e45d0f 100644 --- a/test/regression/varargs1.c +++ b/test/regression/varargs1.c @@ -1,4 +1,5 @@ #include +#include int sum_v(int n, va_list ap) { @@ -16,3 +17,9 @@ int sum_l(int n, ...) va_end(ap); return s; } + +int main() +{ + printf("Sum is %d\n", sum_l(10, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10)); + return 0; +} diff --git a/test/regression/varargs2.c b/test/regression/varargs2.c new file mode 100644 index 0000000..e2eefce --- /dev/null +++ b/test/regression/varargs2.c @@ -0,0 +1,161 @@ +#include +#include + +void minivprintf(const char * fmt, va_list ap) +{ + char c; + + while (1) { + switch(c = *fmt++) { + case 0: + return; + case '%': + switch (*fmt++) { + case '%': + putchar('%'); + break; + case 'c': + printf("%c", (char) va_arg(ap, int)); + break; + case 's': + printf("%s", va_arg(ap, char *)); + break; + case 'd': + printf("%d", va_arg(ap, int)); + break; + case 'l': + printf("%lld", va_arg(ap, long long)); + break; + case 'e': + printf("%.10g", va_arg(ap, double)); + break; + case 'f': + printf("%.10g", (float) va_arg(ap, double)); + break; + default: + puts(""); + return; + } + break; + default: + putchar(c); + break; + } + } +} + +void miniprintf(const char * fmt, ...) +{ + va_list va; + va_start(va, fmt); + minivprintf(fmt, va); + va_end(va); +} + +/* Run va_start twice */ + +void miniprintf2(const char * fmt, ...) +{ + va_list va; + va_start(va, fmt); + minivprintf(fmt, va); + va_end(va); + va_start(va, fmt); + minivprintf(fmt, va); + va_end(va); +} + +/* Use va_copy */ + +void miniprintf3(const char * fmt, ...) +{ + va_list va, va2; + va_start(va, fmt); + va_copy(va2, va); + minivprintf(fmt, va); + minivprintf(fmt, va2); + va_end(va); + va_end(va2); +} + +/* Add some dummy arguments to force overflow into stack-passed params + (mostly relevant for ARM and PowerPC) */ + +void miniprintf_extra(int i1, int i2, int i3, int i4, + int i5, int i6, int i7, int i8, + double f1, double f2, double f3, double f4, + float f5, float f6, float f7, float f8, + const char * fmt, ...) +{ + va_list va; + va_start(va, fmt); + minivprintf(fmt, va); + va_end(va); +} + +/* Test va_list compatibility with the C library */ + +void printf_compat(const char * fmt, ...) +{ + va_list va; + va_start(va, fmt); + vprintf(fmt, va); + va_end(va); +} + +/* The test harness */ + +int main() +{ + miniprintf("An int: %d\n", 42); + miniprintf("A long long: %l\n", 123456789012345LL); + miniprintf("A string: %s\n", "Hello world"); + miniprintf("A double: %e\n", 3.141592654); + miniprintf("A char: %c and " + "A string: %s and " + "An int: %d and " + "A long: %l and " + "A double: %e and " + "A float: %f\n", + 'x', + "Hello, world!", + 42, + 123456789012345LL, + 3.141592654, + 2.71828182); + miniprintf2("Twice: %d %e\n", -1, 1.23); + miniprintf3("With va_copy: %d %e\n", -1, 1.23); + miniprintf_extra(0, 1, 2, 3, 4, 5, 6, 7, + 0.0, 0.1, 0.2, 0.3, 0.4, 0.5, 0.6, 0.7, + "With extra args: " + "A char: %c and " + "A string: %s and " + "An int: %d and " + "A long: %l and " + "A double: %e and " + "A float: %f\n", + 'x', + "Hello, world!", + 42, + 123456789012345LL, + 3.141592654, + 2.71828182); + printf_compat("va_list compatibility: " + "A char: %c and " + "A string: %s and " + "An int: %d and " + "A long: %lld and " + "A double: %.10g and " + "A float: %.10g\n", + 'x', + "Hello, world!", + 42, + 123456789012345LL, + 3.141592654, + (float) 2.71828182); + return 0; +} + + + + -- cgit v1.2.3