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

Diff for: 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

Diff for: src/ansi-c/c_typecheck_expr.cpp

@@ -541,12 +541,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();

Diff for: 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);

Diff for: 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__));

Diff for: src/ansi-c/goto-conversion/builtin_functions.cpp

@@ -593,8 +593,19 @@ 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,7 +1307,7 @@ 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);
 
     if(lhs.is_not_nil())
     {
@@ -1333,7 +1344,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 +1368,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 +1403,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))
     {