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