Skip to content

VSD - Further cross-representation expression evaluation #5887

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 9 commits into from
Mar 8, 2021
Merged
21 changes: 17 additions & 4 deletions src/analyses/variable-sensitivity/abstract_value_object.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -135,8 +135,9 @@ bool any_of_type(const std::vector<abstract_object_pointert> &operands)
operands.begin(),
operands.end(),
[](const abstract_object_pointert &p) {
return std::dynamic_pointer_cast<const representation_type>(p) !=
nullptr;
return (!p->is_top()) &&
(std::dynamic_pointer_cast<const representation_type>(p) !=
nullptr);
}) != operands.end();
}

Expand Down Expand Up @@ -555,13 +556,25 @@ class value_set_evaluator
rewrite_expression(const std::vector<abstract_object_pointert> &ops) const
{
auto operands_expr = exprt::operandst{};
for(auto v : ops)
operands_expr.push_back(v->to_constant());
for(size_t i = 0; i != expression.operands().size(); ++i)
{
const auto &v = ops[i];
if(is_constant_value(v))
operands_expr.push_back(v->to_constant());
else
operands_expr.push_back(expression.operands()[i]);
}
auto rewritten_expr =
exprt(expression.id(), expression.type(), std::move(operands_expr));
return rewritten_expr;
}

static bool is_constant_value(const abstract_object_pointert &v)
{
return std::dynamic_pointer_cast<const constant_abstract_valuet>(v) !=
nullptr;
}

std::vector<value_ranget> operands_as_ranges() const
{
auto unwrapped = std::vector<value_ranget>{};
Expand Down
6 changes: 2 additions & 4 deletions src/analyses/variable-sensitivity/abstract_value_object.h
Original file line number Diff line number Diff line change
Expand Up @@ -287,10 +287,8 @@ class abstract_value_objectt : public abstract_objectt,
virtual index_range_implementation_ptrt
index_range_implementation(const namespacet &ns) const = 0;

virtual value_range_implementation_ptrt value_range_implementation() const
{
return util_make_unique<empty_value_ranget>();
}
virtual value_range_implementation_ptrt
value_range_implementation() const = 0;
};

#endif
Original file line number Diff line number Diff line change
Expand Up @@ -427,6 +427,12 @@ interval_abstract_valuet::index_range_implementation(const namespacet &ns) const
return make_interval_index_range(interval, ns);
}

value_range_implementation_ptrt
interval_abstract_valuet::value_range_implementation() const
{
return make_single_value_range(shared_from_this());
}

