Improving linker warning diagnostics

We previously just reported pointer type conflicts without elaborating
what the exact difference was. To produce type-consistent goto programs,
we chose to use the type that the definition had, but lacked any test
that doing so would actually result in a program that can be analysed
successfully.

This commit fixes bugs in the code producing diagnostics, enables
diagnostics for the case of pointer type conflicts, and adds a test to
demonstrate that we successfully analyse programs after type conflict
resolution. Despite this, however, inconsistencies in the goto program
remain: the call types still need fixing up.

Fixes: #198

Author: tautschnig

regression/ansi-c/incomplete-structs/test.desc

@@ -0,0 +1,12 @@
+CORE
+typesmain.c
+types1.c types2.c types3.c --verbosity 2
+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"
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ansi-c/incomplete-structs/types1.c

@@ -0,0 +1,9 @@
+struct S
+{
+  int s;
+} s_object;
+
+int foobar()
+{
+  return s_object.s;
+}

regression/ansi-c/incomplete-structs/types2.c

@@ -0,0 +1,16 @@
+struct S
+{
+  struct T *t;
+  struct U *u;
+};
+
+struct U
+{
+  struct S *s;
+  int j;
+};
+
+int bar(struct S *s)
+{
+  return s->u->j;
+}

regression/ansi-c/incomplete-structs/types3.c

@@ -0,0 +1,17 @@
+struct T
+{
+  int i;
+};
+
+struct S
+{
+  struct T *t;
+  struct U *u;
+};
+
+int bar(struct S *);
+
+int foo(struct S *s)
+{
+  return bar(s) + s->t->i;
+}

regression/ansi-c/incomplete-structs/typesmain.c

@@ -0,0 +1,29 @@
+#include <assert.h>
+
+struct T
+{
+  int i;
+};
+
+struct U
+{
+  struct S *s;
+  int j;
+};
+
+struct S
+{
+  struct T *t;
+  struct U *u;
+};
+
+int foo(struct S *s);
+
+int main()
+{
+  struct T t = {10};
+  struct U u = {0, 32};
+  struct S s = {&t, &u};
+  int res = foo(&s);
+  assert(res == 42);
+}

src/linking/linking.cpp

@@ -126,25 +126,30 @@ std::string linkingt::type_to_string_verbose(
   return type_to_string(symbol.name, type);
 }
 
