diff --git a/regression/goto-analyzer/heap-allocation-nondet-1/main.c b/regression/goto-analyzer/heap-allocation-nondet-1/main.c new file mode 100644 index 00000000000..e022d770c6e --- /dev/null +++ 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 new file mode 100644 index 00000000000..8e2b3db203e --- /dev/null +++ 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 new file mode 100644 index 00000000000..84ef19235fe --- /dev/null +++ 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 new file mode 100644 index 00000000000..e74d0b420e0 --- /dev/null +++ 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 new file mode 100644 index 00000000000..d49b7ec72b7 --- /dev/null +++ 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 new file mode 100644 index 00000000000..a1d1451339b --- /dev/null +++ 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 new file mode 100644 index 00000000000..7870ce77aa5 --- /dev/null +++ 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 new file mode 100644 index 00000000000..a1d1451339b --- /dev/null +++ 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 new file mode 100644 index 00000000000..faa8283feff --- /dev/null +++ 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 new file mode 100644 index 00000000000..8e2b3db203e --- /dev/null +++ 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 new file mode 100644 index 00000000000..8dabb4a1132 --- /dev/null +++ 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 new file mode 100644 index 00000000000..8e2b3db203e --- /dev/null +++ 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 new file mode 100644 index 00000000000..020067294d8 --- /dev/null +++ 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 new file mode 100644 index 00000000000..dcd33598351 --- /dev/null +++ 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 new file mode 100644 index 00000000000..474b957707e --- /dev/null +++ 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 new file mode 100644 index 00000000000..91687849c60 --- /dev/null +++ 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 new file mode 100644 index 00000000000..6019ab2f1d7 --- /dev/null +++ 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 new file mode 100644 index 00000000000..0aaca9a8b72 --- /dev/null +++ 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 new file mode 100644 index 00000000000..8aa9ea66315 --- /dev/null +++ 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 new file mode 100644 index 00000000000..9d7320b2dc0 --- /dev/null +++ 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 new file mode 100644 index 00000000000..c09abc337b8 --- /dev/null +++ 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 new file mode 100644 index 00000000000..8379e910976 --- /dev/null +++ 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 new file mode 100644 index 00000000000..9329e3a9ced --- /dev/null +++ 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 new file mode 100644 index 00000000000..d0feb9fbd22 --- /dev/null +++ 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 index b473730c36e..4723bec5e24 100644 --- 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 index dbad74720f1..5fec2cfa6ca 100644 --- 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( + 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(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( + 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 index 365cf710deb..6ce6966b1ef 100644 --- 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 &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 index 6cbd1eaba3e..9519e2ada51 100644 --- 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 +#include +#include #include #include @@ -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( - 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(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( + heap_address, env, ns); + return new_pointer; + } + + return std::make_shared(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 index baf09eba2bc..8ea94a645c8 100644 --- a/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h +++ b/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,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 abstract_environmentt &environment, + const namespacet &ns) const override; + void get_statistics( abstract_object_statisticst &statistics, abstract_object_visitedt &visited, diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp index 07fc3fab966..025d2029e09 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp @@ -12,6 +12,7 @@ #include #include #include +#include #include "abstract_environment.h" @@ -24,43 +25,6 @@ unwrap_and_extract_values(const abstract_object_sett &values); static abstract_object_pointert maybe_extract_single_value(const abstract_object_pointert &maybe_singleton); -/// Recursively construct a combination \p sub_con from \p super_con and once -/// constructed call \p f. -/// \param super_con: vector of some containers storing the values -/// \param sub_con: the one combination being currently constructed -/// \param f: callable with side-effects -template -void apply_comb( - const std::vector &super_con, - std::vector &sub_con, - F f) -{ - size_t n = sub_con.size(); - if(n == super_con.size()) - f(sub_con); - else - { - for(const auto &value : super_con[n]) - { - sub_con.push_back(value); - apply_comb(super_con, sub_con, f); - sub_con.pop_back(); - } - } -} - -/// Call the function \p f on every combination of elements in \p super_con. -/// Hence the arity of \p f is `super_con.size()`. <{1,2},{1},{1,2,3}> -> -/// f(1,1,1), f(1,1,2), f(1,1,3), f(2,1,1), f(2,1,2), f(2,1,3). -/// \param super_con: vector of some containers storing the values -/// \param f: callable with side-effects -template -void for_each_comb(const std::vector &super_con, F f) -{ - std::vector sub_con; - apply_comb(super_con, sub_con, f); -} - value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt( const typet &type) : abstract_pointer_objectt(type) @@ -68,6 +32,15 @@ value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt( values.insert(std::make_shared(type)); } +value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt( + const typet &new_type, + bool top, + bool bottom, + const abstract_object_sett &new_values) + : abstract_pointer_objectt(new_type, top, bottom), values(new_values) +{ +} + value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt( const typet &type, bool top, @@ -133,6 +106,26 @@ 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 abstract_environmentt &environment, + const namespacet &ns) const +{ + INVARIANT(is_void_pointer(type()), "Only allow pointer casting from void*"); + abstract_object_sett new_values; + for(auto value : values) + { + if(value->is_top()) // multiple mallocs in the same scope can cause spurious + continue; // TOP values, which we can safely strip out during the cast + + auto pointer = + std::dynamic_pointer_cast(value); + new_values.insert(pointer->typecast(new_type, environment, ns)); + } + return std::make_shared( + new_type, is_top(), is_bottom(), new_values); +} + abstract_object_pointert value_set_pointer_abstract_objectt::resolve_values( const abstract_object_sett &new_values) const { diff --git a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h index bce89cafbed..4e33a384543 100644 --- a/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h +++ b/src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h @@ -22,6 +22,12 @@ 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, + bool top, + bool bottom, + const abstract_object_sett &new_values); + /// \copydoc abstract_objectt::abstract_objectt(const typet &, bool, bool) value_set_pointer_abstract_objectt(const typet &type, bool top, bool bottom); @@ -64,6 +70,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 abstract_environmentt &environment, + const namespacet &ns) const override; + void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override; diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h index c7dd990bc79..f5d7415cd81 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_configuration.h @@ -31,7 +31,8 @@ enum ABSTRACT_OBJECT_TYPET STRUCT_INSENSITIVE, // TODO: plug in UNION_SENSITIVE HERE UNION_INSENSITIVE, - VALUE_SET + VALUE_SET, + HEAP_ALLOCATION }; enum class flow_sensitivityt diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp index 4bb1a8cfd16..551a6373450 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.cpp @@ -114,6 +114,10 @@ variable_sensitivity_object_factoryt::get_abstract_object_type( { return configuration.union_abstract_type; } + else if(type.id() == ID_dynamic_object) + { + return HEAP_ALLOCATION; + } return abstract_object_type; } @@ -174,6 +178,17 @@ variable_sensitivity_object_factoryt::get_abstract_object( return initialize_abstract_object( followed_type, top, bottom, e, environment, ns, configuration); + case HEAP_ALLOCATION: + { + auto dynamic_object = exprt(ID_dynamic_object); + dynamic_object.set( + ID_identifier, "heap-allocation-" + std::to_string(heap_allocations++)); + auto heap_symbol = unary_exprt(ID_address_of, dynamic_object, e.type()); + auto heap_pointer = + get_abstract_object(e.type(), false, false, heap_symbol, environment, ns); + return heap_pointer; + } + default: UNREACHABLE; return initialize_abstract_object( diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h index edfe5c1b22e..2d4a1143892 100644 --- a/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h +++ b/src/analyses/variable-sensitivity/variable_sensitivity_object_factory.h @@ -44,7 +44,7 @@ class variable_sensitivity_object_factoryt } explicit variable_sensitivity_object_factoryt(const vsd_configt &options) - : configuration{options} + : configuration{options}, heap_allocations(0) { } @@ -87,6 +87,7 @@ class variable_sensitivity_object_factoryt ABSTRACT_OBJECT_TYPET get_abstract_object_type(const typet &type) const; vsd_configt configuration; + mutable size_t heap_allocations; }; #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_VARIABLE_SENSITIVITY_OBJECT_FACTORY_H // NOLINT(*) diff --git a/src/analyses/variable-sensitivity/write_stack.cpp b/src/analyses/variable-sensitivity/write_stack.cpp index 05a33c578b2..60b7847ca93 100644 --- a/src/analyses/variable-sensitivity/write_stack.cpp +++ b/src/analyses/variable-sensitivity/write_stack.cpp @@ -39,10 +39,10 @@ write_stackt::write_stackt( if(expr.type().id() == ID_array) { // We are assigning an array to a pointer, which is equivalent to assigning - // the first element of that arary + // the first element of that array // &(expr)[0] construct_stack_to_pointer( - address_of_exprt(index_exprt(expr, from_integer(0, size_type()))), + address_of_exprt(index_exprt(expr, from_integer(0, signed_size_type()))), environment, ns); } @@ -138,7 +138,7 @@ void write_stackt::construct_stack_to_lvalue( construct_stack_to_lvalue( to_member_expr(expr).struct_op(), environment, ns); } - else if(expr.id() == ID_symbol) + else if(expr.id() == ID_symbol || expr.id() == ID_dynamic_object) { add_to_stack(std::make_shared(expr), environment, ns); } diff --git a/src/analyses/variable-sensitivity/write_stack_entry.cpp b/src/analyses/variable-sensitivity/write_stack_entry.cpp index 74d7deca398..24e06815bc1 100644 --- a/src/analyses/variable-sensitivity/write_stack_entry.cpp +++ b/src/analyses/variable-sensitivity/write_stack_entry.cpp @@ -32,7 +32,9 @@ bool write_stack_entryt::try_squash_in( simple_entryt::simple_entryt(exprt expr) : simple_entry(expr) { // Invalid simple expression added to the stack - PRECONDITION(expr.id() == ID_member || expr.id() == ID_symbol); + PRECONDITION( + expr.id() == ID_member || expr.id() == ID_symbol || + expr.id() == ID_dynamic_object); } /// Get the expression part needed to read this stack entry. For simple