Skip to content

Commit ae6775a

Browse files
tautschnigtautschnig
authored
Merge pull request #1790 from martin-cs/fix/correct-domain-interface
Fix/correct domain interface
2 parents 2c69364 + d7bb937 commit ae6775a

22 files changed

+80
-107
lines changed

‎src/analyses/ai.cpp

+4-8
Original file line numberDiff line numberDiff line change
@@ -365,8 +365,7 @@ bool ai_baset::visit(
365365
// initialize state, if necessary
366366
get_state(to_l);
367367

368-
new_values.transform(
369-
l, to_l, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL);
368+
new_values.transform(l, to_l, *this, ns);
370369

371370
if(merge(new_values, l, to_l))
372371
have_new_values=true;
@@ -399,8 +398,7 @@ bool ai_baset::do_function_call(
399398
{
400399
// if we don't have a body, we just do an edige call -> return
401400
std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
402-
tmp_state->transform(
403-
l_call, l_return, *this, ns, ai_domain_baset::edge_typet::FUNCTION_LOCAL);
401+
tmp_state->transform(l_call, l_return, *this, ns);
404402

405403
return merge(*tmp_state, l_call, l_return);
406404
}
@@ -417,8 +415,7 @@ bool ai_baset::do_function_call(
417415

418416
// do the edge from the call site to the beginning of the function
419417
std::unique_ptr<statet> tmp_state(make_temporary_state(get_state(l_call)));
420-
tmp_state->transform(
421-
l_call, l_begin, *this, ns, ai_domain_baset::edge_typet::CALL);
418+
tmp_state->transform(l_call, l_begin, *this, ns);
422419

423420
bool new_data=false;
424421

@@ -445,8 +442,7 @@ bool ai_baset::do_function_call(
445442
return false; // function exit point not reachable
446443

447444
std::unique_ptr<statet> tmp_state(make_temporary_state(end_state));
448-
tmp_state->transform(
449-
l_end, l_return, *this, ns, ai_domain_baset::edge_typet::RETURN);
445+
tmp_state->transform(l_end, l_return, *this, ns);
450446

451447
// Propagate those
452448
return merge(*tmp_state, l_end, l_return);

‎src/analyses/ai.h

+15-9
Original file line numberDiff line numberDiff line change
@@ -31,13 +31,6 @@ class ai_baset;
3131
class ai_domain_baset
3232
{
3333
public:
34-
enum class edge_typet
35-
{
36-
FUNCTION_LOCAL,
37-
CALL,
38-
RETURN,
39-
};
40-
4134
// The constructor is expected to produce 'false'
4235
// or 'bottom'
4336
ai_domain_baset()
@@ -55,13 +48,21 @@ class ai_domain_baset
5548
// b) there is an edge from the last instruction (END_FUNCTION)
5649
// of the function to the instruction _following_ the call site
5750
// (this also needs to set the LHS, if applicable)
51+
//
52+
// "this" is the domain before the instruction "from"
53+
// "from" is the instruction to be interpretted
54+
// "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)
55+
//
56+
// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
57+
// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
58+
// PRECONDITION(are_comparable(from,to) ||
59+
// (from->is_function_call() || from->is_end_function())
5860

5961
virtual void transform(
6062
locationt from,
6163
locationt to,
6264
ai_baset &ai,
63-
const namespacet &ns,
64-
edge_typet edge_type) = 0;
65+
const namespacet &ns) = 0;
6566

6667
virtual void output(
6768
std::ostream &out,
@@ -98,6 +99,11 @@ class ai_domain_baset
9899
//
99100
// This computes the join between "this" and "b".
100101
// Return true if "this" has changed.
102+
// In the usual case, "b" is the updated state after "from"
103+
// and "this" is the state before "to".
104+
//
105+
// PRECONDITION(from.is_dereferenceable(), "Must not be _::end()")
106+
// PRECONDITION(to.is_dereferenceable(), "Must not be _::end()")
101107

102108
// This method allows an expression to be simplified / evaluated using the
103109
// current state. It is used to evaluate assertions and in program

‎src/analyses/constant_propagator.cpp

+8-6
Original file line numberDiff line numberDiff line change
@@ -45,8 +45,7 @@ void constant_propagator_domaint::transform(
4545
locationt from,
4646
locationt to,
4747
ai_baset &ai,
48-
const namespacet &ns,
49-
ai_domain_baset::edge_typet edge_type)
48+
const namespacet &ns)
5049
{
5150
#ifdef DEBUG
5251
std::cout << "Transform from/to:\n";
@@ -94,6 +93,8 @@ void constant_propagator_domaint::transform(
9493
{
9594
exprt g;
9695

96+
// Comparing iterators is safe as the target must be within the same list
97+
// of instructions because this is a GOTO.
9798
if(from->get_target()==to)
9899
g=simplify_expr(from->guard, ns);
99100
else
@@ -122,15 +123,14 @@ void constant_propagator_domaint::transform(
122123
const code_function_callt &function_call=to_code_function_call(from->code);
123124
const exprt &function=function_call.function();
124125

125-
const locationt& next=std::next(from);
126-
127126
if(function.id()==ID_symbol)
128127
{
129128
// called function identifier
130129
const symbol_exprt &symbol_expr=to_symbol_expr(function);
131130
const irep_idt id=symbol_expr.get_identifier();
132131

133-
if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL)
132+
// Functions with no body
133+
if(from->function == to->function)
134134
{
135135
if(id==CPROVER_PREFIX "set_must" ||
136136
id==CPROVER_PREFIX "get_must" ||
@@ -178,7 +178,9 @@ void constant_propagator_domaint::transform(
178178
else
179179
{
180180
// unresolved call
181-
INVARIANT(to==next, "Unresolved call can only be approximated if a skip");
181+
INVARIANT(
182+
from->function == to->function,
183+
"Unresolved call can only be approximated if a skip");
182184

183185
if(have_dirty)
184186
values.set_dirty_to_top(cp->dirty, ns);

‎src/analyses/constant_propagator.h

+1-2
Original file line numberDiff line numberDiff line change
@@ -25,8 +25,7 @@ class constant_propagator_domaint:public ai_domain_baset
2525
locationt from,
2626
locationt to,
2727
ai_baset &ai_base,
28-
const namespacet &ns,
29-
ai_domain_baset::edge_typet edge_type) final override;
28+
const namespacet &ns) final override;
3029

3130
virtual void output(
3231
std::ostream &out,

‎src/analyses/custom_bitvector_analysis.cpp

+4-3
Original file line numberDiff line numberDiff line change
@@ -269,8 +269,7 @@ void custom_bitvector_domaint::transform(
269269
locationt from,
270270
locationt to,
271271
ai_baset &ai,
272-
const namespacet &ns,
273-
ai_domain_baset::edge_typet edge_type)
272+
const namespacet &ns)
274273
{
275274
// upcast of ai
276275
custom_bitvector_analysist &cba=
@@ -397,7 +396,7 @@ void custom_bitvector_domaint::transform(
397396
else
398397
{
399398
// only if there is an actual call, i.e., we have a body
400-
if(edge_type != ai_domain_baset::edge_typet::FUNCTION_LOCAL)
399+
if(from->function != to->function)
401400
{
402401
const code_typet &code_type=
403402
to_code_type(ns.lookup(identifier).type);
@@ -520,6 +519,8 @@ void custom_bitvector_domaint::transform(
520519
{
521520
exprt guard=instruction.guard;
522521

522+
// Comparing iterators is safe as the target must be within the same list
523+
// of instructions because this is a GOTO.
523524
if(to!=from->get_target())
524525
guard.make_not();
525526

‎src/analyses/custom_bitvector_analysis.h

+3-6
Original file line numberDiff line numberDiff line change
@@ -23,12 +23,9 @@ class custom_bitvector_analysist;
2323
class custom_bitvector_domaint:public ai_domain_baset
2424
{
2525
public:
26-
void transform(
27-
locationt from,
28-
locationt to,
29-
ai_baset &ai,
30-
const namespacet &ns,
31-
ai_domain_baset::edge_typet edge_type) final override;
26+
void
27+
transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
28+
final override;
3229

3330
void output(
3431
std::ostream &out,

‎src/analyses/dependence_graph.cpp

+3-5
Original file line numberDiff line numberDiff line change
@@ -187,24 +187,22 @@ void dep_graph_domaint::transform(
187187
goto_programt::const_targett from,
188188
goto_programt::const_targett to,
189189
ai_baset &ai,
190-
const namespacet &ns,
191-
ai_domain_baset::edge_typet edge_type)
190+
const namespacet &ns)
192191
{
193192
dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
194193
assert(dep_graph!=nullptr);
195194

196195
// propagate control dependencies across function calls
197196
if(from->is_function_call())
198197
{
199-
const goto_programt::const_targett next = std::next(from);
200-
201-
if(edge_type == ai_domain_baset::edge_typet::FUNCTION_LOCAL)
198+
if(from->function == to->function)
202199
{
203200
control_dependencies(from, to, *dep_graph);
204201
}
205202
else
206203
{
207204
// edge to function entry point
205+
const goto_programt::const_targett next = std::next(from);
208206

209207
dep_graph_domaint *s=
210208
dynamic_cast<dep_graph_domaint*>(&(dep_graph->get_state(next)));

‎src/analyses/dependence_graph.h

+1-2
Original file line numberDiff line numberDiff line change
@@ -83,8 +83,7 @@ class dep_graph_domaint:public ai_domain_baset
8383
goto_programt::const_targett from,
8484
goto_programt::const_targett to,
8585
ai_baset &ai,
86-
const namespacet &ns,
87-
ai_domain_baset::edge_typet edge_type) final override;
86+
const namespacet &ns) final override;
8887

8988
void output(
9089
std::ostream &out,

‎src/analyses/escape_analysis.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -165,8 +165,7 @@ void escape_domaint::transform(
165165
locationt from,
166166
locationt to,
167167
ai_baset &ai,
168-
const namespacet &ns,
169-
ai_domain_baset::edge_typet /*edge_type*/)
168+
const namespacet &ns)
170169
{
171170
if(has_values.is_false())
172171
return;

‎src/analyses/escape_analysis.h

+3-6
Original file line numberDiff line numberDiff line change
@@ -28,12 +28,9 @@ class escape_domaint:public ai_domain_baset
2828
{
2929
}
3030

31-
void transform(
32-
locationt from,
33-
locationt to,
34-
ai_baset &ai,
35-
const namespacet &ns,
36-
ai_domain_baset::edge_typet edge_type) final override;
31+
void
32+
transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
33+
final override;
3734

3835
void output(
3936
std::ostream &out,

‎src/analyses/global_may_alias.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -79,8 +79,7 @@ void global_may_alias_domaint::transform(
7979
locationt from,
8080
locationt to,
8181
ai_baset &ai,
82-
const namespacet &ns,
83-
ai_domain_baset::edge_typet /*edge_type*/)
82+
const namespacet &ns)
8483
{
8584
if(has_values.is_false())
8685
return;

‎src/analyses/global_may_alias.h

+3-6
Original file line numberDiff line numberDiff line change
@@ -28,12 +28,9 @@ class global_may_alias_domaint:public ai_domain_baset
2828
{
2929
}
3030

31-
void transform(
32-
locationt from,
33-
locationt to,
34-
ai_baset &ai,
35-
const namespacet &ns,
36-
ai_domain_baset::edge_typet edge_type) final override;
31+
void
32+
transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
33+
final override;
3734

3835
void output(
3936
std::ostream &out,

‎src/analyses/interval_domain.cpp

+10-6
Original file line numberDiff line numberDiff line change
@@ -59,8 +59,7 @@ void interval_domaint::transform(
5959
locationt from,
6060
locationt to,
6161
ai_baset &ai,
62-
const namespacet &ns,
63-
ai_domain_baset::edge_typet /*edge_type*/)
62+
const namespacet &ns)
6463
{
6564
const goto_programt::instructiont &instruction=*from;
6665
switch(instruction.type)
@@ -79,12 +78,17 @@ void interval_domaint::transform(
7978

8079
case GOTO:
8180
{
81+
// Comparing iterators is safe as the target must be within the same list
82+
// of instructions because this is a GOTO.
8283
locationt next=from;
8384
next++;
84-
if(next==to)
85-
assume(not_exprt(instruction.guard), ns);
86-
else
87-
assume(instruction.guard, ns);
85+
if(from->get_target() != next) // If equal then a skip
86+
{
87+
if(next == to)
88+
assume(not_exprt(instruction.guard), ns);
89+
else
90+
assume(instruction.guard, ns);
91+
}
8892
}
8993
break;
9094

‎src/analyses/interval_domain.h

+3-6
Original file line numberDiff line numberDiff line change
@@ -32,12 +32,9 @@ class interval_domaint:public ai_domain_baset
3232
{
3333
}
3434

35-
void transform(
36-
locationt from,
37-
locationt to,
38-
ai_baset &ai,
39-
const namespacet &ns,
40-
ai_domain_baset::edge_typet edge_type) final override;
35+
void
36+
transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
37+
final override;
4138

4239
void output(
4340
std::ostream &out,

‎src/analyses/invariant_set_domain.cpp

+3-2
Original file line numberDiff line numberDiff line change
@@ -17,13 +17,14 @@ void invariant_set_domaint::transform(
1717
locationt from_l,
1818
locationt to_l,
1919
ai_baset &ai,
20-
const namespacet &ns,
21-
ai_domain_baset::edge_typet /*edge_type*/)
20+
const namespacet &ns)
2221
{
2322
switch(from_l->type)
2423
{
2524
case GOTO:
2625
{
26+
// Comparing iterators is safe as the target must be within the same list
27+
// of instructions because this is a GOTO.
2728
exprt tmp(from_l->guard);
2829

2930
goto_programt::const_targett next=from_l;

‎src/analyses/invariant_set_domain.h

+1-2
Original file line numberDiff line numberDiff line change
@@ -56,8 +56,7 @@ class invariant_set_domaint:public ai_domain_baset
5656
locationt from_l,
5757
locationt to_l,
5858
ai_baset &ai,
59-
const namespacet &ns,
60-
ai_domain_baset::edge_typet edge_type) final override;
59+
const namespacet &ns) final override;
6160

6261
void make_top() final override
6362
{

‎src/analyses/is_threaded.cpp

+3-6
Original file line numberDiff line numberDiff line change
@@ -48,12 +48,9 @@ class is_threaded_domaint:public ai_domain_baset
4848
old_is_threaded!=is_threaded;
4949
}
5050

51-
void transform(
52-
locationt from,
53-
locationt to,
54-
ai_baset &ai,
55-
const namespacet &ns,
56-
ai_domain_baset::edge_typet /*edge_type*/) final override
51+
void
52+
transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
53+
final override
5754
{
5855
// assert(reachable);
5956

0 commit comments

Comments
 (0)