Go to the documentation of this file.
32 symex_target(nullptr),
50 if(type.
id()==ID_array)
52 else if(type.
id()==ID_struct ||
53 type.
id()==ID_union ||
71 if(expr.
id()==ID_symbol)
74 return expr.
type().
id()!=ID_code;
96 expr.
id() == ID_address_of &&
102 expr.
id() == ID_address_of &&
109 else if(expr.
id()==ID_symbol)
112 return expr.
type().
id()!=ID_code;
133 if(expr.
id() == ID_mult)
138 if(it->find(ID_C_c_sizeof_type).is_not_nil())
146 else if(expr.
id() == ID_with)
167 bool rhs_is_simplified,
169 bool allow_pointer_unsoundness)
185 || l1_identifier==
"goto_symex::\\guard"
186 || ns.
lookup(l1_identifier).is_shared()
192 const auto level2_it =
207 if(
is_shared && lhs.
type().
id() == ID_pointer && !allow_pointer_unsoundness)
209 "pointer handling for concurrency is unsound");
237 std::cout <<
"Assigning " << l1_identifier <<
'\n';
239 std::cout <<
"**********************\n";
280 if(expr.
id()==ID_symbol &&
324 else if(expr.
id()==ID_symbol)
341 else if(expr.
id()==ID_address_of)
357 if(expr.
id()==ID_with)
359 else if(expr.
id()==ID_if)
364 "true case of to_if_expr should be of same type "
383 obj_identifier ==
"goto_symex::\\guard" ||
384 (!ns.
lookup(obj_identifier).is_shared() && !(
dirty)(obj_identifier)))
400 for(
const auto &guard_in_list : a_s_writes->second)
410 write_guard |= guard_in_list;
423 for(std::list<guardt>::const_iterator it=a_s_read.second.begin();
424 it!=a_s_read.second.end();
438 exprt cond=read_guard.as_expr();
439 if(!no_write.op().is_false())
445 if(a_s_read.second.empty())
479 a_s_read.second.push_back(
guard);
480 if(!no_write.op().is_false())
481 a_s_read.second.back().
add(no_write);
486 const auto level2_it =
526 obj_identifier ==
"goto_symex::\\guard" ||
527 (!ns.
lookup(obj_identifier).is_shared() && !(
dirty)(obj_identifier)))
556 if(expr.
id()==ID_symbol &&
567 else if(expr.
id()==ID_symbol)
574 if(expr.
id()==ID_index)
585 else if(expr.
id()==ID_if)
595 else if(expr.
id()==ID_member)
613 expr.
type()=comp.type();
640 std::pair<l1_typest::iterator, bool> l1_type_entry;
642 !l1_identifier.
empty())
644 l1_type_entry=
l1_types.insert(std::make_pair(l1_identifier, type));
646 if(!l1_type_entry.second)
650 const typet &type_prev=l1_type_entry.first->second;
652 if(type.
id()!=ID_array ||
653 type_prev.
id()!=ID_array ||
657 type=l1_type_entry.first->second;
663 if(type.
id()==ID_array)
667 rename(array_type.size(), ns, level);
669 else if(type.
id()==ID_struct ||
670 type.
id()==ID_union ||
676 for(struct_union_typet::componentst::iterator
677 it=components.begin();
678 it!=components.end();
681 if(it->type().id()==ID_array)
683 else if(it->type().id()!=ID_pointer)
686 else if(type.
id()==ID_pointer)
690 else if(type.
id() == ID_symbol_type)
694 rename(type, l1_identifier, ns, level);
696 else if(type.
id() == ID_union_tag)
700 rename(type, l1_identifier, ns, level);
702 else if(type.
id() == ID_struct_tag)
706 rename(type, l1_identifier, ns, level);
710 !l1_identifier.
empty())
711 l1_type_entry.first->second=type;
718 if(expr.
id()==ID_symbol &&
730 if(type.
id()==ID_array)
736 else if(type.
id()==ID_struct ||
737 type.
id()==ID_union ||
743 for(struct_union_typet::componentst::iterator
744 it=components.begin();
745 it!=components.end();
749 else if(type.
id()==ID_pointer)
759 if(expr.
id()==ID_symbol &&
776 out <<
"No stack!\n";
787 const auto &frame = *stackit;
788 if(frame.calling_location.is_set)
790 out << frame.calling_location.pc->function <<
" "
791 << frame.calling_location.pc->location_number <<
"\n";
803 out << name_value.first <<
" <- " <<
format(name_value.second) <<
"\n";
Determine whether an expression is constant.
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.
#define PRECONDITION(CONDITION)
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
bool is_incomplete() const
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
void set_l0_indices(ssa_exprt &expr, const namespacet &ns)
#define Forall_operands(it, expr)
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
void output_propagation_map(std::ostream &)
Print the constant propagation map in a human-friendly format.
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.
goto_programt::const_targett pc
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.
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
Thrown when we encounter an instruction, parameters to an instruction etc.
void add(const exprt &expr)
The trinary if-then-else operator.
irept & add(const irep_namet &name)
void get_original_name(exprt &expr) const
void set_l1_indices(ssa_exprt &expr, const namespacet &ns)
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
const type_with_subtypet & to_type_with_subtype(const typet &type)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
Base class for all expressions.
irep_idt get_object_name() const
std::vector< componentt > componentst
symex_targett::sourcet source
static void increase_counter(const current_namest::iterator &it)
Increase the counter corresponding to an identifier.
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
bool is_true() const
Return whether the expression is a constant representing true.
const exprt & get_original_expr() const
bool is_false() const
Return whether the expression is a constant representing false.
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
static bool check_renaming_l1(const exprt &expr)
unsigned current_count(const irep_idt &identifier) const
Counter corresponding to an identifier.
Expression providing an SSA-renamed symbol of expressions.
const exprt & size() const
std::map< irep_idt, exprt > propagation
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
typet & type()
Return the type of the expression.
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::set< exprt > expr_sett
Set of expressions; only used for the get API, not for internal data representation.
bool get_bool(const irep_namet &name) const
std::vector< threadt > threads
void set_l2_indices(ssa_exprt &expr, const namespacet &ns)
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.
const std::string & id2string(const irep_idt &d)
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
unsigned atomic_section_id
#define forall_operands(it, expr)
bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
const exprt & struct_op() const
const irep_idt & get_identifier() const
void rename_address(exprt &expr, const namespacet &ns, levelt level)
symex_target_equationt * symex_target
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
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
The Boolean constant false.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
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...
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
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.
void output(const namespacet &ns, std::ostream &out) const
Pretty-print this value-set.
static bool check_renaming(const exprt &expr)
write to a variable
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
const irep_idt get_level_1() const
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
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...
void set_level_2(unsigned i)
static void get_l1_name(exprt &expr)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
bool has_prefix(const std::string &s, const std::string &prefix)
irep_idt get_component_name() const
current_namest current_names
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.