43 out << itr->first <<
":" << itr->second;
50 for(rw_range_sett::objectst::iterator it=
r_range_set.begin();
55 for(rw_range_sett::objectst::iterator it=
w_range_set.begin();
64 for(
const auto &read_object_entry :
get_r_set())
66 out <<
" " << read_object_entry.first;
67 read_object_entry.second->output(
ns, out);
74 for(
const auto &written_object_entry :
get_w_set())
76 out <<
" " << written_object_entry.first;
77 written_object_entry.second->output(
ns, out);
153 auto index = numeric_cast<mp_integer>(simp_offset);
155 range_start.
is_unknown() || !index.has_value() ||
156 !object_size_bits_opt.has_value())
163 if(*index >= *object_size_bits_opt)
168 be.
id()==ID_byte_extract_little_endian,
174 map.
map_bit(numeric_cast_v<std::size_t>(*index)));
200 const auto dist = numeric_cast<mp_integer>(simp_distance);
218 if(shift.
id()==ID_ashr || shift.
id()==ID_lshr)
221 sh_range_start+=dist_r;
223 range_spect sh_size=std::min(size, src_size-sh_range_start);
225 if(sh_range_start >=
range_spect{0} && sh_range_start < src_size)
228 if(src_size >= dist_r)
230 range_spect sh_size=std::min(size, src_size-dist_r);
246 type.
id() == ID_union || type.
id() == ID_union_tag ||
262 if(offset_bits.has_value())
265 offset += range_start;
277 if(expr.
array().
id() == ID_null_object)
283 if(type.
id()==ID_vector)
289 if(subtype_bits.has_value())
292 else if(type.
id()==ID_array)
298 if(subtype_bits.has_value())
306 const auto index = numeric_cast<mp_integer>(simp_index);
307 if(!index.has_value())
332 if(!subtype_bits.has_value())
334 for(
const auto &op : expr.
operands())
350 for(
const auto &op : expr.
operands())
352 if(full_r_s<=offset+sub_size && full_r_e>offset)
355 full_r_s <= offset ?
range_spect{0} : full_r_s - offset;
357 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
373 expr.
type().
id() == ID_struct
390 for(
const auto &op : expr.
operands())
404 if(full_r_e.
is_unknown() || full_r_e > offset)
407 full_r_s <= offset ?
range_spect{0} : full_r_s - offset;
416 if(full_r_s<=offset+sub_size)
419 full_r_s <= offset ?
range_spect{0} : full_r_s - offset;
426 else if(full_r_s<=offset+sub_size && full_r_e>offset)
429 full_r_s <= offset ?
range_spect{0} : full_r_s - offset;
431 full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
458 if(new_size<=range_start)
461 new_size-=range_start;
462 new_size=std::min(size, new_size);
471 object.
id() == ID_string_constant ||
object.
id() == ID_label ||
472 object.
id() == ID_array ||
object.
id() == ID_null_object ||
473 object.
id() == ID_symbol)
478 else if(
object.
id()==ID_dereference)
482 else if(
object.
id()==ID_index)
489 else if(
object.
id()==ID_member)
495 else if(
object.
id()==ID_if)
503 else if(
object.
id()==ID_byte_extract_little_endian ||
504 object.
id()==ID_byte_extract_big_endian)
510 else if(
object.
id()==ID_typecast)
517 throw "rw_range_sett: address_of '" +
object.id_string() +
"' not handled";
526 objectst::iterator entry=
529 std::pair<
const irep_idt &, std::unique_ptr<range_domain_baset>>(
530 identifier,
nullptr))
533 if(entry->second==
nullptr)
534 entry->second = std::make_unique<range_domaint>();
537 {range_start, range_end});
546 if(expr.
id() == ID_complex_real)
549 else if(expr.
id() == ID_complex_imag)
552 else if(expr.
id()==ID_typecast)
558 else if(expr.
id()==ID_if)
560 else if(expr.
id()==ID_dereference)
566 else if(expr.
id()==ID_byte_extract_little_endian ||
567 expr.
id()==ID_byte_extract_big_endian)
573 else if(expr.
id()==ID_shl ||
574 expr.
id()==ID_ashr ||
577 else if(expr.
id()==ID_member)
579 else if(expr.
id()==ID_index)
581 else if(expr.
id()==ID_array)
583 else if(expr.
id()==ID_struct)
585 else if(expr.
id()==ID_symbol)
600 range_start >= full_size)))
610 if(!size.is_unknown() && !full_size.
is_unknown())
611 range_end=std::min(range_end, full_size);
613 add(mode, identifier, range_start, range_end);
625 for(
const auto &op : expr.
operands())
628 else if(expr.
id() == ID_null_object ||
629 expr.
id() == ID_string_constant)
635 for(
const auto &op : expr.
operands())
639 throw "rw_range_sett: assignment to '" + expr.
id_string() +
"' not handled";
656 if(type.
id()==ID_array)
668 const exprt &pointer)
695 if(type_bits.has_value())
699 if(range_start.
is_unknown() || new_size <= range_start)
703 new_size -= range_start;
704 new_size = std::min(size, new_size);
710 if(
object.is_not_nil() && !
has_subexpr(
object, ID_dereference))
715 const namespacet &ns, std::ostream &out)
const
724 out << itr->first <<
":" << itr->second.first;
754 guard = std::move(copy);
764 objectst::iterator entry=
767 std::pair<
const irep_idt &, std::unique_ptr<range_domain_baset>>(
768 identifier,
nullptr))
771 if(entry->second==
nullptr)
772 entry->second = std::make_unique<guarded_range_domaint>();
798 if(statement == ID_printf)
801 for(
const auto &op : code.
operands())
807 else if(statement == ID_array_equal)
819 else if(statement == ID_array_set)
827 else if(statement == ID_array_copy || statement == ID_array_replace)
835 else if(statement == ID_havoc_object)
849 const exprt &function_expr,
860 for(
const auto &argument : arguments)
872 switch(target->type())
892 goto_rw_other(
function, target, target->get_other(), rw_set);
909 function, target, target->assign_lhs(), target->assign_rhs(), rw_set);
918 rw_set.
get_objects_rec(
function, target, target->decl_symbol().type());
928 target->call_function(),
929 target->call_arguments(),
941 goto_rw(
function, i_it, rw_set);
948 goto_functionst::function_mapt::const_iterator f_it=
955 goto_rw(f_it->first, body, rw_set);
API to expression classes for bitvectors.
const shift_exprt & to_shift_expr(const exprt &expr)
Cast an exprt to a shift_exprt.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Operator to return the address of an object.
Array constructor from list of elements.
const array_typet & type() const
const typet & element_type() const
The type of the elements of the array.
const exprt & size() const
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
Imaginary part of the expression describing a complex number.
Real part of the expression describing a complex number.
Operator to dereference a pointer.
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.
size_t map_bit(size_t bit) const
Base class for all expressions.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
void add(const exprt &expr)
virtual void output(const namespacet &ns, std::ostream &out) const override
sub_typet::const_iterator const_iterator
The trinary if-then-else operator.
const std::string & id_string() const
const irep_idt & id() const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Split an expression into a base object and a (byte) offset.
void build(const exprt &expr, const namespacet &ns)
Given an expression expr, attempt to find the underlying object it represents by skipping over type c...
static const exprt & root_object(const exprt &expr)
virtual ~range_domain_baset()
void output(const namespacet &ns, std::ostream &out) const override
sub_typet::const_iterator const_iterator
Data type to describe upper and lower bounds of the range of bits that a read or write access may aff...
static range_spect unknown()
static range_spect to_range_spect(const mp_integer &size)
void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size) override
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end) override
void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size) override
goto_programt::const_targett target
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
void output(std::ostream &out) const
virtual void get_objects_dereference(get_modet mode, const dereference_exprt &deref, const range_spect &range_start, const range_spect &size)
virtual void get_objects_complex_real(get_modet mode, const complex_real_exprt &expr, const range_spect &range_start, const range_spect &size)
message_handlert & message_handler
const objectst & get_r_set() const
virtual void get_objects_shift(get_modet mode, const shift_exprt &shift, const range_spect &range_start, const range_spect &size)
virtual void get_objects_index(get_modet mode, const index_exprt &expr, const range_spect &range_start, const range_spect &size)
virtual void get_objects_struct(get_modet mode, const struct_exprt &expr, const range_spect &range_start, const range_spect &size)
virtual void get_objects_complex_imag(get_modet mode, const complex_imag_exprt &expr, const range_spect &range_start, const range_spect &size)
virtual void get_objects_if(get_modet mode, const if_exprt &if_expr, const range_spect &range_start, const range_spect &size)
virtual void get_objects_address_of(const exprt &object)
virtual void get_array_objects(const irep_idt &, goto_programt::const_targett, get_modet, const exprt &)
virtual void get_objects_byte_extract(get_modet mode, const byte_extract_exprt &be, const range_spect &range_start, const range_spect &size)
virtual void get_objects_rec(const irep_idt &, goto_programt::const_targett, get_modet mode, const exprt &expr)
virtual void get_objects_member(get_modet mode, const member_exprt &expr, const range_spect &range_start, const range_spect &size)
const objectst & get_w_set() const
virtual void add(get_modet mode, const irep_idt &identifier, const range_spect &range_start, const range_spect &range_end)
virtual void get_objects_typecast(get_modet mode, const typecast_exprt &tc, const range_spect &range_start, const range_spect &size)
virtual void get_objects_array(get_modet mode, const array_exprt &expr, const range_spect &range_start, const range_spect &size)
A base class for shift and rotate operators.
Struct constructor from list of elements.
Structure type, corresponds to C style structs.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
const typet & subtype() const
Semantic type conversion.
The type of an expression, extends irept.
const typet & element_type() const
The type of the elements of the vector.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
Goto Programs with Functions.
#define forall_goto_program_instructions(it, program)
void dereference(const irep_idt &function_id, goto_programt::const_targett target, exprt &expr, const namespacet &ns, value_setst &value_sets, message_handlert &message_handler)
Remove dereferences in expr using value_sets to determine to what objects the pointers may be pointin...
static void goto_rw_assign(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &rhs, rw_range_sett &rw_set)
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
static void goto_rw_other(const irep_idt &function, goto_programt::const_targett target, const codet &code, rw_range_sett &rw_set)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
API to expression classes for Pointers.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
std::optional< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
std::optional< mp_integer > member_offset_bits(const struct_typet &type, const irep_idt &member, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const struct_exprt & to_struct_expr(const exprt &expr)
Cast an exprt to a struct_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const vector_typet & to_vector_type(const typet &type)
Cast a typet to a vector_typet.
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.
const complex_typet & to_complex_type(const typet &type)
Cast a typet to a complex_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.