Fixes bugs making goto_rw too conservative

When handling the case of pointers, goto_rw would mark both the object pointed
to and the pointer itself as written. For example, if x = &i, the line `*x = 1'
would yield a write set containing both x and i, instead of just i.

This resolves that issue by ensuring that value_set_dereference always
gives at least one object that the dereference can refer to.

This also resolves a bug wherein &a is marked as reading from a by
removing the ID_symbol special case from get_objects_address_of.A

Author: klaas

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

@@ -307,19 +307,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/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"))
     {