goto-symex: expand unknown points-to values to all objects

Non-deterministic pointers should consider all possible objects.
goto-symex is aware of all current objects, and can thus expand
points-to values of "unknown" to all current objects (leaving the
pointer offset unconstrained).

Author: tautschnig

src/goto-symex/symex_dereference_state.cpp

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "symex_dereference_state.h"
 
+#include <util/pointer_expr.h>
 #include <util/symbol_table.h>
 
 /// Get or create a failed symbol for the given pointer-typed expression. These
@@ -80,5 +81,39 @@ symex_dereference_statet::get_or_create_failed_symbol(const exprt &expr)
 std::vector<exprt>
 symex_dereference_statet::get_value_set(const exprt &expr) const
 {
-  return state.value_set.get_value_set(expr, ns);
+  auto result = state.value_set.get_value_set(expr, ns);
+
+  bool has_unknown = result.empty();
+  for(const auto &v : result)
+  {
+    if(v.id() == ID_unknown)
+    {
+      has_unknown = true;
+      break;
+    }
+  }
+
+  if(has_unknown)
+  {
+#if 0
+    // The value set only knows about objects the address of which has been
+    // taken, and may therefore still present an underapproximation for
+    // non-deterministic pointers.
+    result = state.value_set.get_any_object(expr, ns);
+#else
+    state.get_level2().current_names.iterate(
+      [this, &result](
+        const irep_idt &key, const std::pair<ssa_exprt, std::size_t> &entry) {
+        const irep_idt &obj_identifier = entry.first.get_object_name();
+        if(obj_identifier != state.guard_identifier())
+          result.emplace_back(
+            object_descriptor_exprt{ns.lookup(obj_identifier).symbol_expr()});
+      });
+
+    result.emplace_back(object_descriptor_exprt{
+      exprt(ID_null_object, to_pointer_type(expr.type()).subtype())});
+#endif
+  }
+
+  return result;
 }

src/pointer-analysis/value_set.cpp

@@ -371,6 +371,30 @@ value_sett::object_mapt value_sett::get_value_set(
   return dest;
 }
 
+std::vector<exprt>
+value_sett::get_any_object(exprt expr, const namespacet &ns) const
+{
+  if(expr.type().id() != ID_pointer)
+    return {};
+
+  object_mapt object_map;
+
+  // we'll take the union of all objects we see, with unspecified offsets
+  values.iterate([this, &object_map](const irep_idt &key, const entryt &value) {
+    for(const auto &object : value.object_map.read())
+      insert(object_map, object.first, offsett());
+  });
+
+  // we'll add null, in case it's not there yet
+  insert(
+    object_map,
+    exprt(ID_null_object, to_pointer_type(expr.type()).subtype()),
+    offsett());
+
+  return make_range(object_map.read())
+    .map([&](const object_map_dt::value_type &pair) { return to_expr(pair); });
+}
+
 /// Check if 'suffix' starts with 'field'.
 /// Suffix is delimited by periods and '[]' (array access) tokens, so we're
 /// looking for ".field($|[]|.)"
@@ -507,20 +531,7 @@ void value_sett::get_value_set_rec(
   }
   else if(expr.id() == ID_nondet_symbol)
   {
-    if(expr.type().id() == ID_pointer)
-    {
-      // we'll take the union of all objects we see, with unspecified offsets
-      values.iterate([this, &dest](const irep_idt &key, const entryt &value) {
-        for(const auto &object : value.object_map.read())
-          insert(dest, object.first, offsett());
-      });
-
-      // we'll add null, in case it's not there yet
-      insert(
-        dest,
-        exprt(ID_null_object, to_pointer_type(expr_type).subtype()),
-        offsett());
-    }
+    insert(dest, exprt(ID_unknown, original_type));
   }
   else if(expr.id()==ID_if)
   {

src/pointer-analysis/value_set.h

@@ -251,6 +251,13 @@ class value_sett
   ///   are object_descriptor_exprt or have id ID_invalid or ID_unknown.
   std::vector<exprt> get_value_set(exprt expr, const namespacet &ns) const;
 
+  /// Collects all objects known to the value set.
+  /// \param expr: query expression
+  /// \param ns: global namespace
+  /// \return list of objects that any pointer could point to. These expressions
+  ///   are object_descriptor_exprt or have id ID_invalid or ID_unknown.
+  std::vector<exprt> get_any_object(exprt expr, const namespacet &ns) const;
+
   void clear()
   {
     values.clear();