Merge pull request #6218 from jezhiggins/vsd-pointers-to-heap-allocations

martin-cs · web-flow · commit b0b71d0650d5 · 2021-07-27T12:30:52.000+01:00
VSD - pointers to heap allocations
diff --git a/regression/goto-analyzer/heap-allocation-nondet-1/main.c b/regression/goto-analyzer/heap-allocation-nondet-1/main.c
@@ -0,0 +1,10 @@
+
+int main()
+{
+  int *q = malloc(10);
+  int *r = malloc(10);
+
+  int *p = r;
+  if(nondet())
+    p = q;
+}
diff --git a/regression/goto-analyzer/heap-allocation-nondet-1/test.desc b/regression/goto-analyzer/heap-allocation-nondet-1/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\), ptr ->\(heap-allocation-1\[0\]\) :value-set-end
+--
diff --git a/regression/goto-analyzer/heap-allocation-nondet-2/main.c b/regression/goto-analyzer/heap-allocation-nondet-2/main.c
@@ -0,0 +1,7 @@
+
+int main()
+{
+  int *p = malloc(10);
+  if(nondet())
+    ++p;
+}
diff --git a/regression/goto-analyzer/heap-allocation-nondet-2/test.desc b/regression/goto-analyzer/heap-allocation-nondet-2/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\), ptr ->\(heap-allocation-0\[1\]\) :value-set-end
+--
diff --git a/regression/goto-analyzer/heap-allocation-nondet-3/main.c b/regression/goto-analyzer/heap-allocation-nondet-3/main.c
@@ -0,0 +1,10 @@
+
+int main()
+{
+  int *q = malloc(10);
+  int r[10];
+
+  int *p = r;
+  if(nondet())
+    p = q;
+}
diff --git a/regression/goto-analyzer/heap-allocation-nondet-3/test.desc b/regression/goto-analyzer/heap-allocation-nondet-3/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(main::1::r\[0\]\), ptr ->\(heap-allocation-0\[0\]\) :value-set-end
+--
diff --git a/regression/goto-analyzer/heap-allocation-nondet-4/main.c b/regression/goto-analyzer/heap-allocation-nondet-4/main.c
@@ -0,0 +1,10 @@
+
+int main()
+{
+  int *q = malloc(10);
+  int r[10];
+
+  int *p = q;
+  if(nondet())
+    p = r;
+}
diff --git a/regression/goto-analyzer/heap-allocation-nondet-4/test.desc b/regression/goto-analyzer/heap-allocation-nondet-4/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(main::1::r\[0\]\), ptr ->\(heap-allocation-0\[0\]\) :value-set-end
+--
diff --git a/regression/goto-analyzer/heap-allocation-nondet-5/main.c b/regression/goto-analyzer/heap-allocation-nondet-5/main.c
@@ -0,0 +1,8 @@
+
+int main()
+{
+  int *p = malloc(10);
+
+  if(non_det())
+    p = malloc(20);
+}
diff --git a/regression/goto-analyzer/heap-allocation-nondet-5/test.desc b/regression/goto-analyzer/heap-allocation-nondet-5/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\), ptr ->\(heap-allocation-1\[0\]\) :value-set-end
+--
diff --git a/regression/goto-analyzer/heap-allocation-nondet-6/main.c b/regression/goto-analyzer/heap-allocation-nondet-6/main.c
@@ -0,0 +1,5 @@
+
+int main()
+{
+  int *p = nondet() ? malloc(10) : malloc(20);
+}
diff --git a/regression/goto-analyzer/heap-allocation-nondet-6/test.desc b/regression/goto-analyzer/heap-allocation-nondet-6/test.desc
@@ -0,0 +1,7 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\), ptr ->\(heap-allocation-1\[0\]\) :value-set-end
+--
diff --git a/regression/goto-analyzer/heap-allocation-write-2/main.c b/regression/goto-analyzer/heap-allocation-write-2/main.c
@@ -0,0 +1,20 @@
+
+int main()
+{
+  int *p = malloc(sizeof(int) * 5);
+  int *q = malloc(sizeof(int) * 10);
+
+  int *pp = p;
+
+  *p = 10;
+  ++p;
+  *p = 20;
+
+  q[0] = 100;
+  q[99] = 101;
+
+  assert(pp[0] == 10);
+  assert(pp[1] == 20);
+  assert(q[0] == 100);
+  assert(q[99] == 101);
+}
diff --git a/regression/goto-analyzer/heap-allocation-write-2/test-constant-pointers.desc b/regression/goto-analyzer/heap-allocation-write-2/test-constant-pointers.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers constants --vsd-arrays every-element --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .*p\[.*0\] == 10: SUCCESS
+\[main.assertion.2\] .*p\[.*1\] == 20: SUCCESS
+\[main.assertion.3\] .*q\[.*0\] == 100: SUCCESS
+\[main.assertion.4\] .*q\[.*99\] == 101: SUCCESS
+--
diff --git a/regression/goto-analyzer/heap-allocation-write-2/test-two-value-pointers.desc b/regression/goto-analyzer/heap-allocation-write-2/test-two-value-pointers.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers top-bottom --vsd-arrays every-element --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .*p\[.*0\] == 10: UNKNOWN
+\[main.assertion.2\] .*p\[.*1\] == 20: UNKNOWN
+\[main.assertion.3\] .*q\[.*0\] == 100: UNKNOWN
+\[main.assertion.4\] .*q\[.*99\] == 101: UNKNOWN
+--
diff --git a/regression/goto-analyzer/heap-allocation-write-2/test-value-set-pointers.desc b/regression/goto-analyzer/heap-allocation-write-2/test-value-set-pointers.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --vsd-arrays every-element --verify
+^EXIT=0$
+^SIGNAL=0$
+\[main.assertion.1\] .*p\[.*0\] == 10: SUCCESS
+\[main.assertion.2\] .*p\[.*1\] == 20: SUCCESS
+\[main.assertion.3\] .*q\[.*0\] == 100: SUCCESS
+\[main.assertion.4\] .*q\[.*99\] == 101: SUCCESS
+--
diff --git a/regression/goto-analyzer/heap-allocation-write/main.c b/regression/goto-analyzer/heap-allocation-write/main.c
@@ -0,0 +1,18 @@
+
+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);
+
+  i_was_malloced[1] = 102;
+  assert(alias[1] == 102);
+}
diff --git a/regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc b/regression/goto-analyzer/heap-allocation-write/test-constant-pointers.desc
@@ -0,0 +1,10 @@
+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\[.*0\] == 101: SUCCESS
+\[main.assertion.4\] .*alias\[.*1\] == 102: SUCCESS
+--
diff --git a/regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc b/regression/goto-analyzer/heap-allocation-write/test-two-value-pointers.desc
@@ -0,0 +1,10 @@
+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\[.*0\] == 101: UNKNOWN
+\[main.assertion.4\] .*alias\[.*1\] == 102: UNKNOWN
+--
diff --git a/regression/goto-analyzer/heap-allocation-write/test-value-set-pointers.desc b/regression/goto-analyzer/heap-allocation-write/test-value-set-pointers.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --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\[.*0\] == 101: SUCCESS
+\[main.assertion.4\] .*alias\[.*1\] == 102: SUCCESS
+--
diff --git a/regression/goto-analyzer/heap-allocation/main.c b/regression/goto-analyzer/heap-allocation/main.c
@@ -0,0 +1,6 @@
+
+int main()
+{
+  int *p = malloc(sizeof(int) * 10);
+  int *q = malloc(sizeof(int) * 5);
+}
diff --git a/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc b/regression/goto-analyzer/heap-allocation/test-constant-pointers.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers constants --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> ptr ->\(heap-allocation-0\[0\]\)
+main::1::q \(\) -> ptr ->\(heap-allocation-1\[0\]\)
+--
diff --git a/regression/goto-analyzer/heap-allocation/test-two-value-pointers.desc b/regression/goto-analyzer/heap-allocation/test-two-value-pointers.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers top-bottom --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> TOP
+main::1::q \(\) -> TOP
+--
diff --git a/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc b/regression/goto-analyzer/heap-allocation/test-value-set-pointers.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --show
+^EXIT=0$
+^SIGNAL=0$
+main::1::p \(\) -> value-set-begin: ptr ->\(heap-allocation-0\[0\]\) :value-set-end
+main::1::q \(\) -> value-set-begin: ptr ->\(heap-allocation-1\[0\]\) :value-set-end
+--
diff --git a/src/analyses/variable-sensitivity/abstract_environment.cpp b/src/analyses/variable-sensitivity/abstract_environment.cpp
@@ -84,6 +84,16 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
     return abstract_object_factory(simplified_expr.type(), simplified_expr, ns);
   }
 
