46 id==
"value_set::return_value" ||
47 id==
"value_set::memory")
51 return ns.
follow(type).
id()==ID_struct;
66 std::pair<valuest::iterator, bool>
r=
67 values.insert(std::pair<idt, entryt>(index, e));
69 return r.first->second;
82 dest.
write()[n] = offset;
85 else if(!entry->second)
87 else if(offset && *entry->second == *offset)
91 dest.
write()[n].reset();
98 std::ostream &out)
const 100 for(valuest::const_iterator
107 const entryt &e=v_it->second;
114 else if(e.
identifier==
"value_set::return_value")
116 display_name=
"RETURN_VALUE"+e.
suffix;
124 identifier=symbol.
name;
140 o_it=object_map.
begin();
141 o_it!=object_map.
end();
148 if(o.
id()==ID_invalid || o.
id()==ID_unknown)
152 result=
"<"+
from_expr(ns, identifier, o)+
", ";
169 width+=result.size();
174 if(next!=object_map.
end())
190 if(
object.
id()==ID_invalid ||
191 object.
id()==ID_unknown)
210 valuest::iterator v_it=
values.begin();
212 for(valuest::const_iterator
213 it=new_values.begin();
214 it!=new_values.end();
217 if(v_it==
values.end() || it->first<v_it->first)
224 else if(v_it->first<it->first)
230 assert(v_it->first==it->first);
233 const entryt &new_e=it->second;
266 if(expr.
id()==ID_pointer_offset)
278 it=object_map.
begin();
279 it!=object_map.
end();
291 ptr_offset += *it->second;
293 if(mod && ptr_offset!=previous_offset)
297 previous_offset=ptr_offset;
328 for(value_setst::valuest::const_iterator it=dest.begin();
329 it!=dest.end(); it++)
330 std::cout <<
"GET_VALUE_SET: " <<
format(*it) <<
'\n';
338 bool is_simplified)
const 350 const std::string &suffix,
351 const typet &original_type,
355 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
format(expr) <<
"\n";
356 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
361 if(expr.
id()==ID_unknown || expr.
id()==ID_invalid)
365 else if(expr.
id()==ID_index)
372 type.id()==ID_incomplete_array,
373 "operand 0 of index expression must be an array");
377 else if(expr.
id()==ID_member)
384 type.id()==ID_union ||
385 type.id()==ID_incomplete_struct ||
386 type.id()==ID_incomplete_union,
387 "operand 0 of member expression must be struct or union");
389 const std::string &component_name=
393 "."+component_name+suffix, original_type, ns);
395 else if(expr.
id()==ID_symbol)
400 if(expr_type.
id()==ID_pointer ||
401 expr_type.
id()==ID_signedbv ||
402 expr_type.
id()==ID_unsignedbv ||
403 expr_type.
id()==ID_struct ||
404 expr_type.
id()==ID_union ||
405 expr_type.
id()==ID_array)
408 valuest::const_iterator v_it=
413 (expr_type.
id()==ID_struct ||
414 expr_type.
id()==ID_union))
419 const std::string first_component_name=
420 struct_union_type.
components().front().get_string(ID_name);
423 id2string(identifier)+
"."+first_component_name+suffix);
428 v_it=
values.find(identifier);
438 else if(expr.
id()==ID_if)
441 throw "if takes three operands";
446 else if(expr.
id()==ID_address_of)
449 throw expr.
id_string()+
" expected to have one operand";
453 else if(expr.
id()==ID_dereference)
459 if(object_map.
begin()==object_map.
end())
464 it1=object_map.
begin();
465 it1!=object_map.
end();
475 else if(expr.
id()==
"reference_to")
484 if(object_map.
begin()==object_map.
end())
489 it=object_map.
begin();
490 it!=object_map.
end();
503 if(expr.
get(ID_value)==ID_NULL &&
504 expr_type.
id()==ID_pointer)
508 else if(expr_type.
id()==ID_unsignedbv ||
509 expr_type.
id()==ID_signedbv)
517 else if(expr.
id()==ID_typecast)
520 throw "typecast takes one operand";
526 if(op_type.
id()==ID_pointer)
531 else if(op_type.
id()==ID_unsignedbv ||
532 op_type.
id()==ID_signedbv)
566 else if(expr.
id()==ID_plus ||
570 throw expr.
id_string()+
" expected to have at least two operands";
579 expr_type.
id()==ID_pointer)
587 ptr_operand=expr.
op1();
592 ptr_operand=expr.
op0();
598 if(pointer_sub_type.
id()==ID_empty)
611 if(expr.
id()==ID_minus)
617 ptr_operand, pointer_expr_set,
"", ptr_operand.
type(), ns);
625 *it, pointer_expr_set,
"", it->type(), ns);
631 it!=pointer_expr_set.
read().
end();
637 if(offset && i_is_set)
642 insert(dest, it->first, offset);
645 else if(expr.
id()==ID_mult)
651 throw expr.
id_string()+
" expected to have at least two operands";
659 *it, pointer_expr_set,
"", it->type(), ns);
664 it!=pointer_expr_set.
read().
end();
672 insert(dest, it->first, offset);
675 else if(expr.
id()==ID_side_effect)
679 if(statement==ID_function_call)
682 throw "unexpected function_call sideeffect";
684 else if(statement==ID_allocate)
688 const typet &dynamic_type=
689 static_cast<const typet &
>(expr.
find(ID_C_cxx_alloc_type));
697 else if(statement==ID_cpp_new ||
698 statement==ID_cpp_new_array)
701 assert(expr_type.
id()==ID_pointer);
712 else if(expr.
id()==ID_struct)
718 else if(expr.
id()==ID_with)
730 if(expr_type.
id()==ID_struct)
739 it=object_map0.
begin();
740 it!=object_map0.
end();
745 if(e.
id()==ID_member &&
746 e.
get(ID_component_name)==component_name)
750 dest.
write().
insert(tmp_map2.read().begin(), tmp_map2.read().end());
769 else if(expr.
id()==ID_array)
775 else if(expr.
id()==ID_array_of)
781 else if(expr.
id()==ID_dynamic_object)
786 const std::string prefix=
787 "value_set::dynamic_object"+
791 const std::string full_name=prefix+suffix;
794 valuest::const_iterator v_it=
values.find(full_name);
805 else if(expr.
id()==ID_byte_extract_little_endian ||
806 expr.
id()==ID_byte_extract_big_endian)
809 throw "byte_extract takes two operands";
819 if(!
to_integer(op1, op1_offset) && op0_type.
id()==ID_struct)
823 for(struct_union_typet::componentst::const_iterator
825 !found && c_it!=struct_type.
components().end();
828 const irep_idt &name=c_it->get_name();
832 if(comp_offset>op1_offset)
834 else if(comp_offset!=op1_offset)
844 if(op0_type.
id()==ID_union)
849 for(union_typet::componentst::const_iterator
853 const irep_idt &name=c_it->get_name();
863 else if(expr.
id()==ID_byte_update_little_endian ||
864 expr.
id()==ID_byte_update_big_endian)
867 throw "byte_update takes three operands";
878 std::cout <<
"WARNING: not doing " << expr.
id() <<
'\n';
883 std::cout <<
"GET_VALUE_SET_REC RESULT:\n";
884 for(
const auto &obj : dest.
read())
887 std::cout <<
" " <<
format(e) <<
"\n";
898 if(src.
id()==ID_typecast)
900 assert(src.
type().
id()==ID_pointer);
903 throw "typecast expects one operand";
932 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
format(expr)
936 if(expr.
id()==ID_symbol ||
937 expr.
id()==ID_dynamic_object ||
938 expr.
id()==ID_string_constant ||
941 if(expr.
type().
id()==ID_array &&
949 else if(expr.
id()==ID_dereference)
952 throw expr.
id_string()+
" expected to have one operand";
957 for(expr_sett::const_iterator it=value_set.begin();
958 it!=value_set.end(); it++)
959 std::cout <<
"VALUE_SET: " <<
format(*it) <<
'\n';
964 else if(expr.
id()==ID_index)
967 throw "index expected to have two operands";
974 assert(array_type.
id()==ID_array ||
975 array_type.
id()==ID_incomplete_array);
983 a_it=object_map.
begin();
984 a_it!=object_map.
end();
989 if(
object.
id()==ID_unknown)
994 index_expr.
array()=object;
998 if(ns.
follow(
object.type())!=array_type)
1019 insert(dest, index_expr, o);
1025 else if(expr.
id()==ID_member)
1027 const irep_idt &component_name=expr.
get(ID_component_name);
1030 throw "member expected to have one operand";
1040 it=object_map.
begin();
1041 it!=object_map.
end();
1046 if(
object.
id()==ID_unknown)
1057 const typet &final_object_type = ns.
follow(
object.type());
1059 if(final_object_type.id()==ID_struct ||
1060 final_object_type.id()==ID_union)
1063 if(ns.
follow(struct_op.
type())!=final_object_type)
1064 member_expr.op0().make_typecast(struct_op.
type());
1066 insert(dest, member_expr, o);
1075 else if(expr.
id()==ID_if)
1078 throw "if takes three operands";
1096 std::cout <<
"ASSIGN LHS: " <<
format(lhs) <<
" : " 1098 std::cout <<
"ASSIGN RHS: " <<
format(rhs) <<
" : " 1100 std::cout <<
"--------------------------------------------\n";
1106 if(type.
id()==ID_struct ||
1107 type.
id()==ID_union)
1112 for(struct_union_typet::componentst::const_iterator
1117 const typet &subtype=c_it->type();
1118 const irep_idt &name=c_it->get(ID_name);
1121 if(subtype.
id()==ID_code ||
1122 c_it->get_is_padding())
continue;
1128 if(rhs.
id()==ID_unknown ||
1129 rhs.
id()==ID_invalid)
1131 rhs_member=
exprt(rhs.
id(), subtype);
1136 throw "value_sett::assign type mismatch: " 1142 assign(lhs_member, rhs_member, ns, is_simplified, add_to_sets);
1146 else if(type.
id()==ID_array)
1151 if(rhs.
id()==ID_unknown ||
1152 rhs.
id()==ID_invalid)
1164 throw "value_sett::assign type mismatch: " 1168 if(rhs.
id()==ID_array_of)
1171 assign(lhs_index, rhs.
op0(), ns, is_simplified, add_to_sets);
1173 else if(rhs.
id()==ID_array ||
1174 rhs.
id()==ID_constant)
1178 assign(lhs_index, *o_it, ns, is_simplified, add_to_sets);
1182 else if(rhs.
id()==ID_with)
1189 assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
1190 assign(lhs_index, rhs.
op2(), ns, is_simplified,
true);
1196 assign(lhs_index, rhs_index, ns, is_simplified,
true);
1212 assign_rec(lhs, values_rhs,
"", ns, add_to_sets);
1221 if(op.
type().
id()!=ID_pointer)
1222 throw "free expected to have pointer-type operand";
1234 it=object_map.
begin();
1235 it!=object_map.
end();
1240 if(
object.
id()==ID_dynamic_object)
1252 for(valuest::iterator v_it=
values.begin();
1259 v_it->second.object_map.read();
1264 o_it=old_object_map.
begin();
1265 o_it!=old_object_map.
end();
1270 if(
object.
id()==ID_dynamic_object)
1276 set(new_object_map, *o_it);
1283 insert(new_object_map, tmp, o);
1288 set(new_object_map, *o_it);
1292 v_it->second.object_map=new_object_map;
1299 const std::string &suffix,
1304 std::cout <<
"ASSIGN_REC LHS: " <<
format(lhs) <<
'\n';
1305 std::cout <<
"ASSIGN_REC LHS ID: " << lhs.
id() <<
'\n';
1306 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1311 std::cout <<
"ASSIGN_REC RHS: " <<
1316 if(lhs.
id()==ID_symbol)
1327 else if(lhs.
id()==ID_dynamic_object)
1332 const std::string name=
1333 "value_set::dynamic_object"+
1340 else if(lhs.
id()==ID_dereference)
1343 throw lhs.
id_string()+
" expected to have one operand";
1353 it!=reference_set.
read().
end();
1360 if(
object.
id()!=ID_unknown)
1361 assign_rec(
object, values_rhs, suffix, ns, add_to_sets);
1364 else if(lhs.
id()==ID_index)
1367 throw "index expected to have two operands";
1372 "operand 0 of index expression must be an array");
1376 else if(lhs.
id()==ID_member)
1379 throw "member expected to have one operand";
1381 const std::string &component_name=lhs.
get_string(ID_component_name);
1386 type.
id()==ID_union ||
1387 type.
id()==ID_incomplete_struct ||
1388 type.
id()==ID_incomplete_union,
1389 "operand 0 of member expression must be struct or union");
1392 lhs.
op0(), values_rhs,
"."+component_name+suffix, ns, add_to_sets);
1394 else if(lhs.
id()==
"valid_object" ||
1395 lhs.
id()==
"dynamic_size" ||
1396 lhs.
id()==
"dynamic_type" ||
1397 lhs.
id()==
"is_zero_string" ||
1398 lhs.
id()==
"zero_string" ||
1399 lhs.
id()==
"zero_string_length")
1403 else if(lhs.
id()==ID_string_constant)
1408 else if(lhs.
id() == ID_null_object)
1412 else if(lhs.
id()==ID_typecast)
1416 assign_rec(typecast_expr.
op(), values_rhs, suffix, ns, add_to_sets);
1418 else if(lhs.
id()==ID_byte_extract_little_endian ||
1419 lhs.
id()==ID_byte_extract_big_endian)
1424 else if(lhs.
id()==ID_integer_address)
1430 throw "assign NYI: `"+lhs.
id_string()+
"'";
1448 for(std::size_t i=0; i<arguments.size(); i++)
1450 const std::string identifier=
"value_set::dummy_arg_"+
std::to_string(i);
1451 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1452 assign(dummy_lhs, arguments[i], ns,
false,
false);
1459 for(code_typet::parameterst::const_iterator
1460 it=parameter_types.begin();
1461 it!=parameter_types.end();
1464 const irep_idt &identifier=it->get_identifier();
1472 assign(actual_lhs, v_expr, ns,
true,
true);
1488 assign(lhs, rhs, ns,
false,
false);
1497 if(statement==ID_block)
1502 else if(statement==ID_function_call)
1507 else if(statement==ID_assign ||
1511 throw "assignment expected to have two operands";
1515 else if(statement==ID_decl)
1518 throw "decl expected to have one operand";
1522 if(lhs.
id()!=ID_symbol)
1523 throw "decl expected to have symbol on lhs";
1527 if(lhs_type.
id()==ID_pointer ||
1528 (lhs_type.
id()==ID_array &&
1538 assign(lhs, address_of_expr, ns,
false,
false);
1544 else if(statement==ID_expression)
1548 else if(statement==
"cpp_delete" ||
1549 statement==
"cpp_delete[]")
1553 else if(statement==ID_free)
1558 throw "free expected to have one operand";
1562 else if(statement==
"lock" || statement==
"unlock")
1566 else if(statement==ID_asm)
1570 else if(statement==ID_nondet)
1574 else if(statement==ID_printf)
1578 else if(statement==ID_return)
1584 assign(lhs, code.
op0(), ns,
false,
false);
1587 else if(statement==ID_array_set)
1590 else if(statement==ID_array_copy)
1593 else if(statement==ID_array_replace)
1596 else if(statement==ID_assume)
1600 else if(statement==ID_user_specified_predicate ||
1601 statement==ID_user_specified_parameter_predicates ||
1602 statement==ID_user_specified_return_predicates)
1606 else if(statement==ID_fence)
1609 else if(statement==ID_input || statement==ID_output)
1613 else if(statement==ID_dead)
1620 throw "value_sett: unexpected statement: "+
id2string(statement);
1628 if(expr.
id()==ID_and)
1633 else if(expr.
id()==ID_equal)
1636 else if(expr.
id()==ID_notequal)
1639 else if(expr.
id()==ID_not)
1642 else if(expr.
id()==ID_dynamic_object)
1654 assign(expr.
op0(), address_of, ns,
false,
false);
1666 if(src.
id()==ID_struct ||
1667 src.
id()==ID_constant)
1673 else if(src.
id()==ID_with)
1678 const exprt &member_operand=src.
op1();
1680 if(component_name==member_operand.get(ID_component_name))
1687 else if(src.
id()==ID_typecast)
1696 member_exprt member_expr(src, component_name, subtype);
const irep_idt & get_statement() const
The type of an expression.
irep_idt name
The unique identifier.
const std::string & id2string(const irep_idt &d)
Represents a row of a value_sett.
const std::string integer2string(const mp_integer &n, unsigned base)
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const code_assumet & to_code_assume(const codet &code)
const dynamic_object_exprt & to_dynamic_object_expr(const exprt &expr)
Cast a generic exprt to a dynamic_object_exprt.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
const irep_idt & get_identifier() const
mp_integer member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
void assign(const exprt &lhs, const exprt &rhs, const namespacet &ns, bool is_simplified, bool add_to_sets)
Transforms this value-set by executing executing the assignment lhs := rhs against it...
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
virtual void apply_code_rec(const codet &code, const namespacet &ns)
Subclass customisation point for applying code to this domain:
std::vector< parametert > parameterst
void get_reference_set_rec(const exprt &expr, object_mapt &dest, const namespacet &ns) const
See get_reference_set.
void get_value_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
const componentst & components() const
static const object_map_dt blank
static object_numberingt object_numbering
Global shared object numbering, used to abbreviate expressions stored in value sets.
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
void dereference_rec(const exprt &src, exprt &dest) const
Sets dest to src with any wrapping typecasts removed.
virtual void assign_rec(const exprt &lhs, const object_mapt &values_rhs, const std::string &suffix, const namespacet &ns, bool add_to_sets)
Subclass customisation point for recursion over LHS expression:
mp_integer pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
virtual void apply_assign_side_effects(const exprt &lhs, const exprt &rhs, const namespacet &ns)
Subclass customisation point to apply global side-effects to this domain, after RHS values are read b...
Extract member of struct or union.
static bool field_sensitive(const irep_idt &id, const typet &type, const namespacet &)
const irep_idt & id() const
The boolean constant true.
bool eval_pointer_offset(exprt &expr, const namespacet &ns) const
Tries to resolve any pointer_offset_exprt expressions in expr to constant integers using this value-s...
exprt get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
data_typet::value_type value_type
const irep_idt & get(const irep_namet &name) const
void do_function_call(const irep_idt &function, const exprt::operandst &arguments, const namespacet &ns)
Transforms this value-set by executing the actual -> formal parameter assignments for a particular ca...
bool has_prefix(const std::string &s, const std::string &prefix)
data_typet::const_iterator const_iterator
split an expression into a base object and a (byte) offset
optionalt< mp_integer > offsett
Represents the offset into an object: either a unique integer offset, or an unknown value...
virtual void get_value_set_rec(const exprt &expr, object_mapt &dest, const std::string &suffix, const typet &original_type, const namespacet &ns) const
Subclass customisation point for recursion over RHS expression:
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
typename Map::mapped_type number_type
typet component_type(const irep_idt &component_name) const
Operator to return the address of an object.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
virtual void adjust_assign_rhs_values(const exprt &rhs, const namespacet &ns, object_mapt &rhs_values) const
Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set b...
std::vector< exprt > operandst
const irep_idt & display_name() const
mp_integer compute_pointer_offset(const exprt &expr, const namespacet &ns)
const_iterator find(T &&t) const
bool insert(object_mapt &dest, const object_map_dt::value_type &it) const
Merges an existing entry into an object map.
std::unordered_map< idt, entryt, string_hash > valuest
Map representing the entire value set, mapping from string LHS IDs to RHS expression sets...
typet type
Type of symbol.
void do_end_function(const exprt &lhs, const namespacet &ns)
Transforms this value-set by assigning this function's return value to a given LHS expression...
Base type of C structs and unions, and C++ classes.
void get_reference_set(const exprt &expr, value_setst::valuest &dest, const namespacet &ns) const
Gets the set of expressions that expr may refer to, according to this value set.
Base class for all expressions.
const parameterst & parameters() const
std::size_t component_number(const irep_idt &component_name) const
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
const union_typet & to_union_type(const typet &type)
Cast a generic typet to a union_typet.
std::set< unsigned int > dynamic_object_id_sett
Set of dynamic object numbers, equivalent to a set of dynamic_object_exprts with corresponding IDs...
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
Represents a set of expressions (exprt instances) with corresponding offsets (offsett instances)...
const std::string & get_string(const irep_namet &name) const
const std::string & id_string() const
#define Forall_operands(it, expr)
const codet & to_code(const exprt &expr)
Expression to hold a symbol (variable)
void output(const namespacet &ns, std::ostream &out) const
Pretty-print this value-set.
const pointer_typet & to_pointer_type(const typet &type)
Cast a generic typet to a pointer_typet.
exprt dynamic_object(const exprt &pointer)
A statement in a programming language.
exprt to_expr(const object_map_dt::value_type &it) const
Converts an object_map_dt entry object_number -> offset into an object_descriptor_exprt with ...
unsignedbv_typet unsigned_char_type()
const typet & subtype() const
entryt & get_entry(const entryt &e, const typet &type, const namespacet &ns)
Gets or inserts an entry in this value-set.
#define DATA_INVARIANT(CONDITION, REASON)
void guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
void do_free(const exprt &op, const namespacet &ns)
Marks objects that may be pointed to by op as maybe-invalid.
std::list< exprt > valuest
void make_typecast(const typet &_type)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
const irept & find(const irep_namet &name) const
valuest values
Stores the LHS ID -> RHS expression set map.
bitvector_typet char_type()
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
bool simplify(exprt &expr, const namespacet &ns)
unsigned location_number
Matches the location_number field of the instruction that corresponds to this value_sett instance in ...
exprt make_member(const exprt &src, const irep_idt &component_name, const namespacet &ns)
Extracts a member from a struct- or union-typed expression.