cprover
interval_domain.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Interval Domain
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "interval_domain.h"
13 
14 #ifdef DEBUG
15 #include <iostream>
16 #include <langapi/language_util.h>
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  locationt from,
61  locationt to,
62  ai_baset &,
63  const namespacet &ns)
64 {
65  const goto_programt::instructiont &instruction=*from;
66  switch(instruction.type)
67  {
68  case DECL:
69  havoc_rec(to_code_decl(instruction.code).symbol());
70  break;
71 
72  case DEAD:
73  havoc_rec(to_code_dead(instruction.code).symbol());
74  break;
75 
76  case ASSIGN:
77  assign(to_code_assign(instruction.code));
78  break;
79 
80  case GOTO:
81  {
82  // Comparing iterators is safe as the target must be within the same list
83  // of instructions because this is a GOTO.
84  locationt next=from;
85  next++;
86  if(from->get_target() != next) // If equal then a skip
87  {
88  if(next == to)
89  assume(not_exprt(instruction.guard), ns);
90  else
91  assume(instruction.guard, ns);
92  }
93  }
94  break;
95 
96  case ASSUME:
97  assume(instruction.guard, ns);
98  break;
99 
100  case FUNCTION_CALL:
101  {
102  const code_function_callt &code_function_call=
103  to_code_function_call(instruction.code);
104  if(code_function_call.lhs().is_not_nil())
105  havoc_rec(code_function_call.lhs());
106  }
107  break;
108 
109  default:
110  {
111  }
112  }
113 }
114 
128  const interval_domaint &b)
129 {
130  if(b.bottom)
131  return false;
132  if(bottom)
133  {
134  *this=b;
135  return true;
136  }
137 
138  bool result=false;
139 
140  for(int_mapt::iterator it=int_map.begin();
141  it!=int_map.end(); ) // no it++
142  {
143  // search for the variable that needs to be merged
144  // containers have different size and variable order
145  const int_mapt::const_iterator b_it=b.int_map.find(it->first);
146  if(b_it==b.int_map.end())
147  {
148  it=int_map.erase(it);
149  result=true;
150  }
151  else
152  {
153  integer_intervalt previous=it->second;
154  it->second.join(b_it->second);
155  if(it->second!=previous)
156  result=true;
157 
158  it++;
159  }
160  }
161 
162  for(float_mapt::iterator it=float_map.begin();
163  it!=float_map.end(); ) // no it++
164  {
165  const float_mapt::const_iterator b_it=b.float_map.begin();
166  if(b_it==b.float_map.end())
167  {
168  it=float_map.erase(it);
169  result=true;
170  }
171  else
172  {
173  ieee_float_intervalt previous=it->second;
174  it->second.join(b_it->second);
175  if(it->second!=previous)
176  result=true;
177 
178  it++;
179  }
180  }
181 
182  return result;
183 }
184 
185 void interval_domaint::assign(const code_assignt &code_assign)
186 {
187  havoc_rec(code_assign.lhs());
188  assume_rec(code_assign.lhs(), ID_equal, code_assign.rhs());
189 }
190 
192 {
193  if(lhs.id()==ID_if)
194  {
195  havoc_rec(to_if_expr(lhs).true_case());
196  havoc_rec(to_if_expr(lhs).false_case());
197  }
198  else if(lhs.id()==ID_symbol)
199  {
200  irep_idt identifier=to_symbol_expr(lhs).get_identifier();
201 
202  if(is_int(lhs.type()))
203  int_map.erase(identifier);
204  else if(is_float(lhs.type()))
205  float_map.erase(identifier);
206  }
207  else if(lhs.id()==ID_typecast)
208  {
209  havoc_rec(to_typecast_expr(lhs).op());
210  }
211 }
212 
214  const exprt &lhs, irep_idt id, const exprt &rhs)
215 {
216  if(lhs.id()==ID_typecast)
217  return assume_rec(to_typecast_expr(lhs).op(), id, rhs);
218 
219  if(rhs.id()==ID_typecast)
220  return assume_rec(lhs, id, to_typecast_expr(rhs).op());
221 
222  if(id==ID_equal)
223  {
224  assume_rec(lhs, ID_ge, rhs);
225  assume_rec(lhs, ID_le, rhs);
226  return;
227  }
228 
229  if(id==ID_notequal)
230  return; // won't do split
231 
232  if(id==ID_ge)
233  return assume_rec(rhs, ID_le, lhs);
234 
235  if(id==ID_gt)
236  return assume_rec(rhs, ID_lt, lhs);
237 
238  // we now have lhs < rhs or
239  // lhs <= rhs
240 
241  assert(id==ID_lt || id==ID_le);
242 
243  #ifdef DEBUG
244  std::cout << "assume_rec: "
245  << from_expr(lhs) << " " << id << " "
246  << from_expr(rhs) << "\n";
247  #endif
248 
249  if(lhs.id()==ID_symbol && rhs.id()==ID_constant)
250  {
251  irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier();
252 
253  if(is_int(lhs.type()) && is_int(rhs.type()))
254  {
255  mp_integer tmp;
256  to_integer(rhs, tmp);
257  if(id==ID_lt)
258  --tmp;
259  integer_intervalt &ii=int_map[lhs_identifier];
260  ii.make_le_than(tmp);
261  if(ii.is_bottom())
262  make_bottom();
263  }
264  else if(is_float(lhs.type()) && is_float(rhs.type()))
265  {
266  ieee_floatt tmp(to_constant_expr(rhs));
267  if(id==ID_lt)
268  tmp.decrement();
269  ieee_float_intervalt &fi=float_map[lhs_identifier];
270  fi.make_le_than(tmp);
271  if(fi.is_bottom())
272  make_bottom();
273  }
274  }
275  else if(lhs.id()==ID_constant && rhs.id()==ID_symbol)
276  {
277  irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier();
278 
279  if(is_int(lhs.type()) && is_int(rhs.type()))
280  {
281  mp_integer tmp;
282  to_integer(lhs, tmp);
283  if(id==ID_lt)
284  ++tmp;
285  integer_intervalt &ii=int_map[rhs_identifier];
286  ii.make_ge_than(tmp);
287  if(ii.is_bottom())
288  make_bottom();
289  }
290  else if(is_float(lhs.type()) && is_float(rhs.type()))
291  {
292  ieee_floatt tmp(to_constant_expr(lhs));
293  if(id==ID_lt)
294  tmp.increment();
295  ieee_float_intervalt &fi=float_map[rhs_identifier];
296  fi.make_ge_than(tmp);
297  if(fi.is_bottom())
298  make_bottom();
299  }
300  }
301  else if(lhs.id()==ID_symbol && rhs.id()==ID_symbol)
302  {
303  irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier();
304  irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier();
305 
306  if(is_int(lhs.type()) && is_int(rhs.type()))
307  {
308  integer_intervalt &lhs_i=int_map[lhs_identifier];
309  integer_intervalt &rhs_i=int_map[rhs_identifier];
310  lhs_i.meet(rhs_i);
311  rhs_i=lhs_i;
312  if(rhs_i.is_bottom())
313  make_bottom();
314  }
315  else if(is_float(lhs.type()) && is_float(rhs.type()))
316  {
317  ieee_float_intervalt &lhs_i=float_map[lhs_identifier];
318  ieee_float_intervalt &rhs_i=float_map[rhs_identifier];
319  lhs_i.meet(rhs_i);
320  rhs_i=lhs_i;
321  if(rhs_i.is_bottom())
322  make_bottom();
323  }
324  }
325 }
326 
328  const exprt &cond,
329  const namespacet &ns)
330 {
331  assume_rec(simplify_expr(cond, ns), false);
332 }
333 
335  const exprt &cond,
336  bool negation)
337 {
338  if(cond.id()==ID_lt || cond.id()==ID_le ||
339  cond.id()==ID_gt || cond.id()==ID_ge ||
340  cond.id()==ID_equal || cond.id()==ID_notequal)
341  {
342  assert(cond.operands().size()==2);
343 
344  if(negation) // !x<y ---> x>=y
345  {
346  if(cond.id()==ID_lt)
347  assume_rec(cond.op0(), ID_ge, cond.op1());
348  else if(cond.id()==ID_le)
349  assume_rec(cond.op0(), ID_gt, cond.op1());
350  else if(cond.id()==ID_gt)
351  assume_rec(cond.op0(), ID_le, cond.op1());
352  else if(cond.id()==ID_ge)
353  assume_rec(cond.op0(), ID_lt, cond.op1());
354  else if(cond.id()==ID_equal)
355  assume_rec(cond.op0(), ID_notequal, cond.op1());
356  else if(cond.id()==ID_notequal)
357  assume_rec(cond.op0(), ID_equal, cond.op1());
358  }
359  else
360  assume_rec(cond.op0(), cond.id(), cond.op1());
361  }
362  else if(cond.id()==ID_not)
363  {
364  assume_rec(to_not_expr(cond).op(), !negation);
365  }
366  else if(cond.id()==ID_and)
367  {
368  if(!negation)
369  forall_operands(it, cond)
370  assume_rec(*it, false);
371  }
372  else if(cond.id()==ID_or)
373  {
374  if(negation)
375  forall_operands(it, cond)
376  assume_rec(*it, true);
377  }
378 }
379 
381 {
382  if(is_int(src.type()))
383  {
384  int_mapt::const_iterator i_it=int_map.find(src.get_identifier());
385  if(i_it==int_map.end())
386  return true_exprt();
387 
388  const integer_intervalt &interval=i_it->second;
389  if(interval.is_top())
390  return true_exprt();
391  if(interval.is_bottom())
392  return false_exprt();
393 
394  exprt::operandst conjuncts;
395 
396  if(interval.upper_set)
397  {
398  exprt tmp=from_integer(interval.upper, src.type());
399  conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));
400  }
401 
402  if(interval.lower_set)
403  {
404  exprt tmp=from_integer(interval.lower, src.type());
405  conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));
406  }
407 
408  return conjunction(conjuncts);
409  }
410  else if(is_float(src.type()))
411  {
412  float_mapt::const_iterator i_it=float_map.find(src.get_identifier());
413  if(i_it==float_map.end())
414  return true_exprt();
415 
416  const ieee_float_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=interval.upper.to_expr();
427  conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));
428  }
429 
430  if(interval.lower_set)
431  {
432  exprt tmp=interval.lower.to_expr();
433  conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));
434  }
435 
436  return conjunction(conjuncts);
437  }
438  else
439  return true_exprt();
440 }
441 
446 /*
447  * This implementation is aimed at reducing assertions to true, particularly
448  * range checks for arrays and other bounds checks.
449  *
450  * Rather than work with the various kinds of exprt directly, we use assume,
451  * join and is_bottom. It is sufficient for the use case and avoids duplicating
452  * functionality that is in assume anyway.
453  *
454  * As some expressions (1<=a && a<=2) can be represented exactly as intervals
455  * and some can't (a<1 || a>2), the way these operations are used varies
456  * depending on the structure of the expression to try to give the best results.
457  * For example negating a disjunction makes it easier for assume to handle.
458  */
459 
461  exprt &condition,
462  const namespacet &ns) const
463 {
464  bool unchanged=true;
465  interval_domaint d(*this);
466 
467  // merge intervals to properly handle conjunction
468  if(condition.id()==ID_and) // May be directly representable
469  {
471  a.make_top(); // a is everything
472  a.assume(condition, ns); // Restrict a to an over-approximation
473  // of when condition is true
474  if(!a.join(d)) // If d (this) is included in a...
475  { // Then the condition is always true
476  unchanged=condition.is_true();
477  condition.make_true();
478  }
479  }
480  else if(condition.id()==ID_symbol)
481  {
482  // TODO: we have to handle symbol expression
483  }
484  else // Less likely to be representable
485  {
486  d.assume(not_exprt(condition), ns); // Restrict to when condition is false
487  if(d.is_bottom()) // If there there are none...
488  { // Then the condition is always true
489  unchanged=condition.is_true();
490  condition.make_true();
491  }
492  }
493 
494  return unchanged;
495 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:188
void decrement(bool distinguish_zero=false)
Definition: ieee_float.h:224
Boolean negation.
Definition: std_expr.h:3228
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:291
static bool is_float(const typet &src)
BigInt mp_integer
Definition: mp_arith.h:22
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
bool is_not_nil() const
Definition: irep.h:173
exprt & op0()
Definition: expr.h:72
void havoc_rec(const exprt &)
exprt simplify_expr(const exprt &src, const namespacet &ns)
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:344
const exprt & op() const
Definition: std_expr.h:340
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:185
exprt & symbol()
Definition: std_code.h:268
void assume(const exprt &, const namespacet &)
void make_le_than(const T &v)
const irep_idt & get_identifier() const
Definition: std_expr.h:128
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void make_top() final override
all states – the analysis doesn&#39;t use this, and domains may refuse to implement it...
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
void join(const interval_templatet< T > &i)
void transform(locationt from, locationt 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...
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:173
void make_true()
Definition: expr.cpp:144
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:48
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:240
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:209
The boolean constant true.
Definition: std_expr.h:4486
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
void assign(const class code_assignt &assignment)
exprt & rhs()
Definition: std_code.h:214
API to expression classes.
exprt & op1()
Definition: expr.h:75
TO_BE_DOCUMENTED.
Definition: namespace.h:74
A function call.
Definition: std_code.h:858
#define forall_operands(it, expr)
Definition: expr.h:17
void assume_rec(const exprt &, bool negation=false)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
void meet(const interval_templatet< T > &i)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
bool is_bottom() const
exprt & symbol()
Definition: std_code.h:321
float_mapt float_map
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4463
exprt make_expression(const symbol_exprt &) const
The boolean constant false.
Definition: std_expr.h:4497
std::vector< exprt > operandst
Definition: expr.h:45
void make_bottom() final override
no states
virtual bool ai_simplify(exprt &condition, const namespacet &ns) const override
Uses the abstract state to simplify a given expression using context- specific information.
Interval Domain.
void make_ge_than(const T &v)
bool join(const interval_domaint &b)
Sets *this to the mathematical join between the two domains.
The basic interface of an abstract interpreter.
Definition: ai.h:32
Base class for all expressions.
Definition: expr.h:42
void increment(bool distinguish_zero=false)
Definition: ieee_float.h:215
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:2143
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
Definition: std_expr.h:3252
goto_programt::const_targett locationt
Definition: ai_domain.h:40
Expression to hold a symbol (variable)
Definition: std_expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
static bool is_int(const typet &src)
bool is_bottom() const override final
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Assignment.
Definition: std_code.h:196
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:909