Allow void* pointers cast to another pointer type

That's the expr.type() rather than the representation class.

Author: jezhiggins

regression/goto-analyzer/heap-allocation/main.c

@@ -0,0 +1,7 @@
+
+int main()
+{
+  int *i_was_malloced = malloc(sizeof(int) * 10);
+
+  // q[0] = 99;
+}

regression/goto-analyzer/heap-allocation/test-constant-pointers.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::i_was_malloced \(\) -> ptr ->\(heap allocation\)
+--

regression/goto-analyzer/heap-allocation/test-two-value-pointers.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers top-bottom --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::i_was_malloced \(\) -> TOP
+--

regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::i_was_malloced \(\) -> value-set-begin: ptr ->\(heap allocation\) :value-set-end
+--

src/analyses/variable-sensitivity/abstract_pointer_object.cpp

@@ -46,6 +46,19 @@ abstract_object_pointert abstract_pointer_objectt::expression_transform(
   if(expr.id() == ID_dereference)
     return read_dereference(environment, ns);
 
+  if(expr.id() == ID_typecast)
+  {
+    const typecast_exprt &tce = to_typecast_expr(expr);
+    if(tce.op().id() == ID_symbol && is_void_pointer(tce.op().type()))
+    {
+      auto obj = environment.eval(tce.op(), ns);
+      auto pointer = std::dynamic_pointer_cast<const abstract_pointer_objectt>(
+        obj->unwrap_context());
+      if(pointer)
+        return pointer->typecast(tce.type());
+    }
+  }
+
   return abstract_objectt::expression_transform(
     expr, operands, environment, ns);
 }
@@ -87,6 +100,14 @@ abstract_object_pointert abstract_pointer_objectt::write_dereference(
   return std::make_shared<abstract_pointer_objectt>(type(), true, false);
 }
 
+abstract_object_pointert
+abstract_pointer_objectt::typecast(const typet &new_type) const
+{
+  INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
+  return std::make_shared<abstract_pointer_objectt>(
+    new_type, is_top(), is_bottom());
+}
+
 void abstract_pointer_objectt::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,

src/analyses/variable-sensitivity/abstract_pointer_object.h

@@ -95,6 +95,8 @@ class abstract_pointer_objectt : public abstract_objectt,
     const std::stack<exprt> &stack,
     const abstract_object_pointert &value,
     bool merging_write) const;
+
+  virtual abstract_object_pointert typecast(const typet &new_type) const;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -33,8 +33,10 @@ constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
 }
 
 constant_pointer_abstract_objectt::constant_pointer_abstract_objectt(
+  const typet &new_type,
   const constant_pointer_abstract_objectt &old)
-  : abstract_pointer_objectt(old), value_stack(old.value_stack)
+  : abstract_pointer_objectt(new_type, old.is_top(), old.is_bottom()),
+    value_stack(old.value_stack)
 {
 }
 
@@ -121,6 +123,10 @@ void constant_pointer_abstract_objectt::output(
 
         out << symbol_pointed_to.get_identifier();
       }
+      else if(addressee.id() == ID_dynamic_object)
+      {
+        out << "heap allocation";
+      }
       else if(addressee.id() == ID_index)
       {
         auto const &array_index = to_index_expr(addressee);
@@ -209,6 +215,13 @@ abstract_object_pointert constant_pointer_abstract_objectt::write_dereference(
   }
 }
 
+abstract_object_pointert
+constant_pointer_abstract_objectt::typecast(const typet &new_type) const
+{
+  INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
+  return std::make_shared<constant_pointer_abstract_objectt>(new_type, *this);
+}
+
 void constant_pointer_abstract_objectt::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,

src/analyses/variable-sensitivity/constant_pointer_abstract_object.h

@@ -34,8 +34,8 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt
   /// Asserts if both top and bottom are true
   constant_pointer_abstract_objectt(const typet &type, bool top, bool bottom);
 
-  /// \param old: the abstract object to copy from
   constant_pointer_abstract_objectt(
+    const typet &type,
     const constant_pointer_abstract_objectt &old);
 
   /// \param expr: the expression to use as the starting pointer for
@@ -106,6 +106,8 @@ class constant_pointer_abstract_objectt : public abstract_pointer_objectt
     const abstract_object_pointert &value,
     bool merging_write) const override;
 
+  abstract_object_pointert typecast(const typet &new_type) const override;
+
   void get_statistics(
     abstract_object_statisticst &statistics,
     abstract_object_visitedt &visited,

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

@@ -12,6 +12,7 @@
 #include <analyses/variable-sensitivity/constant_pointer_abstract_object.h>
 #include <analyses/variable-sensitivity/context_abstract_object.h>
 #include <analyses/variable-sensitivity/value_set_pointer_abstract_object.h>
+#include <pointer_expr.h>
 
 #include "abstract_environment.h"
 
@@ -68,6 +69,14 @@ value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt(
   values.insert(std::make_shared<constant_pointer_abstract_objectt>(type));
 }
 
+value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt(
+  const typet &new_type,
+  const value_set_pointer_abstract_objectt &old)
+  : abstract_pointer_objectt(new_type, old.is_top(), old.is_bottom()),
+    values(old.values)
+{
+}
+
 value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt(
   const typet &type,
   bool top,
@@ -133,6 +142,13 @@ abstract_object_pointert value_set_pointer_abstract_objectt::write_dereference(
   return shared_from_this();
 }
 
+abstract_object_pointert
+value_set_pointer_abstract_objectt::typecast(const typet &new_type) const
+{
+  INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
+  return std::make_shared<value_set_pointer_abstract_objectt>(new_type, *this);
+}
+
 abstract_object_pointert value_set_pointer_abstract_objectt::resolve_values(
   const abstract_object_sett &new_values) const
 {

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h

@@ -22,6 +22,10 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
   /// \copydoc abstract_objectt::abstract_objectt(const typet&)
   explicit value_set_pointer_abstract_objectt(const typet &type);
 
+  value_set_pointer_abstract_objectt(
+    const typet &new_type,
+    const value_set_pointer_abstract_objectt &old);
+
   /// \copydoc abstract_objectt::abstract_objectt(const typet &, bool, bool)
   value_set_pointer_abstract_objectt(const typet &type, bool top, bool bottom);
 
@@ -64,6 +68,8 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
     const abstract_object_pointert &new_value,
     bool merging_write) const override;
 
+  abstract_object_pointert typecast(const typet &new_type) const override;
+
   void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
     const override;