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/arith_tools.h>
12 #include <util/c_types.h>
13 #include <util/std_expr.h>
14 
16 {
17  bvt bv = convert_bv(expr.old());
18 
19  std::size_t width=boolbv_width(expr.type());
20 
21  if(width==0)
22  {
23  // A zero-length array is acceptable:
24  if(expr.type().id()==ID_array && boolbv_width(expr.type().subtype())!=0)
25  return bvt();
26  else
27  return conversion_failed(expr);
28  }
29 
31  bv.size() == width,
32  "unexpected operand 0 width",
34 
35  bvt prev_bv;
36  prev_bv.resize(width);
37 
38  const exprt::operandst &ops=expr.operands();
39 
40  for(std::size_t op_no=1; op_no<ops.size(); op_no+=2)
41  {
42  bv.swap(prev_bv);
43 
44  convert_with(expr.old().type(), ops[op_no], ops[op_no + 1], prev_bv, bv);
45  }
46 
47  return bv;
48 }
49 
51  const typet &type,
52  const exprt &op1,
53  const exprt &op2,
54  const bvt &prev_bv,
55  bvt &next_bv)
56 {
57  // we only do that on arrays, bitvectors, structs, and unions
58 
59  next_bv.resize(prev_bv.size());
60 
61  if(type.id()==ID_array)
62  return convert_with_array(to_array_type(type), op1, op2, prev_bv, next_bv);
63  else if(type.id()==ID_bv ||
64  type.id()==ID_unsignedbv ||
65  type.id()==ID_signedbv)
66  return convert_with_bv(op1, op2, prev_bv, next_bv);
67  else if(type.id()==ID_struct)
68  return
69  convert_with_struct(to_struct_type(type), op1, op2, prev_bv, next_bv);
70  else if(type.id() == ID_struct_tag)
71  return convert_with(
72  ns.follow_tag(to_struct_tag_type(type)), op1, op2, prev_bv, next_bv);
73  else if(type.id()==ID_union)
74  return convert_with_union(to_union_type(type), op2, prev_bv, next_bv);
75  else if(type.id() == ID_union_tag)
76  return convert_with(
77  ns.follow_tag(to_union_tag_type(type)), op1, op2, prev_bv, next_bv);
78 
80  false, "unexpected with type", irep_pretty_diagnosticst{type});
81 }
82 
84  const array_typet &type,
85  const exprt &op1,
86  const exprt &op2,
87  const bvt &prev_bv,
88  bvt &next_bv)
89 {
90  // can't do this
92  !is_unbounded_array(type),
93  "convert_with_array called for unbounded array",
95 
96  const exprt &array_size=type.size();
97 
98  const auto size = numeric_cast<mp_integer>(array_size);
99 
101  size.has_value(),
102  "convert_with_array expects constant array size",
104 
105  const bvt &op2_bv=convert_bv(op2);
106 
108  *size * op2_bv.size() == prev_bv.size(),
109  "convert_with_array: unexpected operand 2 width",
111 
112  // Is the index a constant?
113  if(const auto op1_value = numeric_cast<mp_integer>(op1))
114  {
115  // Yes, it is!
116  next_bv=prev_bv;
117 
118  if(*op1_value >= 0 && *op1_value < *size) // bounds check
119  {
120  const std::size_t offset =
121  numeric_cast_v<std::size_t>(*op1_value * op2_bv.size());
122 
123  for(std::size_t j=0; j<op2_bv.size(); j++)
124  next_bv[offset+j]=op2_bv[j];
125  }
126 
127  return;
128  }
129 
130  typet counter_type=op1.type();
131 
132  for(mp_integer i=0; i<size; i=i+1)
133  {
134  exprt counter=from_integer(i, counter_type);
135 
136  literalt eq_lit=convert(equal_exprt(op1, counter));
137 
138  const std::size_t offset = numeric_cast_v<std::size_t>(i * op2_bv.size());
139 
140  for(std::size_t j=0; j<op2_bv.size(); j++)
141  next_bv[offset+j]=
142  prop.lselect(eq_lit, op2_bv[j], prev_bv[offset+j]);
143  }
144 }
145 
147  const exprt &op1,
148  const exprt &op2,
149  const bvt &prev_bv,
150  bvt &next_bv)
151 {
152  literalt l=convert(op2);
153 
154  if(const auto op1_value = numeric_cast<mp_integer>(op1))
155  {
156  next_bv=prev_bv;
157 
158  if(*op1_value < next_bv.size())
159  next_bv[numeric_cast_v<std::size_t>(*op1_value)] = l;
160 
161  return;
162  }
163 
164  typet counter_type=op1.type();
165 
166  for(std::size_t i=0; i<prev_bv.size(); i++)
167  {
168  exprt counter=from_integer(i, counter_type);
169 
170  literalt eq_lit=convert(equal_exprt(op1, counter));
171 
172  next_bv[i]=prop.lselect(eq_lit, l, prev_bv[i]);
173  }
174 }
175 
177  const struct_typet &type,
178  const exprt &op1,
179  const exprt &op2,
180  const bvt &prev_bv,
181  bvt &next_bv)
182 {
183  next_bv=prev_bv;
184 
185  const bvt &op2_bv=convert_bv(op2);
186 
187  const irep_idt &component_name=op1.get(ID_component_name);
188  const struct_typet::componentst &components=
189  type.components();
190 
191  std::size_t offset=0;
192 
193  for(const auto &c : components)
194  {
195  const typet &subtype = c.type();
196 
197  std::size_t sub_width=boolbv_width(subtype);
198 
199  if(c.get_name() == component_name)
200  {
202  subtype == op2.type(),
203  "with/struct: component '" + id2string(component_name) +
204  "' type does not match",
205  irep_pretty_diagnosticst{subtype},
207 
209  sub_width == op2_bv.size(),
210  "convert_with_struct: unexpected operand op2 width",
212 
213  for(std::size_t i=0; i<sub_width; i++)
214  next_bv[offset+i]=op2_bv[i];
215 
216  break; // done
217  }
218 
219  offset+=sub_width;
220  }
221 }
222 
224  const union_typet &type,
225  const exprt &op2,
226  const bvt &prev_bv,
227  bvt &next_bv)
228 {
229  next_bv=prev_bv;
230 
231  const bvt &op2_bv=convert_bv(op2);
232 
234  next_bv.size() >= op2_bv.size(),
235  "convert_with_union: unexpected operand op2 width",
237 
238  endianness_mapt map_u = endianness_map(type);
239  endianness_mapt map_op2 = endianness_map(op2.type());
240 
241  for(std::size_t i = 0; i < op2_bv.size(); i++)
242  next_bv[map_u.map_bit(i)] = op2_bv[map_op2.map_bit(i)];
243 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: c_types.h:189
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: c_types.h:149
Arrays with given size.
Definition: std_types.h:763
const exprt & size() const
Definition: std_types.h:771
const namespacet & ns
Definition: arrays.h:54
virtual bvt convert_with(const with_exprt &expr)
Definition: boolbv_with.cpp:15
void convert_with_bv(const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:543
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:40
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
void convert_with_union(const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition: boolbv.cpp:84
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
Definition: boolbv.h:103
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:97
void convert_with_array(const array_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
Definition: boolbv_with.cpp:83
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Maps a big-endian offset to a little-endian offset.
size_t map_bit(size_t bit) const
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const irep_idt & id() const
Definition: irep.h:407
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:45
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:63
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
virtual literalt lselect(literalt a, literalt b, literalt c)=0
Structure type, corresponds to C style structs.
Definition: std_types.h:231
const componentst & components() const
Definition: std_types.h:147
std::vector< componentt > componentst
Definition: std_types.h:140
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
The union type.
Definition: c_types.h:112
Operator to update elements in structs and arrays.
Definition: std_expr.h:2258
exprt & old()
Definition: std_expr.h:2268
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
std::vector< literalt > bvt
Definition: literal.h:201
BigInt mp_integer
Definition: smt_terms.h:12
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:511
API to expression classes.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:813
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:474