26 symex_target(nullptr),
49 if(obj_identifier==
"goto_symex::\\guard")
53 const bool found_l0 = !ns.
lookup(obj_identifier, s);
55 found_l0,
"level0: failed to find " +
id2string(obj_identifier));
58 if(s->
type.
id()==ID_code ||
74 current_namest::const_iterator it=current_names.find(l0_name);
75 if(it==current_names.end())
89 if(expr.
id()==ID_address_of)
95 else if(expr.
id()==ID_typecast)
101 else if(expr.
id()==ID_plus)
109 else if(expr.
id()==ID_mult)
114 if(it->find(ID_C_c_sizeof_type).is_not_nil())
122 else if(expr.
id()==ID_array)
130 else if(expr.
id()==ID_array_of)
134 else if(expr.
id()==ID_with)
146 else if(expr.
id()==ID_struct)
154 else if(expr.
id()==ID_union)
163 else if(expr.
id()==ID_byte_update_big_endian ||
164 expr.
id()==ID_byte_update_little_endian)
179 if(expr.
id()==ID_symbol)
181 else if(expr.
id()==ID_index)
188 else if(expr.
id()==ID_member)
191 throw "member expects one operand";
195 else if(expr.
id()==ID_string_constant)
206 if(type.
id()==ID_array)
208 else if(type.
id()==ID_struct ||
209 type.
id()==ID_union ||
215 for(struct_union_typet::componentst::const_iterator
216 it=components.begin();
217 it!=components.end();
233 if(expr.
id()==ID_symbol)
236 return expr.
type().
id()!=ID_code;
257 if(expr.
id()==ID_address_of &&
258 expr.
op0().
id()==ID_symbol)
260 else if(expr.
id()==ID_address_of &&
261 expr.
op0().
id()==ID_index)
264 else if(expr.
id()==ID_symbol)
267 return expr.
type().
id()!=ID_code;
288 std::cerr << expr.
pretty() <<
'\n';
301 std::cerr << expr.
pretty() <<
'\n';
313 bool rhs_is_simplified,
315 bool allow_pointer_unsoundness)
328 || l1_identifier==
"goto_symex::\\guard" 329 || ns.
lookup(l1_identifier).is_shared()
347 if(
is_shared && lhs.
type().
id() == ID_pointer && !allow_pointer_unsoundness)
348 throw "pointer handling for concurrency is unsound";
373 std::cout <<
"Assigning " << l1_identifier <<
'\n';
375 std::cout <<
"**********************\n";
381 if(expr.
id()==ID_symbol)
383 valuest::const_iterator it =
388 else if(expr.
id()==ID_address_of)
440 if(expr.
id()==ID_symbol &&
445 if(level==
L0 || level==
L1)
469 propagationt::valuest::const_iterator p_it=
479 else if(expr.
id()==ID_symbol)
496 else if(expr.
id()==ID_address_of)
499 expr.
operands().size() == 1,
"address_of should have a single operand");
502 expr.
type().
id() == ID_pointer,
503 "type of address_of should be ID_pointer");
516 if(expr.
id()==ID_with)
518 else if(expr.
id()==ID_if)
523 "true case of to_if_expr should be of same type " 542 obj_identifier ==
"goto_symex::\\guard" ||
543 (!ns.
lookup(obj_identifier).is_shared() && !(
dirty)(obj_identifier)))
556 written_in_atomic_sectiont::const_iterator a_s_writes=
560 for(a_s_w_entryt::const_iterator it=a_s_writes->second.begin();
561 it!=a_s_writes->second.end();
585 for(std::list<guardt>::const_iterator it=a_s_read.second.begin();
586 it!=a_s_read.second.end();
600 exprt cond=read_guard.as_expr();
601 if(!no_write.op().is_false())
607 if(a_s_read.second.empty())
640 a_s_read.second.push_back(
guard);
641 if(!no_write.op().is_false())
642 a_s_read.second.back().
add(no_write);
686 obj_identifier ==
"goto_symex::\\guard" ||
687 (!ns.
lookup(obj_identifier).is_shared() && !(
dirty)(obj_identifier)))
716 if(expr.
id()==ID_symbol &&
727 else if(expr.
id()==ID_symbol)
734 if(expr.
id()==ID_index)
745 else if(expr.
id()==ID_if)
755 else if(expr.
id()==ID_member)
770 expr.
type()=comp.type();
797 std::pair<l1_typest::iterator, bool> l1_type_entry;
799 !l1_identifier.
empty())
801 l1_type_entry=
l1_types.insert(std::make_pair(l1_identifier, type));
803 if(!l1_type_entry.second)
807 const typet &type_prev=l1_type_entry.first->second;
809 if(type.
id()!=ID_array ||
810 type_prev.
id()!=ID_array ||
814 type=l1_type_entry.first->second;
820 if(type.
id()==ID_array)
825 else if(type.
id()==ID_struct ||
826 type.
id()==ID_union ||
832 for(struct_union_typet::componentst::iterator
833 it=components.begin();
834 it!=components.end();
837 if(it->type().id()==ID_array)
839 else if(it->type().id()!=ID_pointer)
842 else if(type.
id()==ID_pointer)
846 else if(type.
id()==ID_symbol)
851 rename(type, l1_identifier, ns, level);
855 !l1_identifier.
empty())
856 l1_type_entry.first->second=type;
863 if(expr.
id()==ID_symbol &&
875 if(type.
id()==ID_array)
880 else if(type.
id()==ID_struct ||
881 type.
id()==ID_union ||
887 for(struct_union_typet::componentst::iterator
888 it=components.begin();
889 it!=components.end();
893 else if(type.
id()==ID_pointer)
903 if(expr.
id()==ID_symbol &&
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
The type of an expression.
#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 assert_l2_renaming(const exprt &expr)
goto_programt::const_targett pc
class goto_symex_statet::propagationt propagation
read_in_atomic_sectiont read_in_atomic_section
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Variables whose address is taken.
void set_level_1(unsigned i)
void remove(const irep_idt &identifier)
void rename(exprt &expr, const namespacet &ns, levelt level=L2)
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...
void operator()(exprt &expr)
std::vector< componentt > componentst
goto_symex_statet::level0t level0
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
symex_target_equationt * symex_target
void increase_counter(const irep_idt &identifier)
void set_ssa_indices(ssa_exprt &expr, const namespacet &ns, levelt level=L2)
const componentst & components() const
bool is_incomplete() const
The trinary if-then-else operator.
written_in_atomic_sectiont written_in_atomic_section
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
void set_level_2(unsigned i)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
bool get_bool(const irep_namet &name) const
const irep_idt get_l1_object_identifier() const
void switch_to_thread(unsigned t)
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
write to a sharedvariable
void get_original_name(exprt &expr) const
Extract member of struct or union.
bool constant_propagation(const exprt &expr) const
This function determines what expressions are to be propagated as "constants".
const irep_idt get_level_1() const
goto_symex_statet::level2t level2
const irep_idt & id() const
bool constant_propagation_reference(const exprt &expr) const
this function determines which reference-typed expressions are constant
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
void set_level_0(unsigned i)
std::set< exprt > expr_sett
Set of expressions; only used for the get API, not for internal data representation.
static bool check_renaming_l1(const exprt &expr)
API to expression classes.
#define PRECONDITION(CONDITION)
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic 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 variable
bool has_prefix(const std::string &s, const std::string &prefix)
goto_symex_statet::level1t level1
const exprt & size() const
bool is_shared(const namespacet &ns, const symbol_exprt &symbol_expr)
#define forall_operands(it, expr)
const irep_idt get_level_0() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
const typet & follow(const typet &) const
current_namest current_names
bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns)
thread encoding
Operator to return the address of an object.
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 a generic 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
void get_l1_name(exprt &expr) const
Base type of C structs and unions, and C++ classes.
void operator()(ssa_exprt &ssa_expr)
unsigned current_count(const irep_idt &identifier) const
static void assert_l1_renaming(const exprt &expr)
const array_typet & to_array_type(const typet &type)
Cast a generic 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 generic typet to a struct_union_typet.
irep_idt get_object_name() const
const exprt & get_original_expr() const
irep_idt get_component_name() const
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
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.
void operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
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 a generic exprt to an index_exprt.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See namespace_baset::lookup().
void add(const exprt &expr)
const componentt & get_component(const irep_idt &component_name) const
void rename_address(exprt &expr, const namespacet &ns, levelt level)
symex_targett::sourcet source