cprover
boolbv_constant.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 <util/arith_tools.h>
10 
11 #include "boolbv.h"
12 
14 {
15  std::size_t width=boolbv_width(expr.type());
16 
17  if(width==0)
18  return conversion_failed(expr);
19 
20  bvt bv;
21  bv.resize(width);
22 
23  const typet &expr_type=expr.type();
24 
25  if(expr_type.id()==ID_array)
26  {
27  std::size_t op_width=width/expr.operands().size();
28  std::size_t offset=0;
29 
30  forall_operands(it, expr)
31  {
32  const bvt &tmp=convert_bv(*it);
33 
35  tmp.size() == op_width,
36  "convert_constant: unexpected operand width",
38 
39  for(std::size_t j=0; j<op_width; j++)
40  bv[offset+j]=tmp[j];
41 
42  offset+=op_width;
43  }
44 
45  return bv;
46  }
47  else if(expr_type.id()==ID_string)
48  {
49  // we use the numbering for strings
50  std::size_t number = string_numbering.number(expr.get_value());
51  return bv_utils.build_constant(number, bv.size());
52  }
53  else if(expr_type.id()==ID_range)
54  {
55  mp_integer from=to_range_type(expr_type).get_from();
57  mp_integer v=value-from;
58 
59  std::string binary=integer2binary(v, width);
60 
61  for(std::size_t i=0; i<width; i++)
62  {
63  bool bit=(binary[binary.size()-i-1]=='1');
64  bv[i]=const_literal(bit);
65  }
66 
67  return bv;
68  }
69  else if(
70  expr_type.id() == ID_unsignedbv || expr_type.id() == ID_signedbv ||
71  expr_type.id() == ID_bv || expr_type.id() == ID_fixedbv ||
72  expr_type.id() == ID_floatbv || expr_type.id() == ID_c_enum ||
73  expr_type.id() == ID_c_enum_tag || expr_type.id() == ID_c_bool ||
74  expr_type.id() == ID_c_bit_field)
75  {
76  const auto &value = expr.get_value();
77 
78  for(std::size_t i=0; i<width; i++)
79  {
80  const bool bit = get_bvrep_bit(value, width, i);
81  bv[i]=const_literal(bit);
82  }
83 
84  return bv;
85  }
86  else if(expr_type.id()==ID_enumeration)
87  {
88  const irept::subt &elements=to_enumeration_type(expr_type).elements();
89  const irep_idt &value=expr.get_value();
90 
91  for(std::size_t i=0; i<elements.size(); i++)
92  if(elements[i].id()==value)
93  return bv_utils.build_constant(i, width);
94  }
95  else if(expr_type.id()==ID_verilog_signedbv ||
96  expr_type.id()==ID_verilog_unsignedbv)
97  {
98  const std::string &binary=id2string(expr.get_value());
99 
101  binary.size() * 2 == width,
102  "wrong value length in constant",
104 
105  for(std::size_t i=0; i<binary.size(); i++)
106  {
107  char bit=binary[binary.size()-i-1];
108 
109  switch(bit)
110  {
111  case '0':
112  bv[i*2]=const_literal(false);
113  bv[i*2+1]=const_literal(false);
114  break;
115 
116  case '1':
117  bv[i*2]=const_literal(true);
118  bv[i*2+1]=const_literal(false);
119  break;
120 
121  case 'x':
122  bv[i*2]=const_literal(false);
123  bv[i*2+1]=const_literal(true);
124  break;
125 
126  case 'z':
127  case '?':
128  bv[i*2]=const_literal(true);
129  bv[i*2+1]=const_literal(true);
130  break;
131 
132  default:
134  false,
135  "unknown character in Verilog constant",
137  }
138  }
139 
140  return bv;
141  }
142 
143  return conversion_failed(expr);
144 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
to_enumeration_type
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
Definition: std_types.h:605
arith_tools.h
typet
The type of an expression, extends irept.
Definition: type.h:29
bvt
std::vector< literalt > bvt
Definition: literal.h:201
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
string2integer
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
boolbvt::convert_constant
virtual bvt convert_constant(const constant_exprt &expr)
Definition: boolbv_constant.cpp:13
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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
boolbvt::string_numbering
numbering< irep_idt > string_numbering
Definition: boolbv.h:265
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
range_typet::get_from
mp_integer get_from() const
Definition: std_types.cpp:156
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
irept::id
const irep_idt & id() const
Definition: irep.h:418
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
sharing_treet< irept, std::map< irep_namet, irept > >::subt
typename dt::subt subt
Definition: irep.h:182
to_range_type
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Definition: std_types.h:1726
irep_pretty_diagnosticst
Definition: irep.h:524
bv_utilst::build_constant
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
enumeration_typet::elements
const irept::subt & elements() const
Definition: std_types.h:577
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
binary
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:204
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:95
integer2binary
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
get_bvrep_bit
bool get_bvrep_bit(const irep_idt &src, std::size_t width, std::size_t bit_index)
Get a bit with given index from bit-vector representation.
Definition: arith_tools.cpp:261