Fix SSA assert construction

CBMC 5.8 added FALSE || to the beginning of instrumented assertions
which revealed a flaw in how the assertions were constructed in 2LS.
Make the approach more general, recursively going through the whole
assertion.

Signed-off-by: František Nečas <[email protected]>

Author: FrNecas

src/ssa/local_ssa.cpp

@@ -537,37 +537,58 @@ void local_SSAt::build_guard(locationt loc)
   (--nodes.end())->equalities.push_back(equality);
 }
 
-/// turns assertions into constraints
-void local_SSAt::build_assertions(locationt loc)
+/// Recursively go through expr and look for an equality with a pointer
+/// object on the right side and construct a disjunct of possible
+/// concrete assignments.
+bool local_SSAt::get_deallocated_disjunction(const exprt &expr, exprt &result)
 {
-  if(loc->is_assert())
+  if(expr.id()==ID_equal && expr.op1().id()==ID_pointer_object &&
+     expr.op1().op0().id()==ID_symbol)
   {
-    exprt assert=loc->guard;
-    if(assert.id()==ID_not && assert.op0().id()==ID_equal &&
-       assert.op0().op1().id()==ID_pointer_object &&
-       assert.op0().op1().op0().id()==ID_symbol)
+    std::string id=id2string(
+      to_symbol_expr(expr.op1().op0()).get_identifier());
+    if(id.find("__CPROVER_deallocated")!=std::string::npos)
     {
-      std::string id=id2string(
-        to_symbol_expr(assert.op0().op1().op0()).get_identifier());
-      if(id.find("__CPROVER_deallocated")!=std::string::npos)
+      const exprt &dealloc_symbol=expr.op1().op0();
+      exprt::operandst d;
+      for(auto &global : assignments.ssa_objects.globals)
       {
-        const exprt &dealloc_symbol=assert.op0().op1().op0();
-        exprt::operandst d;
-        for(auto &global : assignments.ssa_objects.globals)
+        if(global.get_expr().get_bool("#concrete"))
         {
-          if(global.get_expr().get_bool("#concrete"))
-          {
-            d.push_back(
-              equal_exprt(
-                dealloc_symbol,
-                typecast_exprt(
-                  address_of_exprt(global.symbol_expr()),
-                  dealloc_symbol.type())));
-          }
+          d.push_back(
+            equal_exprt(
+              dealloc_symbol,
+              typecast_exprt(
+                address_of_exprt(global.symbol_expr()),
+                dealloc_symbol.type())));
         }
-        assert=implies_exprt(disjunction(d), assert);
       }
+      result=disjunction(d);
+      return true;
     }
+  }
+  else
+  {
+    // Recursively go through the operands
+    if(!expr.has_operands())
+      return false;
+    else
+      for(const exprt &op : expr.operands())
+        if(get_deallocated_disjunction(op, result))
+          return true;
+  }
+  return false;
+}
+
+/// turns assertions into constraints
+void local_SSAt::build_assertions(locationt loc)
+{
+  if(loc->is_assert())
+  {
+    exprt assert=loc->guard;
+    exprt antecedent;
+    if(get_deallocated_disjunction(assert, antecedent))
+      assert=implies_exprt(antecedent, assert);
 
     const exprt deref_rhs=dereference(assert, loc);
 

src/ssa/local_ssa.h

@@ -281,6 +281,7 @@ class local_SSAt
   void build_cond(locationt loc);
   void build_guard(locationt loc);
   void build_function_call(locationt loc);
+  bool get_deallocated_disjunction(const exprt &expr, exprt &result);
   void build_assertions(locationt loc);
   void build_unknown_objs(locationt loc);
 

src/ssa/malloc_ssa.cpp

@@ -93,6 +93,8 @@ std::vector<exprt> collect_pointer_vars(
   std::vector<exprt> pointers;
   forall_symbols(it, symbol_table.symbols)
   {
+    if(it->second.is_type)
+      continue;
     if(ns.follow(it->second.type).id()==ID_struct)
     {
       for(auto &component : to_struct_type(