28 const std::size_t pointer_width = 2 * type.
get_width();
31 return pointer_width - object_width;
42 bv.begin() + offset_width, bv.begin() + offset_width + object_width);
51 return bvt(bv.begin(), bv.begin() + offset_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());
72 if(expr.
id() == ID_is_invalid_pointer)
74 if(operands.size() == 1 && operands[0].type().id() == ID_pointer)
89 equal_invalid_bv.reserve(object_bits);
91 for(std::size_t i = 0; i < object_bits; i++)
93 equal_invalid_bv.push_back(
prop.lequal(object_bv[i], invalid_bv[i]));
96 return prop.land(equal_invalid_bv);
100 else if(expr.
id() == ID_is_dynamic_object)
102 if(operands.size() == 1 && operands[0].type().id() == ID_pointer)
113 expr.
id() == ID_lt || expr.
id() == ID_le || expr.
id() == ID_gt ||
117 operands.size() == 2 && operands[0].type().id() == ID_pointer &&
118 operands[1].type().id() == ID_pointer)
138 return same_object_lit;
166 if(expr.
id() == ID_symbol)
170 else if(expr.
id() == ID_label)
174 else if(expr.
id() == ID_null_object)
179 else if(expr.
id() == ID_index)
192 if(array_type.id() == ID_pointer)
199 array_type.id() == ID_array || array_type.id() == ID_string_constant)
202 if(!bv_opt.has_value())
204 bv = std::move(*bv_opt);
217 return std::move(bv);
220 expr.
id() == ID_byte_extract_little_endian ||
221 expr.
id() == ID_byte_extract_big_endian)
227 if(!bv_opt.has_value())
236 return std::move(bv);
238 else if(expr.
id() == ID_member)
245 if(!bv_opt.has_value())
248 bvt bv = std::move(*bv_opt);
249 if(struct_op.
type().
id() == ID_struct_tag)
264 struct_op.
type().
id() == ID_union_tag,
265 "member expression should operate on struct or union");
269 return std::move(bv);
273 expr.
id() == ID_array)
277 else if(expr.
id() == ID_if)
286 if(!bv1_opt.has_value())
290 if(!bv2_opt.has_value())
293 return bv_utils.select(cond, *bv1_opt, *bv2_opt);
305 if(expr.
id() == ID_symbol)
309 return map.get_literals(identifier, type,
bits);
311 else if(expr.
id() == ID_nondet_symbol)
315 else if(expr.
id() == ID_typecast)
319 const exprt &op = typecast_expr.
op();
322 if(op_type.
id() == ID_pointer)
326 op_type.
id() == ID_c_enum || op_type.
id() == ID_c_enum_tag)
332 auto top_bit = op_bv.back();
333 const auto numbered_pointer_bv =
prop.new_variables(
bits);
341 {const_literal(true)}));
345 numbered_pointer_bv);
355 return bv_utils.select(top_bit, numbered_pointer_bv, null_object_bv);
358 else if(expr.
id() == ID_if)
362 else if(expr.
id() == ID_index)
366 else if(expr.
id() == ID_member)
370 else if(expr.
id() == ID_address_of)
375 if(!bv_opt.has_value())
381 else if(expr.
id() == ID_object_address)
384 return add_addr(object_address_expr.object_expr());
398 else if(expr.
id() == ID_plus)
407 std::size_t count = 0;
409 for(
const auto &op : plus_expr.
operands())
411 if(op.type().id() == ID_pointer)
419 pointer_base_type.
id() != ID_empty,
420 "no pointer arithmetic over void pointers");
429 "there should be exactly one pointer-type operand in a pointer-type sum");
434 for(
const auto &op : plus_expr.
operands())
436 if(op.type().id() == ID_pointer)
439 if(op.type().id() != ID_unsignedbv && op.type().id() != ID_signedbv)
451 op_bv =
bv_utils.extension(op_bv, offset_bits, rep);
458 else if(expr.
id() == ID_minus)
465 minus_expr.
lhs().
type().
id() == ID_pointer,
466 "first operand should be of pointer type");
469 minus_expr.
rhs().
type().
id() != ID_unsignedbv &&
470 minus_expr.
rhs().
type().
id() != ID_signedbv)
479 typet pointer_base_type =
482 pointer_base_type.
id() != ID_empty,
483 "no pointer arithmetic over void pointers");
485 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
489 expr.
id() == ID_byte_extract_little_endian ||
490 expr.
id() == ID_byte_extract_big_endian)
495 expr.
id() == ID_byte_update_little_endian ||
496 expr.
id() == ID_byte_update_big_endian)
500 else if(expr.
id() == ID_field_address)
507 if(field_address_expr.compound_type().id() == ID_struct_tag)
511 field_address_expr.component_name(),
518 else if(field_address_expr.compound_type().id() == ID_union_tag)
524 INVARIANT(
false,
"field address expressions operate on struct or union");
529 else if(expr.
id() == ID_element_address)
542 element_address_expr.type(), bv, *size, element_address_expr.index());
552 if(expr.
id() != ID_minus)
557 return minus_expr.lhs().type().id() == ID_pointer &&
558 minus_expr.rhs().type().id() == ID_pointer;
563 if(expr.
type().
id() == ID_pointer)
584 const bvt object_size_bv =
587 bvt bv =
prop.new_variables(width);
593 const bvt lhs_offset =
606 const bvt rhs_offset =
617 bvt difference =
bv_utils.sub(lhs_offset, rhs_offset);
621 "no pointer arithmetic over void pointers");
623 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
625 if(*element_size_opt != 1)
627 bvt element_size_bv =
bv_utils.build_constant(*element_size_opt, width);
633 prop.land(same_object_lit,
prop.land(lhs_in_bounds, rhs_in_bounds)),
640 expr.
id() == ID_pointer_offset &&
655 return bv_utils.sign_extension(offset_bv, width);
664 prop.new_variables(width),
671 expr.
id() == ID_pointer_object &&
685 return bv_utils.zero_extension(object_bv, width);
688 expr.
id() == ID_typecast &&
700 if(target_width == 0)
714 bv_utils.build_constant(number, target_width - 1),
715 {const_literal(true)}));
725 for(
const auto &literal : bv)
738 result = ch + result;
747 std::size_t offset)
const
749 const auto &type = expr.
type();
751 if(type.id() != ID_pointer)
756 bvt value_bv(bv.begin() + offset, bv.begin() + offset +
bits);
760 std::string value_offset =
767 return value[value.size() - 1 - i] ==
'1';
787 bvt object =
bv_utils.build_constant(addr, object_bits);
800 type, bv, 1,
bv_utils.build_constant(x, offset_bits));
816 bv_index =
bv_utils.extension(bv_index, offset_bits, rep);
833 bvt bv_factor =
bv_utils.build_constant(factor, index.size());
834 bv_index =
bv_utils.signed_multiplier(index, bv_factor);
838 bv_index =
bv_utils.sign_extension(bv_index, offset_bits);
853 const std::size_t max_objects = std::size_t(1) << object_bits;
857 "too many addressed objects: maximum number of objects is set to 2^n=" +
858 std::to_string(max_objects) +
" (with n=" + std::to_string(object_bits) +
860 "use the `--object-bits n` option to increase the maximum number");
867 if(postponed.
expr.
id() == ID_is_dynamic_object)
872 std::size_t number = 0;
874 for(
auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
876 const exprt &expr = *it;
895 prop.l_set_to_true(
prop.limplies(l1, l2));
899 const auto postponed_object_size =
902 const auto &type =
to_pointer_type(postponed_object_size->pointer().type());
904 std::size_t number = 0;
906 for(
auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
908 const exprt &expr = *it;
910 if(expr.
id() != ID_symbol && expr.
id() != ID_string_constant)
915 if(!size_expr.has_value())
919 size_expr.value(), postponed_object_size->type());
936 prop.l_set_to_true(
prop.limplies(l1, l2));
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.
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...
message_handlert & message_handler
bool get_array_constraints
std::size_t get_width() const
virtual bvt convert_index(const exprt &array, const mp_integer &index)
index operator with constant index
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
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...
boolbvt(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
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
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.
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
bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &)
std::optional< bvt > convert_address_of_rec(const exprt &)
void do_postponed(const postponedt &postponed)
exprt bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override
virtual 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 bvt zero_extension(const bvt &bv, std::size_t new_size)
static bvt build_constant(const mp_integer &i, std::size_t width)
static bvt concatenate(const bvt &a, const bvt &b)
A constant literal expression.
const irep_idt & get_value() const
bool is_null_pointer() const
Returns true if expr has a pointer type and a value NULL; it also returns true when expr has value ze...
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.
const exprt & compound() const
irep_idt get_component_name() const
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.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
const typet & base_type() const
The type of the data what we point to.
virtual tvt l_get(literalt a) const =0
const irep_idt & get_identifier() const
tv_enumt get_value() const
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 can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
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.
std::optional< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
std::optional< exprt > size_of_expr(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
Various predicates over pointers in programs.
const std::size_t sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::bits
#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_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.