CBMC
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  bvt bv;
18  bv.resize(width);
19 
20  const typet &expr_type=expr.type();
21 
22  if(expr_type.id() == ID_string)
23  {
24  // we use the numbering for strings
25  std::size_t number = string_numbering.number(expr.get_value());
26  return bv_utils.build_constant(number, bv.size());
27  }
28  else if(expr_type.id()==ID_range)
29  {
30  mp_integer from=to_range_type(expr_type).get_from();
32  mp_integer v=value-from;
33 
34  std::string binary=integer2binary(v, width);
35 
36  for(std::size_t i=0; i<width; i++)
37  {
38  bool bit=(binary[binary.size()-i-1]=='1');
39  bv[i]=const_literal(bit);
40  }
41 
42  return bv;
43  }
44  else if(
45  expr_type.id() == ID_unsignedbv || expr_type.id() == ID_signedbv ||
46  expr_type.id() == ID_bv || expr_type.id() == ID_fixedbv ||
47  expr_type.id() == ID_floatbv || expr_type.id() == ID_c_enum ||
48  expr_type.id() == ID_c_enum_tag || expr_type.id() == ID_c_bool ||
49  expr_type.id() == ID_c_bit_field)
50  {
51  const auto &value = expr.get_value();
52 
53  for(std::size_t i=0; i<width; i++)
54  {
55  const bool bit = get_bvrep_bit(value, width, i);
56  bv[i]=const_literal(bit);
57  }
58 
59  return bv;
60  }
61  else if(expr_type.id()==ID_enumeration)
62  {
63  const irept::subt &elements=to_enumeration_type(expr_type).elements();
64  const irep_idt &value=expr.get_value();
65 
66  for(std::size_t i=0; i<elements.size(); i++)
67  if(elements[i].id()==value)
68  return bv_utils.build_constant(i, width);
69  }
70  else if(expr_type.id()==ID_verilog_signedbv ||
71  expr_type.id()==ID_verilog_unsignedbv)
72  {
73  const std::string &binary=id2string(expr.get_value());
74 
76  binary.size() * 2 == width,
77  "wrong value length in constant",
79 
80  for(std::size_t i=0; i<binary.size(); i++)
81  {
82  char bit=binary[binary.size()-i-1];
83 
84  switch(bit)
85  {
86  case '0':
87  bv[i*2]=const_literal(false);
88  bv[i*2+1]=const_literal(false);
89  break;
90 
91  case '1':
92  bv[i*2]=const_literal(true);
93  bv[i*2+1]=const_literal(false);
94  break;
95 
96  case 'x':
97  bv[i*2]=const_literal(false);
98  bv[i*2+1]=const_literal(true);
99  break;
100 
101  case 'z':
102  case '?':
103  bv[i*2]=const_literal(true);
104  bv[i*2+1]=const_literal(true);
105  break;
106 
107  default:
109  false,
110  "unknown character in Verilog constant",
112  }
113  }
114 
115  return bv;
116  }
117 
118  return conversion_failed(expr);
119 }
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.
virtual bvt convert_constant(const constant_exprt &expr)
numberingt< irep_idt > string_numbering
Definition: boolbv.h:279
bv_utilst bv_utils
Definition: boolbv.h:116
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition: boolbv.cpp:83
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:101
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:14
A constant literal expression.
Definition: std_expr.h:2987
const irep_idt & get_value() const
Definition: std_expr.h:2995
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
const irept::subt & elements() const
Definition: std_types.h:540
typet & type()
Return the type of the expression.
Definition: expr.h:84
const irep_idt & id() const
Definition: irep.h:384
number_type number(const key_type &a)
Definition: numbering.h:37
mp_integer get_from() const
Definition: std_types.cpp:167
The type of an expression, extends irept.
Definition: type.h:29
const std::string & id2string(const irep_idt &d)
Definition: irep.h:40
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:187
std::vector< literalt > bvt
Definition: literal.h:201
literalt const_literal(bool value)
Definition: literal.h:188
const mp_integer string2integer(const std::string &n, unsigned base)
Definition: mp_arith.cpp:54
const std::string integer2binary(const mp_integer &n, std::size_t width)
Definition: mp_arith.cpp:64
BigInt mp_integer
Definition: smt_terms.h:17
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:535
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Definition: std_types.h:1028
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
Definition: std_types.h:568