CBMC
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 &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:
135  case NO_INSTRUCTION_TYPE:
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 
211 void 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  {
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  {
291  ieee_floatt tmp(to_constant_expr(rhs));
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  {
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  {
316  ieee_floatt tmp(to_constant_expr(lhs));
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)
Definition: arith_tools.cpp:99
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:117
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:73
goto_programt::const_targett locationt
Definition: ai_domain.h:72
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:762
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
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
typet & type()
Return the type of the expression.
Definition: expr.h:84
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.h:212
operandst & operands()
Definition: expr.h:94
The Boolean constant false.
Definition: std_expr.h:3077
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:181
const exprt & condition() const
Get the condition of gotos, assume, assert.
Definition: goto_program.h:366
const exprt & call_lhs() const
Get the lhs of a FUNCTION_CALL (may be nil)
Definition: goto_program.h:286
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
Definition: goto_program.h:214
const symbol_exprt & dead_symbol() const
Get the symbol for DEAD.
Definition: goto_program.h:244
const symbol_exprt & decl_symbol() const
Get the declared symbol for DECL.
Definition: goto_program.h:228
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
Definition: goto_program.h:200
goto_program_instruction_typet type() const
What kind of instruction?
Definition: goto_program.h:344
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
float_mapt float_map
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)
bool is_bottom() const
void make_less_than_eq(interval_templatet &i)
const irep_idt & id() const
Definition: irep.h:388
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Boolean negation.
Definition: std_expr.h:2332
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
The Boolean constant true.
Definition: std_expr.h:3068
@ FUNCTION_CALL
Definition: goto_program.h:49
@ ATOMIC_END
Definition: goto_program.h:44
@ DEAD
Definition: goto_program.h:48
@ END_FUNCTION
Definition: goto_program.h:42
@ ASSIGN
Definition: goto_program.h:46
@ ASSERT
Definition: goto_program.h:36
@ SET_RETURN_VALUE
Definition: goto_program.h:45
@ ATOMIC_BEGIN
Definition: goto_program.h:43
@ CATCH
Definition: goto_program.h:51
@ END_THREAD
Definition: goto_program.h:40
@ SKIP
Definition: goto_program.h:38
@ NO_INSTRUCTION_TYPE
Definition: goto_program.h:33
@ START_THREAD
Definition: goto_program.h:39
@ THROW
Definition: goto_program.h:50
@ DECL
Definition: goto_program.h:47
@ OTHER
Definition: goto_program.h:37
@ GOTO
Definition: goto_program.h:34
@ INCOMPLETE_GOTO
Definition: goto_program.h:52
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:17
#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:83
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:2455
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3050
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
Definition: std_expr.h:2107
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2357
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:895
int first
Definition: wcwidth.c:65