Go to the documentation of this file.
38 std::size_t max_field_sensitive_array_size,
40 std::function<std::size_t(
const irep_idt &)> fresh_l2_name_provider)
43 guard_manager(manager),
44 symex_target(nullptr),
45 field_sensitivity(max_field_sensitive_array_size),
46 record_events({
true}),
47 fresh_l2_name_provider(fresh_l2_name_provider)
81 bool rhs_is_simplified,
83 bool allow_pointer_unsoundness)
86 lhs = rename_ssa<L1>(std::move(lhs), ns).
get();
90 rename<L2>(lhs.
type(), l1_identifier, ns);
112 if(
is_shared && lhs.
type().
id() == ID_pointer && !allow_pointer_unsoundness)
114 "pointer handling for concurrency is unsound");
119 const auto propagation_entry =
propagation.find(l1_identifier);
120 if(!propagation_entry.has_value())
122 else if(propagation_entry->get() != rhs)
144 std::cout <<
"Assigning " << l1_identifier <<
'\n';
146 std::cout <<
"**********************\n";
152 template <levelt level>
157 level ==
L0 || level ==
L1,
158 "rename_ssa can only be used for levels L0 and L1");
159 ssa = set_indices<level>(std::move(ssa), ns).
get();
171 template <levelt level>
180 "must handle all renaming levels");
184 exprt original_expr = expr;
190 std::move(rename_ssa<L0>(std::move(ssa), ns).value())};
195 std::move(rename_ssa<L1>(std::move(ssa), ns).value())};
199 ssa = set_indices<L1>(std::move(ssa), ns).
get();
228 ssa = set_indices<L2>(std::move(ssa), ns).
get();
234 else if(expr.
id()==ID_symbol)
236 const auto &type =
as_const(expr).type();
239 if(type.id() == ID_code || type.id() == ID_mathematical_function)
245 return rename<level>(
ssa_exprt{expr}, ns);
247 else if(expr.
id()==ID_address_of)
250 rename_address<level>(address_of_expr.object(), ns);
252 as_const(address_of_expr).object().type();
265 *it = rename<level>(std::move(*it), ns).get();
269 (expr.
id() != ID_with ||
271 (expr.
id() != ID_if ||
274 "Type of renamed expr should be the same as operands for with_exprt and "
293 if(lvalue.
id() == ID_symbol)
301 else if(lvalue.
id() == ID_typecast)
306 else if(lvalue.
id() == ID_member)
311 else if(lvalue.
id() == ID_index)
316 index_lvalue.index() =
rename(index_lvalue.index(), ns).get();
319 lvalue.
id() == ID_byte_extract_little_endian ||
320 lvalue.
id() == ID_byte_extract_big_endian)
325 byte_extract_lvalue.offset() =
rename(byte_extract_lvalue.offset(), ns);
327 else if(lvalue.
id() == ID_if)
331 if_lvalue.cond() =
rename(if_lvalue.cond(), ns);
332 if(!if_lvalue.cond().is_false())
334 if(!if_lvalue.cond().is_true())
337 else if(lvalue.
id() == ID_complex_real)
342 else if(lvalue.
id() == ID_complex_imag)
350 "l2_rename_rvalues case `" + lvalue.
id_string() +
"' not handled");
373 (!ns.
lookup(obj_identifier).is_shared() && !(*
dirty)(obj_identifier)))
394 for(
const auto &guard_in_list : a_s_writes->second)
404 write_guard |= guard_in_list;
408 not_exprt no_write(write_guard.as_expr());
416 for(
const auto &a_s_read_guard : a_s_read.second)
418 guardt g = a_s_read_guard;
425 read_guard |= a_s_read_guard;
437 const exprt l2_true_case =
438 p_it.has_value() ? *p_it : set_indices<L2>(ssa_l1, ns).
get();
443 if(a_s_read.second.empty())
450 tmp = l2_false_case.
get();
470 expr = std::move(ssa_l2);
472 a_s_read.second.push_back(
guard);
474 a_s_read.second.back().add(no_write);
482 expr = set_indices<L2>(std::move(ssa_l1), ns).
get();
488 expr = set_indices<L2>(std::move(ssa_l1), ns).
get();
509 (!ns.
lookup(obj_identifier).is_shared() && !(*
dirty)(obj_identifier)))
554 template <levelt level>
562 ssa = set_indices<L1>(std::move(ssa), ns).
get();
567 else if(expr.
id()==ID_symbol)
570 rename_address<level>(expr, ns);
574 if(expr.
id()==ID_index)
578 rename_address<level>(index_expr.
array(), ns);
584 rename<level>(std::move(index_expr.
index()), ns).
get();
586 else if(expr.
id()==ID_if)
590 if_expr.
cond() = rename<level>(std::move(if_expr.
cond()), ns).
get();
591 rename_address<level>(if_expr.
true_case(), ns);
592 rename_address<level>(if_expr.
false_case(), ns);
596 else if(expr.
id()==ID_member)
600 rename_address<level>(member_expr.
struct_op(), ns);
626 rename_address<level>(*it, ns);
636 if(type.
id() == ID_array)
640 !array_type.size().is_constant();
642 else if(type.
id() == ID_struct || type.
id() == ID_union)
665 else if(type.
id() == ID_pointer)
669 else if(type.
id() == ID_union_tag)
674 else if(type.
id() == ID_struct_tag)
683 template <levelt level>
697 std::pair<l1_typest::iterator, bool> l1_type_entry;
699 !l1_identifier.
empty())
701 l1_type_entry=
l1_types.insert(std::make_pair(l1_identifier, type));
703 if(!l1_type_entry.second)
707 const typet &type_prev=l1_type_entry.first->second;
709 if(type.
id()!=ID_array ||
710 type_prev.
id()!=ID_array ||
714 type=l1_type_entry.first->second;
723 if(type.
id()==ID_array)
726 rename<level>(array_type.subtype(),
irep_idt(), ns);
727 array_type.size() = rename<level>(std::move(array_type.size()), ns).get();
729 else if(type.
id() == ID_struct || type.
id() == ID_union)
741 rename<level>(std::move(array_type.size()), ns).get();
743 else if(
component.type().id() != ID_pointer)
747 else if(type.
id()==ID_pointer)
753 !l1_identifier.
empty())
754 l1_type_entry.first->second=type;
777 out <<
"No stack!\n";
788 const auto &frame = *stackit;
789 out << frame.calling_location.function_id <<
" "
790 << frame.calling_location.pc->location_number <<
"\n";
796 std::function<std::size_t(
const irep_idt &)> index_generator,
802 const irep_idt l0_name = renamed.get_identifier();
803 const std::size_t l1_index = index_generator(l0_name);
814 INVARIANT(inserted,
"l1_name expected to be unique by construction");
828 if(ssa.
type().
id() == ID_pointer)
836 rhs =
exprt(ID_invalid);
838 exprt l1_rhs = rename<L1>(std::move(rhs), ns).
get();
856 "symbol to declare should not be replaced by constant propagation");
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
optionalt< symbol_exprt > get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
void print_backtrace(std::ostream &) const
Dumps the current state of symex, printing the function name and location number for each stack frame...
const typet & subtype() const
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
bool check_renaming_l1(const exprt &expr)
Check that expr is correctly renamed to level 1 and return true in case an error is detected.
Variables whose address is taken.
#define Forall_operands(it, expr)
NODISCARD renamedt< ssa_exprt, L2 > assignment(ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
static irep_idt guard_identifier()
#define CHECK_RETURN(CONDITION)
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.
The type of an expression, extends irept.
NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
goto_programt::const_targett pc
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
const incremental_dirtyt * dirty
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.
Base type for structs and unions.
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
typet type
Type of symbol.
Thrown when we encounter an instruction, parameters to an instruction etc.
The trinary if-then-else operator.
Various predicates over pointers in programs.
std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider
guard_managert & guard_manager
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
Base class for all expressions.
irep_idt get_object_name() const
std::vector< componentt > componentst
symex_targett::sourcet source
static bool is_read_only_object(const exprt &lvalue)
Returns true if lvalue is a read-only object, such as the null object.
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
std::size_t increase_generation(const irep_idt &l1_identifier, const ssa_exprt &lhs, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
Allocates a fresh L2 name for the given L1 identifier, and makes it the latest generation on this pat...
renamedt< ssa_exprt, L0 > symex_level0(ssa_exprt ssa_expr, const namespacet &ns, std::size_t thread_nr)
Set the level 0 renaming of SSA expressions.
Expression to hold a symbol (variable)
NODISCARD exprt apply(const namespacet &ns, goto_symex_statet &state, exprt expr, bool write) const
Turn an expression expr into a field-sensitive SSA expression.
const exprt & get_original_expr() const
const underlyingt & get() const
GOTO Symex constant propagation.
bool is_false() const
Return whether the expression is a constant representing false.
goto_symex_statet(const symex_targett::sourcet &, std::size_t max_field_sensitive_array_size, guard_managert &manager, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
sharing_mapt< irep_idt, exprt > propagation
static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
Expression providing an SSA-renamed symbol of expressions.
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Generic exception types primarily designed for use with invariants.
This is unused by this implementation of guards, but can be used by other implementations of the same...
typet & type()
Return the type of the expression.
framet & new_frame(symex_targett::sourcet calling_location, const guardt &guard)
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)
thread encoding
std::vector< threadt > threads
Expression classes for byte-level operators.
bool is_ssa_expr(const exprt &expr)
call_stackt & call_stack()
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
void output(std::ostream &out, const std::string &indent="") const
Pretty-print this value-set.
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
static bool failed(bool error_indicator)
const exprt & struct_op() const
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
symex_target_equationt * symex_target
const std::string & id_string() const
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const irep_idt get_level_2() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
void insert(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Assume ssa is not already known.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
The Boolean constant false.
Stack frames – these are used for function calls and for exceptions.
void find_symbols(const exprt &src, find_symbols_sett &dest, bool current, bool next)
Add to the set dest the sub-expressions of src with id ID_symbol if current is true,...
write_is_shared_resultt write_is_shared(const ssa_exprt &expr, const namespacet &ns) const
@ L1_WITH_CONSTANT_PROPAGATION
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
Container for data that varies per program point, e.g.
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible b...
field_sensitivityt field_sensitivity
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
bool run_validation_checks
Should the additional validation checks be run?
Extract member of struct or union.
Deprecated expression utility functions.
static bool requires_renaming(const typet &type, const namespacet &ns)
Return true if, and only if, the type or one of its subtypes requires SSA renaming.
ssa_exprt remove_level_2(ssa_exprt ssa)
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt & get(const irep_namet &name) const
ssa_exprt declare(ssa_exprt ssa, const namespacet &ns)
Add invalid (or a failed symbol) to the value_set if ssa is a pointer, ensure that level2 index of sy...
unsigned atomic_section_id
Threads.
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.
bool check_renaming(const typet &type)
Check that type is correctly renamed to level 2 and return true in case an error is detected.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
std::set< irep_idt > local_objects
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Read from a shared variable ssa_object (which is both the left- and the right–hand side of assignment...
static void get_l1_name(exprt &expr)
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
std::stack< bool > record_events
bool has(const renamedt< ssa_exprt, L0 > &ssa) const
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
NODISCARD renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
irep_idt get_component_name() const
exprt get_fields(const namespacet &ns, goto_symex_statet &state, const ssa_exprt &ssa_expr) const
Compute an expression representing the individual components of a field-sensitive SSA representation ...
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
unsigned latest_index(const irep_idt &identifier) const
Counter corresponding to an identifier.
Identifies source in the context of symbolic execution.
Operator to return the address of an object.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
The Boolean constant true.
API to expression classes.
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
ssa_exprt add_object(const symbol_exprt &expr, std::function< std::size_t(const irep_idt &)> index_generator, const namespacet &ns)
Instantiate the object expr.
void rename_address(exprt &expr, const namespacet &ns)
Wrapper for expressions or types which have been renamed up to a given level.
optionalt< std::pair< ssa_exprt, std::size_t > > insert_or_replace(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Set the index for ssa to index.
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)
Write to a local variable.