Create heap allocation abstract object on pointer typecast

We can't ensure the modified pointer object will be properly assigned
back to its symbol if we wait until first write.

If we defer then modified pointer may, or may not, be assigned depending
on how the write is expressed

 *p = 1;   // good :)
 p[0] = 1; // bad :(

Author: jezhiggins

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

@@ -0,0 +1,14 @@
+
+int main() {
+  int* i_was_malloced = malloc(sizeof(int) * 10);
+  int* alias = i_was_malloced;
+
+  *i_was_malloced = 99;
+  assert(*alias == 99);
+
+  i_was_malloced[0] = 100;
+  assert(*alias == 100);
+
+  *alias += 1;
+  assert(i_was_malloced[0] == 101);
+}

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

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .*alias == 99: SUCCESS
+\[main.assertion.2\] .*alias == 100: SUCCESS
+\[main.assertion.3\] .*i_was_malloced.* == 101: SUCCESS
+--

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

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers top-bottom --vsd-arrays every-element --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .*alias == 99: UNKNOWN
+\[main.assertion.2\] .*alias == 100: UNKNOWN
+\[main.assertion.3\] .*i_was_malloced.* == 101: UNKNOWN
+--

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

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

src/analyses/variable-sensitivity/abstract_pointer_object.cpp

@@ -55,7 +55,7 @@ abstract_object_pointert abstract_pointer_objectt::expression_transform(
       auto pointer = std::dynamic_pointer_cast<const abstract_pointer_objectt>(
         obj->unwrap_context());
       if(pointer)
-        return pointer->typecast(tce.type());
+        return pointer->typecast(tce.type(), environment, ns);
     }
   }
 
@@ -101,7 +101,11 @@ abstract_object_pointert abstract_pointer_objectt::write_dereference(
 }
 
 abstract_object_pointert
-abstract_pointer_objectt::typecast(const typet &new_type) const
+abstract_pointer_objectt::typecast(
+  const typet &new_type,
+  const abstract_environmentt &environment,
+  const namespacet &ns
+) const
 {
   INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
   return std::make_shared<abstract_pointer_objectt>(

src/analyses/variable-sensitivity/abstract_pointer_object.h

@@ -96,7 +96,11 @@ class abstract_pointer_objectt : public abstract_objectt,
     const abstract_object_pointert &value,
     bool merging_write) const;
 
-  virtual abstract_object_pointert typecast(const typet &new_type) const;
+  virtual abstract_object_pointert typecast(
+    const typet &new_type,
+    const abstract_environmentt &environment,
+    const namespacet &ns
+  ) const;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -9,6 +9,8 @@
 #include "constant_pointer_abstract_object.h"
 
 #include <analyses/variable-sensitivity/abstract_environment.h>
+#include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/pointer_expr.h>
 #include <util/std_expr.h>
 
@@ -207,18 +209,40 @@ abstract_object_pointert constant_pointer_abstract_objectt::write_dereference(
       abstract_object_pointert modified_value =
         environment.write(pointed_value, new_value, stack, ns, merging_write);
       environment.assign(value, modified_value, ns);
-
       // but the pointer itself does not change!
     }
-    return std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(
-      shared_from_this());
+
+    return shared_from_this();
   }
 }
 
 abstract_object_pointert
-constant_pointer_abstract_objectt::typecast(const typet &new_type) const
+constant_pointer_abstract_objectt::typecast(
+  const typet &new_type,
+  const abstract_environmentt &environment,
+  const namespacet &ns
+) const
 {
   INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
+
+  // Get an expression that we can assign to
+  exprt value = to_address_of_expr(value_stack.to_expression()).object();
+  if (value.id() == ID_dynamic_object) {
+    auto& env = const_cast<abstract_environmentt&>(environment);
+
+    auto heap_array_type = array_typet(new_type.subtype(), nil_exprt());
+    auto array_object = environment.abstract_object_factory(heap_array_type, ns, true, false);
+    auto heap_symbol = symbol_exprt("heap-object", heap_array_type);
+    env.assign(heap_symbol, array_object, ns);
+    auto heap_address = address_of_exprt(
+      index_exprt(heap_symbol, from_integer(0, size_type())));
+    auto new_pointer = std::make_shared<constant_pointer_abstract_objectt>(
+      heap_address,
+      env,
+      ns);
+    return new_pointer;
+  }
+
   return std::make_shared<constant_pointer_abstract_objectt>(new_type, *this);
 }
 

src/analyses/variable-sensitivity/constant_pointer_abstract_object.h

@@ -106,7 +106,11 @@ 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;
+  abstract_object_pointert typecast(
+    const typet &new_type,
+    const abstract_environmentt &environment,
+    const namespacet &ns
+  ) const override;
 
   void get_statistics(
     abstract_object_statisticst &statistics,

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

@@ -143,7 +143,11 @@ abstract_object_pointert value_set_pointer_abstract_objectt::write_dereference(
 }
 
 abstract_object_pointert
-value_set_pointer_abstract_objectt::typecast(const typet &new_type) const
+value_set_pointer_abstract_objectt::typecast(
+  const typet &new_type,
+  const abstract_environmentt &environment,
+  const namespacet &ns
+) const
 {
   INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*");
   return std::make_shared<value_set_pointer_abstract_objectt>(new_type, *this);

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h

@@ -68,7 +68,11 @@ 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;
+  abstract_object_pointert typecast(
+    const typet &new_type,
+    const abstract_environmentt &environment,
+    const namespacet &ns
+  ) const override;
 
   void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
     const override;