From a90ffe0a21a3a813df4eb9a4dc23b06f50699cde Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Fri, 20 Mar 2015 16:43:14 +0100
Subject: Support va_arg for vararg arguments of composite (struct/union)
 types.

ARM is done, IA32 and PowerPC remain to be updated.
---
 cfrontend/C2C.ml | 50 +++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 37 insertions(+), 13 deletions(-)

(limited to 'cfrontend/C2C.ml')

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 *)
-- 
cgit