invalid_object(pointer) is true for all non-existent objects

Check whether the object part of a pointer is greater or equal the total
number of objects, or equals a dynamic object that has not actually been
allocated on a given trace.

Author: tautschnig

src/goto-symex/symex_builtin_functions.cpp

@@ -184,18 +184,20 @@ void goto_symext::symex_allocate(
 
   exprt rhs;
 
+  symbol_exprt v=value_symbol.symbol_expr();
+  v.add("#dynamic_guard", state.guard);
+
   if(object_type.id()==ID_array)
   {
-    const auto &array_type = to_array_type(object_type);
+    const auto &array_type = to_array_type(value_symbol.type);
     index_exprt index_expr(array_type.subtype());
-    index_expr.array()=value_symbol.symbol_expr();
+    index_expr.array() = v;
     index_expr.index()=from_integer(0, index_type());
     rhs = address_of_exprt(index_expr, pointer_type(array_type.subtype()));
   }
   else
   {
-    rhs=address_of_exprt(
-      value_symbol.symbol_expr(), pointer_type(value_symbol.type));
+    rhs = address_of_exprt(v, pointer_type(value_symbol.type));
   }
 
   if(rhs.type()!=lhs.type())

src/solvers/flattening/bv_pointers.cpp

@@ -12,7 +12,11 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/exception_utils.h>
+#include <util/invariant.h>
 #include <util/pointer_offset_size.h>
+#include <util/prefix.h>
+#include <util/ssa_expr.h>
+#include <util/std_expr.h>
 
 literalt bv_pointerst::convert_rest(const exprt &expr)
 {
@@ -25,24 +29,15 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
     if(operands.size()==1 &&
        operands[0].type().id()==ID_pointer)
     {
-      const bvt &bv=convert_bv(operands[0]);
-
-      if(!bv.empty())
-      {
-        bvt invalid_bv;
-        encode(pointer_logic.get_invalid_object(), invalid_bv);
-
-        bvt equal_invalid_bv;
-        equal_invalid_bv.resize(object_bits);
+      // we postpone
+      literalt l=prop.new_variable();
 
-        for(std::size_t i=0; i<object_bits; i++)
-        {
-          equal_invalid_bv[i]=prop.lequal(bv[offset_bits+i],
-                                          invalid_bv[offset_bits+i]);
-        }
+      postponed_list.push_back(postponedt());
+      postponed_list.back().op=convert_bv(operands[0]);
+      postponed_list.back().bv.push_back(l);
+      postponed_list.back().expr=expr;
 
-        return prop.land(equal_invalid_bv);
-      }
+      return l;
     }
   }
   else if(expr.id()==ID_dynamic_object)
@@ -820,6 +815,78 @@ void bv_pointerst::do_postponed(
       prop.l_set_to(prop.limplies(l1, l2), true);
     }
   }
+  else if(postponed.expr.id()==ID_invalid_pointer)
+  {
+    const pointer_logict::objectst &objects=pointer_logic.objects;
+
+    bvt disj;
+    disj.reserve(objects.size());
+
+    bvt saved_bv=postponed.op;
+    saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
+
+    bvt invalid_bv, null_bv;
+    encode(pointer_logic.get_invalid_object(), invalid_bv);
+    invalid_bv.erase(invalid_bv.begin(), invalid_bv.begin()+offset_bits);
+    encode(pointer_logic.get_null_object(),    null_bv);
+    null_bv.erase(null_bv.begin(), null_bv.begin()+offset_bits);
+
+    disj.push_back(bv_utils.equal(saved_bv, invalid_bv));
+    disj.push_back(bv_utils.equal(saved_bv, null_bv));
+
+    // compare object part to non-allocated dynamic objects
+    std::size_t number=0;
+
+    for(pointer_logict::objectst::const_iterator
+        it=objects.begin();
+        it!=objects.end();
+        it++, number++)
+    {
+      const exprt &expr=*it;
+
+      if(!pointer_logic.is_dynamic_object(expr) ||
+         !is_ssa_expr(expr))
+        continue;
+
+      // only compare object part
+      bvt bv;
+      encode(number, bv);
+
+      bv.erase(bv.begin(), bv.begin()+offset_bits);
+      assert(bv.size()==saved_bv.size());
+
+      literalt l1=bv_utils.equal(bv, saved_bv);
+
+      const ssa_exprt &ssa=to_ssa_expr(expr);
+
+      const exprt &guard=
+        static_cast<const exprt&>(
+          ssa.get_original_expr().find("#dynamic_guard"));
+
+      if(guard.is_nil())
+        continue;
+
+      const bvt &guard_bv=convert_bv(guard);
+      assert(guard_bv.size()==1);
+      literalt l_guard=guard_bv[0];
+
+      disj.push_back(prop.land(!l_guard, l1));
+    }
+
+    // compare object part to max object number
+    bvt bv;
+    encode(number, bv);
+
+    bv.erase(bv.begin(), bv.begin()+offset_bits);
+    assert(bv.size()==saved_bv.size());
+
+    disj.push_back(
+      bv_utils.rel(saved_bv, ID_ge, bv, bv_utilst::representationt::UNSIGNED));
+
+    assert(postponed.bv.size()==1);
+    literalt l=postponed.bv.front();
+    prop.l_set_to(prop.lequal(prop.lor(disj), l), true);
+  }
   else
     UNREACHABLE;
 }