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  const irep_idt &,
61  locationt from,
62  const irep_idt &,
63  locationt to,
64  ai_baset &,
65  const namespacet &ns)
66 {
67  const goto_programt::instructiont &instruction=*from;
68  switch(instruction.type)
69  {
70  case DECL:
71  havoc_rec(to_code_decl(instruction.code).symbol());
72  break;
73 
74  case DEAD:
75  havoc_rec(to_code_dead(instruction.code).symbol());
76  break;
77 
78  case ASSIGN:
79  assign(to_code_assign(instruction.code));
80  break;
81 
82  case GOTO:
83  {
84  // Comparing iterators is safe as the target must be within the same list
85  // of instructions because this is a GOTO.
86  locationt next=from;
87  next++;
88  if(from->get_target() != next) // If equal then a skip
89  {
90  if(next == to)
91  assume(not_exprt(instruction.guard), ns);
92  else
93  assume(instruction.guard, ns);
94  }
95  }
96  break;
97 
98  case ASSUME:
99  assume(instruction.guard, ns);
100  break;
101 
102  case FUNCTION_CALL:
103  {
104  const code_function_callt &code_function_call=
105  to_code_function_call(instruction.code);
106  if(code_function_call.lhs().is_not_nil())
107  havoc_rec(code_function_call.lhs());
108  }
109  break;
110 
111  default:
112  {
113  }
114  }
115 }
116 
130  const interval_domaint &b)
131 {
132  if(b.bottom)
133  return false;
134  if(bottom)
135  {
136  *this=b;
137  return true;
138  }
139 
140  bool result=false;
141 
142  for(int_mapt::iterator it=int_map.begin();
143  it!=int_map.end(); ) // no it++
144  {
145  // search for the variable that needs to be merged
146  // containers have different size and variable order
147  const int_mapt::const_iterator b_it=b.int_map.find(it->first);
148  if(b_it==b.int_map.end())
149  {
150  it=int_map.erase(it);
151  result=true;
152  }
153  else
154  {
155  integer_intervalt previous=it->second;
156  it->second.join(b_it->second);
157  if(it->second!=previous)
158  result=true;
159 
160  it++;
161  }
162  }
163 
164  for(float_mapt::iterator it=float_map.begin();
165  it!=float_map.end(); ) // no it++
166  {
167  const float_mapt::const_iterator b_it=b.float_map.begin();
168  if(b_it==b.float_map.end())
169  {
170  it=float_map.erase(it);
171  result=true;
172  }
173  else
174  {
175  ieee_float_intervalt previous=it->second;
176  it->second.join(b_it->second);
177  if(it->second!=previous)
178  result=true;
179 
180  it++;
181  }
182  }
183 
184  return result;
185 }
186 
187 void interval_domaint::assign(const code_assignt &code_assign)
188 {
189  havoc_rec(code_assign.lhs());
190  assume_rec(code_assign.lhs(), ID_equal, code_assign.rhs());
191 }
192 
194 {
195  if(lhs.id()==ID_if)
196  {
197  havoc_rec(to_if_expr(lhs).true_case());
198  havoc_rec(to_if_expr(lhs).false_case());
199  }
200  else if(lhs.id()==ID_symbol)
201  {
202  irep_idt identifier=to_symbol_expr(lhs).get_identifier();
203 
204  if(is_int(lhs.type()))
205  int_map.erase(identifier);
206  else if(is_float(lhs.type()))
207  float_map.erase(identifier);
208  }
209  else if(lhs.id()==ID_typecast)
210  {
211  havoc_rec(to_typecast_expr(lhs).op());
212  }
213 }
214 
216  const exprt &lhs, irep_idt id, const exprt &rhs)
217 {
218  if(lhs.id()==ID_typecast)
219  return assume_rec(to_typecast_expr(lhs).op(), id, rhs);
220 
221  if(rhs.id()==ID_typecast)
222  return assume_rec(lhs, id, to_typecast_expr(rhs).op());
223 
224  if(id==ID_equal)
225  {
226  assume_rec(lhs, ID_ge, rhs);
227  assume_rec(lhs, ID_le, rhs);
228  return;
229  }
230 
231  if(id==ID_notequal)
232  return; // won't do split
233 
234  if(id==ID_ge)
235  return assume_rec(rhs, ID_le, lhs);
236 
237  if(id==ID_gt)
238  return assume_rec(rhs, ID_lt, lhs);
239 
240  // we now have lhs < rhs or
241  // lhs <= rhs
242 
243  assert(id==ID_lt || id==ID_le);
244 
245  #ifdef DEBUG
246  std::cout << "assume_rec: "
247  << from_expr(lhs) << " " << id << " "
248  << from_expr(rhs) << "\n";
249  #endif
250 
251  if(lhs.id()==ID_symbol && rhs.id()==ID_constant)
252  {
253  irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier();
254 
255  if(is_int(lhs.type()) && is_int(rhs.type()))
256  {
257  mp_integer tmp = numeric_cast_v<mp_integer>(rhs);
258  if(id==ID_lt)
259  --tmp;
260  integer_intervalt &ii=int_map[lhs_identifier];
261  ii.make_le_than(tmp);
262  if(ii.is_bottom())
263  make_bottom();
264  }
265  else if(is_float(lhs.type()) && is_float(rhs.type()))
266  {
267  ieee_floatt tmp(to_constant_expr(rhs));
268  if(id==ID_lt)
269  tmp.decrement();
270  ieee_float_intervalt &fi=float_map[lhs_identifier];
271  fi.make_le_than(tmp);
272  if(fi.is_bottom())
273  make_bottom();
274  }
275  }
276  else if(lhs.id()==ID_constant && rhs.id()==ID_symbol)
277  {
278  irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier();
279 
280  if(is_int(lhs.type()) && is_int(rhs.type()))
281  {
282  mp_integer tmp = numeric_cast_v<mp_integer>(lhs);
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  const auto &rel = to_binary_relation_expr(cond);
343 
344  if(negation) // !x<y ---> x>=y
345  {
346  if(rel.id() == ID_lt)
347  assume_rec(rel.op0(), ID_ge, rel.op1());
348  else if(rel.id() == ID_le)
349  assume_rec(rel.op0(), ID_gt, rel.op1());
350  else if(rel.id() == ID_gt)
351  assume_rec(rel.op0(), ID_le, rel.op1());
352  else if(rel.id() == ID_ge)
353  assume_rec(rel.op0(), ID_lt, rel.op1());
354  else if(rel.id() == ID_equal)
355  assume_rec(rel.op0(), ID_notequal, rel.op1());
356  else if(rel.id() == ID_notequal)
357  assume_rec(rel.op0(), ID_equal, rel.op1());
358  }
359  else
360  assume_rec(rel.op0(), rel.id(), rel.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 = true_exprt();
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 = true_exprt();
491  }
492  }
493 
494  return unchanged;
495 }
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
exprt guard
Guard for gotos, assume, assert.
Definition: goto_program.h:193
void decrement(bool distinguish_zero=false)
Definition: ieee_float.h:224
Boolean negation.
Definition: std_expr.h:3308
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:399
static bool is_float(const typet &src)
BigInt mp_integer
Definition: mp_arith.h:22
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
bool is_not_nil() const
Definition: irep.h:173
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:473
const exprt & op() const
Definition: std_expr.h:371
goto_program_instruction_typet type
What kind of instruction?
Definition: goto_program.h:190
void assume(const exprt &, const namespacet &)
void make_le_than(const T &v)
const irep_idt & get_identifier() const
Definition: std_expr.h:176
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
typet & type()
Return the type of the expression.
Definition: expr.h:68
void join(const interval_templatet< T > &i)
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:178
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:50
void transform(const irep_idt &function_from, locationt from, const irep_idt &function_to, 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...
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
const irep_idt & id() const
Definition: irep.h:259
exprt & lhs()
Definition: std_code.h:269
The Boolean constant true.
Definition: std_expr.h:4443
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:274
API to expression classes.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:948
codet representation of a function call statement.
Definition: std_code.h:1036
#define forall_operands(it, expr)
Definition: expr.h:20
void assume_rec(const exprt &, bool negation=false)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
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:35
bool is_bottom() const
float_mapt float_map
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
exprt make_expression(const symbol_exprt &) const
The Boolean constant false.
Definition: std_expr.h:4452
std::vector< exprt > operandst
Definition: expr.h:57
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.
symbol_exprt & symbol()
Definition: std_code.h:432
symbol_exprt & symbol()
Definition: std_code.h:360
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:54
void increment(bool distinguish_zero=false)
Definition: ieee_float.h:215
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2306
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:3328
goto_programt::const_targett locationt
Definition: ai_domain.h:40
Expression to hold a symbol (variable)
Definition: std_expr.h:143
static bool is_int(const typet &src)
bool is_bottom() const override final
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
A codet representing an assignment in the program.
Definition: std_code.h:256
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173