cprover
Loading...
Searching...
No Matches
interval_domain.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Interval Domain
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#include "interval_domain.h"
13
14#ifdef DEBUG
15#include <iostream>
17#endif
18
19#include <util/simplify_expr.h>
20#include <util/std_expr.h>
21#include <util/arith_tools.h>
22
24 std::ostream &out,
25 const ai_baset &,
26 const namespacet &) const
27{
28 if(bottom)
29 {
30 out << "BOTTOM\n";
31 return;
32 }
33
34 for(const auto &interval : int_map)
35 {
36 if(interval.second.is_top())
37 continue;
38 if(interval.second.lower_set)
39 out << interval.second.lower << " <= ";
40 out << interval.first;
41 if(interval.second.upper_set)
42 out << " <= " << interval.second.upper;
43 out << "\n";
44 }
45
46 for(const auto &interval : float_map)
47 {
48 if(interval.second.is_top())
49 continue;
50 if(interval.second.lower_set)
51 out << interval.second.lower << " <= ";
52 out << interval.first;
53 if(interval.second.upper_set)
54 out << " <= " << interval.second.upper;
55 out << "\n";
56 }
57}
58
60 const irep_idt &function_from,
61 trace_ptrt trace_from,
62 const irep_idt &function_to,
63 trace_ptrt trace_to,
64 ai_baset &ai,
65 const namespacet &ns)
66{
67 locationt from{trace_from->current_location()};
68 locationt to{trace_to->current_location()};
69
70 const goto_programt::instructiont &instruction=*from;
71 switch(instruction.type())
72 {
73 case DECL:
74 havoc_rec(instruction.decl_symbol());
75 break;
76
77 case DEAD:
78 havoc_rec(instruction.dead_symbol());
79 break;
80
81 case ASSIGN:
82 assign(instruction.assign_lhs(), instruction.assign_rhs());
83 break;
84
85 case GOTO:
86 {
87 // Comparing iterators is safe as the target must be within the same list
88 // of instructions because this is a GOTO.
89 locationt next = from;
90 next++;
91 if(from->get_target() != next) // If equal then a skip
92 {
93 if(next == to)
94 assume(not_exprt(instruction.condition()), ns);
95 else
96 assume(instruction.condition(), ns);
97 }
98 break;
99 }
100
101 case ASSUME:
102 assume(instruction.condition(), ns);
103 break;
104
105 case FUNCTION_CALL:
106 {
107 const auto &lhs = instruction.call_lhs();
108 if(lhs.is_not_nil())
109 havoc_rec(lhs);
110 break;
111 }
112
113 case CATCH:
114 case THROW:
115 DATA_INVARIANT(false, "Exceptions must be removed before analysis");
116 break;
117 case SET_RETURN_VALUE:
118 DATA_INVARIANT(false, "SET_RETURN_VALUE must be removed before analysis");
119 break;
120 case ATOMIC_BEGIN: // Ignoring is a valid over-approximation
121 case ATOMIC_END: // Ignoring is a valid over-approximation
122 case END_FUNCTION: // No action required
123 case START_THREAD: // Require a concurrent analysis at higher level
124 case END_THREAD: // Require a concurrent analysis at higher level
125 case ASSERT: // No action required
126 case LOCATION: // No action required
127 case SKIP: // No action required
128 break;
129 case OTHER:
130#if 0
131 DATA_INVARIANT(false, "Unclear what is a safe over-approximation of OTHER");
132#endif
133 break;
134 case INCOMPLETE_GOTO:
136 DATA_INVARIANT(false, "Only complete instructions can be analyzed");
137 break;
138 }
139}
140
154 const interval_domaint &b)
155{
156 if(b.bottom)
157 return false;
158 if(bottom)
159 {
160 *this=b;
161 return true;
162 }
163
164 bool result=false;
165
166 for(int_mapt::iterator it=int_map.begin();
167 it!=int_map.end(); ) // no it++
168 {
169 // search for the variable that needs to be merged
170 // containers have different size and variable order
171 const int_mapt::const_iterator b_it=b.int_map.find(it->first);
172 if(b_it==b.int_map.end())
173 {
174 it=int_map.erase(it);
175 result=true;
176 }
177 else
178 {
179 integer_intervalt previous=it->second;
180 it->second.join(b_it->second);
181 if(it->second!=previous)
182 result=true;
183
184 it++;
185 }
186 }
187
188 for(float_mapt::iterator it=float_map.begin();
189 it!=float_map.end(); ) // no it++
190 {
191 const float_mapt::const_iterator b_it=b.float_map.begin();
192 if(b_it==b.float_map.end())
193 {
194 it=float_map.erase(it);
195 result=true;
196 }
197 else
198 {
199 ieee_float_intervalt previous=it->second;
200 it->second.join(b_it->second);
201 if(it->second!=previous)
202 result=true;
203
204 it++;
205 }
206 }
207
208 return result;
209}
210
211void interval_domaint::assign(const exprt &lhs, const exprt &rhs)
212{
213 havoc_rec(lhs);
214 assume_rec(lhs, ID_equal, rhs);
215}
216
218{
219 if(lhs.id()==ID_if)
220 {
221 havoc_rec(to_if_expr(lhs).true_case());
222 havoc_rec(to_if_expr(lhs).false_case());
223 }
224 else if(lhs.id()==ID_symbol)
225 {
226 irep_idt identifier=to_symbol_expr(lhs).get_identifier();
227
228 if(is_int(lhs.type()))
229 int_map.erase(identifier);
230 else if(is_float(lhs.type()))
231 float_map.erase(identifier);
232 }
233 else if(lhs.id()==ID_typecast)
234 {
235 havoc_rec(to_typecast_expr(lhs).op());
236 }
237}
238
240 const exprt &lhs, irep_idt id, const exprt &rhs)
241{
242 if(lhs.id()==ID_typecast)
243 return assume_rec(to_typecast_expr(lhs).op(), id, rhs);
244
245 if(rhs.id()==ID_typecast)
246 return assume_rec(lhs, id, to_typecast_expr(rhs).op());
247
248 if(id==ID_equal)
249 {
250 assume_rec(lhs, ID_ge, rhs);
251 assume_rec(lhs, ID_le, rhs);
252 return;
253 }
254
255 if(id==ID_notequal)
256 return; // won't do split
257
258 if(id==ID_ge)
259 return assume_rec(rhs, ID_le, lhs);
260
261 if(id==ID_gt)
262 return assume_rec(rhs, ID_lt, lhs);
263
264 // we now have lhs < rhs or
265 // lhs <= rhs
266
267 DATA_INVARIANT(id == ID_lt || id == ID_le, "unexpected comparison operator");
268
269#ifdef DEBUG
270 std::cout << "assume_rec: "
271 << from_expr(lhs) << " " << id << " "
272 << from_expr(rhs) << "\n";
273 #endif
274
275 if(lhs.id() == ID_symbol && rhs.is_constant())
276 {
277 irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier();
278
279 if(is_int(lhs.type()) && is_int(rhs.type()))
280 {
282 if(id==ID_lt)
283 --tmp;
284 integer_intervalt &ii=int_map[lhs_identifier];
285 ii.make_le_than(tmp);
286 if(ii.is_bottom())
287 make_bottom();
288 }
289 else if(is_float(lhs.type()) && is_float(rhs.type()))
290 {
292 if(id==ID_lt)
293 tmp.decrement();
294 ieee_float_intervalt &fi=float_map[lhs_identifier];
295 fi.make_le_than(tmp);
296 if(fi.is_bottom())
297 make_bottom();
298 }
299 }
300 else if(lhs.is_constant() && rhs.id() == ID_symbol)
301 {
302 irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier();
303
304 if(is_int(lhs.type()) && is_int(rhs.type()))
305 {
307 if(id==ID_lt)
308 ++tmp;
309 integer_intervalt &ii=int_map[rhs_identifier];
310 ii.make_ge_than(tmp);
311 if(ii.is_bottom())
312 make_bottom();
313 }
314 else if(is_float(lhs.type()) && is_float(rhs.type()))
315 {
317 if(id==ID_lt)
318 tmp.increment();
319 ieee_float_intervalt &fi=float_map[rhs_identifier];
320 fi.make_ge_than(tmp);
321 if(fi.is_bottom())
322 make_bottom();
323 }
324 }
325 else if(lhs.id()==ID_symbol && rhs.id()==ID_symbol)
326 {
327 irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier();
328 irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier();
329
330 if(is_int(lhs.type()) && is_int(rhs.type()))
331 {
332 integer_intervalt &lhs_i=int_map[lhs_identifier];
333 integer_intervalt &rhs_i=int_map[rhs_identifier];
334 if(id == ID_lt && !lhs_i.is_less_than(rhs_i))
335 lhs_i.make_less_than(rhs_i);
336 if(id == ID_le && !lhs_i.is_less_than_eq(rhs_i))
337 lhs_i.make_less_than_eq(rhs_i);
338 }
339 else if(is_float(lhs.type()) && is_float(rhs.type()))
340 {
341 ieee_float_intervalt &lhs_i=float_map[lhs_identifier];
342 ieee_float_intervalt &rhs_i=float_map[rhs_identifier];
343 lhs_i.meet(rhs_i);
344 rhs_i=lhs_i;
345 if(rhs_i.is_bottom())
346 make_bottom();
347 }
348 }
349}
350
352 const exprt &cond,
353 const namespacet &ns)
354{
355 assume_rec(simplify_expr(cond, ns), false);
356}
357
359 const exprt &cond,
360 bool negation)
361{
362 if(cond.id()==ID_lt || cond.id()==ID_le ||
363 cond.id()==ID_gt || cond.id()==ID_ge ||
364 cond.id()==ID_equal || cond.id()==ID_notequal)
365 {
366 const auto &rel = to_binary_relation_expr(cond);
367
368 if(negation) // !x<y ---> x>=y
369 {
370 if(rel.id() == ID_lt)
371 assume_rec(rel.op0(), ID_ge, rel.op1());
372 else if(rel.id() == ID_le)
373 assume_rec(rel.op0(), ID_gt, rel.op1());
374 else if(rel.id() == ID_gt)
375 assume_rec(rel.op0(), ID_le, rel.op1());
376 else if(rel.id() == ID_ge)
377 assume_rec(rel.op0(), ID_lt, rel.op1());
378 else if(rel.id() == ID_equal)
379 assume_rec(rel.op0(), ID_notequal, rel.op1());
380 else if(rel.id() == ID_notequal)
381 assume_rec(rel.op0(), ID_equal, rel.op1());
382 }
383 else
384 assume_rec(rel.op0(), rel.id(), rel.op1());
385 }
386 else if(cond.id()==ID_not)
387 {
388 assume_rec(to_not_expr(cond).op(), !negation);
389 }
390 else if(cond.id()==ID_and)
391 {
392 if(!negation)
393 {
394 for(const auto &op : cond.operands())
395 assume_rec(op, false);
396 }
397 }
398 else if(cond.id()==ID_or)
399 {
400 if(negation)
401 {
402 for(const auto &op : cond.operands())
403 assume_rec(op, true);
404 }
405 }
406}
407
409{
410 if(is_int(src.type()))
411 {
412 int_mapt::const_iterator i_it=int_map.find(src.get_identifier());
413 if(i_it==int_map.end())
414 return true_exprt();
415
416 const integer_intervalt &interval=i_it->second;
417 if(interval.is_top())
418 return true_exprt();
419 if(interval.is_bottom())
420 return false_exprt();
421
422 exprt::operandst conjuncts;
423
424 if(interval.upper_set)
425 {
426 exprt tmp=from_integer(interval.upper, src.type());
427 conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));
428 }
429
430 if(interval.lower_set)
431 {
432 exprt tmp=from_integer(interval.lower, src.type());
433 conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));
434 }
435
436 return conjunction(conjuncts);
437 }
438 else if(is_float(src.type()))
439 {
440 float_mapt::const_iterator i_it=float_map.find(src.get_identifier());
441 if(i_it==float_map.end())
442 return true_exprt();
443
444 const ieee_float_intervalt &interval=i_it->second;
445 if(interval.is_top())
446 return true_exprt();
447 if(interval.is_bottom())
448 return false_exprt();
449
450 exprt::operandst conjuncts;
451
452 if(interval.upper_set)
453 {
454 exprt tmp=interval.upper.to_expr();
455 conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));
456 }
457
458 if(interval.lower_set)
459 {
460 exprt tmp=interval.lower.to_expr();
461 conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));
462 }
463
464 return conjunction(conjuncts);
465 }
466 else
467 return true_exprt();
468}
469
474/*
475 * This implementation is aimed at reducing assertions to true, particularly
476 * range checks for arrays and other bounds checks.
477 *
478 * Rather than work with the various kinds of exprt directly, we use assume,
479 * join and is_bottom. It is sufficient for the use case and avoids duplicating
480 * functionality that is in assume anyway.
481 *
482 * As some expressions (1<=a && a<=2) can be represented exactly as intervals
483 * and some can't (a<1 || a>2), the way these operations are used varies
484 * depending on the structure of the expression to try to give the best results.
485 * For example negating a disjunction makes it easier for assume to handle.
486 */
487
489 exprt &condition,
490 const namespacet &ns) const
491{
492 bool unchanged=true;
493 interval_domaint d(*this);
494
495 // merge intervals to properly handle conjunction
496 if(condition.id()==ID_and) // May be directly representable
497 {
499 a.make_top(); // a is everything
500 a.assume(condition, ns); // Restrict a to an over-approximation
501 // of when condition is true
502 if(!a.join(d)) // If d (this) is included in a...
503 { // Then the condition is always true
504 unchanged=condition.is_true();
505 condition = true_exprt();
506 }
507 }
508 else if(condition.id()==ID_symbol)
509 {
510 // TODO: we have to handle symbol expression
511 }
512 else // Less likely to be representable
513 {
514 d.assume(not_exprt(condition), ns); // Restrict to when condition is false
515 if(d.is_bottom()) // If there there are none...
516 { // Then the condition is always true
517 unchanged=condition.is_true();
518 condition = true_exprt();
519 }
520 }
521
522 return unchanged;
523}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:118
ai_history_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:74
goto_programt::const_targett locationt
Definition ai_domain.h:73
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:39
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
The Boolean constant false.
Definition std_expr.h:3017
This class represents an instruction in the GOTO intermediate representation.
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
const exprt & condition() const
Get the condition of gotos, assume, assert.
goto_program_instruction_typet type() const
What kind of instruction?
void increment(bool distinguish_zero=false)
Definition ieee_float.h:226
void decrement(bool distinguish_zero=false)
Definition ieee_float.h:235
void assign(const exprt &lhs, const exprt &rhs)
static bool is_int(const typet &src)
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
bool is_bottom() const override final
void make_bottom() final override
no states
void assume_rec(const exprt &, bool negation=false)
bool join(const interval_domaint &b)
Sets *this to the mathematical join between the two domains.
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
exprt make_expression(const symbol_exprt &) const
void make_top() final override
all states – the analysis doesn't use this directly (see make_entry) and domains may refuse to implem...
void havoc_rec(const exprt &)
void assume(const exprt &, const namespacet &)
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Uses the abstract state to simplify a given expression using context- specific information.
static bool is_float(const typet &src)
bool is_less_than(const interval_templatet &i)
bool is_less_than_eq(const interval_templatet &i)
void make_le_than(const T &v)
void join(const interval_templatet< T > &i)
void make_ge_than(const T &v)
void make_less_than(interval_templatet &i)
void meet(const interval_templatet< T > &i)
void make_less_than_eq(interval_templatet &i)
const irep_idt & id() const
Definition irep.h:396
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Boolean negation.
Definition std_expr.h:2278
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
The Boolean constant true.
Definition std_expr.h:3008
@ FUNCTION_CALL
@ ATOMIC_END
@ DEAD
@ LOCATION
@ END_FUNCTION
@ ASSIGN
@ ASSERT
@ SET_RETURN_VALUE
@ ATOMIC_BEGIN
@ CATCH
@ END_THREAD
@ SKIP
@ NO_INSTRUCTION_TYPE
@ START_THREAD
@ THROW
@ DECL
@ OTHER
@ GOTO
@ INCOMPLETE_GOTO
@ ASSUME
Interval Domain.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:18
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:63
API to expression classes.
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition std_expr.h:840
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:2051
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2303
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:222