47 id==
"value_set::return_value" ||
48 id==
"value_set::memory")
58 return !found.has_value() ?
nullptr : &(found->get());
105 auto entry=
dest.read().find(
n);
107 if(entry==
dest.read().end())
112 else if(!entry->second)
114 else if(offset && *entry->second == *offset)
145 display_name = id2string(e.identifier) + e.suffix;
148 else if(e.
identifier ==
"value_set::return_value")
150 display_name =
"RETURN_VALUE" + e.suffix;
156 const symbolt &symbol=ns.lookup(e.identifier);
157 display_name=id2string(symbol.display_name())+e.suffix;
158 identifier=symbol.name;
160 identifier = id2string(e.identifier);
161 display_name = id2string(identifier) + e.suffix;
165 out << indent << display_name <<
" = { ";
169 std::size_t width = 0;
171 for(object_map_dt::const_iterator
o_it = object_map.begin();
172 o_it != object_map.end();
177 std::ostringstream
stream;
198 const std::string result =
stream.str();
200 width += result.size();
202 object_map_dt::const_iterator next(
o_it);
205 if(next != object_map.end())
209 out <<
"\n" << std::string(indent.size(),
' ') <<
" ";
232 od.type()=
od.object().type();
234 return std::move(
od);
291 for(object_map_dt::const_iterator it=src.
read().begin();
292 it!=src.
read().end();
317 for(object_map_dt::const_iterator
318 it=object_map.begin();
319 it!=object_map.end();
358 .map([&](
const object_map_dt::value_type &
pair) {
return to_expr(
pair); });
378 const std::string &suffix,
const std::string &
field)
383 suffix.compare(1,
field.length(),
field) == 0 &&
384 (suffix.length() ==
field.length() + 1 ||
385 suffix[
field.length() + 1] ==
'.' ||
386 suffix[
field.length() + 1] ==
'[');
390 const std::string &suffix,
const std::string &
field)
394 "suffix should start with " +
field);
395 return suffix.substr(
field.length() + 1);
401 const std::string &suffix,
417 return std::move(index);
440 return std::move(index);
447 return std::move(identifier);
455 const std::string &suffix,
460 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
format(expr) <<
"\n";
461 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
475 type.
id() ==
ID_array,
"operand 0 of index expression must be an array");
486 "compound of member expression must be struct or union");
488 const std::string &component_name=
494 "." + component_name + suffix,
544 if(object_map.begin()==object_map.end())
548 for(object_map_dt::const_iterator
549 it1=object_map.begin();
550 it1!=object_map.end();
604 if(
tmp.read().empty())
609 else if(
tmp.read().size()==1 &&
618 dest.write().insert(
tmp.read().begin(),
tmp.read().end());
632 throw expr.
id_string()+
" expected to have at least two operands";
644 for(
const auto &op : expr.
operands())
659 if(!offset.has_value())
681 if(!size.has_value() || (*size) == 0)
693 "unexpected subtraction of pointer from integer");
715 for(object_map_dt::const_iterator
723 if(offset &&
i.has_value())
737 throw expr.
id_string()+
" expected to have at least two operands";
748 for(object_map_dt::const_iterator
768 throw "unexpected function_call sideeffect";
804 "struct expression should have an operand per component");
812 const std::string &component_name =
919 const std::string prefix=
920 "value_set::dynamic_object"+
924 const std::string full_name=prefix+suffix;
1035 std::cout <<
"GET_VALUE_SET_REC RESULT:\n";
1036 for(
const auto &
obj :
dest.read())
1039 std::cout <<
" " <<
format(e) <<
"\n";
1068 for(object_map_dt::const_iterator
1069 it=object_map.
read().begin();
1070 it!=object_map.
read().end();
1081 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
format(expr)
1118 throw "index expected to have two operands";
1125 array.
type().
id() ==
ID_array,
"index takes array-typed operand");
1134 for(object_map_dt::const_iterator
1135 a_it=object_map.begin();
1136 a_it!=object_map.end();
1155 else if(
i.has_value() && o)
1159 if(!size.has_value() || *size == 0)
1184 for(object_map_dt::const_iterator
1185 it=object_map.begin();
1186 it!=object_map.end();
1241 std::cout <<
"ASSIGN LHS: " <<
format(lhs) <<
" : "
1243 std::cout <<
"ASSIGN RHS: " <<
format(rhs) <<
" : "
1245 std::cout <<
"--------------------------------------------\n";
1255 const typet &subtype =
c.type();
1259 if(subtype.
id() ==
ID_code ||
c.get_is_padding())
1278 "value_sett::assign types should match, got: "
1313 "value_sett::assign types should match, got: "
1374 const std::string &suffix,
1379 std::cout <<
"ASSIGN_REC LHS: " <<
format(lhs) <<
'\n';
1380 std::cout <<
"ASSIGN_REC LHS ID: " << lhs.
id() <<
'\n';
1381 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1383 for(object_map_dt::const_iterator it=
values_rhs.read().begin();
1386 std::cout <<
"ASSIGN_REC RHS: " <<
1403 const std::string name=
1404 "value_set::dynamic_object"+
1412 throw lhs.
id_string()+
" expected to have one operand";
1420 for(object_map_dt::const_iterator
1437 const typet &type = array.type();
1440 type.
id() ==
ID_array,
"operand 0 of index expression must be an array");
1453 "operand 0 of member expression must be struct or union");
1458 "." +
id2string(component_name) + suffix,
1462 else if(lhs.
id()==
"valid_object" ||
1463 lhs.
id()==
"dynamic_type" ||
1464 lhs.
id()==
"is_zero_string" ||
1465 lhs.
id()==
"zero_string" ||
1466 lhs.
id()==
"zero_string_length")
1496 throw "assign NYI: '" + lhs.
id_string() +
"'";
1514 for(std::size_t
i=0;
i<arguments.size();
i++)
1516 const std::string identifier=
"value_set::dummy_arg_"+std::to_string(
i);
1525 for(code_typet::parameterst::const_iterator
1530 const irep_idt &identifier=it->get_identifier();
1531 if(identifier.
empty())
1535 symbol_exprt(
"value_set::dummy_arg_"+std::to_string(
i), it->type());
1554 assign(lhs, rhs, ns,
false,
false);
1576 throw "assignment expected to have two operands";
1583 throw "decl expected to have one operand";
1588 throw "decl expected to have symbol on lhs";
1611 else if(statement==
"cpp_delete" ||
1612 statement==
"cpp_delete[]")
1616 else if(statement==
"lock" || statement==
"unlock")
1620 else if(statement==
ID_asm)
1637 "value_set::return_value",
code_return.return_value().type());
1673 throw "value_sett: unexpected statement: "+
id2string(statement);
1722 for(
auto &
key_value : entry->object_map.read())
1733 "value_sett::erase_value_from_entry() should erase exactly one value for "
1734 "each element in the set it is given");
1751 const typet &subtype =
c.type();
1755 if(subtype.
id() ==
ID_code ||
c.get_is_padding())
optionalt< symbol_exprt > get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
void base_type(typet &type, const namespacet &ns)
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)
unsignedbv_typet unsigned_char_type()
bitvector_typet char_type()
bitvector_typet c_index_type()
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
const typet & element_type() const
The type of the elements of the array.
codet representation of a "return from a function" statement.
std::vector< parametert > parameterst
const parameterst & parameters() const
Data structure for representing an arbitrary statement in a program.
const irep_idt & get_statement() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Representation of heap-allocated objects.
Base class for all expressions.
std::vector< exprt > operandst
bool is_zero() const
Return whether the expression is a constant representing 0.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irept & find(const irep_idt &name) const
const irep_idt & get(const irep_idt &name) const
const std::string & id_string() const
const irep_idt & id() const
const std::string & get_string(const irep_idt &name) const
Extract member of struct or union.
const exprt & compound() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
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...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Split an expression into a base object and a (byte) offset.
void insert(const key_type &k, valueU &&m)
Insert element, element must not exist in map.
void iterate(std::function< void(const key_type &k, const mapped_type &m)> f) const
Call a function for every key-value pair in the map.
void erase(const key_type &k)
Erase element, element must exist in map.
bool has_key(const key_type &k) const
Check if key is in map.
void replace(const key_type &k, valueU &&m)
Replace element, element must exist in map.
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
optionalt< std::reference_wrapper< const mapped_type > > find(const key_type &k) const
Find element.
void update(const key_type &k, std::function< void(mapped_type &)> mutator)
Update an element in place; element must exist in map.
const irep_idt & get_statement() const
Structure type, corresponds to C style structs.
Base type for structs and unions.
const componentst & components() const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
typet type
Type of symbol.
The Boolean constant true.
Semantic type conversion.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
std::list< exprt > valuest
State type in value_set_domaint, used in value-set analysis and goto-symex.
virtual void apply_code_rec(const codet &code, const namespacet &ns)
Subclass customisation point for applying code to this domain:
optionalt< irep_idt > get_index_of_symbol(irep_idt identifier, const typet &type, const std::string &suffix, const namespacet &ns) const
Get the index of the symbol and suffix.
bool eval_pointer_offset(exprt &expr, const namespacet &ns) const
Tries to resolve any pointer_offset_exprt expressions in expr to constant integers using this value-s...
const entryt * find_entry(const irep_idt &id) const
Finds an entry in this value-set.
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
void output(std::ostream &out, const std::string &indent="") const
Pretty-print this value-set.
void dereference_rec(const exprt &src, exprt &dest) const
Sets dest to src with any wrapping typecasts removed.
void erase_symbol(const symbol_exprt &symbol_expr, const namespacet &ns)
valuest values
Stores the LHS ID -> RHS expression set map.
unsigned location_number
Matches the location_number field of the instruction that corresponds to this value_sett instance in ...
static object_numberingt object_numbering
Global shared object numbering, used to abbreviate expressions stored in value sets.
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
Merges an existing element into an object map.
void erase_struct_union_symbol(const struct_union_typet &struct_union_type, const std::string &erase_prefix, const namespacet &ns)
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See get_reference_set.
exprt to_expr(const object_map_dt::value_type &it) const
Converts an object_map_dt element object_number -> offset into an object_descriptor_exprt with ....
void erase_values_from_entry(const irep_idt &index, const std::unordered_set< exprt, irep_hash > &values_to_erase)
Update the entry stored at index by erasing any values listed in values_to_erase.
void update_entry(const entryt &e, const typet &type, const object_mapt &new_values, bool add_to_sets)
Adds or replaces an entry in this value-set.
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Transforms this value-set by executing executing the assignment lhs := rhs against it.
virtual void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
Subclass customisation point for recursion over LHS expression:
insert_actiont get_insert_action(const object_mapt &dest, object_numberingt::number_type n, const offsett &offset) const
Determines what would happen if object number n was inserted into map dest with offset offset – the p...
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
virtual bool field_sensitive(const irep_idt &id, const typet &type)
Determines whether an identifier of a given type should have its fields distinguished.
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
void guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
bool make_union_would_change(const object_mapt &dest, const object_mapt &src) const
Determines whether merging two RHS expression sets would cause any change.
void do_end_function(const exprt &lhs, const namespacet &ns)
Transforms this value-set by assigning this function's return value to a given LHS expression.
static const object_map_dt empty_object_map
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Transforms this value-set by executing the actual -> formal parameter assignments for a particular ca...
virtual void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
Subclass customisation point for recursion over RHS expression:
void get_reference_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets the set of expressions that expr may refer to, according to this value set.
virtual void apply_assign_side_effects(const exprt &lhs, const exprt &rhs, const namespacet &)
Subclass customisation point to apply global side-effects to this domain, after RHS values are read b...
std::map< object_numberingt::number_type, offsett > object_map_dt
Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances).
virtual void adjust_assign_rhs_values(const exprt &rhs, const namespacet &, object_mapt &rhs_values) const
Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set b...
void erase_symbol_rec(const typet &type, const std::string &erase_prefix, const namespacet &ns)
Operator to update elements in structs and arrays.
bool has_prefix(const std::string &s, const std::string &prefix)
#define forall_operands(it, expr)
#define Forall_operands(it, expr)
const code_returnt & to_code_return(const codet &code)
const std::string & id2string(const irep_idt &d)
API to expression classes for Pointers.
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 dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
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.
exprt dynamic_object(const exprt &pointer)
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
static optionalt< smt_termt > get_identifier(const exprt &expr, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_handle_identifiers, const std::unordered_map< exprt, smt_identifier_termt, irep_hash > &expression_identifiers)
#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'.
side_effect_exprt & to_side_effect_expr(exprt &expr)
const code_assumet & to_code_assume(const codet &code)
const codet & to_code(const exprt &expr)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
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 unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
const let_exprt & to_let_expr(const exprt &expr)
Cast an exprt to a let_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 union_exprt & to_union_expr(const exprt &expr)
Cast an exprt to a union_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
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.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Represents a row of a value_sett.
static bool failed(bool error_indicator)
static std::string strip_first_field_from_suffix(const std::string &suffix, const std::string &field)
static bool suffix_starts_with_field(const std::string &suffix, const std::string &field)
Check if 'suffix' starts with 'field'.