Go to the documentation of this file.
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");
const componentst & components() const
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
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 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,...
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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.