41 build(type, little_endian);
54 if(!width_opt.has_value())
57 const std::size_t new_size =
map.size() + *width_opt;
58 map.reserve(new_size);
60 for(std::size_t i =
map.size(); i < new_size; ++i)
66 if(src.
id() == ID_pointer)
86 const std::size_t pointer_width = type.
get_width();
89 return pointer_width - object_width;
105 bv.begin() + offset_width, bv.begin() + offset_width + object_width);
114 return bvt(bv.begin(), bv.begin() + offset_width);
120 result.reserve(offset.size() +
object.size());
121 result.insert(result.end(), offset.begin(), offset.end());
122 result.insert(result.end(),
object.begin(),
object.end());
133 if(expr.
id() == ID_is_invalid_pointer)
135 if(operands.size()==1 &&
136 operands[0].type().id()==ID_pointer)
150 bvt equal_invalid_bv;
151 equal_invalid_bv.reserve(object_bits);
153 for(std::size_t i=0; i<object_bits; i++)
155 equal_invalid_bv.push_back(
prop.
lequal(object_bv[i], invalid_bv[i]));
162 else if(expr.
id() == ID_is_dynamic_object)
164 if(operands.size()==1 &&
165 operands[0].type().id()==ID_pointer)
175 else if(expr.
id()==ID_lt || expr.
id()==ID_le ||
176 expr.
id()==ID_gt || expr.
id()==ID_ge)
178 if(operands.size()==2 &&
179 operands[0].type().id()==ID_pointer &&
180 operands[1].type().id()==ID_pointer)
200 return same_object_lit;
213 auto prophecy_r_or_w_ok =
214 expr_try_dynamic_cast<prophecy_r_or_w_ok_exprt>(expr))
219 auto prophecy_pointer_in_range =
220 expr_try_dynamic_cast<prophecy_pointer_in_range_exprt>(expr))
232 bool get_array_constraints)
233 :
boolbvt(_ns, _prop, message_handler, get_array_constraints),
240 if(expr.
id()==ID_symbol)
244 else if(expr.
id()==ID_label)
248 else if(expr.
id() == ID_null_object)
253 else if(expr.
id()==ID_index)
266 if(array_type.id()==ID_pointer)
272 else if(array_type.id()==ID_array ||
273 array_type.id()==ID_string_constant)
276 if(!bv_opt.has_value())
278 bv = std::move(*bv_opt);
291 return std::move(bv);
293 else if(expr.
id()==ID_byte_extract_little_endian ||
294 expr.
id()==ID_byte_extract_big_endian)
300 if(!bv_opt.has_value())
309 return std::move(bv);
311 else if(expr.
id()==ID_member)
319 if(!bv_opt.has_value())
322 bvt bv = std::move(*bv_opt);
323 if(struct_op_type.
id()==ID_struct)
336 struct_op_type.
id() == ID_union,
337 "member expression should operate on struct or union");
341 return std::move(bv);
345 expr.
id() == ID_array)
349 else if(expr.
id()==ID_if)
358 if(!bv1_opt.has_value())
362 if(!bv2_opt.has_value())
377 if(expr.
id()==ID_symbol)
383 else if(expr.
id()==ID_nondet_symbol)
387 else if(expr.
id()==ID_typecast)
391 const exprt &op = typecast_expr.
op();
394 if(op_type.
id()==ID_pointer)
398 op_type.
id() == ID_c_enum || op_type.
id() == ID_c_enum_tag)
408 else if(expr.
id()==ID_if)
412 else if(expr.
id()==ID_index)
416 else if(expr.
id()==ID_member)
420 else if(expr.
id()==ID_address_of)
425 if(!bv_opt.has_value())
431 else if(expr.
id() == ID_object_address)
434 return add_addr(object_address_expr.object_expr());
448 else if(expr.
id()==ID_plus)
459 for(
const auto &op : plus_expr.
operands())
461 if(op.type().id() == ID_pointer)
469 pointer_base_type.
id() != ID_empty,
470 "no pointer arithmetic over void pointers");
479 "there should be exactly one pointer-type operand in a pointer-type sum");
484 for(
const auto &operand : plus_expr.
operands())
486 if(operand.type().id() == ID_pointer)
490 operand.type().id() != ID_unsignedbv &&
491 operand.type().id() != ID_signedbv)
510 else if(expr.
id()==ID_minus)
517 minus_expr.
lhs().
type().
id() == ID_pointer,
518 "first operand should be of pointer type");
521 minus_expr.
rhs().
type().
id() != ID_unsignedbv &&
522 minus_expr.
rhs().
type().
id() != ID_signedbv)
531 typet pointer_base_type =
534 pointer_base_type.
id() != ID_empty,
535 "no pointer arithmetic over void pointers");
537 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
540 else if(expr.
id()==ID_byte_extract_little_endian ||
541 expr.
id()==ID_byte_extract_big_endian)
546 expr.
id() == ID_byte_update_little_endian ||
547 expr.
id() == ID_byte_update_big_endian)
551 else if(expr.
id() == ID_field_address)
554 const typet &compound_type =
ns.
follow(field_address_expr.compound_type());
559 if(compound_type.
id() == ID_struct)
568 else if(compound_type.
id() == ID_union)
574 INVARIANT(
false,
"field address expressions operate on struct or union");
579 else if(expr.
id() == ID_element_address)
592 element_address_expr.type(), bv, *size, element_address_expr.index());
602 if(expr.
id() != ID_minus)
607 return minus_expr.lhs().type().id() == ID_pointer &&
608 minus_expr.rhs().type().id() == ID_pointer;
613 if(expr.
type().
id()==ID_pointer)
635 const bvt lhs_offset =
640 const bvt rhs_offset =
647 "no pointer arithmetic over void pointers");
649 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
651 if(*element_size_opt != 1)
666 const bvt object_size_bv =
696 expr.
id() == ID_pointer_offset &&
710 const auto object_size = expr_try_dynamic_cast<object_size_exprt>(expr))
723 expr.
id() == ID_pointer_object &&
737 expr.
id() == ID_typecast &&
756 for(
const auto &literal : bv)
769 result = ch + result;
778 std::size_t offset)
const
782 if(type.
id() != ID_pointer)
787 bvt value_bv(bv.begin() + offset, bv.begin() + offset + bits);
791 std::string value_offset =
798 return value[value.size() - 1 - i] ==
'1';
906 const std::size_t max_objects=std::size_t(1)<<object_bits;
910 "too many addressed objects: maximum number of objects is set to 2^n=" +
913 "use the `--object-bits n` option to increase the maximum number");
919 std::vector<symbol_exprt> &placeholders)
const
924 std::size_t number = 0;
927 dynamic_objects_ops.reserve(objects.size());
928 not_dynamic_objects_ops.reserve(objects.size());
930 for(
auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
932 const exprt &expr = *it;
939 conjuncts.reserve(bv.size());
940 placeholders.reserve(bv.size());
941 for(std::size_t i = 0; i < bv.size(); ++i)
943 if(placeholders.size() <= i)
948 conjuncts.emplace_back(placeholders[i]);
950 conjuncts.emplace_back(
not_exprt{placeholders[i]});
954 dynamic_objects_ops.push_back(
conjunction(conjuncts));
956 not_dynamic_objects_ops.push_back(
conjunction(conjuncts));
964 bddt not_dyn_bdd = bdd_converter.
from_expr(not_dynamic_objects);
966 return {bdd_converter.
as_expr(dyn_bdd), bdd_converter.
as_expr(not_dyn_bdd)};
969 std::unordered_map<exprt, exprt, irep_hash>
971 std::vector<symbol_exprt> &placeholders)
const
976 std::size_t number = 0;
978 std::unordered_map<exprt, exprt::operandst, irep_hash> per_size_object_ops;
980 for(
auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
982 const exprt &expr = *it;
984 if(expr.
id() != ID_symbol && expr.
id() != ID_string_constant)
988 if(!size_expr.has_value())
996 conjuncts.reserve(bv.size());
997 placeholders.reserve(bv.size());
998 for(std::size_t i = 0; i < bv.size(); ++i)
1000 if(placeholders.size() <= i)
1005 conjuncts.emplace_back(placeholders[i]);
1007 conjuncts.emplace_back(
not_exprt{placeholders[i]});
1010 per_size_object_ops[size_expr.value()].push_back(
conjunction(conjuncts));
1013 std::unordered_map<exprt, exprt, irep_hash> result;
1014 for(
const auto &size_entry : per_size_object_ops)
1020 result.emplace(size_entry.first, bdd_converter.
as_expr(bdd));
1034 std::vector<symbol_exprt> is_dynamic_placeholders;
1036 std::unordered_map<exprt, exprt, irep_hash> object_sizes;
1037 std::vector<symbol_exprt> object_size_placeholders;
1041 if(postponed.expr.id() == ID_is_dynamic_object)
1043 if(is_dynamic_expr.first.is_nil())
1050 POSTCONDITION(saved_bv.size() == is_dynamic_placeholders.size());
1052 for(std::size_t i = 0; i < saved_bv.size(); ++i)
1054 replacements.emplace(
1057 exprt is_dyn = is_dynamic_expr.first;
1059 exprt is_not_dyn = is_dynamic_expr.second;
1069 const auto postponed_object_size =
1070 expr_try_dynamic_cast<object_size_exprt>(postponed.expr))
1072 if(object_sizes.empty())
1076 if(object_size_placeholders.empty())
1082 POSTCONDITION(saved_bv.size() == object_size_placeholders.size());
1084 for(std::size_t i = 0; i < saved_bv.size(); ++i)
1086 replacements.emplace(
1090 for(
const auto &object_size_entry : object_sizes)
1093 object_size_entry.first, postponed_object_size->type());
1097 exprt all_objects_this_size = object_size_entry.second;
1103 for(std::size_t i = 0; i < postponed.bv.size(); ++i)
1109 #define COMPACT_OBJECT_SIZE_EQ
1110 #ifndef COMPACT_OBJECT_SIZE_EQ
1115 for(std::size_t i = 0; i < postponed.bv.size(); ++i)
1117 prop.
lcnf({!l1, !postponed.bv[i], size_bv[i]});
1118 prop.
lcnf({!l1, postponed.bv[i], !size_bv[i]});
Conversion between exprt and miniBDD.
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...
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
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
virtual std::optional< std::size_t > get_width_opt(const typet &type) 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...
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 &)
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 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)
bvt sub(const bvt &op0, const bvt &op1)
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
bvt multiplier(const bvt &op0, const bvt &op1, representationt rep)
static bvt extension(const bvt &bv, std::size_t new_size, representationt rep)
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
struct configt::bv_encodingt bv_encoding
A constant literal expression.
const irep_idt & get_value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Maps a big-endian offset to a little-endian offset.
virtual void build_big_endian(const typet &type)
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.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
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
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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
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)
const mp_integer & get_null_object() const
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 ...
const typet & base_type() const
The type of the data what we point to.
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
void l_set_to_true(literalt a)
virtual literalt land(literalt a, literalt b)=0
virtual literalt limplies(literalt a, literalt b)=0
void lcnf(literalt l0, literalt l1)
virtual void set_equal(literalt a, literalt b)
asserts a==b in the propositional formula
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 literalt lor(literalt a, literalt b)=0
virtual tvt l_get(literalt a) const =0
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 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.
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 pointer_offset_exprt & to_pointer_offset_expr(const exprt &expr)
Cast an exprt to a pointer_offset_exprt.
const field_address_exprt & to_field_address_expr(const exprt &expr)
Cast an exprt to an field_address_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const pointer_object_exprt & to_pointer_object_expr(const exprt &expr)
Cast an exprt to a pointer_object_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 element_address_exprt & to_element_address_expr(const exprt &expr)
Cast an exprt to an element_address_exprt.
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)
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.
exprt object_size(const exprt &pointer)
exprt same_object(const exprt &p1, const exprt &p2)
exprt null_object(const exprt &pointer)
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
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 POSTCONDITION(CONDITION)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_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 typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const minus_exprt & to_minus_expr(const exprt &expr)
Cast an exprt to a minus_exprt.
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
bool is_constant(const typet &type)
This method tests, if the given typet is a constant.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.