Skip to content

Commit 7d483d4

Browse files
committed
Dereferencing a value-set of pointers
Remove expression_transform and write from value-set of pointers. Dereference value-set of pointers to a single value
1 parent 4bb4246 commit 7d483d4

File tree

7 files changed

+48
-129
lines changed

7 files changed

+48
-129
lines changed
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
#include <assert.h>
2+
3+
int main()
4+
{
5+
int a = 10;
6+
int *p = &a;
7+
8+
int q = *p;
9+
10+
assert(q == a);
11+
}
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--verify --variable-sensitivity --vsd-pointers constants
4+
^\[main.assertion.1\] line 10 assertion q == a: SUCCESS
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--verify --variable-sensitivity --vsd-pointers top-bottom
4+
^\[main.assertion.1\] line 10 assertion q == a: UNKNOWN
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
CORE
2+
main.c
3+
--verify --variable-sensitivity --vsd-pointers value-set
4+
^\[main.assertion.1\] line 10 assertion q == a: SUCCESS
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--

src/analyses/variable-sensitivity/abstract_pointer_object.h

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -62,7 +62,6 @@ class abstract_pointer_objectt : public abstract_objectt,
6262
const abstract_environmentt &env,
6363
const namespacet &ns) const override;
6464

65-
protected:
6665
/// Evaluate reading the pointer's value. More precise
6766
/// abstractions may override this to provide more precise results.
6867
///
@@ -74,6 +73,7 @@ class abstract_pointer_objectt : public abstract_objectt,
7473
const abstract_environmentt &env,
7574
const namespacet &ns) const;
7675

76+
protected:
7777
/// Evaluate writing to a pointer's value. More precise abstractions
7878
/// may override this provide more precise results.
7979
///

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

Lines changed: 11 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -14,13 +14,6 @@
1414
#include <analyses/variable-sensitivity/context_abstract_object.h>
1515
#include <analyses/variable-sensitivity/value_set_pointer_abstract_object.h>
1616

17-
static exprt rewrite_expression(
18-
const exprt &expr,
19-
const std::vector<abstract_object_pointert> &ops);
20-
21-
static std::vector<abstract_object_sett>
22-
unwrap_operands(const std::vector<abstract_object_pointert> &operands);
23-
2417
static abstract_object_sett
2518
unwrap_and_extract_values(const abstract_object_sett &values);
2619

@@ -101,81 +94,25 @@ value_set_pointer_abstract_objectt::value_set_pointer_abstract_objectt(
10194
std::make_shared<constant_pointer_abstract_objectt>(expr, environment, ns));
10295
}
10396

