cprover
boolbv_constant.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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}
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 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:40
virtual bvt convert_constant(const constant_exprt &expr)
numberingt< irep_idt > string_numbering
Definition: boolbv.h:278
bv_utilst bv_utils
Definition: boolbv.h:114
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:84
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:99
static bvt build_constant(const mp_integer &i, std::size_t width)
Definition: bv_utils.cpp:11
A constant literal expression.
Definition: std_expr.h:2807
const irep_idt & get_value() const
Definition: std_expr.h:2815
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
const irept::subt & elements() const
Definition: std_types.h:496
typet & type()
Return the type of the expression.
Definition: expr.h:82
operandst & operands()
Definition: expr.h:92
const irep_idt & id() const
Definition: irep.h:396
number_type number(const key_type &a)
Definition: numbering.h:37
mp_integer get_from() const
Definition: std_types.cpp:160
The type of an expression, extends irept.
Definition: type.h:29
#define forall_operands(it, expr)
Definition: expr.h:18
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
static std::string binary(const constant_exprt &src)
Definition: json_expr.cpp:206
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:12
#define DATA_INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Definition: invariant.h:511
const range_typet & to_range_type(const typet &type)
Cast a typet to a range_typet.
Definition: std_types.h:972
const enumeration_typet & to_enumeration_type(const typet &type)
Cast a typet to a enumeration_typet.
Definition: std_types.h:524