void interval_abstract_valuet::get_statistics(
abstract_object_statisticst &statistics,
abstract_object_visitedt &visited,
Expand Down
2 changes: 2 additions & 0 deletions src/analyses/variable-sensitivity/interval_abstract_value.h
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,8 @@ class interval_abstract_valuet : public abstract_value_objectt
index_range_implementation_ptrt
index_range_implementation(const namespacet &ns) const override;

value_range_implementation_ptrt value_range_implementation() const override;

exprt to_constant() const override;
const constant_interval_exprt &to_interval() const
{
Expand Down
23 changes: 15 additions & 8 deletions src/analyses/variable-sensitivity/value_set_abstract_object.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -11,18 +11,17 @@

#include <analyses/variable-sensitivity/constant_abstract_value.h>
#include <analyses/variable-sensitivity/context_abstract_object.h>
#include <analyses/variable-sensitivity/interval_abstract_value.h>
#include <analyses/variable-sensitivity/two_value_array_abstract_object.h>
#include <analyses/variable-sensitivity/value_set_abstract_object.h>
#include <util/make_unique.h>

static index_range_implementation_ptrt
make_value_set_index_range(const abstract_object_sett &vals);
make_value_set_index_range(const std::set<exprt> &vals);

class value_set_index_ranget : public index_range_implementationt
{
public:
explicit value_set_index_ranget(const abstract_object_sett &vals)
explicit value_set_index_ranget(const std::set<exprt> &vals)
: values(vals), cur(), next(values.begin())
{
PRECONDITION(!values.empty());
Expand All @@ -37,7 +36,7 @@ class value_set_index_ranget : public index_range_implementationt
if(next == values.end())
return false;

cur = (*next)->to_constant();
cur = *next;
++next;
return true;
}
Expand All @@ -47,13 +46,13 @@ class value_set_index_ranget : public index_range_implementationt
}

private:
const abstract_object_sett &values;
std::set<exprt> values;
exprt cur;
abstract_object_sett::const_iterator next;
std::set<exprt>::const_iterator next;
};

static index_range_implementation_ptrt
make_value_set_index_range(const abstract_object_sett &vals)
make_value_set_index_range(const std::set<exprt> &vals)
{
return util_make_unique<value_set_index_ranget>(vals);
}
Expand Down Expand Up @@ -146,7 +145,15 @@ value_set_abstract_objectt::index_range_implementation(
if(values.empty())
return make_indeterminate_index_range();

return make_value_set_index_range(values);
std::set<exprt> flattened;
for(const auto &o : values)
{
const auto &v = std::dynamic_pointer_cast<const abstract_value_objectt>(o);
for(auto e : v->index_range(ns))
flattened.insert(e);
}

return make_value_set_index_range(flattened);
}

value_range_implementation_ptrt
Expand Down
3 changes: 1 addition & 2 deletions unit/Makefile
Original file line number Diff line number Diff line change
Expand Up @@ -16,16 +16,15 @@ SRC += analyses/ai/ai.cpp \
analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
analyses/variable-sensitivity/abstract_object/merge.cpp \
analyses/variable-sensitivity/abstract_object/index_range.cpp \
analyses/variable-sensitivity/constant_abstract_value/expression_evaluation.cpp \
analyses/variable-sensitivity/constant_abstract_value/merge.cpp \
analyses/variable-sensitivity/full_array_abstract_object/merge.cpp \
analyses/variable-sensitivity/eval.cpp \
analyses/variable-sensitivity/eval-member-access.cpp \
analyses/variable-sensitivity/interval_abstract_value/meet.cpp \
analyses/variable-sensitivity/full_struct_abstract_object/merge.cpp \
analyses/variable-sensitivity/last_written_location.cpp \
analyses/variable-sensitivity/value_expression_evaluation/expression_evaluation.cpp \
analyses/variable-sensitivity/value_set/abstract_value.cpp \
analyses/variable-sensitivity/value_set_abstract_object/expression_evaluation.cpp \
analyses/variable-sensitivity/value_set_abstract_object/merge.cpp \
analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp \
ansi-c/max_malloc_size.cpp \
Expand Down
129 changes: 103 additions & 26 deletions unit/analyses/variable-sensitivity/abstract_object/index_range.cpp
Original file line number Diff line number Diff line change
@@ -1,17 +1,16 @@
#include "analyses/variable-sensitivity/variable_sensitivity_test_helpers.h"
#include <analyses/variable-sensitivity/abstract_environment.h>
#include <analyses/variable-sensitivity/abstract_object.h>
#include <analyses/variable-sensitivity/constant_abstract_value.h>
#include <analyses/variable-sensitivity/value_set_abstract_object.h>
#include <analyses/variable-sensitivity/variable_sensitivity_object_factory.h>
#include <testing-utils/use_catch.h>
#include <util/arith_tools.h>
#include <util/mathematical_types.h>
#include <util/namespace.h>
#include <util/symbol_table.h>

SCENARIO(
"index_range for constant_abstract_values"
"[core][analyses][variable-sensitivity][constant_abstract_value][index-"
"[core][analyses][variable-sensitivity][constant_abstract_value][index_"
"range]")
{
auto type = signedbv_typet(32);
Expand All @@ -26,8 +25,7 @@ SCENARIO(
{
auto int_value = 99;
auto value_expr = from_integer(int_value, type);
auto value =
std::make_shared<constant_abstract_valuet>(value_expr, env, ns);
auto value = make_constant(value_expr, env, ns);

auto range = value->index_range(ns);

Expand Down Expand Up @@ -59,7 +57,7 @@ SCENARIO(

GIVEN("a top constant's range is has a single nil expression")
{
auto value = std::make_shared<constant_abstract_valuet>(type);
auto value = make_top_constant();

auto range = value->index_range(ns);

Expand All @@ -78,7 +76,7 @@ SCENARIO(

SCENARIO(
"index_range for interval_abstract_values"
"[core][analyses][variable-sensitivity][interval_abstract_value][index-"
"[core][analyses][variable-sensitivity][interval_abstract_value][index_"
"range]")
{
auto object_factory = variable_sensitivity_object_factoryt::configured_with(
Expand All @@ -91,7 +89,7 @@ SCENARIO(

GIVEN("a top intervals's range is empty")
{
auto value = std::make_shared<interval_abstract_valuet>(type, true, false);
auto value = make_top_interval();

auto range = value->index_range(ns);

Expand All @@ -105,8 +103,7 @@ SCENARIO(
{
auto int_value = 99;
auto value_expr = from_integer(int_value, type);
auto value =
std::make_shared<interval_abstract_valuet>(value_expr, env, ns);
auto value = make_interval(value_expr, value_expr, env, ns);

auto range = value->index_range(ns);

Expand All @@ -127,12 +124,9 @@ SCENARIO(
GIVEN("a [99,100] interval's index_range has two elements")
{
auto int_value = 99;
auto value_expr = from_integer(int_value, type);
auto value = std::make_shared<interval_abstract_valuet>(
constant_interval_exprt(
from_integer(int_value, type), from_integer(int_value + 1, type), type),
env,
ns);
auto lower = from_integer(int_value, type);
auto upper = from_integer(int_value + 1, type);
auto value = make_interval(lower, upper, env, ns);

auto range = value->index_range(ns);

Expand All @@ -159,12 +153,9 @@ SCENARIO(
GIVEN("a [99,102] interval's index_range has four elements")
{
auto int_value = 99;
auto value_expr = from_integer(int_value, type);
auto value = std::make_shared<interval_abstract_valuet>(
constant_interval_exprt(
from_integer(int_value, type), from_integer(int_value + 3, type), type),
env,
ns);
auto lower = from_integer(int_value, type);
auto upper = from_integer(int_value + 3, type);
auto value = make_interval(lower, upper, env, ns);

auto range = value->index_range(ns);

Expand All @@ -186,7 +177,7 @@ SCENARIO(

SCENARIO(
"index_range for value_set_abstract_values"
"[core][analyses][variable-sensitivity][value_set_abstract_value][index-"
"[core][analyses][variable-sensitivity][value_set_abstract_value][index_"
"range]")
{
auto object_factory = variable_sensitivity_object_factoryt::configured_with(
Expand All @@ -197,10 +188,9 @@ SCENARIO(
namespacet ns(symbol_table);
auto type = signedbv_typet(32);

GIVEN("a value_set is empty")
GIVEN("a TOP value_set is empty")
{
auto value =
std::make_shared<value_set_abstract_objectt>(type, true, false);
auto value = make_top_value_set();
auto range = value->index_range(ns);

THEN("range should have a nil expr")
Expand All @@ -214,4 +204,91 @@ SCENARIO(
REQUIRE(i == range.end());
}
}
GIVEN("a value_set { 99, 100, 101, 102 } index_range has four elements")
{
auto int_value = 99;
auto _99 = from_integer(int_value, type);
auto _100 = from_integer(100, type);
auto _101 = from_integer(101, type);
auto _102 = from_integer(102, type);
auto value = make_value_set({_99, _100, _101, _102}, env, ns);

auto range = value->index_range(ns);

THEN("range has four values")
{
auto values = std::vector<exprt>();
for(const auto &e : range)
values.push_back(to_constant_expr(e));

REQUIRE(values.size() == 4);
EXPECT(values, {_99, _100, _101, _102});
}
}
GIVEN("a value_set { [99, 102] } index_range has four elements")
{
auto int_value = 99;
auto _99 = from_integer(int_value, type);
auto _100 = from_integer(100, type);
auto _101 = from_integer(101, type);
auto _102 = from_integer(102, type);
auto _99_102 = constant_interval_exprt(_99, _102);
auto value = make_value_set({_99_102}, env, ns);

auto range = value->index_range(ns);

THEN("range has four values")
{
auto values = std::vector<exprt>();
for(const auto &e : range)
values.push_back(to_constant_expr(e));

REQUIRE(values.size() == 4);
EXPECT(values, {_99, _100, _101, _102});
}
}
GIVEN("a value_set { 99, 100, [101, 102] } index_range has four elements")
{
auto int_value = 99;
auto _99 = from_integer(int_value, type);
auto _100 = from_integer(100, type);
auto _101 = from_integer(101, type);
auto _102 = from_integer(102, type);
auto _101_102 = constant_interval_exprt(_101, _102);
auto value = make_value_set({_99, _101_102, _100}, env, ns);

auto range = value->index_range(ns);

THEN("range has four values")
{
auto values = std::vector<exprt>();
for(const auto &e : range)
values.push_back(to_constant_expr(e));

REQUIRE(values.size() == 4);
EXPECT(values, {_99, _100, _101, _102});
}
}
GIVEN("a value_set { [99, 102], 100, 101 } index_range has four elements")
{
auto int_value = 99;
auto _99 = from_integer(int_value, type);
auto _100 = from_integer(100, type);
auto _101 = from_integer(101, type);
auto _102 = from_integer(102, type);
auto _99_102 = constant_interval_exprt(_99, _102);
auto value = make_value_set({_99_102, _100, _101}, env, ns);

auto range = value->index_range(ns);

THEN("range has four values")
{
auto values = std::vector<exprt>();
for(const auto &e : range)
values.push_back(to_constant_expr(e));

REQUIRE(values.size() == 4);
EXPECT(values, {_99, _100, _101, _102});
}
}
}
Loading