From d05703f808d3111a73106d8a0e90441fe743415d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 15 May 2023 10:41:23 +0000
Subject: [PATCH] Variadic args/va_arg: handle unexpected va_list types

Our regression test has `void*` lists when we'd expected `void**`. This,
however, went unnoticed as we only tried to access the first element.
Attempts to access the second element would have been misaligned, and
failed an invariant as of 35cc503 (we don't handle pointer arithmetic
over void pointers in the back-end anymore).

We now make sure that we always increment by size-of-`void*`.

Fixes: #7706
---
 regression/cbmc/va_list2/main.c               |  6 +++--
 .../goto-conversion/builtin_functions.cpp     | 23 +++++++++++++++----
 2 files changed, 22 insertions(+), 7 deletions(-)

diff --git a/regression/cbmc/va_list2/main.c b/regression/cbmc/va_list2/main.c
index 90950aca44b..3be9e17c67b 100644
--- a/regression/cbmc/va_list2/main.c
+++ b/regression/cbmc/va_list2/main.c
@@ -11,14 +11,16 @@ void my_f(int first, ...)
 
   int v;
   v=__builtin_va_arg(args, int);
-  assert(v==2);
+  assert(v == 1);
+  v = __builtin_va_arg(args, int);
+  assert(v == 0);
 
   __builtin_va_end(args);
 }
 
 int main()
 {
-  my_f(1, 2);
+  my_f(2, 1, 0);
 }
 
 #else
diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp
index dc944e3d964..86e9790718b 100644
--- a/src/ansi-c/goto-conversion/builtin_functions.cpp
+++ b/src/ansi-c/goto-conversion/builtin_functions.cpp
@@ -20,6 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/mathematical_expr.h>
 #include <util/mathematical_types.h>
 #include <util/pointer_expr.h>
+#include <util/pointer_offset_size.h>
 #include <util/rational.h>
 #include <util/rational_tools.h>
 #include <util/simplify_expr.h>
@@ -1306,12 +1307,24 @@ 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())}};
-    assign.rhs().set(
-      ID_C_va_arg_type, to_code_type(function.type()).return_type());
+    exprt rhs;
+    if(list_arg.type() == pointer_type(pointer_type(empty_typet{})))
+      rhs = plus_exprt{list_arg, from_integer(1, pointer_diff_type())};
+    else
+    {
+      // handle unexpected va_list types by just enforcing pointer increments by
+      // size-of-void*
+      rhs = typecast_exprt{
+        plus_exprt{
+          typecast_exprt{list_arg, pointer_type(char_type())},
+          from_integer(
+            *pointer_offset_size(pointer_type(empty_typet{}), ns),
+            pointer_diff_type())},
+        list_arg.type()};
+    }
+    rhs.set(ID_C_va_arg_type, to_code_type(function.type()).return_type());
     dest.add(goto_programt::make_assignment(
-      std::move(assign), function.source_location()));
+      list_arg, std::move(rhs), function.source_location()));
   }
   else if(identifier == "__builtin_va_copy")
   {