Go to the documentation of this file.
36 #define forall_objects(it, map) \
37 for(object_map_dt::const_iterator it = (map).begin(); \
41 #define Forall_objects(it, map) \
42 for(object_map_dt::iterator it = (map).begin(); \
48 std::ostream &out)
const
50 for(valuest::const_iterator
57 const entryt &e=v_it->second;
69 identifier=symbol.
name;
91 if(o.
id()==ID_invalid || o.
id()==ID_unknown)
96 if(o.
type().
id()==ID_unknown)
104 result=
"<"+
from_expr(ns, identifier, o)+
", ";
113 if(o.
type().
id()==ID_unknown)
123 width+=result.size();
128 if(next!=object_map.
read().
end())
152 std::cout <<
"FLATTEN: Done.\n";
166 assert(seen.find(identifier + e.
suffix)==seen.end());
168 bool generalize_index =
false;
170 seen.insert(identifier + e.
suffix);
176 if(o.
type().
id()==
"#REF#")
178 if(seen.find(o.
get(ID_identifier))!=seen.end())
180 generalize_index =
true;
184 valuest::const_iterator fi =
values.find(o.
get(ID_identifier));
200 if(t_it->second && it->second)
202 *t_it->second += *it->second;
205 t_it->second.reset();
222 seen.erase(identifier + e.
suffix);
229 if(
object.
id()==ID_invalid ||
230 object.
id()==ID_unknown)
242 return std::move(od);
250 for(valuest::const_iterator
251 it=new_values.begin();
252 it!=new_values.end();
255 valuest::iterator it2=
values.find(it->first);
261 "value_set::dynamic_object") ||
263 "value_set::return_value"))
273 const entryt &new_e=it->second;
299 std::list<exprt> &value_set,
302 std::vector<exprt> result_as_vector =
get_value_set(expr, ns);
304 result_as_vector.begin(),
305 result_as_vector.end(),
306 std::back_inserter(value_set));
320 if(
object.type().
id()==
"#REF#")
322 assert(
object.
id()==ID_symbol);
324 const irep_idt &ident =
object.get(ID_identifier);
325 valuest::const_iterator v_it =
values.find(ident);
336 if(t_it->second && it->second)
338 *t_it->second += *it->second;
341 t_it->second.reset();
343 flat_map.
write()[t_it->first]=t_it->second;
348 flat_map.
write()[it->first]=it->second;
351 std::vector<exprt> result;
353 result.push_back(
to_expr(*fit));
357 for(std::list<exprt>::const_iterator it=value_set.begin();
360 assert(it->type().id()!=
"#REF");
364 for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
365 std::cout <<
"GET_VALUE_SET: " <<
format(*it) <<
'\n';
386 const std::string &suffix,
387 const typet &original_type,
392 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
format(expr)
394 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
398 if(expr.
type().
id()==
"#REF#")
400 valuest::const_iterator fi =
values.find(expr.
get(ID_identifier));
406 original_type, ns, recursion_set);
415 else if(expr.
id()==ID_unknown || expr.
id()==ID_invalid)
420 else if(expr.
id()==ID_index)
426 "operand 0 of index expression must be an array");
438 else if(expr.
id()==ID_member)
442 if(compound.is_not_nil())
447 type.
id() == ID_struct || type.
id() == ID_union,
448 "operand 0 of member expression must be struct or union");
450 const std::string &component_name =
456 "." + component_name + suffix,
464 else if(expr.
id()==ID_symbol)
469 valuest::const_iterator v_it=
values.find(ident);
476 else if(v_it!=
values.end())
485 else if(expr.
id()==ID_if)
504 else if(expr.
id()==ID_address_of)
510 else if(expr.
id()==ID_dereference)
516 if(object_map.
begin()!=object_map.
end())
522 original_type, ns, recursion_set);
531 if(expr.
get(ID_value)==ID_NULL &&
532 expr.
type().
id()==ID_pointer)
538 else if(expr.
id()==ID_typecast)
550 else if(expr.
id()==ID_plus || expr.
id()==ID_minus)
553 throw expr.
id_string()+
" expected to have at least two operands";
555 if(expr.
type().
id()==ID_pointer)
558 const exprt *ptr_operand=
nullptr;
561 if(it->type().id()==ID_pointer)
563 if(ptr_operand==
nullptr)
566 throw "more than one pointer operand in pointer arithmetic";
569 if(ptr_operand==
nullptr)
570 throw "pointer type sum expected to have pointer operand";
574 ptr_operand->
type(), ns, recursion_set);
584 const auto i = numeric_cast<mp_integer>(
to_binary_expr(expr).op0());
588 *offset = (expr.
id() == ID_plus) ? *i : -*i;
592 const auto i = numeric_cast<mp_integer>(
to_binary_expr(expr).op1());
596 *offset = (expr.
id() == ID_plus) ? *i : -*i;
602 insert(dest, it->first, offset);
608 else if(expr.
id()==ID_side_effect)
612 if(statement==ID_function_call)
615 throw "unexpected function_call sideeffect";
617 else if(statement==ID_allocate)
619 if(expr.
type().
id()!=ID_pointer)
620 throw "malloc expected to return pointer type";
624 const typet &dynamic_type=
625 static_cast<const typet &
>(expr.
find(ID_C_cxx_alloc_type));
636 else if(statement==ID_cpp_new ||
637 statement==ID_cpp_new_array)
640 assert(expr.
type().
id()==ID_pointer);
651 else if(expr.
id()==ID_struct)
657 else if(expr.
id()==ID_with)
660 throw "unexpected value in get_value_set: "+expr.
id_string();
662 else if(expr.
id()==ID_array_of ||
669 else if(expr.
id()==ID_dynamic_object)
674 const std::string name=
675 "value_set::dynamic_object"+
680 valuest::const_iterator v_it=
values.find(name);
697 if(src.
id()==ID_typecast)
699 assert(src.
type().
id()==ID_pointer);
719 if(
object.type().
id() ==
"#REF#")
721 const irep_idt &ident =
object.get(ID_identifier);
722 valuest::const_iterator vit =
values.find(ident);
727 dest.insert(
exprt(ID_unknown,
object.type()));
738 if(t_it->second && it->second)
740 *t_it->second += *it->second;
743 t_it->second.reset();
746 for(
const auto &o : omt.
read())
773 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
format(expr)
777 if(expr.
type().
id()==
"#REF#")
779 valuest::const_iterator fi =
values.find(expr.
get(ID_identifier));
787 else if(expr.
id()==ID_symbol ||
788 expr.
id()==ID_dynamic_object ||
789 expr.
id()==ID_string_constant)
791 if(expr.
type().
id()==ID_array &&
799 else if(expr.
id()==ID_dereference)
815 if(obj.
type().
id()==
"#REF#")
818 valuest::const_iterator v_it =
values.find(ident);
829 if(t_it->second && it->second)
831 *t_it->second += *it->second;
834 t_it->second.reset();
848 for(expr_sett::const_iterator it=value_set.begin();
851 std::cout <<
"VALUE_SET: " <<
format(*it) <<
'\n';
856 else if(expr.
id()==ID_index)
863 array_type.
id() == ID_array,
"index takes array-typed operand");
874 if(
object.
id()==ID_unknown)
884 if(
object.type().
id() !=
"#REF#" &&
object.type() != array_type)
887 casted_index = index_expr;
890 const auto i = numeric_cast<mp_integer>(offset);
900 insert(dest, casted_index, o);
906 else if(expr.
id()==ID_member)
908 const irep_idt &component_name=expr.
get(ID_component_name);
918 const typet &obj_type =
object.type();
920 if(
object.
id()==ID_unknown)
923 object.
id() == ID_dynamic_object && obj_type.
id() != ID_struct &&
924 obj_type.
id() != ID_union && obj_type.
id() != ID_struct_tag &&
925 obj_type.
id() != ID_union_tag)
944 insert(dest, member_expr, o);
950 else if(expr.
id()==ID_if)
966 std::cout <<
"ASSIGN LHS: " <<
format(lhs) <<
'\n';
967 std::cout <<
"ASSIGN RHS: " <<
format(rhs) <<
'\n';
979 if(type.
id()==ID_struct ||
986 for(struct_typet::componentst::const_iterator
991 const typet &subtype=c_it->type();
992 const irep_idt &name = c_it->get_name();
995 if(subtype.
id()==ID_code)
1002 if(rhs.
id()==ID_unknown ||
1003 rhs.
id()==ID_invalid)
1005 rhs_member=
exprt(rhs.
id(), subtype);
1010 throw "value_set_fit::assign type mismatch: "
1014 if(rhs.
id()==ID_struct ||
1015 rhs.
id()==ID_constant)
1020 else if(rhs.
id()==ID_with)
1024 const exprt &member_operand = rhs_with.where();
1027 member_operand.
get(ID_component_name);
1029 if(component_name==name)
1032 rhs_member = rhs_with.new_value();
1037 rhs_member=
exprt(ID_member, subtype);
1039 rhs_member.
set(ID_component_name, name);
1044 rhs_member=
exprt(ID_member, subtype);
1046 rhs_member.
set(ID_component_name, name);
1049 assign(lhs_member, rhs_member, ns);
1053 else if(type.
id()==ID_array)
1058 if(rhs.
id()==ID_unknown ||
1059 rhs.
id()==ID_invalid)
1069 if(rhs.
type() != type)
1070 throw "value_set_fit::assign type mismatch: "
1074 if(rhs.
id()==ID_array_of)
1078 else if(rhs.
id()==ID_array ||
1079 rhs.
id()==ID_constant)
1083 assign(lhs_index, *o_it, ns);
1086 else if(rhs.
id()==ID_with)
1093 assign(lhs_index, op0_index, ns);
1100 assign(lhs_index, rhs_index, ns);
1119 const std::string &suffix,
1124 std::cout <<
"ASSIGN_REC LHS: " <<
format(lhs) <<
'\n';
1125 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1128 it!=values_rhs.
read().
end(); it++)
1129 std::cout <<
"ASSIGN_REC RHS: " <<
to_expr(it) <<
'\n';
1132 if(lhs.
type().
id()==
"#REF#")
1139 if(recursion_set.find(ident)!=recursion_set.end())
1141 recursion_set.insert(ident);
1146 suffix, ns, recursion_set);
1148 recursion_set.erase(ident);
1151 else if(lhs.
id()==ID_symbol)
1156 "value_set::dynamic_object") ||
1158 "value_set::return_value") ||
1168 else if(lhs.
id()==ID_dynamic_object)
1173 const std::string name=
1174 "value_set::dynamic_object"+
1180 else if(lhs.
id()==ID_dereference)
1183 throw lhs.
id_string()+
" expected to have one operand";
1192 if(
object.
id()!=ID_unknown)
1193 assign_rec(
object, values_rhs, suffix, ns, recursion_set);
1196 else if(lhs.
id()==ID_index)
1202 "operand 0 of index expression must be an array");
1205 to_index_expr(lhs).array(), values_rhs,
"[]" + suffix, ns, recursion_set);
1207 else if(lhs.
id()==ID_member)
1212 const std::string &component_name=lhs.
get_string(ID_component_name);
1217 type.
id() == ID_struct || type.
id() == ID_union,
1218 "operand 0 of member expression must be struct or union");
1223 "." + component_name + suffix,
1227 else if(lhs.
id()==
"valid_object" ||
1228 lhs.
id()==
"dynamic_size" ||
1229 lhs.
id()==
"dynamic_type")
1233 else if(lhs.
id()==ID_string_constant)
1238 else if(lhs.
id() == ID_null_object)
1242 else if(lhs.
id()==ID_typecast)
1246 assign_rec(typecast_expr.
op(), values_rhs, suffix, ns, recursion_set);
1248 else if(lhs.
id()==
"zero_string" ||
1249 lhs.
id()==
"is_zero_string" ||
1250 lhs.
id()==
"zero_string_length")
1254 else if(lhs.
id()==ID_byte_extract_little_endian ||
1255 lhs.
id()==ID_byte_extract_big_endian)
1261 throw "assign NYI: '" + lhs.
id_string() +
"'";
1279 for(std::size_t i=0; i<arguments.size(); i++)
1281 const std::string identifier=
"value_set::" +
id2string(
function) +
"::" +
1284 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1285 assign(dummy_lhs, arguments[i], ns);
1292 for(code_typet::parameterst::const_iterator
1293 it=parameter_types.begin();
1294 it!=parameter_types.end();
1297 const irep_idt &identifier=it->get_identifier();
1298 if(identifier.
empty())
1308 assign(actual_lhs, v_expr, ns);
1330 if(statement==ID_block)
1335 else if(statement==ID_function_call)
1340 else if(statement==ID_assign)
1343 throw "assignment expected to have two operands";
1347 else if(statement==ID_decl)
1350 throw "decl expected to have one operand";
1354 if(lhs.
id()!=ID_symbol)
1355 throw "decl expected to have symbol on lhs";
1359 else if(statement==ID_expression)
1363 else if(statement==ID_cpp_delete ||
1364 statement==ID_cpp_delete_array)
1368 else if(statement==
"lock" || statement==
"unlock")
1372 else if(statement==ID_asm)
1376 else if(statement==ID_nondet)
1380 else if(statement==ID_printf)
1384 else if(statement==ID_return)
1395 else if(statement==ID_fence)
1398 else if(statement==ID_array_copy ||
1399 statement==ID_array_replace ||
1400 statement==ID_array_set)
1410 "value_set_fit: unexpected statement: "+
id2string(statement);
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
#define UNREACHABLE
This should be used to mark dead code.
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
entryt & get_entry(const idt &id, const std::string &suffix)
static const char * alloc_adapter_prefix
std::unordered_set< idt, string_hash > assign_recursion_sett
const typet & subtype() const
bool can_cast_expr< code_inputt >(const exprt &base)
static hash_numbering< irep_idt, irep_id_hash > function_numbering
std::unordered_map< idt, entryt, string_hash > valuest
bool offset_is_zero(const offsett &offset) const
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
Value Set (Flow Insensitive, Sharing)
data_typet::iterator iterator
const irep_idt & display_name() const
Return language specific display name if present.
The type of an expression, extends irept.
std::vector< parametert > parameterst
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns)
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.
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
Base type for structs and unions.
typet type
Type of symbol.
Representation of heap-allocated objects.
std::unordered_set< idt, string_hash > flatten_seent
std::unordered_set< exprt, irep_hash > expr_sett
Split an expression into a base object and a (byte) offset.
const irept & find(const irep_namet &name) const
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
const array_of_exprt & to_array_of_expr(const exprt &expr)
Cast an exprt to an array_of_exprt.
Base class for all expressions.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
std::unordered_set< idt, string_hash > gvs_recursion_sett
void dereference_rec(const exprt &src, exprt &dest) const
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
exprt dynamic_object(const exprt &pointer)
unsigned from_target_index
side_effect_exprt & to_side_effect_expr(exprt &expr)
#define Forall_objects(it, map)
void flatten(const entryt &e, object_mapt &dest) const
Expression to hold a symbol (variable)
void flatten_rec(const entryt &, object_mapt &, flatten_seent &) const
bitvector_typet index_type()
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
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.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void apply_code(const codet &code, const namespacet &ns)
Expression classes for byte-level operators.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
#define forall_objects(it, map)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const std::string & id2string(const irep_idt &d)
void get_value_set(const exprt &expr, std::list< exprt > &dest, const namespacet &ns) const
const exprt & compound() const
#define forall_operands(it, expr)
data_typet::const_iterator const_iterator
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
const std::string & id_string() const
bool simplify(exprt &expr, const namespacet &ns)
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
std::vector< exprt > operandst
const code_returnt & to_code_return(const codet &code)
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
const parameterst & parameters() const
static const object_map_dt blank
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const irep_idt & get_statement() const
bool is_zero() const
Return whether the expression is a constant representing 0.
Extract member of struct or union.
bool make_union(object_mapt &dest, const object_mapt &src) const
const std::string & get_string(const irep_namet &name) const
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
bool has_return_value() const
void output(const namespacet &ns, std::ostream &out) const
bool can_cast_expr< code_outputt >(const exprt &base)
codet representation of a "return from a function" statement.
exprt to_expr(const object_map_dt::value_type &it) const
void do_end_function(const exprt &lhs, const namespacet &ns)
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
bool is_constant() const
Return whether the expression is a constant.
static object_numberingt object_numbering
const code_blockt & to_code_block(const codet &code)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
bool has_prefix(const std::string &s, const std::string &prefix)
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value,...
Operator to return the address of an object.
data_typet::value_type value_type
Semantic type conversion.
const exprt & return_value() const
The Boolean constant true.
API to expression classes.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
irep_idt name
The unique identifier.
void add_var(const idt &id)
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns, gvs_recursion_sett &recursion_set) const
Data structure for representing an arbitrary statement in a program.
const std::string integer2string(const mp_integer &n, unsigned base)