21 if(expr.
type().
id()!=ID_bool)
22 throw "bv_pointerst::convert_rest got non-boolean operand";
26 if(expr.
id()==ID_invalid_pointer)
28 if(operands.size()==1 &&
29 is_ptr(operands[0].type()))
35 bvt invalid_bv, null_bv;
39 bvt equal_invalid_bv, equal_null_bv;
54 return prop.
lor(equal_invalid, equal_null);
58 else if(expr.
id()==ID_dynamic_object)
60 if(operands.size()==1 &&
61 is_ptr(operands[0].type()))
74 else if(expr.
id()==ID_lt || expr.
id()==ID_le ||
75 expr.
id()==ID_gt || expr.
id()==ID_ge)
77 if(operands.size()==2 &&
78 is_ptr(operands[0].type()) &&
79 is_ptr(operands[1].type()))
107 if(expr.
id()==ID_symbol)
112 else if(expr.
id()==ID_label)
117 else if(expr.
id()==
"NULL-object")
122 else if(expr.
id()==ID_index)
125 throw "index takes two operands";
133 if(array_type.
id()==ID_pointer)
137 assert(bv.size()==
bits);
139 else if(array_type.
id()==ID_array ||
140 array_type.
id()==ID_incomplete_array ||
141 array_type.
id()==ID_string_constant)
145 assert(bv.size()==
bits);
156 assert(bv.size()==
bits);
159 else if(expr.
id()==ID_member)
162 const exprt &struct_op=member_expr.
op0();
169 if(struct_op_type.
id()==ID_struct)
179 else if(struct_op_type.
id()==ID_union)
184 throw "member takes struct or union operand";
188 else if(expr.
id()==ID_constant ||
189 expr.
id()==ID_string_constant ||
195 else if(expr.
id()==ID_if)
220 throw "convert_pointer_type got non-pointer type";
225 if(expr.
id()==ID_symbol)
237 else if(expr.
id()==ID_nondet_symbol)
247 else if(expr.
id()==ID_typecast)
250 throw "typecast takes one operand";
255 if(op_type.
id()==ID_pointer)
257 else if(op_type.
id()==ID_signedbv ||
258 op_type.
id()==ID_unsignedbv ||
259 op_type.
id()==ID_bool ||
260 op_type.
id()==ID_c_enum ||
261 op_type.
id()==ID_c_enum_tag)
271 else if(expr.
id()==ID_if)
275 else if(expr.
id()==ID_index)
279 else if(expr.
id()==ID_member)
283 else if(expr.
id()==ID_address_of)
286 throw expr.
id_string()+
" takes one operand";
297 assert(bv.size()==
bits);
300 else if(expr.
id()==ID_constant)
317 else if(expr.
id()==ID_plus)
322 throw "operator + takes at least two operands";
331 if(it->type().id()==ID_pointer)
335 assert(bv.size()==
bits);
338 if(pointer_sub_type.id()==ID_empty)
346 throw "found no pointer in pointer-type sum";
348 throw "found more than one pointer in sum";
354 if(it->type().id()==ID_pointer)
357 if(it->type().id()!=ID_unsignedbv &&
358 it->type().id()!=ID_signedbv)
372 throw "unexpected pointer arithmetic operand width";
378 else if(op.size()<
bits)
388 else if(expr.
id()==ID_minus)
393 throw "operator "+expr.
id_string()+
" takes two operands";
396 throw "found no pointer in pointer type in difference";
400 if(expr.
op1().
type().
id()!=ID_unsignedbv &&
409 ID_unary_minus, expr.
op1(), expr.
op1().
type());
415 assert(element_size>0);
421 else if(expr.
id()==ID_lshr ||
426 else if(expr.
id()==ID_bitand ||
427 expr.
id()==ID_bitor ||
428 expr.
id()==ID_bitnot)
432 else if(expr.
id()==ID_concatenation)
436 else if(expr.
id()==ID_byte_extract_little_endian ||
437 expr.
id()==ID_byte_extract_big_endian)
450 if(expr.
id()==ID_minus &&
472 assert(element_size>0);
484 else if(expr.
id()==ID_pointer_offset &&
501 else if(expr.
id()==ID_object_size &&
511 for(std::size_t i=0; i<width; i++)
522 else if(expr.
id()==ID_pointer_object &&
539 else if(expr.
id()==ID_typecast &&
561 const std::vector<bool> &unknown,
563 const typet &type)
const 568 std::string value_addr, value_offset, value;
570 for(std::size_t i=0; i<
bits; i++)
573 std::size_t bit_nr=i+offset;
584 default: assert(
false);
591 value_offset=ch+value_offset;
593 value_addr=ch+value_addr;
623 bv[offset_bits+i]=
const_literal((addr&(std::size_t(1)<<i))!=0);
685 throw "too many variables";
693 if(postponed.
expr.
id()==ID_dynamic_object)
698 std::size_t number=0;
700 for(pointer_logict::objectst::const_iterator
705 const exprt &expr=*it;
715 bvt saved_bv=postponed.
op;
716 saved_bv.erase(saved_bv.begin(), saved_bv.begin()+
offset_bits);
718 assert(bv.size()==saved_bv.size());
719 assert(postponed.
bv.size()==1);
730 else if(postponed.
expr.
id()==ID_object_size)
735 std::size_t number=0;
737 for(pointer_logict::objectst::const_iterator
742 const exprt &expr=*it;
746 if(expr.
id()==ID_symbol)
768 bvt saved_bv=postponed.
op;
769 saved_bv.erase(saved_bv.begin(), saved_bv.begin()+
offset_bits);
771 assert(bv.size()==saved_bv.size());
772 assert(postponed.
bv.size()>=1);
791 for(postponed_listt::const_iterator
The type of an expression.
exprt size_of_expr(const typet &type, const namespacet &ns)
std::size_t get_null_object() const
const typet & follow(const typet &src) const
struct configt::ansi_ct ansi_c
virtual bvt convert_concatenation(const exprt &expr)
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
const std::string & id2string(const irep_idt &d)
virtual literalt convert(const exprt &expr) override
const mp_integer string2integer(const std::string &n, unsigned base)
virtual bvt convert_shift(const binary_exprt &expr)
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
literalt convert_rest(const exprt &expr) override
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
boolbv_widtht boolbv_width
void copy_to_operands(const exprt &expr)
const irep_idt & get_identifier() const
bvt convert_bitvector(const exprt &expr) override
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
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.
const irep_idt & get_value() const
static bool is_ptr(const typet &type)
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
virtual literalt lor(literalt a, literalt b)=0
The trinary if-then-else operator.
bvt sub(const bvt &op0, const bvt &op1)
A constant literal expression.
void post_process() override
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
virtual literalt limplies(literalt a, literalt b)=0
std::size_t get_invalid_object() const
Extract member of struct or union.
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
virtual literalt land(literalt a, literalt b)=0
exprt object_size(const exprt &pointer)
const irep_idt & id() const
void set_value(const irep_idt &value)
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
virtual const bvt & convert_bv(const exprt &expr)
virtual void l_set_to(literalt a, bool value)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
virtual bvt convert_bitvector(const exprt &expr)
API to expression classes.
virtual void add_addr(const exprt &expr, bvt &bv)
pointer_logict pointer_logic
void conversion_failed(const exprt &expr, bvt &bv)
Generic base class for unary expressions.
bool is_dynamic_object(const exprt &expr) const
#define forall_operands(it, expr)
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
virtual literalt convert_rest(const exprt &expr) override
bvt zero_extension(const bvt &bv, std::size_t new_size)
bv_pointerst(const namespacet &_ns, propt &_prop)
exprt pointer_expr(const pointert &pointer, const typet &type) const
postponed_listt postponed_list
std::vector< exprt > operandst
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
virtual literalt lequal(literalt a, literalt b)=0
unsigned integer2unsigned(const mp_integer &n)
literalt const_literal(bool value)
void post_process() override
bvt add(const bvt &op0, const bvt &op1)
void encode(std::size_t object, bvt &bv)
exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override
Base class for all expressions.
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
void do_postponed(const postponedt &postponed)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
virtual exprt bv_get_rec(const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const
virtual bvt convert_pointer_type(const exprt &expr)
irep_idt get_component_name() const
virtual tvt l_get(literalt a) const =0
virtual bvt convert_member(const member_exprt &expr)
virtual bvt convert_if(const if_exprt &expr)
const std::string & id_string() const
bool convert_address_of_rec(const exprt &expr, bvt &bv)
tv_enumt get_value() const
bvt sign_extension(const bvt &bv, std::size_t new_size)
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
const typet & subtype() const
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
std::size_t add_object(const exprt &expr)
bitvector_typet char_type()
std::vector< literalt > bvt
bvt build_constant(const mp_integer &i, std::size_t width)
void offset_arithmetic(bvt &bv, const mp_integer &x)
virtual bvt convert_bitwise(const exprt &expr)