Linking: actually replace code type information in expressions

tautschnig · tautschnig · commit 39e7078c1381 · 2022-10-09T15:31:33.000Z
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.
diff --git a/regression/ansi-c/undeclared_function/fileB.c b/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()
 {
diff --git a/regression/ansi-c/undeclared_function/undeclared_function1.desc b/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$
diff --git a/regression/cbmc/incomplete-structs/test.desc b/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$
 --
diff --git a/regression/cbmc/incomplete-structs/types1.c b/regression/cbmc/incomplete-structs/types1.c
diff --git a/regression/cbmc/incomplete-structs/types2.c b/regression/cbmc/incomplete-structs/types2.c
diff --git a/regression/cbmc/incomplete-structs/types3.c b/regression/cbmc/incomplete-structs/types3.c
diff --git a/regression/cbmc/incomplete-structs/typesmain.c b/regression/cbmc/incomplete-structs/typesmain.c
diff --git a/regression/cbmc/return6/test.desc b/regression/cbmc/return6/test.desc
@@ -1,9 +1,8 @@
 CORE
 main.c
 f_def.c
-^EXIT=6$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
 ^SIGNAL=0$
-CONVERSION ERROR
 --
 ^warning: ignoring
-^VERIFICATION SUCCESSFUL$
diff --git a/regression/linking-goto-binaries/chain.sh b/regression/linking-goto-binaries/chain.sh
@@ -21,4 +21,4 @@ else
   $goto_cc "${main}.gb" "${next}.gb" -o "final.gb"
 fi
 
-$cbmc "final.gb"
+$cbmc --validate-goto-model "final.gb"
diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-main.c b/regression/linking-goto-binaries/type_conflicts/Linking7-main.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;
+}
diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-module.c b/regression/linking-goto-binaries/type_conflicts/Linking7-module.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});
+}
diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-module2.c b/regression/linking-goto-binaries/type_conflicts/Linking7-module2.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 *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});
+}
diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-return_type1.c b/regression/linking-goto-binaries/type_conflicts/Linking7-return_type1.c
@@ -0,0 +1,13 @@
+#include <assert.h>
+
+struct S
+{
+  int i;
+};
+
+struct S *function();
+
+int main()
+{
+  assert(function() != 0);
+}
diff --git a/regression/linking-goto-binaries/type_conflicts/Linking7-return_type2.c b/regression/linking-goto-binaries/type_conflicts/Linking7-return_type2.c
@@ -0,0 +1,10 @@
+struct S
+{
+  int i;
+  int j; // extra member
+} some_var;
+
+struct S *function()
+{
+  return &some_var;
+}
diff --git a/regression/linking-goto-binaries/type_conflicts/member-name-mismatch.desc b/regression/linking-goto-binaries/type_conflicts/member-name-mismatch.desc
@@ -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 3 failed
+--
+^warning: ignoring
diff --git a/regression/linking-goto-binaries/type_conflicts/return_type.desc b/regression/linking-goto-binaries/type_conflicts/return_type.desc
@@ -0,0 +1,10 @@
+CORE
+Linking7-return_type1.c
+Linking7-return_type2.c
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+Note issue #3081
diff --git a/regression/linking-goto-binaries/type_conflicts/test.desc b/regression/linking-goto-binaries/type_conflicts/test.desc
@@ -0,0 +1,11 @@
+CORE
+Linking7-main.c
+Linking7-module.c
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\*\* 1 of 3 failed
+line 21 assertion \*g\.a == 42: SUCCESS
+line 22 assertion \*g\.b == 41: FAILURE
+--
+^warning: ignoring
diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp
@@ -148,7 +148,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());
 
@@ -196,10 +196,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;
+          });
+        }
       }
     }
   }
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
diff --git a/src/linking/linking_class.h b/src/linking/linking_class.h

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,7 @@`
`1`		`-#include <stdlib.h>`
	`1`	`+void *malloc(__CPROVER_size_t s)`
	`2`	`+{`
	`3`	`+ return (void *)0 + s;`
	`4`	`+}`
`2`	`5`
`3`	`6`	`int f()`
`4`	`7`	`{`
Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-KNOWNBUG`
	`1`	`+CORE gcc-only`
`2`	`2`	`fileA.c`
`3`	`3`	`fileB.c --validate-goto-model`
`4`	`4`	`^EXIT=0$`