summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--arm/CBuiltins.ml5
-rw-r--r--arm/PrintAsm.ml98
-rw-r--r--cfrontend/C2C.ml87
-rw-r--r--cparser/Elab.ml12
-rw-r--r--ia32/CBuiltins.ml6
-rw-r--r--ia32/PrintAsm.ml23
-rw-r--r--powerpc/CBuiltins.ml7
-rw-r--r--powerpc/PrintAsm.ml57
-rw-r--r--runtime/Makefile3
-rw-r--r--runtime/arm/vararg.S83
-rw-r--r--runtime/ia32/vararg.S69
-rw-r--r--runtime/powerpc/vararg.s156
-rw-r--r--test/regression/Makefile5
-rw-r--r--test/regression/Results/varargs11
-rw-r--r--test/regression/Results/varargs211
-rw-r--r--test/regression/varargs1.c7
-rw-r--r--test/regression/varargs2.c161
17 files changed, 755 insertions, 36 deletions
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 <organization> 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 <COPYRIGHT
+@ HOLDER> 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 <stdarg.h>. 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 <organization> 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 <COPYRIGHT
+// HOLDER> 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 <stdarg.h>. 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 <organization> 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 <COPYRIGHT
+# HOLDER> 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 <stdarg.h>. 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 <stdarg.h>
+#include <stdio.h>
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 <stdarg.h>
+#include <stdio.h>
+
+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("<bad format>");
+ 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;
+}
+
+
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 09:07:41 +0000