From 40a3dbbe6af4c54a186a2e8ec829935108ec7145 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 2 Jul 2024 11:11:59 +0000
Subject: [PATCH] C library: fix use of va_list for AARCH64

This is a fixup to "C model library: Support ARM64 va_list types" that
1) only changed only a subset of the code locations that required change
   and
2) did so with a crude workaround.

Really, we need to abide by ARM's procedure call standard for ARM64,
which mandates that `va_list` be a particular struct. See

https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst#definition-of-va-list
and
https://github.com/ARM-software/abi-aa/blob/main/aapcs64/aapcs64.rst#the-va-arg-macro

While at it, also add the necessary define for Visual Studio's support
of ARM64.

Fixes: #8357
---
 src/ansi-c/library/stdio.c | 100 +++++++++++++++++++++++++++++++++----
 src/util/config.cpp        |   5 +-
 2 files changed, 93 insertions(+), 12 deletions(-)

diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c
index ef4932d30ad..e2cfe4543cf 100644
--- a/src/ansi-c/library/stdio.c
+++ b/src/ansi-c/library/stdio.c
@@ -1134,14 +1134,23 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
   }
 
   (void)*format;
-  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
+#  if defined(__aarch64__) || defined(_M_ARM64)
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
+        __CPROVER_OBJECT_SIZE(arg.__stack))
+  {
+    void *a = va_arg(arg, void *);
+    __CPROVER_havoc_object(a);
+  }
+#  else
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
         __CPROVER_OBJECT_SIZE(arg))
   {
     void *a = va_arg(arg, void *);
     __CPROVER_havoc_object(a);
   }
+#  endif
 
-#ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
+#  ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(__CPROVER_get_must(stream, "open"),
                    "vfscanf file must be open");
 #endif
@@ -1183,12 +1192,21 @@ __CPROVER_HIDE:;
   }
 
   (void)*format;
-  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
-        __CPROVER_OBJECT_SIZE(*(void **)&arg))
+#if defined(__aarch64__) || defined(_M_ARM64)
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
+        __CPROVER_OBJECT_SIZE(arg.__stack))
+  {
+    void *a = va_arg(arg, void *);
+    __CPROVER_havoc_object(a);
+  }
+#else
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
+        __CPROVER_OBJECT_SIZE(arg))
   {
     void *a = va_arg(arg, void *);
     __CPROVER_havoc_object(a);
   }
+#endif
 
 #ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(
@@ -1232,12 +1250,21 @@ int __stdio_common_vfscanf(
   }
 
   (void)*format;
-  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
+#  if defined(__aarch64__) || defined(_M_ARM64)
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args.__stack) <
+        __CPROVER_OBJECT_SIZE(args.__stack))
+  {
+    void *a = va_arg(args, void *);
+    __CPROVER_havoc_object(a);
+  }
+#  else
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
         __CPROVER_OBJECT_SIZE(args))
   {
     void *a = va_arg(args, void *);
     __CPROVER_havoc_object(a);
   }
+#  endif
 
 #  ifdef __CPROVER_CUSTOM_BITVECTOR_ANALYSIS
   __CPROVER_assert(
@@ -1311,12 +1338,21 @@ __CPROVER_HIDE:;
   int result = __VERIFIER_nondet_int();
   (void)*s;
   (void)*format;
-  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
+#  if defined(__aarch64__) || defined(_M_ARM64)
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
+        __CPROVER_OBJECT_SIZE(arg.__stack))
+  {
+    void *a = va_arg(arg, void *);
+    __CPROVER_havoc_object(a);
+  }
+#  else
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
         __CPROVER_OBJECT_SIZE(arg))
   {
     void *a = va_arg(arg, void *);
     __CPROVER_havoc_object(a);
   }
+#  endif
 
   return result;
 }
@@ -1346,12 +1382,21 @@ __CPROVER_HIDE:;
   int result = __VERIFIER_nondet_int();
   (void)*s;
   (void)*format;
-  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
-        __CPROVER_OBJECT_SIZE(*(void **)&arg))
+#if defined(__aarch64__) || defined(_M_ARM64)
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg.__stack) <
+        __CPROVER_OBJECT_SIZE(arg.__stack))
+  {
+    void *a = va_arg(arg, void *);
+    __CPROVER_havoc_object(a);
+  }
+#else
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(arg) <
+        __CPROVER_OBJECT_SIZE(arg))
   {
     void *a = va_arg(arg, void *);
     __CPROVER_havoc_object(a);
   }
+#endif
 
   return result;
 }
@@ -1387,12 +1432,21 @@ int __stdio_common_vsscanf(
 
   (void)*s;
   (void)*format;
-  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
+#  if defined(__aarch64__) || defined(_M_ARM64)
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args.__stack) <
+        __CPROVER_OBJECT_SIZE(args.__stack))
+  {
+    void *a = va_arg(args, void *);
+    __CPROVER_havoc_object(a);
+  }
+#  else
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(args) <
         __CPROVER_OBJECT_SIZE(args))
   {
     void *a = va_arg(args, void *);
     __CPROVER_havoc_object(a);
   }
+#  endif
 
   return result;
 }
@@ -1773,7 +1827,18 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
 {
   (void)*fmt;
 
-  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
+#if defined(__aarch64__) || defined(_M_ARM64)
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
+        __CPROVER_OBJECT_SIZE(ap.__stack))
+
+  {
+    (void)va_arg(ap, int);
+    __CPROVER_precondition(
+      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap.__stack),
+      "vsnprintf object overlap");
+  }
+#else
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap) <
         __CPROVER_OBJECT_SIZE(ap))
 
   {
@@ -1782,6 +1847,7 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
       __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
       "vsnprintf object overlap");
   }
+#endif
 
   size_t i = 0;
   for(; i < size; ++i)
@@ -1821,7 +1887,18 @@ int __builtin___vsnprintf_chk(
   (void)bufsize;
   (void)*fmt;
 
-  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
+#if defined(__aarch64__) || defined(_M_ARM64)
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap.__stack) <
+        __CPROVER_OBJECT_SIZE(ap.__stack))
+
+  {
+    (void)va_arg(ap, int);
+    __CPROVER_precondition(
+      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap.__stack),
+      "vsnprintf object overlap");
+  }
+#else
+  while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(ap) <
         __CPROVER_OBJECT_SIZE(ap))
 
   {
@@ -1830,6 +1907,7 @@ int __builtin___vsnprintf_chk(
       __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
       "vsnprintf object overlap");
   }
+#endif
 
   size_t i = 0;
   for(; i < size; ++i)
diff --git a/src/util/config.cpp b/src/util/config.cpp
index 8768423b38a..34654d2780a 100644
--- a/src/util/config.cpp
+++ b/src/util/config.cpp
@@ -308,7 +308,10 @@ void configt::ansi_ct::set_arch_spec_arm(const irep_idt &subarch)
     break;
 
   case flavourt::VISUAL_STUDIO:
-    defines.push_back("_M_ARM");
+    if(subarch == "arm64")
+      defines.push_back("_M_ARM64");
+    else
+      defines.push_back("_M_ARM");
     break;
 
   case flavourt::CODEWARRIOR: