Skip to content

Commit cc26814

Browse files
martinDaniel Kroening
martin
authored and
Daniel Kroening
committed
Fixes and improvements to the constant and interval domain.
1 parent b0846b2 commit cc26814

File tree

3 files changed

+194
-30
lines changed

3 files changed

+194
-30
lines changed

‎src/analyses/constant_propagator.cpp

Lines changed: 183 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,61 @@ Author: Peter Schrammel
1818

1919
/*******************************************************************\
2020
21+
Function: concatenate_array_id
22+
23+
Inputs:
24+
25+
Outputs:
26+
27+
Purpose:
28+
29+
\*******************************************************************/
30+
31+
exprt concatenate_array_id(
32+
const exprt &array, const exprt &index,
33+
const typet &type)
34+
{
35+
std::string a, idx, identifier;
36+
a = array.get_string(ID_identifier);
37+
38+
if (index.id()==ID_typecast)
39+
idx = index.op0().get_string(ID_value);
40+
else
41+
idx = index.get_string(ID_value);
42+
43+
mp_integer i=string2integer(idx);
44+
identifier=a+"["+integer2string(i)+"]";
45+
symbol_exprt new_expr(identifier, type);
46+
47+
return new_expr;
48+
}
49+
50+
/*******************************************************************\
51+
52+
Function: concatenate_array_id
53+
54+
Inputs:
55+
56+
Outputs:
57+
58+
Purpose:
59+
60+
\*******************************************************************/
61+
62+
exprt concatenate_array_id(
63+
const exprt &array, const mp_integer &index,
64+
const typet &type)
65+
{
66+
std::string a, identifier;
67+
a = array.get_string(ID_identifier);
68+
identifier=a+"["+integer2string(index)+"]";
69+
symbol_exprt new_expr(identifier, type);
70+
71+
return new_expr;
72+
}
73+
74+
/*******************************************************************\
75+
2176
Function: constant_propagator_domaint::assign_rec
2277
2378
Inputs:
@@ -33,14 +88,36 @@ void constant_propagator_domaint::assign_rec(
3388
const exprt &lhs, const exprt &rhs,
3489
const namespacet &ns)
3590
{
36-
const typet &rhs_type = ns.follow(rhs.type());
91+
const typet & lhs_type = ns.follow(lhs.type());
92+
const typet & rhs_type = ns.follow(rhs.type());
3793

3894
#ifdef DEBUG
3995
std::cout << "assign: " << from_expr(ns, "", lhs)
4096
<< " := " << from_type(ns, "", rhs_type) << std::endl;
4197
#endif
4298

43-
if(lhs.id()==ID_symbol && rhs_type.id()!=ID_array
99+
if(lhs.id()==ID_symbol && rhs.id()==ID_if)
100+
{
101+
exprt cond=rhs.op0();
102+
assert(cond.operands().size()==2);
103+
if(values.is_constant(cond.op0())
104+
&& values.is_constant(cond.op1()))
105+
{
106+
if(cond.op0().id()==ID_index)
107+
{
108+
exprt index=cond.op0();
109+
exprt new_expr=concatenate_array_id(index.op0(), index.op1(), index.type());
110+
values.replace_const(new_expr);
111+
cond.op0()=new_expr;
112+
cond = simplify_expr(cond,ns);
113+
}
114+
else
115+
assert(0);
116+
117+
assign(values, to_symbol_expr(lhs), cond, ns);
118+
}
119+
}
120+
else if(lhs.id()==ID_symbol && rhs_type.id()!=ID_array
44121
&& rhs_type.id()!=ID_struct
45122
&& rhs_type.id()!=ID_union)
46123
{
@@ -49,6 +126,27 @@ void constant_propagator_domaint::assign_rec(
49126
else
50127
values.set_to_top(to_symbol_expr(lhs));
51128
}
129+
else if(lhs.id()==ID_symbol && lhs_type.id()==ID_array
130+
&& rhs_type.id()==ID_array)
131+
{
132+
exprt new_expr;
133+
mp_integer idx=0;
134+
forall_operands(it, rhs)
135+
{
136+
new_expr=concatenate_array_id(lhs, idx, it->type());
137+
assign(values, to_symbol_expr(new_expr), *it, ns);
138+
idx = idx +1;
139+
}
140+
}
141+
else if (lhs.id()==ID_index)
142+
{
143+
if (values.is_constant(lhs.op1())
144+
&& values.is_constant(rhs))
145+
{
146+
exprt new_expr=concatenate_array_id(lhs.op0(), lhs.op1(), rhs.type());
147+
assign(values, to_symbol_expr(new_expr), rhs, ns);
148+
}
149+
}
52150
#if 0
53151
else // TODO: could make field or array element-sensitive
54152
{
@@ -104,12 +202,22 @@ void constant_propagator_domaint::transform(
104202
else if(from->is_goto())
105203
{
106204
exprt g;
205+
107206
if(from->get_target()==to)
108207
g = simplify_expr(from->guard, ns);
109208
else
110209
g = simplify_expr(not_exprt(from->guard), ns);
111210

112-
two_way_propagate_rec(g, ns);
211+
if (g.is_false())
212+
values.set_to_bottom();
213+
else
214+
{
215+
//TODO: we need to support widening!
216+
if (g.is_constant())
217+
values.set_to_top();
218+
else
219+
two_way_propagate_rec(g, ns);
220+
}
113221
}
114222
else if(from->is_dead())
115223
{
@@ -139,6 +247,7 @@ void constant_propagator_domaint::transform(
139247
else
140248
values.set_to_top();
141249
}
250+
142251
#ifdef DEBUG
143252
std::cout << "after:\n";
144253
output(std::cout, ai, ns);
@@ -224,6 +333,30 @@ void constant_propagator_domaint::assign(
224333

225334
/*******************************************************************\
226335
336+
Function: constant_propagator_domaint::is_array_constant
337+
338+
Inputs:
339+
340+
Outputs:
341+
342+
Purpose:
343+
344+
\*******************************************************************/
345+
346+
bool constant_propagator_domaint::valuest::is_array_constant(const exprt &expr) const
347+
{
348+
exprt new_expr = concatenate_array_id(expr.op0(),
349+
expr.op1(), expr.type());
350+
351+
if (replace_const.expr_map.find(to_symbol_expr(new_expr).get_identifier()) ==
352+
replace_const.expr_map.end())
353+
return false;
354+
355+
return true;
356+
}
357+
358+
/*******************************************************************\
359+
227360
Function: constant_propagator_domaint::valuest::is_constant
228361
229362
Inputs:
@@ -249,6 +382,9 @@ bool constant_propagator_domaint::valuest::is_constant(const exprt &expr) const
249382
replace_const.expr_map.end())
250383
return false;
251384

385+
if (expr.id()==ID_index)
386+
return is_array_constant(expr);
387+
252388
if(expr.id()==ID_address_of)
253389
return is_constant_address_of(to_address_of_expr(expr).object());
254390

@@ -399,38 +535,25 @@ bool constant_propagator_domaint::valuest::merge(const valuest &src)
399535
it!=replace_const.expr_map.end();
400536
) // no it++
401537
{
402-
if(src.replace_const.expr_map.find(it->first) ==
403-
src.replace_const.expr_map.end())
538+
const replace_symbolt::expr_mapt::const_iterator
539+
b_it=src.replace_const.expr_map.find(it->first);
540+
541+
if(b_it==src.replace_const.expr_map.end())
404542
{
405-
// cannot use set_to_top here
406-
replace_const.expr_map.erase(it++);
543+
//cannot use set_to_top here
544+
replace_const.expr_map.erase(it);
407545
changed = true;
546+
break;
408547
}
409-
else ++it;
410-
}
411-
412-
for(const auto &src_replace_pair : src.replace_const.expr_map)
413-
{
414-
replace_symbolt::expr_mapt::iterator c_it=
415-
replace_const.expr_map.find(src_replace_pair.first);
416-
417-
if(c_it!=replace_const.expr_map.end())
548+
else
418549
{
419-
// values are different, set to top
420-
if(c_it->second!=src_replace_pair.second)
421-
{
422-
changed=set_to_top(src_replace_pair.first);
423-
assert(changed);
424-
}
550+
const exprt previous=it->second;
551+
replace_const.expr_map[b_it->first]=b_it->second;
552+
if (it->second != previous) changed = true;
553+
554+
it++;
425555
}
426-
// is not in "this", ignore
427-
else { }
428556
}
429-
430-
#ifdef DEBUG
431-
std::cout << "merged: " << changed << '\n';
432-
#endif
433-
434557
return changed;
435558
}
436559

@@ -519,6 +642,34 @@ void constant_propagator_ait::replace(
519642

520643
/*******************************************************************\
521644
645+
Function: constant_propagator_ait::replace_array_symbol
646+
647+
Inputs:
648+
649+
Outputs:
650+
651+
Purpose:
652+
653+
\*******************************************************************/
654+
655+
void constant_propagator_ait::replace_array_symbol(exprt &expr)
656+
{
657+
if (expr.id()==ID_index)
658+
expr = concatenate_array_id(expr.op0(),
659+
expr.op1(), expr.type());
660+
661+
Forall_operands(it, expr)
662+
{
663+
if (it->id()==ID_equal)
664+
replace_array_symbol(it->op0());
665+
else if (it->id()==ID_index)
666+
replace_array_symbol(expr.op0());
667+
}
668+
669+
}
670+
671+
/*******************************************************************\
672+
522673
Function: constant_propagator_ait::replace
523674
524675
Inputs:
@@ -545,6 +696,7 @@ void constant_propagator_ait::replace(
545696

546697
if(it->is_goto() || it->is_assume() || it->is_assert())
547698
{
699+
replace_array_symbol(it->guard);
548700
s_it->second.values.replace_const(it->guard);
549701
it->guard = simplify_expr(it->guard, ns);
550702
}
@@ -553,6 +705,8 @@ void constant_propagator_ait::replace(
553705
exprt &rhs = to_code_assign(it->code).rhs();
554706
s_it->second.values.replace_const(rhs);
555707
rhs = simplify_expr(rhs, ns);
708+
if (rhs.id()==ID_constant)
709+
rhs.add_source_location()=it->code.op0().source_location();
556710
}
557711
else if(it->is_function_call())
558712
{

‎src/analyses/constant_propagator.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,7 @@ class constant_propagator_domaint:public ai_domain_baset
6262
}
6363

6464
bool is_constant(const exprt &expr) const;
65+
bool is_array_constant(const exprt &expr) const;
6566
bool is_constant_address_of(const exprt &expr) const;
6667
bool set_to_top(const irep_idt &id);
6768

@@ -75,6 +76,7 @@ class constant_propagator_domaint:public ai_domain_baset
7576
replace_const.clear();
7677
is_bottom = false;
7778
}
79+
7880
};
7981

8082
valuest values;
@@ -117,6 +119,11 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
117119
}
118120

119121
protected:
122+
friend class constant_propagator_domaint;
123+
124+
void replace_array_symbol(
125+
exprt &expr);
126+
120127
void replace(
121128
goto_functionst::goto_functiont &,
122129
const namespacet &);
@@ -128,6 +135,7 @@ class constant_propagator_ait:public ait<constant_propagator_domaint>
128135
void replace_types_rec(
129136
const replace_symbolt &replace_const,
130137
exprt &expr);
138+
131139
};
132140

133141
#endif // CPROVER_ANALYSES_CONSTANT_PROPAGATOR_H

‎src/analyses/interval_domain.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -157,7 +157,9 @@ bool interval_domaint::merge(
157157
for(int_mapt::iterator it=int_map.begin();
158158
it!=int_map.end(); ) // no it++
159159
{
160-
const int_mapt::const_iterator b_it=b.int_map.begin();
160+
//search for the variable that needs to be merged
161+
//containers have different size and variable order
162+
const int_mapt::const_iterator b_it=b.int_map.find(it->first);
161163
if(b_it==b.int_map.end())
162164
{
163165
it=int_map.erase(it);

0 commit comments

Comments
 (0)