Go to the documentation of this file.
23 if(expr.
id() == ID_is_invalid_pointer)
25 if(operands.size()==1 &&
26 operands[0].type().id()==ID_pointer)
48 else if(expr.
id() == ID_is_dynamic_object)
50 if(operands.size()==1 &&
51 operands[0].type().id()==ID_pointer)
64 else if(expr.
id()==ID_lt || expr.
id()==ID_le ||
65 expr.
id()==ID_gt || expr.
id()==ID_ge)
67 if(operands.size()==2 &&
68 operands[0].type().id()==ID_pointer &&
69 operands[1].type().id()==ID_pointer)
86 :
boolbvt(_ns, _prop, message_handler), pointer_logic(_ns)
98 if(expr.
id()==ID_symbol)
103 else if(expr.
id()==ID_label)
108 else if(expr.
id() == ID_null_object)
113 else if(expr.
id()==ID_index)
121 if(array_type.
id()==ID_pointer)
127 else if(array_type.
id()==ID_array ||
128 array_type.
id()==ID_string_constant)
145 else if(expr.
id()==ID_byte_extract_little_endian ||
146 expr.
id()==ID_byte_extract_big_endian)
160 else if(expr.
id()==ID_member)
170 if(struct_op_type.
id()==ID_struct)
182 struct_op_type.
id() == ID_union,
183 "member expression should operate on struct or union");
189 else if(expr.
id()==ID_constant ||
190 expr.
id()==ID_string_constant ||
196 else if(expr.
id()==ID_if)
225 if(expr.
id()==ID_symbol)
237 else if(expr.
id()==ID_nondet_symbol)
247 else if(expr.
id()==ID_typecast)
251 const exprt &op = typecast_expr.
op();
254 if(op_type.
id()==ID_pointer)
258 op_type.
id() == ID_c_enum || op_type.
id() == ID_c_enum_tag)
268 else if(expr.
id()==ID_if)
272 else if(expr.
id()==ID_index)
276 else if(expr.
id()==ID_member)
280 else if(expr.
id()==ID_address_of)
296 else if(expr.
id()==ID_constant)
313 else if(expr.
id()==ID_plus)
326 if(it->type().id()==ID_pointer)
334 if(pointer_sub_type.
id()==ID_empty)
351 "there should be exactly one pointer-type operand in a pointer-type sum");
357 if(it->type().id()==ID_pointer)
360 if(it->type().id()!=ID_unsignedbv &&
361 it->type().id()!=ID_signedbv)
379 else if(op.size()<
bits)
389 else if(expr.
id()==ID_minus)
396 minus_expr.
lhs().
type().
id() == ID_pointer,
397 "first operand should be of pointer type");
400 minus_expr.
rhs().
type().
id() != ID_unsignedbv &&
401 minus_expr.
rhs().
type().
id() != ID_signedbv)
415 if(pointer_sub_type.
id()==ID_empty)
424 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
425 element_size = *element_size_opt;
432 else if(expr.
id()==ID_lshr ||
437 else if(expr.
id()==ID_bitand ||
438 expr.
id()==ID_bitor ||
439 expr.
id()==ID_bitnot)
443 else if(expr.
id()==ID_concatenation)
447 else if(expr.
id()==ID_byte_extract_little_endian ||
448 expr.
id()==ID_byte_extract_big_endian)
462 if(expr.
id() != ID_minus)
467 return minus_expr.lhs().type().id() == ID_pointer &&
468 minus_expr.rhs().type().id() == ID_pointer;
473 if(expr.
type().
id()==ID_pointer)
494 typet pointer_sub_type = minus_expr.lhs().type().
subtype();
497 if(pointer_sub_type.
id()==ID_empty)
506 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
507 element_size = *element_size_opt;
510 if(element_size != 1)
520 expr.
id() == ID_pointer_offset &&
537 expr.
id() == ID_object_size &&
546 for(std::size_t i=0; i<width; i++)
558 expr.
id() == ID_pointer_object &&
575 expr.
id() == ID_typecast &&
597 const std::vector<bool> &unknown,
599 const typet &type)
const
601 if(type.
id()!=ID_pointer)
604 std::string value_addr, value_offset, value;
606 for(std::size_t i=0; i<
bits; i++)
609 std::size_t bit_nr=i+offset;
627 value_offset=ch+value_offset;
629 value_addr=ch+value_addr;
636 return value[value.size() - 1 - i] ==
'1';
647 result.copy_to_operands(
650 return std::move(result);
724 const std::size_t max_objects=std::size_t(1)<<
object_bits;
728 "too many addressed objects: maximum number of objects is set to 2^n=" +
731 "use the `--object-bits n` option to increase the maximum number");
739 if(postponed.
expr.
id() == ID_is_dynamic_object)
742 std::size_t number=0;
744 for(
auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
746 const exprt &expr=*it;
756 bvt saved_bv=postponed.
op;
757 saved_bv.erase(saved_bv.begin(), saved_bv.begin()+
offset_bits);
771 else if(postponed.
expr.
id()==ID_object_size)
774 std::size_t number=0;
776 for(
auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
778 const exprt &expr=*it;
780 if(expr.
id() != ID_symbol && expr.
id() != ID_string_constant)
785 if(!size_expr.has_value())
789 size_expr.value(), postponed.
expr.
type());
797 bvt saved_bv=postponed.
op;
798 saved_bv.erase(saved_bv.begin(), saved_bv.begin()+
offset_bits);
821 for(postponed_listt::const_iterator
#define UNREACHABLE
This should be used to mark dead code.
std::size_t get_null_object() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
static exprt conditional_cast(const exprt &expr, const typet &type)
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const typet & subtype() const
virtual bvt convert_member(const member_exprt &expr)
virtual bvt convert_byte_update(const byte_update_exprt &expr)
struct configt::bv_encodingt bv_encoding
bool convert_address_of_rec(const exprt &expr, bvt &bv)
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
virtual bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
#define CHECK_RETURN(CONDITION)
The type of an expression, extends irept.
std::vector< literalt > bvt
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
postponed_listt postponed_list
bv_pointerst(const namespacet &_ns, propt &_prop, message_handlert &message_handler)
The trinary if-then-else operator.
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const
const mp_integer string2integer(const std::string &n, unsigned base)
std::size_t add_object(const exprt &expr)
void get_literals(const irep_idt &identifier, const typet &type, const std::size_t width, bvt &literals)
bvt sign_extension(const bvt &bv, std::size_t new_size)
The plus expression Associativity is not specified.
void do_postponed(const postponedt &postponed)
virtual literalt new_variable()=0
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
Base class for all expressions.
void l_set_to_true(literalt a)
exprt bv_get_rec(const exprt &expr, const bvt &bv, const std::vector< bool > &unknown, std::size_t offset, const typet &type) const override
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
virtual bvt convert_pointer_type(const exprt &expr)
bvt unsigned_multiplier(const bvt &op0, const bvt &op1)
virtual literalt land(literalt a, literalt b)=0
#define Forall_literals(it, bv)
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
virtual bvt convert_concatenation(const concatenation_exprt &expr)
const concatenation_exprt & to_concatenation_expr(const exprt &expr)
Cast an exprt to a concatenation_exprt.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
virtual bvt convert_shift(const binary_exprt &expr)
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
hash_numbering< exprt, irep_hash > objects
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
bvt add(const bvt &op0, const bvt &op1)
boolbv_widtht boolbv_width
void conversion_failed(const exprt &expr, bvt &bv)
virtual literalt limplies(literalt a, literalt b)=0
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
bvt convert_bitvector(const exprt &expr) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
const exprt & compound() const
#define forall_operands(it, expr)
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
virtual bvt convert_if(const if_exprt &expr)
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
literalt const_literal(bool value)
void post_process() override
pointer_logict pointer_logic
pointer_typet pointer_type(const typet &subtype)
The unary minus expression.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
exprt object_size(const exprt &pointer)
const irep_idt & id() const
std::vector< exprt > operandst
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...
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
void encode(std::size_t object, bvt &bv)
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Extract member of struct or union.
virtual bvt convert_bitwise(const exprt &expr)
bvt build_constant(const mp_integer &i, std::size_t width)
virtual literalt lequal(literalt a, literalt b)=0
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
#define POSTCONDITION(CONDITION)
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
bool is_dynamic_object(const exprt &expr) const
virtual tvt l_get(literalt a) const =0
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
std::size_t get_invalid_object() const
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
irep_idt get_component_name() const
Operator to return the address of an object.
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Semantic type conversion.
tv_enumt get_value() const
void offset_arithmetic(bvt &bv, const mp_integer &x)
literalt convert_rest(const exprt &expr) override
A constant literal expression.
literalt convert_rest(const exprt &expr) override
void post_process() override
static bool is_pointer_subtraction(const exprt &expr)
const irep_idt & get_value() const
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
virtual void add_addr(const exprt &expr, bvt &bv)
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
bvt zero_extension(const bvt &bv, std::size_t new_size)
bvt sub(const bvt &op0, const bvt &op1)
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.