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.op0().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:200
bv_endianness_mapt
Map bytes according to the configured endianness.
Definition: bv_endianness_map.h:20
union_exprt
Union constructor from single element.
Definition: std_expr.h:1840
propt::new_variable
virtual literalt new_variable()=0
exprt::op0
exprt & op0()
Definition: expr.h:84
configt::ansi_c
struct configt::ansi_ct ansi_c
boolbvt::convert_union
virtual bvt convert_union(const union_exprt &expr)
Definition: boolbv_union.cpp:16
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:92
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:110
decision_proceduret::ns
const namespacet & ns
Definition: decision_procedure.h:61
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
config
configt config
Definition: config.cpp:24
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
config.h
boolbv.h
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:76
validation_modet::INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152