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
 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

@@ -8,17 +8,19 @@ is_windows=$3
 
 main=${*:$#}
 main=${main%.c}
+main_local=$(basename ${main})
 args=${*:4:$#-4}
 next=${args%.c}
+next_local=$(basename ${next})
 
 if [[ "${is_windows}" == "true" ]]; then
-  $goto_cc /c "${main}.c" "/Fo${main}.gb"
-  $goto_cc /c "${next}.c" "/Fo${next}.gb"
-  $goto_cc "${main}.gb" "${next}.gb" "/Fefinal.gb"
+  $goto_cc /c "${main}.c" "/Fo${main_local}.gb"
+  $goto_cc /c "${next}.c" "/Fo${next_local}.gb"
+  $goto_cc "${main_local}.gb" "${next_local}.gb" "/Fefinal.gb"
 else
-  $goto_cc -c -o "${main}.gb" "${main}.c"
-  $goto_cc -c -o "${next}.gb" "${next}.c"
-  $goto_cc "${main}.gb" "${next}.gb" -o "final.gb"
+  $goto_cc -c -o "${main_local}.gb" "${main}.c"
+  $goto_cc -c -o "${next_local}.gb" "${next}.c"
+  $goto_cc "${main_local}.gb" "${next_local}.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,11 @@
+CORE
+../../cbmc/Linking7/main.c
+../../cbmc/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/ansi-c/incomplete-structs/typesmain.c renamed to regression/cbmc/incomplete-structs/typesmain.c

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

regression/cbmc/return6/test.desc

@@ -0,0 +1,11 @@
+CORE
+../../cbmc/Linking7/main.c
+../../cbmc/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/chain.sh

@@ -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;
+          });
+        }
       }
     }
   }

regression/linking-goto-binaries/type_conflicts/member-name-mismatch.desc

@@ -21,12 +21,77 @@ Author: Daniel Kroening, [email protected]
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
 #include <util/simplify_expr.h>
+#include <util/std_code.h>
 #include <util/symbol_table.h>
 
 #include <langapi/language_util.h>
 
 #include "linking_class.h"
 
