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");
181 if(expr.
id()==ID_symbol &&
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();
261 *it = rename<level>(std::move(*it), ns).get();
265 (expr.
id() != ID_with ||
267 (expr.
id() != ID_if ||
270 "Type of renamed expr should be the same as operands for with_exprt and "
289 if(lvalue.
id() == ID_symbol)
297 else if(lvalue.
id() == ID_typecast)
302 else if(lvalue.
id() == ID_member)
307 else if(lvalue.
id() == ID_index)
312 index_lvalue.index() =
rename(index_lvalue.index(), ns).get();
315 lvalue.
id() == ID_byte_extract_little_endian ||
316 lvalue.
id() == ID_byte_extract_big_endian)
321 byte_extract_lvalue.offset() =
rename(byte_extract_lvalue.offset(), ns);
323 else if(lvalue.
id() == ID_if)
327 if_lvalue.cond() =
rename(if_lvalue.cond(), ns);
328 if(!if_lvalue.cond().is_false())
330 if(!if_lvalue.cond().is_true())
333 else if(lvalue.
id() == ID_complex_real)
338 else if(lvalue.
id() == ID_complex_imag)
346 "l2_rename_rvalues case `" + lvalue.
id_string() +
"' not handled");
369 (!ns.
lookup(obj_identifier).is_shared() && !(*
dirty)(obj_identifier)))
390 for(
const auto &guard_in_list : a_s_writes->second)
400 write_guard |= guard_in_list;
404 not_exprt no_write(write_guard.as_expr());
412 for(
const auto &a_s_read_guard : a_s_read.second)
414 guardt g = a_s_read_guard;
422 read_guard |= a_s_read_guard;
431 if(a_s_read.second.empty())
440 tmp = l2_false_case.
get();
458 expr = std::move(ssa_l2);
460 a_s_read.second.push_back(
guard);
462 a_s_read.second.back().add(no_write);
470 expr = set_indices<L2>(std::move(ssa_l1), ns).
get();
476 expr = set_indices<L2>(std::move(ssa_l1), ns).
get();
497 (!ns.
lookup(obj_identifier).is_shared() && !(*
dirty)(obj_identifier)))
542 template <levelt level>
545 if(expr.
id()==ID_symbol &&
551 ssa = set_indices<L1>(std::move(ssa), ns).
get();
556 else if(expr.
id()==ID_symbol)
559 rename_address<level>(expr, ns);
563 if(expr.
id()==ID_index)
567 rename_address<level>(index_expr.
array(), ns);
573 rename<level>(std::move(index_expr.
index()), ns).
get();
575 else if(expr.
id()==ID_if)
579 if_expr.
cond() = rename<level>(std::move(if_expr.
cond()), ns).
get();
580 rename_address<level>(if_expr.
true_case(), ns);
581 rename_address<level>(if_expr.
false_case(), ns);
585 else if(expr.
id()==ID_member)
589 rename_address<level>(member_expr.
struct_op(), ns);
615 rename_address<level>(*it, ns);
625 if(type.
id() == ID_array)
629 !array_type.size().is_constant();
631 else if(type.
id() == ID_struct || type.
id() == ID_union)
654 else if(type.
id() == ID_pointer)
658 else if(type.
id() == ID_union_tag)
663 else if(type.
id() == ID_struct_tag)
672 template <levelt level>
686 std::pair<l1_typest::iterator, bool> l1_type_entry;
688 !l1_identifier.
empty())
690 l1_type_entry=
l1_types.insert(std::make_pair(l1_identifier, type));
692 if(!l1_type_entry.second)
696 const typet &type_prev=l1_type_entry.first->second;
698 if(type.
id()!=ID_array ||
699 type_prev.
id()!=ID_array ||
703 type=l1_type_entry.first->second;
712 if(type.
id()==ID_array)
715 rename<level>(array_type.subtype(),
irep_idt(), ns);
716 array_type.size() = rename<level>(std::move(array_type.size()), ns).get();
718 else if(type.
id() == ID_struct || type.
id() == ID_union)
730 rename<level>(std::move(array_type.size()), ns).get();
732 else if(
component.type().id() != ID_pointer)
736 else if(type.
id()==ID_pointer)
742 !l1_identifier.
empty())
743 l1_type_entry.first->second=type;
750 if(expr.
id()==ID_symbol &&
767 out <<
"No stack!\n";
778 const auto &frame = *stackit;
779 out << frame.calling_location.function_id <<
" "
780 << frame.calling_location.pc->location_number <<
"\n";
786 std::function<std::size_t(
const irep_idt &)> index_generator,
792 const irep_idt l0_name = renamed.get_identifier();
793 const auto l1_index = narrow_cast<unsigned>(index_generator(l0_name));
804 INVARIANT(inserted,
"l1_name expected to be unique by construction");
818 if(ssa.
type().
id() == ID_pointer)
826 rhs =
exprt(ID_invalid);
828 exprt l1_rhs = rename<L1>(std::move(rhs), ns).
get();
845 expr_l2.
id() == ID_symbol && expr_l2.
get_bool(ID_C_SSA_symbol),
846 "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)
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
bool get_bool(const irep_namet &name) const
std::vector< threadt > threads
Expression classes for byte-level operators.
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.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_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 ...
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.
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.