46 id==
"value_set::return_value" ||
47 id==
"value_set::memory")
51 return ns.
follow(type).
id()==ID_struct;
57 auto found =
values.find(
id);
58 return found ==
values.end() ? nullptr : &found->second;
73 std::pair<valuest::iterator, bool>
r=
74 values.insert(std::pair<idt, entryt>(index, e));
76 return r.first->second;
89 dest.
write()[n] = offset;
92 else if(!entry->second)
94 else if(offset && *entry->second == *offset)
98 dest.
write()[n].reset();
105 std::ostream &out)
const 107 for(valuest::const_iterator
114 const entryt &e=v_it->second;
121 else if(e.
identifier==
"value_set::return_value")
123 display_name=
"RETURN_VALUE"+e.
suffix;
131 identifier=symbol.
name;
147 o_it=object_map.
begin();
148 o_it!=object_map.
end();
155 if(o.
id()==ID_invalid || o.
id()==ID_unknown)
159 result=
"<"+
from_expr(ns, identifier, o)+
", ";
176 width+=result.size();
181 if(next!=object_map.
end())
197 if(
object.
id()==ID_invalid ||
198 object.
id()==ID_unknown)
210 return std::move(od);
217 valuest::iterator v_it=
values.begin();
219 for(valuest::const_iterator
220 it=new_values.begin();
221 it!=new_values.end();
224 if(v_it==
values.end() || it->first<v_it->first)
231 else if(v_it->first<it->first)
237 assert(v_it->first==it->first);
240 const entryt &new_e=it->second;
273 if(expr.
id()==ID_pointer_offset)
285 it=object_map.
begin();
286 it!=object_map.
end();
295 if(!ptr_offset.has_value())
298 *ptr_offset += *it->second;
300 if(mod && *ptr_offset != previous_offset)
304 previous_offset = *ptr_offset;
335 for(value_setst::valuest::const_iterator it=dest.begin();
336 it!=dest.end(); it++)
337 std::cout <<
"GET_VALUE_SET: " <<
format(*it) <<
'\n';
345 bool is_simplified)
const 358 const std::string &suffix,
const std::string &field)
363 suffix.compare(1, field.length(), field) == 0 &&
364 (suffix.length() == field.length() + 1 ||
365 suffix[field.length() + 1] ==
'.' ||
366 suffix[field.length() + 1] ==
'[');
370 const std::string &suffix,
const std::string &field)
374 "suffix should start with " + field);
375 return suffix.substr(field.length() + 1);
381 const std::string &suffix,
382 const typet &original_type,
386 std::cout <<
"GET_VALUE_SET_REC EXPR: " <<
format(expr) <<
"\n";
387 std::cout <<
"GET_VALUE_SET_REC SUFFIX: " << suffix <<
'\n';
392 if(expr.
id()==ID_unknown || expr.
id()==ID_invalid)
396 else if(expr.
id()==ID_index)
403 type.id()==ID_incomplete_array,
404 "operand 0 of index expression must be an array");
408 else if(expr.
id()==ID_member)
415 type.id()==ID_union ||
416 type.id()==ID_incomplete_struct ||
417 type.id()==ID_incomplete_union,
418 "operand 0 of member expression must be struct or union");
420 const std::string &component_name=
424 "."+component_name+suffix, original_type, ns);
426 else if(expr.
id()==ID_symbol)
431 if(expr_type.
id()==ID_pointer ||
432 expr_type.
id()==ID_signedbv ||
433 expr_type.
id()==ID_unsignedbv ||
434 expr_type.
id()==ID_struct ||
435 expr_type.
id()==ID_union ||
436 expr_type.
id()==ID_array)
443 if(!entry && (expr_type.
id() == ID_struct || expr_type.
id() == ID_union))
448 const irep_idt &first_component_name =
449 struct_union_type.
components().front().get_name();
468 else if(expr.
id()==ID_if)
471 throw "if takes three operands";
476 else if(expr.
id()==ID_address_of)
479 throw expr.
id_string()+
" expected to have one operand";
483 else if(expr.
id()==ID_dereference)
489 if(object_map.
begin()==object_map.
end())
494 it1=object_map.
begin();
495 it1!=object_map.
end();
505 else if(expr.
id()==
"reference_to")
514 if(object_map.
begin()==object_map.
end())
519 it=object_map.
begin();
520 it!=object_map.
end();
533 if(expr.
get(ID_value)==ID_NULL &&
534 expr_type.
id()==ID_pointer)
538 else if(expr_type.
id()==ID_unsignedbv ||
539 expr_type.
id()==ID_signedbv)
547 else if(expr.
id()==ID_typecast)
550 throw "typecast takes one operand";
556 if(op_type.
id()==ID_pointer)
561 else if(op_type.
id()==ID_unsignedbv ||
562 op_type.
id()==ID_signedbv)
596 else if(expr.
id()==ID_plus ||
600 throw expr.
id_string()+
" expected to have at least two operands";
609 expr_type.
id()==ID_pointer)
617 ptr_operand=expr.
op1();
622 ptr_operand=expr.
op0();
628 if(pointer_sub_type.
id()==ID_empty)
633 if(!size.has_value() || (*size) == 0)
641 if(expr.
id()==ID_minus)
647 ptr_operand, pointer_expr_set,
"", ptr_operand.
type(), ns);
655 *it, pointer_expr_set,
"", it->type(), ns);
661 it!=pointer_expr_set.
read().
end();
667 if(offset && i_is_set)
672 insert(dest, it->first, offset);
675 else if(expr.
id()==ID_mult)
681 throw expr.
id_string()+
" expected to have at least two operands";
689 *it, pointer_expr_set,
"", it->type(), ns);
694 it!=pointer_expr_set.
read().
end();
702 insert(dest, it->first, offset);
705 else if(expr.
id()==ID_side_effect)
709 if(statement==ID_function_call)
712 throw "unexpected function_call sideeffect";
714 else if(statement==ID_allocate)
718 const typet &dynamic_type=
719 static_cast<const typet &
>(expr.
find(ID_C_cxx_alloc_type));
727 else if(statement==ID_cpp_new ||
728 statement==ID_cpp_new_array)
731 assert(expr_type.
id()==ID_pointer);
742 else if(expr.
id()==ID_struct)
746 struct_components.size() == expr.
operands().size(),
747 "struct expression should have an operand per component");
748 auto component_iter = struct_components.begin();
749 bool found_component =
false;
755 const std::string &component_name =
759 std::string remaining_suffix =
762 found_component =
true;
776 else if(expr.
id()==ID_with)
782 if(expr_type.
id() == ID_struct && !suffix.
empty())
788 std::string remaining_suffix =
791 with_expr.
new_value(), dest, remaining_suffix, original_type, ns);
807 else if(expr_type.
id() == ID_array && !suffix.
empty())
809 std::string new_value_suffix;
811 new_value_suffix = suffix.substr(2);
818 with_expr.
new_value(), dest, new_value_suffix, original_type, ns);
828 else if(expr.
id()==ID_array)
831 std::string new_suffix = suffix;
833 new_suffix = suffix.substr(2);
840 else if(expr.
id()==ID_array_of)
843 std::string new_suffix = suffix;
845 new_suffix = suffix.substr(2);
852 else if(expr.
id()==ID_dynamic_object)
857 const std::string prefix=
858 "value_set::dynamic_object"+
862 const std::string full_name=prefix+suffix;
876 else if(expr.
id()==ID_byte_extract_little_endian ||
877 expr.
id()==ID_byte_extract_big_endian)
880 throw "byte_extract takes two operands";
890 if(!
to_integer(op1, op1_offset) && op0_type.
id()==ID_struct)
896 const irep_idt &name = c.get_name();
900 if(!comp_offset.has_value())
902 else if(*comp_offset > op1_offset)
904 else if(*comp_offset != op1_offset)
915 if(op0_type.
id()==ID_union)
920 const irep_idt &name = c.get_name();
930 else if(expr.
id()==ID_byte_update_little_endian ||
931 expr.
id()==ID_byte_update_big_endian)
934 throw "byte_update takes three operands";
945 std::cout <<
"WARNING: not doing " << expr.
id() <<
'\n';
950 std::cout <<
"GET_VALUE_SET_REC RESULT:\n";
951 for(
const auto &obj : dest.
read())
954 std::cout <<
" " <<
format(e) <<
"\n";
965 if(src.
id()==ID_typecast)
967 assert(src.
type().
id()==ID_pointer);
970 throw "typecast expects one operand";
999 std::cout <<
"GET_REFERENCE_SET_REC EXPR: " <<
format(expr)
1003 if(expr.
id()==ID_symbol ||
1004 expr.
id()==ID_dynamic_object ||
1005 expr.
id()==ID_string_constant ||
1006 expr.
id()==ID_array)
1008 if(expr.
type().
id()==ID_array &&
1016 else if(expr.
id()==ID_dereference)
1019 throw expr.
id_string()+
" expected to have one operand";
1024 for(expr_sett::const_iterator it=value_set.begin();
1025 it!=value_set.end(); it++)
1026 std::cout <<
"VALUE_SET: " <<
format(*it) <<
'\n';
1031 else if(expr.
id()==ID_index)
1034 throw "index expected to have two operands";
1041 assert(array_type.
id()==ID_array ||
1042 array_type.
id()==ID_incomplete_array);
1050 a_it=object_map.
begin();
1051 a_it!=object_map.
end();
1056 if(
object.
id()==ID_unknown)
1074 if(!size.has_value() || *size == 0)
1082 insert(dest, deref_index_expr, o);
1088 else if(expr.
id()==ID_member)
1090 const irep_idt &component_name=expr.
get(ID_component_name);
1093 throw "member expected to have one operand";
1103 it=object_map.
begin();
1104 it!=object_map.
end();
1109 if(
object.
id()==ID_unknown)
1120 const typet &final_object_type = ns.
follow(
object.type());
1122 if(final_object_type.id()==ID_struct ||
1123 final_object_type.id()==ID_union)
1126 if(ns.
follow(struct_op.
type())!=final_object_type)
1127 member_expr.op0().make_typecast(struct_op.
type());
1129 insert(dest, member_expr, o);
1138 else if(expr.
id()==ID_if)
1141 throw "if takes three operands";
1159 std::cout <<
"ASSIGN LHS: " <<
format(lhs) <<
" : " 1161 std::cout <<
"ASSIGN RHS: " <<
format(rhs) <<
" : " 1163 std::cout <<
"--------------------------------------------\n";
1169 if(type.
id()==ID_struct ||
1170 type.
id()==ID_union)
1174 const typet &subtype = c.type();
1175 const irep_idt &name = c.get_name();
1178 if(subtype.
id() == ID_code || c.get_is_padding())
1185 if(rhs.
id()==ID_unknown ||
1186 rhs.
id()==ID_invalid)
1188 rhs_member=
exprt(rhs.
id(), subtype);
1193 throw "value_sett::assign type mismatch: " 1199 assign(lhs_member, rhs_member, ns,
false, add_to_sets);
1203 else if(type.
id()==ID_array)
1208 if(rhs.
id()==ID_unknown ||
1209 rhs.
id()==ID_invalid)
1221 throw "value_sett::assign type mismatch: " 1225 if(rhs.
id()==ID_array_of)
1228 assign(lhs_index, rhs.
op0(), ns, is_simplified, add_to_sets);
1230 else if(rhs.
id()==ID_array ||
1231 rhs.
id()==ID_constant)
1235 assign(lhs_index, *o_it, ns, is_simplified, add_to_sets);
1239 else if(rhs.
id()==ID_with)
1246 assign(lhs_index, op0_index, ns, is_simplified, add_to_sets);
1247 assign(lhs_index, rhs.
op2(), ns, is_simplified,
true);
1253 assign(lhs_index, rhs_index, ns, is_simplified,
true);
1269 assign_rec(lhs, values_rhs,
"", ns, add_to_sets);
1276 const std::string &suffix,
1281 std::cout <<
"ASSIGN_REC LHS: " <<
format(lhs) <<
'\n';
1282 std::cout <<
"ASSIGN_REC LHS ID: " << lhs.
id() <<
'\n';
1283 std::cout <<
"ASSIGN_REC SUFFIX: " << suffix <<
'\n';
1288 std::cout <<
"ASSIGN_REC RHS: " <<
1293 if(lhs.
id()==ID_symbol)
1304 else if(lhs.
id()==ID_dynamic_object)
1309 const std::string name=
1310 "value_set::dynamic_object"+
1317 else if(lhs.
id()==ID_dereference)
1320 throw lhs.
id_string()+
" expected to have one operand";
1330 it!=reference_set.
read().
end();
1337 if(
object.
id()!=ID_unknown)
1338 assign_rec(
object, values_rhs, suffix, ns, add_to_sets);
1341 else if(lhs.
id()==ID_index)
1344 throw "index expected to have two operands";
1349 "operand 0 of index expression must be an array");
1353 else if(lhs.
id()==ID_member)
1356 throw "member expected to have one operand";
1358 const std::string &component_name=lhs.
get_string(ID_component_name);
1363 type.
id()==ID_union ||
1364 type.
id()==ID_incomplete_struct ||
1365 type.
id()==ID_incomplete_union,
1366 "operand 0 of member expression must be struct or union");
1369 lhs.
op0(), values_rhs,
"."+component_name+suffix, ns, add_to_sets);
1371 else if(lhs.
id()==
"valid_object" ||
1372 lhs.
id()==
"dynamic_size" ||
1373 lhs.
id()==
"dynamic_type" ||
1374 lhs.
id()==
"is_zero_string" ||
1375 lhs.
id()==
"zero_string" ||
1376 lhs.
id()==
"zero_string_length")
1380 else if(lhs.
id()==ID_string_constant)
1385 else if(lhs.
id() == ID_null_object)
1389 else if(lhs.
id()==ID_typecast)
1393 assign_rec(typecast_expr.
op(), values_rhs, suffix, ns, add_to_sets);
1395 else if(lhs.
id()==ID_byte_extract_little_endian ||
1396 lhs.
id()==ID_byte_extract_big_endian)
1401 else if(lhs.
id()==ID_integer_address)
1407 throw "assign NYI: `"+lhs.
id_string()+
"'";
1425 for(std::size_t i=0; i<arguments.size(); i++)
1427 const std::string identifier=
"value_set::dummy_arg_"+
std::to_string(i);
1428 const symbol_exprt dummy_lhs(identifier, arguments[i].type());
1429 assign(dummy_lhs, arguments[i], ns,
false,
false);
1436 for(code_typet::parameterst::const_iterator
1437 it=parameter_types.begin();
1438 it!=parameter_types.end();
1441 const irep_idt &identifier=it->get_identifier();
1449 assign(actual_lhs, v_expr, ns,
true,
true);
1465 assign(lhs, rhs, ns,
false,
false);
1474 if(statement==ID_block)
1479 else if(statement==ID_function_call)
1484 else if(statement==ID_assign)
1487 throw "assignment expected to have two operands";
1491 else if(statement==ID_decl)
1494 throw "decl expected to have one operand";
1498 if(lhs.
id()!=ID_symbol)
1499 throw "decl expected to have symbol on lhs";
1503 if(lhs_type.
id()==ID_pointer ||
1504 (lhs_type.
id()==ID_array &&
1514 assign(lhs, address_of_expr, ns,
false,
false);
1520 else if(statement==ID_expression)
1524 else if(statement==
"cpp_delete" ||
1525 statement==
"cpp_delete[]")
1529 else if(statement==
"lock" || statement==
"unlock")
1533 else if(statement==ID_asm)
1537 else if(statement==ID_nondet)
1541 else if(statement==ID_printf)
1545 else if(statement==ID_return)
1551 assign(lhs, code.
op0(), ns,
false,
false);
1554 else if(statement==ID_array_set)
1557 else if(statement==ID_array_copy)
1560 else if(statement==ID_array_replace)
1563 else if(statement==ID_assume)
1567 else if(statement==ID_user_specified_predicate ||
1568 statement==ID_user_specified_parameter_predicates ||
1569 statement==ID_user_specified_return_predicates)
1573 else if(statement==ID_fence)
1576 else if(statement==ID_input || statement==ID_output)
1580 else if(statement==ID_dead)
1587 throw "value_sett: unexpected statement: "+
id2string(statement);
1595 if(expr.
id()==ID_and)
1600 else if(expr.
id()==ID_equal)
1603 else if(expr.
id()==ID_notequal)
1606 else if(expr.
id()==ID_not)
1609 else if(expr.
id()==ID_dynamic_object)
1621 assign(expr.
op0(), address_of, ns,
false,
false);
virtual void apply_assign_side_effects(const exprt &lhs, const exprt &rhs, const namespacet &)
Subclass customisation point to apply global side-effects to this domain, after RHS values are read b...
const irep_idt & get_statement() const
The type of an expression, extends irept.
irep_idt name
The unique identifier.
Semantic type conversion.
const typet & component_type(const irep_idt &component_name) const
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 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.
static bool suffix_starts_with_field(const std::string &suffix, const std::string &field)
Check if 'suffix' starts with 'field'.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
const irep_idt & get_identifier() const
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
typet & type()
Return the type of the expression.
static object_numberingt object_numbering
Global shared object numbering, used to abbreviate expressions stored in value sets.
void dereference_rec(const exprt &src, exprt &dest) const
Sets dest to src with any wrapping typecasts removed.
Structure type, corresponds to C style structs.
virtual void adjust_assign_rhs_values(const exprt &rhs, const namespacet &, object_mapt &rhs_values) const
Subclass customisation point to filter or otherwise alter the value-set returned from get_value_set b...
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:
static std::string strip_first_field_from_suffix(const std::string &suffix, const std::string &field)
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.
const entryt * find_entry(const idt &id) const
Finds an entry in this value-set.
optionalt< mp_integer > pointer_offset_size(const typet &type, const namespacet &ns)
Compute the size of a type in bytes, rounding up to full bytes.
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...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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 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()
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
typename Map::mapped_type number_type
Operator to return the address of an object.
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
bool is_constant() const
Return whether the expression is a constant.
static exprt conditional_cast(const exprt &expr, const typet &type)
bool has_component(const irep_idt &component_name) const
std::vector< exprt > operandst
optionalt< mp_integer > member_offset(const struct_typet &type, const irep_idt &member, const namespacet &ns)
const irep_idt & display_name() const
Return language specific display name if present.
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...
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
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 for structs and unions.
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
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
optionalt< mp_integer > compute_pointer_offset(const exprt &expr, const namespacet &ns)
Operator to update elements in structs and arrays.
const union_typet & to_union_type(const typet &type)
Cast a typet to a union_typet.
#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.
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)
bool is_zero() const
Return whether the expression is a constant representing 0.
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 typet to a pointer_typet.
exprt dynamic_object(const exprt &pointer)
Data structure for representing an arbitrary statement in a program.
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)
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 guard(const exprt &expr, const namespacet &ns)
Transforms this value-set by assuming an expression holds.
std::list< exprt > valuest
const index_exprt & to_index_expr(const exprt &expr)
Cast an 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 documentation for 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.