+bool casting_replace_symbolt::replace(exprt &dest) const
+{
+  bool result = true; // unchanged
+
+  // first look at type
+
+  const exprt &const_dest(dest);
+  if(have_to_replace(const_dest.type()))
+    if(!replace_symbolt::replace(dest.type()))
+      result = false;
+
+  // now do expression itself
+
+  if(!have_to_replace(dest))
+    return result;
+
+  if(dest.id() == ID_side_effect)
+  {
+    if(auto call = expr_try_dynamic_cast<side_effect_expr_function_callt>(dest))
+    {
+      if(!have_to_replace(call->function()))
+        return replace_symbolt::replace(dest);
+
+      exprt before = dest;
+      code_typet type = to_code_type(call->function().type());
+
+      result &= replace_symbolt::replace(call->function());
+
+      // maybe add type casts here?
+      for(auto &arg : call->arguments())
+        result &= replace_symbolt::replace(arg);
+
+      if(
+        type.return_type() !=
+        to_code_type(call->function().type()).return_type())
+      {
+        call->type() = to_code_type(call->function().type()).return_type();
+        dest = typecast_exprt(*call, type.return_type());
+        result = true;
+      }
+
+      return result;
+    }
+  }
+  else if(dest.id() == ID_address_of)
+  {
+    pointer_typet ptr_type = to_pointer_type(dest.type());
+
+    result &= replace_symbolt::replace(dest);
+
+    address_of_exprt address_of = to_address_of_expr(dest);
+    if(address_of.object().type() != ptr_type.subtype())
+    {
+      to_pointer_type(address_of.type()).subtype() = address_of.object().type();
+      dest = typecast_exprt(address_of, ptr_type);
+      result = true;
+    }
+
+    return result;
+  }
+
+  return replace_symbolt::replace(dest);
+}
+
 bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
 {
   expr_mapt::const_iterator it = expr_map.find(s.get_identifier());
@@ -36,7 +101,7 @@ bool casting_replace_symbolt::replace_symbol_expr(symbol_exprt &s) const
 
   const exprt &e = it->second;
 
-  if(e.type().id() != ID_array)
+  if(e.type().id() != ID_array && e.type().id() != ID_code)
   {
     typet type = s.type();
     static_cast<exprt &>(s) = typecast_exprt::conditional_cast(e, type);
@@ -480,22 +545,9 @@ void linkingt::duplicate_code_symbol(
     const code_typet &old_t=to_code_type(old_symbol.type);
     const code_typet &new_t=to_code_type(new_symbol.type);
 
-    // if one of them was an implicit declaration then only conflicts on the
-    // return type are an error as we would end up with assignments with
-    // mismatching types; as we currently do not patch these by inserting type
-    // casts we need to fail hard
     if(old_symbol.type.get_bool(ID_C_incomplete) && old_symbol.value.is_nil())
     {
-      if(base_type_eq(old_t.return_type(), new_t.return_type(), ns))
-         link_warning(
-           old_symbol,
-           new_symbol,
-           "implicit function declaration");
-      else
-        link_error(
-          old_symbol,
-          new_symbol,
-          "implicit function declaration");
+      link_warning(old_symbol, new_symbol, "implicit function declaration");
 
       old_symbol.type=new_symbol.type;
       old_symbol.location=new_symbol.location;
@@ -504,24 +556,15 @@ void linkingt::duplicate_code_symbol(
     else if(
       new_symbol.type.get_bool(ID_C_incomplete) && new_symbol.value.is_nil())
     {
-      if(base_type_eq(old_t.return_type(), new_t.return_type(), ns))
-        link_warning(
-          old_symbol,
-          new_symbol,
-          "ignoring conflicting implicit function declaration");
-      else
-        link_error(
-          old_symbol,
-          new_symbol,
-          "implicit function declaration");
+      link_warning(
+        old_symbol,
+        new_symbol,
+        "ignoring conflicting implicit function declaration");
     }
     // handle (incomplete) function prototypes
-    else if(base_type_eq(old_t.return_type(), new_t.return_type(), ns) &&
-            ((old_t.parameters().empty() &&
-              old_t.has_ellipsis() &&
+    else if(((old_t.parameters().empty() && old_t.has_ellipsis() &&
               old_symbol.value.is_nil()) ||
-             (new_t.parameters().empty() &&
-              new_t.has_ellipsis() &&
+             (new_t.parameters().empty() && new_t.has_ellipsis() &&
               new_symbol.value.is_nil())))
     {
       if(old_t.parameters().empty() &&
@@ -572,9 +615,7 @@ void linkingt::duplicate_code_symbol(
     }
     // conflicting declarations without a definition, matching return
     // types
-    else if(base_type_eq(old_t.return_type(), new_t.return_type(), ns) &&
-            old_symbol.value.is_nil() &&
-            new_symbol.value.is_nil())
+    else if(old_symbol.value.is_nil() && new_symbol.value.is_nil())
     {
       link_warning(
         old_symbol,
@@ -614,8 +655,11 @@ void linkingt::duplicate_code_symbol(
       conflictst conflicts;
 
       if(!base_type_eq(old_t.return_type(), new_t.return_type(), ns))
-        conflicts.push_back(
-          std::make_pair(old_t.return_type(), new_t.return_type()));
+      {
+        link_warning(old_symbol, new_symbol, "conflicting return types");
+
+        conflicts.emplace_back(old_t.return_type(), new_t.return_type());
+      }
 
       code_typet::parameterst::const_iterator
         n_it=new_t.parameters().begin(),
@@ -665,21 +709,11 @@ void linkingt::duplicate_code_symbol(
         const typet &t1=follow_tags_symbols(ns, conflicts.front().first);
         const typet &t2=follow_tags_symbols(ns, conflicts.front().second);
 
-        // void vs. non-void return type may be acceptable if the
-        // return value is never used
-        if((t1.id()==ID_empty || t2.id()==ID_empty) &&
-           (old_symbol.value.is_nil() || new_symbol.value.is_nil()))
-        {
-          if(warn_msg.empty())
-            warn_msg="void/non-void return type conflict on function";
-          replace=
-            new_symbol.value.is_not_nil() ||
-            (old_symbol.value.is_nil() && t2.id()==ID_empty);
-        }
         // different pointer arguments without implementation may work
-        else if((t1.id()==ID_pointer || t2.id()==ID_pointer) &&
-                pointer_offset_bits(t1, ns)==pointer_offset_bits(t2, ns) &&
-                old_symbol.value.is_nil() && new_symbol.value.is_nil())
+        if(
+          (t1.id() == ID_pointer || t2.id() == ID_pointer) &&
+          pointer_offset_bits(t1, ns) == pointer_offset_bits(t2, ns) &&
+          old_symbol.value.is_nil() && new_symbol.value.is_nil())
         {
           if(warn_msg.empty())
             warn_msg="different pointer types in extern function";
@@ -782,6 +816,9 @@ void linkingt::duplicate_code_symbol(
         }
       }
     }
+
+    object_type_updates.insert(
+      old_symbol.symbol_expr(), old_symbol.symbol_expr());
   }
 
   if(!new_symbol.value.is_nil())
@@ -796,6 +833,11 @@ void linkingt::duplicate_code_symbol(
       old_symbol.is_weak=new_symbol.is_weak;
       old_symbol.location=new_symbol.location;
       old_symbol.is_macro=new_symbol.is_macro;
+
+      // replace any previous update
+      object_type_updates.erase(old_symbol.name);
+      object_type_updates.insert(
+        old_symbol.symbol_expr(), old_symbol.symbol_expr());
     }
     else if(to_code_type(old_symbol.type).get_inlined())
     {

regression/linking-goto-binaries/type_conflicts/return_type.desc

@@ -21,6 +21,9 @@ Author: Daniel Kroening, [email protected]
 
 class casting_replace_symbolt : public replace_symbolt
 {
+public:
+  bool replace(exprt &dest) const override;
+
 private:
   bool replace_symbol_expr(symbol_exprt &dest) const override;
 };