Fully support aarch64 ABI's va_list struct

aarch64 ABI (section 7.1.4) mandates that va_list is a struct with
particular members. The C library model was fixed in diffblue#8366, but we
didn't yet implement the struct type support in goto conversion.

Author: tautschnig

regression/cbmc/va_list2/main.c

@@ -1,4 +1,4 @@
-#ifdef __GNUC__
+#if defined(__GNUC__) && (!defined(__aarch64__) || defined(__APPLE__))
 
 #  include <assert.h>
 

regression/cbmc/va_list4/main.c

@@ -1,4 +1,4 @@
-#ifdef __GNUC__
+#if defined(__GNUC__) && (!defined(__aarch64__) || defined(__APPLE__))
 
 struct __va_list_tag;
 typedef struct __va_list_tag __va_list_tag;

src/ansi-c/ansi_c_internal_additions.cpp

@@ -286,6 +286,23 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type)
       code+="typedef signed __int128 __int128_t;\n"
             "typedef unsigned __int128 __uint128_t;\n";
     }
+
+    if(
+      config.ansi_c.arch == "arm64" &&
+      config.ansi_c.os != configt::ansi_ct::ost::OS_MACOS)
+    {
+      code += "typedef struct __va_list {";
+      code += "void *__stack;";
+      code += "void *__gr_top;";
+      code += "void *__vr_top;";
+      code += "int   __gr_offs;";
+      code += "int   __vr_offs;";
+      code += " } __builtin_va_list;\n";
+    }
+    else
+    {
+      code += "typedef void ** __builtin_va_list;\n";
+    }
   }
 
   // this is Visual C/C++ only

src/ansi-c/c_typecheck_expr.cpp

@@ -544,15 +544,23 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
   // is the type, which will need to be fixed and checked.
   // The type is given by the parser as type of the expression.
 
-  typet arg_type=expr.type();
-  typecheck_type(arg_type);
-
-  const code_typet new_type(
-    {code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type));
-
   exprt arg = to_unary_expr(expr).op();
+  auto typedef_id = arg.type().get(ID_C_typedef);
+  if(
+    typedef_id != "__builtin_va_list" && typedef_id != "__builtin_ms_va_list" &&
+    typedef_id != "va_list")
+  {
+    error().source_location = expr.source_location();
+    error() << "argument of type '" << to_string(arg.type())
+            << "' not permitted for va_arg" << eom;
+    throw 0;
+  }
+
+  typet arg_type = expr.type();
+  typecheck_type(arg_type);
 
-  implicit_typecast(arg, pointer_type(void_type()));
+  const code_typet new_type{
+    {code_typet::parametert{arg.type()}}, std::move(arg_type)};
 
   symbol_exprt function(ID_gcc_builtin_va_arg, new_type);
   function.add_source_location() = expr.source_location();

src/ansi-c/compiler_headers/gcc_builtin_headers_generic.h

@@ -2,14 +2,14 @@
 // stdarg
 void* __builtin_apply_args();
 void* __builtin_apply(void (*)(), void*, __CPROVER_size_t);
-void __builtin_ms_va_end(void *ap);
-void __builtin_ms_va_start(void *ap, ...);
+void __builtin_ms_va_end(__builtin_ms_va_list ap);
+void __builtin_ms_va_start(__builtin_ms_va_list ap, ...);
 void* __builtin_next_arg();
 int __builtin_va_arg_pack();
 int __builtin_va_arg_pack_len();
 void __builtin_va_copy(__builtin_va_list dest, __builtin_va_list src);
-void __builtin_va_end(void *ap);
-void __builtin_va_start(void *ap, ...);
+void __builtin_va_end(__builtin_va_list ap);
+void __builtin_va_start(__builtin_va_list ap, ...);
 
 // stdlib
 void __builtin__Exit(int);

src/ansi-c/compiler_headers/gcc_builtin_headers_types.h

@@ -1,5 +1,4 @@
 // clang-format off
-typedef void ** __builtin_va_list;
 typedef void ** __builtin_ms_va_list;
 
 typedef int    __gcc_m64   __attribute__ ((__vector_size__ (8), __may_alias__));

src/ansi-c/goto-conversion/builtin_functions.cpp

@@ -593,8 +593,20 @@ void goto_convertt::do_array_op(
   copy(array_op_statement, OTHER, dest);
 }
 
