18 if(expr.
type().
id()!=ID_bool)
19 throw "bv_pointerst::convert_rest got non-boolean operand";
23 if(expr.
id()==ID_invalid_pointer)
25 if(operands.size()==1 &&
26 operands[0].type().id()==ID_pointer)
32 bvt invalid_bv, null_bv;
36 bvt equal_invalid_bv, equal_null_bv;
51 return prop.
lor(equal_invalid, equal_null);
55 else if(expr.
id()==ID_dynamic_object)
57 if(operands.size()==1 &&
58 operands[0].type().id()==ID_pointer)
71 else if(expr.
id()==ID_lt || expr.
id()==ID_le ||
72 expr.
id()==ID_gt || expr.
id()==ID_ge)
74 if(operands.size()==2 &&
75 operands[0].type().id()==ID_pointer &&
76 operands[1].type().id()==ID_pointer)
105 if(expr.
id()==ID_symbol)
110 else if(expr.
id()==ID_label)
115 else if(expr.
id() == ID_null_object)
120 else if(expr.
id()==ID_index)
123 throw "index takes two operands";
131 if(array_type.
id()==ID_pointer)
137 else if(array_type.
id()==ID_array ||
138 array_type.
id()==ID_incomplete_array ||
139 array_type.
id()==ID_string_constant)
151 DATA_INVARIANT(size>0,
"array subtype expected to have non-zero size");
157 else if(expr.
id()==ID_byte_extract_little_endian ||
158 expr.
id()==ID_byte_extract_big_endian)
172 else if(expr.
id()==ID_member)
175 const exprt &struct_op=member_expr.
op0();
182 if(struct_op_type.
id()==ID_struct)
187 DATA_INVARIANT(offset>=0,
"member offset expected to be positive");
192 else if(struct_op_type.
id()==ID_union)
197 throw "member takes struct or union operand";
201 else if(expr.
id()==ID_constant ||
202 expr.
id()==ID_string_constant ||
208 else if(expr.
id()==ID_if)
232 if(expr.
type().
id()!=ID_pointer)
233 throw "convert_pointer_type got non-pointer type";
238 if(expr.
id()==ID_symbol)
250 else if(expr.
id()==ID_nondet_symbol)
260 else if(expr.
id()==ID_typecast)
263 throw "typecast takes one operand";
268 if(op_type.
id()==ID_pointer)
270 else if(op_type.
id()==ID_signedbv ||
271 op_type.
id()==ID_unsignedbv ||
272 op_type.
id()==ID_bool ||
273 op_type.
id()==ID_c_enum ||
274 op_type.
id()==ID_c_enum_tag)
284 else if(expr.
id()==ID_if)
288 else if(expr.
id()==ID_index)
292 else if(expr.
id()==ID_member)
296 else if(expr.
id()==ID_address_of)
299 throw expr.
id_string()+
" takes one operand";
313 else if(expr.
id()==ID_constant)
330 else if(expr.
id()==ID_plus)
335 throw "operator + takes at least two operands";
344 if(it->type().id()==ID_pointer)
352 if(pointer_sub_type.id()==ID_empty)
367 throw "found no pointer in pointer-type sum";
369 throw "found more than one pointer in sum";
375 if(it->type().id()==ID_pointer)
378 if(it->type().id()!=ID_unsignedbv &&
379 it->type().id()!=ID_signedbv)
393 throw "unexpected pointer arithmetic operand width";
399 else if(op.size()<
bits)
409 else if(expr.
id()==ID_minus)
414 throw "operator "+expr.
id_string()+
" takes two operands";
417 throw "found no pointer in pointer type in difference";
421 if(expr.
op1().
type().
id()!=ID_unsignedbv &&
436 if(pointer_sub_type.id()==ID_empty)
445 DATA_INVARIANT(element_size > 0,
"object size expected to be positive");
452 else if(expr.
id()==ID_lshr ||
457 else if(expr.
id()==ID_bitand ||
458 expr.
id()==ID_bitor ||
459 expr.
id()==ID_bitnot)
463 else if(expr.
id()==ID_concatenation)
467 else if(expr.
id()==ID_byte_extract_little_endian ||
468 expr.
id()==ID_byte_extract_big_endian)
473 expr.
id() == ID_byte_update_little_endian ||
474 expr.
id() == ID_byte_update_big_endian)
476 throw "byte-wise updates of pointers are unsupported";
484 if(expr.
type().
id()==ID_pointer)
487 if(expr.
id()==ID_minus &&
510 if(pointer_sub_type.
id()==ID_empty)
519 DATA_INVARIANT(element_size > 0,
"object size expected to be positive");
532 else if(expr.
id()==ID_pointer_offset &&
549 else if(expr.
id()==ID_object_size &&
559 for(std::size_t i=0; i<width; i++)
570 else if(expr.
id()==ID_pointer_object &&
587 else if(expr.
id()==ID_typecast &&
609 const std::vector<bool> &unknown,
611 const typet &type)
const 613 if(type.
id()!=ID_pointer)
616 std::string value_addr, value_offset, value;
618 for(std::size_t i=0; i<
bits; i++)
621 std::size_t bit_nr=i+offset;
639 value_offset=ch+value_offset;
641 value_addr=ch+value_addr;
732 const std::size_t max_objects=std::size_t(1)<<
object_bits;
735 "too many addressed objects: maximum number of objects is set to 2^n="+
737 "use the `--object-bits n` option to increase the maximum number";
745 if(postponed.
expr.
id()==ID_dynamic_object)
750 std::size_t number=0;
757 const exprt &expr=*it;
767 bvt saved_bv=postponed.
op;
768 saved_bv.erase(saved_bv.begin(), saved_bv.begin()+
offset_bits);
782 else if(postponed.
expr.
id()==ID_object_size)
787 std::size_t number=0;
794 const exprt &expr=*it;
798 if(expr.
id()==ID_symbol)
820 bvt saved_bv=postponed.
op;
821 saved_bv.erase(saved_bv.begin(), saved_bv.begin()+
offset_bits);
843 for(postponed_listt::const_iterator
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
The type of an expression.
exprt size_of_expr(const typet &type, const namespacet &ns)
std::size_t get_null_object() const
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)
pointer_typet pointer_type(const typet &subtype)
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
const irep_idt & get_identifier() const
bvt convert_bitvector(const exprt &expr) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
const irep_idt & get_value() const
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.
#define CHECK_RETURN(CONDITION)
void post_process() override
#define POSTCONDITION(CONDITION)
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
virtual literalt limplies(literalt a, literalt b)=0
std::size_t get_invalid_object() const
Extract member of struct or union.
struct configt::bv_encodingt bv_encoding
virtual literalt land(literalt a, literalt b)=0
exprt object_size(const exprt &pointer)
const irep_idt & id() const
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)
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
virtual bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
virtual void add_addr(const exprt &expr, bvt &bv)
pointer_logict pointer_logic
void conversion_failed(const exprt &expr, bvt &bv)
bool is_dynamic_object(const exprt &expr) const
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
const typet & follow(const typet &) const
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
The unary minus expression.
literalt convert_rest(const exprt &expr) override
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
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 pointer_typet &type) const
typename data_typet::const_iterator const_iterator
postponed_listt postponed_list
std::vector< exprt > operandst
virtual literalt lequal(literalt a, literalt b)=0
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)
const shift_exprt & to_shift_expr(const exprt &expr)
Cast a generic exprt to a shift_exprt.
mstreamt & result() const
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)
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)
std::string to_string(const string_constraintt &expr)
Used for debug printing.
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)
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
std::size_t integer2size_t(const mp_integer &n)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
std::size_t add_object(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
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)