40 build(type, little_endian);
53 if(!width_opt.has_value())
56 const std::size_t new_size =
map.size() + *width_opt;
57 map.reserve(new_size);
59 for(std::size_t i =
map.size(); i < new_size; ++i)
65 if(src.
id() == ID_pointer)
80 return config.bv_encoding.object_bits;
85 const std::size_t pointer_width = type.
get_width();
88 return pointer_width - object_width;
104 bv.begin() + offset_width, bv.begin() + offset_width + object_width);
113 return bvt(bv.begin(), bv.begin() + offset_width);
119 result.reserve(offset.size() +
object.size());
120 result.insert(result.end(), offset.begin(), offset.end());
121 result.insert(result.end(),
object.begin(),
object.end());
132 if(expr.
id() == ID_is_invalid_pointer)
134 if(operands.size()==1 &&
135 operands[0].type().id()==ID_pointer)
149 bvt equal_invalid_bv;
150 equal_invalid_bv.reserve(object_bits);
152 for(std::size_t i=0; i<object_bits; i++)
154 equal_invalid_bv.push_back(
prop.lequal(object_bv[i], invalid_bv[i]));
157 return prop.land(equal_invalid_bv);
161 else if(expr.
id() == ID_is_dynamic_object)
163 if(operands.size()==1 &&
164 operands[0].type().id()==ID_pointer)
174 else if(expr.
id()==ID_lt || expr.
id()==ID_le ||
175 expr.
id()==ID_gt || expr.
id()==ID_ge)
177 if(operands.size()==2 &&
178 operands[0].type().id()==ID_pointer &&
179 operands[1].type().id()==ID_pointer)
199 return same_object_lit;
212 auto prophecy_r_or_w_ok =
218 auto prophecy_pointer_in_range =
239 if(expr.
id()==ID_symbol)
243 else if(expr.
id()==ID_label)
247 else if(expr.
id() == ID_null_object)
252 else if(expr.
id()==ID_index)
265 if(array_type.id()==ID_pointer)
271 else if(array_type.id()==ID_array ||
272 array_type.id()==ID_string_constant)
275 if(!bv_opt.has_value())
277 bv = std::move(*bv_opt);
290 return std::move(bv);
292 else if(expr.
id()==ID_byte_extract_little_endian ||
293 expr.
id()==ID_byte_extract_big_endian)
299 if(!bv_opt.has_value())
308 return std::move(bv);
310 else if(expr.
id()==ID_member)
317 if(!bv_opt.has_value())
320 bvt bv = std::move(*bv_opt);
322 struct_op.
type().
id() == ID_struct ||
323 struct_op.
type().
id() == ID_struct_tag)
326 struct_op.
type().
id() == ID_struct_tag
340 struct_op.
type().
id() == ID_union ||
341 struct_op.
type().
id() == ID_union_tag,
342 "member expression should operate on struct or union");
346 return std::move(bv);
350 expr.
id() == ID_array)
354 else if(expr.
id()==ID_if)
363 if(!bv1_opt.has_value())
367 if(!bv2_opt.has_value())
370 return bv_utils.select(cond, *bv1_opt, *bv2_opt);
382 if(expr.
id()==ID_symbol)
386 return map.get_literals(identifier, type,
bits);
388 else if(expr.
id()==ID_nondet_symbol)
392 else if(expr.
id()==ID_typecast)
396 const exprt &op = typecast_expr.
op();
399 if(op_type.
id()==ID_pointer)
403 op_type.
id() == ID_c_enum || op_type.
id() == ID_c_enum_tag)
413 else if(expr.
id()==ID_if)
417 else if(expr.
id()==ID_index)
421 else if(expr.
id()==ID_member)
425 else if(expr.
id()==ID_address_of)
430 if(!bv_opt.has_value())
436 else if(expr.
id() == ID_object_address)
439 return add_addr(object_address_expr.object_expr());
453 else if(expr.
id()==ID_plus)
464 for(
const auto &op : plus_expr.
operands())
466 if(op.type().id() == ID_pointer)
474 pointer_base_type.
id() != ID_empty,
475 "no pointer arithmetic over void pointers");
484 "there should be exactly one pointer-type operand in a pointer-type sum");
489 for(
const auto &operand : plus_expr.
operands())
491 if(operand.type().id() == ID_pointer)
495 operand.type().id() != ID_unsignedbv &&
496 operand.type().id() != ID_signedbv)
508 op =
bv_utils.extension(op, offset_bits, rep);
515 else if(expr.
id()==ID_minus)
522 minus_expr.
lhs().
type().
id() == ID_pointer,
523 "first operand should be of pointer type");
526 minus_expr.
rhs().
type().
id() != ID_unsignedbv &&
527 minus_expr.
rhs().
type().
id() != ID_signedbv)
536 typet pointer_base_type =
539 pointer_base_type.
id() != ID_empty,
540 "no pointer arithmetic over void pointers");
542 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
545 else if(expr.
id()==ID_byte_extract_little_endian ||
546 expr.
id()==ID_byte_extract_big_endian)
551 expr.
id() == ID_byte_update_little_endian ||
552 expr.
id() == ID_byte_update_big_endian)
556 else if(expr.
id() == ID_field_address)
559 const typet &compound_type = field_address_expr.compound_type();
564 if(compound_type.
id() == ID_struct || compound_type.
id() == ID_struct_tag)
567 compound_type.
id() == ID_struct_tag
578 compound_type.
id() == ID_union || compound_type.
id() == ID_union_tag)
584 INVARIANT(
false,
"field address expressions operate on struct or union");
589 else if(expr.
id() == ID_element_address)
602 element_address_expr.type(), bv, *size, element_address_expr.index());
612 if(expr.
id() != ID_minus)
617 return minus_expr.lhs().type().id() == ID_pointer &&
618 minus_expr.rhs().type().id() == ID_pointer;
623 if(expr.
type().
id()==ID_pointer)
639 bvt bv =
prop.new_variables(width);
645 const bvt lhs_offset =
650 const bvt rhs_offset =
653 bvt difference =
bv_utils.sub(lhs_offset, rhs_offset);
657 "no pointer arithmetic over void pointers");
659 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
661 if(*element_size_opt != 1)
663 bvt element_size_bv =
bv_utils.build_constant(*element_size_opt, width);
669 prop.limplies(same_object_lit,
bv_utils.equal(difference, bv)));
675 expr.
id() == ID_pointer_offset &&
686 return bv_utils.zero_extension(offset_bv, width);
695 prop.new_variables(width),
702 expr.
id() == ID_pointer_object &&
713 return bv_utils.zero_extension(object_bv, width);
716 expr.
id() == ID_typecast &&
725 return bv_utils.zero_extension(op0, width);
735 for(
const auto &literal : bv)
748 result = ch + result;
757 std::size_t offset)
const
761 if(type.
id() != ID_pointer)
766 bvt value_bv(bv.begin() + offset, bv.begin() + offset +
bits);
770 std::string value_offset =
777 return value[value.size() - 1 - i] ==
'1';
797 bvt object =
bv_utils.build_constant(addr, object_bits);
810 type, bv, 1,
bv_utils.build_constant(x, offset_bits));
826 bv_index=
bv_utils.extension(bv_index, offset_bits, rep);
845 bv_index =
bv_utils.multiplier(bv_index, bv_factor, rep);
848 bv_index =
bv_utils.extension(bv_index, offset_bits, rep);
865 bvt bv_factor=
bv_utils.build_constant(factor, index.size());
866 bv_index =
bv_utils.signed_multiplier(index, bv_factor);
870 bv_index =
bv_utils.zero_extension(bv_index, offset_bits);
885 const std::size_t max_objects=std::size_t(1)<<object_bits;
889 "too many addressed objects: maximum number of objects is set to 2^n=" +
890 std::to_string(max_objects) +
" (with n=" + std::to_string(object_bits) +
892 "use the `--object-bits n` option to increase the maximum number");
898 std::vector<symbol_exprt> &placeholders)
const
903 std::size_t number = 0;
906 dynamic_objects_ops.reserve(objects.size());
907 not_dynamic_objects_ops.reserve(objects.size());
909 for(
auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
911 const exprt &expr = *it;
918 conjuncts.reserve(bv.size());
919 placeholders.reserve(bv.size());
920 for(std::size_t i = 0; i < bv.size(); ++i)
922 if(placeholders.size() <= i)
927 conjuncts.emplace_back(placeholders[i]);
929 conjuncts.emplace_back(
not_exprt{placeholders[i]});
933 dynamic_objects_ops.push_back(
conjunction(conjuncts));
935 not_dynamic_objects_ops.push_back(
conjunction(conjuncts));
943 bddt not_dyn_bdd = bdd_converter.
from_expr(not_dynamic_objects);
945 return {bdd_converter.
as_expr(dyn_bdd), bdd_converter.
as_expr(not_dyn_bdd)};
948std::unordered_map<exprt, exprt, irep_hash>
950 std::vector<symbol_exprt> &placeholders)
const
955 std::size_t number = 0;
957 std::unordered_map<exprt, exprt::operandst, irep_hash> per_size_object_ops;
959 for(
auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
961 const exprt &expr = *it;
963 if(expr.
id() != ID_symbol && expr.
id() != ID_string_constant)
967 if(!size_expr.has_value())
975 conjuncts.reserve(bv.size());
976 placeholders.reserve(bv.size());
977 for(std::size_t i = 0; i < bv.size(); ++i)
979 if(placeholders.size() <= i)
984 conjuncts.emplace_back(placeholders[i]);
986 conjuncts.emplace_back(
not_exprt{placeholders[i]});
989 per_size_object_ops[size_expr.value()].push_back(
conjunction(conjuncts));
992 std::unordered_map<exprt, exprt, irep_hash> result;
993 for(
const auto &size_entry : per_size_object_ops)
999 result.emplace(size_entry.first, bdd_converter.
as_expr(bdd));
1013 std::vector<symbol_exprt> is_dynamic_placeholders;
1015 std::unordered_map<exprt, exprt, irep_hash> object_sizes;
1016 std::vector<symbol_exprt> object_size_placeholders;
1020 if(postponed.expr.id() == ID_is_dynamic_object)
1022 if(is_dynamic_expr.first.is_nil())
1029 POSTCONDITION(saved_bv.size() == is_dynamic_placeholders.size());
1031 for(std::size_t i = 0; i < saved_bv.size(); ++i)
1033 replacements.emplace(
1036 exprt is_dyn = is_dynamic_expr.first;
1038 exprt is_not_dyn = is_dynamic_expr.second;
1045 prop.limplies(
convert_bv(is_not_dyn)[0], !postponed.bv.front()));
1048 const auto postponed_object_size =
1051 if(object_sizes.empty())
1055 if(object_size_placeholders.empty())
1061 POSTCONDITION(saved_bv.size() == object_size_placeholders.size());
1063 for(std::size_t i = 0; i < saved_bv.size(); ++i)
1065 replacements.emplace(
1069 for(
const auto &object_size_entry : object_sizes)
1072 object_size_entry.first, postponed_object_size->type());
1076 exprt all_objects_this_size = object_size_entry.second;
1082 for(std::size_t i = 0; i < postponed.bv.size(); ++i)
1083 prop.set_equal(postponed.bv[i], size_bv[i]);
1088#define COMPACT_OBJECT_SIZE_EQ
1089#ifndef COMPACT_OBJECT_SIZE_EQ
1092 prop.l_set_to_true(
prop.limplies(l1, l2));
1094 for(std::size_t i = 0; i < postponed.bv.size(); ++i)
1096 prop.lcnf({!l1, !postponed.bv[i], size_bv[i]});
1097 prop.lcnf({!l1, postponed.bv[i], !size_bv[i]});
Conversion between exprt and miniBDD.
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)
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
Conversion between exprt and bbdt This encapsulate a bdd_managert, thus BDDs created with this class ...
exprt as_expr(const bddt &root) const
bddt from_expr(const exprt &expr)
Logical operations on BDDs.
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.
virtual std::size_t boolbv_width(const typet &type) const
literalt convert_rest(const exprt &expr) override
Map bytes according to the configured endianness.
void build_little_endian(const typet &type) override
void build_big_endian(const typet &type) override
const boolbv_widtht & boolbv_width
bv_endianness_mapt(const typet &type, bool little_endian, const namespacet &_ns, const boolbv_widtht &_boolbv_width)
std::size_t get_object_width(const pointer_typet &) const
pointer_logict pointer_logic
std::unordered_map< exprt, exprt, irep_hash > prepare_postponed_object_size(std::vector< symbol_exprt > &placeholders) const
Create Boolean functions describing all objects of each known object size over placeholders as input ...
bvt offset_arithmetic(const pointer_typet &, const bvt &, const mp_integer &)
postponed_listt postponed_list
std::size_t get_address_width(const pointer_typet &) const
virtual bvt add_addr(const exprt &)
endianness_mapt endianness_map(const typet &, bool little_endian) const override
void finish_eager_conversion() override
exprt bv_get_rec(const exprt &, const bvt &, std::size_t offset) const override
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::pair< exprt, exprt > prepare_postponed_is_dynamic_object(std::vector< symbol_exprt > &placeholders) const
Create Boolean functions describing all dynamic and all not-dynamic object encodings over placeholder...
std::size_t get_offset_width(const pointer_typet &) const
literalt convert_rest(const exprt &) override
bv_pointerst(const namespacet &, propt &, message_handlert &, bool get_array_constraints=false)
bvt convert_bitvector(const exprt &) override
Converts an expression into its gate-level representation and returns a vector of literals correspond...
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...
std::optional< bvt > convert_address_of_rec(const exprt &)
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...
virtual bvt convert_pointer_type(const exprt &)
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...
Maps a big-endian offset to a little-endian offset.
virtual void build_big_endian(const typet &type)
endianness_mapt(const typet &type, bool little_endian, const namespacet &_ns)
void build(const typet &type, bool little_endian)
std::vector< size_t > map
Base class for all expressions.
std::vector< exprt > operandst
bool is_boolean() const
Return whether the expression represents a Boolean.
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
Structure type, corresponds to C style structs.
Expression to hold a symbol (variable)
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.
bool is_true(const literalt &l)
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
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.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
const std::size_t sharing_mapt< keyT, valueT, fail_if_equal, hashT, equalT >::bits
exprt simplify_expr(exprt src, const namespacet &ns)
#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)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
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.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
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.