37 std::size_t max_field_sensitive_array_size,
39 std::function<std::size_t(
const irep_idt &)> fresh_l2_name_provider)
42 guard_manager(manager),
43 symex_target(nullptr),
44 field_sensitivity(max_field_sensitive_array_size),
45 record_events({
true}),
46 fresh_l2_name_provider(fresh_l2_name_provider)
80 bool rhs_is_simplified,
82 bool allow_pointer_unsoundness)
85 lhs = rename_ssa<L1>(std::move(lhs), ns).
get();
89 rename<L2>(lhs.
type(), l1_identifier, ns);
111 if(
is_shared && lhs.
type().
id() == ID_pointer && !allow_pointer_unsoundness)
113 "pointer handling for concurrency is unsound");
118 const auto propagation_entry =
propagation.find(l1_identifier);
119 if(!propagation_entry.has_value())
121 else if(propagation_entry->get() != rhs)
143 std::cout <<
"Assigning " << l1_identifier <<
'\n';
145 std::cout <<
"**********************\n";
151 template <levelt level>
156 level ==
L0 || level ==
L1,
157 "rename_ssa can only be used for levels L0 and L1");
158 ssa = set_indices<level>(std::move(ssa), ns).
get();
170 template <levelt level>
179 "must handle all renaming levels");
183 exprt original_expr = expr;
189 std::move(rename_ssa<L0>(std::move(ssa), ns).value())};
194 std::move(rename_ssa<L1>(std::move(ssa), ns).value())};
198 ssa = set_indices<L1>(std::move(ssa), ns).
get();
227 ssa = set_indices<L2>(std::move(ssa), ns).
get();
233 else if(expr.
id()==ID_symbol)
235 const auto &type =
as_const(expr).type();
238 if(type.id() == ID_code || type.id() == ID_mathematical_function)
244 return rename<level>(
ssa_exprt{expr}, ns);
246 else if(expr.
id()==ID_address_of)
249 rename_address<level>(address_of_expr.object(), ns);
251 as_const(address_of_expr).object().type();
264 *it = rename<level>(std::move(*it), ns).get();
268 (expr.
id() != ID_with ||
270 (expr.
id() != ID_if ||
273 "Type of renamed expr should be the same as operands for with_exprt and "
292 if(lvalue.
id() == ID_symbol)
300 else if(lvalue.
id() == ID_typecast)
305 else if(lvalue.
id() == ID_member)
310 else if(lvalue.
id() == ID_index)
315 index_lvalue.index() =
rename(index_lvalue.index(), ns).get();
318 lvalue.
id() == ID_byte_extract_little_endian ||
319 lvalue.
id() == ID_byte_extract_big_endian)
324 byte_extract_lvalue.offset() =
rename(byte_extract_lvalue.offset(), ns);
326 else if(lvalue.
id() == ID_if)
330 if_lvalue.cond() =
rename(if_lvalue.cond(), ns);
331 if(!if_lvalue.cond().is_false())
333 if(!if_lvalue.cond().is_true())
336 else if(lvalue.
id() == ID_complex_real)
341 else if(lvalue.
id() == ID_complex_imag)
349 "l2_rename_rvalues case `" + lvalue.
id_string() +
"' not handled");
372 (!ns.
lookup(obj_identifier).is_shared() && !(*
dirty)(obj_identifier)))
393 for(
const auto &guard_in_list : a_s_writes->second)
403 write_guard |= guard_in_list;
407 not_exprt no_write(write_guard.as_expr());
415 for(
const auto &a_s_read_guard : a_s_read.second)
417 guardt g = a_s_read_guard;
424 read_guard |= a_s_read_guard;
436 const exprt l2_true_case =
437 p_it.has_value() ? *p_it : set_indices<L2>(ssa_l1, ns).
get();
442 if(a_s_read.second.empty())
449 tmp = l2_false_case.
get();
469 expr = std::move(ssa_l2);
471 a_s_read.second.push_back(
guard);
473 a_s_read.second.back().add(no_write);
481 expr = set_indices<L2>(std::move(ssa_l1), ns).
get();
487 expr = set_indices<L2>(std::move(ssa_l1), ns).
get();
508 (!ns.
lookup(obj_identifier).is_shared() && !(*
dirty)(obj_identifier)))
553 template <levelt level>
561 ssa = set_indices<L1>(std::move(ssa), ns).
get();
566 else if(expr.
id()==ID_symbol)
569 rename_address<level>(expr, ns);
573 if(expr.
id()==ID_index)
577 rename_address<level>(index_expr.
array(), ns);
583 rename<level>(std::move(index_expr.
index()), ns).
get();
585 else if(expr.
id()==ID_if)
589 if_expr.
cond() = rename<level>(std::move(if_expr.
cond()), ns).
get();
590 rename_address<level>(if_expr.
true_case(), ns);
591 rename_address<level>(if_expr.
false_case(), ns);
595 else if(expr.
id()==ID_member)
599 rename_address<level>(member_expr.
struct_op(), ns);
625 rename_address<level>(*it, ns);
635 if(type.
id() == ID_array)
639 !array_type.size().is_constant();
641 else if(type.
id() == ID_struct || type.
id() == ID_union)
664 else if(type.
id() == ID_pointer)
668 else if(type.
id() == ID_union_tag)
673 else if(type.
id() == ID_struct_tag)
682 template <levelt level>
696 std::pair<l1_typest::iterator, bool> l1_type_entry;
698 !l1_identifier.
empty())
700 l1_type_entry=
l1_types.insert(std::make_pair(l1_identifier, type));
702 if(!l1_type_entry.second)
706 const typet &type_prev=l1_type_entry.first->second;
708 if(type.
id()!=ID_array ||
709 type_prev.
id()!=ID_array ||
713 type=l1_type_entry.first->second;
722 if(type.
id()==ID_array)
725 rename<level>(array_type.subtype(),
irep_idt(), ns);
726 array_type.size() = rename<level>(std::move(array_type.size()), ns).get();
728 else if(type.
id() == ID_struct || type.
id() == ID_union)
740 rename<level>(std::move(array_type.size()), ns).get();
742 else if(
component.type().id() != ID_pointer)
746 else if(type.
id()==ID_pointer)
752 !l1_identifier.
empty())
753 l1_type_entry.first->second=type;
776 out <<
"No stack!\n";
787 const auto &frame = *stackit;
788 out << frame.calling_location.function_id <<
" "
789 << frame.calling_location.pc->location_number <<
"\n";
795 std::function<std::size_t(
const irep_idt &)> index_generator,
801 const irep_idt l0_name = renamed.get_identifier();
802 const auto l1_index = narrow_cast<unsigned>(index_generator(l0_name));
813 INVARIANT(inserted,
"l1_name expected to be unique by construction");
827 if(ssa.
type().
id() == ID_pointer)
835 rhs =
exprt(ID_invalid);
837 exprt l1_rhs = rename<L1>(std::move(rhs), ns).
get();
855 "symbol to declare should not be replaced by constant propagation");
optionalt< symbol_exprt > get_failed_symbol(const symbol_exprt &expr, const namespacet &ns)
Get the failed-dereference symbol for the given symbol.
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Generic exception types primarily designed for use with invariants.
Expression classes for byte-level operators.
const byte_extract_exprt & to_byte_extract_expr(const exprt &expr)
Operator to return the address of an object.
const exprt & size() const
framet & new_frame(symex_targett::sourcet calling_location, const guardt &guard)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
The Boolean constant false.
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
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 ...
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.
Container for data that varies per program point, e.g.
unsigned atomic_section_id
Threads.
sharing_mapt< irep_idt, exprt > propagation
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
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...
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.
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
std::stack< bool > record_events
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)
thread encoding
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...
NODISCARD exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
static irep_idt guard_identifier()
call_stackt & call_stack()
const incremental_dirtyt * dirty
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)
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
void rename_address(exprt &expr, const namespacet &ns)
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)
guard_managert & guard_manager
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
void print_backtrace(std::ostream &) const
Dumps the current state of symex, printing the function name and location number for each stack frame...
symex_target_equationt * symex_target
static bool is_read_only_object(const exprt &lvalue)
Returns true if lvalue is a read-only object, such as the null object.
field_sensitivityt field_sensitivity
write_is_shared_resultt write_is_shared(const ssa_exprt &expr, const namespacet &ns) const
symex_targett::sourcet source
bool run_validation_checks
Should the additional validation checks be run?
std::vector< threadt > threads
std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider
The trinary if-then-else operator.
const std::string & id_string() const
const irep_idt & id() const
const irep_idt & get(const irep_namet &name) const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Wrapper for expressions or types which have been renamed up to a given level.
const underlyingt & get() const
Expression providing an SSA-renamed symbol of expressions.
const irep_idt get_level_2() const
const exprt & get_original_expr() const
irep_idt get_object_name() const
Base type for structs and unions.
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
const componentst & components() const
std::vector< componentt > componentst
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
typet type
Type of symbol.
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...
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...
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.
The Boolean constant true.
The type of an expression, extends irept.
const typet & subtype() const
Thrown when we encounter an instruction, parameters to an instruction etc.
void output(std::ostream &out, const std::string &indent="") const
Pretty-print this value-set.
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.
Variables whose address is taken.
#define Forall_operands(it, expr)
Deprecated expression utility functions.
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,...
GOTO Symex constant propagation.
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.
static void get_l1_name(exprt &expr)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
Various predicates over pointers in programs.
static bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
@ L1_WITH_CONSTANT_PROPAGATION
bool check_renaming(const typet &type)
Check that type is correctly renamed to level 2 and return true in case an error is detected.
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.
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.
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
#define CHECK_RETURN(CONDITION)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
bool is_ssa_expr(const exprt &expr)
ssa_exprt remove_level_2(ssa_exprt ssa)
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
const complex_imag_exprt & to_complex_imag_expr(const exprt &expr)
Cast an exprt to a complex_imag_exprt.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
Stack frames – these are used for function calls and for exceptions.
std::set< irep_idt > local_objects
This is unused by this implementation of guards, but can be used by other implementations of the same...
bool has(const renamedt< ssa_exprt, L0 > &ssa) const
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.
void insert(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Assume ssa is not already known.
unsigned latest_index(const irep_idt &identifier) const
Counter corresponding to an identifier.
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...
Identifies source in the context of symbolic execution.
goto_programt::const_targett pc
static bool failed(bool error_indicator)