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.get_condition()), ns);
95 else
96 assume(instruction.get_condition(), ns);
97 }
98 break;
99 }
100
101 case ASSUME:
102 assume(instruction.get_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 assert(id==ID_lt || id==ID_le);
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.id()==ID_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 {
281 mp_integer tmp = numeric_cast_v<mp_integer>(to_constant_expr(rhs));
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.id()==ID_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 {
306 mp_integer tmp = numeric_cast_v<mp_integer>(to_constant_expr(lhs));
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 forall_operands(it, cond)
394 assume_rec(*it, false);
395 }
396 else if(cond.id()==ID_or)
397 {
398 if(negation)
399 forall_operands(it, cond)
400 assume_rec(*it, true);
401 }
402}
403
405{
406 if(is_int(src.type()))
407 {
408 int_mapt::const_iterator i_it=int_map.find(src.get_identifier());
409 if(i_it==int_map.end())
410 return true_exprt();
411
412 const integer_intervalt &interval=i_it->second;
413 if(interval.is_top())
414 return true_exprt();
415 if(interval.is_bottom())
416 return false_exprt();
417
418 exprt::operandst conjuncts;
419
420 if(interval.upper_set)
421 {
422 exprt tmp=from_integer(interval.upper, src.type());
423 conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));
424 }
425
426 if(interval.lower_set)
427 {
428 exprt tmp=from_integer(interval.lower, src.type());
429 conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));
430 }
431
432 return conjunction(conjuncts);
433 }
434 else if(is_float(src.type()))
435 {
436 float_mapt::const_iterator i_it=float_map.find(src.get_identifier());
437 if(i_it==float_map.end())
438 return true_exprt();
439
440 const ieee_float_intervalt &interval=i_it->second;
441 if(interval.is_top())
442 return true_exprt();
443 if(interval.is_bottom())
444 return false_exprt();
445
446 exprt::operandst conjuncts;
447
448 if(interval.upper_set)
449 {
450 exprt tmp=interval.upper.to_expr();
451 conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));
452 }
453
454 if(interval.lower_set)
455 {
456 exprt tmp=interval.lower.to_expr();
457 conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));
458 }
459
460 return conjunction(conjuncts);
461 }
462 else
463 return true_exprt();
464}
465
470/*
471 * This implementation is aimed at reducing assertions to true, particularly
472 * range checks for arrays and other bounds checks.
473 *
474 * Rather than work with the various kinds of exprt directly, we use assume,
475 * join and is_bottom. It is sufficient for the use case and avoids duplicating
476 * functionality that is in assume anyway.
477 *
478 * As some expressions (1<=a && a<=2) can be represented exactly as intervals
479 * and some can't (a<1 || a>2), the way these operations are used varies
480 * depending on the structure of the expression to try to give the best results.
481 * For example negating a disjunction makes it easier for assume to handle.
482 */
483
485 exprt &condition,
486 const namespacet &ns) const
487{
488 bool unchanged=true;
489 interval_domaint d(*this);
490
491 // merge intervals to properly handle conjunction
492 if(condition.id()==ID_and) // May be directly representable
493 {
495 a.make_top(); // a is everything
496 a.assume(condition, ns); // Restrict a to an over-approximation
497 // of when condition is true
498 if(!a.join(d)) // If d (this) is included in a...
499 { // Then the condition is always true
500 unchanged=condition.is_true();
501 condition = true_exprt();
502 }
503 }
504 else if(condition.id()==ID_symbol)
505 {
506 // TODO: we have to handle symbol expression
507 }
508 else // Less likely to be representable
509 {
510 d.assume(not_exprt(condition), ns); // Restrict to when condition is false
511 if(d.is_bottom()) // If there there are none...
512 { // Then the condition is always true
513 unchanged=condition.is_true();
514 condition = true_exprt();
515 }
516 }
517
518 return unchanged;
519}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:119
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:674
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:33
typet & type()
Return the type of the expression.
Definition expr.h:82
The Boolean constant false.
Definition std_expr.h:2865
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 & get_condition() const
Get the condition of gotos, assume, assert.
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.
goto_program_instruction_typet type() const
What kind of instruction?
void increment(bool distinguish_zero=false)
Definition ieee_float.h:227
void decrement(bool distinguish_zero=false)
Definition ieee_float.h:236
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, and domains may refuse to implement it.
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:2181
Expression to hold a symbol (variable)
Definition std_expr.h:80
const irep_idt & get_identifier() const
Definition std_expr.h:109
The Boolean constant true.
Definition std_expr.h:2856
#define forall_operands(it, expr)
Definition expr.h:18
@ 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:12
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
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:34
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:807
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition std_expr.h:1954
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2291
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2840
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition std_expr.h:2206
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition std_expr.h:189