Linking: actually replace code type information in expressions

The linker already accepted a number of type mismatches for function
declarations, but did not actually modify the goto functions to reflect
these type mismatches, just the type information in the symbol table was
updated. These changes enable support for conflicts on function return
types, which are now resolved by introducing type casts.

Author: tautschnig

regression/ansi-c/undeclared_function/fileB.c

@@ -1,4 +1,7 @@
-#include <stdlib.h>
+void *malloc(__CPROVER_size_t s)
+{
+  return (void *)0 + s;
+}
 
 int f()
 {

regression/ansi-c/undeclared_function/undeclared_function1.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE gcc-only
 fileA.c
 fileB.c --validate-goto-model
 ^EXIT=0$

regression/ansi-c/incomplete-structs/test.desc renamed to regression/cbmc/incomplete-structs/test.desc

@@ -1,11 +1,12 @@
 CORE
 typesmain.c
-types1.c types2.c types3.c --verbosity 2
+types1.c types2.c types3.c
 reason for conflict at \*#this.u: number of members is different \(3/0\)
 reason for conflict at \*#this.u: number of members is different \(0/3\)
 struct U   \(incomplete\)
 warning: pointer parameter types differ between declaration and definition "bar"
 warning: pointer parameter types differ between declaration and definition "foo"
+^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/ansi-c/incomplete-structs/types1.c renamed to regression/cbmc/incomplete-structs/types1.c

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

regression/ansi-c/incomplete-structs/types2.c renamed to regression/cbmc/incomplete-structs/types2.c

@@ -21,4 +21,4 @@ else
   $goto_cc "${main}.gb" "${next}.gb" -o "final.gb"
 fi
 
-$cbmc "final.gb"
+$cbmc --validate-goto-model "final.gb"

regression/ansi-c/incomplete-structs/types3.c renamed to regression/cbmc/incomplete-structs/types3.c

@@ -0,0 +1,19 @@
+struct S
+{
+  void *a;
+  void *b;
+};
+
+typedef void (*fptr)(struct S);
+
+extern void foo(struct S s);
+
+fptr A[] = {foo};
+
+extern void bar();
+
+int main()
+{
+  bar();
+  return 0;
+}

regression/ansi-c/incomplete-structs/typesmain.c renamed to regression/cbmc/incomplete-structs/typesmain.c

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+struct S
+{
+  void *a;
+  void *b;
+};
+
+typedef void (*fptr)(struct S);
+
+extern fptr A[1];
+
+struct real_S
+{
+  int *a;
+  int *b;
+};
+
+void foo(struct real_S g)
+{
+  assert(*g.a == 42);
+  assert(*g.b == 41);
+}
+
+void bar()
+{
+  int x = 42;
+  struct real_S s;
+  s.a = &x;
+  s.b = &x;
+  A[0]((struct S){s.a, s.b});
+}

regression/cbmc/return6/test.desc

@@ -0,0 +1,32 @@
+#include <assert.h>
+
+struct S
+{
+  void *a;
+  void *b;
+};
+
+typedef void (*fptr)(struct S);
+
+extern fptr A[1];
+
+struct real_S
+{
+  int *a;
+  int *c;
+};
+
+void foo(struct real_S g)
+{
+  assert(*g.a == 42);
+  assert(*g.c == 41);
+}
+
+void bar()
+{
+  int x = 42;
+  struct real_S s;
+  s.a = &x;
+  s.c = &x;
+  A[0]((struct S){s.a, s.c});
+}

regression/linking-goto-binaries/chain.sh

@@ -0,0 +1,13 @@
+#include <assert.h>
+
+struct S
+{
+  int i;
+};
+
+struct S *function();
+
+int main()
+{
+  assert(function() != 0);
+}

regression/linking-goto-binaries/type_conflicts/Linking7-main.c

@@ -0,0 +1,10 @@
+struct S
+{
+  int i;
+  int j; // extra member
+} some_var;
+
+struct S *function()
+{
+  return &some_var;
+}

regression/linking-goto-binaries/type_conflicts/Linking7-module.c

@@ -0,0 +1,11 @@
+CORE
+Linking7-main.c
+Linking7-module2.c
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+line 21 assertion \*g\.a == 42: SUCCESS
+line 22 assertion \*g\.c == 41: FAILURE
+^\*\* 1 of 2 failed
+--
+^warning: ignoring

regression/linking-goto-binaries/type_conflicts/Linking7-module2.c

@@ -0,0 +1,10 @@
+CORE
+Linking7-return_type1.c
+Linking7-return_type2.c
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Note issue #3081

regression/linking-goto-binaries/type_conflicts/Linking7-return_type1.c

@@ -0,0 +1,11 @@
+CORE
+Linking7-main.c
+Linking7-module.c
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\*\* 1 of 2 failed
+line 21 assertion \*g\.a == 42: SUCCESS
+line 22 assertion \*g\.b == 41: FAILURE
+--
+^warning: ignoring

regression/linking-goto-binaries/type_conflicts/Linking7-return_type2.c

@@ -152,7 +152,7 @@ void finalize_linking(
   goto_modelt &dest,
   const replace_symbolt::expr_mapt &type_updates)
 {
-  unchecked_replace_symbolt object_type_updates;
+  casting_replace_symbolt object_type_updates;
   object_type_updates.get_expr_map().insert(
     type_updates.begin(), type_updates.end());
 
@@ -200,10 +200,30 @@ void finalize_linking(
     {
       for(auto &instruction : gf_entry.second.body.instructions)
       {
-        instruction.transform([&object_type_updates](exprt expr) {
-          object_type_updates(expr);
-          return expr;
-        });
+        if(instruction.is_function_call())
+        {
+          const bool changed =
+            !object_type_updates.replace(instruction.call_function());
+          if(changed && instruction.call_lhs().is_not_nil())
+          {
+            object_type_updates(instruction.call_lhs());
+            if(
+              instruction.call_lhs().type() !=
+              to_code_type(instruction.call_function().type()).return_type())
+            {
+              instruction.call_lhs() = typecast_exprt{
+                instruction.call_lhs(),
+                to_code_type(instruction.call_function().type()).return_type()};
+            }
+          }
+        }
+        else
+        {
+          instruction.transform([&object_type_updates](exprt expr) {
+            const bool changed = !object_type_updates.replace(expr);
+            return changed ? optionalt<exprt>{expr} : nullopt;
+          });
+        }
       }
     }
   }