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 #endif
17 
18 #include <util/simplify_expr.h>
19 #include <util/std_expr.h>
20 #include <util/arith_tools.h>
21 
23  std::ostream &out,
24  const ai_baset &ai,
25  const namespacet &ns) const
26 {
27  if(bottom)
28  {
29  out << "BOTTOM\n";
30  return;
31  }
32 
33  for(const auto &interval : int_map)
34  {
35  if(interval.second.is_top())
36  continue;
37  if(interval.second.lower_set)
38  out << interval.second.lower << " <= ";
39  out << interval.first;
40  if(interval.second.upper_set)
41  out << " <= " << interval.second.upper;
42  out << "\n";
43  }
44 
45  for(const auto &interval : float_map)
46  {
47  if(interval.second.is_top())
48  continue;
49  if(interval.second.lower_set)
50  out << interval.second.lower << " <= ";
51  out << interval.first;
52  if(interval.second.upper_set)
53  out << " <= " << interval.second.upper;
54  out << "\n";
55  }
56 }
57 
59  locationt from,
60  locationt to,
61  ai_baset &ai,
62  const namespacet &ns)
63 {
64  const goto_programt::instructiont &instruction=*from;
65  switch(instruction.type)
66  {
67  case DECL:
68  havoc_rec(to_code_decl(instruction.code).symbol());
69  break;
70 
71  case DEAD:
72  havoc_rec(to_code_dead(instruction.code).symbol());
73  break;
74 
75  case ASSIGN:
76  assign(to_code_assign(instruction.code));
77  break;
78 
79  case GOTO:
80  {
81  locationt next=from;
82  next++;
83  if(next==to)
84  assume(not_exprt(instruction.guard), ns);
85  else
86  assume(instruction.guard, ns);
87  }
88  break;
89 
90  case ASSUME:
91  assume(instruction.guard, ns);
92  break;
93 
94  case FUNCTION_CALL:
95  {
96  const code_function_callt &code_function_call=
97  to_code_function_call(instruction.code);
98  if(code_function_call.lhs().is_not_nil())
99  havoc_rec(code_function_call.lhs());
100  }
101  break;
102 
103  default:
104  {
105  }
106  }
107 }
108 
122  const interval_domaint &b)
123 {
124  if(b.bottom)
125  return false;
126  if(bottom)
127  {
128  *this=b;
129  return true;
130  }
131 
132  bool result=false;
133 
134  for(int_mapt::iterator it=int_map.begin();
135  it!=int_map.end(); ) // no it++
136  {
137  // search for the variable that needs to be merged
138  // containers have different size and variable order
139  const int_mapt::const_iterator b_it=b.int_map.find(it->first);
140  if(b_it==b.int_map.end())
141  {
142  it=int_map.erase(it);
143  result=true;
144  }
145  else
146  {
147  integer_intervalt previous=it->second;
148  it->second.join(b_it->second);
149  if(it->second!=previous)
150  result=true;
151 
152  it++;
153  }
154  }
155 
156  for(float_mapt::iterator it=float_map.begin();
157  it!=float_map.end(); ) // no it++
158  {
159  const float_mapt::const_iterator b_it=b.float_map.begin();
160  if(b_it==b.float_map.end())
161  {
162  it=float_map.erase(it);
163  result=true;
164  }
165  else
166  {
167  ieee_float_intervalt previous=it->second;
168  it->second.join(b_it->second);
169  if(it->second!=previous)
170  result=true;
171 
172  it++;
173  }
174  }
175 
176  return result;
177 }
178 
179 void interval_domaint::assign(const code_assignt &code_assign)
180 {
181  havoc_rec(code_assign.lhs());
182  assume_rec(code_assign.lhs(), ID_equal, code_assign.rhs());
183 }
184 
186 {
187  if(lhs.id()==ID_if)
188  {
189  havoc_rec(to_if_expr(lhs).true_case());
190  havoc_rec(to_if_expr(lhs).false_case());
191  }
192  else if(lhs.id()==ID_symbol)
193  {
194  irep_idt identifier=to_symbol_expr(lhs).get_identifier();
195 
196  if(is_int(lhs.type()))
197  int_map.erase(identifier);
198  else if(is_float(lhs.type()))
199  float_map.erase(identifier);
200  }
201  else if(lhs.id()==ID_typecast)
202  {
203  havoc_rec(to_typecast_expr(lhs).op());
204  }
205 }
206 
208  const exprt &lhs, irep_idt id, const exprt &rhs)
209 {
210  if(lhs.id()==ID_typecast)
211  return assume_rec(to_typecast_expr(lhs).op(), id, rhs);
212 
213  if(rhs.id()==ID_typecast)
214  return assume_rec(lhs, id, to_typecast_expr(rhs).op());
215 
216  if(id==ID_equal)
217  {
218  assume_rec(lhs, ID_ge, rhs);
219  assume_rec(lhs, ID_le, rhs);
220  return;
221  }
222 
223  if(id==ID_notequal)
224  return; // won't do split
225 
226  if(id==ID_ge)
227  return assume_rec(rhs, ID_le, lhs);
228 
229  if(id==ID_gt)
230  return assume_rec(rhs, ID_lt, lhs);
231 
232  // we now have lhs < rhs or
233  // lhs <= rhs
234 
235  assert(id==ID_lt || id==ID_le);
236 
237  #ifdef DEBUG
238  std::cout << "assume_rec: "
239  << from_expr(lhs) << " " << id << " "
240  << from_expr(rhs) << "\n";
241  #endif
242 
243  if(lhs.id()==ID_symbol && rhs.id()==ID_constant)
244  {
245  irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier();
246 
247  if(is_int(lhs.type()) && is_int(rhs.type()))
248  {
249  mp_integer tmp;
250  to_integer(rhs, tmp);
251  if(id==ID_lt)
252  --tmp;
253  integer_intervalt &ii=int_map[lhs_identifier];
254  ii.make_le_than(tmp);
255  if(ii.is_bottom())
256  make_bottom();
257  }
258  else if(is_float(lhs.type()) && is_float(rhs.type()))
259  {
260  ieee_floatt tmp(to_constant_expr(rhs));
261  if(id==ID_lt)
262  tmp.decrement();
263  ieee_float_intervalt &fi=float_map[lhs_identifier];
264  fi.make_le_than(tmp);
265  if(fi.is_bottom())
266  make_bottom();
267  }
268  }
269  else if(lhs.id()==ID_constant && rhs.id()==ID_symbol)
270  {
271  irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier();
272 
273  if(is_int(lhs.type()) && is_int(rhs.type()))
274  {
275  mp_integer tmp;
276  to_integer(lhs, tmp);
277  if(id==ID_lt)
278  ++tmp;
279  integer_intervalt &ii=int_map[rhs_identifier];
280  ii.make_ge_than(tmp);
281  if(ii.is_bottom())
282  make_bottom();
283  }
284  else if(is_float(lhs.type()) && is_float(rhs.type()))
285  {
286  ieee_floatt tmp(to_constant_expr(lhs));
287  if(id==ID_lt)
288  tmp.increment();
289  ieee_float_intervalt &fi=float_map[rhs_identifier];
290  fi.make_ge_than(tmp);
291  if(fi.is_bottom())
292  make_bottom();
293  }
294  }
295  else if(lhs.id()==ID_symbol && rhs.id()==ID_symbol)
296  {
297  irep_idt lhs_identifier=to_symbol_expr(lhs).get_identifier();
298  irep_idt rhs_identifier=to_symbol_expr(rhs).get_identifier();
299 
300  if(is_int(lhs.type()) && is_int(rhs.type()))
301  {
302  integer_intervalt &lhs_i=int_map[lhs_identifier];
303  integer_intervalt &rhs_i=int_map[rhs_identifier];
304  lhs_i.meet(rhs_i);
305  rhs_i=lhs_i;
306  if(rhs_i.is_bottom())
307  make_bottom();
308  }
309  else if(is_float(lhs.type()) && is_float(rhs.type()))
310  {
311  ieee_float_intervalt &lhs_i=float_map[lhs_identifier];
312  ieee_float_intervalt &rhs_i=float_map[rhs_identifier];
313  lhs_i.meet(rhs_i);
314  rhs_i=lhs_i;
315  if(rhs_i.is_bottom())
316  make_bottom();
317  }
318  }
319 }
320 
322  const exprt &cond,
323  const namespacet &ns)
324 {
325  assume_rec(simplify_expr(cond, ns), false);
326 }
327 
329  const exprt &cond,
330  bool negation)
331 {
332  if(cond.id()==ID_lt || cond.id()==ID_le ||
333  cond.id()==ID_gt || cond.id()==ID_ge ||
334  cond.id()==ID_equal || cond.id()==ID_notequal)
335  {
336  assert(cond.operands().size()==2);
337 
338  if(negation) // !x<y ---> x>=y
339  {
340  if(cond.id()==ID_lt)
341  assume_rec(cond.op0(), ID_ge, cond.op1());
342  else if(cond.id()==ID_le)
343  assume_rec(cond.op0(), ID_gt, cond.op1());
344  else if(cond.id()==ID_gt)
345  assume_rec(cond.op0(), ID_le, cond.op1());
346  else if(cond.id()==ID_ge)
347  assume_rec(cond.op0(), ID_lt, cond.op1());
348  else if(cond.id()==ID_equal)
349  assume_rec(cond.op0(), ID_notequal, cond.op1());
350  else if(cond.id()==ID_notequal)
351  assume_rec(cond.op0(), ID_equal, cond.op1());
352  }
353  else
354  assume_rec(cond.op0(), cond.id(), cond.op1());
355  }
356  else if(cond.id()==ID_not)
357  {
358  assume_rec(to_not_expr(cond).op(), !negation);
359  }
360  else if(cond.id()==ID_and)
361  {
362  if(!negation)
363  forall_operands(it, cond)
364  assume_rec(*it, false);
365  }
366  else if(cond.id()==ID_or)
367  {
368  if(negation)
369  forall_operands(it, cond)
370  assume_rec(*it, true);
371  }
372 }
373 
375 {
376  if(is_int(src.type()))
377  {
378  int_mapt::const_iterator i_it=int_map.find(src.get_identifier());
379  if(i_it==int_map.end())
380  return true_exprt();
381 
382  const integer_intervalt &interval=i_it->second;
383  if(interval.is_top())
384  return true_exprt();
385  if(interval.is_bottom())
386  return false_exprt();
387 
388  exprt::operandst conjuncts;
389 
390  if(interval.upper_set)
391  {
392  exprt tmp=from_integer(interval.upper, src.type());
393  conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));
394  }
395 
396  if(interval.lower_set)
397  {
398  exprt tmp=from_integer(interval.lower, src.type());
399  conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));
400  }
401 
402  return conjunction(conjuncts);
403  }
404  else if(is_float(src.type()))
405  {
406  float_mapt::const_iterator i_it=float_map.find(src.get_identifier());
407  if(i_it==float_map.end())
408  return true_exprt();
409 
410  const ieee_float_intervalt &interval=i_it->second;
411  if(interval.is_top())
412  return true_exprt();
413  if(interval.is_bottom())
414  return false_exprt();
415 
416  exprt::operandst conjuncts;
417 
418  if(interval.upper_set)
419  {
420  exprt tmp=interval.upper.to_expr();
421  conjuncts.push_back(binary_relation_exprt(src, ID_le, tmp));
422  }
423 
424  if(interval.lower_set)
425  {
426  exprt tmp=interval.lower.to_expr();
427  conjuncts.push_back(binary_relation_exprt(tmp, ID_le, src));
428  }
429 
430  return conjunction(conjuncts);
431  }
432  else
433  return true_exprt();
434 }
435 
440 /*
441  * This implementation is aimed at reducing assertions to true, particularly
442  * range checks for arrays and other bounds checks.
443  *
444  * Rather than work with the various kinds of exprt directly, we use assume,
445  * join and is_bottom. It is sufficient for the use case and avoids duplicating
446  * functionality that is in assume anyway.
447  *
448  * As some expressions (1<=a && a<=2) can be represented exactly as intervals
449  * and some can't (a<1 || a>2), the way these operations are used varies
450  * depending on the structure of the expression to try to give the best results.
451  * For example negating a disjunction makes it easier for assume to handle.
452  */
453 
455  exprt &condition,
456  const namespacet &ns) const
457 {
458  bool unchanged=true;
459  interval_domaint d(*this);
460 
461  // merge intervals to properly handle conjunction
462  if(condition.id()==ID_and) // May be directly representable
463  {
465  a.make_top(); // a is everything
466  a.assume(condition, ns); // Restrict a to an over-approximation
467  // of when condition is true
468  if(!a.join(d)) // If d (this) is included in a...
469  { // Then the condition is always true
470  unchanged=condition.is_true();
471  condition.make_true();
472  }
473  }
474  else if(condition.id()==ID_symbol)
475  {
476  // TODO: we have to handle symbol expression
477  }
478  else // Less likely to be representable
479  {
480  d.assume(not_exprt(condition), ns); // Restrict to when condition is false
481  if(d.is_bottom()) // If there there are none...
482  { // Then the condition is always true
483  unchanged=condition.is_true();
484  condition.make_true();
485  }
486  }
487 
488  return unchanged;
489 }
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Definition: std_expr.h:1760
void decrement(bool distinguish_zero=false)
Definition: ieee_float.h:213
Boolean negation.
Definition: std_expr.h:2648
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
static bool is_float(const typet &src)
BigInt mp_integer
Definition: mp_arith.h:19
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
bool is_not_nil() const
Definition: irep.h:104
exprt & op0()
Definition: expr.h:84
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:260
exprt & symbol()
Definition: std_code.h:205
void assume(const exprt &, const namespacet &)
void make_le_than(const T &v)
const irep_idt & get_identifier() const
Definition: std_expr.h:120
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool is_true() const
Definition: expr.cpp:133
typet & type()
Definition: expr.h:60
void join(const interval_templatet< T > &i)
exprt & op()
Definition: std_expr.h:1739
bool is_bottom() const
void make_true()
Definition: expr.cpp:153
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:50
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
void make_bottom() final
The boolean constant true.
Definition: std_expr.h:3742
void assign(const class code_assignt &assignment)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:2836
exprt & rhs()
Definition: std_code.h:162
API to expression classes.
exprt & op1()
Definition: expr.h:87
TO_BE_DOCUMENTED.
Definition: namespace.h:62
A function call.
Definition: std_code.h:657
#define forall_operands(it, expr)
Definition: expr.h:17
void assume_rec(const exprt &, bool negation=false)
void meet(const interval_templatet< T > &i)
void transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns) final
bool is_bottom() const
exprt & symbol()
Definition: std_code.h:247
float_mapt float_map
exprt make_expression(const symbol_exprt &) const
The boolean constant false.
Definition: std_expr.h:3753
std::vector< exprt > operandst
Definition: expr.h:49
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
Definition: std_expr.h:2682
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.
Definition: ai.h:108
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
void increment(bool distinguish_zero=false)
Definition: ieee_float.h:204
goto_programt::const_targett locationt
Definition: ai.h:42
Expression to hold a symbol (variable)
Definition: std_expr.h:82
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
static bool is_int(const typet &src)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:3725
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void make_top() final
Assignment.
Definition: std_code.h:144
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:700