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 
10 #include "boolbv.h"
11 
13 {
14  std::size_t width=boolbv_width(expr.type());
15 
16  if(width==0)
17  return conversion_failed(expr);
18 
19  bvt bv;
20  bv.resize(width);
21 
22  const typet &expr_type=expr.type();
23 
24  if(expr_type.id()==ID_array)
25  {
26  std::size_t op_width=width/expr.operands().size();
27  std::size_t offset=0;
28 
29  forall_operands(it, expr)
30  {
31  const bvt &tmp=convert_bv(*it);
32 
33  if(tmp.size()!=op_width)
34  {
36  error() << "convert_constant: unexpected operand width" << eom;
37  throw 0;
38  }
39 
40  for(std::size_t j=0; j<op_width; j++)
41  bv[offset+j]=tmp[j];
42 
43  offset+=op_width;
44  }
45 
46  return bv;
47  }
48  else if(expr_type.id()==ID_string)
49  {
50  // we use the numbering for strings
51  std::size_t number=string_numbering(expr.get_value());
52  return bv_utils.build_constant(number, bv.size());
53  }
54  else if(expr_type.id()==ID_range)
55  {
56  mp_integer from=to_range_type(expr_type).get_from();
58  mp_integer v=value-from;
59 
60  std::string binary=integer2binary(v, width);
61 
62  for(std::size_t i=0; i<width; i++)
63  {
64  bool bit=(binary[binary.size()-i-1]=='1');
65  bv[i]=const_literal(bit);
66  }
67 
68  return bv;
69  }
70  else if(expr_type.id()==ID_unsignedbv ||
71  expr_type.id()==ID_signedbv ||
72  expr_type.id()==ID_bv ||
73  expr_type.id()==ID_fixedbv ||
74  expr_type.id()==ID_floatbv ||
75  expr_type.id()==ID_c_enum ||
76  expr_type.id()==ID_c_enum_tag ||
77  expr_type.id()==ID_c_bool ||
78  expr_type.id()==ID_c_bit_field ||
79  expr_type.id()==ID_incomplete_c_enum)
80  {
81  const std::string &binary=id2string(expr.get_value());
82 
83  if(binary.size()!=width)
84  {
86  error() << "wrong value length in constant: "
87  << expr.pretty() << eom;
88  throw 0;
89  }
90 
91  for(std::size_t i=0; i<width; i++)
92  {
93  bool bit=(binary[binary.size()-i-1]=='1');
94  bv[i]=const_literal(bit);
95  }
96 
97  return bv;
98  }
99  else if(expr_type.id()==ID_enumeration)
100  {
101  const irept::subt &elements=to_enumeration_type(expr_type).elements();
102  const irep_idt &value=expr.get_value();
103 
104  for(std::size_t i=0; i<elements.size(); i++)
105  if(elements[i].id()==value)
106  return bv_utils.build_constant(i, width);
107  }
108  else if(expr_type.id()==ID_verilog_signedbv ||
109  expr_type.id()==ID_verilog_unsignedbv)
110  {
111  const std::string &binary=id2string(expr.get_value());
112 
113  if(binary.size()*2!=width)
114  {
116  error() << "wrong value length in constant: "
117  << expr.pretty() << eom;
118  throw 0;
119  }
120 
121  for(std::size_t i=0; i<binary.size(); i++)
122  {
123  char bit=binary[binary.size()-i-1];
124 
125  switch(bit)
126  {
127  case '0':
128  bv[i*2]=const_literal(false);
129  bv[i*2+1]=const_literal(false);
130  break;
131 
132  case '1':
133  bv[i*2]=const_literal(true);
134  bv[i*2+1]=const_literal(false);
135  break;
136 
137  case 'x':
138  bv[i*2]=const_literal(false);
139  bv[i*2+1]=const_literal(true);
140  break;
141 
142  case 'z':
143  case '?':
144  bv[i*2]=const_literal(true);
145  bv[i*2+1]=const_literal(true);
146  break;
147 
148  default:
150  error() << "unknown character in Verilog constant:"
151  << expr.pretty() << eom;
152  throw 0;
153  }
154  }
155 
156  return bv;
157  }
158 
159  return conversion_failed(expr);
160 }
The type of an expression.
Definition: type.h:20
bv_utilst bv_utils
Definition: boolbv.h:93
BigInt mp_integer
Definition: mp_arith.h:19
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:53
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
std::vector< irept > subt
Definition: irep.h:91
boolbv_widtht boolbv_width
Definition: boolbv.h:90
const irep_idt & get_value() const
Definition: std_expr.h:3702
const range_typet & to_range_type(const typet &type)
Cast a generic typet to a range_typet.
Definition: std_types.h:1546
typet & type()
Definition: expr.h:60
A constant literal expression.
Definition: std_expr.h:3685
static mstreamt & eom(mstreamt &m)
Definition: message.h:193
virtual bvt convert_constant(const constant_exprt &expr)
const irep_idt & id() const
Definition: irep.h:189
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
const source_locationt & find_source_location() const
Definition: expr.cpp:466
source_locationt source_location
Definition: message.h:175
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
numbering< irep_idt > string_numbering
Definition: boolbv.h:254
#define forall_operands(it, expr)
Definition: expr.h:17
const irept::subt & elements() const
Definition: std_types.h:598
literalt const_literal(bool value)
Definition: literal.h:187
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:63
mstreamt & error()
Definition: message.h:223
operandst & operands()
Definition: expr.h:70
std::vector< literalt > bvt
Definition: literal.h:197
bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:15
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a generic typet to a enumeration_typet.
Definition: std_types.h:619
mp_integer get_from() const
Definition: std_types.cpp:127