Skip to content

Commit 2d3ffb0

Browse files
committed
Explicitly create values with the required representation
When we create values through the factory, the representation used is determined by the factory configuration. Up until now, that configuration has always lined up with the representation - eg if we were evaluating using intervals, then the factory is creating intervals. This is no longer the case. As we move forward with cross-representation evaluation, it's entirely possible that the factory configuration does _not_ match the representation we have in hand during an evaluation. Consequently, if we need a new constant value we should directly create it. As we leave the expression_transform, we use the factory to wrap any required context around the returned object.
1 parent ea92e73 commit 2d3ffb0

File tree

1 file changed

+40
-49
lines changed

1 file changed

+40
-49
lines changed

src/analyses/variable-sensitivity/abstract_value_object.cpp

Lines changed: 40 additions & 49 deletions
Original file line numberDiff line numberDiff line change
@@ -169,7 +169,15 @@ abstract_object_pointert abstract_value_objectt::expression_transform(
169169
const abstract_environmentt &environment,
170170
const namespacet &ns) const
171171
{
172-
return transform(expr, operands, environment, ns);
172+
auto result = transform(expr, operands, environment, ns);
173+
return environment.add_object_context(result);
174+
}
175+
176+
// evaluation helpers
177+
template <class representation_type>
178+
abstract_object_pointert make_top(const typet &type)
179+
{
180+
return std::make_shared<representation_type>(type, true, false);
173181
}
174182

175183
// constant_abstract_value expression transfrom
@@ -221,8 +229,8 @@ class constants_evaluator
221229
}
222230

223231
// the expression is fully simplified
224-
return environment.abstract_object_factory(
225-
simplified.type(), simplified, ns);
232+
return std::make_shared<constant_abstract_valuet>(
233+
simplified, environment, ns);
226234
}
227235

228236
abstract_object_pointert try_transform_expr_with_all_rounding_modes() const
@@ -274,7 +282,7 @@ class constants_evaluator
274282

275283
abstract_object_pointert top(const typet &type) const
276284
{
277-
return environment.abstract_object_factory(type, ns, true, false);
285+
return make_top<constant_abstract_valuet>(type);
278286
}
279287

280288
bool rounding_mode_is_not_set() const
@@ -351,8 +359,7 @@ class interval_evaluator
351359
}
352360

353361
if(num_operands == 0)
354-
return environment.abstract_object_factory(
355-
expression.type(), ns, true, false);
362+
return make_top<interval_abstract_valuet>(expression.type());
356363

357364
if(expression.id() == ID_if)
358365
return interval_evaluate_conditional(interval_operands);
@@ -371,7 +378,7 @@ class interval_evaluator
371378
INVARIANT(
372379
result.type() == expression.type(),
373380
"Type of result interval should match expression type");
374-
return make_interval(expression.type(), result);
381+
return make_interval(result);
375382
}
376383

377384
std::vector<interval_abstract_value_pointert> operands_as_intervals() const
@@ -391,18 +398,7 @@ class interval_evaluator
391398
if(op_as_constant.is_nil())
392399
return std::vector<interval_abstract_value_pointert>();
393400

394-
const auto ivop =
395-
environment.abstract_object_factory(op->type(), op_as_constant, ns);
396-
const auto ivop_context =
397-
std::dynamic_pointer_cast<const context_abstract_objectt>(ivop);
398-
if(ivop_context)
399-
{
400-
iav = std::dynamic_pointer_cast<const interval_abstract_valuet>(
401-
ivop_context->get_child());
402-
}
403-
else
404-
iav =
405-
std::dynamic_pointer_cast<const interval_abstract_valuet>(ivop);
401+
iav = make_interval(op_as_constant);
406402
}
407403
CHECK_RETURN(
408404
!std::dynamic_pointer_cast<const context_abstract_objectt>(iav));
@@ -429,18 +425,15 @@ class interval_evaluator
429425
{
430426
// Value of the condition is both true and false, so
431427
// combine the intervals of both the true and false expressions
432-
return make_interval(
433-
expression.type(),
434-
constant_interval_exprt(
435-
constant_interval_exprt::get_min(
436-
true_interval.get_lower(), false_interval.get_lower()),
437-
constant_interval_exprt::get_max(
438-
true_interval.get_upper(), false_interval.get_upper())));
428+
return make_interval(constant_interval_exprt(
429+
constant_interval_exprt::get_min(
430+
true_interval.get_lower(), false_interval.get_lower()),
431+
constant_interval_exprt::get_max(
432+
true_interval.get_upper(), false_interval.get_upper())));
439433
}
440434

