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(type, 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), op1, 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 typet &type,
176  const exprt &op1,
177  const exprt &op2,
178  const bvt &prev_bv,
179  bvt &next_bv)
180 {
181  literalt l=convert(op2);
182 
183  mp_integer op1_value;
184  if(!to_integer(op1, op1_value))
185  {
186  next_bv=prev_bv;
187 
188  if(op1_value<next_bv.size())
189  next_bv[integer2size_t(op1_value)]=l;
190 
191  return;
192  }
193 
194  typet counter_type=op1.type();
195 
196  for(std::size_t i=0; i<prev_bv.size(); i++)
197  {
198  exprt counter=from_integer(i, counter_type);
199 
200  literalt eq_lit=convert(equal_exprt(op1, counter));
201 
202  next_bv[i]=prop.lselect(eq_lit, l, prev_bv[i]);
203  }
204 }
205 
207  const struct_typet &type,
208  const exprt &op1,
209  const exprt &op2,
210  const bvt &prev_bv,
211  bvt &next_bv)
212 {
213  next_bv=prev_bv;
214 
215  const bvt &op2_bv=convert_bv(op2);
216 
217  const irep_idt &component_name=op1.get(ID_component_name);
218  const struct_typet::componentst &components=
219  type.components();
220 
221  std::size_t offset=0;
222 
223  for(struct_typet::componentst::const_iterator
224  it=components.begin();
225  it!=components.end();
226  it++)
227  {
228  const typet &subtype=it->type();
229 
230  std::size_t sub_width=boolbv_width(subtype);
231 
232  if(it->get_name()==component_name)
233  {
234  if(!base_type_eq(subtype, op2.type(), ns))
235  {
237  error() << "with/struct: component `" << component_name
238  << "' type does not match: "
239  << subtype.pretty() << " vs. "
240  << op2.type().pretty() << eom;
241  throw 0;
242  }
243 
244  if(sub_width!=op2_bv.size())
245  {
247  error() << "convert_with_struct: unexpected operand op2 width"
248  << eom;
249  throw 0;
250  }
251 
252  for(std::size_t i=0; i<sub_width; i++)
253  next_bv[offset+i]=op2_bv[i];
254 
255  break; // done
256  }
257 
258  offset+=sub_width;
259  }
260 }
261 
263  const union_typet &type,
264  const exprt &op1,
265  const exprt &op2,
266  const bvt &prev_bv,
267  bvt &next_bv)
268 {
269  next_bv=prev_bv;
270 
271  const bvt &op2_bv=convert_bv(op2);
272 
273  if(next_bv.size()<op2_bv.size())
274  {
276  error() << "convert_with_union: unexpected operand op2 width" << eom;
277  throw 0;
278  }
279 
281  {
282  for(std::size_t i=0; i<op2_bv.size(); i++)
283  next_bv[i]=op2_bv[i];
284  }
285  else
286  {
287  assert(
289 
290  bv_endianness_mapt map_u(type, false, ns, boolbv_width);
291  bv_endianness_mapt map_op2(op2.type(), false, ns, boolbv_width);
292 
293  for(std::size_t i=0; i<op2_bv.size(); i++)
294  next_bv[map_u.map_bit(i)]=op2_bv[map_op2.map_bit(i)];
295  }
296 }
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:189
void convert_with_union(const union_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
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:1014
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
Map bytes according to the configured endianness.
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:202
API to type classes.
void convert_with_bv(const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
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:1004
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