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/endianness_map.h>
16 #include <util/config.h>
17 
19 {
20  if(expr.operands().size()<3)
21  {
23  error() << "with takes at least three operands" << eom;
24  throw 0;
25  }
26 
27  if((expr.operands().size()%2)!=1)
28  {
30  error() << "with takes an odd number of operands" << eom;
31  throw 0;
32  }
33 
34  bvt bv=convert_bv(expr.op0());
35 
36  std::size_t width=boolbv_width(expr.type());
37 
38  if(width==0)
39  {
40  // A zero-length array is acceptable:
41  if(expr.type().id()==ID_array && boolbv_width(expr.type().subtype())!=0)
42  return bvt();
43  else
44  return conversion_failed(expr);
45  }
46 
47  if(bv.size()!=width)
48  {
50  error() << "unexpected operand 0 width" << eom;
51  throw 0;
52  }
53 
54  bvt prev_bv;
55  prev_bv.resize(width);
56 
57  const exprt::operandst &ops=expr.operands();
58 
59  for(std::size_t op_no=1; op_no<ops.size(); op_no+=2)
60  {
61  bv.swap(prev_bv);
62 
64  expr.op0().type(),
65  ops[op_no],
66  ops[op_no+1],
67  prev_bv,
68  bv);
69  }
70 
71  return bv;
72 }
73 
75  const typet &type,
76  const exprt &op1,
77  const exprt &op2,
78  const bvt &prev_bv,
79  bvt &next_bv)
80 {
81  // we only do that on arrays, bitvectors, structs, and unions
82 
83  next_bv.resize(prev_bv.size());
84 
85  if(type.id()==ID_array)
86  return convert_with_array(to_array_type(type), op1, op2, prev_bv, next_bv);
87  else if(type.id()==ID_bv ||
88  type.id()==ID_unsignedbv ||
89  type.id()==ID_signedbv)
90  return convert_with_bv(type, op1, op2, prev_bv, next_bv);
91  else if(type.id()==ID_struct)
92  return
93  convert_with_struct(to_struct_type(type), op1, op2, prev_bv, next_bv);
94  else if(type.id()==ID_union)
95  return convert_with_union(to_union_type(type), op1, op2, prev_bv, next_bv);
96  else if(type.id()==ID_symbol)
97  return convert_with(ns.follow(type), op1, op2, prev_bv, next_bv);
98 
100  error() << "unexpected with type: " << type.id();
101  throw 0;
102 }
103 
105  const array_typet &type,
106  const exprt &op1,
107  const exprt &op2,
108  const bvt &prev_bv,
109  bvt &next_bv)
110 {
111  if(is_unbounded_array(type))
112  {
113  // can't do this
115  error() << "convert_with_array called for unbounded array" << eom;
116  throw 0;
117  }
118 
119  const exprt &array_size=type.size();
120 
121  mp_integer size;
122 
123  if(to_integer(array_size, size))
124  {
126  error() << "convert_with_array expects constant array size" << eom;
127  throw 0;
128  }
129 
130  const bvt &op2_bv=convert_bv(op2);
131 
132  if(size*op2_bv.size()!=prev_bv.size())
133  {
135  error() << "convert_with_array: unexpected operand 2 width" << eom;
136  throw 0;
137  }
138 
139  // Is the index a constant?
140  mp_integer op1_value;
141  if(!to_integer(op1, op1_value))
142  {
143  // Yes, it is!
144  next_bv=prev_bv;
145 
146  if(op1_value>=0 && op1_value<size) // bounds check
147  {
148  std::size_t offset=integer2unsigned(op1_value*op2_bv.size());
149 
150  for(std::size_t j=0; j<op2_bv.size(); j++)
151  next_bv[offset+j]=op2_bv[j];
152  }
153 
154  return;
155  }
156 
157  typet counter_type=op1.type();
158 
159  for(mp_integer i=0; i<size; i=i+1)
160  {
161  exprt counter=from_integer(i, counter_type);
162 
163  literalt eq_lit=convert(equal_exprt(op1, counter));
164 
165  std::size_t offset=integer2unsigned(i*op2_bv.size());
166 
167  for(std::size_t j=0; j<op2_bv.size(); j++)
168  next_bv[offset+j]=
169  prop.lselect(eq_lit, op2_bv[j], prev_bv[offset+j]);
170  }
171 }
172 
174  const typet &type,
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 &op1,
264  const exprt &op2,
265  const bvt &prev_bv,
266  bvt &next_bv)
267 {
268  next_bv=prev_bv;
269 
270  const bvt &op2_bv=convert_bv(op2);
271 
272  if(next_bv.size()<op2_bv.size())
273  {
275  error() << "convert_with_union: unexpected operand op2 width" << eom;
276  throw 0;
277  }
278 
280  {
281  for(std::size_t i=0; i<op2_bv.size(); i++)
282  next_bv[i]=op2_bv[i];
283  }
284  else
285  {
286  assert(
288 
289  endianness_mapt map_u(type, false, ns);
290  endianness_mapt map_op2(op2.type(), false, ns);
291 
292  for(std::size_t i=0; i<op2_bv.size(); i++)
293  next_bv[map_u.map_bit(i)]=op2_bv[map_op2.map_bit(i)];
294  }
295 }
The type of an expression.
Definition: type.h:20
const typet & follow(const typet &src) const
Definition: namespace.cpp:66
struct configt::ansi_ct ansi_c
virtual bvt convert_with(const exprt &expr)
Definition: boolbv_with.cpp:18
BigInt mp_integer
Definition: mp_arith.h:19
Maps a big-endian offset to a little-endian offset.
virtual literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:175
exprt & op0()
Definition: expr.h:84
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:270
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
Definition: std_types.h:442
boolbv_widtht boolbv_width
Definition: boolbv.h:90
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:673
endiannesst endianness
Definition: config.h:75
std::vector< componentt > componentst
Definition: std_types.h:240
const componentst & components() const
Definition: std_types.h:242
typet & type()
Definition: expr.h:60
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
Structure type.
Definition: std_types.h:296
configt config
Definition: config.cpp:21
equality
Definition: std_expr.h:1082
const irep_idt & id() const
Definition: irep.h:189
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:946
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:115
const source_locationt & find_source_location() const
Definition: expr.cpp:466
source_locationt source_location
Definition: message.h:175
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
const exprt & size() const
Definition: std_types.h:915
const namespacet & ns
std::vector< exprt > operandst
Definition: expr.h:49
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:317
const source_locationt & source_location() const
Definition: type.h:95
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.
void convert_with_bv(const typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
Base class for all expressions.
Definition: expr.h:46
The union type.
Definition: std_types.h:424
mstreamt & error()
Definition: message.h:223
arrays with given size
Definition: std_types.h:901
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:18
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:31
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