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 #8366, but we
didn't yet implement the struct type support in goto conversion.

Author: tautschnig

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

@@ -547,12 +547,20 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
   typet arg_type=expr.type();
   typecheck_type(arg_type);
 
+  const symbolt *symbol_ptr;
+  if(lookup("__builtin_va_list", symbol_ptr))
+  {
+    error().source_location = expr.source_location();
+    error() << "failed to find typedef name __builtin_va_list" << eom;
+    throw 0;
+  }
+
   const code_typet new_type(
-    {code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type));
+    {code_typet::parametert(symbol_ptr->type)}, std::move(arg_type));
 
   exprt arg = to_unary_expr(expr).op();
 
-  implicit_typecast(arg, pointer_type(void_type()));
+  implicit_typecast(arg, new_type.parameters().front().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