Value sets: make pointers nondet only once

When `get_value_set_rec` discovers a nondet symbol it will consider the
pointer pointing to any of the known objects (as of 3789670). It
suffices to do this once for each run of `get_value_set`, even when
multiple nondet symbols are encountered while traversing an expression.

This reduces the symex time on the test of #7357 from 930 seconds to 404
seconds.

Author: tautschnig

src/pointer-analysis/value_set.cpp

@@ -371,6 +371,24 @@ value_sett::object_mapt value_sett::get_value_set(
 
   object_mapt dest;
   get_value_set_rec(expr, dest, "", expr.type(), ns);
+
+  if(nondet_pointer && 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()).base_type()),
+      offsett());
+
+    nondet_pointer = false;
+  }
+
   return dest;
 }
 
@@ -512,17 +530,7 @@ void value_sett::get_value_set_rec(
   {
     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).base_type()),
-        offsett());
+      nondet_pointer = true;
     }
     else
       insert(dest, exprt(ID_unknown, original_type));

src/pointer-analysis/value_set.h

@@ -494,7 +494,9 @@ class value_sett
     const codet &code,
     const namespacet &ns);
 
- private:
+  mutable bool nondet_pointer = false;
+
+private:
   /// Subclass customisation point to filter or otherwise alter the value-set
   /// returned from get_value_set before it is passed into assign. For example,
   /// this is used in one subclass to tag and thus differentiate values that