+  if(
+    simplified_id == ID_side_effect &&
+    (simplified_expr.get(ID_statement) == ID_allocate))
+  {
+    return abstract_object_factory(
+      typet(ID_dynamic_object),
+      exprt(ID_dynamic_object, simplified_expr.type()),
+      ns);
+  }
+
   // No special handling required by the abstract environment
   // delegate to the abstract object
   if(!simplified_expr.operands().empty())
diff --git a/src/analyses/variable-sensitivity/abstract_pointer_object.cpp b/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(), environment, ns);
+    }
+  }
+
   return abstract_objectt::expression_transform(
     expr, operands, environment, ns);
 }
@@ -87,6 +100,16 @@ 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 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>(
+    new_type, is_top(), is_bottom());
+}
+
 void abstract_pointer_objectt::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,
diff --git a/src/analyses/variable-sensitivity/abstract_pointer_object.h b/src/analyses/variable-sensitivity/abstract_pointer_object.h
@@ -95,6 +95,11 @@ 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 abstract_environmentt &environment,
+    const namespacet &ns) const;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H
diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp b/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>
 
@@ -33,8 +35,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 +125,10 @@ void constant_pointer_abstract_objectt::output(
 
         out << symbol_pointed_to.get_identifier();
       }
+      else if(addressee.id() == ID_dynamic_object)
+      {
+        out << addressee.get(ID_identifier);
+      }
       else if(addressee.id() == ID_index)
       {
         auto const &array_index = to_index_expr(addressee);
@@ -201,14 +209,41 @@ 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 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(value.get(ID_identifier), heap_array_type);
+    env.assign(heap_symbol, array_object, ns);
+    auto heap_address = address_of_exprt(
+      index_exprt(heap_symbol, from_integer(0, signed_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);
+}
+
 void constant_pointer_abstract_objectt::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,
diff --git a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h b/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h
diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp
diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h
diff --git a/src/analyses/variable-sensitivity/write_stack.cpp b/src/analyses/variable-sensitivity/write_stack.cpp
diff --git a/src/analyses/variable-sensitivity/write_stack_entry.cpp b/src/analyses/variable-sensitivity/write_stack_entry.cpp
