39 std::ostream &out)
const
41 for(valuest::const_iterator
48 const entryt &e=v_it->second;
60 identifier=symbol.
name;
76 const auto &entries = object_map.
read();
78 o_it != entries.end();
85 if(o.
id()==ID_invalid || o.
id()==ID_unknown)
90 if(o.
type().
id()==ID_unknown)
98 result=
"<"+
from_expr(ns, identifier, o)+
", ";
107 if(o.
type().
id()==ID_unknown)
117 width+=result.size();
122 if(next != entries.end())
146 std::cout <<
"FLATTEN: Done.\n";
162 bool generalize_index =
false;
164 seen.insert(identifier + e.
suffix);
170 if(o.
type().
id()==
"#REF#")
172 if(seen.find(o.
get(ID_identifier))!=seen.end())
174 generalize_index =
true;
178 valuest::const_iterator fi =
values.find(o.
get(ID_identifier));
195 if(t_it->second && object_entry.second)
197 *t_it->second += *object_entry.second;
200 t_it->second.reset();
203 for(
const auto &object_entry : temp.
read())
204 insert(dest, object_entry);
208 insert(dest, object_entry);
213 for(
auto &object_entry : dest.
write())
214 object_entry.second.reset();
217 seen.erase(identifier + e.
suffix);
224 if(
object.
id()==ID_invalid ||
225 object.
id()==ID_unknown)
237 return std::move(od);
245 for(valuest::const_iterator
246 it=new_values.begin();
247 it!=new_values.end();
250 valuest::iterator it2=
values.find(it->first);
256 it->second.identifier.starts_with(
"value_set::dynamic_object") ||
257 it->second.identifier.starts_with(
"value_set::return_value"))
267 const entryt &new_e=it->second;
282 for(
const auto &object_entry : src.
read())
284 if(
insert(dest, object_entry))
299 for(
const auto &object_entry : object_map.
read())
302 if(
object.type().
id()==
"#REF#")
304 DATA_INVARIANT(
object.
id() == ID_symbol,
"reference to symbol required");
306 const irep_idt &ident =
object.get(ID_identifier);
307 valuest::const_iterator v_it =
values.find(ident);
318 if(t_it->second && object_entry.second)
320 *t_it->second += *object_entry.second;
323 t_it->second.reset();
325 flat_map.
write()[t_it->first]=t_it->second;
330 flat_map.
write()[object_entry.first] = object_entry.second;
333 std::vector<exprt> result;
334 for(
const auto &object_entry : flat_map.
read())
335 result.push_back(
to_expr(object_entry));
339 for(std::list<exprt>::const_iterator it=value_set.begin();
342 assert(it->type().id()!=
"#REF");
346 for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
347 std::cout <<
"GET_VALUE_SET: " <<
format(*it) <<
'\n';
362 bool includes_nondet_pointer =
false;
364 tmp, dest, includes_nondet_pointer,
"", tmp.
type(), ns, recset);
370 bool &includes_nondet_pointer,
371 const std::string &suffix,
372 const typet &original_type,
377 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
format(expr)
379 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
383 if(expr.
type().
id()==
"#REF#")
385 valuest::const_iterator fi =
values.find(expr.
get(ID_identifier));
389 for(
const auto &object_entry : fi->second.object_map.read())
394 includes_nondet_pointer,
408 else if(expr.
id()==ID_unknown || expr.
id()==ID_invalid)
413 else if(expr.
id()==ID_index)
417 if(type.
id() == ID_array)
422 includes_nondet_pointer,
433 else if(expr.
id()==ID_member)
437 if(compound.is_not_nil())
440 compound.type().id() == ID_struct ||
441 compound.type().id() == ID_struct_tag ||
442 compound.type().id() == ID_union ||
443 compound.type().id() == ID_union_tag,
444 "operand 0 of member expression must be struct or union");
446 const std::string &component_name =
452 includes_nondet_pointer,
453 "." + component_name + suffix,
461 else if(expr.
id()==ID_symbol)
466 valuest::const_iterator v_it=
values.find(ident);
473 else if(v_it!=
values.end())
481 else if(expr.
id()==ID_if)
486 includes_nondet_pointer,
494 includes_nondet_pointer,
502 else if(expr.
id()==ID_address_of)
508 else if(expr.
id()==ID_dereference)
514 if(object_map.
begin()!=object_map.
end())
516 for(
const auto &object_entry : object_map)
522 includes_nondet_pointer,
544 else if(expr.
id()==ID_typecast)
549 includes_nondet_pointer,
557 else if(expr.
id()==ID_plus || expr.
id()==ID_minus)
560 throw expr.
id_string()+
" expected to have at least two operands";
562 if(expr.
type().
id()==ID_pointer)
565 const exprt *ptr_operand=
nullptr;
567 for(
const auto &op : expr.
operands())
569 if(op.type().id() == ID_pointer)
571 if(ptr_operand==
nullptr)
574 throw "more than one pointer operand in pointer arithmetic";
578 if(ptr_operand==
nullptr)
579 throw "pointer type sum expected to have pointer operand";
585 includes_nondet_pointer,
591 for(
const auto &object_entry : pointer_expr_set.
read())
593 offsett offset = object_entry.second;
603 *offset = (expr.
id() == ID_plus) ? *i : -*i;
611 *offset = (expr.
id() == ID_plus) ? *i : -*i;
617 insert(dest, object_entry.first, offset);
623 else if(expr.
id()==ID_side_effect)
627 if(statement==ID_function_call)
630 throw "unexpected function_call sideeffect";
632 else if(statement==ID_allocate)
634 if(expr.
type().
id()!=ID_pointer)
635 throw "malloc expected to return pointer type";
639 const typet &dynamic_type=
640 static_cast<const typet &
>(expr.
find(ID_C_cxx_alloc_type));
651 else if(statement==ID_cpp_new ||
652 statement==ID_cpp_new_array)
667 else if(expr.
id()==ID_struct)
673 else if(expr.
id()==ID_with)
676 throw "unexpected value in get_value_set: "+expr.
id_string();
678 else if(expr.
id()==ID_array_of ||
682 for(
const auto &op : expr.
operands())
687 includes_nondet_pointer,
694 else if(expr.
id()==ID_dynamic_object)
699 const std::string name=
700 "value_set::dynamic_object"+
705 valuest::const_iterator v_it=
values.find(name);
722 if(src.
id()==ID_typecast)
740 for(
const auto &object_entry : object_map.
read())
744 if(
object.type().
id() ==
"#REF#")
746 const irep_idt &ident =
object.get(ID_identifier);
747 valuest::const_iterator vit =
values.find(ident);
752 dest.insert(
exprt(ID_unknown,
object.type()));
763 if(t_it->second && object_entry.second)
765 *t_it->second += *object_entry.second;
768 t_it->second.reset();
771 for(
const auto &o : omt.
read())
776 dest.insert(
to_expr(object_entry));
788 for(
const auto &object_entry : object_map.
read())
789 dest.insert(
to_expr(object_entry));
798 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
format(expr)
802 if(expr.
type().
id()==
"#REF#")
804 valuest::const_iterator fi =
values.find(expr.
get(ID_identifier));
807 for(
const auto &object_entry : fi->second.object_map.read())
815 else if(expr.
id()==ID_symbol ||
816 expr.
id()==ID_dynamic_object ||
817 expr.
id()==ID_string_constant)
820 expr.
type().
id() == ID_array &&
830 else if(expr.
id()==ID_dereference)
834 bool includes_nondet_pointer =
false;
838 includes_nondet_pointer,
845 for(
const auto &object_entry : temp.
read())
848 if(obj.
type().
id()==
"#REF#")
851 valuest::const_iterator v_it =
values.find(ident);
862 if(t_it->second && object_entry.second)
864 *t_it->second += *object_entry.second;
867 t_it->second.reset();
870 for(
const auto &t2_object_entry : t2.
read())
871 insert(dest, t2_object_entry);
879 insert(dest, object_entry);
883 for(expr_sett::const_iterator it=value_set.begin();
886 std::cout <<
"VALUE_SET: " <<
format(*it) <<
'\n';
891 else if(expr.
id()==ID_index)
898 array_type.
id() == ID_array,
"index takes array-typed operand");
905 for(
const auto &object_entry : object_map)
909 if(
object.
id()==ID_unknown)
919 if(
object.type().
id() !=
"#REF#" &&
object.type() != array_type)
922 casted_index = index_expr;
924 offsett o = object_entry.second;
935 insert(dest, casted_index, o);
941 else if(expr.
id()==ID_member)
943 const irep_idt &component_name=expr.
get(ID_component_name);
950 for(
const auto &object_entry : struct_references.
read())
953 const typet &obj_type =
object.type();
955 if(
object.
id()==ID_unknown)
958 obj_type.
id() != ID_struct && obj_type.
id() != ID_union &&
959 obj_type.
id() != ID_struct_tag && obj_type.
id() != ID_union_tag)
967 offsett o = object_entry.second;
972 if(struct_op.
type() !=
object.type())
978 insert(dest, member_expr, o);
984 else if(expr.
id()==ID_if)
1000 std::cout <<
"ASSIGN LHS: " <<
format(lhs) <<
'\n';
1001 std::cout <<
"ASSIGN RHS: " <<
format(rhs) <<
'\n';
1012 lhs.
type().
id() == ID_struct || lhs.
type().
id() == ID_struct_tag ||
1013 lhs.
type().
id() == ID_union || lhs.
type().
id() == ID_union_tag)
1015 const auto &components =
1016 (lhs.
type().
id() == ID_struct_tag || lhs.
type().
id() == ID_union_tag)
1022 for(struct_typet::componentst::const_iterator c_it = components.begin();
1023 c_it != components.end();
1026 const typet &subtype=c_it->type();
1027 const irep_idt &name = c_it->get_name();
1031 subtype.
id() != ID_code,
1032 "struct/union member must not be of code type");
1033 if(c_it->get_is_padding())
1040 if(rhs.
id()==ID_unknown ||
1041 rhs.
id()==ID_invalid)
1043 rhs_member=
exprt(rhs.
id(), subtype);
1048 throw "value_set_fit::assign type mismatch: "
1055 no < rhs.
operands().size(),
"component index must be in bounds");
1058 else if(rhs.
id()==ID_with)
1062 const exprt &member_operand = rhs_with.where();
1065 member_operand.
get(ID_component_name);
1067 if(component_name==name)
1070 rhs_member = rhs_with.new_value();
1075 rhs_member=
exprt(ID_member, subtype);
1077 rhs_member.
set(ID_component_name, name);
1082 rhs_member=
exprt(ID_member, subtype);
1084 rhs_member.
set(ID_component_name, name);
1087 assign(lhs_member, rhs_member, ns);
1091 else if(lhs.
type().
id() == ID_array)
1098 if(rhs.
id()==ID_unknown ||
1099 rhs.
id()==ID_invalid)
1113 throw "value_set_fit::assign type mismatch: "
1117 if(rhs.
id()==ID_array_of)
1123 for(
const auto &op : rhs.
operands())
1125 assign(lhs_index, op, ns);
1128 else if(rhs.
id()==ID_with)
1135 assign(lhs_index, op0_index, ns);
1144 assign(lhs_index, rhs_index, ns);
1163 const std::string &suffix,
1168 std::cout <<
"ASSIGN_REC LHS: " <<
format(lhs) <<
'\n';
1169 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1172 it!=values_rhs.
read().
end(); it++)
1173 std::cout <<
"ASSIGN_REC RHS: " <<
to_expr(it) <<
'\n';
1176 if(lhs.
type().
id()==
"#REF#")
1181 bool includes_nondet_pointer =
false;
1185 includes_nondet_pointer,
1191 if(recursion_set.find(ident)!=recursion_set.end())
1193 recursion_set.insert(ident);
1195 for(
const auto &object_entry : temp.
read())
1199 if(
object.
id() != ID_unknown)
1200 assign_rec(
object, values_rhs, suffix, ns, recursion_set);
1203 recursion_set.erase(ident);
1206 else if(lhs.
id()==ID_symbol)
1211 identifier.
starts_with(
"value_set::dynamic_object") ||
1212 identifier.
starts_with(
"value_set::return_value") ||
1222 else if(lhs.
id()==ID_dynamic_object)
1227 const std::string name=
1228 "value_set::dynamic_object"+
1234 else if(lhs.
id()==ID_dereference)
1237 throw lhs.
id_string()+
" expected to have one operand";
1242 for(
const auto &object_entry : reference_set.
read())
1246 if(
object.
id()!=ID_unknown)
1247 assign_rec(
object, values_rhs, suffix, ns, recursion_set);
1250 else if(lhs.
id()==ID_index)
1254 if(type.
id() == ID_array)
1264 else if(lhs.
id()==ID_member)
1269 const std::string &component_name=lhs.
get_string(ID_component_name);
1273 compound.
type().
id() == ID_struct ||
1274 compound.
type().
id() == ID_struct_tag ||
1275 compound.
type().
id() == ID_union ||
1276 compound.
type().
id() == ID_union_tag,
1277 "operand 0 of member expression must be struct or union");
1280 compound, values_rhs,
"." + component_name + suffix, ns, recursion_set);
1282 else if(lhs.
id()==
"valid_object" ||
1283 lhs.
id()==
"dynamic_type")
1287 else if(lhs.
id()==ID_string_constant)
1292 else if(lhs.
id() == ID_null_object)
1296 else if(lhs.
id()==ID_typecast)
1300 assign_rec(typecast_expr.
op(), values_rhs, suffix, ns, recursion_set);
1303 lhs.
id() ==
"zero_string" || lhs.
id() ==
"is_zero_string" ||
1304 lhs.
id() ==
"zero_string_length" || lhs.
id() == ID_address_of)
1308 else if(lhs.
id()==ID_byte_extract_little_endian ||
1309 lhs.
id()==ID_byte_extract_big_endian)
1315 throw "assign NYI: '" + lhs.
id_string() +
"'";
1333 for(std::size_t i=0; i<arguments.size(); i++)
1335 const std::string identifier=
"value_set::" +
id2string(function) +
"::" +
1336 "argument$"+std::to_string(i);
1338 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1339 assign(dummy_lhs, arguments[i], ns);
1346 for(code_typet::parameterst::const_iterator
1347 it=parameter_types.begin();
1348 it!=parameter_types.end();
1351 const irep_idt &identifier=it->get_identifier();
1352 if(identifier.
empty())
1359 "argument$"+std::to_string(i), it->type());
1362 assign(actual_lhs, v_expr, ns);
1374 std::string rvs =
"value_set::return_value" + std::to_string(
from_function);
1384 if(statement==ID_block)
1389 else if(statement==ID_function_call)
1394 else if(statement==ID_assign)
1397 throw "assignment expected to have two operands";
1401 else if(statement==ID_decl)
1404 throw "decl expected to have one operand";
1408 if(lhs.
id()!=ID_symbol)
1409 throw "decl expected to have symbol on lhs";
1413 else if(statement==ID_expression)
1417 else if(statement==ID_cpp_delete ||
1418 statement==ID_cpp_delete_array)
1422 else if(statement==
"lock" || statement==
"unlock")
1426 else if(statement==ID_asm)
1430 else if(statement==ID_nondet)
1434 else if(statement==ID_printf)
1438 else if(statement==ID_return)
1442 std::string rvs =
"value_set::return_value" + std::to_string(
from_function);
1446 else if(statement==ID_fence)
1450 statement == ID_array_copy || statement == ID_array_replace ||
1451 statement == ID_array_set || statement == ID_array_equal)
1458 else if(statement == ID_havoc_object)
1464 "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.
const typet & element_type() const
The type of the elements of the array.
goto_instruction_codet representation of a "return from afunction" statement.
const exprt & return_value() const
const parameterst & parameters() const
std::vector< parametert > parameterst
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.
unsigned int get_instance() const
void set_instance(unsigned int instance)
Base class for all expressions.
std::vector< exprt > operandst
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
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
void set(const irep_idt &name, const irep_idt &value)
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 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 typet & base_type() const
The type of the data what we point to.
const irep_idt & get_statement() const
const componentst & components() const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
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.
const typet & subtype() const
Semantic type conversion.
The type of an expression, extends irept.
data_typet::iterator iterator
data_typet::value_type value_type
data_typet::const_iterator const_iterator
static const object_map_dt blank
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)
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
std::unordered_set< exprt, irep_hash > expr_sett
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
void do_end_function(const exprt &lhs, const namespacet &ns)
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)
std::unordered_set< idt > assign_recursion_sett
unsigned from_target_index
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
exprt to_expr(const object_map_dt::value_type &it) const
std::set< idt > flatten_seent
std::map< idt, entryt > valuest
std::unordered_set< idt > gvs_recursion_sett
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...
Deprecated expression utility functions.
bool can_cast_expr< code_inputt >(const exprt &base)
bool can_cast_expr< code_outputt >(const exprt &base)
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)