33 std::size_t max_field_sensitive_array_size,
43 fresh_l2_name_provider(fresh_l2_name_provider)
45 threads.emplace_back(guard_manager);
77 bool rhs_is_simplified,
79 bool allow_pointer_unsoundness)
110 if(
is_shared && lhs.
type().
id() == ID_pointer && !allow_pointer_unsoundness)
112 "pointer handling for concurrency is unsound");
117 const auto propagation_entry =
propagation.find(l1_identifier);
118 if(!propagation_entry.has_value())
120 else if(propagation_entry->get() != rhs)
142 std::cout <<
"Assigning " << l1_identifier <<
'\n';
144 std::cout <<
"**********************\n";
150template <levelt level>
155 level ==
L0 || level ==
L1,
156 "rename_ssa can only be used for levels L0 and L1");
169template <levelt level>
178 "must handle all renaming levels");
182 exprt original_expr = expr;
232 else if(expr.
id()==ID_symbol)
234 const auto &type =
as_const(expr).type();
237 if(type.id() == ID_code || type.id() == ID_mathematical_function)
245 else if(expr.
id()==ID_address_of)
250 as_const(address_of_expr).object().type();
278 c_with_expr->type() != c_with_expr->old().type())
283 expr.
id() != ID_with ||
285 "Type of renamed expr should be the same as operands for with_exprt",
289 expr.
id() != ID_if ||
291 "Type of renamed expr should be the same as operands for if_exprt",
293 to_if_expr(c_expr).true_case().type().pretty());
295 expr.
id() != ID_if ||
297 "Type of renamed expr should be the same as operands for if_exprt",
299 to_if_expr(c_expr).false_case().type().pretty());
317 if(lvalue.
id() == ID_symbol)
325 else if(lvalue.
id() == ID_typecast)
330 else if(lvalue.
id() == ID_member)
335 else if(lvalue.
id() == ID_index)
340 index_lvalue.index() =
rename(index_lvalue.index(), ns).get();
343 lvalue.
id() == ID_byte_extract_little_endian ||
344 lvalue.
id() == ID_byte_extract_big_endian)
349 byte_extract_lvalue.offset() =
rename(byte_extract_lvalue.offset(), ns);
351 else if(lvalue.
id() == ID_if)
355 if_lvalue.cond() =
rename(if_lvalue.cond(), ns);
356 if(!if_lvalue.cond().is_false())
358 if(!if_lvalue.cond().is_true())
361 else if(lvalue.
id() == ID_complex_real)
366 else if(lvalue.
id() == ID_complex_imag)
374 "l2_rename_rvalues case `" + lvalue.
id_string() +
"' not handled");
397 (!ns.
lookup(obj_identifier).is_shared() && !(*
dirty)(obj_identifier)))
418 for(
const auto &guard_in_list : a_s_writes->second)
428 write_guard |= guard_in_list;
432 not_exprt no_write(write_guard.as_expr());
440 for(
const auto &a_s_read_guard : a_s_read.second)
442 guardt g = a_s_read_guard;
449 read_guard |= a_s_read_guard;
461 const exprt l2_true_case =
467 if(a_s_read.second.empty())
468 a_s_read.first =
level2.latest_index(l1_identifier);
474 tmp = l2_false_case.
get();
494 expr = std::move(ssa_l2);
496 a_s_read.second.push_back(
guard);
498 a_s_read.second.back().add(no_write);
533 (!ns.
lookup(obj_identifier).is_shared() && !(*
dirty)(obj_identifier)))
578template <levelt level>
591 else if(expr.
id()==ID_symbol)
598 if(expr.
id()==ID_index)
610 else if(expr.
id()==ID_if)
620 else if(expr.
id()==ID_member)
660 if(type.
id() == ID_array)
664 !array_type.size().is_constant();
666 else if(type.
id() == ID_struct || type.
id() == ID_union)
689 else if(type.
id() == ID_pointer)
693 else if(type.
id() == ID_union_tag)
698 else if(type.
id() == ID_struct_tag)
707template <levelt level>
721 std::pair<l1_typest::iterator, bool> l1_type_entry;
723 !l1_identifier.
empty())
725 l1_type_entry=
l1_types.insert(std::make_pair(l1_identifier, type));
727 if(!l1_type_entry.second)
731 const typet &type_prev=l1_type_entry.first->second;
733 if(type.
id()!=ID_array ||
734 type_prev.
id()!=ID_array ||
738 type=l1_type_entry.first->second;
744 if(type.
id()==ID_array)
748 array_type.size() =
rename<level>(std::move(array_type.size()), ns).get();
751 type.
id() == ID_struct || type.
id() == ID_union ||
752 type.
id() == ID_struct_tag || type.
id() == ID_union_tag)
755 if(type.
id() == ID_struct_tag)
757 else if(type.
id() == ID_union_tag)
772 else if(
component.type().id() != ID_pointer)
776 else if(type.
id()==ID_pointer)
782 !l1_identifier.
empty())
783 l1_type_entry.first->second=type;
806 out <<
"No stack!\n";
810 out <<
source.function_id <<
" " <<
source.pc->location_number <<
"\n";
812 for(
auto stackit =
threads[
source.thread_nr].call_stack.rbegin(),
817 const auto &frame = *stackit;
818 out << frame.calling_location.function_id <<
" "
819 << frame.calling_location.pc->location_number <<
"\n";
825 std::function<std::size_t(
const irep_idt &)> index_generator,
831 const irep_idt l0_name = renamed.get_identifier();
832 const std::size_t l1_index = index_generator(l0_name);
834 if(
const auto old_value =
level1.insert_or_replace(renamed, l1_index))
843 INVARIANT(inserted,
"l1_name expected to be unique by construction");
857 if(ssa.
type().
id() == ID_pointer)
865 rhs =
exprt(ID_invalid);
868 value_set.assign(ssa, l1_rhs, ns,
true,
false);
877 const std::size_t field_generation =
level2.increase_generation(
883 const ssa_exprt &ssa = fs_ssa->get_object_ssa();
884 const std::size_t field_generation =
level2.increase_generation(
894 "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
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
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.
goto_symex_statet(const symex_targett::sourcet &, std::size_t max_field_sensitive_array_size, bool should_simplify, guard_managert &manager, std::function< std::size_t(const irep_idt &)> fresh_l2_name_provider)
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
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.
static void get_l1_name(exprt &expr)
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.
bool simplify(exprt &expr, const namespacet &ns)
#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)