Add pointer field to value_set_dereferencet::valuet

value_set_dereferencet::valuet is only used as the return value of
value_set_dereferencet::build_reference_to. valuet::value is an
expression for the object pointed to, which is what's needed for
dereferencing. In other contexts, e.g. filtering value-sets, what
is needed is an expression for the pointer. This logic already
existed in try_filter_value_set, but putting it directly in
build_reference_to makes it easier to use it in other places and
makes it clear that it didn't cope with typecasts properly.

Author: Owen

src/goto-symex/symex_main.cpp

@@ -721,9 +721,11 @@ void goto_symext::try_filter_value_sets(
   // one of its possible values in turn. If that leads to a true for some
   // value_set_element then we can delete it from the value set that will be
   // used if the condition is false, and vice versa.
-  for(const auto &value_set_element : value_set_elements)
+  for(const exprt &value_set_element : value_set_elements)
   {
-    if(value_set_element.id() == ID_unknown)
+    if(
+      value_set_element.id() == ID_unknown ||
+      value_set_element.id() == ID_invalid)
     {
       continue;
     }
@@ -735,19 +737,17 @@ void goto_symext::try_filter_value_sets(
       continue;
     }
 
-    value_set_dereferencet::valuet possible_value =
+    value_set_dereferencet::valuet value =
       value_set_dereferencet::build_reference_to(
         value_set_element, *symbol_expr, ns);
 
-    exprt replacement_expr =
-      possible_value.value.is_nil()
-        ? static_cast<exprt>(null_pointer_exprt{symbol_type})
-        : static_cast<exprt>(address_of_exprt{possible_value.value});
+    if(value.pointer.is_nil())
+      continue;
 
     exprt modified_condition(condition);
 
     address_of_aware_replace_symbolt replace_symbol{};
-    replace_symbol.insert(*symbol_expr, replacement_expr);
+    replace_symbol.insert(*symbol_expr, value.pointer);
     replace_symbol(modified_condition);
 
     // This do_simplify() is needed for the following reason: if `condition` is

src/pointer-analysis/value_set_dereference.cpp

@@ -23,6 +23,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/expr_iterator.h>
+#include <util/expr_util.h>
 #include <util/format_type.h>
 #include <util/fresh_symbol.h>
 #include <util/options.h>
@@ -361,7 +362,9 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
   const exprt &pointer_expr,
   const namespacet &ns)
 {
-  const typet &dereference_type = pointer_expr.type().subtype();
+  const pointer_typet &pointer_type =
+    type_checked_cast<pointer_typet>(pointer_expr.type());
+  const typet &dereference_type = pointer_type.subtype();
 
   if(what.id()==ID_unknown ||
      what.id()==ID_invalid)
@@ -385,6 +388,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
 
   if(root_object.id() == ID_null_object)
   {
+    result.pointer = null_pointer_exprt{pointer_type};
   }
   else if(root_object.id()==ID_dynamic_object)
   {
@@ -394,6 +398,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
 
     // can't remove here, turn into *p
     result.value = dereference_exprt{pointer_expr};
+    result.pointer = pointer_expr;
   }
   else if(root_object.id()==ID_integer_address)
   {
@@ -414,6 +419,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         memory_symbol.type.subtype());
 
       result.value=index_expr;
+      result.pointer = address_of_exprt{index_expr};
     }
     else if(
       dereference_type_compare(
@@ -424,6 +430,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         pointer_offset(pointer_expr),
         memory_symbol.type.subtype());
       result.value=typecast_exprt(index_expr, dereference_type);
+      result.pointer =
+        typecast_exprt{address_of_exprt{index_expr}, pointer_type};
     }
     else
     {
@@ -440,6 +448,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
           symbol_expr,
           pointer_offset(pointer_expr),
           dereference_type);
+        result.pointer = address_of_exprt{result.value};
       }
     }
   }
@@ -472,6 +481,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       // This is great, we are almost done.
 
       result.value = typecast_exprt::conditional_cast(object, dereference_type);
+      result.pointer =
+        typecast_exprt::conditional_cast(object_pointer, pointer_type);
     }
     else if(
       root_object_type.id() == ID_array &&
@@ -515,9 +526,12 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         // TODO: need to assert well-alignedness
       }
 
-      result.value = typecast_exprt::conditional_cast(
-        index_exprt(root_object, adjusted_offset, root_object_type.subtype()),
-        dereference_type);
+      const index_exprt &index_expr =
+        index_exprt(root_object, adjusted_offset, root_object_type.subtype());
+      result.value =
+        typecast_exprt::conditional_cast(index_expr, dereference_type);
+      result.pointer = typecast_exprt::conditional_cast(
+        address_of_exprt{index_expr}, pointer_type);
     }
     else
     {
@@ -531,11 +545,15 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         // Successfully found a member, array index, or combination thereof
         // that matches the desired type and offset:
         result.value = subexpr.value();
+        result.pointer = typecast_exprt::conditional_cast(
+          address_of_exprt{skip_typecast(subexpr.value())}, pointer_type);
         return result;
       }
 
       // we extract something from the root object
       result.value=o.root_object();
+      result.pointer = typecast_exprt::conditional_cast(
+        address_of_exprt{skip_typecast(o.root_object())}, pointer_type);
 
       // this is relative to the root object
       exprt offset;

src/pointer-analysis/value_set_dereference.h

@@ -59,9 +59,11 @@ class value_set_dereferencet final
   {
   public:
     exprt value;
+    exprt pointer;
     exprt pointer_guard;
 
-    valuet() : value(nil_exprt()), pointer_guard(false_exprt())
+    valuet()
+      : value{nil_exprt{}}, pointer{nil_exprt{}}, pointer_guard{false_exprt{}}
     {
     }
   };