28 const std::size_t pointer_width = 2 * type.
get_width();
59 result.reserve(offset.size() +
object.size());
60 result.insert(result.end(), offset.begin(), offset.end());
61 result.insert(result.end(),
object.begin(),
object.end());
74 if(operands.size() == 1 && operands[0].type().id() ==
ID_pointer)
91 for(std::size_t i = 0; i < object_bits; i++)
102 if(operands.size() == 1 && operands[0].type().id() ==
ID_pointer)
117 operands.size() == 2 && operands[0].type().id() ==
ID_pointer &&
158 bool get_array_constraints)
217 return std::move(bv);
236 return std::move(bv);
264 "member expression should operate on struct or union");
268 return std::move(bv);
340 {const_literal(true)}));
406 std::size_t count = 0;
408 for(
const auto &op :
plus_expr.operands())
419 "no pointer arithmetic over void pointers");
428 "there should be exactly one pointer-type operand in a pointer-type sum");
433 for(
const auto &op :
plus_expr.operands())
465 "first operand should be of pointer type");
482 "no pointer arithmetic over void pointers");
522 INVARIANT(
false,
"field address expressions operate on struct or union");
619 "no pointer arithmetic over void pointers");
713 {const_literal(true)}));
736 result =
ch + result;
745 std::size_t offset)
const
747 const auto &type = expr.
type();
754 bvt value_bv(bv.begin() + offset, bv.begin() + offset + bits);
765 return value[value.size() - 1 - i] ==
'1';
851 const std::size_t
max_objects = std::size_t(1) << object_bits;
855 "too many addressed objects: maximum number of objects is set to 2^n=" +
856 std::to_string(
max_objects) +
" (with n=" + std::to_string(object_bits) +
858 "use the `--object-bits n` option to increase the maximum number");
870 std::size_t number = 0;
872 for(
auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
874 const exprt &expr = *it;
902 std::size_t number = 0;
904 for(
auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
906 const exprt &expr = *it;
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_table_baset &symbol_table, message_handlert &message_handler)
static std::string bits_to_string(const propt &prop, const bvt &bv)
static bool is_pointer_subtraction(const exprt &expr)
Expression classes for byte-level operators.
const byte_update_exprt & to_byte_update_expr(const exprt &expr)
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
pointer_typet pointer_type(const typet &subtype)
Operator to return the address of an object.
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Thrown when an unexpected error occurs during the analysis (e.g., when the SAT solver returns an erro...
Pointer-typed bitvector constant annotated with the pointer expression that the bitvector is the nume...
std::size_t get_width() const
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
virtual bvt convert_bitvector(const exprt &expr)
Converts an expression into its gate-level representation and returns a vector of literals correspond...
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset) const
virtual bvt convert_member(const member_exprt &expr)
virtual bvt convert_if(const if_exprt &expr)
virtual bvt convert_byte_update(const byte_update_exprt &expr)
void finish_eager_conversion() override
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
literalt convert_rest(const exprt &expr) override
bv_pointers_widet(const namespacet &, propt &, message_handlert &, bool get_array_constraints=false)
virtual bvt convert_pointer_type(const exprt &)
bvt object_literals(const bvt &bv, const pointer_typet &type) const
Given a pointer encoded in bv, extract the literals identifying the object that the pointer points to...
literalt convert_rest(const exprt &) override
bvt convert_bitvector(const exprt &) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
std::size_t get_object_width(const pointer_typet &) const
static bvt object_offset_encoding(const bvt &object, const bvt &offset)
Construct a pointer encoding from given encodings of object and offset.
NODISCARD optionalt< bvt > convert_address_of_rec(const exprt &)
NODISCARD bvt encode(const mp_integer &object, const pointer_typet &) const
std::vector< bvt > numbered_pointers
Table that maps a 'pointer number' to its full-width bit-vector.
pointer_logict pointer_logic
postponed_listt postponed_list
NODISCARD bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &)
void do_postponed(const postponedt &postponed)
exprt bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override
virtual NODISCARD bvt add_addr(const exprt &)
void finish_eager_conversion() override
std::size_t get_offset_width(const pointer_typet &) const
bvt offset_literals(const bvt &bv, const pointer_typet &type) const
Given a pointer encoded in bv, extract the literals representing the offset into an object that the p...
std::size_t boolbv_width(const typet &type) const override
static literalt sign_bit(const bvt &op)
bvt add(const bvt &op0, const bvt &op1)
static bvt zero_extension(const bvt &bv, std::size_t new_size)
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
static bvt build_constant(const mp_integer &i, std::size_t width)
literalt is_zero(const bvt &op)
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
bvt signed_multiplier(const bvt &op0, const bvt &op1)
void cond_implies_equal(literalt cond, const bvt &a, const bvt &b)
static bvt concatenate(const bvt &a, const bvt &b)
bvt sub(const bvt &op0, const bvt &op1)
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
static bvt zeros(std::size_t new_size)
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
static bvt sign_extension(const bvt &bv, std::size_t new_size)
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
The trinary if-then-else operator.
const irep_idt & id() const
Extract member of struct or union.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The plus expression Associativity is not specified.
const mp_integer & get_invalid_object() const
const mp_integer & get_null_object() const
numberingt< exprt, irep_hash > objects
exprt pointer_expr(const pointert &pointer, const pointer_typet &type) const
Convert an (object,offset) pair to an expression.
mp_integer add_object(const exprt &expr)
bool is_dynamic_object(const exprt &expr) const
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
virtual literalt limplies(literalt a, literalt b)=0
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
virtual literalt new_variable()=0
virtual literalt lequal(literalt a, literalt b)=0
virtual tvt l_get(literalt a) const =0
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
The unary minus expression.
bool is_null_pointer(const constant_exprt &expr)
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
Deprecated expression utility functions.
std::vector< literalt > bvt
literalt const_literal(bool value)
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
static bool is_dynamic(const exprt &object)
This function returns true for heap allocated objects or false for stack allocated objects.
API to expression classes for Pointers.
const element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
const object_address_exprt & to_object_address_expr(const exprt &expr)
Cast an exprt to an object_address_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_exprt.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
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.
optionalt< exprt > size_of_expr(const typet &type, const namespacet &ns)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
#define POSTCONDITION(CONDITION)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.