-exprt make_va_list(const exprt &expr)
+static exprt make_va_list(const exprt &expr, const namespacet &ns)
 {
+  if(
+    auto struct_tag_type = type_try_dynamic_cast<struct_tag_typet>(expr.type()))
+  {
+    // aarch64 ABI mandates that va_list has struct type with member names as
+    // specified
+    const auto &components = ns.follow_tag(*struct_tag_type).components();
+    DATA_INVARIANT(
+      components.size() == 5,
+      "va_list struct type expected to have 5 components");
+    return member_exprt{expr, components.front()};
+  }
+
   exprt result = skip_typecast(expr);
 
   // if it's an address of an lvalue, we take that
@@ -1296,14 +1308,15 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
-    exprt list_arg = make_va_list(arguments[0]);
+    exprt list_arg = make_va_list(arguments[0], ns);
+    const bool va_list_is_void_ptr =
+      list_arg.type().id() == ID_pointer &&
+      to_pointer_type(list_arg.type()).base_type().id() == ID_empty;
 
     if(lhs.is_not_nil())
     {
       exprt list_arg_cast = list_arg;
-      if(
-        list_arg.type().id() == ID_pointer &&
-        to_pointer_type(list_arg.type()).base_type().id() == ID_empty)
+      if(va_list_is_void_ptr)
       {
         list_arg_cast =
           typecast_exprt{list_arg, pointer_type(pointer_type(empty_typet{}))};
@@ -1317,8 +1330,14 @@ void goto_convertt::do_function_call_symbol(
         goto_programt::make_assignment(lhs, rhs, function.source_location()));
     }
 
-    code_assignt assign{
-      list_arg, plus_exprt{list_arg, from_integer(1, pointer_diff_type())}};
+    exprt list_arg_ptr_arithmetic = typecast_exprt::conditional_cast(
+      plus_exprt{
+        (va_list_is_void_ptr
+           ? typecast_exprt{list_arg, pointer_type(pointer_type(empty_typet{}))}
+           : list_arg),
+        from_integer(1, pointer_diff_type())},
+      list_arg.type());
+    code_assignt assign{list_arg, std::move(list_arg_ptr_arithmetic)};
     assign.rhs().set(
       ID_C_va_arg_type, to_code_type(function.type()).return_type());
     dest.add(goto_programt::make_assignment(
@@ -1333,7 +1352,7 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
-    exprt dest_expr = make_va_list(arguments[0]);
+    exprt dest_expr = make_va_list(arguments[0], ns);
     const typecast_exprt src_expr(arguments[1], dest_expr.type());
 
     if(!is_assignable(dest_expr))
@@ -1357,7 +1376,7 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
-    exprt dest_expr = make_va_list(arguments[0]);
+    exprt dest_expr = make_va_list(arguments[0], ns);
 
     if(!is_assignable(dest_expr))
     {
@@ -1392,7 +1411,7 @@ void goto_convertt::do_function_call_symbol(
       throw 0;
     }
 
-    exprt dest_expr = make_va_list(arguments[0]);
+    exprt dest_expr = make_va_list(arguments[0], ns);
 
     if(!is_assignable(dest_expr))
     {

src/cpp/cpp_internal_additions.cpp

@@ -155,6 +155,23 @@ void cpp_internal_additions(std::ostream &out)
       out << "typedef signed __int128 __int128_t;" << '\n';
       out << "typedef unsigned __int128 __uint128_t;" << '\n';
     }
+
+    if(
+      config.ansi_c.arch == "arm64" &&
+      config.ansi_c.os != configt::ansi_ct::ost::OS_MACOS)
+    {
+      out << "typedef struct __va_list {";
+      out << "void *__stack;";
+      out << "void *__gr_top;";
+      out << "void *__vr_top;";
+      out << "int   __gr_offs;";
+      out << "int   __vr_offs;";
+      out << " } __builtin_va_list;" << '\n';
+    }
+    else
+    {
+      out << "typedef void ** __builtin_va_list;" << '\n';
+    }
   }
 
   // this is Visual C/C++ only

src/goto-symex/symex_builtin_functions.cpp

@@ -351,7 +351,17 @@ static std::optional<exprt> get_va_args(const exprt::operandst &operands)
   if(operands.size() != 2)
     return {};
 
-  const exprt &second_op = skip_typecast(operands.back());
+  exprt second_op = skip_typecast(operands.back());
+  if(second_op.id() == ID_struct)
+  {
+    // aarch64 ABI mandates that va_list has struct type with member names as
+    // specified
+    if(second_op.operands().size() != 5)
+      return {};
+
+    second_op = skip_typecast(second_op.operands().front());
+  }
+
   if(second_op.id() != ID_address_of)
     return {};
 
@@ -402,11 +412,12 @@ void goto_symext::symex_printf(
       return;
     }
 
-    // Visual Studio has va_list == char*, else we have va_list == void** and
-    // need to add dereferencing
+    // Visual Studio has va_list == char*, else we have va_list == void** or a
+    // struct containing void** (aarch64) and need to add dereferencing
     const bool need_deref =
-      operands.back().type().id() == ID_pointer &&
-      to_pointer_type(operands.back().type()).base_type().id() == ID_pointer;
+      operands.back().type().id() == ID_struct_tag ||
+      (operands.back().type().id() == ID_pointer &&
+       to_pointer_type(operands.back().type()).base_type().id() == ID_pointer);
 
     for(const auto &op : va_args->operands())
     {