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 
34  if(tmp.size()!=op_width)
35  {
37  error() << "convert_constant: unexpected operand width" << eom;
38  throw 0;
39  }
40 
41  for(std::size_t j=0; j<op_width; j++)
42  bv[offset+j]=tmp[j];
43 
44  offset+=op_width;
45  }
46 
47  return bv;
48  }
49  else if(expr_type.id()==ID_string)
50  {
51  // we use the numbering for strings
52  std::size_t number = string_numbering.number(expr.get_value());
53  return bv_utils.build_constant(number, bv.size());
54  }
55  else if(expr_type.id()==ID_range)
56  {
57  mp_integer from=to_range_type(expr_type).get_from();
59  mp_integer v=value-from;
60 
61  std::string binary=integer2binary(v, width);
62 
63  for(std::size_t i=0; i<width; i++)
64  {
65  bool bit=(binary[binary.size()-i-1]=='1');
66  bv[i]=const_literal(bit);
67  }
68 
69  return bv;
70  }
71  else if(expr_type.id()==ID_unsignedbv ||
72  expr_type.id()==ID_signedbv ||
73  expr_type.id()==ID_bv ||
74  expr_type.id()==ID_fixedbv ||
75  expr_type.id()==ID_floatbv ||
76  expr_type.id()==ID_c_enum ||
77  expr_type.id()==ID_c_enum_tag ||
78  expr_type.id()==ID_c_bool ||
79  expr_type.id()==ID_c_bit_field ||
80  expr_type.id()==ID_incomplete_c_enum)
81  {
82  const auto &value = expr.get_value();
83 
84  for(std::size_t i=0; i<width; i++)
85  {
86  const bool bit = get_bvrep_bit(value, width, i);
87  bv[i]=const_literal(bit);
88  }
89 
90  return bv;
91  }
92  else if(expr_type.id()==ID_enumeration)
93  {
94  const irept::subt &elements=to_enumeration_type(expr_type).elements();
95  const irep_idt &value=expr.get_value();
96 
97  for(std::size_t i=0; i<elements.size(); i++)
98  if(elements[i].id()==value)
99  return bv_utils.build_constant(i, width);
100  }
101  else if(expr_type.id()==ID_verilog_signedbv ||
102  expr_type.id()==ID_verilog_unsignedbv)
103  {
104  const std::string &binary=id2string(expr.get_value());
105 
106  if(binary.size()*2!=width)
107  {
109  error() << "wrong value length in constant: "
110  << expr.pretty() << eom;
111  throw 0;
112  }
113 
114  for(std::size_t i=0; i<binary.size(); i++)
115  {
116  char bit=binary[binary.size()-i-1];
117 
118  switch(bit)
119  {
120  case '0':
121  bv[i*2]=const_literal(false);
122  bv[i*2+1]=const_literal(false);
123  break;
124 
125  case '1':
126  bv[i*2]=const_literal(true);
127  bv[i*2+1]=const_literal(false);
128  break;
129 
130  case 'x':
131  bv[i*2]=const_literal(false);
132  bv[i*2+1]=const_literal(true);
133  break;
134 
135  case 'z':
136  case '?':
137  bv[i*2]=const_literal(true);
138  bv[i*2+1]=const_literal(true);
139  break;
140 
141  default:
143  error() << "unknown character in Verilog constant:"
144  << expr.pretty() << eom;
145  throw 0;
146  }
147  }
148 
149  return bv;
150  }
151 
152  return conversion_failed(expr);
153 }
The type of an expression, extends irept.
Definition: type.h:27
bv_utilst bv_utils
Definition: boolbv.h:95
BigInt mp_integer
Definition: mp_arith.h:22
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:57
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:640
std::vector< irept > subt
Definition: irep.h:160
boolbv_widtht boolbv_width
Definition: boolbv.h:92
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.
const irep_idt & get_value() const
Definition: std_expr.h:4403
typet & type()
Return the type of the expression.
Definition: expr.h:68
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
A constant literal expression.
Definition: std_expr.h:4384
virtual bvt convert_constant(const constant_exprt &expr)
const irep_idt & id() const
Definition: irep.h:259
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
Definition: std_types.h:633
const source_locationt & find_source_location() const
Get a source_locationt from the expression or from its operands (non-recursively).
Definition: expr.cpp:229
source_locationt source_location
Definition: message.h:236
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:110
mstreamt & error() const
Definition: message.h:386
numbering< irep_idt > string_numbering
Definition: boolbv.h:256
#define forall_operands(it, expr)
Definition: expr.h:20
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:35
const irept::subt & elements() const
Definition: std_types.h:605
static eomt eom
Definition: message.h:284
literalt const_literal(bool value)
Definition: literal.h:187
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:224
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:67
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Definition: std_types.h:1734
operandst & operands()
Definition: expr.h:78
std::vector< literalt > bvt
Definition: literal.h:200
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
mp_integer get_from() const
Definition: std_types.cpp:155