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";
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
The type of an expression, extends irept.
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
const std::string & id2string(const irep_idt &d)
bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns)
thread encoding
static void increase_counter(const current_namest::iterator &it)
Increase the counter corresponding to an identifier.
goto_programt::const_targett pc
void print_backtrace(std::ostream &) const
Dumps the current state of symex, printing the function name and location number for each stack frame...
Variables whose address is taken.
Determine whether an expression is constant.
Deprecated expression utility functions.
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
bool run_validation_checks
Should the additional validation checks be run?
const irep_idt & get_identifier() const
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...
std::vector< componentt > componentst
bool is_false() const
Return whether the expression is a constant representing false.
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
const symbol_typet & to_symbol_type(const typet &type)
Cast a typet to a symbol_typet.
Thrown when we encounter an instruction, parameters to an instruction etc.
symex_target_equationt * symex_target
const componentst & components() const
bool is_incomplete() const
The trinary if-then-else operator.
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast an exprt to an address_of_exprt.
void set_level_2(unsigned i)
void set_l1_indices(ssa_exprt &expr, const namespacet &ns)
bool get_bool(const irep_namet &name) const
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...
std::map< irep_idt, exprt > propagation
void get_original_name(exprt &expr) const
Extract member of struct or union.
const irep_idt get_level_1() const
const irep_idt & id() const
virtual bool is_constant(const exprt &) const
This function determines what expressions are to be propagated as "constants".
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
std::unordered_map< ssa_exprt, a_s_r_entryt, irep_hash > read_in_atomic_section
void set_l0_indices(ssa_exprt &expr, const namespacet &ns)
std::set< exprt > expr_sett
Set of expressions; only used for the get API, not for internal data representation.
const union_tag_typet & to_union_tag_type(const typet &type)
Cast a typet to a union_tag_typet.
std::unordered_map< ssa_exprt, a_s_w_entryt, irep_hash > written_in_atomic_section
static bool check_renaming_l1(const exprt &expr)
API to expression classes.
const type_with_subtypet & to_type_with_subtype(const typet &type)
bool is_constant(const exprt &expr) const override
This function determines what expressions are to be propagated as "constants".
unsigned current_count(const irep_idt &identifier) const
Counter corresponding to an identifier.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static void get_l1_name(exprt &expr)
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast an exprt to a member_exprt.
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.
bool has_prefix(const std::string &s, const std::string &prefix)
const struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_typet.
const exprt & size() const
std::vector< threadt > threads
bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
#define forall_operands(it, expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
current_namest current_names
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
void set_l2_indices(ssa_exprt &expr, const namespacet &ns)
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
unsigned atomic_section_id
The Boolean constant false.
static bool check_renaming(const exprt &expr)
write to a variable
const with_exprt & to_with_expr(const exprt &expr)
Cast an exprt to a with_exprt.
typet type
Type of symbol.
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 assignme...
Base type for structs and unions.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Base class for all expressions.
const exprt & struct_op() const
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a typet to a struct_union_typet.
irep_idt get_object_name() const
const exprt & get_original_expr() const
irep_idt get_component_name() const
void output_propagation_map(std::ostream &)
Print the constant propagation map in a human-friendly format.
irept & add(const irep_namet &name)
#define Forall_operands(it, expr)
void output(const namespacet &ns, std::ostream &out) const
Pretty-print this value-set.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions, goto_programs, exprts, etc.
const irep_idt get_level_2() const
Generic exception types primarily designed for use with invariants.
Expression providing an SSA-renamed symbol of expressions.
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void add(const exprt &expr)
const componentt & get_component(const irep_idt &component_name) const
Get the reference to a component with given name.
void rename_address(exprt &expr, const namespacet &ns, levelt level)
symex_targett::sourcet source