cprover
boolbv_union.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/config.h>
13 
14 #include "bv_endianness_map.h"
15 
17 {
18  std::size_t width=boolbv_width(expr.type());
19 
20  if(width==0)
21  return conversion_failed(expr);
22 
23  const bvt &op_bv=convert_bv(expr.op());
24 
25  INVARIANT(
26  op_bv.size() <= width,
27  "operand bitvector width shall not be larger than the width indicated by "
28  "the union type");
29 
30  bvt bv;
31  bv.resize(width);
32 
34  {
35  for(std::size_t i=0; i<op_bv.size(); i++)
36  bv[i]=op_bv[i];
37 
38  // pad with nondets
39  for(std::size_t i=op_bv.size(); i<bv.size(); i++)
40  bv[i]=prop.new_variable();
41  }
42  else
43  {
44  INVARIANT(
46  "endianness should be set to either little endian or big endian");
47 
48  bv_endianness_mapt map_u(expr.type(), false, ns, boolbv_width);
49  bv_endianness_mapt map_op(expr.op().type(), false, ns, boolbv_width);
50 
51  for(std::size_t i=0; i<op_bv.size(); i++)
52  bv[map_u.map_bit(i)]=op_bv[map_op.map_bit(i)];
53 
54  // pad with nondets
55  for(std::size_t i=op_bv.size(); i<bv.size(); i++)
56  bv[map_u.map_bit(i)]=prop.new_variable();
57  }
58 
59  return bv;
60 }
arith_tools.h
bv_endianness_map.h
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
union_exprt
Union constructor from single element.
Definition: std_expr.h:1567
propt::new_variable
virtual literalt new_variable()=0
boolbvt::convert_union
virtual bvt convert_union(const union_exprt &expr)
Definition: boolbv_union.cpp:16
configt::ansi_c
struct configt::ansi_ct ansi_c
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
@ IS_LITTLE_ENDIAN
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
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
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
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
config
configt config
Definition: config.cpp:24
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
@ IS_BIG_ENDIAN
config.h
boolbv.h
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:77
validation_modet::INVARIANT
@ INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131