441-
return condition_result.is_true()
442-
? make_interval(true_interval.type(), true_interval)
443-
: make_interval(false_interval.type(), false_interval);
435+
return condition_result.is_true() ? make_interval(true_interval)
436+
: make_interval(false_interval);
444437
}
445438

446439
abstract_object_pointert interval_evaluate_unary_expr(
@@ -461,21 +454,20 @@ class interval_evaluator
461454
new_interval.type() == expression.type(),
462455
"Type of result interval should match expression type");
463456

464-
return make_interval(tce.type(), new_interval);
457+
return make_interval(new_interval);
465458
}
466459

467460
const constant_interval_exprt &interval_result =
468461
operand_expr.eval(expression.id());
469462
INVARIANT(
470463
interval_result.type() == expression.type(),
471464
"Type of result interval should match expression type");
472-
return make_interval(expression.type(), interval_result);
465+
return make_interval(interval_result);
473466
}
474467

475-
abstract_object_pointert
476-
make_interval(const typet &type, const exprt &expr) const
468+
interval_abstract_value_pointert make_interval(const exprt &expr) const
477469
{
478-
return environment.abstract_object_factory(type, expr, ns);
470+
return std::make_shared<interval_abstract_valuet>(expr, environment, ns);
479471
}
480472

481473
const exprt &expression;
@@ -524,7 +516,7 @@ class value_set_evaluator
524516

525517
auto resulting_objects = evaluate_each_combination(collective_operands);
526518

527-
return resolve_new_values(resulting_objects);
519+
return resolve_values(resulting_objects);
528520
}
529521

530522
/// Evaluate expression for every combination of values in \p value_ranges.
@@ -618,13 +610,6 @@ class value_set_evaluator
618610
return maybe_singleton;
619611
}
620612

621-
abstract_object_pointert
622-
resolve_new_values(const abstract_object_sett &new_values) const
623-
{
624-
auto result = resolve_values(new_values);
625-
return environment.add_object_context(result);
626-
}
627-
628613
static abstract_object_pointert
629614
resolve_values(const abstract_object_sett &new_values)
630615
{
@@ -635,14 +620,20 @@ class value_set_evaluator
635620
if(unwrapped_values.size() > value_set_abstract_objectt::max_value_set_size)
636621
return unwrapped_values.to_interval();
637622

638-
const auto &type = new_values.first()->type();
639-
auto result = std::make_shared<value_set_abstract_objectt>(type);
640-
result->set_values(unwrapped_values);
641-
return result;
623+
return make_value_set(unwrapped_values);
642624
}
643625

644-
abstract_object_pointert
645-
value_set_evaluate_conditional(const std::vector<value_ranget> &ops) const
626+
static abstract_object_pointert
627+
make_value_set(const abstract_object_sett &values)
628+
{
629+
const auto &type = values.first()->type();
630+
auto value_set = std::make_shared<value_set_abstract_objectt>(type);
631+
value_set->set_values(values);
632+
return value_set;
633+
}
634+
635+
static abstract_object_pointert
636+
value_set_evaluate_conditional(const std::vector<value_ranget> &ops)
646637
{
647638
auto const &condition = ops[0];
648639

@@ -664,7 +655,7 @@ class value_set_evaluator
664655
resulting_objects.insert(true_result);
665656
if(all_false || indeterminate)
666657
resulting_objects.insert(false_result);
667-
return resolve_new_values(resulting_objects);
658+
return resolve_values(resulting_objects);
668659
}
669660

670661
const exprt &expression;

0 commit comments

Comments
 (0)