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 
15 {
16  std::size_t width=boolbv_width(expr.type());
17 
18  if(width==0)
19  return conversion_failed(expr);
20 
21  const bvt &op_bv=convert_bv(expr.op());
22 
23  INVARIANT(
24  op_bv.size() <= width,
25  "operand bitvector width shall not be larger than the width indicated by "
26  "the union type");
27 
28  bvt bv;
29  bv.resize(width);
30 
32  {
33  for(std::size_t i=0; i<op_bv.size(); i++)
34  bv[i]=op_bv[i];
35 
36  // pad with nondets
37  for(std::size_t i=op_bv.size(); i<bv.size(); i++)
38  bv[i]=prop.new_variable();
39  }
40  else
41  {
42  INVARIANT(
44  "endianness should be set to either little endian or big endian");
45 
46  endianness_mapt map_u = endianness_map(expr.type(), false);
47  endianness_mapt map_op = endianness_map(expr.op().type(), false);
48 
49  for(std::size_t i=0; i<op_bv.size(); i++)
50  bv[map_u.map_bit(i)]=op_bv[map_op.map_bit(i)];
51 
52  // pad with nondets
53  for(std::size_t i=op_bv.size(); i<bv.size(); i++)
54  bv[map_u.map_bit(i)]=prop.new_variable();
55  }
56 
57  return bv;
58 }
arith_tools.h
bvt
std::vector< literalt > bvt
Definition: literal.h:201
union_exprt
Union constructor from single element.
Definition: std_expr.h:1517
propt::new_variable
virtual literalt new_variable()=0
boolbvt::convert_union
virtual bvt convert_union(const union_exprt &expr)
Definition: boolbv_union.cpp:14
configt::ansi_c
struct configt::ansi_ct ansi_c
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN
@ IS_LITTLE_ENDIAN
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:124
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:96
endianness_mapt::map_bit
size_t map_bit(size_t bit) const
Definition: endianness_map.h:47
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:294
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:38
config
configt config
Definition: config.cpp:24
configt::ansi_ct::endiannesst::IS_BIG_ENDIAN
@ IS_BIG_ENDIAN
endianness_mapt
Maps a big-endian offset to a little-endian offset.
Definition: endianness_map.h:31
config.h
boolbv.h
boolbvt::endianness_map
virtual endianness_mapt endianness_map(const typet &type, bool little_endian) const
Definition: boolbv.h:102
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
configt::ansi_ct::endianness
endiannesst endianness
Definition: config.h:157
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:128