Skip to content

Commit 5efbdcd

Browse files
committed
Gather interval widening out into a little helper class of its own
1 parent 9bfa965 commit 5efbdcd

File tree

4 files changed

+113
-68
lines changed

4 files changed

+113
-68
lines changed

src/analyses/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,7 @@ SRC = ai.cpp \
5252
variable-sensitivity/variable_sensitivity_dependence_graph.cpp \
5353
variable-sensitivity/variable_sensitivity_domain.cpp \
5454
variable-sensitivity/variable_sensitivity_object_factory.cpp \
55+
variable-sensitivity/widened_range.cpp \
5556
variable-sensitivity/write_location_context.cpp \
5657
variable-sensitivity/write_stack.cpp \
5758
variable-sensitivity/write_stack_entry.cpp \

src/analyses/variable-sensitivity/interval_abstract_value.cpp

Lines changed: 4 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@
1717
#include "abstract_environment.h"
1818
#include "abstract_object_statistics.h"
1919
#include "interval_abstract_value.h"
20+
#include "widened_range.h"
2021

2122
static index_range_implementation_ptrt make_interval_index_range(
2223
const constant_interval_exprt &interval,
@@ -346,83 +347,18 @@ void interval_abstract_valuet::output(
346347
}
347348
}
348349

349-
exprt extend_lower_bound(
350-
const exprt &lower_bound,
351-
const exprt &range,
352-
const namespacet &ns);
353-
exprt extend_upper_bound(
354-
const exprt &upper_bound,
355-
const exprt &range,
356-
const namespacet &ns);
357-
358350
abstract_object_pointert widening_merge(
359351
const constant_interval_exprt &lhs,
360352
const constant_interval_exprt &rhs)
361353
{
362-
auto lower_bound =
363-
constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower());
364-
auto upper_bound =
365-
constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper());
366-
367-
auto dummy_symbol_table = symbol_tablet{};
368-
auto dummy_namespace = namespacet{dummy_symbol_table};
369-
370-
auto range = plus_exprt(
371-
minus_exprt(upper_bound, lower_bound), from_integer(1, lhs.type()));
372-
373-
// should extend lower bound?
374-
if(constant_interval_exprt::less_than(rhs.get_lower(), lhs.get_lower()))
375-
lower_bound = extend_lower_bound(lower_bound, range, dummy_namespace);
376-
// should extend upper bound?
377-
if(constant_interval_exprt::less_than(lhs.get_upper(), rhs.get_upper()))
378-
upper_bound = extend_upper_bound(upper_bound, range, dummy_namespace);
354+
auto widened = widened_ranget(lhs, rhs);
379355

380356
// new interval ...
381-
auto new_interval = constant_interval_exprt(lower_bound, upper_bound);
357+
auto new_interval =
358+
constant_interval_exprt(widened.lower_bound, widened.upper_bound);
382359
return interval_abstract_valuet::make_interval(new_interval);
383360
}
384361

