diff options
| -rw-r--r-- | cfrontend/C2C.ml | 50 | ||||
| -rw-r--r-- | runtime/arm/vararg.S | 12 | ||||
| -rw-r--r-- | test/regression/Results/varargs2 | 4 | ||||
| -rw-r--r-- | test/regression/varargs2.c | 16 |
4 files changed, 67 insertions, 15 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml index 2b9a54a4..4cb4ded6 100644 --- a/cfrontend/C2C.ml +++ b/cfrontend/C2C.ml @@ -199,6 +199,10 @@ let builtins_generic = { (TFloat(FDouble, []), [TPtr(TVoid [], [])], false); + "__compcert_va_composite", + (TPtr(TVoid [], []), + [TPtr(TVoid [], []); TInt(IUInt, [])], + false); (* Helper functions for int64 arithmetic *) "__i64_dtos", (TInt(ILongLong, []), @@ -381,26 +385,46 @@ let va_list_ptr e = | Evalof(e', _) -> Eaddrof(e', Tpointer(typeof e, noattr)) | _ -> error "bad use of a va_list object"; e -let make_builtin_va_arg env ty e = - let (helper, ty_ret) = - match ty with - | Tint _ | Tpointer _ -> - ("__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 +let make_builtin_va_arg_by_val helper ty ty_ret arg = let ty_fun = Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), ty_ret, cc_default) in Ecast (Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), - Econs(va_list_ptr e, Enil), + Econs(va_list_ptr arg, Enil), ty_ret), ty) +let make_builtin_va_arg_by_ref helper ty arg = + let ty_fun = + Tfunction(Tcons(Tpointer(Tvoid, noattr), Tnil), + Tpointer(Tvoid, noattr), cc_default) in + let ty_ptr = + Tpointer(ty, noattr) in + let call = + Ecall(Evalof(Evar(intern_string helper, ty_fun), ty_fun), + Econs(va_list_ptr arg, + Econs(Esizeof(ty, Tint(I32, Unsigned, noattr)), Enil)), + Tpointer(Tvoid, noattr)) in + Evalof(Ederef(Ecast(call, ty_ptr), ty), ty) + +let make_builtin_va_arg env ty e = + match ty with + | Tint _ | Tpointer _ -> + make_builtin_va_arg_by_val + "__compcert_va_int32" ty (Tint(I32, Unsigned, noattr)) e + | Tlong _ -> + make_builtin_va_arg_by_val + "__compcert_va_int64" ty (Tlong(Unsigned, noattr)) e + | Tfloat _ -> + make_builtin_va_arg_by_val + "__compcert_va_float64" ty (Tfloat(F64, noattr)) e + | Tstruct _ | Tunion _ -> + make_builtin_va_arg_by_ref + "__compcert_va_composite" ty e + | _ -> + unsupported "va_arg at this type"; + Eval(Vint(coqint_of_camlint 0l), type_int32s) + (** ** Translation functions *) (** Constants *) diff --git a/runtime/arm/vararg.S b/runtime/arm/vararg.S index ae06e361..5e319b8b 100644 --- a/runtime/arm/vararg.S +++ b/runtime/arm/vararg.S @@ -75,3 +75,15 @@ FUNCTION(__compcert_va_float64) #endif bx lr ENDFUNCTION(__compcert_va_float64) + +FUNCTION(__compcert_va_composite) + @ r0 = ap parameter + @ r1 = size of the composite, in bytes + ldr r2, [r0, #0] @ r2 = pointer to next argument + ADD r3, r2, r1 @ advance by size + ADD r3, r3, #3 @ 4-align + BIC r3, r3, #3 + str r3, [r0, #0] @ update ap + mov r0, r2 @ result is pointer to composite in stack + bx lr +ENDFUNCTION(__compcert_va_composite) diff --git a/test/regression/Results/varargs2 b/test/regression/Results/varargs2 index f954927e..96ee9d63 100644 --- a/test/regression/Results/varargs2 +++ b/test/regression/Results/varargs2 @@ -2,7 +2,9 @@ An int: 42 A long long: 123456789012345 A string: Hello world A double: 3.141592654 -A mixture: x & Hello, world! & 42 & 123456789012345 & 3.141592654 & 2.718281746 +A small struct: x12 +A bigger struct: (123,456,789) +A mixture: x & Hello, world! & y2 & 42 & 123456789012345 & 3.141592654 & 2.718281746 Twice: -1 1.23 Twice: -1 1.23 With va_copy: -1 1.23 diff --git a/test/regression/varargs2.c b/test/regression/varargs2.c index 6c091d8b..b96d1940 100644 --- a/test/regression/varargs2.c +++ b/test/regression/varargs2.c @@ -1,6 +1,9 @@ #include <stdarg.h> #include <stdio.h> +struct Y { char kind; unsigned char num; }; +struct Z { int x, y, z; }; + void minivprintf(const char * fmt, va_list ap) { char c; @@ -32,6 +35,14 @@ void minivprintf(const char * fmt, va_list ap) case 'f': printf("%.10g", (float) va_arg(ap, double)); break; + case 'y': + { struct Y s = va_arg(ap, struct Y); + printf("%c%d", s.kind, s.num); + break; } + case 'z': + { struct Z s = va_arg(ap, struct Z); + printf("(%d,%d,%d)", s.x, s.y, s.z); + break; } default: puts("<bad format>"); return; @@ -111,9 +122,12 @@ int main() miniprintf("A long long: %l\n", 123456789012345LL); miniprintf("A string: %s\n", "Hello world"); miniprintf("A double: %e\n", 3.141592654); - miniprintf("A mixture: %c & %s & %d & %l & %e & %f\n", + miniprintf("A small struct: %y\n", (struct Y) { 'x', 12 }); + miniprintf("A bigger struct: %z\n", (struct Z) { 123, 456, 789 }); + miniprintf("A mixture: %c & %s & %y & %d & %l & %e & %f\n", 'x', "Hello, world!", + (struct Y) { 'y', 2 }, 42, 123456789012345LL, 3.141592654, |