104-
abstract_object_pointert
105-
value_set_pointer_abstract_objectt::expression_transform(
106-
const exprt &expr,
107-
const std::vector<abstract_object_pointert> &operands,
108-
const abstract_environmentt &environment,
109-
const namespacet &ns) const
110-
{
111-
PRECONDITION(operands.size() == expr.operands().size());
112-
113-
auto collective_operands = unwrap_operands(operands);
114-
115-
if(expr.id() == ID_if)
116-
return evaluate_conditional(
117-
expr.type(), collective_operands, environment, ns);
118-
119-
abstract_object_sett resulting_objects;
120-
121-
auto dispatcher = values.first();
122-
for_each_comb(
123-
collective_operands,
124-
[&resulting_objects, &dispatcher, &expr, &environment, &ns](
125-
const std::vector<abstract_object_pointert> &ops) {
126-
auto rewritten_expr = rewrite_expression(expr, ops);
127-
resulting_objects.insert(
128-
dispatcher->expression_transform(rewritten_expr, ops, environment, ns));
129-
});
130-
131-
return resolve_new_values(resulting_objects, environment);
132-
}
133-
134-
abstract_object_pointert
135-
value_set_pointer_abstract_objectt::evaluate_conditional(
136-
const typet &type,
137-
const std::vector<abstract_object_sett> &operands,
97+
abstract_object_pointert value_set_pointer_abstract_objectt::read_dereference(
13898
const abstract_environmentt &env,
13999
const namespacet &ns) const
140100
{
141-
auto const condition = operands[0];
142-
143-
auto const true_result = operands[1];
144-
auto const false_result = operands[2];
145-
146-
auto all_true = true;
147-
auto all_false = true;
148-
for(auto v : condition)
101+
if(is_top() || is_bottom())
149102
{
150-
auto expr = v->to_constant();
151-
all_true = all_true && expr.is_true();
152-
all_false = all_false && expr.is_false();
103+
return env.abstract_object_factory(
104+
type().subtype(), ns, is_top(), !is_top());
153105
}
154-
auto indeterminate = !all_true && !all_false;
155-
156-
abstract_object_sett resulting_objects;
157-
if(all_true || indeterminate)
158-
resulting_objects.insert(true_result);
159-
if(all_false || indeterminate)
160-
resulting_objects.insert(false_result);
161-
return resolve_new_values(resulting_objects, env);
162-
}
163106

164-
abstract_object_pointert value_set_pointer_abstract_objectt::write(
165-
abstract_environmentt &environment,
166-
const namespacet &ns,
167-
const std::stack<exprt> &stack,
168-
const exprt &specifier,
169-
const abstract_object_pointert &value,
170-
bool merging_write) const
171-
{
172-
abstract_object_sett new_values;
173-
for(const auto &st_value : values)
107+
abstract_object_sett results;
108+
for(auto value : values)
174109
{
175-
new_values.insert(
176-
st_value->write(environment, ns, stack, specifier, value, merging_write));
110+
auto pointer =
111+
std::dynamic_pointer_cast<const abstract_pointer_objectt>(value);
112+
results.insert(pointer->read_dereference(env, ns));
177113
}
178-
return resolve_new_values(new_values, environment);
114+
115+
return results.first();
179116
}
180117

181118
abstract_object_pointert value_set_pointer_abstract_objectt::resolve_new_values(
@@ -255,33 +192,6 @@ void value_set_pointer_abstract_objectt::output(
255192
}
256193
}
257194

258-
exprt rewrite_expression(
259-
const exprt &expr,
260-
const std::vector<abstract_object_pointert> &ops)
261-
{
262-
auto operands_expr = exprt::operandst{};
263-
for(auto v : ops)
264-
operands_expr.push_back(v->to_constant());
265-
auto rewritten_expr = exprt(expr.id(), expr.type(), std::move(operands_expr));
266-
return rewritten_expr;
267-
}
268-
269-
std::vector<abstract_object_sett>
270-
unwrap_operands(const std::vector<abstract_object_pointert> &operands)
271-
{
272-
auto unwrapped = std::vector<abstract_object_sett>{};
273-
274-
for(const auto &op : operands)
275-
{
276-
auto vsab =
277-
std::dynamic_pointer_cast<const value_set_tag>(maybe_unwrap_context(op));
278-
INVARIANT(vsab, "should be a value set abstract object");
279-
unwrapped.push_back(vsab->get_values());
280-
}
281-
282-
return unwrapped;
283-
}
284-
285195
abstract_object_sett
286196
unwrap_and_extract_values(const abstract_object_sett &values)
287197
{

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h

Lines changed: 4 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -38,19 +38,9 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
3838
: abstract_objectt::to_constant();
3939
}
4040

41-
/// \copydoc abstract_objectt::expression_transform
42-
///
43-
/// Transforms the \p expr for every combination of \p operands (since these
44-
/// can be value-sets as well).
45-
abstract_object_pointert expression_transform(
46-
const exprt &expr,
47-
const std::vector<abstract_object_pointert> &operands,
48-
const abstract_environmentt &environment,
49-
const namespacet &ns) const override;
50-
5141
/// Getter for the set of stored abstract objects.
5242
/// \return the values represented by this abstract object
53-
const abstract_object_sett &get_values() const
43+
const abstract_object_sett &get_values() const override
5444
{
5545
return values;
5646
}
@@ -63,16 +53,9 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
6353
/// either converted to interval or marked as `top`.
6454
static const size_t max_value_set_size = 10;
6555

66-
/// \copydoc abstract_objectt::write
67-
///
68-
/// Delegate writing to stored values.
69-
abstract_object_pointert write(
70-
abstract_environmentt &environment,
71-
const namespacet &ns,
72-
const std::stack<exprt> &stack,
73-
const exprt &specifier,
74-
const abstract_object_pointert &value,
75-
bool merging_write) const override;
56+
abstract_object_pointert read_dereference(
57+
const abstract_environmentt &env,
58+
const namespacet &ns) const override;
7659

7760
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
7861
const override;
@@ -84,12 +67,6 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
8467
abstract_object_pointert merge(abstract_object_pointert other) const override;
8568

8669
private:
87-
abstract_object_pointert evaluate_conditional(
88-
const typet &type,
89-
const std::vector<abstract_object_sett> &operands,
90-
const abstract_environmentt &env,
91-
const namespacet &ns) const;
92-
9370
/// Update the set of stored values to \p new_values. Build a new abstract
9471
/// object of the right type if necessary.
9572
/// \param new_values: potentially new set of values

0 commit comments

Comments
 (0)