34 #define forall_objects(it, map) \ 35 for(object_map_dt::const_iterator (it) = (map).begin(); \ 39 #define Forall_objects(it, map) \ 40 for(object_map_dt::iterator (it) = (map).begin(); \ 46 std::ostream &out)
const 48 for(valuest::const_iterator
55 const entryt &e=v_it->second;
67 identifier=symbol.
name;
89 if(o.
id()==ID_invalid || o.
id()==ID_unknown)
94 if(o.
type().
id()==ID_unknown)
102 result=
"<"+
from_expr(ns, identifier, o)+
", ";
104 if(o_it->second.offset_is_set)
111 if(o.
type().
id()==ID_unknown)
121 width+=result.size();
123 object_map_dt::const_iterator next(o_it);
126 if(next!=object_map.
read().end())
150 std::cout <<
"FLATTEN: Done.\n";
164 assert(seen.find(identifier + e.
suffix)==seen.end());
166 bool generalize_index =
false;
168 seen.insert(identifier + e.
suffix);
174 if(o.
type().
id()==
"#REF#")
176 if(seen.find(o.
get(ID_identifier))!=seen.end())
178 generalize_index =
true;
182 valuest::const_iterator fi =
values.find(o.
get(ID_identifier));
187 se.
set(ID_identifier, o.
get(ID_identifier));
195 for(object_map_dt::iterator t_it=temp.
write().begin();
196 t_it!=temp.
write().end();
199 if(t_it->second.offset_is_set &&
200 it->second.offset_is_set)
202 t_it->second.offset += it->second.offset;
205 t_it->second.offset_is_set=
false;
219 it->second.offset_is_set =
false;
222 seen.erase(identifier + e.
suffix);
229 if(
object.
id()==ID_invalid ||
230 object.
id()==ID_unknown)
237 if(it->second.offset_is_set)
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,
310 if(
object.type().id()==
"#REF#")
312 assert(
object.
id()==ID_symbol);
314 const irep_idt &ident =
object.get(ID_identifier);
315 valuest::const_iterator v_it =
values.find(ident);
322 for(object_map_dt::iterator t_it=temp.
write().begin();
323 t_it!=temp.
write().end();
326 if(t_it->second.offset_is_set &&
327 it->second.offset_is_set)
329 t_it->second.offset += it->second.offset;
332 t_it->second.offset_is_set=
false;
334 flat_map.
write()[t_it->first]=t_it->second;
339 flat_map.
write()[it->first]=it->second;
343 value_set.push_back(
to_expr(fit));
347 for(std::list<exprt>::const_iterator it=value_set.begin();
350 assert(it->type().id()!=
"#REF");
354 for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
355 std::cout <<
"GET_VALUE_SET: " <<
from_expr(ns,
"", *it) <<
'\n';
374 const std::string &suffix,
375 const typet &original_type,
380 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
from_expr(ns,
"", expr)
382 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
386 if(expr.
type().
id()==
"#REF#")
388 valuest::const_iterator fi =
values.find(expr.
get(ID_identifier));
394 original_type, ns, recursion_set);
403 else if(expr.
id()==ID_unknown || expr.
id()==ID_invalid)
408 else if(expr.
id()==ID_index)
414 assert(type.id()==ID_array ||
415 type.id()==ID_incomplete_array ||
419 original_type, ns, recursion_set);
423 else if(expr.
id()==ID_member)
431 assert(type.
id()==ID_struct ||
432 type.
id()==ID_union ||
433 type.
id()==ID_incomplete_struct ||
434 type.
id()==ID_incomplete_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);
575 if(
object.offset_is_zero() &&
584 object.offset=(expr.
id()==ID_plus)? i : -i;
590 object.offset_is_set=
false;
592 object.offset=(expr.
id()==ID_plus)? i : -i;
596 object.offset_is_set=
false;
598 insert(dest, it->first,
object);
604 else if(expr.
id()==ID_side_effect)
608 if(statement==ID_function_call)
611 throw "unexpected function_call sideeffect";
613 else if(statement==ID_malloc)
615 if(expr.
type().
id()!=ID_pointer)
616 throw "malloc expected to return pointer type";
620 const typet &dynamic_type=
621 static_cast<const typet &
>(expr.
find(ID_C_cxx_alloc_type));
632 else if(statement==ID_cpp_new ||
633 statement==ID_cpp_new_array)
636 assert(expr.
type().
id()==ID_pointer);
647 else if(expr.
id()==ID_struct)
653 else if(expr.
id()==ID_with)
656 throw "unexpected value in get_value_set: "+expr.
id_string();
658 else if(expr.
id()==ID_array_of ||
665 else if(expr.
id()==ID_dynamic_object)
670 const std::string name=
671 "value_set::dynamic_object"+
676 valuest::const_iterator v_it=
values.find(name);
693 if(src.
id()==ID_typecast)
695 assert(src.
type().
id()==ID_pointer);
698 throw "typecast expects one operand";
718 if(expr.
type().
id()==
"#REF#")
721 valuest::const_iterator vit =
values.find(ident);
726 dest.insert(
exprt(ID_unknown, expr.
type()));
733 for(object_map_dt::iterator t_it=omt.
write().begin();
734 t_it!=omt.
write().end();
737 if(t_it->second.offset_is_set &&
738 it->second.offset_is_set)
740 t_it->second.offset += it->second.offset;
743 t_it->second.offset_is_set=
false;
773 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
from_expr(ns,
"", 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)
802 throw expr.
id_string()+
" expected to have one operand";
812 if(obj.
type().
id()==
"#REF#")
815 valuest::const_iterator v_it =
values.find(ident);
822 for(object_map_dt::iterator t_it=t2.
write().begin();
823 t_it!=t2.
write().end();
826 if(t_it->second.offset_is_set &&
827 it->second.offset_is_set)
829 t_it->second.offset += it->second.offset;
832 t_it->second.offset_is_set=
false;
846 for(expr_sett::const_iterator it=value_set.begin();
849 std::cout <<
"VALUE_SET: " <<
from_expr(ns,
"", *it) <<
'\n';
854 else if(expr.
id()==ID_index)
857 throw "index expected to have two operands";
863 assert(array_type.
id()==ID_array ||
864 array_type.
id()==ID_incomplete_array);
875 if(
object.
id()==ID_unknown)
881 index_expr.op0()=object;
885 if(
object.type().
id()!=
"#REF#" &&
886 ns.
follow(
object.type())!=array_type)
887 index_expr.make_typecast(array.
type());
901 insert(dest, index_expr, o);
907 else if(expr.
id()==ID_member)
909 const irep_idt &component_name=expr.
get(ID_component_name);
912 throw "member expected to have one operand";
924 if(
object.
id()==ID_unknown)
926 else if(
object.
id()==ID_dynamic_object &&
927 obj_type.
id()!=ID_struct &&
928 obj_type.
id()!=ID_union)
938 exprt member_expr(ID_member, expr.
type());
940 member_expr.set(ID_component_name, component_name);
944 member_expr.op0().make_typecast(struct_op.
type());
946 insert(dest, member_expr, o);
952 else if(expr.
id()==ID_if)
955 throw "if takes three operands";
971 std::cout <<
"ASSIGN LHS: " <<
from_expr(ns,
"", lhs) <<
'\n';
972 std::cout <<
"ASSIGN RHS: " <<
from_expr(ns,
"", rhs) <<
'\n';
978 throw "if takes three operands";
987 if(type.
id()==ID_struct ||
994 for(struct_typet::componentst::const_iterator
999 const typet &subtype=c_it->type();
1000 const irep_idt &name=c_it->get(ID_name);
1003 if(subtype.
id()==ID_code)
1006 exprt lhs_member(ID_member, subtype);
1007 lhs_member.
set(ID_component_name, name);
1012 if(rhs.
id()==ID_unknown ||
1013 rhs.
id()==ID_invalid)
1015 rhs_member=
exprt(rhs.
id(), subtype);
1020 throw "value_set_fit::assign type mismatch: " 1024 if(rhs.
id()==ID_struct ||
1025 rhs.
id()==ID_constant)
1030 else if(rhs.
id()==ID_with)
1035 const exprt &member_operand=rhs.
op1();
1038 member_operand.get(ID_component_name);
1040 if(component_name==name)
1043 rhs_member=rhs.
op2();
1048 rhs_member=
exprt(ID_member, subtype);
1050 rhs_member.
set(ID_component_name, name);
1055 rhs_member=
exprt(ID_member, subtype);
1057 rhs_member.
set(ID_component_name, name);
1060 assign(lhs_member, rhs_member, ns);
1064 else if(type.
id()==ID_array)
1069 if(rhs.
id()==ID_unknown ||
1070 rhs.
id()==ID_invalid)
1081 throw "value_set_fit::assign type mismatch: " 1085 if(rhs.
id()==ID_array_of)
1090 else if(rhs.
id()==ID_array ||
1091 rhs.
id()==ID_constant)
1095 assign(lhs_index, *o_it, ns);
1098 else if(rhs.
id()==ID_with)
1105 assign(lhs_index, op0_index, ns);
1112 assign(lhs_index, rhs_index, ns);
1133 if(op.
type().
id()!=ID_pointer)
1134 throw "free expected to have pointer-type operand";
1152 if(
object.
id()==ID_dynamic_object)
1164 for(valuest::iterator v_it=
values.begin();
1171 v_it->second.object_map.read();
1179 if(
object.
id()==ID_dynamic_object)
1185 set(new_object_map, o_it);
1192 insert(new_object_map, tmp, o);
1197 set(new_object_map, o_it);
1201 v_it->second.object_map=new_object_map;
1208 const std::string &suffix,
1213 std::cout <<
"ASSIGN_REC LHS: " <<
from_expr(ns,
"", lhs) <<
'\n';
1214 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1216 for(object_map_dt::const_iterator it=values_rhs.
read().begin();
1217 it!=values_rhs.
read().end(); it++)
1218 std::cout <<
"ASSIGN_REC RHS: " <<
to_expr(it) <<
'\n';
1221 if(lhs.
type().
id()==
"#REF#")
1228 if(recursion_set.find(ident)!=recursion_set.end())
1230 recursion_set.insert(ident);
1235 suffix, ns, recursion_set);
1237 recursion_set.erase(ident);
1240 else if(lhs.
id()==ID_symbol)
1242 const irep_idt &identifier=lhs.
get(ID_identifier);
1245 "value_set::dynamic_object") ||
1247 "value_set::return_value") ||
1257 else if(lhs.
id()==ID_dynamic_object)
1262 const std::string name=
1263 "value_set::dynamic_object"+
1269 else if(lhs.
id()==ID_dereference)
1272 throw lhs.
id_string()+
" expected to have one operand";
1281 if(
object.
id()!=ID_unknown)
1282 assign_rec(
object, values_rhs, suffix, ns, recursion_set);
1285 else if(lhs.
id()==ID_index)
1288 throw "index expected to have two operands";
1292 assert(type.
id()==ID_array ||
1293 type.
id()==ID_incomplete_array ||
1294 type.
id()==
"#REF#");
1296 assign_rec(lhs.
op0(), values_rhs,
"[]"+suffix, ns, recursion_set);
1298 else if(lhs.
id()==ID_member)
1301 throw "member expected to have one operand";
1306 const std::string &component_name=lhs.
get_string(ID_component_name);
1310 assert(type.
id()==ID_struct ||
1311 type.
id()==ID_union ||
1312 type.
id()==ID_incomplete_struct ||
1313 type.
id()==ID_incomplete_union);
1315 assign_rec(lhs.
op0(), values_rhs,
"."+component_name+suffix,
1318 else if(lhs.
id()==
"valid_object" ||
1319 lhs.
id()==
"dynamic_size" ||
1320 lhs.
id()==
"dynamic_type")
1324 else if(lhs.
id()==ID_string_constant)
1329 else if(lhs.
id()==
"NULL-object")
1333 else if(lhs.
id()==ID_typecast)
1337 assign_rec(typecast_expr.
op(), values_rhs, suffix, ns, recursion_set);
1339 else if(lhs.
id()==
"zero_string" ||
1340 lhs.
id()==
"is_zero_string" ||
1341 lhs.
id()==
"zero_string_length")
1345 else if(lhs.
id()==ID_byte_extract_little_endian ||
1346 lhs.
id()==ID_byte_extract_big_endian)
1349 assign_rec(lhs.
op0(), values_rhs, suffix, ns, recursion_set);
1352 throw "assign NYI: `"+lhs.
id_string()+
"'";
1370 for(
unsigned i=0; i<arguments.size(); i++)
1372 const std::string identifier=
"value_set::" +
id2string(
function) +
"::" +
1373 "argument$"+std::to_string(i);
1376 assign(dummy_lhs, arguments[i], ns);
1383 for(code_typet::parameterst::const_iterator
1384 it=parameter_types.begin();
1385 it!=parameter_types.end();
1388 const irep_idt &identifier=it->get_identifier();
1389 if(identifier.
empty())
1396 "argument$"+std::to_string(i), it->type());
1399 assign(actual_lhs, v_expr, ns);
1411 std::string rvs =
"value_set::return_value" + std::to_string(
from_function);
1423 if(statement==ID_block)
1428 else if(statement==ID_function_call)
1433 else if(statement==ID_assign ||
1437 throw "assignment expected to have two operands";
1441 else if(statement==ID_decl)
1444 throw "decl expected to have one operand";
1448 if(lhs.
id()!=ID_symbol)
1449 throw "decl expected to have symbol on lhs";
1453 else if(statement==ID_specc_notify ||
1454 statement==ID_specc_wait)
1458 else if(statement==ID_expression)
1462 else if(statement==ID_cpp_delete ||
1463 statement==ID_cpp_delete_array)
1467 else if(statement==ID_free)
1472 throw "free expected to have one operand";
1476 else if(statement==
"lock" || statement==
"unlock")
1480 else if(statement==ID_asm)
1484 else if(statement==ID_nondet)
1488 else if(statement==ID_printf)
1492 else if(statement==ID_return)
1497 std::string rvs=
"value_set::return_value"+std::to_string(
from_function);
1502 else if(statement==ID_fence)
1505 else if(statement==ID_array_copy ||
1506 statement==ID_array_replace ||
1507 statement==ID_array_set)
1510 else if(statement==ID_input || statement==ID_output)
1517 "value_set_fit: unexpected statement: "+
id2string(statement);
The type of an expression.
irep_idt name
The unique identifier.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
void output(const namespacet &ns, std::ostream &out) const
const typet & follow(const typet &src) const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
std::unordered_set< unsigned int > dynamic_object_id_sett
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
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
void do_free(const exprt &op, const namespacet &ns)
std::unordered_map< idt, entryt, string_hash > valuest
void copy_to_operands(const exprt &expr)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::vector< parametert > parameterst
exprt to_expr(object_map_dt::const_iterator it) const
const componentst & components() const
static const char * alloc_adapter_prefix
Value Set (Flow Insensitive, Sharing)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
static const object_map_dt blank
void get_reference_set_sharing_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) 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)
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
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
entryt & get_entry(const idt &id, const std::string &suffix)
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)
bitvector_typet index_type()
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
std::vector< exprt > operandst
bool has_prefix(const std::string &s, const std::string &prefix)
const irep_idt & display_name() const
void do_end_function(const exprt &lhs, const namespacet &ns)
typet type
Type of symbol.
Base type of C structs and unions, and C++ classes.
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
Base class for all expressions.
const parameterst & parameters() const
void dereference_rec(const exprt &src, exprt &dest) const
static hash_numbering< irep_idt, irep_id_hash > function_numbering
const std::string & get_string(const irep_namet &name) const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const std::string & id_string() const
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns)
void add_var(const idt &id, const std::string &suffix)
bool offset_is_zero() const
Expression to hold a symbol (variable)
exprt dynamic_object(const exprt &pointer)
bool insert(object_mapt &dest, object_map_dt::const_iterator it) const
const typet & subtype() const
const irept & find(const irep_namet &name) const
void set(const irep_namet &name, const irep_idt &value)
unsigned from_target_index
#define forall_objects(it, map)
bool simplify(exprt &expr, const namespacet &ns)