Go to the documentation of this file.
34 build(type, little_endian);
51 const std::size_t new_size =
map.size() + width;
52 map.reserve(new_size);
54 for(std::size_t i =
map.size(); i < new_size; ++i)
60 if(src.
id() == ID_pointer)
75 if(type.
id() != ID_pointer)
79 std::pair<cachet::iterator, bool> cache_result =
80 cache.insert(std::pair<typet, entryt>(type,
entryt()));
82 if(cache_result.second)
84 std::size_t &total_width = cache_result.first->second.total_width;
87 DATA_INVARIANT(total_width > 0,
"pointer width shall be greater than zero");
90 return cache_result.first->second.total_width;
104 const std::size_t pointer_width = type.
get_width();
105 const std::size_t object_width = get_object_width(type);
107 return pointer_width - object_width;
122 if(expr.
id() == ID_is_invalid_pointer)
124 if(operands.size()==1 &&
125 operands[0].type().id()==ID_pointer)
137 const std::size_t object_bits =
140 bvt equal_invalid_bv;
141 equal_invalid_bv.reserve(object_bits);
143 for(std::size_t i=0; i<object_bits; i++)
145 equal_invalid_bv.push_back(
prop.
lequal(object_bv[i], invalid_bv[i]));
152 else if(expr.
id() == ID_is_dynamic_object)
154 if(operands.size()==1 &&
155 operands[0].type().id()==ID_pointer)
168 else if(expr.
id()==ID_lt || expr.
id()==ID_le ||
169 expr.
id()==ID_gt || expr.
id()==ID_ge)
171 if(operands.size()==2 &&
172 operands[0].type().id()==ID_pointer &&
173 operands[1].type().id()==ID_pointer)
199 if(expr.
id()==ID_symbol)
203 else if(expr.
id()==ID_label)
207 else if(expr.
id() == ID_null_object)
212 else if(expr.
id()==ID_index)
225 if(array_type.
id()==ID_pointer)
231 else if(array_type.
id()==ID_array ||
232 array_type.
id()==ID_string_constant)
235 if(!bv_opt.has_value())
237 bv = std::move(*bv_opt);
250 return std::move(bv);
252 else if(expr.
id()==ID_byte_extract_little_endian ||
253 expr.
id()==ID_byte_extract_big_endian)
259 if(!bv_opt.has_value())
268 return std::move(bv);
270 else if(expr.
id()==ID_member)
278 if(!bv_opt.has_value())
281 bvt bv = std::move(*bv_opt);
282 if(struct_op_type.
id()==ID_struct)
295 struct_op_type.
id() == ID_union,
296 "member expression should operate on struct or union");
300 return std::move(bv);
302 else if(expr.
id()==ID_constant ||
303 expr.
id()==ID_string_constant ||
308 else if(expr.
id()==ID_if)
317 if(!bv1_opt.has_value())
321 if(!bv2_opt.has_value())
336 if(expr.
id()==ID_symbol)
342 else if(expr.
id()==ID_nondet_symbol)
347 for(
auto &literal : bv)
352 else if(expr.
id()==ID_typecast)
356 const exprt &op = typecast_expr.
op();
359 if(op_type.
id()==ID_pointer)
363 op_type.
id() == ID_c_enum || op_type.
id() == ID_c_enum_tag)
373 else if(expr.
id()==ID_if)
377 else if(expr.
id()==ID_index)
381 else if(expr.
id()==ID_member)
385 else if(expr.
id()==ID_address_of)
390 if(!bv_opt.has_value())
401 else if(expr.
id()==ID_constant)
413 else if(expr.
id()==ID_plus)
426 if(it->type().id()==ID_pointer)
434 if(pointer_sub_type.
id()==ID_empty)
451 "there should be exactly one pointer-type operand in a pointer-type sum");
457 if(it->type().id()==ID_pointer)
460 if(it->type().id()!=ID_unsignedbv &&
461 it->type().id()!=ID_signedbv)
479 else if(op.size()<bits)
487 else if(expr.
id()==ID_minus)
494 minus_expr.
lhs().
type().
id() == ID_pointer,
495 "first operand should be of pointer type");
498 minus_expr.
rhs().
type().
id() != ID_unsignedbv &&
499 minus_expr.
rhs().
type().
id() != ID_signedbv)
513 if(pointer_sub_type.
id()==ID_empty)
522 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
523 element_size = *element_size_opt;
528 else if(expr.
id()==ID_byte_extract_little_endian ||
529 expr.
id()==ID_byte_extract_big_endian)
543 if(expr.
id() != ID_minus)
548 return minus_expr.lhs().type().id() == ID_pointer &&
549 minus_expr.rhs().type().id() == ID_pointer;
554 if(expr.
type().
id()==ID_pointer)
576 const bvt object_size_bv =
582 for(std::size_t i = 0; i < width; ++i)
589 const bvt lhs_offset =
602 const bvt rhs_offset =
621 CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
623 if(*element_size_opt != 1)
625 bvt element_size_bv =
640 expr.
id() == ID_pointer_offset &&
657 expr.
id() == ID_object_size &&
666 for(std::size_t i=0; i<width; i++)
678 expr.
id() == ID_pointer_object &&
694 expr.
id() == ID_typecast &&
717 for(
const auto &literal : bv)
730 result = ch + result;
740 const typet &type)
const
742 if(type.
id() != ID_pointer)
747 bvt value_bv(bv.begin() + offset, bv.begin() + offset + bits);
751 std::string value_offset =
758 return value[value.size() - 1 - i] ==
'1';
771 return std::move(result);
783 object.reserve(object_bits);
784 for(std::size_t i=0; i<object_bits; i++)
785 object.push_back(
const_literal((addr & (std::size_t(1) << i)) != 0));
856 const std::size_t max_objects=std::size_t(1)<<object_bits;
860 "too many addressed objects: maximum number of objects is set to 2^n=" +
863 "use the `--object-bits n` option to increase the maximum number");
871 if(postponed.
expr.
id() == ID_is_dynamic_object)
876 std::size_t number=0;
878 for(
auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
880 const exprt &expr=*it;
902 else if(postponed.
expr.
id()==ID_object_size)
907 std::size_t number=0;
909 for(
auto it = objects.cbegin(); it != objects.cend(); ++it, ++number)
911 const exprt &expr=*it;
913 if(expr.
id() != ID_symbol && expr.
id() != ID_string_constant)
918 if(!size_expr.has_value())
922 size_expr.value(), postponed.
expr.
type());
951 for(postponed_listt::const_iterator
void build_big_endian(const typet &type) override
#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.
bv_pointerst(const namespacet &_ns, propt &_prop, message_handlert &message_handler, bool get_array_constraints=false)
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.
std::size_t operator()(const typet &type) const override
const typet & subtype() const
virtual bvt convert_member(const member_exprt &expr)
bv_endianness_mapt(const typet &type, bool little_endian, const namespacet &_ns, const boolbv_widtht &_boolbv_width)
void build(const typet &type, bool little_endian)
const boolbv_widtht & boolbv_width
virtual bvt convert_byte_update(const byte_update_exprt &expr)
struct configt::bv_encodingt bv_encoding
exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset, const typet &type) const override
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.
bvt signed_multiplier(const bvt &op0, const bvt &op1)
Map bytes according to the configured endianness.
std::size_t boolbv_width(const typet &type) const override
postponed_listt postponed_list
The trinary if-then-else operator.
Various predicates over pointers in programs.
const bvt & get_literals(const irep_idt &identifier, const typet &type, std::size_t width)
std::size_t add_object(const exprt &expr)
virtual exprt bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset, const typet &type) const
bvt sign_extension(const bvt &bv, std::size_t new_size)
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...
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)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
virtual bvt convert_pointer_type(const exprt &expr)
virtual void build_big_endian(const typet &type)
virtual literalt land(literalt a, literalt b)=0
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.
bool is_false(const literalt &l)
std::size_t get_address_width(const pointer_typet &type) const
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.
virtual bvt convert_byte_extract(const byte_extract_exprt &expr)
bvt add(const bvt &op0, const bvt &op1)
virtual std::size_t operator()(const typet &type) const
std::vector< size_t > map
void conversion_failed(const exprt &expr, bvt &bv)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
virtual literalt limplies(literalt a, literalt b)=0
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)
std::size_t get_object_width(const pointer_typet &type) const
const plus_exprt & to_plus_expr(const exprt &expr)
Cast an exprt to a plus_exprt.
API to expression classes for Pointers.
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.
NODISCARD bvt offset_arithmetic(const pointer_typet &type, const bvt &bv, const mp_integer &x)
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.
nonstd::optional< T > optionalt
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
numberingt< exprt, irep_hash > objects
std::size_t get_width() const
std::size_t get_offset_width(const pointer_typet &type) const
Extract member of struct or union.
static 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)
virtual NODISCARD bvt add_addr(const exprt &expr)
void build_little_endian(const typet &type) override
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.
NODISCARD optionalt< bvt > convert_address_of_rec(const exprt &expr)
static literalt sign_bit(const bvt &op)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
static 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
static std::string bits_to_string(const propt &prop, const bvt &bv)
exprt same_object(const exprt &p1, const exprt &p2)
bvt divider(const bvt &op0, const bvt &op1, representationt rep)
bv_pointers_widtht bv_pointers_width
Maps a big-endian offset to a little-endian offset.
std::size_t get_invalid_object() const
endianness_mapt endianness_map(const typet &type, bool little_endian) const override
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
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_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...
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Semantic type conversion.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
tv_enumt get_value() const
literalt convert_rest(const exprt &expr) override
bool get_array_constraints
A constant literal expression.
literalt convert_rest(const exprt &expr) override
void post_process() override
static bool is_pointer_subtraction(const exprt &expr)
message_handlert & message_handler
const irep_idt & get_value() const
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
static bvt object_offset_encoding(const bvt &object, const bvt &offset)
Construct a pointer encoding from given encodings of object and offset.
bool can_cast_type< bitvector_typet >(const typet &type)
Check whether a reference to a typet is a bitvector_typet.
API to expression classes for bitvectors.
bvt zero_extension(const bvt &bv, std::size_t new_size)
NODISCARD bvt encode(std::size_t object, const pointer_typet &type) const
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.