385-
bool has_underflowed(const exprt &value)
386-
{
387-
return constant_interval_exprt::greater_than(
388-
value, from_integer(0, value.type()));
389-
}
390-
bool has_overflowed(const exprt &value)
391-
{
392-
return constant_interval_exprt::less_than(
393-
value, from_integer(0, value.type()));
394-
}
395-
396-
exprt extend_lower_bound(
397-
const exprt &lower_bound,
398-
const exprt &range,
399-
const namespacet &ns)
400-
{
401-
auto new_lower_bound = simplify_expr(minus_exprt(lower_bound, range), ns);
402-
403-
if(
404-
constant_interval_exprt::contains_extreme(new_lower_bound) ||
405-
has_underflowed(new_lower_bound))
406-
return min_exprt(lower_bound.type());
407-
408-
return new_lower_bound;
409-
}
410-
411-
exprt extend_upper_bound(
412-
const exprt &upper_bound,
413-
const exprt &range,
414-
const namespacet &ns)
415-
{
416-
auto new_upper_bound = simplify_expr(plus_exprt(upper_bound, range), ns);
417-
418-
if(
419-
constant_interval_exprt::contains_extreme(new_upper_bound) ||
420-
has_overflowed(new_upper_bound))
421-
return max_exprt(upper_bound.type());
422-
423-
return new_upper_bound;
424-
}
425-
426362
abstract_object_pointert interval_abstract_valuet::merge_with_value(
427363
const abstract_value_pointert &other,
428364
const widen_modet &widen_mode) const
Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
/*******************************************************************\
2+
3+
Module: helper for extending intervals during widening merges
4+
5+
Author: Jez Higgins
6+
7+
\*******************************************************************/
8+
9+
#include "widened_range.h"
10+
#include <util/simplify_expr.h>
11+
12+
static bool has_underflowed(const exprt &value)
13+
{
14+
return constant_interval_exprt::greater_than(
15+
value, from_integer(0, value.type()));
16+
}
17+
static bool has_overflowed(const exprt &value)
18+
{
19+
return constant_interval_exprt::less_than(
20+
value, from_integer(0, value.type()));
21+
}
22+
23+
exprt widened_ranget::make_lower_bound() const
24+
{
25+
if(!lower_extended)
26+
return lower_;
27+
28+
auto new_lower_bound = simplify_expr(minus_exprt(lower_, range_), ns_);
29+
30+
if(
31+
constant_interval_exprt::contains_extreme(new_lower_bound) ||
32+
has_underflowed(new_lower_bound))
33+
return min_exprt(lower_.type());
34+
35+
return new_lower_bound;
36+
}
37+
38+
exprt widened_ranget::make_upper_bound() const
39+
{
40+
if(!upper_extended)
41+
return upper_;
42+
43+
auto new_upper_bound = simplify_expr(plus_exprt(upper_, range_), ns_);
44+
45+
if(
46+
constant_interval_exprt::contains_extreme(new_upper_bound) ||
47+
has_overflowed(new_upper_bound))
48+
return max_exprt(upper_.type());
49+
50+
return new_upper_bound;
51+
}
Lines changed: 57 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,57 @@
1+
/*******************************************************************\
2+
3+
Module: helper for extending intervals during widening merges
4+
5+
Author: Jez Higgins
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H
10+
#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H
11+
12+
#include <util/arith_tools.h>
13+
#include <util/interval.h>
14+
#include <util/namespace.h>
15+
#include <util/symbol_table.h>
16+
17+
class widened_ranget
18+
{
19+
public:
20+
widened_ranget(
21+
const constant_interval_exprt &lhs,
22+
const constant_interval_exprt &rhs)
23+
: lower_extended(
24+
constant_interval_exprt::less_than(rhs.get_lower(), lhs.get_lower())),
25+
upper_extended(
26+
constant_interval_exprt::less_than(lhs.get_upper(), rhs.get_upper())),
27+
ns_(symbol_tablet{}),
28+
lower_(
29+
constant_interval_exprt::get_min(lhs.get_lower(), rhs.get_lower())),
30+
upper_(
31+
constant_interval_exprt::get_max(lhs.get_upper(), rhs.get_upper())),
32+
range_(
33+
plus_exprt(minus_exprt(upper_, lower_), from_integer(1, lhs.type()))),
34+
lower_bound(make_lower_bound()),
35+
upper_bound(make_upper_bound())
36+
{
37+
}
38+
39+
const bool lower_extended;
40+
const bool upper_extended;
41+
42+
private:
43+
namespacet ns_;
44+
exprt lower_;
45+
exprt upper_;
46+
exprt range_;
47+
48+
public:
49+
const exprt lower_bound;
50+
const exprt upper_bound;
51+
52+
private:
53+
exprt make_lower_bound() const;
54+
exprt make_upper_bound() const;
55+
};
56+
57+
#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_WIDENED_RANGE_H

0 commit comments

Comments
 (0)