Function pointer removal: argument conversion must use byte extract

Only POD can be handled via type casts, all other cases require
reinterpreting the byte sequence. For POD, the simplifier will clean up
the byte extract.

The same problem had already been fixed for goto-symex' function
argument conversion back in bb80cdc.

Co-authored-by: Celina G. Val <[email protected]>

Fixes: #6956

Author: tautschnig

regression/cbmc/Function_Pointer19/main.c

@@ -0,0 +1,51 @@
+#include <assert.h>
+
+struct PtrWrapperInner
+{
+  int *value;
+};
+
+struct PtrWrapper
+{
+  int *value;
+  struct PtrWrapperInner inner;
+};
+
+struct AltPtrWrapperInner
+{
+  int *value;
+};
+
+struct AltPtrWrapper
+{
+  unsigned int *value;
+  // A) Doesn't work
+  struct AltPtrWrapperInner inner;
+  // B) Works
+  // struct PtrWrapperInner inner;
+};
+
+void fn(struct PtrWrapper wrapper)
+{
+  assert(*wrapper.value == 10);
+  assert(*wrapper.inner.value == 10);
+}
+
+int main()
+{
+  int ret = 10;
+  int *ptr = &ret;
+
+  struct AltPtrWrapper alt;
+  alt.inner.value = ptr;
+  alt.value = ptr;
+
+  // Casting the structure itself works.
+  struct PtrWrapper wrapper = *(struct PtrWrapper *)&alt;
+  assert(*wrapper.value == 10);
+  assert(*wrapper.inner.value == 10);
+
+  // This only works if there is one level of casting.
+  int (*alias)(struct AltPtrWrapper) = (int (*)(struct AltPtrWrapper))fn;
+  alias(alt);
+}

regression/cbmc/Function_Pointer19/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/cbmc/Linking7/member-name-mismatch.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 module2.c
 ^EXIT=10$

regression/cbmc/Linking7/test.desc

@@ -1,4 +1,4 @@
-CORE broken-smt-backend
+CORE
 main.c
 module.c
 ^EXIT=10$

src/goto-programs/remove_function_pointers.cpp

@@ -11,6 +11,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "remove_function_pointers.h"
 
+#include <util/arith_tools.h>
+#include <util/byte_operators.h>
 #include <util/c_types.h>
 #include <util/fresh_symbol.h>
 #include <util/invariant.h>
@@ -195,8 +197,10 @@ static void fix_argument_types(code_function_callt &function_call)
     {
       if(call_arguments[i].type() != function_parameters[i].type())
       {
-        call_arguments[i] =
-          typecast_exprt(call_arguments[i], function_parameters[i].type());
+        call_arguments[i] = make_byte_extract(
+          call_arguments[i],
+          from_integer(0, c_index_type()),
+          function_parameters[i].type());
       }
     }
   }
@@ -235,8 +239,10 @@ static void fix_return_type(
   exprt old_lhs=function_call.lhs();
   function_call.lhs()=tmp_symbol_expr;
 
-  dest.add(goto_programt::make_assignment(
-    code_assignt(old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()))));
+  dest.add(goto_programt::make_assignment(code_assignt(
+    old_lhs,
+    make_byte_extract(
+      tmp_symbol_expr, from_integer(0, c_index_type()), old_lhs.type()))));
 }
 
 void remove_function_pointerst::remove_function_pointer(