32 std::size_t max_field_sensitive_array_size,
42 max_field_sensitive_array_size,
46 language_mode(language_mode),
47 fresh_l2_name_provider(fresh_l2_name_provider)
49 threads.emplace_back(guard_manager);
81 bool rhs_is_simplified,
83 bool allow_pointer_unsoundness)
114 if(
is_shared && lhs.
type().
id() == ID_pointer && !allow_pointer_unsoundness)
116 "pointer handling for concurrency is unsound");
121 const auto propagation_entry =
propagation.find(l1_identifier);
122 if(!propagation_entry.has_value())
124 else if(propagation_entry->get() != rhs)
133 std::cout <<
"Assigning " << l1_identifier <<
'\n';
135 std::cout <<
"**********************\n";
141template <levelt level>
146 level ==
L0 || level ==
L1,
147 "rename_ssa can only be used for levels L0 and L1");
160template <levelt level>
169 "must handle all renaming levels");
173 exprt original_expr = expr;
223 else if(expr.
id()==ID_symbol)
225 const auto &type =
as_const(expr).type();
228 if(type.id() == ID_code || type.id() == ID_mathematical_function)
236 else if(expr.
id()==ID_address_of)
241 as_const(address_of_expr).object().type();
269 c_with_expr->type() != c_with_expr->old().type())
274 expr.
id() != ID_with ||
276 "Type of renamed expr should be the same as operands for with_exprt",
280 expr.
id() != ID_if ||
282 "Type of renamed expr should be the same as operands for if_exprt",
284 to_if_expr(c_expr).true_case().type().pretty());
286 expr.
id() != ID_if ||
288 "Type of renamed expr should be the same as operands for if_exprt",
290 to_if_expr(c_expr).false_case().type().pretty());
308 if(lvalue.
id() == ID_symbol)
316 else if(lvalue.
id() == ID_typecast)
321 else if(lvalue.
id() == ID_member)
326 else if(lvalue.
id() == ID_index)
331 index_lvalue.index() =
rename(index_lvalue.index(), ns).get();
334 lvalue.
id() == ID_byte_extract_little_endian ||
335 lvalue.
id() == ID_byte_extract_big_endian)
340 byte_extract_lvalue.offset() =
rename(byte_extract_lvalue.offset(), ns);
342 else if(lvalue.
id() == ID_if)
346 if_lvalue.cond() =
rename(if_lvalue.cond(), ns);
347 if(!if_lvalue.cond().is_false())
349 if(!if_lvalue.cond().is_true())
352 else if(lvalue.
id() == ID_complex_real)
357 else if(lvalue.
id() == ID_complex_imag)
365 "l2_rename_rvalues case `" + lvalue.
id_string() +
"' not handled");
388 (!ns.
lookup(obj_identifier).is_shared() && !(*
dirty)(obj_identifier)))
409 for(
const auto &guard_in_list : a_s_writes->second)
419 write_guard |= guard_in_list;
431 for(
const auto &a_s_read_guard : a_s_read.second)
433 guardt g = a_s_read_guard;
440 read_guard |= a_s_read_guard;
452 const exprt l2_true_case =
458 if(a_s_read.second.empty())
459 a_s_read.first =
level2.latest_index(l1_identifier);
465 tmp = l2_false_case.
get();
485 expr = std::move(ssa_l2);
487 a_s_read.second.push_back(
guard);
489 a_s_read.second.back().add(no_write);
524 (!ns.
lookup(obj_identifier).is_shared() && !(*
dirty)(obj_identifier)))
569template <levelt level>
582 else if(expr.
id()==ID_symbol)
589 if(expr.
id()==ID_index)
601 else if(expr.
id()==ID_if)
611 else if(expr.
id()==ID_member)
651 if(type.
id() == ID_array)
655 !array_type.size().is_constant();
657 else if(type.
id() == ID_struct || type.
id() == ID_union)
680 else if(type.
id() == ID_pointer)
684 else if(type.
id() == ID_union_tag)
689 else if(type.
id() == ID_struct_tag)
698template <levelt level>
712 std::pair<l1_typest::iterator, bool> l1_type_entry;
714 !l1_identifier.
empty())
716 l1_type_entry=
l1_types.insert(std::make_pair(l1_identifier, type));
718 if(!l1_type_entry.second)
722 const typet &type_prev=l1_type_entry.first->second;
724 if(type.
id()!=ID_array ||
725 type_prev.
id()!=ID_array ||
729 type=l1_type_entry.first->second;
735 if(type.
id()==ID_array)
739 array_type.size() =
rename<level>(std::move(array_type.size()), ns).get();
742 type.
id() == ID_struct || type.
id() == ID_union ||
743 type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
746 if(type.
id() == ID_struct_tag)
748 else if(type.
id() == ID_union_tag)
763 else if(
component.type().id() != ID_pointer)
767 else if(type.
id()==ID_pointer)
773 !l1_identifier.
empty())
774 l1_type_entry.first->second=type;
786 out <<
"No stack!\n";
790 out <<
source.function_id <<
" " <<
source.pc->location_number <<
"\n";
792 for(
auto stackit =
threads[
source.thread_nr].call_stack.rbegin(),
797 const auto &frame = *stackit;
798 out << frame.calling_location.function_id <<
" "
799 << frame.calling_location.pc->location_number <<
"\n";
805 std::function<std::size_t(
const irep_idt &)> index_generator,
811 const irep_idt l0_name = renamed.get_identifier();
812 const std::size_t l1_index = index_generator(l0_name);
814 if(
const auto old_value =
level1.insert_or_replace(renamed, l1_index))
823 INVARIANT(inserted,
"l1_name expected to be unique by construction");
837 if(ssa.
type().
id() == ID_pointer)
845 rhs =
exprt(ID_invalid);
848 value_set.assign(ssa, l1_rhs, ns,
true,
false);
857 const std::size_t field_generation =
level2.increase_generation(
863 const ssa_exprt &ssa = fs_ssa->get_object_ssa();
864 const std::size_t field_generation =
level2.increase_generation(
874 "symbol to declare should not be replaced by constant propagation");
std::optional< 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)
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
Operator to return the address of an object.
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
Base class for all expressions.
bool is_false() const
Return whether the expression is a constant representing false.
void visit_pre(std::function< void(exprt &)>)
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
The Boolean constant false.
Stack frames – these are used for function calls and for exceptions.
std::set< irep_idt > local_objects
unsigned atomic_section_id
Threads.
sharing_mapt< irep_idt, exprt > propagation
goto_statet()=delete
Constructors.
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.
call_stackt & call_stack()
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
exprt l2_rename_rvalues(exprt lvalue, const namespacet &ns)
static irep_idt guard_identifier()
const incremental_dirtyt * dirty
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
const irep_idt & language_mode
void rename_address(exprt &expr, const namespacet &ns)
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
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...
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...
symex_target_equationt * symex_target
goto_symex_statet(const symex_targett::sourcet &, std::size_t max_field_sensitive_array_size, bool should_simplify, const irep_idt &language_mode, guard_managert &manager, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
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
renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
renamedt< ssa_exprt, level > set_indices(ssa_exprt expr, const namespacet &ns)
Update values up to level.
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.
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & get(const irep_idt &name) const
const std::string & id_string() const
const irep_idt & id() const
Extract member of struct or union.
const exprt & struct_op() const
irep_idt get_component_name() const
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
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().
const typet & base_type() const
The type of the data what we point to.
Wrapper for expressions or types which have been renamed up to a given level.
const underlyingt & get() const
virtual bool simplify(exprt &expr)
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 componentst & components() const
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
std::vector< componentt > componentst
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
typet type
Type of symbol.
The Boolean constant true.
The type of an expression, extends irept.
Thrown when we encounter an instruction, parameters to an instruction etc.
Variables whose address is taken.
#define Forall_operands(it, expr)
bool can_cast_type(const typet &base)
Check whether a reference to a generic typet is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Deprecated expression utility functions.
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.
guard_expr_managert guard_managert
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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)
#define INVARIANT_WITH_DIAGNOSTICS(CONDITION, REASON,...)
Same as invariant, with one or more diagnostics attached Diagnostics can be of any type that has a sp...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
ssa_exprt remove_level_2(ssa_exprt ssa)
bool is_ssa_expr(const exprt &expr)
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
auto component(T &struct_expr, const irep_idt &name, const namespacet &ns) -> decltype(struct_expr.op0())
API to expression classes.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast an exprt to a typecast_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_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 complex_real_exprt & to_complex_real_expr(const exprt &expr)
Cast an exprt to a complex_real_exprt.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
bool has(const renamedt< ssa_exprt, L0 > &ssa) const
void insert(const renamedt< ssa_exprt, L0 > &ssa, std::size_t index)
Assume ssa is not already known.
Identifies source in the context of symbolic execution.
Generate Equation using Symbolic Execution.
static bool failed(bool error_indicator)