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/config.h>
15 
16 #include "bv_endianness_map.h"
17 
19 {
20  bvt bv = convert_bv(expr.old());
21 
22  std::size_t width=boolbv_width(expr.type());
23 
24  if(width==0)
25  {
26  // A zero-length array is acceptable:
27  if(expr.type().id()==ID_array && boolbv_width(expr.type().subtype())!=0)
28  return bvt();
29  else
30  return conversion_failed(expr);
31  }
32 
34  bv.size() == width,
35  "unexpected operand 0 width",
37 
38  bvt prev_bv;
39  prev_bv.resize(width);
40 
41  const exprt::operandst &ops=expr.operands();
42 
43  for(std::size_t op_no=1; op_no<ops.size(); op_no+=2)
44  {
45  bv.swap(prev_bv);
46 
47  convert_with(expr.old().type(), ops[op_no], ops[op_no + 1], prev_bv, bv);
48  }
49 
50  return bv;
51 }
52 
54  const typet &type,
55  const exprt &op1,
56  const exprt &op2,
57  const bvt &prev_bv,
58  bvt &next_bv)
59 {
60  // we only do that on arrays, bitvectors, structs, and unions
61 
62  next_bv.resize(prev_bv.size());
63 
64  if(type.id()==ID_array)
65  return convert_with_array(to_array_type(type), op1, op2, prev_bv, next_bv);
66  else if(type.id()==ID_bv ||
67  type.id()==ID_unsignedbv ||
68  type.id()==ID_signedbv)
69  return convert_with_bv(op1, op2, prev_bv, next_bv);
70  else if(type.id()==ID_struct)
71  return
72  convert_with_struct(to_struct_type(type), op1, op2, prev_bv, next_bv);
73  else if(type.id() == ID_struct_tag)
74  return convert_with(
75  ns.follow_tag(to_struct_tag_type(type)), op1, op2, prev_bv, next_bv);
76  else if(type.id()==ID_union)
77  return convert_with_union(to_union_type(type), op2, prev_bv, next_bv);
78  else if(type.id() == ID_union_tag)
79  return convert_with(
80  ns.follow_tag(to_union_tag_type(type)), op1, op2, prev_bv, next_bv);
81 
83  false, "unexpected with type", irep_pretty_diagnosticst{type});
84 }
85 
87  const array_typet &type,
88  const exprt &op1,
89  const exprt &op2,
90  const bvt &prev_bv,
91  bvt &next_bv)
92 {
93  // can't do this
95  !is_unbounded_array(type),
96  "convert_with_array called for unbounded array",
98 
99  const exprt &array_size=type.size();
100 
101  const auto size = numeric_cast<mp_integer>(array_size);
102 
104  size.has_value(),
105  "convert_with_array expects constant array size",
107 
108  const bvt &op2_bv=convert_bv(op2);
109 
111  *size * op2_bv.size() == prev_bv.size(),
112  "convert_with_array: unexpected operand 2 width",
114 
115  // Is the index a constant?
116  if(const auto op1_value = numeric_cast<mp_integer>(op1))
117  {
118  // Yes, it is!
119  next_bv=prev_bv;
120 
121  if(*op1_value >= 0 && *op1_value < *size) // bounds check
122  {
123  const std::size_t offset =
124  numeric_cast_v<std::size_t>(*op1_value * op2_bv.size());
125 
126  for(std::size_t j=0; j<op2_bv.size(); j++)
127  next_bv[offset+j]=op2_bv[j];
128  }
129 
130  return;
131  }
132 
133  typet counter_type=op1.type();
134 
135  for(mp_integer i=0; i<size; i=i+1)
136  {
137  exprt counter=from_integer(i, counter_type);
138 
139  literalt eq_lit=convert(equal_exprt(op1, counter));
140 
141  const std::size_t offset = numeric_cast_v<std::size_t>(i * op2_bv.size());
142 
143  for(std::size_t j=0; j<op2_bv.size(); j++)
144  next_bv[offset+j]=
145  prop.lselect(eq_lit, op2_bv[j], prev_bv[offset+j]);
146  }
147 }
148 
150  const exprt &op1,
151  const exprt &op2,
152  const bvt &prev_bv,
153  bvt &next_bv)
154 {
155  literalt l=convert(op2);
156 
157  if(const auto op1_value = numeric_cast<mp_integer>(op1))
158  {
159  next_bv=prev_bv;
160 
161  if(*op1_value < next_bv.size())
162  next_bv[numeric_cast_v<std::size_t>(*op1_value)] = l;
163 
164  return;
165  }
166 
167  typet counter_type=op1.type();
168 
169  for(std::size_t i=0; i<prev_bv.size(); i++)
170  {
171  exprt counter=from_integer(i, counter_type);
172 
173  literalt eq_lit=convert(equal_exprt(op1, counter));
174 
175  next_bv[i]=prop.lselect(eq_lit, l, prev_bv[i]);
176  }
177 }
178 
180  const struct_typet &type,
181  const exprt &op1,
182  const exprt &op2,
183  const bvt &prev_bv,
184  bvt &next_bv)
185 {
186  next_bv=prev_bv;
187 
188  const bvt &op2_bv=convert_bv(op2);
189 
190  const irep_idt &component_name=op1.get(ID_component_name);
191  const struct_typet::componentst &components=
192  type.components();
193 
194  std::size_t offset=0;
195 
196  for(const auto &c : components)
197  {
198  const typet &subtype = c.type();
199 
200  std::size_t sub_width=boolbv_width(subtype);
201 
202  if(c.get_name() == component_name)
203  {
205  subtype == op2.type(),
206  "with/struct: component '" + id2string(component_name) +
207  "' type does not match",
208  irep_pretty_diagnosticst{subtype},
210 
212  sub_width == op2_bv.size(),
213  "convert_with_struct: unexpected operand op2 width",
215 
216  for(std::size_t i=0; i<sub_width; i++)
217  next_bv[offset+i]=op2_bv[i];
218 
219  break; // done
220  }
221 
222  offset+=sub_width;
223  }
224 }
225 
227  const union_typet &type,
228  const exprt &op2,
229  const bvt &prev_bv,
230  bvt &next_bv)
231 {
232  next_bv=prev_bv;
233 
234  const bvt &op2_bv=convert_bv(op2);
235 
237  next_bv.size() >= op2_bv.size(),
238  "convert_with_union: unexpected operand op2 width",
240 
242  {
243  for(std::size_t i=0; i<op2_bv.size(); i++)
244  next_bv[i]=op2_bv[i];
245  }
246  else
247  {
248  assert(
250 
251  bv_endianness_mapt map_u(type, false, ns, boolbv_width);
252  bv_endianness_mapt map_op2(op2.type(), false, ns, boolbv_width);
253 
254  for(std::size_t i=0; i<op2_bv.size(); i++)
255  next_bv[map_u.map_bit(i)]=op2_bv[map_op2.map_bit(i)];
256  }
257 }
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3050
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:142
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_union_tag_type
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Definition: std_types.h:555
boolbvt::convert_with_array
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:86
typet::subtype
const typet & subtype() const
Definition: type.h:47
arith_tools.h
bv_endianness_map.h
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:303
boolbvt::is_unbounded_array
bool is_unbounded_array(const typet &type) const override
Definition: boolbv.cpp:632
typet
The type of an expression, extends irept.
Definition: type.h:29
bvt
std::vector< literalt > bvt
Definition: literal.h:201
bv_endianness_mapt
Map bytes according to the configured endianness.
Definition: bv_endianness_map.h:21
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
boolbvt::convert_with_struct
void convert_with_struct(const struct_typet &type, const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
Definition: boolbv_with.cpp:179
exprt
Base class for all expressions.
Definition: expr.h:53
struct_union_typet::componentst
std::vector< componentt > componentst
Definition: std_types.h:135
namespace_baset::follow_tag
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
Definition: namespace.cpp:65
configt::ansi_c
struct configt::ansi_ct ansi_c
equal_exprt
Equality.
Definition: std_expr.h:1190
array_typet::size
const exprt & size() const
Definition: std_types.h:973
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
@ IS_LITTLE_ENDIAN
with_exprt::old
exprt & old()
Definition: std_expr.h:3060
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
DATA_INVARIANT_WITH_DIAGNOSTICS
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:512
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
arrayst::ns
const namespacet & ns
Definition: arrays.h:51
endianness_mapt::map_bit
size_t map_bit(size_t bit) const
Definition: endianness_map.h:48
std_types.h
Pre-defined types.
boolbvt::convert_with_union
void convert_with_union(const union_typet &type, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
Definition: boolbv_with.cpp:226
irept::id
const irep_idt & id() const
Definition: irep.h:418
to_struct_tag_type
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Definition: std_types.h:515
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
union_typet
The union type.
Definition: std_types.h:393
boolbvt::convert_bv
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:119
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:168
config
configt config
Definition: config.cpp:24
irep_pretty_diagnosticst
Definition: irep.h:524
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:226
array_typet
Arrays with given size.
Definition: std_types.h:965
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
@ IS_BIG_ENDIAN
irept::get
const irep_idt & get(const irep_namet &name) const
Definition: irep.cpp:51
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
boolbvt::convert_with_bv
void convert_with_bv(const exprt &op1, const exprt &op2, const bvt &prev_bv, bvt &next_bv)
Definition: boolbv_with.cpp:149
literalt
Definition: literal.h:26
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1011
config.h
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:95
to_union_type
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
Definition: std_types.h:422
std_expr.h
API to expression classes.
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:77
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131
boolbvt::convert_with
virtual bvt convert_with(const with_exprt &expr)
Definition: boolbv_with.cpp:18