29 #include "../floatbv/float_utils.h" 33 const std::size_t bit,
36 if(expr.
type().
id()==ID_bool)
43 if(expr.
id()==ID_symbol ||
44 expr.
id()==ID_nondet_symbol)
48 boolbv_mapt::mappingt::const_iterator it_m=
63 else if(expr.
id()==ID_index)
70 throw "literal expects a bit-vector type";
74 throw "literal expects constant index";
80 else if(expr.
id()==ID_member)
90 for(struct_typet::componentst::const_iterator
91 it=components.begin();
95 const typet &subtype=it->type();
97 if(it->get_name()==component_name)
103 throw "literal expects a bit-vector type";
105 offset+=element_width;
108 throw "failed to find component";
112 throw "found no literal for expression";
118 std::pair<bv_cachet::iterator, bool> cache_result=
120 if(!cache_result.second)
122 return cache_result.first->second;
142 return cache_result.first->second;
156 if(expr.
type().
id()==ID_bool)
164 if(expr.
id()==ID_index)
166 else if(expr.
id()==ID_constraint_select_one)
168 else if(expr.
id()==ID_member)
170 else if(expr.
id()==ID_with)
172 else if(expr.
id()==ID_update)
174 else if(expr.
id()==ID_width)
189 if(expr.
type().
id()==ID_unsignedbv ||
190 expr.
type().
id()==ID_signedbv)
193 else if(expr.
id()==ID_case)
195 else if(expr.
id()==ID_cond)
197 else if(expr.
id()==ID_if)
199 else if(expr.
id()==ID_constant)
201 else if(expr.
id()==ID_typecast)
203 else if(expr.
id()==ID_symbol)
205 else if(expr.
id()==ID_bv_literals)
207 else if(expr.
id()==ID_plus || expr.
id()==ID_minus ||
208 expr.
id()==
"no-overflow-plus" ||
209 expr.
id()==
"no-overflow-minus")
211 else if(expr.
id()==ID_mult ||
212 expr.
id()==
"no-overflow-mult")
214 else if(expr.
id()==ID_div)
216 else if(expr.
id()==ID_mod)
218 else if(expr.
id()==ID_shl || expr.
id()==ID_ashr || expr.
id()==ID_lshr)
220 else if(expr.
id()==ID_floatbv_plus || expr.
id()==ID_floatbv_minus ||
221 expr.
id()==ID_floatbv_mult || expr.
id()==ID_floatbv_div ||
222 expr.
id()==ID_floatbv_rem)
224 else if(expr.
id()==ID_floatbv_typecast)
226 else if(expr.
id()==ID_concatenation)
228 else if(expr.
id()==ID_replication)
230 else if(expr.
id()==ID_extractbits)
232 else if(expr.
id()==ID_bitnot || expr.
id()==ID_bitand ||
233 expr.
id()==ID_bitor || expr.
id()==ID_bitxor ||
234 expr.
id()==ID_bitxnor || expr.
id()==ID_bitnor ||
235 expr.
id()==ID_bitnand)
237 else if(expr.
id()==ID_unary_minus ||
238 expr.
id()==
"no-overflow-unary-minus")
240 else if(expr.
id()==ID_unary_plus)
245 else if(expr.
id()==ID_abs)
247 else if(expr.
id()==ID_byte_extract_little_endian ||
248 expr.
id()==ID_byte_extract_big_endian)
250 else if(expr.
id()==ID_byte_update_little_endian ||
251 expr.
id()==ID_byte_update_big_endian)
253 else if(expr.
id()==ID_nondet_symbol ||
254 expr.
id()==
"quant_symbol")
256 else if(expr.
id()==ID_struct)
258 else if(expr.
id()==ID_union)
260 else if(expr.
id()==ID_string_constant)
263 else if(expr.
id()==ID_array)
265 else if(expr.
id()==ID_vector)
267 else if(expr.
id()==ID_complex)
269 else if(expr.
id()==ID_complex_real)
271 else if(expr.
id()==ID_complex_imag)
273 else if(expr.
id()==ID_lambda)
275 else if(expr.
id()==ID_array_of)
277 else if(expr.
id()==ID_let)
282 else if(expr.
id()==ID_function_application)
286 else if(expr.
id()==ID_reduction_or || expr.
id()==ID_reduction_and ||
287 expr.
id()==ID_reduction_nor || expr.
id()==ID_reduction_nand ||
288 expr.
id()==ID_reduction_xor || expr.
id()==ID_reduction_xnor)
290 else if(expr.
id()==ID_not)
292 else if(expr.
id()==ID_power)
294 else if(expr.
id()==ID_float_debug1 ||
295 expr.
id()==ID_float_debug2)
301 bvt bv=expr.
id()==ID_float_debug1?
302 float_utils.debug1(bv0, bv1):
303 float_utils.debug2(bv0, bv1);
318 throw "lambda takes two operands";
320 if(expr.
type().
id()!=ID_array)
323 const exprt &array_size=
347 if(size*tmp.size()!=width)
348 throw "convert_lambda: unexpected operand width";
350 for(std::size_t j=0; j<tmp.size(); j++)
369 if(bv_sub.size()!=width)
370 throw "bv_literals with wrong size";
372 for(std::size_t i=0; i<width; i++)
386 const irep_idt &identifier=expr.
get(ID_identifier);
388 if(identifier.
empty())
389 throw "convert_symbol got empty identifier";
426 if(expr.
type().
id()!=ID_bool)
428 error() <<
"boolbvt::convert_rest got non-boolean operand: " 435 if(expr.
id()==ID_typecast)
437 else if(expr.
id()==ID_equal)
439 else if(expr.
id()==ID_verilog_case_equality ||
440 expr.
id()==ID_verilog_case_inequality)
442 else if(expr.
id()==ID_notequal)
445 throw "notequal expects two operands";
449 else if(expr.
id()==ID_ieee_float_equal ||
450 expr.
id()==ID_ieee_float_notequal)
452 else if(expr.
id()==ID_le || expr.
id()==ID_ge ||
453 expr.
id()==ID_lt || expr.
id()==ID_gt)
455 else if(expr.
id()==ID_extractbit)
457 else if(expr.
id()==ID_forall)
459 else if(expr.
id()==ID_exists)
461 else if(expr.
id()==ID_index)
466 throw "convert_index returned non-bool bitvector";
470 else if(expr.
id()==ID_member)
475 throw "convert_member returned non-bool bitvector";
479 else if(expr.
id()==ID_case)
484 throw "convert_case returned non-bool bitvector";
488 else if(expr.
id()==ID_cond)
493 throw "convert_cond returned non-bool bitvector";
497 else if(expr.
id()==ID_sign)
500 throw "sign expects one operand";
505 throw "sign operator takes one non-empty operand";
507 if(operands[0].type().id()==ID_signedbv)
508 return bv[bv.size()-1];
509 else if(operands[0].type().
id()==ID_unsignedbv)
511 else if(operands[0].type().
id()==ID_fixedbv)
512 return bv[bv.size()-1];
513 else if(operands[0].type().
id()==ID_floatbv)
514 return bv[bv.size()-1];
516 else if(expr.
id()==ID_reduction_or || expr.
id()==ID_reduction_and ||
517 expr.
id()==ID_reduction_nor || expr.
id()==ID_reduction_nand ||
518 expr.
id()==ID_reduction_xor || expr.
id()==ID_reduction_xnor)
520 else if(expr.
id()==ID_onehot || expr.
id()==ID_onehot0)
524 else if(expr.
id()==ID_isnan)
527 throw "isnan expects one operand";
534 return float_utils.
is_NaN(bv);
536 else if(expr.
op0().
type().
id()==ID_fixedbv)
539 else if(expr.
id()==ID_isfinite)
542 throw "isfinite expects one operand";
553 else if(expr.
op0().
type().
id()==ID_fixedbv)
556 else if(expr.
id()==ID_isinf)
559 throw "isinf expects one operand";
568 else if(expr.
op0().
type().
id()==ID_fixedbv)
571 else if(expr.
id()==ID_isnormal)
574 throw "isnormal expects one operand";
583 else if(expr.
op0().
type().
id()==ID_fixedbv)
597 if(expr.
lhs().
id()==ID_symbol &&
623 if(expr.
type().
id()!=ID_bool)
625 error() <<
"boolbvt::set_to got non-boolean operand: " 632 if(expr.
id()==ID_equal)
644 dest=
exprt(ID_bv_literals, type);
647 bv_sub.resize(bv.size());
649 for(std::size_t i=0; i<bv.size(); i++)
650 bv_sub[i].
id(std::to_string(bv[i].
get()));
675 if(type.
id()==ID_symbol)
678 if(type.
id()!=ID_array)
699 for(boolbv_mapt::mappingt::const_iterator it=
map.
mapping.begin();
703 out << it->first <<
"=" 704 << it->second.get_value(
prop) <<
'\n';
713 dest.resize(components.size());
714 std::size_t offset=0;
715 for(std::size_t i=0; i<components.size(); i++)
717 std::size_t comp_width=
boolbv_width(components[i].type());
virtual bvt convert_case(const exprt &expr)
virtual bvt convert_complex_real(const exprt &expr)
map_entryt & get_map_entry(const irep_idt &identifier, const typet &type)
The type of an expression.
void print_assignment(std::ostream &out) const override
std::vector< std::size_t > offset_mapt
virtual bvt convert_floatbv_typecast(const floatbv_typecast_exprt &expr)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const typet & follow(const typet &src) const
virtual bvt convert_with(const exprt &expr)
virtual bvt convert_concatenation(const exprt &expr)
const function_application_exprt & to_function_application_expr(const exprt &expr)
Cast a generic exprt to a function_application_exprt.
virtual bvt convert_abs(const exprt &expr)
virtual literalt convert_ieee_float_rel(const exprt &expr)
virtual bvt convert_array_of(const array_of_exprt &expr)
const extractbits_exprt & to_extractbits_expr(const exprt &expr)
Cast a generic exprt to an extractbits_exprt.
virtual bvt convert_bv_reduction(const unary_exprt &expr)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast a generic exprt to an array_of_exprt.
const std::string & id2string(const irep_idt &d)
application of (mathematical) function
virtual literalt convert(const exprt &expr) override
virtual void set_frozen(literalt a)
bool equality_propagation
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
std::vector< irept > subt
virtual literalt convert_onehot(const unary_exprt &expr)
virtual bvt convert_shift(const binary_exprt &expr)
virtual literalt convert_overflow(const exprt &expr)
bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
virtual literalt convert_equality(const equal_exprt &expr)
bool is_unbounded_array(const typet &type) const override
virtual bvt convert_replication(const replication_exprt &expr)
static var_not unused_var_no()
virtual bvt convert_bv_literals(const exprt &expr)
std::vector< componentt > componentst
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
virtual bvt convert_struct(const struct_exprt &expr)
const componentst & components() const
virtual bvt convert_function_application(const function_application_exprt &expr)
const struct_exprt & to_struct_expr(const exprt &expr)
Cast a generic exprt to a struct_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
virtual bvt convert_lambda(const exprt &expr)
virtual void set_frozen(literalt a) override
void build_offset_map(const struct_typet &src, offset_mapt &dest)
static mstreamt & eom(mstreamt &m)
virtual void set_to(const exprt &expr, bool value) override
virtual bool literal(const exprt &expr, literalt &literal) const
virtual bvt convert_constant(const constant_exprt &expr)
#define forall_literals(it, bv)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
const extractbit_exprt & to_extractbit_expr(const exprt &expr)
Cast a generic exprt to an extractbit_exprt.
virtual bvt convert_symbol(const exprt &expr)
virtual bvt convert_mult(const exprt &expr)
Extract member of struct or union.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
virtual bvt convert_complex(const exprt &expr)
virtual literalt convert_quantifier(const exprt &expr)
virtual bvt convert_update(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
literalt is_normal(const bvt &)
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
virtual literalt new_variable()=0
virtual literalt convert_bv_rel(const exprt &expr)
#define Forall_literals(it, bv)
virtual bvt convert_add_sub(const exprt &expr)
virtual literalt convert_reduction(const unary_exprt &expr)
virtual const bvt & convert_bv(const exprt &expr)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
virtual size_t no_variables() const =0
virtual void make_free_bv_expr(const typet &type, exprt &dest)
void set_literals(const irep_idt &identifier, const typet &type, const bvt &literals)
virtual bvt convert_bitvector(const exprt &expr)
API to expression classes.
virtual bvt convert_floatbv_op(const exprt &expr)
void conversion_failed(const exprt &expr, bvt &bv)
const irep_idt & get(const irep_namet &name) const
virtual bool boolbv_set_equality_to_true(const equal_exprt &expr)
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
const exprt & size() const
const mod_exprt & to_mod_expr(const exprt &expr)
Cast a generic exprt to a mod_exprt.
virtual bvt convert_union(const union_exprt &expr)
array_exprt to_array_expr() const
convert string into array constant
const union_exprt & to_union_expr(const exprt &expr)
Cast a generic exprt to a union_exprt.
virtual bvt convert_extractbits(const extractbits_exprt &expr)
virtual literalt convert_rest(const exprt &expr) override
virtual bvt convert_complex_imag(const exprt &expr)
const binary_exprt & to_binary_expr(const exprt &expr)
Cast a generic exprt to a binary_exprt.
virtual bvt convert_cond(const exprt &expr)
std::vector< exprt > operandst
bool has_prefix(const std::string &s, const std::string &prefix)
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
virtual bvt convert_not(const not_exprt &expr)
const not_exprt & to_not_expr(const exprt &expr)
Cast a generic exprt to an not_exprt.
literalt is_infinity(const bvt &)
unsigned integer2unsigned(const mp_integer &n)
virtual bvt convert_byte_update(const byte_update_exprt &expr)
virtual bvt convert_bv_typecast(const typecast_exprt &expr)
literalt const_literal(bool value)
literalt is_NaN(const bvt &)
virtual bvt convert_constraint_select_one(const exprt &expr)
const floatbv_typecast_exprt & to_floatbv_typecast_expr(const exprt &expr)
Cast a generic exprt to a floatbv_typecast_exprt.
void record(const function_application_exprt &function_application)
const div_exprt & to_div_expr(const exprt &expr)
Cast a generic exprt to a div_exprt.
unbounded_arrayt unbounded_array
virtual bvt convert_vector(const exprt &expr)
const string_constantt & to_string_constant(const exprt &expr)
virtual bvt convert_array(const exprt &expr)
virtual void make_bv_expr(const typet &type, const bvt &bv, exprt &dest)
Base class for all expressions.
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
virtual bvt convert_mod(const mod_exprt &expr)
irep_idt get_component_name() const
irept & add(const irep_namet &name)
virtual bvt convert_member(const member_exprt &expr)
virtual bvt convert_if(const if_exprt &expr)
virtual literalt convert_rest(const exprt &expr)
const std::string & id_string() const
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast a generic exprt to a binary_relation_exprt.
const replication_exprt & to_replication_expr(const exprt &expr)
Cast a generic exprt to a replication_exprt.
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
virtual bvt convert_unary_minus(const unary_exprt &expr)
virtual literalt convert_verilog_case_equality(const binary_relation_exprt &expr)
virtual bvt convert_div(const div_exprt &expr)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
void set_to(const exprt &expr, bool value) override
virtual literalt convert_extractbit(const extractbit_exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
virtual void ignoring(const exprt &expr)
int unsafe_string2int(const std::string &str, int base)
const irept & find(const irep_namet &name) const
std::vector< literalt > bvt
bvt build_constant(const mp_integer &i, std::size_t width)
virtual literalt convert_typecast(const typecast_exprt &expr)
conversion from bitvector types to boolean
virtual bvt convert_bitwise(const exprt &expr)
virtual bvt convert_power(const binary_exprt &expr)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast a generic exprt to a unary_exprt.