[SV-COMP'18 11/19] invalid_object(pointer) is true for all non-existent objects

src/goto-symex/symex_builtin_functions.cpp

@@ -194,17 +194,20 @@ void goto_symext::symex_allocate(
 
   exprt rhs;
 
+  symbol_exprt value_expr=value_symbol.symbol_expr();
+  value_expr.add(ID_C_dynamic_guard, state.guard);
+
   if(object_type->id() == ID_array)
   {
     const auto &array_type = to_array_type(*object_type);
     index_exprt index_expr(
-      value_symbol.symbol_expr(), from_integer(0, index_type()));
+      value_expr, 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));
+      value_expr, pointer_type(value_symbol.type));
   }
 
   symex_assign(

src/solvers/flattening/bv_pointers.cpp

@@ -27,32 +27,25 @@ 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);
+      // condition can only be evaluated once all (address-taken)
+      // objects are known, thus 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_is_dynamic_object)
   {
     if(operands.size()==1 &&
        operands[0].type().id()==ID_pointer)
     {
-      // we postpone
+      // condition can only be evaluated once all (address-taken)
+      // objects are known, thus postpone
       literalt l=prop.new_variable();
 
       postponed_list.push_back(postponedt());
@@ -813,6 +806,82 @@ void bv_pointerst::do_postponed(
       prop.l_set_to_true(prop.limplies(l1, l2));
     }
   }
+  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));
+
+    // the pointer is invalid if its object part compares equal to
+    // any of the object parts of dynamic objects that have *not*
+    // been allocated (as their path condition, stored in
+    // ID_C_dynamic_guard, evaluates to false)
+    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);
+      POSTCONDITION(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(ID_C_dynamic_guard));
+
+      if(guard.is_nil())
+        continue;
+
+      const bvt &guard_bv=convert_bv(guard);
+      DATA_INVARIANT(guard_bv.size()==1, "guard expected to be Boolean");
+      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);
+    POSTCONDITION(bv.size()==saved_bv.size());
+
+    disj.push_back(
+      bv_utils.rel(
+        saved_bv, ID_ge, bv, bv_utilst::representationt::UNSIGNED));
+
+    PRECONDITION(postponed.bv.size()==1);
+    literalt l=postponed.bv.front();
+    prop.l_set_to(prop.lequal(prop.lor(disj), l), true);
+  }
   else
     UNREACHABLE;
 }

src/util/irep_ids.def

@@ -841,6 +841,11 @@ IREP_ID_ONE(statement_list_instructions)
 IREP_ID_ONE(max)
 IREP_ID_ONE(min)
 IREP_ID_ONE(constant_interval)
+// dynamic objects get created during symbolic execution, but need
+// not ever exist on any feasible path; use ID_C_dynamic_guard to
+// store the path condition corresponding to the creation of a
+// dynamic object
+IREP_ID_TWO(C_dynamic_guard, #dynamic_guard)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree