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_struct_tag)
96  return convert_with(
97  ns.follow_tag(to_struct_tag_type(type)), op1, op2, prev_bv, next_bv);
98  else if(type.id()==ID_union)
99  return convert_with_union(to_union_type(type), op2, prev_bv, next_bv);
100  else if(type.id() == ID_union_tag)
101  return convert_with(
102  ns.follow_tag(to_union_tag_type(type)), op1, op2, prev_bv, next_bv);
103  else if(type.id() == ID_symbol_type)
104  return convert_with(ns.follow(type), op1, op2, prev_bv, next_bv);
105 
107  error() << "unexpected with type: " << type.id() << eom;
108  throw 0;
109 }
110 
112  const array_typet &type,
113  const exprt &op1,
114  const exprt &op2,
115  const bvt &prev_bv,
116  bvt &next_bv)
117 {
118  if(is_unbounded_array(type))
119  {
120  // can't do this
122  error() << "convert_with_array called for unbounded array" << eom;
123  throw 0;
124  }
125 
126  const exprt &array_size=type.size();
127 
128  const auto size = numeric_cast<mp_integer>(array_size);
129 
130  if(!size.has_value())
131  {
133  error() << "convert_with_array expects constant array size" << eom;
134  throw 0;
135  }
136 
137  const bvt &op2_bv=convert_bv(op2);
138 
139  if(*size * op2_bv.size() != prev_bv.size())
140  {
142  error() << "convert_with_array: unexpected operand 2 width" << eom;
143  throw 0;
144  }
145 
146  // Is the index a constant?
147  mp_integer op1_value;
148  if(!to_integer(op1, op1_value))
149  {
150  // Yes, it is!
151  next_bv=prev_bv;
152 
153  if(op1_value >= 0 && op1_value < *size) // bounds check
154  {
155  const std::size_t offset =
156  numeric_cast_v<std::size_t>(op1_value * op2_bv.size());
157 
158  for(std::size_t j=0; j<op2_bv.size(); j++)
159  next_bv[offset+j]=op2_bv[j];
160  }
161 
162  return;
163  }
164 
165  typet counter_type=op1.type();
166 
167  for(mp_integer i=0; i<size; i=i+1)
168  {
169  exprt counter=from_integer(i, counter_type);
170 
171  literalt eq_lit=convert(equal_exprt(op1, counter));
172 
173  const std::size_t offset = numeric_cast_v<std::size_t>(i * op2_bv.size());
174 
175  for(std::size_t j=0; j<op2_bv.size(); j++)
176  next_bv[offset+j]=
177  prop.lselect(eq_lit, op2_bv[j], prev_bv[offset+j]);
178  }
179 }
180 
182  const exprt &op1,
183  const exprt &op2,
184  const bvt &prev_bv,
185  bvt &next_bv)
186 {
187  literalt l=convert(op2);
188 
189  mp_integer op1_value;
190  if(!to_integer(op1, op1_value))
191  {
192  next_bv=prev_bv;
193 
194  if(op1_value<next_bv.size())
195  next_bv[numeric_cast_v<std::size_t>(op1_value)] = l;
196 
197  return;
198  }
199 
200  typet counter_type=op1.type();
201 
202  for(std::size_t i=0; i<prev_bv.size(); i++)
203  {
204  exprt counter=from_integer(i, counter_type);
205 
206  literalt eq_lit=convert(equal_exprt(op1, counter));
207 
208  next_bv[i]=prop.lselect(eq_lit, l, prev_bv[i]);
209  }
210 }
211 
213  const struct_typet &type,
214  const exprt &op1,
215  const exprt &op2,
216  const bvt &prev_bv,
217  bvt &next_bv)
218 {
219  next_bv=prev_bv;
220 
221  const bvt &op2_bv=convert_bv(op2);
222 
223  const irep_idt &component_name=op1.get(ID_component_name);
224  const struct_typet::componentst &components=
225  type.components();
226 
227  std::size_t offset=0;
228 
229  for(const auto &c : components)
230  {
231  const typet &subtype = c.type();
232 
233  std::size_t sub_width=boolbv_width(subtype);
234 
235  if(c.get_name() == component_name)
236  {
237  if(!base_type_eq(subtype, op2.type(), ns))
238  {
240  error() << "with/struct: component `" << component_name
241  << "' type does not match: "
242  << subtype.pretty() << " vs. "
243  << op2.type().pretty() << eom;
244  throw 0;
245  }
246 
247  if(sub_width!=op2_bv.size())
248  {
250  error() << "convert_with_struct: unexpected operand op2 width"
251  << eom;
252  throw 0;
253  }
254 
255  for(std::size_t i=0; i<sub_width; i++)
256  next_bv[offset+i]=op2_bv[i];
257 
258  break; // done
259  }
260 
261  offset+=sub_width;
262  }
263 }
264 
266  const union_typet &type,
267  const exprt &op2,
268  const bvt &prev_bv,
269  bvt &next_bv)
270 {
271  next_bv=prev_bv;
272 
273  const bvt &op2_bv=convert_bv(op2);
274 
275  if(next_bv.size()<op2_bv.size())
276  {
278  error() << "convert_with_union: unexpected operand op2 width" << eom;
279  throw 0;
280  }
281 
283  {
284  for(std::size_t i=0; i<op2_bv.size(); i++)
285  next_bv[i]=op2_bv[i];
286  }
287  else
288  {
289  assert(
291 
292  bv_endianness_mapt map_u(type, false, ns, boolbv_width);
293  bv_endianness_mapt map_op2(op2.type(), false, ns, boolbv_width);
294 
295  for(std::size_t i=0; i<op2_bv.size(); i++)
296  next_bv[map_u.map_bit(i)]=op2_bv[map_op2.map_bit(i)];
297  }
298 }
The type of an expression, extends irept.
Definition: type.h:27
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:157
exprt & op0()
Definition: expr.h:84
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
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)
Check types for equality across all levels of hierarchy.
Definition: base_type.cpp:332
boolbv_widtht boolbv_width
Definition: boolbv.h:92
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:624
endiannesst endianness
Definition: config.h:76
std::vector< componentt > componentst
Definition: std_types.h:203
const componentst & components() const
Definition: std_types.h:205
typet & type()
Return the type of the expression.
Definition: expr.h:68
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
Structure type, corresponds to C style structs.
Definition: std_types.h:276
configt config
Definition: config.cpp:24
const typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:90
Equality.
Definition: std_expr.h:1484
const irep_idt & id() const
Definition: irep.h:259
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
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:229
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:583
source_locationt source_location
Definition: message.h:236
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:123
API to expression classes.
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:110
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:212
mstreamt & error() const
Definition: message.h:386
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:543
const exprt & size() const
Definition: std_types.h:1010
const namespacet & ns
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
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:57
const source_locationt & source_location() const
Definition: type.h:62
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
static eomt eom
Definition: message.h:284
Pre-defined types.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
Base class for all expressions.
Definition: expr.h:54
The union type.
Definition: std_types.h:425
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:450
Arrays with given size.
Definition: std_types.h:1000
bool to_integer(const exprt &expr, mp_integer &int_value)
Definition: arith_tools.cpp:19
size_t map_bit(size_t bit) const
virtual literalt lselect(literalt a, literalt b, literalt c)=0
Base Type Computation.
const typet & subtype() const
Definition: type.h:38
operandst & operands()
Definition: expr.h:78
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
std::vector< literalt > bvt
Definition: literal.h:200