Simplify equal/not-equal over pointer_object expressions using value set

The value set can help us infer that, e.g., a particular pointer cannot
be among the ones assigned to __CPROVER_dead_object, whereby we can
simplify R_OK/W_OK expressions.

Author: tautschnig

src/goto-symex/simplify_expr_with_value_set.cpp

@@ -155,6 +155,78 @@ simplify_exprt::resultt<> simplify_expr_with_value_sett::simplify_inequality(
     return unchanged(expr);
 }
 
+simplify_exprt::resultt<>
+simplify_expr_with_value_sett::simplify_inequality_pointer_object(
+  const binary_relation_exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
+  PRECONDITION(expr.is_boolean());
+
+  auto collect_objects = [this](const exprt &pointer)
+  {
+    std::set<exprt> objects;
+    if(auto address_of = expr_try_dynamic_cast<address_of_exprt>(pointer))
+    {
+      objects.insert(
+        object_descriptor_exprt::root_object(address_of->object()));
+    }
+    else if(auto ssa_expr = expr_try_dynamic_cast<ssa_exprt>(pointer))
+    {
+      ssa_exprt l1_expr{*ssa_expr};
+      l1_expr.remove_level_2();
+      const std::vector<exprt> value_set_elements =
+        value_set.get_value_set(l1_expr, ns);
+
+      for(const auto &value_set_element : value_set_elements)
+      {
+        if(
+          value_set_element.id() == ID_unknown ||
+          value_set_element.id() == ID_invalid ||
+          is_failed_symbol(
+            to_object_descriptor_expr(value_set_element).root_object()))
+        {
+          objects.clear();
+          break;
+        }
+
+        objects.insert(
+          to_object_descriptor_expr(value_set_element).root_object());
+      }
+    }
+    return objects;
+  };
+
+  auto lhs_objects =
+    collect_objects(to_pointer_object_expr(expr.lhs()).pointer());
+  auto rhs_objects =
+    collect_objects(to_pointer_object_expr(expr.rhs()).pointer());
+
+  if(lhs_objects.size() == 1 && lhs_objects == rhs_objects)
+  {
+    // there is exactly one pointed-to object on both left-hand and right-hand
+    // side, and that object is the same
+    return expr.id() == ID_equal ? changed(static_cast<exprt>(true_exprt{}))
+                                 : changed(static_cast<exprt>(false_exprt{}));
+  }
+
+  std::list<exprt> intersection;
+  std::set_intersection(
+    lhs_objects.begin(),
+    lhs_objects.end(),
+    rhs_objects.begin(),
+    rhs_objects.end(),
+    std::back_inserter(intersection));
+  if(!lhs_objects.empty() && !rhs_objects.empty() && intersection.empty())
+  {
+    // all pointed-to objects on the left-hand side are different from any of
+    // the pointed-to objects on the right-hand side
+    return expr.id() == ID_equal ? changed(static_cast<exprt>(false_exprt{}))
+                                 : changed(static_cast<exprt>(true_exprt{}));
+  }
+
+  return simplify_exprt::simplify_inequality_pointer_object(expr);
+}
+
 simplify_exprt::resultt<>
 simplify_expr_with_value_sett::simplify_pointer_offset(
   const pointer_offset_exprt &expr)

src/goto-symex/simplify_expr_with_value_set.h

@@ -27,6 +27,8 @@ class simplify_expr_with_value_sett : public simplify_exprt
   [[nodiscard]] resultt<>
   simplify_inequality(const binary_relation_exprt &) override;
   [[nodiscard]] resultt<>
+  simplify_inequality_pointer_object(const binary_relation_exprt &) override;
+  [[nodiscard]] resultt<>
   simplify_pointer_offset(const pointer_offset_exprt &) override;
 
 protected:

src/util/simplify_expr_class.h

@@ -273,7 +273,7 @@ class simplify_exprt
   simplify_inequality_rhs_is_constant(const binary_relation_exprt &);
   [[nodiscard]] resultt<>
   simplify_inequality_address_of(const binary_relation_exprt &);
-  [[nodiscard]] resultt<>
+  [[nodiscard]] virtual resultt<>
   simplify_inequality_pointer_object(const binary_relation_exprt &);
 
   // main recursion