26 symex_target(nullptr),
37 goto_functionst::function_mapt::const_iterator it=
41 throw "program has no entry point";
62 if(obj_identifier==
"goto_symex::\\guard")
67 if(ns.
lookup(obj_identifier, s))
69 std::cerr <<
"level0: failed to find " << obj_identifier <<
'\n';
74 if(s->
type.
id()==ID_code ||
90 current_namest::const_iterator it=current_names.find(l0_name);
91 if(it==current_names.end())
105 if(expr.
id()==ID_address_of)
111 else if(expr.
id()==ID_typecast)
117 else if(expr.
id()==ID_plus)
125 else if(expr.
id()==ID_mult)
130 if(it->find(ID_C_c_sizeof_type).is_not_nil())
138 else if(expr.
id()==ID_array)
146 else if(expr.
id()==ID_array_of)
150 else if(expr.
id()==ID_with)
162 else if(expr.
id()==ID_struct)
170 else if(expr.
id()==ID_union)
179 else if(expr.
id()==ID_byte_update_big_endian ||
180 expr.
id()==ID_byte_update_little_endian)
195 if(expr.
id()==ID_symbol)
197 else if(expr.
id()==ID_index)
204 else if(expr.
id()==ID_member)
207 throw "member expects one operand";
211 else if(expr.
id()==ID_string_constant)
222 if(type.
id()==ID_array)
224 else if(type.
id()==ID_struct ||
225 type.
id()==ID_union ||
231 for(struct_union_typet::componentst::const_iterator
232 it=components.begin();
233 it!=components.end();
249 if(expr.
id()==ID_symbol)
252 return expr.
type().
id()!=ID_code;
273 if(expr.
id()==ID_address_of &&
274 expr.
op0().
id()==ID_symbol)
276 else if(expr.
id()==ID_address_of &&
277 expr.
op0().
id()==ID_index)
280 else if(expr.
id()==ID_symbol)
283 return expr.
type().
id()!=ID_code;
304 std::cerr << expr.
pretty() <<
'\n';
317 std::cerr << expr.
pretty() <<
'\n';
329 bool rhs_is_simplified,
343 || l1_identifier==
"goto_symex::\\guard" 344 || ns.
lookup(l1_identifier).is_shared()
384 std::cout <<
"Assigning " << l1_identifier <<
'\n';
386 std::cout <<
"**********************\n";
392 if(expr.
id()==ID_symbol)
394 valuest::const_iterator it=
395 values.find(expr.
get(ID_identifier));
399 else if(expr.
id()==ID_address_of)
451 if(expr.
id()==ID_symbol &&
456 if(level==
L0 || level==
L1)
480 propagationt::valuest::const_iterator p_it=
490 else if(expr.
id()==ID_symbol)
507 else if(expr.
id()==ID_address_of)
511 assert(expr.
type().
id()==ID_pointer);
524 if(expr.
id()==ID_with)
526 else if(expr.
id()==ID_if)
547 if(obj_identifier==
"goto_symex::\\guard" ||
548 (!ns.
lookup(obj_identifier).is_shared() &&
549 !(*dirty)(obj_identifier)))
562 written_in_atomic_sectiont::const_iterator a_s_writes=
566 for(a_s_w_entryt::const_iterator it=a_s_writes->second.begin();
567 it!=a_s_writes->second.end();
591 for(std::list<guardt>::const_iterator it=a_s_read.second.begin();
592 it!=a_s_read.second.end();
606 exprt cond=read_guard.as_expr();
607 if(!no_write.op().is_false())
613 if(a_s_read.second.empty())
646 a_s_read.second.push_back(
guard);
647 if(!no_write.op().is_false())
648 a_s_read.second.back().
add(no_write);
692 if(obj_identifier==
"goto_symex::\\guard" ||
693 (!ns.
lookup(obj_identifier).is_shared() &&
694 !(*dirty)(obj_identifier)))
723 if(expr.
id()==ID_symbol &&
734 else if(expr.
id()==ID_symbol)
741 if(expr.
id()==ID_index)
752 else if(expr.
id()==ID_if)
762 else if(expr.
id()==ID_member)
776 assert(comp.is_not_nil());
777 expr.
type()=comp.type();
804 std::pair<l1_typest::iterator, bool> l1_type_entry;
806 !l1_identifier.
empty())
808 l1_type_entry=
l1_types.insert(std::make_pair(l1_identifier, type));
810 if(!l1_type_entry.second)
814 const typet &type_prev=l1_type_entry.first->second;
816 if(type.
id()!=ID_array ||
817 type_prev.
id()!=ID_array ||
821 type=l1_type_entry.first->second;
827 if(type.
id()==ID_array)
832 else if(type.
id()==ID_struct ||
833 type.
id()==ID_union ||
839 for(struct_union_typet::componentst::iterator
840 it=components.begin();
841 it!=components.end();
844 if(it->type().id()==ID_array)
846 else if(it->type().id()!=ID_pointer)
849 else if(type.
id()==ID_pointer)
853 else if(type.
id()==ID_symbol)
858 rename(type, l1_identifier, ns, level);
862 !l1_identifier.
empty())
863 l1_type_entry.first->second=type;
870 if(expr.
id()==ID_symbol &&
882 if(type.
id()==ID_array)
887 else if(type.
id()==ID_struct ||
888 type.
id()==ID_union ||
894 for(struct_union_typet::componentst::iterator
895 it=components.begin();
896 it!=components.end();
900 else if(type.
id()==ID_pointer)
910 if(expr.
id()==ID_symbol &&
const with_exprt & to_with_expr(const exprt &expr)
Cast a generic exprt to a with_exprt.
The type of an expression.
#define INVARIANT_STRUCTURED(CONDITION, TYPENAME,...)
const typecast_exprt & to_typecast_expr(const exprt &expr)
Cast a generic exprt to a typecast_exprt.
const typet & follow(const typet &src) const
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
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)
instructionst instructions
The list of instructions in the goto program.
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)
void operator()(exprt &expr)
std::vector< componentt > componentst
const member_exprt & to_member_expr(const exprt &expr)
Cast a generic exprt to a member_exprt.
goto_symex_statet::level0t level0
std::pair< unsigned, std::list< guardt > > a_s_r_entryt
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
symex_targett * symex_target
The trinary if-then-else operator.
written_in_atomic_sectiont written_in_atomic_section
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)
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
const struct_union_typet & to_struct_union_type(const typet &type)
Cast a generic typet to a struct_union_typet.
goto_symex_statet::level2t level2
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
void initialize(const goto_functionst &goto_functions)
const irep_idt & id() const
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
bool constant_propagation_reference(const exprt &expr) const
this function determines which reference-typed expressions are constant
void set_level_0(unsigned i)
const address_of_exprt & to_address_of_expr(const exprt &expr)
Cast a generic exprt to an address_of_exprt.
const symbol_typet & to_symbol_type(const typet &type)
Cast a generic typet to a symbol_typet.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
std::set< exprt > expr_sett
static irep_idt entry_point()
static bool check_renaming_l1(const exprt &expr)
API to expression classes.
const irep_idt & get(const irep_namet &name) const
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
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0
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.
function_mapt function_map
unsigned atomic_section_id
The boolean constant false.
bool has_prefix(const std::string &s, const std::string &prefix)
static bool check_renaming(const exprt &expr)
write to a variable
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
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)=0
typet type
Type of symbol.
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)
Base class for all expressions.
const exprt & struct_op() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
void assignment(ssa_exprt &lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value)
irep_idt get_object_name() const
const exprt & get_original_expr() const
irep_idt get_component_name() const
irept & add(const irep_namet &name)
#define Forall_operands(it, expr)
symex_targett::sourcet calling_location
void output(const namespacet &ns, std::ostream &out) const
void operator()(ssa_exprt &ssa_expr, const namespacet &ns, unsigned thread_nr)
const typet & subtype() const
const irep_idt get_level_2() const
Generic exception types primarily designed for use with invariants.
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_rhs, unsigned atomic_section_id, const sourcet &source)=0
Expression providing an SSA-renamed symbol of expressions.
goto_programt::const_targett end_of_function
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