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  exprt new_cycle;
24  const exprt &old_cycle=expr.op0();
25  const exprt &cycle_var=expr.op1();
26  const exprt &bound=expr.op2();
27  const exprt &predicate=expr.op3();
28 
29  make_free_bv_expr(expr.type(), new_cycle);
30 
31  mp_integer bound_value;
32  if(to_integer(bound, bound_value))
33  {
35  error() << "waitfor bound must be a constant" << eom;
36  throw 0;
37  }
38 
39  {
40  // constraint: new_cycle>=old_cycle
41 
42  exprt rel_expr(ID_ge, bool_typet());
43  rel_expr.copy_to_operands(new_cycle, old_cycle);
44  set_to_true(rel_expr);
45  }
46 
47  {
48  // constraint: new_cycle<=bound+1
49 
50  exprt one=from_integer(1, bound.type());
51 
52  exprt bound_plus1(ID_plus, bound.type());
53  bound_plus1.reserve_operands(2);
54  bound_plus1.copy_to_operands(bound);
55  bound_plus1.move_to_operands(one);
56 
57  exprt rel_expr(ID_le, bool_typet());
58  rel_expr.copy_to_operands(new_cycle, bound_plus1);
59  set_to_true(rel_expr);
60  }
61 
62  for(mp_integer i=0; i<=bound_value; i=i+1)
63  {
64  // replace cycle_var by old_cycle+i;
65 
66  exprt old_cycle_plus_i(ID_plus, old_cycle.type());
67  old_cycle_plus_i.operands().resize(2);
68  old_cycle_plus_i.op0()=old_cycle;
69  old_cycle_plus_i.op1()=from_integer(i, old_cycle.type());
70 
71  exprt tmp_predicate=predicate;
72  replace_expr(cycle_var, old_cycle_plus_i, tmp_predicate);
73 
74  // CONSTRAINT:
75  // if((cycle)<=bound) {
76  // if((cycle)<new_cycle)
77  // assume(!property);
78  // else if((cycle)==new_cycle)
79  // assume(property);
80 
81  {
82  exprt cycle_le_bound(ID_le, bool_typet());
83  cycle_le_bound.operands().resize(2);
84  cycle_le_bound.op0()=old_cycle_plus_i;
85  cycle_le_bound.op1()=bound;
86 
87  exprt cycle_lt_new_cycle(ID_lt, bool_typet());
88  cycle_lt_new_cycle.operands().resize(2);
89  cycle_lt_new_cycle.op0()=old_cycle_plus_i;
90  cycle_lt_new_cycle.op1()=new_cycle;
91 
92  exprt and_expr(ID_and, bool_typet());
93  and_expr.operands().resize(2);
94  and_expr.op0().swap(cycle_le_bound);
95  and_expr.op1().swap(cycle_lt_new_cycle);
96 
97  exprt top_impl(ID_implies, bool_typet());
98  top_impl.reserve_operands(2);
99  top_impl.move_to_operands(and_expr);
100  top_impl.copy_to_operands(tmp_predicate);
101  top_impl.op1().make_not();
102 
103  set_to_true(top_impl);
104  }
105 
106  {
107  exprt cycle_le_bound(ID_le, bool_typet());
108  cycle_le_bound.operands().resize(2);
109  cycle_le_bound.op0()=old_cycle_plus_i;
110  cycle_le_bound.op1()=bound;
111 
112  exprt cycle_eq_new_cycle(ID_equal, bool_typet());
113  cycle_eq_new_cycle.operands().resize(2);
114  cycle_eq_new_cycle.op0()=old_cycle_plus_i;
115  cycle_eq_new_cycle.op1()=new_cycle;
116 
117  exprt and_expr(ID_and, bool_typet());
118  and_expr.operands().resize(2);
119  and_expr.op0().swap(cycle_le_bound);
120  and_expr.op1().swap(cycle_eq_new_cycle);
121 
122  exprt top_impl(ID_implies, bool_typet());
123  top_impl.reserve_operands(2);
124  top_impl.move_to_operands(and_expr);
125  top_impl.copy_to_operands(tmp_predicate);
126 
127  set_to_true(top_impl);
128  }
129  }
130 
131  // result: new_cycle
132  return convert_bitvector(new_cycle);
133 }
134 
136 {
137  if(expr.operands().size()!=1)
138  {
140  error() << "waitfor_symbol expected to have one operand" << eom;
141  throw 0;
142  }
143 
144  exprt result;
145  const exprt &bound=expr.op0();
146 
147  make_free_bv_expr(expr.type(), result);
148 
149  // constraint: result<=bound
150 
151  exprt rel_expr(ID_le, bool_typet());
152  rel_expr.copy_to_operands(result, bound);
153  set_to_true(rel_expr);
154 
155  return convert_bitvector(result);
156 }
157 
159 {
160  if(expr.id()=="waitfor")
161  return convert_waitfor(expr);
162 
163  if(expr.id()=="waitfor_symbol")
164  return convert_waitfor_symbol(expr);
165 
166  return bv_pointerst::convert_bitvector(expr);
167 }
mstreamt & result()
Definition: message.h:233
BigInt mp_integer
Definition: mp_arith.h:19
exprt & op0()
Definition: expr.h:84
void copy_to_operands(const exprt &expr)
Definition: expr.cpp:61
bvt convert_bitvector(const exprt &expr) override
void move_to_operands(exprt &expr)
Definition: expr.cpp:28
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
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:135
const source_locationt & find_source_location() const
Definition: expr.cpp:466
source_locationt source_location
Definition: message.h:175
virtual void make_free_bv_expr(const typet &type, exprt &dest)
Definition: boolbv.cpp:653
exprt & op1()
Definition: expr.h:87
virtual bvt convert_bitvector(const exprt &expr)
Definition: bv_cbmc.cpp:158
void make_not()
Definition: expr.cpp:100
Base class for all expressions.
Definition: expr.h:46
void set_to_true(const exprt &expr)
void swap(irept &irep)
Definition: irep.h:231
mstreamt & error()
Definition: message.h:223
exprt & op2()
Definition: expr.h:90
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
virtual bvt convert_waitfor(const exprt &expr)
Definition: bv_cbmc.cpp:14
operandst & operands()
Definition: expr.h:70
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::vector< literalt > bvt
Definition: literal.h:197
void reserve_operands(operandst::size_type n)
Definition: expr.h:108
exprt & op3()
Definition: expr.h:93