Fix a bug where dynamic objects' dependency across function call is not recognized [depends-on: #2646]

regression/goto-instrument/slice19/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --full-slice
 ^EXIT=0$

regression/goto-instrument/slice24/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+#include <stdlib.h>
+
+static void f(int *x) { *x = 5; }
+static void g(int *x) { assert(*x == 5); }
+
+int main(int argc, char **argv)
+{
+  int *x = (int*)malloc(sizeof(int));
+  f(x);
+  g(x);
+
+  return 0;
+}

regression/goto-instrument/slice24/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--full-slice --add-library
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+Data dependencies across function calls are still not working correctly.

src/analyses/dependence_graph.cpp

@@ -175,7 +175,9 @@ void dep_graph_domaint::data_dependencies(
     {
       bool found=false;
       for(const auto &wr : w_range.second)
+      {
         for(const auto &r_range : r_ranges)
+        {
           if(!found &&
              may_be_def_use_pair(wr.first, wr.second,
                                  r_range.first, r_range.second))
@@ -184,6 +186,8 @@ void dep_graph_domaint::data_dependencies(
             data_deps.insert(w_range.first);
             found=true;
           }
+        }
+      }
     }
 
     dep_graph.reaching_definitions()[to].clear_cache(it->first);

src/analyses/goto_rw.cpp

@@ -128,8 +128,6 @@ void rw_range_sett::get_objects_dereference(
 {
   const exprt &pointer=deref.pointer();
   get_objects_rec(get_modet::READ, pointer);
-  if(mode!=get_modet::READ)
-    get_objects_rec(mode, pointer);
 }
 
 void rw_range_sett::get_objects_byte_extract(
@@ -414,16 +412,19 @@ void rw_range_sett::get_objects_typecast(
 
 void rw_range_sett::get_objects_address_of(const exprt &object)
 {
-  if(object.id() == ID_string_constant ||
+  if(object.id() == ID_symbol ||
+     object.id() == ID_string_constant ||
      object.id() == ID_label ||
      object.id() == ID_array ||
      object.id() == ID_null_object)
     // constant, nothing to do
+  {
     return;
-  else if(object.id()==ID_symbol)
-    get_objects_rec(get_modet::READ, object);
+  }
   else if(object.id()==ID_dereference)
+  {
     get_objects_rec(get_modet::READ, object);
+  }
   else if(object.id()==ID_index)
   {
     const index_exprt &index=to_index_expr(object);
@@ -524,6 +525,11 @@ void rw_range_sett::get_objects_rec(
     get_objects_array(mode, to_array_expr(expr), range_start, size);
   else if(expr.id()==ID_struct)
     get_objects_struct(mode, to_struct_expr(expr), range_start, size);
+  else if(expr.id()==ID_dynamic_object)
+  {
+    const auto obj_instance = to_dynamic_object_expr(expr).get_instance();
+    add(mode, "goto_rw::dynamic_object-" + std::to_string(obj_instance), 0, -1);
+  }
   else if(expr.id()==ID_symbol)
   {
     const symbol_exprt &symbol=to_symbol_expr(expr);
@@ -564,11 +570,6 @@ void rw_range_sett::get_objects_rec(
   {
     // dereferencing may yield some weird ones, ignore these
   }
-  else if(mode==get_modet::LHS_W)
-  {
-    forall_operands(it, expr)
-      get_objects_rec(mode, *it);
-  }
   else
     throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled";
 }
@@ -605,6 +606,8 @@ void rw_range_set_value_sett::get_objects_dereference(
   exprt object=deref;
   dereference(target, object, ns, value_sets);
 
+  PRECONDITION(object.is_not_nil());
+
   range_spect new_size=
     to_range_spect(pointer_offset_bits(object.type(), ns));
 

src/analyses/reaching_definitions.cpp

@@ -186,7 +186,8 @@ void rd_range_domaint::transform_function_call(
       const symbolt *sym;
       if((ns.lookup(identifier, sym) ||
           !sym->is_shared()) &&
-         !rd.get_is_dirty()(identifier))
+         !rd.get_is_dirty()(identifier) &&
+         !has_prefix(id2string(identifier), "goto_rw::dynamic_object"))
       {
         export_cache.erase(identifier);
 
@@ -307,19 +308,19 @@ void rd_range_domaint::transform_assign(
   {
     const irep_idt &identifier=it->first;
     // ignore symex::invalid_object
-    const symbolt *symbol_ptr;
-    if(ns.lookup(identifier, symbol_ptr))
+    const symbolt *symbol_ptr = nullptr;
+    bool not_found = ns.lookup(identifier, symbol_ptr);
+    if(not_found && has_prefix(id2string(identifier), "symex::invalid_object"))
+    {
       continue;
-    INVARIANT_STRUCTURED(
-      symbol_ptr!=nullptr,
-      nullptr_exceptiont,
-      "Symbol is in symbol table");
+    }
 
     const range_domaint &ranges=rw_set.get_ranges(it);
 
     if(is_must_alias &&
        (!rd.get_is_threaded()(from) ||
-        (!symbol_ptr->is_shared() &&
+        (symbol_ptr != nullptr &&
+         symbol_ptr->is_shared() &&
          !rd.get_is_dirty()(identifier))))
       for(const auto &range : ranges)
         kill(identifier, range.first, range.second);

src/ansi-c/c_typecheck_expr.cpp

@@ -2141,7 +2141,7 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    exprt dynamic_object_expr=exprt(ID_dynamic_object, expr.type());
+    exprt dynamic_object_expr=exprt(ID_is_dynamic_object, expr.type());
     dynamic_object_expr.operands()=expr.arguments();
     dynamic_object_expr.add_source_location()=source_location;
 

src/ansi-c/expr2c.cpp

@@ -3580,8 +3580,8 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_invalid_pointer)
     return convert_function(src, "__CPROVER_invalid_pointer", precedence=16);
 
-  else if(src.id()==ID_dynamic_object)
-    return convert_function(src, "DYNAMIC_OBJECT", precedence=16);
+  else if(src.id()==ID_is_dynamic_object)
+    return convert_function(src, "IS_DYNAMIC_OBJECT", precedence=16);
 
   else if(src.id()=="is_zero_string")
     return convert_function(src, "IS_ZERO_STRING", precedence=16);

src/pointer-analysis/value_set_dereference.cpp

@@ -358,8 +358,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
     // this is also our guard
     result.pointer_guard = dynamic_object(pointer_expr);
 
-    // can't remove here, turn into *p
-    result.value=dereference_exprt(pointer_expr, dereference_type);
+    // TODO should this be object or root_object?
+    // TODO It's unclear whether this is a good approach to take --- it
+    // successfully ensures that every (non-null) dereference points to
+    // something, making the write set computation work correctly, but dynamic
+    // objects do not seem to be intended to be used in this way.
+    result.value = object;
 
     if(options.get_bool_option("pointer-check"))
     {

src/solvers/flattening/bv_pointers.cpp

@@ -45,21 +45,21 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
       }
     }
   }
-  else if(expr.id()==ID_dynamic_object)
+  else if(expr.id()==ID_is_dynamic_object)
   {
-    if(operands.size()==1 &&
-       operands[0].type().id()==ID_pointer)
-    {
-      // we postpone
-      literalt l=prop.new_variable();
+    DATA_INVARIANT(operands.size() == 1 &&
+                   operands[0].type().id() == ID_pointer,
+                   std::string("is_dynamic_object_exprt should have one") +
+                   "operand, which should have pointer type.");
+    // we postpone
+    literalt l=prop.new_variable();
 
-      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;
+    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 l;
-    }
+    return l;
   }
   else if(expr.id()==ID_lt || expr.id()==ID_le ||
           expr.id()==ID_gt || expr.id()==ID_ge)
@@ -735,7 +735,7 @@ void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
 void bv_pointerst::do_postponed(
   const postponedt &postponed)
 {
-  if(postponed.expr.id()==ID_dynamic_object)
+  if(postponed.expr.id()==ID_is_dynamic_object)
   {
     const pointer_logict::objectst &objects=
       pointer_logic.objects;

src/solvers/smt2/smt2_conv.cpp

@@ -1367,7 +1367,7 @@ void smt2_convt::convert_expr(const exprt &expr)
     if(ext>0)
       out << ")"; // zero_extend
   }
-  else if(expr.id()==ID_dynamic_object)
+  else if(expr.id()==ID_is_dynamic_object)
   {
     convert_is_dynamic_object(expr);
   }

src/util/irep_ids.def

@@ -448,6 +448,7 @@ IREP_ID_TWO(overflow_minus, overflow--)
 IREP_ID_TWO(overflow_mult, overflow-*)
 IREP_ID_TWO(overflow_unary_minus, overflow-unary-)
 IREP_ID_ONE(object_descriptor)
+IREP_ID_ONE(is_dynamic_object)
 IREP_ID_ONE(dynamic_object)
 IREP_ID_TWO(C_dynamic, #dynamic)
 IREP_ID_ONE(object_size)

src/util/pointer_predicates.cpp

@@ -70,7 +70,7 @@ exprt dynamic_size(const namespacet &ns)
 
 exprt dynamic_object(const exprt &pointer)
 {
-  exprt dynamic_expr(ID_dynamic_object, bool_typet());
+  exprt dynamic_expr(ID_is_dynamic_object, bool_typet());
   dynamic_expr.copy_to_operands(pointer);
   return dynamic_expr;
 }

src/util/simplify_expr.cpp

@@ -2266,8 +2266,8 @@ bool simplify_exprt::simplify_node(exprt &expr)
     result=simplify_byte_extract(to_byte_extract_expr(expr)) && result;
   else if(expr.id()==ID_pointer_object)
     result=simplify_pointer_object(expr) && result;
-  else if(expr.id()==ID_dynamic_object)
-    result=simplify_dynamic_object(expr) && result;
+  else if(expr.id()==ID_is_dynamic_object)
+    result=simplify_is_dynamic_object(expr) && result;
   else if(expr.id()==ID_invalid_pointer)
     result=simplify_invalid_pointer(expr) && result;
   else if(expr.id()==ID_object_size)

src/util/simplify_expr_class.h

@@ -96,7 +96,7 @@ class simplify_exprt
   bool simplify_pointer_object(exprt &expr);
   bool simplify_object_size(exprt &expr);
   bool simplify_dynamic_size(exprt &expr);
-  bool simplify_dynamic_object(exprt &expr);
+  bool simplify_is_dynamic_object(exprt &expr);
   bool simplify_invalid_pointer(exprt &expr);
   bool simplify_same_object(exprt &expr);
   bool simplify_good_pointer(exprt &expr);

src/util/simplify_expr_int.cpp

@@ -1699,7 +1699,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
          expr.op0().operands().size()==1)
       {
         if(expr.op0().op0().id()==ID_symbol ||
-           expr.op0().op0().id()==ID_dynamic_object ||
+           expr.op0().op0().id()==ID_is_dynamic_object ||
            expr.op0().op0().id()==ID_member ||
            expr.op0().op0().id()==ID_index ||
            expr.op0().op0().id()==ID_string_constant)
@@ -1715,7 +1715,7 @@ bool simplify_exprt::simplify_inequality_constant(exprt &expr)
               expr.op0().op0().operands().size()==1)
       {
         if(expr.op0().op0().op0().id()==ID_symbol ||
-           expr.op0().op0().op0().id()==ID_dynamic_object ||
+           expr.op0().op0().op0().id()==ID_is_dynamic_object ||
            expr.op0().op0().op0().id()==ID_member ||
            expr.op0().op0().op0().id()==ID_index ||
            expr.op0().op0().op0().id()==ID_string_constant)

src/util/simplify_expr_pointer.cpp

@@ -464,7 +464,7 @@ bool simplify_exprt::simplify_inequality_pointer_object(exprt &expr)
     {
       if(op.operands().size()!=1 ||
          (op.op0().id()!=ID_symbol &&
-          op.op0().id()!=ID_dynamic_object &&
+          op.op0().id()!=ID_is_dynamic_object &&
           op.op0().id()!=ID_string_constant))
         return true;
     }
@@ -508,18 +508,20 @@ bool simplify_exprt::simplify_pointer_object(exprt &expr)
   return result;
 }
 
-bool simplify_exprt::simplify_dynamic_object(exprt &expr)
+bool simplify_exprt::simplify_is_dynamic_object(exprt &expr)
 {
-  if(expr.operands().size()!=1)
-    return true;
+  DATA_INVARIANT(expr.operands().size() == 1 &&
+                 expr.op0().type().id() == ID_pointer,
+                 std::string("is_dynamic_object_exprt should have one") +
+                 "operand, which should have pointer type.");
 
   exprt &op=expr.op0();
 
   if(op.id()==ID_if && op.operands().size()==3)
   {
     if_exprt if_expr=lift_if(expr, 0);
-    simplify_dynamic_object(if_expr.true_case());
-    simplify_dynamic_object(if_expr.false_case());
+    simplify_is_dynamic_object(if_expr.true_case());
+    simplify_is_dynamic_object(if_expr.false_case());
     simplify_if(if_expr);
     expr.swap(if_expr);
 

src/util/std_expr.h

@@ -2106,6 +2106,54 @@ inline void validate_expr(const dynamic_object_exprt &value)
 }
 
 
+/*! \brief Evaluates to true if the operand is a pointer to a dynamic object.
+*/
+class is_dynamic_object_exprt:public unary_predicate_exprt
+{
+public:
+  is_dynamic_object_exprt():unary_predicate_exprt(ID_is_dynamic_object)
+  {
+  }
+
+  explicit is_dynamic_object_exprt(const exprt &op):
+    unary_predicate_exprt(ID_is_dynamic_object, op)
+  {
+  }
+};
+
+/*! \brief Cast a generic exprt to a \ref is_dynamic_object_exprt
+ *
+ * This is an unchecked conversion. \a expr must be known to be \ref
+ * is_dynamic_object_exprt.
+ *
+ * \param expr Source expression
+ * \return Object of type \ref is_dynamic_object_exprt
+ *
+ * \ingroup gr_std_expr
+*/
+inline const is_dynamic_object_exprt &to_is_dynamic_object_expr(
+  const exprt &expr)
+{
+  PRECONDITION(expr.id()==ID_is_dynamic_object);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "is_dynamic_object must have one operand");
+  return static_cast<const is_dynamic_object_exprt &>(expr);
+}
+
+/*! \copydoc to_is_dynamic_object_expr(const exprt &)
+ * \ingroup gr_std_expr
+*/
+inline is_dynamic_object_exprt &to_is_dynamic_object_expr(exprt &expr)
+{
+  PRECONDITION(expr.id()==ID_is_dynamic_object);
+  DATA_INVARIANT(
+    expr.operands().size()==1,
+    "is_dynamic_object must have one operand");
+  return static_cast<is_dynamic_object_exprt &>(expr);
+}
+
+
 /*! \brief semantic type conversion
 */
 class typecast_exprt:public unary_exprt