-void linkingt::detailed_conflict_report_rec(
+bool linkingt::detailed_conflict_report_rec(
   const symbolt &old_symbol,
   const symbolt &new_symbol,
   const typet &type1,
   const typet &type2,
   unsigned depth,
   exprt &conflict_path)
 {
-  #ifdef DEBUG
+  bool conclusive = false;
+
+#ifdef DEBUG
   debug() << "<BEGIN DEPTH " << depth << ">" << eom;
-  #endif
+#endif
 
   std::string msg;
 
   const typet &t1=follow_tags_symbols(ns, type1);
   const typet &t2=follow_tags_symbols(ns, type2);
 
   if(t1.id()!=t2.id())
+  {
     msg="type classes differ";
+    conclusive = true;
+  }
   else if(t1.id()==ID_pointer ||
           t1.id()==ID_array)
   {
@@ -155,7 +160,7 @@ void linkingt::detailed_conflict_report_rec(
       if(conflict_path.type().id() == ID_pointer)
         conflict_path = dereference_exprt(conflict_path);
 
-      detailed_conflict_report_rec(
+      conclusive = detailed_conflict_report_rec(
         old_symbol,
         new_symbol,
         to_type_with_subtype(t1).subtype(),
@@ -184,6 +189,7 @@ void linkingt::detailed_conflict_report_rec(
       msg="number of members is different (";
       msg+=std::to_string(components1.size())+'/';
       msg+=std::to_string(components2.size())+')';
+      conclusive = true;
     }
     else
     {
@@ -197,7 +203,7 @@ void linkingt::detailed_conflict_report_rec(
           msg="names of member "+std::to_string(i)+" differ (";
           msg+=id2string(components1[i].get_name())+'/';
           msg+=id2string(components2[i].get_name())+')';
-          break;
+          conclusive = true;
         }
         else if(subtype1 != subtype2)
         {
@@ -210,6 +216,7 @@ void linkingt::detailed_conflict_report_rec(
                 e.id()==ID_index)
           {
             parent_types.insert(e.type());
+            parent_types.insert(follow_tags_symbols(ns, e.type()));
             if(e.id() == ID_dereference)
               e = to_dereference_expr(e).pointer();
             else if(e.id() == ID_member)
@@ -220,44 +227,32 @@ void linkingt::detailed_conflict_report_rec(
               UNREACHABLE;
           }
 
-          conflict_path=conflict_path_before;
-          conflict_path.type()=t1;
-          conflict_path=
-            member_exprt(conflict_path, components1[i]);
-
-          if(depth>0 &&
-             parent_types.find(t1)==parent_types.end())
-            detailed_conflict_report_rec(
-              old_symbol,
-              new_symbol,
-              subtype1,
-              subtype2,
-              depth-1,
-              conflict_path);
-          else
+          if(parent_types.find(subtype1) == parent_types.end())
           {
-            msg="type of member "+
-                id2string(components1[i].get_name())+
-                " differs";
-            if(depth>0)
+            conflict_path = conflict_path_before;
+            conflict_path.type() = t1;
+            conflict_path = member_exprt(conflict_path, components1[i]);
+
+            if(depth > 0)
             {
-              std::string msg_bak;
-              msg_bak.swap(msg);
-              symbol_exprt c = symbol_exprt::typeless(ID_C_this);
-              detailed_conflict_report_rec(
+              conclusive = detailed_conflict_report_rec(
                 old_symbol,
                 new_symbol,
                 subtype1,
                 subtype2,
-                depth-1,
-                c);
-              msg.swap(msg_bak);
+                depth - 1,
+                conflict_path);
             }
           }
-
-          if(parent_types.find(t1)==parent_types.end())
-            break;
+          else
+          {
+            msg = "type of member " + id2string(components1[i].get_name()) +
+                  " differs (recursive)";
+          }
         }
+
+        if(conclusive)
+          break;
       }
     }
   }
@@ -280,12 +275,14 @@ void linkingt::detailed_conflict_report_rec(
       msg +=
         type_to_string(new_symbol.name, to_c_enum_type(t2).underlying_type()) +
         ')';
+      conclusive = true;
     }
     else if(members1.size()!=members2.size())
     {
       msg="number of enum members is different (";
       msg+=std::to_string(members1.size())+'/';
       msg+=std::to_string(members2.size())+')';
+      conclusive = true;
     }
     else
     {
@@ -296,15 +293,18 @@ void linkingt::detailed_conflict_report_rec(
           msg="names of member "+std::to_string(i)+" differ (";
           msg+=id2string(members1[i].get_base_name())+'/';
           msg+=id2string(members2[i].get_base_name())+')';
-          break;
+          conclusive = true;
         }
         else if(members1[i].get_value()!=members2[i].get_value())
         {
           msg="values of member "+std::to_string(i)+" differ (";
           msg+=id2string(members1[i].get_value())+'/';
           msg+=id2string(members2[i].get_value())+')';
-          break;
+          conclusive = true;
         }
+
+        if(conclusive)
+          break;
       }
     }
 
@@ -328,21 +328,25 @@ void linkingt::detailed_conflict_report_rec(
       msg="parameter counts differ (";
       msg+=std::to_string(parameters1.size())+'/';
       msg+=std::to_string(parameters2.size())+')';
+      conclusive = true;
     }
     else if(return_type1 != return_type2)
     {
+      conflict_path.type() = array_typet{void_type(), nil_exprt{}};
       conflict_path=
         index_exprt(conflict_path,
                     constant_exprt(std::to_string(-1), integer_typet()));
 
       if(depth>0)
-        detailed_conflict_report_rec(
+      {
+        conclusive = detailed_conflict_report_rec(
           old_symbol,
           new_symbol,
           return_type1,
           return_type2,
-          depth-1,
+          depth - 1,
           conflict_path);
+      }
       else
         msg="return types differ";
     }
@@ -355,30 +359,37 @@ void linkingt::detailed_conflict_report_rec(
 
         if(subtype1 != subtype2)
         {
+          conflict_path.type() = array_typet{void_type(), nil_exprt{}};
           conflict_path=
             index_exprt(conflict_path,
                         constant_exprt(std::to_string(i), integer_typet()));
 
           if(depth>0)
-            detailed_conflict_report_rec(
+          {
+            conclusive = detailed_conflict_report_rec(
               old_symbol,
               new_symbol,
               subtype1,
               subtype2,
-              depth-1,
+              depth - 1,
               conflict_path);
+          }
           else
             msg="parameter types differ";
+        }
 
+        if(conclusive)
           break;
-        }
       }
     }
   }
   else
+  {
     msg="conflict on POD";
+    conclusive = true;
+  }
 
-  if(!msg.empty())
+  if(conclusive && !msg.empty())
   {
     error() << '\n';
     error() << "reason for conflict at "
@@ -392,6 +403,8 @@ void linkingt::detailed_conflict_report_rec(
   #ifdef DEBUG
   debug() << "<END DEPTH " << depth << ">" << eom;
   #endif
+
+  return conclusive;
 }
 
 void linkingt::link_error(
@@ -685,8 +698,16 @@ void linkingt::duplicate_code_symbol(
                 old_symbol.value.is_nil()!=new_symbol.value.is_nil())
         {
           if(warn_msg.empty())
+          {
             warn_msg="pointer parameter types differ between "
                      "declaration and definition";
+            detailed_conflict_report(
+              old_symbol,
+              new_symbol,
+              conflicts.front().first,
+              conflicts.front().second);
+          }
+
           replace=new_symbol.value.is_not_nil();
         }
         // transparent union with (or entirely without) implementation is

src/linking/linking_class.h

@@ -131,7 +131,10 @@ class linkingt:public typecheckt
     return type_to_string_verbose(symbol, symbol.type);
   }
 
-  void detailed_conflict_report_rec(
+  /// Returns true iff the conflict report on a particular branch of the tree of
+  /// types was a definitive result, and not contingent on conflicts within a
+  /// tag type.
+  bool detailed_conflict_report_rec(
     const symbolt &old_symbol,
     const symbolt &new_symbol,
     const typet &type1,