cprover
boolbv_with.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 "boolbv.h"
10 
11 #include <util/std_types.h>
12 #include <util/std_expr.h>
13 #include <util/arith_tools.h>
14 #include <util/base_type.h>
15 #include <util/config.h>
16 
17 #include "bv_endianness_map.h"
18 
20 {
21  if(expr.operands().size()<3)
22  {
24  error() << "with takes at least three operands" << eom;
25  throw 0;
26  }
27 
28  if((expr.operands().size()%2)!=1)
29  {
31  error() << "with takes an odd number of operands" << eom;
32  throw 0;
33  }
34 
35  bvt bv=convert_bv(expr.op0());
36 
37  std::size_t width=boolbv_width(expr.type());
38 
39  if(width==0)
40  {
41  // A zero-length array is acceptable:
42  if(expr.type().id()==ID_array && boolbv_width(expr.type().subtype())!=0)
43  return bvt();
44  else
45  return conversion_failed(expr);
46  }
47 
48  if(bv.size()!=width)
49  {
51  error() << "unexpected operand 0 width" << eom;
52  throw 0;
53  }
54 
55  bvt prev_bv;
56  prev_bv.resize(width);
57 
58  const exprt::operandst &ops=expr.operands();
59 
60  for(std::size_t op_no=1; op_no<ops.size(); op_no+=2)
61  {
62  bv.swap(prev_bv);
63 
65  expr.op0().type(),
66  ops[op_no],
67  ops[op_no+1],
68  prev_bv,
69  bv);
70  }
71 
72  return bv;
73 }
74 
76  const typet &type,
77  const exprt &op1,
78  const exprt &op2,
79  const bvt &prev_bv,
80  bvt &next_bv)
81 {
82  // we only do that on arrays, bitvectors, structs, and unions
83 
84  next_bv.resize(prev_bv.size());
85 
86  if(type.id()==ID_array)
87  return convert_with_array(to_array_type(type), op1, op2, prev_bv, next_bv);
88  else if(type.id()==ID_bv ||
89  type.id()==ID_unsignedbv ||
90  type.id()==ID_signedbv)
91  return convert_with_bv(op1, op2, prev_bv, next_bv);
92  else if(type.id()==ID_struct)
93  return
94  convert_with_struct(to_struct_type(type), op1, op2, prev_bv, next_bv);
95  else if(type.id()==ID_union)
96  return convert_with_union(to_union_type(type), op2, prev_bv, next_bv);
97  else if(type.id()==ID_symbol)
98  return convert_with(ns.follow(type), op1, op2, prev_bv, next_bv);
99 
101  error() << "unexpected with type: " << type.id();
102  throw 0;
103 }
104 
106  const array_typet &type,
107  const exprt &op1,
108  const exprt &op2,
109  const bvt &prev_bv,
110  bvt &next_bv)
111 {
112  if(is_unbounded_array(type))
113  {
114  // can't do this
116  error() << "convert_with_array called for unbounded array" << eom;
117  throw 0;
118  }
119 
120  const exprt &array_size=type.size();
121 
122  mp_integer size;
123 
124  if(to_integer(array_size, size))
125  {
127  error() << "convert_with_array expects constant array size" << eom;
128  throw 0;
129  }
130 
131  const bvt &op2_bv=convert_bv(op2);
132 
133  if(size*op2_bv.size()!=prev_bv.size())
134  {
136  error() << "convert_with_array: unexpected operand 2 width" << eom;
137  throw 0;
138  }
139 
140  // Is the index a constant?
141  mp_integer op1_value;
142  if(!to_integer(op1, op1_value))
143  {
144  // Yes, it is!
145  next_bv=prev_bv;
146 
147  if(op1_value>=0 && op1_value<size) // bounds check
148  {
149  std::size_t offset=integer2unsigned(op1_value*op2_bv.size());
150 
151  for(std::size_t j=0; j<op2_bv.size(); j++)
152  next_bv[offset+j]=op2_bv[j];
153  }
154 
155  return;
156  }
157 
158  typet counter_type=op1.type();
159 
160  for(mp_integer i=0; i<size; i=i+1)
161  {
162  exprt counter=from_integer(i, counter_type);
163 
164  literalt eq_lit=convert(equal_exprt(op1, counter));
165 
166  std::size_t offset=integer2unsigned(i*op2_bv.size());
167 
168  for(std::size_t j=0; j<op2_bv.size(); j++)
169  next_bv[offset+j]=
170  prop.lselect(eq_lit, op2_bv[j], prev_bv[offset+j]);
171  }
172 }
173 
175  const exprt &op1,
176  const exprt &op2,
177  const bvt &prev_bv,
178  bvt &next_bv)
179 {
180  literalt l=convert(op2);
181 
182  mp_integer op1_value;
183  if(!to_integer(op1, op1_value))
184  {
185  next_bv=prev_bv;
186 
187  if(op1_value<next_bv.size())
188  next_bv[integer2size_t(op1_value)]=l;
189 
190  return;
191  }
192 
193  typet counter_type=op1.type();
194 
195  for(std::size_t i=0; i<prev_bv.size(); i++)
196  {
197  exprt counter=from_integer(i, counter_type);
198 
199  literalt eq_lit=convert(equal_exprt(op1, counter));
200 
201  next_bv[i]=prop.lselect(eq_lit, l, prev_bv[i]);
202  }
203 }
204 
206  const struct_typet &type,
207  const exprt &op1,
208  const exprt &op2,
209  const bvt &prev_bv,
210  bvt &next_bv)
211 {
212  next_bv=prev_bv;
213 
214  const bvt &op2_bv=convert_bv(op2);
215 
216  const irep_idt &component_name=op1.get(ID_component_name);
217  const struct_typet::componentst &components=
218  type.components();
219 
220  std::size_t offset=0;
221 
222  for(struct_typet::componentst::const_iterator
223  it=components.begin();
224  it!=components.end();
225  it++)
226  {
227  const typet &subtype=it->type();
228 
229  std::size_t sub_width=boolbv_width(subtype);
230 
231  if(it->get_name()==component_name)
232  {
233  if(!base_type_eq(subtype, op2.type(), ns))
234  {
236  error() << "with/struct: component `" << component_name
237  << "' type does not match: "
238  << subtype.pretty() << " vs. "
239  << op2.type().pretty() << eom;
240  throw 0;
241  }
242 
243  if(sub_width!=op2_bv.size())
244  {
246  error() << "convert_with_struct: unexpected operand op2 width"
247  << eom;
248  throw 0;
249  }
250 
251  for(std::size_t i=0; i<sub_width; i++)
252  next_bv[offset+i]=op2_bv[i];
253 
254  break; // done
255  }
256 
257  offset+=sub_width;
258  }
259 }
260 
262  const union_typet &type,
263  const exprt &op2,
264  const bvt &prev_bv,
265  bvt &next_bv)
266 {
267  next_bv=prev_bv;
268 
269  const bvt &op2_bv=convert_bv(op2);
270 
271  if(next_bv.size()<op2_bv.size())
272  {
274  error() << "convert_with_union: unexpected operand op2 width" << eom;
275  throw 0;
276  }
277 
279  {
280  for(std::size_t i=0; i<op2_bv.size(); i++)
281  next_bv[i]=op2_bv[i];
282  }
283  else
284  {
285  assert(
287 
288  bv_endianness_mapt map_u(type, false, ns, boolbv_width);
289  bv_endianness_mapt map_op2(op2.type(), false, ns, boolbv_width);
290 
291  for(std::size_t i=0; i<op2_bv.size(); i++)
292  next_bv[map_u.map_bit(i)]=op2_bv[map_op2.map_bit(i)];
293  }
294 }
The type of an expression.
Definition: type.h:22
struct configt::ansi_ct ansi_c
virtual bvt convert_with(const exprt &expr)
Definition: boolbv_with.cpp:19
BigInt mp_integer
Definition: mp_arith.h:22
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:162
exprt & op0()
Definition: expr.h:72
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
void convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Definition: base_type.cpp:326
boolbv_widtht boolbv_width
Definition: boolbv.h:90
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:632
endiannesst endianness
Definition: config.h:76
std::vector< componentt > componentst
Definition: std_types.h:243
const componentst & components() const
Definition: std_types.h:245
typet & type()
Definition: expr.h:56
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Structure type.
Definition: std_types.h:297
configt config
Definition: config.cpp:23
equality
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:259
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
void convert_with_union(const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
const source_locationt & find_source_location() const
Definition: expr.cpp:246
source_locationt source_location
Definition: message.h:214
API to expression classes.
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:213
mstreamt & error() const
Definition: message.h:302
const exprt & size() const
Definition: std_types.h:1023
const namespacet & ns
const typet & follow(const typet &) const
Definition: namespace.cpp:55
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
Map bytes according to the configured endianness.
void convert_with_bv(const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
std::vector< exprt > operandst
Definition: expr.h:45
const source_locationt & source_location() const
Definition: type.h:97
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
unsigned integer2unsigned(const mp_integer &n)
Definition: mp_arith.cpp:203
API to type classes.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1054
Base class for all expressions.
Definition: expr.h:42
The union type.
Definition: std_types.h:458
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:476
arrays with given size
Definition: std_types.h:1013
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:17
size_t map_bit(size_t bit) const
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::size_t integer2size_t(const mp_integer &n)
Definition: mp_arith.cpp:195
Base Type Computation.
const typet & subtype() const
Definition: type.h:33
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