38 std::ostream &out)
const
40 for(valuest::const_iterator
59 identifier=symbol.
name;
75 const auto &entries = object_map.
read();
77 o_it != entries.end();
97 result=
"<"+
from_expr(ns, identifier, o)+
", ";
116 width+=result.size();
121 if(next != entries.end())
145 std::cout <<
"FLATTEN: Done.\n";
163 seen.insert(identifier + e.
suffix);
169 if(o.
type().
id()==
"#REF#")
199 t_it->second.reset();
216 seen.erase(identifier + e.
suffix);
234 od.type()=
od.object().type();
236 return std::move(
od);
244 for(valuest::const_iterator
249 valuest::iterator
it2=
values.find(it->first);
255 it->second.identifier.starts_with(
"value_set::dynamic_object") ||
256 it->second.identifier.starts_with(
"value_set::return_value"))
301 if(
object.type().id()==
"#REF#")
322 t_it->second.reset();
332 std::vector<exprt> result;
338 for(std::list<exprt>::const_iterator it=value_set.begin();
341 assert(it->type().id()!=
"#REF");
345 for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
346 std::cout <<
"GET_VALUE_SET: " <<
format(*it) <<
'\n';
370 const std::string &suffix,
376 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
format(expr)
378 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
382 if(expr.
type().
id()==
"#REF#")
436 if(compound.is_not_nil())
443 "operand 0 of member expression must be struct or union");
445 const std::string &component_name =
452 "." + component_name + suffix,
513 if(object_map.
begin()!=object_map.
end())
559 throw expr.
id_string()+
" expected to have at least two operands";
566 for(
const auto &op : expr.
operands())
573 throw "more than one pointer operand in pointer arithmetic";
578 throw "pointer type sum expected to have pointer operand";
602 *offset = (expr.
id() ==
ID_plus) ? *i : -*i;
610 *offset = (expr.
id() ==
ID_plus) ? *i : -*i;
629 throw "unexpected function_call sideeffect";
634 throw "malloc expected to return pointer type";
675 throw "unexpected value in get_value_set: "+expr.
id_string();
681 for(
const auto &op : expr.
operands())
698 const std::string name=
699 "value_set::dynamic_object"+
704 valuest::const_iterator
v_it=
values.find(name);
743 if(
object.type().id() ==
"#REF#")
767 t_it->second.reset();
770 for(
const auto &o :
omt.read())
797 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
format(expr)
801 if(expr.
type().
id()==
"#REF#")
847 if(
obj.type().id()==
"#REF#")
866 t_it->second.reset();
882 for(expr_sett::const_iterator it=value_set.begin();
885 std::cout <<
"VALUE_SET: " <<
format(*it) <<
'\n';
918 if(
object.type().
id() !=
"#REF#" &&
object.type() !=
array_type)
971 if(struct_op.
type() !=
object.type())
999 std::cout <<
"ASSIGN LHS: " <<
format(lhs) <<
'\n';
1000 std::cout <<
"ASSIGN RHS: " <<
format(rhs) <<
'\n';
1014 const auto &components =
1021 for(struct_typet::componentst::const_iterator
c_it = components.begin();
1022 c_it != components.end();
1031 "struct/union member must not be of code type");
1032 if(
c_it->get_is_padding())
1047 throw "value_set_fit::assign type mismatch: "
1054 no < rhs.
operands().size(),
"component index must be in bounds");
1066 if(component_name==name)
1112 throw "value_set_fit::assign type mismatch: "
1122 for(
const auto &op : rhs.
operands())
1162 const std::string &suffix,
1167 std::cout <<
"ASSIGN_REC LHS: " <<
format(lhs) <<
'\n';
1168 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1172 std::cout <<
"ASSIGN_REC RHS: " <<
to_expr(it) <<
'\n';
1175 if(lhs.
type().
id()==
"#REF#")
1190 if(recursion_set.find(
ident)!=recursion_set.end())
1192 recursion_set.insert(
ident);
1202 recursion_set.erase(
ident);
1210 identifier.
starts_with(
"value_set::dynamic_object") ||
1211 identifier.
starts_with(
"value_set::return_value") ||
1226 const std::string name=
1227 "value_set::dynamic_object"+
1236 throw lhs.
id_string()+
" expected to have one operand";
1276 "operand 0 of member expression must be struct or union");
1279 compound,
values_rhs,
"." + component_name + suffix, ns, recursion_set);
1281 else if(lhs.
id()==
"valid_object" ||
1282 lhs.
id()==
"dynamic_type")
1302 lhs.
id() ==
"zero_string" || lhs.
id() ==
"is_zero_string" ||
1314 throw "assign NYI: '" + lhs.
id_string() +
"'";
1332 for(std::size_t i=0; i<arguments.size(); i++)
1334 const std::string identifier=
"value_set::" +
id2string(function) +
"::" +
1335 "argument$"+std::to_string(i);
1345 for(code_typet::parameterst::const_iterator
1350 const irep_idt &identifier=it->get_identifier();
1351 if(identifier.
empty())
1358 "argument$"+std::to_string(i), it->type());
1373 std::string
rvs =
"value_set::return_value" + std::to_string(
from_function);
1396 throw "assignment expected to have two operands";
1403 throw "decl expected to have one operand";
1408 throw "decl expected to have symbol on lhs";
1421 else if(statement==
"lock" || statement==
"unlock")
1425 else if(statement==
ID_asm)
1441 std::string
rvs =
"value_set::return_value" + std::to_string(
from_function);
1463 "value_set_fit: unexpected statement: "+
id2string(statement);
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
bitvector_typet c_index_type()
Operator to return the address of an object.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
goto_instruction_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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool starts_with(const char *s) const
equivalent of as_string().starts_with(s)
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 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.
const irep_idt & get_statement() const
Expression to hold a symbol (variable)
typet type
Type of symbol.
irep_idt name
The unique identifier.
const irep_idt & display_name() const
Return language specific display name if present.
The Boolean constant true.
Type with a single subtype.
Semantic type conversion.
The type of an expression, extends irept.
data_typet::value_type value_type
data_typet::const_iterator const_iterator
static const object_map_dt blank
data_typet::iterator iterator
std::optional< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
static object_numberingt object_numbering
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns)
static numberingt< irep_idt > function_numbering
void add_var(const idt &id)
std::unordered_set< idt > assign_recursion_sett
bool make_union(object_mapt &dest, const object_mapt &src) const
std::vector< exprt > get_value_set(const exprt &expr, const namespacet &ns) const
void apply_code(const codet &code, const namespacet &ns)
void get_value_set_rec(const exprt &expr, object_mapt &dest, bool &includes_nondet_pointer, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)
void dereference_rec(const exprt &src, exprt &dest) const
void output(const namespacet &ns, std::ostream &out) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &) const
std::unordered_set< exprt, irep_hash > expr_sett
void do_end_function(const exprt &lhs, const namespacet &ns)
std::set< idt > flatten_seent
void flatten(const entryt &e, object_mapt &dest) const
bool offset_is_zero(const offsett &offset) const
entryt & get_entry(const idt &id, const std::string &suffix)
unsigned from_target_index
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
std::unordered_set< idt > gvs_recursion_sett
std::map< idt, entryt > valuest
exprt to_expr(const object_map_dt::value_type &it) const
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
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...
const code_returnt & to_code_return(const goto_instruction_codet &code)
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
const std::string integer2string(const mp_integer &n, unsigned base)
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.
bool simplify(exprt &expr, 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)
side_effect_exprt & to_side_effect_expr(exprt &expr)
const code_blockt & to_code_block(const codet &code)
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 binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_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 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 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_or_union_tag_typet & to_struct_or_union_tag_type(const typet &type)
Cast a typet to a struct_or_union_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.
const type_with_subtypet & to_type_with_subtype(const typet &type)
static const char * alloc_adapter_prefix
Value Set (Flow Insensitive, Sharing)