cprover
bv_cbmc.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "bv_cbmc.h"
10 
11 #include <util/arith_tools.h>
12 #include <util/replace_expr.h>
13 
15 {
16  if(expr.operands().size()!=4)
17  {
19  error() << "waitfor expected to have four operands" << eom;
20  throw 0;
21  }
22 
23  const exprt &old_cycle=expr.op0();
24  const exprt &cycle_var=expr.op1();
25  const exprt &bound=expr.op2();
26  const exprt &predicate=expr.op3();
27  const exprt new_cycle = make_free_bv_expr(expr.type());
28 
29  mp_integer bound_value;
30  if(to_integer(bound, bound_value))
31  {
33  error() << "waitfor bound must be a constant" << eom;
34  throw 0;
35  }
36 
37  {
38  // constraint: new_cycle>=old_cycle
39 
40  set_to_true(binary_relation_exprt(new_cycle, ID_ge, old_cycle));
41  }
42 
43  {
44  // constraint: new_cycle<=bound+1
45 
46  exprt one=from_integer(1, bound.type());
47  const plus_exprt bound_plus1(bound, one);
48  set_to_true(binary_relation_exprt(new_cycle, ID_le, bound_plus1));
49  }
50 
51  for(mp_integer i=0; i<=bound_value; i=i+1)
52  {
53  // replace cycle_var by old_cycle+i;
54 
55  const plus_exprt old_cycle_plus_i(
56  old_cycle, from_integer(i, old_cycle.type()));
57 
58  exprt tmp_predicate=predicate;
59  replace_expr(cycle_var, old_cycle_plus_i, tmp_predicate);
60 
61  // CONSTRAINT:
62  // if((cycle)<=bound) {
63  // if((cycle)<new_cycle)
64  // assume(!property);
65  // else if((cycle)==new_cycle)
66  // assume(property);
67 
68  {
69  const binary_relation_exprt cycle_le_bound(
70  old_cycle_plus_i, ID_le, bound);
71  const binary_relation_exprt cycle_lt_new_cycle(
72  old_cycle_plus_i, ID_lt, new_cycle);
73  const and_exprt and_expr(cycle_le_bound, cycle_lt_new_cycle);
74 
75  implies_exprt top_impl(and_expr, tmp_predicate);
76  top_impl.op1().make_not();
77 
78  set_to_true(top_impl);
79  }
80 
81  {
82  const binary_relation_exprt cycle_le_bound(
83  old_cycle_plus_i, ID_le, bound);
84  const equal_exprt cycle_eq_new_cycle(old_cycle_plus_i, new_cycle);
85  const and_exprt and_expr(cycle_le_bound, cycle_eq_new_cycle);
86 
87  const implies_exprt top_impl(and_expr, tmp_predicate);
88 
89  set_to_true(top_impl);
90  }
91  }
92 
93  // result: new_cycle
94  return convert_bitvector(new_cycle);
95 }
96 
98 {
99  PRECONDITION(expr.operands().size() == 1);
100  const exprt &bound=expr.op0();
101  const exprt result = make_free_bv_expr(expr.type());
102  // constraint: result<=bound
103 
104  set_to_true(binary_relation_exprt(result, ID_le, bound));
105 
106  return convert_bitvector(result);
107 }
108 
110 {
111  if(expr.id()=="waitfor")
112  return convert_waitfor(expr);
113 
114  if(expr.id()=="waitfor_symbol")
115  return convert_waitfor_symbol(expr);
116 
117  return bv_pointerst::convert_bitvector(expr);
118 }
BigInt mp_integer
Definition: mp_arith.h:22
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
exprt & op0()
Definition: expr.h:72
bvt convert_bitvector(const exprt &expr) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
typet & type()
Definition: expr.h:56
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
boolean implication
Definition: std_expr.h:2339
equality
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:189
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
virtual bvt convert_waitfor_symbol(const exprt &expr)
Definition: bv_cbmc.cpp:97
const source_locationt & find_source_location() const
Definition: expr.cpp:246
source_locationt source_location
Definition: message.h:214
boolean AND
Definition: std_expr.h:2255
exprt & op1()
Definition: expr.h:75
mstreamt & error() const
Definition: message.h:302
virtual bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
Definition: bv_cbmc.cpp:109
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
The plus expression.
Definition: std_expr.h:893
virtual exprt make_free_bv_expr(const typet &type)
Definition: boolbv.cpp:622
void make_not()
Definition: expr.cpp:91
mstreamt & result() const
Definition: message.h:312
Base class for all expressions.
Definition: expr.h:42
void set_to_true(const exprt &expr)
exprt & op2()
Definition: expr.h:78
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
virtual bvt convert_waitfor(const exprt &expr)
Definition: bv_cbmc.cpp:14
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::vector< literalt > bvt
Definition: literal.h:200
exprt & op3()
Definition: expr.h:81