35 #define forall_objects(it, map) \ 36 for(object_map_dt::const_iterator it = (map).begin(); \ 40 #define Forall_objects(it, map) \ 41 for(object_map_dt::iterator it = (map).begin(); \ 47 std::ostream &out)
const 49 for(valuest::const_iterator
56 const entryt &e=v_it->second;
68 identifier=symbol.
name;
90 if(o.
id()==ID_invalid || o.
id()==ID_unknown)
95 if(o.
type().
id()==ID_unknown)
103 result=
"<"+
from_expr(ns, identifier, o)+
", ";
112 if(o.
type().
id()==ID_unknown)
122 width+=result.size();
127 if(next!=object_map.
read().
end())
151 std::cout <<
"FLATTEN: Done.\n";
165 assert(seen.find(identifier + e.
suffix)==seen.end());
167 bool generalize_index =
false;
169 seen.insert(identifier + e.
suffix);
175 if(o.
type().
id()==
"#REF#")
177 if(seen.find(o.
get(ID_identifier))!=seen.end())
179 generalize_index =
true;
183 valuest::const_iterator fi =
values.find(o.
get(ID_identifier));
199 if(t_it->second && it->second)
201 *t_it->second += *it->second;
204 t_it->second.reset();
221 seen.erase(identifier + e.
suffix);
228 if(
object.
id()==ID_invalid ||
229 object.
id()==ID_unknown)
241 return std::move(od);
249 for(valuest::const_iterator
250 it=new_values.begin();
251 it!=new_values.end();
254 valuest::iterator it2=
values.find(it->first);
260 "value_set::dynamic_object") ||
262 "value_set::return_value"))
272 const entryt &new_e=it->second;
298 std::list<exprt> &value_set,
309 if(
object.type().id()==
"#REF#")
311 assert(
object.
id()==ID_symbol);
313 const irep_idt &ident =
object.get(ID_identifier);
314 valuest::const_iterator v_it =
values.find(ident);
325 if(t_it->second && it->second)
327 *t_it->second += *it->second;
330 t_it->second.reset();
332 flat_map.
write()[t_it->first]=t_it->second;
337 flat_map.
write()[it->first]=it->second;
341 value_set.push_back(
to_expr(*fit));
345 for(std::list<exprt>::const_iterator it=value_set.begin();
348 assert(it->type().id()!=
"#REF");
352 for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
353 std::cout <<
"GET_VALUE_SET: " <<
format(*it) <<
'\n';
372 const std::string &suffix,
373 const typet &original_type,
378 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
format(expr)
380 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
384 if(expr.
type().
id()==
"#REF#")
386 valuest::const_iterator fi =
values.find(expr.
get(ID_identifier));
392 original_type, ns, recursion_set);
401 else if(expr.
id()==ID_unknown || expr.
id()==ID_invalid)
406 else if(expr.
id()==ID_index)
413 type.id()==ID_incomplete_array ||
415 "operand 0 of index expression must be an array");
418 original_type, ns, recursion_set);
422 else if(expr.
id()==ID_member)
431 type.
id()==ID_union ||
432 type.
id()==ID_incomplete_struct ||
433 type.
id()==ID_incomplete_union,
434 "operand 0 of member expression must be struct or union");
436 const std::string &component_name=
440 original_type, ns, recursion_set);
445 else if(expr.
id()==ID_symbol)
450 valuest::const_iterator v_it=
values.find(ident);
457 else if(v_it!=
values.end())
466 else if(expr.
id()==ID_if)
469 throw "if takes three operands";
472 original_type, ns, recursion_set);
474 original_type, ns, recursion_set);
478 else if(expr.
id()==ID_address_of)
481 throw expr.
id_string()+
" expected to have one operand";
487 else if(expr.
id()==ID_dereference)
493 if(object_map.
begin()!=object_map.
end())
499 original_type, ns, recursion_set);
505 else if(expr.
id()==
"reference_to")
513 if(object_map.
begin()!=object_map.
end())
519 original_type, ns, recursion_set);
528 if(expr.
get(ID_value)==ID_NULL &&
529 expr.
type().
id()==ID_pointer)
535 else if(expr.
id()==ID_typecast)
538 throw "typecast takes one operand";
541 original_type, ns, recursion_set);
545 else if(expr.
id()==ID_plus || expr.
id()==ID_minus)
548 throw expr.
id_string()+
" expected to have at least two operands";
550 if(expr.
type().
id()==ID_pointer)
553 const exprt *ptr_operand=
nullptr;
556 if(it->type().id()==ID_pointer)
558 if(ptr_operand==
nullptr)
561 throw "more than one pointer operand in pointer arithmetic";
564 if(ptr_operand==
nullptr)
565 throw "pointer type sum expected to have pointer operand";
569 ptr_operand->
type(), ns, recursion_set);
583 *offset = (expr.
id() == ID_plus) ? i : -i;
591 *offset = (expr.
id() == ID_plus) ? i : -i;
597 insert(dest, it->first, offset);
603 else if(expr.
id()==ID_side_effect)
607 if(statement==ID_function_call)
610 throw "unexpected function_call sideeffect";
612 else if(statement==ID_allocate)
614 if(expr.
type().
id()!=ID_pointer)
615 throw "malloc expected to return pointer type";
619 const typet &dynamic_type=
620 static_cast<const typet &
>(expr.
find(ID_C_cxx_alloc_type));
631 else if(statement==ID_cpp_new ||
632 statement==ID_cpp_new_array)
635 assert(expr.
type().
id()==ID_pointer);
646 else if(expr.
id()==ID_struct)
652 else if(expr.
id()==ID_with)
655 throw "unexpected value in get_value_set: "+expr.
id_string();
657 else if(expr.
id()==ID_array_of ||
664 else if(expr.
id()==ID_dynamic_object)
669 const std::string name=
670 "value_set::dynamic_object"+
675 valuest::const_iterator v_it=
values.find(name);
692 if(src.
id()==ID_typecast)
694 assert(src.
type().
id()==ID_pointer);
697 throw "typecast expects one operand";
717 if(
object.type().id() ==
"#REF#")
719 const irep_idt &ident =
object.get(ID_identifier);
720 valuest::const_iterator vit =
values.find(ident);
725 dest.insert(
exprt(ID_unknown,
object.type()));
736 if(t_it->second && it->second)
738 *t_it->second += *it->second;
741 t_it->second.reset();
744 for(
const auto &o : omt.
read())
771 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
format(expr)
775 if(expr.
type().
id()==
"#REF#")
777 valuest::const_iterator fi =
values.find(expr.
get(ID_identifier));
785 else if(expr.
id()==ID_symbol ||
786 expr.
id()==ID_dynamic_object ||
787 expr.
id()==ID_string_constant)
789 if(expr.
type().
id()==ID_array &&
797 else if(expr.
id()==ID_dereference)
800 throw expr.
id_string()+
" expected to have one operand";
810 if(obj.
type().
id()==
"#REF#")
813 valuest::const_iterator v_it =
values.find(ident);
824 if(t_it->second && it->second)
826 *t_it->second += *it->second;
829 t_it->second.reset();
843 for(expr_sett::const_iterator it=value_set.begin();
846 std::cout <<
"VALUE_SET: " <<
format(*it) <<
'\n';
851 else if(expr.
id()==ID_index)
854 throw "index expected to have two operands";
860 assert(array_type.
id()==ID_array ||
861 array_type.
id()==ID_incomplete_array);
872 if(
object.
id()==ID_unknown)
880 if(
object.type().id()!=
"#REF#" &&
881 ns.
follow(
object.type())!=array_type)
895 insert(dest, index_expr, o);
901 else if(expr.
id()==ID_member)
903 const irep_idt &component_name=expr.
get(ID_component_name);
906 throw "member expected to have one operand";
918 if(
object.
id()==ID_unknown)
920 else if(
object.
id()==ID_dynamic_object &&
921 obj_type.
id()!=ID_struct &&
922 obj_type.
id()!=ID_union)
938 insert(dest, member_expr, o);
944 else if(expr.
id()==ID_if)
947 throw "if takes three operands";
963 std::cout <<
"ASSIGN LHS: " <<
format(lhs) <<
'\n';
964 std::cout <<
"ASSIGN RHS: " <<
format(rhs) <<
'\n';
970 throw "if takes three operands";
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)
1025 const exprt &member_operand=rhs.
op1();
1028 member_operand.get(ID_component_name);
1030 if(component_name==name)
1033 rhs_member=rhs.
op2();
1038 rhs_member=
exprt(ID_member, subtype);
1040 rhs_member.
set(ID_component_name, name);
1045 rhs_member=
exprt(ID_member, subtype);
1047 rhs_member.
set(ID_component_name, name);
1050 assign(lhs_member, rhs_member, ns);
1054 else if(type.
id()==ID_array)
1059 if(rhs.
id()==ID_unknown ||
1060 rhs.
id()==ID_invalid)
1071 throw "value_set_fit::assign type mismatch: " 1075 if(rhs.
id()==ID_array_of)
1080 else if(rhs.
id()==ID_array ||
1081 rhs.
id()==ID_constant)
1085 assign(lhs_index, *o_it, ns);
1088 else if(rhs.
id()==ID_with)
1095 assign(lhs_index, op0_index, ns);
1102 assign(lhs_index, rhs_index, ns);
1121 const std::string &suffix,
1126 std::cout <<
"ASSIGN_REC LHS: " <<
format(lhs) <<
'\n';
1127 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1130 it!=values_rhs.
read().
end(); it++)
1131 std::cout <<
"ASSIGN_REC RHS: " <<
to_expr(it) <<
'\n';
1134 if(lhs.
type().
id()==
"#REF#")
1141 if(recursion_set.find(ident)!=recursion_set.end())
1143 recursion_set.insert(ident);
1148 suffix, ns, recursion_set);
1150 recursion_set.erase(ident);
1153 else if(lhs.
id()==ID_symbol)
1158 "value_set::dynamic_object") ||
1160 "value_set::return_value") ||
1170 else if(lhs.
id()==ID_dynamic_object)
1175 const std::string name=
1176 "value_set::dynamic_object"+
1182 else if(lhs.
id()==ID_dereference)
1185 throw lhs.
id_string()+
" expected to have one operand";
1194 if(
object.
id()!=ID_unknown)
1195 assign_rec(
object, values_rhs, suffix, ns, recursion_set);
1198 else if(lhs.
id()==ID_index)
1201 throw "index expected to have two operands";
1206 type.
id()==ID_incomplete_array ||
1208 "operand 0 of index expression must be an array");
1210 assign_rec(lhs.
op0(), values_rhs,
"[]"+suffix, ns, recursion_set);
1212 else if(lhs.
id()==ID_member)
1215 throw "member expected to have one operand";
1220 const std::string &component_name=lhs.
get_string(ID_component_name);
1225 type.
id()==ID_union ||
1226 type.
id()==ID_incomplete_struct ||
1227 type.
id()==ID_incomplete_union,
1228 "operand 0 of member expression must be struct or union");
1230 assign_rec(lhs.
op0(), values_rhs,
"."+component_name+suffix,
1233 else if(lhs.
id()==
"valid_object" ||
1234 lhs.
id()==
"dynamic_size" ||
1235 lhs.
id()==
"dynamic_type")
1239 else if(lhs.
id()==ID_string_constant)
1244 else if(lhs.
id() == ID_null_object)
1248 else if(lhs.
id()==ID_typecast)
1252 assign_rec(typecast_expr.
op(), values_rhs, suffix, ns, recursion_set);
1254 else if(lhs.
id()==
"zero_string" ||
1255 lhs.
id()==
"is_zero_string" ||
1256 lhs.
id()==
"zero_string_length")
1260 else if(lhs.
id()==ID_byte_extract_little_endian ||
1261 lhs.
id()==ID_byte_extract_big_endian)
1264 assign_rec(lhs.
op0(), values_rhs, suffix, ns, recursion_set);
1267 throw "assign NYI: `"+lhs.
id_string()+
"'";
1285 for(std::size_t i=0; i<arguments.size(); i++)
1287 const std::string identifier=
"value_set::" +
id2string(
function) +
"::" +
1290 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1291 assign(dummy_lhs, arguments[i], ns);
1298 for(code_typet::parameterst::const_iterator
1299 it=parameter_types.begin();
1300 it!=parameter_types.end();
1303 const irep_idt &identifier=it->get_identifier();
1304 if(identifier.
empty())
1314 assign(actual_lhs, v_expr, ns);
1338 if(statement==ID_block)
1343 else if(statement==ID_function_call)
1348 else if(statement==ID_assign)
1351 throw "assignment expected to have two operands";
1355 else if(statement==ID_decl)
1358 throw "decl expected to have one operand";
1362 if(lhs.
id()!=ID_symbol)
1363 throw "decl expected to have symbol on lhs";
1367 else if(statement==ID_expression)
1371 else if(statement==ID_cpp_delete ||
1372 statement==ID_cpp_delete_array)
1376 else if(statement==
"lock" || statement==
"unlock")
1380 else if(statement==ID_asm)
1384 else if(statement==ID_nondet)
1388 else if(statement==ID_printf)
1392 else if(statement==ID_return)
1402 else if(statement==ID_fence)
1405 else if(statement==ID_array_copy ||
1406 statement==ID_array_replace ||
1407 statement==ID_array_set)
1410 else if(statement==ID_input || statement==ID_output)
1417 "value_set_fit: unexpected statement: "+
id2string(statement);
The type of an expression, extends irept.
irep_idt name
The unique identifier.
void output(const namespacet &ns, std::ostream &out) const
data_typet::value_type value_type
Semantic type conversion.
const std::string & id2string(const irep_idt &d)
const std::string integer2string(const mp_integer &n, unsigned base)
std::unordered_set< idt, string_hash > flatten_seent
std::unordered_set< exprt, irep_hash > expr_sett
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast an exprt to a dynamic_object_exprt.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
std::unordered_map< idt, entryt, string_hash > valuest
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
const irep_idt & get_identifier() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< parametert > parameterst
const componentst & components() const
static const char * alloc_adapter_prefix
exprt to_expr(const object_map_dt::value_type &it) const
Value Set (Flow Insensitive, Sharing)
typet & type()
Return the type of the expression.
static const object_map_dt blank
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
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
void apply_code(const exprt &code, const namespacet &ns)
Extract member of struct or union.
std::unordered_set< idt, string_hash > gvs_recursion_sett
const irep_idt & id() const
bool make_union(object_mapt &dest, const object_mapt &src) const
void flatten_rec(const entryt &, object_mapt &, flatten_seent &) const
The Boolean constant true.
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
#define Forall_objects(it, map)
static object_numberingt object_numbering
API to expression classes.
void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, assign_recursion_sett &recursion_set)
const irep_idt & get(const irep_namet &name) const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
entryt & get_entry(const idt &id, const std::string &suffix)
bool has_prefix(const std::string &s, const std::string &prefix)
Split an expression into a base object and a (byte) offset.
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bitvector_typet index_type()
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void get_value_set(const exprt &expr, std::list< exprt > &dest, const namespacet &ns) const
Operator to return the address of an object.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
void flatten(const entryt &e, object_mapt &dest) const
bool is_constant() const
Return whether the expression is a constant.
std::vector< exprt > operandst
const irep_idt & display_name() const
Return language specific display name if present.
void do_end_function(const exprt &lhs, const namespacet &ns)
typet type
Type of symbol.
Base type for structs and unions.
std::unordered_set< idt, string_hash > assign_recursion_sett
void get_reference_set_sharing(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
data_typet::const_iterator const_iterator
Base class for all expressions.
const parameterst & parameters() const
data_typet::iterator iterator
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
void dereference_rec(const exprt &src, exprt &dest) const
static hash_numbering< irep_idt, irep_id_hash > function_numbering
bool offset_is_zero(const offsett &offset) const
#define UNREACHABLE
This should be used to mark dead code.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const std::string & get_string(const irep_namet &name) const
const std::string & id_string() const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns)
bool is_zero() const
Return whether the expression is a constant representing 0.
void add_var(const idt &id, const std::string &suffix)
Expression to hold a symbol (variable)
exprt dynamic_object(const exprt &pointer)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
Representation of heap-allocated objects.
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
const irept & find(const irep_namet &name) const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void set(const irep_namet &name, const irep_idt &value)
unsigned from_target_index
#define forall_objects(it, map)
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value...
bool simplify(exprt &expr, const namespacet &ns)