diff --git a/src/analyses/Makefile b/src/analyses/Makefile index 7502f6a..70d78a1 100644 --- a/src/analyses/Makefile +++ b/src/analyses/Makefile @@ -2,7 +2,7 @@ SRC = natural_loops.cpp is_threaded.cpp dirty.cpp interval_analysis.cpp \ invariant_set.cpp invariant_set_domain.cpp invariant_propagation.cpp \ static_analysis.cpp uninitialized_domain.cpp local_may_alias.cpp \ locals.cpp goto_check.cpp call_graph.cpp interval_domain.cpp \ - reaching_definitions.cpp ai.cpp + goto_rw.cpp reaching_definitions.cpp ai.cpp may_alias.cpp INCLUDES= -I .. diff --git a/src/analyses/cfg_dominators.h b/src/analyses/cfg_dominators.h index c48d3cd..f297ac0 100644 --- a/src/analyses/cfg_dominators.h +++ b/src/analyses/cfg_dominators.h @@ -16,6 +16,7 @@ Author: Georg Weissenbacher, georg@weissenbacher.name #include #include +#include template class cfg_dominators_templatet @@ -26,13 +27,10 @@ public: struct nodet { target_sett dominators; - std::list successors, predecessors; - - T PC; }; - typedef std::map node_mapt; - node_mapt node_map; + typedef procedure_local_cfg_baset cfgt; + cfgt cfg; void operator()(P &program); @@ -43,8 +41,6 @@ public: protected: void initialise(P &program); - void construct_cfg(P &program); - void construct_cfg(P &program, T PC); void fixedpoint(P &program); }; @@ -69,88 +65,47 @@ std::ostream &operator << ( return out; } -template -void cfg_dominators_templatet::operator()(P &program) -{ - initialise(program); - fixedpoint(program); -} - /*******************************************************************\ -Function: cfg_dominators_templatet::initialise +Function: operator () Inputs: Outputs: - Purpose: Initialises the elements of the fixed point analysis + Purpose: Compute dominators \*******************************************************************/ template -void cfg_dominators_templatet::initialise(P &program) +void cfg_dominators_templatet::operator()(P &program) { - construct_cfg(program); - - // initialise top element - for(typename node_mapt::const_iterator e_it=node_map.begin(); - e_it!=node_map.end(); ++e_it) - top.insert(e_it->first); + initialise(program); + fixedpoint(program); } /*******************************************************************\ -Function: cfg_dominators_templatet::construct_cfg +Function: cfg_dominators_templatet::initialise Inputs: Outputs: - Purpose: Initialises the predecessor and successor sets + Purpose: Initialises the elements of the fixed point analysis \*******************************************************************/ template -void cfg_dominators_templatet::construct_cfg(P &program) -{ - for(T it = program.instructions.begin(); - it != program.instructions.end(); - ++it) - { - construct_cfg(program, it); - } -} - -/*******************************************************************\ - -Function: cfg_dominators_templatet::construct_cfg - - Inputs: - - Outputs: - - Purpose: Initialises the predecessor and successor sets - -\*******************************************************************/ - -template -void cfg_dominators_templatet::construct_cfg(P &program, T PC) +void cfg_dominators_templatet::initialise(P &program) { - nodet &node=node_map[PC]; - node.PC=PC; - - program.get_successors(PC, node.successors); - - // now do backward edges - for(typename std::list::const_iterator - s_it=node.successors.begin(); - s_it!=node.successors.end(); - s_it++) - { - node_map[*s_it].predecessors.push_back(node.PC); - } + cfg(program); + // initialise top element + for(typename cfgt::entry_mapt::const_iterator + e_it=cfg.entry_map.begin(); + e_it!=cfg.entry_map.end(); ++e_it) + top.insert(cfg[e_it->second].PC); } /*******************************************************************\ @@ -171,14 +126,14 @@ void cfg_dominators_templatet::fixedpoint(P &program) std::list worklist; entry_node = program.instructions.begin(); - nodet &n=node_map[entry_node]; + typename cfgt::nodet &n=cfg[cfg.entry_map[entry_node]]; n.dominators.insert(entry_node); - for(typename std::list::const_iterator - s_it=n.successors.begin(); - s_it!=n.successors.end(); + for(typename cfgt::edgest::const_iterator + s_it=n.out.begin(); + s_it!=n.out.end(); ++s_it) - worklist.push_back(*s_it); + worklist.push_back(cfg[s_it->first].PC); while(!worklist.empty()) { @@ -187,26 +142,26 @@ void cfg_dominators_templatet::fixedpoint(P &program) worklist.pop_front(); bool changed=false; - nodet &node=node_map[current]; + typename cfgt::nodet &node=cfg[cfg.entry_map[current]]; if(node.dominators.empty()) - for(typename std::list::const_iterator - p_it=node.predecessors.begin(); - !changed && p_it!=node.predecessors.end(); + for(typename cfgt::edgest::const_iterator + p_it=node.in.begin(); + !changed && p_it!=node.in.end(); ++p_it) - if(!node_map[*p_it].dominators.empty()) + if(!cfg[p_it->first].dominators.empty()) { - node.dominators=node_map[*p_it].dominators; + node.dominators=cfg[p_it->first].dominators; node.dominators.insert(current); changed=true; } // compute intersection of predecessors - for(typename std::list::const_iterator - p_it=node.predecessors.begin(); - p_it!=node.predecessors.end(); + for(typename cfgt::edgest::const_iterator + p_it=node.in.begin(); + p_it!=node.in.end(); ++p_it) { - const target_sett &other=node_map[*p_it].dominators; + const target_sett &other=cfg[p_it->first].dominators; if(other.empty()) continue; @@ -236,12 +191,12 @@ void cfg_dominators_templatet::fixedpoint(P &program) if(changed) // fixed point for node reached? { - for(typename std::list::const_iterator - s_it=node.successors.begin(); - s_it!=node.successors.end(); + for(typename cfgt::edgest::const_iterator + s_it=node.out.begin(); + s_it!=node.out.end(); ++s_it) { - worklist.push_back(*s_it); + worklist.push_back(cfg[s_it->first].PC); } } } @@ -262,8 +217,9 @@ Function: cfg_dominators_templatet::output template void cfg_dominators_templatet::output(std::ostream &out) const { - for(typename node_mapt::const_iterator it=node_map.begin(); - it!=node_map.end(); ++it) + for(typename cfgt::entry_mapt::const_iterator + it=cfg.entry_map.begin(); + it!=cfg.entry_map.end(); ++it) { unsigned n=it->first->location_number; diff --git a/src/analyses/dirty.h b/src/analyses/dirty.h index 4b936b7..8be3f37 100644 --- a/src/analyses/dirty.h +++ b/src/analyses/dirty.h @@ -24,6 +24,12 @@ public: build(goto_function); } + explicit dirtyt(const goto_functionst &goto_functions) + { + forall_goto_functions(it, goto_functions) + build(it->second); + } + void output(std::ostream &out) const; // will go away, use below diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp index 97e6fb5..19e8646 100644 --- a/src/analyses/goto_check.cpp +++ b/src/analyses/goto_check.cpp @@ -1347,7 +1347,7 @@ void goto_checkt::goto_check(goto_functiont &goto_function) { assertions.clear(); - local_may_aliast local_may_alias_obj(goto_function); + local_may_aliast local_may_alias_obj(goto_function, ns); local_may_alias=&local_may_alias_obj; goto_programt &goto_program=goto_function.body; diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp new file mode 100644 index 0000000..2f8e97f --- /dev/null +++ b/src/analyses/goto_rw.cpp @@ -0,0 +1,1089 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening + +Date: April 2010 + +\*******************************************************************/ + +#include + +#include +#include +#include +#include +#include + +#include + +#include +#include + +#include "goto_rw.h" + +/*******************************************************************\ + +Function: range_domain_baset::~range_domain_baset + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +range_domain_baset::~range_domain_baset() +{ +} + +/*******************************************************************\ + +Function: range_domaint::output + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void range_domaint::output( + const namespacet &ns, std::ostream &out) const +{ + out << "["; + for(const_iterator itr=begin(); + itr!=end(); + ++itr) + { + if(itr!=begin()) out << ";"; + out << itr->first << ":" << itr->second; + } + out << "]"; +} + +/*******************************************************************\ + +Function: rw_range_sett::~rw_range_sett + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +rw_range_sett::~rw_range_sett() +{ + for(rw_range_sett::objectst::iterator it=r_range_set.begin(); + it!=r_range_set.end(); + ++it) + delete it->second; + + for(rw_range_sett::objectst::iterator it=w_range_set.begin(); + it!=w_range_set.end(); + ++it) + delete it->second; +} + +/*******************************************************************\ + +Function: rw_range_sett::output + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_sett::output(std::ostream &out) const +{ + out << "READ:" << std::endl; + forall_rw_range_set_r_objects(it, *this) + { + out << " " << it->first; + it->second->output(ns, out); + out << std::endl; + } + + out << std::endl; + + out << "WRITE:" << std::endl; + forall_rw_range_set_w_objects(it, *this) + { + out << " " << it->first; + it->second->output(ns, out); + out << std::endl; + } +} + +/*******************************************************************\ + +Function: rw_range_sett::get_objects_complex + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_sett::get_objects_complex( + get_modet mode, + const exprt &expr, + const mp_integer &range_start, + const mp_integer &size) +{ + const exprt &op=expr.op0(); + assert(op.type().id()==ID_complex); + + mp_integer sub_size=pointer_offset_size(ns, op.type().subtype()); + mp_integer offset= + (range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size; + + get_objects_rec(mode, op, range_start+offset, size); +} + +/*******************************************************************\ + +Function: rw_range_sett::get_objects_if + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_sett::get_objects_if( + get_modet mode, + const if_exprt &if_expr, + const mp_integer &range_start, + const mp_integer &size) +{ + if(if_expr.cond().is_false()) + get_objects_rec(mode, if_expr.false_case(), range_start, size); + else if(if_expr.cond().is_true()) + get_objects_rec(mode, if_expr.true_case(), range_start, size); + else + { + get_objects_rec(READ, if_expr.cond()); + + get_objects_rec(mode, if_expr.false_case(), range_start, size); + get_objects_rec(mode, if_expr.true_case(), range_start, size); + } +} + +/*******************************************************************\ + +Function: rw_range_sett::get_objects_dereference + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_sett::get_objects_dereference( + get_modet mode, + const dereference_exprt &deref, + const mp_integer &range_start, + const mp_integer &size) +{ + const exprt &pointer=deref.pointer(); + get_objects_rec(READ, pointer); +} + +/*******************************************************************\ + +Function: rw_range_sett::get_objects_byte_extract + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_sett::get_objects_byte_extract( + get_modet mode, + const byte_extract_exprt &be, + const mp_integer &range_start, + const mp_integer &size) +{ + mp_integer index; + if(range_start==-1 || to_integer(be.offset(), index)) + get_objects_rec(mode, be.op(), -1, size); + else + { + endianness_mapt map( + be.op().type(), + be.id()==ID_byte_extract_little_endian, + ns); + assert(index::max()); + mp_integer offset=range_start + map.map_byte(integer2long(index)); + get_objects_rec(mode, be.op(), offset, size); + } +} + +/*******************************************************************\ + +Function: rw_range_sett::get_objects_shift + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_sett::get_objects_shift( + get_modet mode, + const shift_exprt &shift, + const mp_integer &range_start, + const mp_integer &size) +{ + mp_integer src_size=pointer_offset_size(ns, shift.op().type()); + + mp_integer dist; + if(range_start==-1 || + size==-1 || + src_size==-1 || + to_integer(shift.distance(), dist)) + { + get_objects_rec(mode, shift.op(), -1, -1); + get_objects_rec(mode, shift.distance(), -1, -1); + } + else + { + dist/=8; + + // not sure whether to worry about + // config.ansi_c.endianness==configt::ansi_ct::IS_LITTLE_ENDIAN + // right here maybe? + + if(shift.id()==ID_ashr || shift.id()==ID_lshr) + { + mp_integer sh_range_start=range_start; + sh_range_start+=dist; + + mp_integer sh_size=std::min(size, src_size-sh_range_start); + + if(sh_range_start>=0 && sh_range_start=0); + mp_integer sh_size=std::min(size, src_size-dist); + + get_objects_rec(mode, shift.op(), range_start, sh_size); + } + } +} + +/*******************************************************************\ + +Function: rw_range_sett::get_objects_member + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_sett::get_objects_member( + get_modet mode, + const member_exprt &expr, + const mp_integer &range_start, + const mp_integer &size) +{ + const typet &type=ns.follow(expr.struct_op().type()); + + if(type.id()==ID_union || + range_start==-1) + { + get_objects_rec(mode, expr.struct_op(), range_start, size); + return; + } + + const struct_typet &struct_type=to_struct_type(type); + const struct_typet::componentt &comp= + struct_type.get_component(expr.get_component_name()); + + mp_integer offset= + member_offset( + ns, + struct_type, + expr.get_component_name()); + + if(offset==-1 || + comp.get_is_bit_field()) + get_objects_rec(mode, expr.struct_op(), -1, size); + else + { + offset+=range_start; + get_objects_rec(mode, expr.struct_op(), offset, size); + } +} + +/*******************************************************************\ + +Function: rw_range_sett::get_objects_index + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_sett::get_objects_index( + get_modet mode, + const index_exprt &expr, + const mp_integer &range_start, + const mp_integer &size) +{ + const array_typet &array_type= + to_array_type(ns.follow(expr.array().type())); + + mp_integer sub_size= + pointer_offset_size(ns, array_type.subtype()); + + mp_integer index; + if(to_integer(expr.index(), index)) + { + get_objects_rec(READ, expr.index()); + index=-1; + } + + if(range_start==-1 || + sub_size==-1 || + index==-1) + get_objects_rec(mode, expr.array(), -1, size); + else + get_objects_rec( + mode, + expr.array(), + range_start+(index*sub_size), + size); +} + +/*******************************************************************\ + +Function: rw_range_sett::get_objects_array + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_sett::get_objects_array( + get_modet mode, + const array_exprt &expr, + const mp_integer &range_start, + const mp_integer &size) +{ + const array_typet &array_type= + to_array_type(ns.follow(expr.type())); + + mp_integer sub_size= + pointer_offset_size(ns, array_type.subtype()); + + if(sub_size==-1) + { + forall_operands(it, expr) + get_objects_rec(mode, *it, 0, -1); + + return; + } + + mp_integer offset=0; + mp_integer full_r_s=range_start==-1 ? 0 : range_start; + mp_integer full_r_e= + size==-1 ? sub_size*expr.operands().size() : full_r_s+size; + + forall_operands(it, expr) + { + if(full_r_s<=offset+sub_size && full_r_e>offset) + { + mp_integer cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset; + mp_integer cur_r_e= + full_r_e>offset+sub_size ? sub_size : full_r_e-offset; + + get_objects_rec(mode, *it, cur_r_s, cur_r_e-cur_r_s); + } + + offset+=sub_size; + } +} + +/*******************************************************************\ + +Function: rw_range_sett::get_objects_struct + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_sett::get_objects_struct( + get_modet mode, + const struct_exprt &expr, + const mp_integer &range_start, + const mp_integer &size) +{ + const struct_typet &struct_type= + to_struct_type(ns.follow(expr.type())); + + mp_integer full_size=pointer_offset_size(ns, struct_type); + + mp_integer offset=0; + mp_integer full_r_s=range_start==-1 ? 0 : range_start; + mp_integer full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size; + + forall_operands(it, expr) + { + mp_integer sub_size=pointer_offset_size(ns, it->type()); + + if(offset==-1) + { + get_objects_rec(mode, *it, 0, sub_size); + } + else if(sub_size==-1) + { + if(full_r_e==-1 || full_r_e>offset) + { + mp_integer cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset; + + get_objects_rec(mode, *it, cur_r_s, -1); + } + + offset=-1; + } + else if(full_r_e==-1) + { + if(full_r_s<=offset+sub_size) + { + mp_integer cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset; + + get_objects_rec(mode, *it, cur_r_s, sub_size-cur_r_s); + } + + offset+=sub_size; + } + else if(full_r_s<=offset+sub_size && full_r_e>offset) + { + mp_integer cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset; + mp_integer cur_r_e= + full_r_e>offset+sub_size ? sub_size : full_r_e-offset; + + get_objects_rec(mode, *it, cur_r_s, cur_r_e-cur_r_s); + + offset+=sub_size; + } + } +} + +/*******************************************************************\ + +Function: rw_range_sett::get_objects_typecast + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_sett::get_objects_typecast( + get_modet mode, + const typecast_exprt &tc, + const mp_integer &range_start, + const mp_integer &size) +{ + const exprt& op=tc.op(); + + mp_integer new_size=pointer_offset_size(ns, op.type()); + if(range_start==-1) + new_size=-1; + else if(new_size!=-1) + { + if(new_size(identifier, 0)).first; + + if(entry->second==0) + entry->second=new range_domaint(); + + static_cast(entry->second)->insert( + std::make_pair(range_start, range_end)); +} + +/*******************************************************************\ + +Function: rw_range_sett::get_objects_rec + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_sett::get_objects_rec( + get_modet mode, + const exprt &expr, + const mp_integer &range_start, + const mp_integer &size) +{ + if(expr.id()==ID_complex_real || + expr.id()==ID_complex_imag) + get_objects_complex(mode, expr, range_start, size); + else if(expr.id()==ID_typecast) + get_objects_typecast( + mode, + to_typecast_expr(expr), + range_start, + size); + else if(expr.id()==ID_if) + get_objects_if(mode, to_if_expr(expr), range_start, size); + else if(expr.id()==ID_dereference) + get_objects_dereference( + mode, + to_dereference_expr(expr), + range_start, + size); + else if(expr.id()==ID_byte_extract_little_endian || + expr.id()==ID_byte_extract_big_endian) + get_objects_byte_extract( + mode, + to_byte_extract_expr(expr), + range_start, + size); + else if(expr.id()==ID_shl || + expr.id()==ID_ashr || + expr.id()==ID_lshr) + get_objects_shift(mode, to_shift_expr(expr), range_start, size); + else if(expr.id()==ID_member) + get_objects_member(mode, to_member_expr(expr), range_start, size); + else if(expr.id()==ID_index) + get_objects_index(mode, to_index_expr(expr), range_start, size); + else if(expr.id()==ID_array) + get_objects_array(mode, to_array_expr(expr), range_start, size); + else if(expr.id()==ID_struct) + get_objects_struct(mode, to_struct_expr(expr), range_start, size); + else if(expr.id()==ID_symbol) + { + const symbol_exprt &symbol=to_symbol_expr(expr); + const irep_idt identifier=symbol.get_identifier(); + mp_integer full_size=pointer_offset_size(ns, symbol.type()); + + if(full_size==0) + { + // nothing to do, these are effectively constants (like function + // symbols or structs with no members) + } + else if(range_start>=0) + { + mp_integer range_end=size==-1 ? -1 : range_start+size; + assert(full_size==-1 || range_end<=full_size); + + add(mode, identifier, range_start, range_end); + } + else + add(mode, identifier, 0, full_size); + } + else if(mode==READ && expr.id()==ID_address_of) + get_objects_address_of(to_address_of_expr(expr).object()); + else if(mode==READ) + { + // possibly affects the full object size, even if range_start/size + // are only a subset of the bytes (e.g., when using the result of + // arithmetic operations) + forall_operands(it, expr) + get_objects_rec(mode, *it); + } + else + throw "rw_range_sett: assignment to `"+expr.id_string()+"' not handled"; +} + +/*******************************************************************\ + +Function: rw_range_sett::get_objects_rec + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_sett::get_objects_rec(get_modet mode, const exprt &expr) +{ + mp_integer size=pointer_offset_size(ns, expr.type()); + get_objects_rec(mode, expr, 0, size); +} + +/*******************************************************************\ + +Function: rw_range_set_dereft::get_objects_dereference + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_set_dereft::get_objects_dereference( + get_modet mode, + const dereference_exprt &deref, + const mp_integer &range_start, + const mp_integer &size) +{ + rw_range_sett::get_objects_dereference( + mode, + deref, + range_start, + size); + + const exprt &pointer=deref.pointer(); + std::set alias_set=may_alias.get(target, pointer); + + for(std::set::const_iterator it=alias_set.begin(); + it!=alias_set.end(); + it++) + if(it->id()!=ID_unknown && + it->id()!=ID_dynamic_object && + it->id()!=ID_null_object && + it->id()!=ID_integer_address_object) + { + mp_integer new_size=pointer_offset_size(ns, it->type()); + if(range_start==-1 || new_size<=range_start) + new_size=-1; + else + { + new_size-=range_start; + new_size=std::min(size, new_size); + } + + get_objects_rec(mode, *it, range_start, new_size); + } +} + +/*******************************************************************\ + +Function: rw_range_set_value_sett::get_objects_dereference + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_range_set_value_sett::get_objects_dereference( + get_modet mode, + const dereference_exprt &deref, + const mp_integer &range_start, + const mp_integer &size) +{ + rw_range_sett::get_objects_dereference( + mode, + deref, + range_start, + size); + + exprt tmp=deref; + dereference(target, tmp, ns, value_sets); + + get_objects_rec(mode, tmp); +} + +/*******************************************************************\ + +Function: guarded_range_domaint::output + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void guarded_range_domaint::output( + const namespacet &ns, std::ostream &out) const +{ + out << "["; + for(const_iterator itr=begin(); + itr!=end(); + ++itr) + { + if(itr!=begin()) out << ";"; + out << itr->first << ":" << itr->second.first; + out << " if " << from_expr(ns, "", itr->second.second); + } + out << "]"; +} + +/*******************************************************************\ + +Function: rw_guarded_range_set_value_sett::get_objects_if + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_guarded_range_set_value_sett::get_objects_if( + get_modet mode, + const if_exprt &if_expr, + const mp_integer &range_start, + const mp_integer &size) +{ + if(if_expr.cond().is_false()) + get_objects_rec(mode, if_expr.false_case(), range_start, size); + else if(if_expr.cond().is_true()) + get_objects_rec(mode, if_expr.true_case(), range_start, size); + else + { + get_objects_rec(READ, if_expr.cond()); + + guardt guard_bak1(guard), guard_bak2(guard); + + guard.add(not_exprt(if_expr.cond())); + get_objects_rec(mode, if_expr.false_case(), range_start, size); + guard.swap(guard_bak1); + + guard.add(if_expr.cond()); + get_objects_rec(mode, if_expr.true_case(), range_start, size); + guard.swap(guard_bak2); + } +} + +/*******************************************************************\ + +Function: rw_guarded_range_set_value_sett::add + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void rw_guarded_range_set_value_sett::add( + get_modet mode, + const irep_idt &identifier, + const mp_integer &range_start, + const mp_integer &range_end) +{ + objectst::iterator entry=(mode==LHS_W ? w_range_set : r_range_set). + insert(std::make_pair(identifier, 0)).first; + + if(entry->second==0) + entry->second=new guarded_range_domaint(); + + static_cast(entry->second)->insert( + std::make_pair(range_start, + std::make_pair(range_end, guard.as_expr()))); +} + +/*******************************************************************\ + +Function: goto_rw + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_rw(goto_programt::const_targett target, + const code_assignt &assign, + rw_range_sett &rw_set) +{ + rw_set.get_objects_rec(target, rw_range_sett::LHS_W, assign.lhs()); + rw_set.get_objects_rec(target, rw_range_sett::READ, assign.rhs()); +} + +/*******************************************************************\ + +Function: goto_rw + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_rw(goto_programt::const_targett target, + const code_function_callt &function_call, + rw_range_sett &rw_set) +{ + if(function_call.lhs().is_not_nil()) + rw_set.get_objects_rec( + target, + rw_range_sett::LHS_W, + function_call.lhs()); + + rw_set.get_objects_rec( + target, + rw_range_sett::READ, + function_call.function()); + + forall_expr(it, function_call.arguments()) + rw_set.get_objects_rec(target, rw_range_sett::READ, *it); +} + +/*******************************************************************\ + +Function: goto_rw + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_rw(goto_programt::const_targett target, + rw_range_sett &rw_set) +{ + switch(target->type) + { + case NO_INSTRUCTION_TYPE: + assert(false); + break; + + case GOTO: + case ASSUME: + case ASSERT: + rw_set.get_objects_rec( + target, + rw_range_sett::READ, + target->guard); + break; + + case RETURN: + { + const code_returnt &code_return= + to_code_return(target->code); + if(code_return.has_return_value()) + rw_set.get_objects_rec( + target, + rw_range_sett::READ, + code_return.return_value()); + } + break; + + case OTHER: + // don't know + break; + + case SKIP: + case START_THREAD: + case END_THREAD: + case LOCATION: + case END_FUNCTION: + case ATOMIC_BEGIN: + case ATOMIC_END: + case THROW: + case CATCH: + // these don't read or write anything + break; + + case ASSIGN: + goto_rw(target, to_code_assign(target->code), rw_set); + break; + + case DEAD: + rw_set.get_objects_rec( + target, + rw_range_sett::LHS_W, + to_code_dead(target->code).symbol()); + break; + + case DECL: + rw_set.get_objects_rec( + target, + rw_range_sett::LHS_W, + to_code_decl(target->code).symbol()); + break; + + case FUNCTION_CALL: + goto_rw(target, to_code_function_call(target->code), rw_set); + break; + } +} + +/*******************************************************************\ + +Function: goto_rw + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_rw(const goto_programt::goto_programt &goto_program, + rw_range_sett &rw_set) +{ + forall_goto_program_instructions(i_it, goto_program) + goto_rw(i_it, rw_set); +} + +/*******************************************************************\ + +Function: goto_rw + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void goto_rw(const goto_functionst &goto_functions, + const irep_idt &function, + rw_range_sett &rw_set) +{ + goto_functionst::function_mapt::const_iterator f_it= + goto_functions.function_map.find(function); + + if(f_it!=goto_functions.function_map.end()) + { + const goto_programt &body=f_it->second.body; + + goto_rw(body, rw_set); + } +} + diff --git a/src/analyses/goto_rw.h b/src/analyses/goto_rw.h new file mode 100644 index 0000000..5ba01ae --- /dev/null +++ b/src/analyses/goto_rw.h @@ -0,0 +1,333 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening + +Date: April 2010 + +\*******************************************************************/ + +#ifndef CPROVER_GOTO_PROGRAMS_GOTO_RW_H +#define CPROVER_GOTO_PROGRAMS_GOTO_RW_H + +#include +#include + +#include + +#include + +#define forall_rw_range_set_r_objects(it, rw_set) \ + for(rw_range_sett::objectst::const_iterator it=(rw_set).get_r_set().begin(); \ + it!=(rw_set).get_r_set().end(); ++it) + +#define forall_rw_range_set_w_objects(it, rw_set) \ + for(rw_range_sett::objectst::const_iterator it=(rw_set).get_w_set().begin(); \ + it!=(rw_set).get_w_set().end(); ++it) + +class rw_range_sett; +class goto_functionst; + +void goto_rw(goto_programt::const_targett target, + rw_range_sett &rw_set); + +void goto_rw(const goto_programt::goto_programt &goto_program, + rw_range_sett &rw_set); + +void goto_rw(const goto_functionst &goto_functions, + const irep_idt &function, + rw_range_sett &rw_set); + +class range_domain_baset +{ +public: + virtual ~range_domain_baset(); + + virtual void output(const namespacet &ns, std::ostream &out) const=0; +}; + +// each element x represents a range [x.first, x.second.first) +class range_domaint: + public range_domain_baset, + public std::multimap +{ +public: + virtual void output(const namespacet &ns, std::ostream &out) const; +}; + +class array_exprt; +class byte_extract_exprt; +class dereference_exprt; +class if_exprt; +class index_exprt; +class member_exprt; +class shift_exprt; +class struct_exprt; +class typecast_exprt; + +class rw_range_sett +{ +public: + #ifdef USE_DSTRING + typedef std::map objectst; + #else + typedef hash_map_cont objectst; + #endif + + virtual ~rw_range_sett(); + + explicit rw_range_sett(const namespacet &_ns): + ns(_ns) + { + } + + const objectst & get_r_set() const + { + return r_range_set; + } + + const objectst & get_w_set() const + { + return w_range_set; + } + + const range_domaint& get_ranges(objectst::const_iterator it) const + { + assert(dynamic_cast(it->second)!=0); + return *static_cast(it->second); + } + + typedef enum { LHS_W, READ } get_modet; + + virtual void get_objects_rec( + goto_programt::const_targett _target, + get_modet mode, + const exprt &expr) + { + get_objects_rec(mode, expr); + } + + void output(std::ostream &out) const; + +protected: + const namespacet &ns; + + objectst r_range_set, w_range_set; + + virtual void get_objects_rec( + get_modet mode, + const exprt &expr); + + virtual void get_objects_complex( + get_modet mode, + const exprt &expr, + const mp_integer &range_start, + const mp_integer &size); + + virtual void get_objects_if( + get_modet mode, + const if_exprt &if_expr, + const mp_integer &range_start, + const mp_integer &size); + + // overload to include expressions read/written + // through dereferencing + virtual void get_objects_dereference( + get_modet mode, + const dereference_exprt &deref, + const mp_integer &range_start, + const mp_integer &size); + + virtual void get_objects_byte_extract( + get_modet mode, + const byte_extract_exprt &be, + const mp_integer &range_start, + const mp_integer &size); + + virtual void get_objects_shift( + get_modet mode, + const shift_exprt &shift, + const mp_integer &range_start, + const mp_integer &size); + + virtual void get_objects_member( + get_modet mode, + const member_exprt &expr, + const mp_integer &range_start, + const mp_integer &size); + + virtual void get_objects_index( + get_modet mode, + const index_exprt &expr, + const mp_integer &range_start, + const mp_integer &size); + + virtual void get_objects_array( + get_modet mode, + const array_exprt &expr, + const mp_integer &range_start, + const mp_integer &size); + + virtual void get_objects_struct( + get_modet mode, + const struct_exprt &expr, + const mp_integer &range_start, + const mp_integer &size); + + virtual void get_objects_typecast( + get_modet mode, + const typecast_exprt &tc, + const mp_integer &range_start, + const mp_integer &size); + + virtual void get_objects_address_of(const exprt &object); + + virtual void get_objects_rec( + get_modet mode, + const exprt &expr, + const mp_integer &range_start, + const mp_integer &size); + + virtual void add( + get_modet mode, + const irep_idt &identifier, + const mp_integer &range_start, + const mp_integer &range_end); +}; + +inline std::ostream & operator << ( + std::ostream &out, + const rw_range_sett &rw_set) +{ + rw_set.output(out); + return out; +} + +class may_aliast; + +class rw_range_set_dereft:public rw_range_sett +{ +public: + rw_range_set_dereft( + const namespacet &_ns, + may_aliast &_may_alias): + rw_range_sett(_ns), + may_alias(_may_alias) + { + } + + using rw_range_sett::get_objects_rec; + + virtual void get_objects_rec( + goto_programt::const_targett _target, + get_modet mode, + const exprt &expr) + { + target=_target; + + rw_range_sett::get_objects_rec(mode, expr); + } + +protected: + may_aliast &may_alias; + + goto_programt::const_targett target; + + virtual void get_objects_dereference( + get_modet mode, + const dereference_exprt &deref, + const mp_integer &range_start, + const mp_integer &size); +}; + +class value_setst; + +class rw_range_set_value_sett:public rw_range_sett +{ +public: + rw_range_set_value_sett( + const namespacet &_ns, + value_setst &_value_sets): + rw_range_sett(_ns), + value_sets(_value_sets) + { + } + + using rw_range_sett::get_objects_rec; + + virtual void get_objects_rec( + goto_programt::const_targett _target, + get_modet mode, + const exprt &expr) + { + target=_target; + + rw_range_sett::get_objects_rec(mode, expr); + } + +protected: + value_setst &value_sets; + + goto_programt::const_targett target; + + virtual void get_objects_dereference( + get_modet mode, + const dereference_exprt &deref, + const mp_integer &range_start, + const mp_integer &size); +}; + +class guarded_range_domaint: + public range_domain_baset, + public std::multimap > +{ +public: + virtual void output(const namespacet &ns, std::ostream &out) const; +}; + +class rw_guarded_range_set_value_sett:public rw_range_set_value_sett +{ +public: + rw_guarded_range_set_value_sett( + const namespacet &_ns, + value_setst &_value_sets): + rw_range_set_value_sett(_ns, _value_sets) + { + } + + const guarded_range_domaint& get_ranges(objectst::const_iterator it) const + { + assert(dynamic_cast(it->second)!=0); + return *static_cast(it->second); + } + + virtual void get_objects_rec( + goto_programt::const_targett _target, + get_modet mode, + const exprt &expr) + { + guard.make_true(); + + rw_range_set_value_sett::get_objects_rec(_target, mode, expr); + } + +protected: + guardt guard; + + using rw_range_sett::get_objects_rec; + + virtual void get_objects_if( + get_modet mode, + const if_exprt &if_expr, + const mp_integer &range_start, + const mp_integer &size); + + virtual void add( + get_modet mode, + const irep_idt &identifier, + const mp_integer &range_start, + const mp_integer &range_end); +}; + +#endif diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp index 877642e..ea4a09d 100644 --- a/src/analyses/interval_domain.cpp +++ b/src/analyses/interval_domain.cpp @@ -72,8 +72,8 @@ Function: interval_domaint::transform void interval_domaint::transform( const namespacet &ns, - locationt from, - locationt to) + goto_programt::const_targett from, + goto_programt::const_targett to) { const goto_programt::instructiont &instruction=*from; switch(instruction.type) @@ -92,7 +92,7 @@ void interval_domaint::transform( case GOTO: { - locationt next=from; + goto_programt::const_targett next=from; next++; if(next==to) assume_rec(not_exprt(instruction.guard)); @@ -130,7 +130,9 @@ Function: interval_domaint::merge \*******************************************************************/ -bool interval_domaint::merge(const interval_domaint &b, locationt to) +bool interval_domaint::merge( + const interval_domaint &b, + goto_programt::const_targett to) { if(!b.seen) return false; if(!seen) { *this=b; return true; } diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h index aed6715..6e5934d 100644 --- a/src/analyses/interval_domain.h +++ b/src/analyses/interval_domain.h @@ -30,14 +30,16 @@ public: virtual void transform( const namespacet &ns, - locationt from, - locationt to); + goto_programt::const_targett from, + goto_programt::const_targett to); virtual void output( const namespacet &ns, std::ostream &out) const; - bool merge(const interval_domaint &b, locationt to); + bool merge( + const interval_domaint &b, + goto_programt::const_targett to); exprt make_expression(const symbol_exprt &) const; diff --git a/src/analyses/invariant_propagation.h b/src/analyses/invariant_propagation.h index eac5455..e318bd5 100644 --- a/src/analyses/invariant_propagation.h +++ b/src/analyses/invariant_propagation.h @@ -27,7 +27,7 @@ public: { } - const invariant_sett &lookup(locationt l) const + const invariant_sett &lookup(goto_programt::const_targett l) const { return (*this)[l].invariant_set; } diff --git a/src/analyses/invariant_set_domain.cpp b/src/analyses/invariant_set_domain.cpp index 56659e8..d3b1091 100644 --- a/src/analyses/invariant_set_domain.cpp +++ b/src/analyses/invariant_set_domain.cpp @@ -24,8 +24,8 @@ Function: invariant_set_domaint::transform void invariant_set_domaint::transform( const namespacet &ns, - locationt from_l, - locationt to_l) + goto_programt::const_targett from_l, + goto_programt::const_targett to_l) { switch(from_l->type) { diff --git a/src/analyses/invariant_set_domain.h b/src/analyses/invariant_set_domain.h index 06e2f19..1f402d0 100644 --- a/src/analyses/invariant_set_domain.h +++ b/src/analyses/invariant_set_domain.h @@ -19,7 +19,9 @@ public: // overloading - inline bool merge(const invariant_set_domaint &other, locationt to) + inline bool merge( + const invariant_set_domaint &other, + goto_programt::const_targett to) { return invariant_set.make_union(other.invariant_set); } @@ -33,15 +35,15 @@ public: virtual void initialize( const namespacet &ns, - locationt l) + goto_programt::const_targett l) { invariant_set.make_true(); } virtual void transform( const namespacet &ns, - locationt from_l, - locationt to_l); + goto_programt::const_targett from_l, + goto_programt::const_targett to_l); }; #endif diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp index 99e7d8d..4847373 100644 --- a/src/analyses/is_threaded.cpp +++ b/src/analyses/is_threaded.cpp @@ -20,7 +20,9 @@ public: { } - inline bool merge(const is_threaded_domaint &other, locationt to) + inline bool merge( + const is_threaded_domaint &other, + goto_programt::const_targett to) { bool old=is_threaded; is_threaded=is_threaded || other.is_threaded; @@ -29,8 +31,8 @@ public: void transform( const namespacet &ns, - locationt from, - locationt to) + goto_programt::const_targett from, + goto_programt::const_targett to) { if(from->is_start_thread()) is_threaded=true; @@ -59,18 +61,9 @@ void is_threadedt::compute(const goto_functionst &goto_functions) is_threaded_analysis(goto_functions); - for(goto_functionst::function_mapt::const_iterator - f_it=goto_functions.function_map.begin(); - f_it!=goto_functions.function_map.end(); - f_it++) - { - const goto_programt &goto_program=f_it->second.body; - for(goto_programt::instructionst::const_iterator - i_it=goto_program.instructions.begin(); - i_it!=goto_program.instructions.end(); - i_it++) + forall_goto_functions(f_it, goto_functions) + forall_goto_program_instructions(i_it, f_it->second.body) if(is_threaded_analysis[i_it].is_threaded) is_threaded_set.insert(i_it); - } } diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp index 9ca6bab..2562169 100644 --- a/src/analyses/local_may_alias.cpp +++ b/src/analyses/local_may_alias.cpp @@ -20,7 +20,7 @@ Author: Daniel Kroening, kroening@kroening.com /*******************************************************************\ -Function: cfgt::build +Function: local_may_aliast::~local_may_aliast Inputs: @@ -30,69 +30,8 @@ Function: cfgt::build \*******************************************************************/ -void local_cfgt::build(const goto_programt &goto_program) +local_may_aliast::~local_may_aliast() { - locs.resize(goto_program.instructions.size()); - - { - unsigned loc_nr=0; - - for(goto_programt::const_targett it=goto_program.instructions.begin(); - it!=goto_program.instructions.end(); - it++, loc_nr++) - { - loc_map[it]=loc_nr; - locs[loc_nr].t=it; - } - } - - for(unsigned loc_nr=0; loc_nrsecond; - loc.successors.push_back(l); - } - break; - - case START_THREAD: - loc.successors.push_back(loc_nr+1); - - for(goto_programt::targetst::const_iterator - t_it=instruction.targets.begin(); - t_it!=instruction.targets.end(); - t_it++) - { - unsigned l=loc_map.find(*t_it)->second; - loc.successors.push_back(l); - } - break; - - case RETURN: - loc.successors.push_back(locs.size()-1); - break; - - case THROW: - case END_FUNCTION: - case END_THREAD: - break; // no successor - - default: - loc.successors.push_back(loc_nr+1); - } - } } /*******************************************************************\ @@ -189,7 +128,7 @@ Function: local_may_aliast::is_tracked \*******************************************************************/ -bool local_may_aliast::is_tracked(const irep_idt &identifier) +bool local_may_aliast::is_tracked(const irep_idt &identifier) const { localst::locals_mapt::const_iterator it=locals.locals_map.find(identifier); if(it==locals.locals_map.end()) return false; @@ -224,7 +163,8 @@ void local_may_aliast::assign_lhs( { unsigned dest_pointer=pointers.number(identifier); destt &dest_set=loc_info_dest.points_to[dest_pointer]; - dest_set.clear(); + if(kill_foreign || local_may_aliast::is_tracked(identifier)) + dest_set.clear(); get_rec(dest_set, rhs, loc_info_src); } } @@ -266,11 +206,7 @@ std::set local_may_aliast::get( const goto_programt::const_targett t, const exprt &rhs) { - local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t); - - assert(loc_it!=cfg.loc_map.end()); - - const loc_infot &loc_info_src=loc_infos[loc_it->second]; + const loc_infot &loc_info_src=loc_infos[t]; destt result_tmp; get_rec(result_tmp, rhs, loc_info_src); @@ -304,11 +240,7 @@ bool local_may_aliast::may_use_offset( const goto_programt::const_targett t, const exprt &rhs) { - local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t); - - assert(loc_it!=cfg.loc_map.end()); - - const loc_infot &loc_info_src=loc_infos[loc_it->second]; + const loc_infot &loc_info_src=loc_infos[t]; destt result_tmp; get_rec(result_tmp, rhs, loc_info_src); @@ -332,11 +264,7 @@ bool local_may_aliast::aliases( const goto_programt::const_targett t, const exprt &src1, const exprt &src2) { - local_cfgt::loc_mapt::const_iterator loc_it=cfg.loc_map.find(t); - - assert(loc_it!=cfg.loc_map.end()); - - const loc_infot &loc_info_src=loc_infos[loc_it->second]; + const loc_infot &loc_info_src=loc_infos[t]; destt tmp1, tmp2; get_rec(tmp1, src1, loc_info_src); @@ -503,44 +431,30 @@ Function: local_may_aliast::build void local_may_aliast::build(const goto_functiont &goto_function) { - if(cfg.locs.empty()) return; + if(cfg.entry_map.empty() || + goto_function.body.instructions.empty()) return; + goto_programt::const_targett entry=goto_function.body.instructions.begin(); work_queuet work_queue; - work_queue.push(0); + work_queue.push(entry); unknown_object=objects.number(exprt(ID_unknown)); - loc_infos.resize(cfg.locs.size()); - // feed in sufficiently bad defaults - for(code_typet::argumentst::const_iterator - it=goto_function.type.arguments().begin(); - it!=goto_function.type.arguments().end(); - it++) - { - const irep_idt &identifier=it->get_identifier(); - if(is_tracked(identifier)) - loc_infos[0].points_to[pointers.number(identifier)].objects.insert(unknown_object); - } - - for(localst::locals_mapt::const_iterator - l_it=locals.locals_map.begin(); - l_it!=locals.locals_map.end(); - l_it++) - { - if(is_tracked(l_it->first)) - loc_infos[0].points_to[pointers.number(l_it->first)].objects.insert(unknown_object); - } + loc_infot &loc_info=loc_infos[entry]; + forall_symbols(it, ns.get_symbol_table().symbols) + if(is_tracked(it->second.name)) + loc_info.points_to[pointers.number(it->second.name)].objects.insert(unknown_object); while(!work_queue.empty()) { - unsigned loc_nr=work_queue.top(); - const local_cfgt::loct &loc=cfg.locs[loc_nr]; - const goto_programt::instructiont &instruction=*loc.t; + goto_programt::const_targett t=work_queue.top(); + const local_cfgt::nodet &loc=cfg[cfg.entry_map[t]]; + const goto_programt::instructiont &instruction=*t; work_queue.pop(); - const loc_infot &loc_info_src=loc_infos[loc_nr]; - loc_infot loc_info_dest=loc_infos[loc_nr]; + const loc_infot &loc_info_src=loc_infos[t]; + loc_infot loc_info_dest=loc_infos[t]; switch(instruction.type) { @@ -576,13 +490,13 @@ void local_may_aliast::build(const goto_functiont &goto_function) default:; } - for(local_cfgt::successorst::const_iterator - it=loc.successors.begin(); - it!=loc.successors.end(); + for(local_cfgt::edgest::const_iterator + it=loc.out.begin(); + it!=loc.out.end(); it++) { - if(loc_infos[*it].merge(loc_info_dest)) - work_queue.push(*it); + if(loc_infos[cfg[it->first].PC].merge(loc_info_dest)) + work_queue.push(cfg[it->first].PC); } } } @@ -601,16 +515,15 @@ Function: local_may_aliast::output void local_may_aliast::output( std::ostream &out, - const goto_functiont &goto_function, - const namespacet &ns) const + const goto_functiont &goto_function) const { - unsigned l=0; - forall_goto_program_instructions(i_it, goto_function.body) { out << "**** " << i_it->location << "\n"; - const loc_infot &loc_info=loc_infos[l]; + loc_infost::const_iterator entry=loc_infos.find(i_it); + assert(entry!=loc_infos.end()); + const loc_infot &loc_info=entry->second; for(points_tot::const_iterator p_it=loc_info.points_to.begin(); @@ -639,8 +552,6 @@ void local_may_aliast::output( out << "\n"; goto_function.body.output_instruction(ns, "", out, i_it); out << "\n"; - - l++; } } diff --git a/src/analyses/local_may_alias.h b/src/analyses/local_may_alias.h index 62a3c1f..bc808fe 100644 --- a/src/analyses/local_may_alias.h +++ b/src/analyses/local_may_alias.h @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include #include "dirty.h" #include "locals.h" @@ -27,55 +28,36 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -class local_cfgt -{ -public: - typedef std::vector successorst; - - class loct - { - public: - goto_programt::const_targett t; - successorst successors; - }; - - typedef std::map loc_mapt; - loc_mapt loc_map; - - typedef std::vector locst; - locst locs; - - inline explicit local_cfgt(const goto_programt &_goto_program) - { - build(_goto_program); - } - -protected: - void build(const goto_programt &goto_program); -}; - class local_may_aliast { public: typedef goto_functionst::goto_functiont goto_functiont; + + virtual ~local_may_aliast(); - explicit local_may_aliast( - const goto_functiont &_goto_function): + local_may_aliast( + const goto_functiont &_goto_function, + const namespacet &_ns): dirty(_goto_function), locals(_goto_function), - cfg(_goto_function.body) + ns(_ns), + kill_foreign(true) { + cfg(_goto_function.body); build(_goto_function); } void output( std::ostream &out, - const goto_functiont &goto_function, - const namespacet &ns) const; + const goto_functiont &goto_function) const; + + typedef procedure_local_concurrent_cfg_baset local_cfgt; dirtyt dirty; localst locals; local_cfgt cfg; + const namespacet &ns; + const bool kill_foreign; std::set get( const goto_programt::const_targett t, @@ -90,9 +72,21 @@ public: const exprt &src); protected: + local_may_aliast( + const goto_functiont &_goto_function, + const namespacet &_ns, + bool _kill_foreign): + dirty(_goto_function), + locals(_goto_function), + ns(_ns), + kill_foreign(_kill_foreign) + { + cfg(_goto_function.body); + } + void build(const goto_functiont &goto_function); - typedef std::stack work_queuet; + typedef std::stack work_queuet; // the following may eventually get merged numbering pointers; @@ -124,7 +118,7 @@ protected: bool merge(const loc_infot &src); }; - typedef std::vector loc_infost; + typedef std::map loc_infost; loc_infost loc_infos; void assign_lhs( @@ -138,7 +132,7 @@ protected: const exprt &rhs, const loc_infot &loc_info_src); - bool is_tracked(const irep_idt &identifier); + virtual bool is_tracked(const irep_idt &identifier) const; unsigned unknown_object; std::set empty_set; diff --git a/src/analyses/may_alias.cpp b/src/analyses/may_alias.cpp new file mode 100644 index 0000000..455e22c --- /dev/null +++ b/src/analyses/may_alias.cpp @@ -0,0 +1,128 @@ +/*******************************************************************\ + +Module: Field-insensitive, location-sensitive may-alias analysis + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include + +#include "may_alias.h" + +/*******************************************************************\ + +Function: may_aliast::may_aliast + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +may_aliast::may_aliast( + const goto_functionst &goto_functions, + const namespacet &ns): + local_may_aliast(goto_functionst::goto_functiont(), ns, false) +{ + assert(!goto_functions.function_map.empty()); + + dirty=dirtyt(goto_functions); + cfg(goto_functions); + + forall_goto_functions(it, goto_functions) + { + locals=localst(it->second); + + build(it->second); + } + + // make it context-insensitive for all non-local variables + // relies on the fact that local_may_aliast is flow-insensitive for + // non-local variables + points_tot merged; + for(numbering::const_iterator it=pointers.begin(); + it!=pointers.end(); + ++it) + if(!local_may_aliast::is_tracked(*it)) + merged.insert(std::make_pair(pointers.number(*it), destt())); + + // build the merged destt + forall_goto_functions(it, goto_functions) + { + goto_programt::const_targett last= + --(it->second.body.instructions.end()); + const loc_infot &loc_info=loc_infos[last]; + + for(points_tot::iterator m_it=merged.begin(); + m_it!=merged.end(); + ++m_it) + { + points_tot::const_iterator entry= + loc_info.points_to.find(m_it->first); + if(entry!=loc_info.points_to.end()) + m_it->second.merge(entry->second); + } + } + + // update points_to at all locations + forall_goto_functions(it, goto_functions) + forall_goto_program_instructions(l_it, it->second.body) + { + loc_infot &loc_info=loc_infos[l_it]; + + for(points_tot::iterator m_it=merged.begin(); + m_it!=merged.end(); + ++m_it) + loc_info.points_to[m_it->first]=m_it->second; + } +} + +/*******************************************************************\ + +Function: may_aliast::is_tracked + + Inputs: + + Outputs: return 'true' iff we track the object with given + identifier + + Purpose: + +\*******************************************************************/ + +bool may_aliast::is_tracked(const irep_idt &identifier) const +{ + if(ns.lookup(identifier).type.id()!=ID_pointer) return false; + if(dirty.is_dirty(identifier)) return false; + return true; +} + +/*******************************************************************\ + +Function: may_aliast::output + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void may_aliast::output( + std::ostream &out, + const goto_functionst &goto_functions) const +{ + forall_goto_functions(it, goto_functions) + { + out << ">>>>" << std::endl; + out << ">>>> " << it->first << std::endl; + out << ">>>>" << std::endl; + local_may_aliast::output(out, it->second); + out << std::endl; + } +} + diff --git a/src/analyses/may_alias.h b/src/analyses/may_alias.h new file mode 100644 index 0000000..1e3f044 --- /dev/null +++ b/src/analyses/may_alias.h @@ -0,0 +1,37 @@ +/*******************************************************************\ + +Module: Field-insensitive, location-sensitive may-alias analysis + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_MAY_ALIAS_H +#define CPROVER_MAY_ALIAS_H + +#include "local_may_alias.h" + +/*******************************************************************\ + + Class: may_aliast + + Purpose: + +\*******************************************************************/ + +class may_aliast:public local_may_aliast +{ +public: + may_aliast( + const goto_functionst &goto_functions, + const namespacet &ns); + + void output( + std::ostream &out, + const goto_functionst &goto_functions) const; + +protected: + virtual bool is_tracked(const irep_idt &identifier) const; +}; + +#endif diff --git a/src/analyses/natural_loops.h b/src/analyses/natural_loops.h index 8b16717..5c5f30a 100644 --- a/src/analyses/natural_loops.h +++ b/src/analyses/natural_loops.h @@ -52,6 +52,7 @@ public: protected: cfg_dominators_templatet cfg_dominators; + typedef typename cfg_dominators_templatet::cfgt::nodet nodet; void compute(P &program); void compute_natural_loop(T, T); @@ -105,8 +106,8 @@ void natural_loops_templatet::compute(P &program) { if((*n_it)->location_number<=m_it->location_number) { - const typename cfg_dominators_templatet::nodet &node= - cfg_dominators.node_map[m_it]; + const nodet &node= + cfg_dominators.cfg[cfg_dominators.cfg.entry_map[m_it]]; #ifdef DEBUG std::cout << "Computing loop for " @@ -156,15 +157,15 @@ void natural_loops_templatet::compute_natural_loop(T m, T n) T p=stack.top(); stack.pop(); - typename cfg_dominators_templatet::nodet &node= - cfg_dominators.node_map[p]; + const nodet &node= + cfg_dominators.cfg[cfg_dominators.cfg.entry_map[p]]; - for(typename std::list::const_iterator - q_it=node.predecessors.begin(); - q_it!=node.predecessors.end(); + for(typename nodet::edgest::const_iterator + q_it=node.in.begin(); + q_it!=node.in.end(); ++q_it) { - T q=*q_it; + T q=cfg_dominators.cfg[q_it->first].PC; std::pair result= loop.insert(q); if(result.second) diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp index 66e8653..45c8365 100644 --- a/src/analyses/reaching_definitions.cpp +++ b/src/analyses/reaching_definitions.cpp @@ -9,13 +9,9 @@ Date: February 2013 \*******************************************************************/ -#include - -#include -#include -#include -#include -#include +#include "goto_rw.h" +#include "may_alias.h" +#include "is_threaded.h" #include "reaching_definitions.h" @@ -33,46 +29,26 @@ Function: rd_range_domaint::transform void rd_range_domaint::transform( const namespacet &ns, - locationt from, - locationt to) + goto_programt::const_targett from, + goto_programt::const_targett to) { - if(from->is_dead()) - { - const symbol_exprt &symbol= - to_symbol_expr(to_code_dead(from->code).symbol()); - values.erase(symbol.get_identifier()); - return; - } - else if(!from->is_assign()) - return; - - const exprt &lhs=to_code_assign(from->code).lhs(); + assert(is_threaded); - if(lhs.id()==ID_complex_real || - lhs.id()==ID_complex_imag) - { - assert(lhs.type().id()==ID_complex); - mp_integer offset=compute_pointer_offset(ns, lhs.op0()); - mp_integer sub_size=pointer_offset_size(ns, lhs.type().subtype()); - - assign( - ns, - from, - lhs.op0(), - offset+((offset==-1 || lhs.id()==ID_complex_real) ? 0 : sub_size), - sub_size); - } - else - { - mp_integer size=pointer_offset_size(ns, lhs.type()); - - assign(ns, from, lhs, size); - } + if(from->is_dead()) + transform_dead(ns, from); + else if(from->is_start_thread()) + transform_start_thread(ns); + else if(from->is_function_call()) + transform_function_call(ns, from, to); + else if(from->is_end_function()) + transform_end_function(ns, from); + else if(from->is_assign()) + transform_assign(ns, from, to_code_assign(from->code).lhs()); } /*******************************************************************\ -Function: rd_range_domaint::assign +Function: rd_range_domaint::transform_dead Inputs: @@ -82,32 +58,19 @@ Function: rd_range_domaint::assign \*******************************************************************/ -void rd_range_domaint::assign( +void rd_range_domaint::transform_dead( const namespacet &ns, - locationt from, - const exprt &lhs, - const mp_integer &size) + goto_programt::const_targett from) { - if(lhs.id()==ID_typecast) - assign(ns, from, to_typecast_expr(lhs).op(), size); - else if(lhs.id()==ID_if) - assign_if(ns, from, to_if_expr(lhs), size); - else if(lhs.id()==ID_dereference) - assign_dereference(ns, from, to_dereference_expr(lhs), size); - else if(lhs.id()==ID_byte_extract_little_endian || - lhs.id()==ID_byte_extract_big_endian) - assign_byte_extract(ns, from, to_byte_extract_expr(lhs), size); - else if(lhs.id()==ID_symbol || - lhs.id()==ID_index || - lhs.id()==ID_member) - assign(ns, from, lhs, compute_pointer_offset(ns, lhs), size); - else - throw "assignment to `"+lhs.id_string()+"' not handled"; + const irep_idt& identifier= + to_symbol_expr(to_code_dead(from->code).symbol()).get_identifier(); + + values.erase(identifier); } /*******************************************************************\ -Function: rd_range_domaint::assign_if +Function: rd_range_domaint::transform_start_thread Inputs: @@ -117,30 +80,25 @@ Function: rd_range_domaint::assign_if \*******************************************************************/ -void rd_range_domaint::assign_if( - const namespacet &ns, - locationt from, - const if_exprt &if_expr, - const mp_integer &size) +void rd_range_domaint::transform_start_thread(const namespacet &ns) { - if(if_expr.cond().is_false()) - assign(ns, from, if_expr.false_case(), size); - else if(if_expr.cond().is_true()) - assign(ns, from, if_expr.true_case(), size); - else - { - rd_range_domaint false_case(*this); - assign(ns, from, if_expr.false_case(), size); - values.swap(false_case.values); - assign(ns, from, if_expr.true_case(), size); - - merge(false_case, from); - } + for(valuest::iterator it=values.begin(); + it!=values.end(); + ) // no ++it + if(ns.lookup(it->first).is_thread_local) + { + valuest::iterator next=it; + ++next; + values.erase(it); + it=next; + } + else + ++it; } /*******************************************************************\ -Function: rd_range_domaint::assign_dereference +Function: rd_range_domaint::transform_function_call Inputs: @@ -150,44 +108,55 @@ Function: rd_range_domaint::assign_dereference \*******************************************************************/ -void rd_range_domaint::assign_dereference( +void rd_range_domaint::transform_function_call( const namespacet &ns, - locationt from, - const dereference_exprt &deref, - const mp_integer &size) + goto_programt::const_targett from, + goto_programt::const_targett to) { - assert(local_may_alias); + const code_function_callt &code=to_code_function_call(from->code); - const exprt &pointer=deref.pointer(); - std::set alias_set=local_may_alias->get(from, pointer); + goto_programt::const_targett next=from; + ++next; - valuest before(values); - for(std::set::const_iterator it=alias_set.begin(); - it!=alias_set.end(); - it++) + if(next!=to) { - if(it->id()!=ID_unknown && - it->id()!=ID_dynamic_object && - it->id()!=ID_null_object) - { - valuest bak; - bak.swap(values); + for(valuest::iterator it=values.begin(); + it!=values.end(); + ) // no ++it + if(!ns.lookup(it->first).is_static_lifetime) + { + valuest::iterator next=it; + ++next; + values.erase(it); + it=next; + } + else + ++it; - values=before; - assign(ns, from, *it, size); + const symbol_exprt& fn_symbol_expr=to_symbol_expr(code.function()); + const code_typet &code_type= + to_code_type(ns.lookup(fn_symbol_expr.get_identifier()).type); - rd_range_domaint this_object; - this_object.values.swap(values); - values.swap(bak); + const code_typet::parameterst ¶meters=code_type.parameters(); + for(code_typet::parameterst::const_iterator it=parameters.begin(); + it!=parameters.end(); + ++it) + { + if(it->get_identifier().empty()) + continue; - merge(this_object, from); + symbol_exprt parameter(it->get_identifier(), it->type()); + transform_assign(ns, from, parameter); } } + + if(code.lhs().is_not_nil()) + transform_assign(ns, from, code.lhs()); } /*******************************************************************\ -Function: rd_range_domaint::assign_byte_extract +Function: rd_range_domaint::transform_end_function Inputs: @@ -197,33 +166,24 @@ Function: rd_range_domaint::assign_byte_extract \*******************************************************************/ -void rd_range_domaint::assign_byte_extract( +void rd_range_domaint::transform_end_function( const namespacet &ns, - locationt from, - const byte_extract_exprt &be, - const mp_integer &size) + goto_programt::const_targett from) { - assert(size==1); - mp_integer op_offset=compute_pointer_offset(ns, be.op()); + const code_typet &code_type= + to_code_type(ns.lookup(from->function).type); - mp_integer index; - if(op_offset==-1 || to_integer(be.offset(), index)) - assign(ns, from, be.op(), -1, 1); - else - { - endianness_mapt map( - be.op().type(), - be.id()==ID_byte_extract_little_endian, - ns); - assert(index::max()); - op_offset+=map.map_byte(integer2long(index)); - assign(ns, from, be.op(), op_offset, 1); - } + const code_typet::parameterst ¶meters=code_type.parameters(); + for(code_typet::parameterst::const_iterator it=parameters.begin(); + it!=parameters.end(); + ++it) + if(!it->get_identifier().empty()) + values.erase(it->get_identifier()); } /*******************************************************************\ -Function: rd_range_domaint::assign +Function: rd_range_domaint::transform_assign Inputs: @@ -233,32 +193,33 @@ Function: rd_range_domaint::assign \*******************************************************************/ -void rd_range_domaint::assign( +void rd_range_domaint::transform_assign( const namespacet &ns, - locationt from, - const exprt &lhs, - const mp_integer &range_start, - const mp_integer &size) + goto_programt::const_targett from, + const exprt &lhs) { - if(lhs.id()==ID_member) - assign(ns, from, to_member_expr(lhs).struct_op(), range_start, size); - else if(lhs.id()==ID_index) - assign(ns, from, to_index_expr(lhs).array(), range_start, size); - else - { - const symbol_exprt &symbol=to_symbol_expr(lhs); - const irep_idt identifier=symbol.get_identifier(); + assert(may_alias); + rw_range_set_dereft rw_set(ns, *may_alias); + goto_rw(from, rw_set); - if(range_start>=0) - { - kill(from, identifier, range_start, size); - gen(from, identifier, range_start, size); - } - else - { - mp_integer full_size=pointer_offset_size(ns, symbol.type()); - gen(from, identifier, 0, full_size); - } + forall_rw_range_set_w_objects(it, rw_set) + { + const irep_idt &identifier=it->first; + const range_domaint &ranges=rw_set.get_ranges(it); + + if(!(*is_threaded)(from) || + !ns.lookup(identifier).is_shared()) + for(range_domaint::const_iterator + r_it=ranges.begin(); + r_it!=ranges.end(); + ++r_it) + kill(from, identifier, r_it->first, r_it->second); + + for(range_domaint::const_iterator + r_it=ranges.begin(); + r_it!=ranges.end(); + ++r_it) + gen(from, identifier, r_it->first, r_it->second); } } @@ -275,21 +236,20 @@ Function: rd_range_domaint::kill \*******************************************************************/ void rd_range_domaint::kill( - locationt from, + goto_programt::const_targett from, const irep_idt &identifier, const mp_integer &range_start, - const mp_integer &size) + const mp_integer &range_end) { assert(range_start>=0); // -1 for objects of infinite/unknown size - if(size==-1) + if(range_end==-1) { kill_inf(from, identifier, range_start); return; } - assert(size>0); - mp_integer range_end=range_start+size; + assert(range_end>range_start); valuest::iterator entry=values.find(identifier); if(entry==values.end()) @@ -317,13 +277,13 @@ void rd_range_domaint::kill( ranges.erase(it++); } else if(it->second.first==-1 || - it->second.first >= range_end) // a <= rs < re <= b + it->second.first > range_end) // a <= rs < re < b { ranges.insert(std::make_pair(range_end, it->second)); it->second.first=range_start; ++it; } - else // a <= rs < b < re + else // a <= rs < b <= re { it->second.first=range_start; ++it; @@ -343,7 +303,7 @@ Function: rd_range_domaint::kill_inf \*******************************************************************/ void rd_range_domaint::kill_inf( - locationt from, + goto_programt::const_targett from, const irep_idt &identifier, const mp_integer &range_start) { @@ -385,21 +345,23 @@ Function: rd_range_domaint::gen \*******************************************************************/ bool rd_range_domaint::gen( - locationt from, + goto_programt::const_targett from, const irep_idt &identifier, const mp_integer &range_start, - const mp_integer &size) + const mp_integer &range_end) { assert(range_start>=0); // -1 for objects of infinite/unknown size - assert(size>0 || size==-1); - mp_integer range_end=size==-1 ? -1 : range_start+size; + assert(range_end>range_start || range_end==-1); + + mp_integer merged_range_end=range_end; std::pair entry= values.insert(std::make_pair(identifier, rangest())); rangest &ranges=entry.first->second; if(!entry.second) + { for(rangest::iterator it=ranges.begin(); it!=ranges.end(); ) // no ++it @@ -411,7 +373,7 @@ bool rd_range_domaint::gen( else if(it->first > range_start) // rs < a < b,re { if(range_end!=-1) - range_end=std::max(range_end, it->second.first); + merged_range_end=std::max(range_end, it->second.first); ranges.erase(it++); } else if(it->second.first==-1 || @@ -427,10 +389,11 @@ bool rd_range_domaint::gen( return true; } } + } ranges.insert(std::make_pair( range_start, - std::make_pair(range_end, from))); + std::make_pair(merged_range_end, from))); return true; } @@ -464,6 +427,7 @@ void rd_range_domaint::output( { if(itr!=it->second.begin()) out << ";"; out << itr->first << ":" << itr->second.first; + out << "@" << itr->second.second->location_number; } out << "]" << std::endl; } @@ -483,7 +447,7 @@ Function: rd_range_domaint::merge bool rd_range_domaint::merge( const rd_range_domaint &other, - locationt to) + goto_programt::const_targett to) { bool more=false; @@ -520,6 +484,107 @@ bool rd_range_domaint::merge( /*******************************************************************\ +Function: rd_range_domaint::merge_shared + + Inputs: + + Outputs: returns true iff there is s.th. new + + Purpose: + +\*******************************************************************/ + +bool rd_range_domaint::merge_shared( + const namespacet &ns, + const rd_range_domaint &other, + goto_programt::const_targett to) +{ + bool more=false; + + valuest::iterator it=values.begin(); + for(valuest::const_iterator ito=other.values.begin(); + ito!=other.values.end(); + ++ito) + { + while(it!=values.end() && it->firstfirst) + ++it; + if(it==values.end() || ito->firstfirst) + { + if(ns.lookup(ito->first).is_shared()) + { + values.insert(*ito); + more=true; + } + } + else if(it!=values.end() && + !ns.lookup(ito->first).is_shared()) + { + ++it; + } + else if(it!=values.end()) + { + assert(it->first==ito->first); + const rangest &rangeso=ito->second; + for(rangest::const_iterator itro=rangeso.begin(); + itro!=rangeso.end(); + ++itro) + more|=gen( + itro->second.second, + ito->first, + itro->first, + itro->second.first); + ++it; + } + } + + return more; +} + +/*******************************************************************\ + +Function: rd_range_domaint::get + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +const rd_range_domaint::rangest& rd_range_domaint::get( + const irep_idt &identifier) const +{ + static rangest empty; + + valuest::const_iterator entry=values.find(identifier); + + if(entry==values.end()) + return empty; + else + return entry->second; +} + +/*******************************************************************\ + +Function: reaching_definitions_analysist::~reaching_definitions_analysist + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +reaching_definitions_analysist::~reaching_definitions_analysist() +{ + if(is_threaded) delete is_threaded; + if(may_alias) delete may_alias; +} + +/*******************************************************************\ + Function: reaching_definitions_analysist::initialize Inputs: @@ -533,11 +598,8 @@ Function: reaching_definitions_analysist::initialize void reaching_definitions_analysist::initialize( const goto_functionst &goto_functions) { - forall_goto_functions(f_it, goto_functions) - { - local_may_aliases.insert( - std::make_pair(f_it->first, local_may_aliast(f_it->second))); - } + may_alias=new may_aliast(goto_functions, ns); + is_threaded=new is_threadedt(goto_functions); static_analysist::initialize(goto_functions); } @@ -554,13 +616,11 @@ Function: reaching_definitions_analysist::generate_state \*******************************************************************/ -void reaching_definitions_analysist::generate_state(locationt l) +void reaching_definitions_analysist::generate_state( + goto_programt::const_targett l) { static_analysist::generate_state(l); - may_aliasest::iterator entry= - local_may_aliases.find(l->function); - if(entry!=local_may_aliases.end()) - state_map[l].set_may_alias(&(entry->second)); + state_map[l].set_sub_analyses(may_alias, is_threaded); } diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h index 32c0ba8..7753ef9 100644 --- a/src/analyses/reaching_definitions.h +++ b/src/analyses/reaching_definitions.h @@ -9,114 +9,128 @@ Date: February 2013 \*******************************************************************/ +#ifndef CPROVER_REACHING_DEFINITIONS_H +#define CPROVER_REACHING_DEFINITIONS_H + #include "static_analysis.h" -#include "local_may_alias.h" -class if_exprt; -class byte_extract_exprt; -class dereference_exprt; +class may_aliast; +class is_threadedt; class rd_range_domaint:public domain_baset { public: rd_range_domaint(): - local_may_alias(0) + may_alias(0), + is_threaded(0) { } virtual void transform( const namespacet &ns, - locationt from, - locationt to); + goto_programt::const_targett from, + goto_programt::const_targett to); virtual void output( const namespacet &ns, std::ostream &out) const; // returns true iff there is s.th. new - bool merge(const rd_range_domaint &other, locationt to); + bool merge( + const rd_range_domaint &other, + goto_programt::const_targett to); + bool merge_shared( + const namespacet &ns, + const rd_range_domaint &other, + goto_programt::const_targett to); - void set_may_alias(local_may_aliast *a) + void set_sub_analyses( + may_aliast *a, + is_threadedt *i) { - local_may_alias=a; + may_alias=a; + is_threaded=i; } -protected: // each element x represents a range [x.first, x.second.first) - typedef std::multimap > - rangest; - typedef hash_map_cont valuest; + typedef std::multimap > rangest; + #ifdef USE_DSTRING + typedef std::map valuest; + #else + typedef hash_map_cont valuest; + #endif + + const rangest& get(const irep_idt &identifier) const; + +protected: valuest values; - local_may_aliast * local_may_alias; + may_aliast * may_alias; + is_threadedt * is_threaded; - void assign( + void transform_dead( const namespacet &ns, - locationt from, - const exprt &lhs, - const mp_integer &size); - void assign_if( + goto_programt::const_targett from); + void transform_start_thread(const namespacet &ns); + void transform_function_call( const namespacet &ns, - locationt from, - const if_exprt &if_expr, - const mp_integer &size); - void assign_dereference( + goto_programt::const_targett from, + goto_programt::const_targett to); + void transform_end_function( const namespacet &ns, - locationt from, - const dereference_exprt &deref, - const mp_integer &size); - void assign_byte_extract( + goto_programt::const_targett from); + void transform_assign( const namespacet &ns, - locationt from, - const byte_extract_exprt &be, - const mp_integer &size); - - void assign( - const namespacet &ns, - locationt from, - const exprt &lhs, - const mp_integer &range_start, - const mp_integer &size); + goto_programt::const_targett from, + const exprt &lhs); void kill( - locationt from, + goto_programt::const_targett from, const irep_idt &identifier, const mp_integer &range_start, - const mp_integer &size); + const mp_integer &range_end); void kill_inf( - locationt from, + goto_programt::const_targett from, const irep_idt &identifier, const mp_integer &range_start); bool gen( - locationt from, + goto_programt::const_targett from, const irep_idt &identifier, const mp_integer &range_start, - const mp_integer &size); + const mp_integer &range_end); }; class reaching_definitions_analysist : - public static_analysist + public concurrency_aware_static_analysist { public: // constructor explicit reaching_definitions_analysist(const namespacet &_ns): - static_analysist(_ns) + concurrency_aware_static_analysist(_ns), + may_alias(0), + is_threaded(0) { } + virtual ~reaching_definitions_analysist(); + virtual void initialize( const goto_programt &goto_program) { - throw "reaching definitions uses local_may_aliast, cannot be used on goto_programt"; + throw "reaching definitions uses may_aliast, cannot be used on goto_programt"; } virtual void initialize( const goto_functionst &goto_functions); protected: - typedef hash_map_cont may_aliasest; - may_aliasest local_may_aliases; + may_aliast * may_alias; + is_threadedt * is_threaded; - virtual void generate_state(locationt l); + virtual void generate_state(goto_programt::const_targett l); }; +#endif + diff --git a/src/analyses/static_analysis.cpp b/src/analyses/static_analysis.cpp index 6171e72..a434c6c 100644 --- a/src/analyses/static_analysis.cpp +++ b/src/analyses/static_analysis.cpp @@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include "is_threaded.h" + #include "static_analysis.h" /*******************************************************************\ @@ -28,13 +30,13 @@ Function: static_analysis_baset::get_guard \*******************************************************************/ exprt static_analysis_baset::get_guard( - locationt from, - locationt to) + goto_programt::const_targett from, + goto_programt::const_targett to) { if(!from->is_goto()) return true_exprt(); - locationt next=from; + goto_programt::const_targett next=from; next++; if(next==to) @@ -59,7 +61,8 @@ Function: static_analysis_baset::get_return_lhs \*******************************************************************/ -exprt static_analysis_baset::get_return_lhs(locationt to) +exprt static_analysis_baset::get_return_lhs( + goto_programt::const_targett to) { // get predecessor of "to" @@ -258,7 +261,7 @@ Function: static_analysis_baset::generate_states void static_analysis_baset::update( const goto_programt &goto_program) { - locationt previous; + goto_programt::const_targett previous; bool first=true; forall_goto_program_instructions(i_it, goto_program) @@ -289,13 +292,13 @@ Function: static_analysis_baset::get_next \*******************************************************************/ -static_analysis_baset::locationt static_analysis_baset::get_next( +goto_programt::const_targett static_analysis_baset::get_next( working_sett &working_set) { assert(!working_set.empty()); working_sett::iterator i=working_set.begin(); - locationt l=i->second; + goto_programt::const_targett l=i->second; working_set.erase(i); return l; @@ -330,7 +333,7 @@ bool static_analysis_baset::fixedpoint( while(!working_set.empty()) { - locationt l=get_next(working_set); + goto_programt::const_targett l=get_next(working_set); if(visit(l, working_set, goto_program, goto_functions)) new_data=true; @@ -352,7 +355,7 @@ Function: static_analysis_baset::visit \*******************************************************************/ bool static_analysis_baset::visit( - locationt l, + goto_programt::const_targett l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions) @@ -372,7 +375,7 @@ bool static_analysis_baset::visit( it!=successors.end(); it++) { - locationt to_l=*it; + goto_programt::const_targett to_l=*it; if(to_l==goto_program.instructions.end()) continue; @@ -426,7 +429,8 @@ Function: static_analysis_baset::do_function_call \*******************************************************************/ void static_analysis_baset::do_function_call( - locationt l_call, locationt l_return, + goto_programt::const_targett l_call, + goto_programt::const_targett l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, @@ -441,17 +445,19 @@ void static_analysis_baset::do_function_call( { // get the state at the beginning of the function - locationt l_begin=goto_function.body.instructions.begin(); + goto_programt::const_targett l_begin= + goto_function.body.instructions.begin(); // do the edge from the call site to the beginning of the function - new_state.transform(ns, l_call, l_begin); + std::auto_ptr tmp_state(make_temporary_state(new_state)); + tmp_state->transform(ns, l_call, l_begin); statet &begin_state=get_state(l_begin); bool new_data=false; // merge the new stuff - if(merge(begin_state, new_state, l_begin)) + if(merge(begin_state, *tmp_state, l_begin)) new_data=true; // do each function at least once @@ -472,21 +478,27 @@ void static_analysis_baset::do_function_call( { // get location at end of procedure - locationt l_end=--goto_function.body.instructions.end(); + goto_programt::const_targett l_end= + --goto_function.body.instructions.end(); assert(l_end->is_end_function()); statet &end_of_function=get_state(l_end); // do edge from end of function to instruction after call - locationt l_next=l_call; - l_next++; - end_of_function.transform(ns, l_end, l_next); + std::auto_ptr tmp_state( + make_temporary_state(end_of_function)); + tmp_state->transform(ns, l_end, l_return); // propagate those -- not exceedingly precise, this is, // as still it contains all the state from the // call site - merge(new_state, end_of_function, l_end); + merge(new_state, *tmp_state, l_return); + } + + { + // effect on current procedure (if any) + new_state.transform(ns, l_call, l_return); } } @@ -503,7 +515,8 @@ Function: static_analysis_baset::do_function_call_rec \*******************************************************************/ void static_analysis_baset::do_function_call_rec( - locationt l_call, locationt l_return, + goto_programt::const_targett l_call, + goto_programt::const_targett l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, @@ -580,7 +593,13 @@ void static_analysis_baset::do_function_call_rec( { const object_descriptor_exprt &o=to_object_descriptor_expr(*it); std::auto_ptr n2(make_temporary_state(new_state)); - do_function_call_rec(l_call, l_return, o.object(), arguments, *n2, goto_functions); + do_function_call_rec( + l_call, + l_return, + o.object(), + arguments, + *n2, + goto_functions); merge(new_state, *n2, l_return); } } @@ -606,7 +625,7 @@ void static_analysis_baset::do_function_call_rec( /*******************************************************************\ -Function: static_analysis_baset::fixedpoint +Function: static_analysis_baset::sequential_fixedpoint Inputs: @@ -616,25 +635,19 @@ Function: static_analysis_baset::fixedpoint \*******************************************************************/ -void static_analysis_baset::fixedpoint( +void static_analysis_baset::sequential_fixedpoint( const goto_functionst &goto_functions) { // do each function at least once - for(goto_functionst::function_mapt::const_iterator - it=goto_functions.function_map.begin(); - it!=goto_functions.function_map.end(); - it++) - if(functions_done.find(it->first)== - functions_done.end()) - { - fixedpoint(it, goto_functions); - } + forall_goto_functions(it, goto_functions) + if(functions_done.insert(it->first).second) + fixedpoint(it->second.body, goto_functions); } /*******************************************************************\ -Function: static_analysis_baset::fixedpoint +Function: static_analysis_baset::concurrent_fixedpoint Inputs: @@ -644,10 +657,74 @@ Function: static_analysis_baset::fixedpoint \*******************************************************************/ -bool static_analysis_baset::fixedpoint( - const goto_functionst::function_mapt::const_iterator it, +void static_analysis_baset::concurrent_fixedpoint( const goto_functionst &goto_functions) { - functions_done.insert(it->first); - return fixedpoint(it->second.body, goto_functions); + sequential_fixedpoint(goto_functions); + + is_threadedt is_threaded(goto_functions); + + // construct an initial shared state collecting the results of all + // functions + goto_programt tmp; + tmp.add_instruction(); + goto_programt::const_targett sh_target=tmp.instructions.begin(); + generate_state(sh_target); + statet &shared_state=get_state(sh_target); + + typedef std::list > thread_wlt; + thread_wlt thread_wl; + + forall_goto_functions(it, goto_functions) + forall_goto_program_instructions(t_it, it->second.body) + { + if(is_threaded(t_it)) + { + thread_wl.push_back(std::make_pair(&(it->second.body), t_it)); + + goto_programt::const_targett l_end= + it->second.body.instructions.end(); + --l_end; + + const statet &end_state=get_state(l_end); + merge_shared(shared_state, end_state, sh_target); + } + } + + // new feed in the shared state into all concurrently executing + // functions, and iterate until the shared state stabilizes + bool new_shared=true; + while(new_shared) + { + new_shared=false; + + for(thread_wlt::const_iterator it=thread_wl.begin(); + it!=thread_wl.end(); + ++it) + { + working_sett working_set; + put_in_working_set(working_set, it->second); + + statet &begin_state=get_state(it->second); + merge(begin_state, shared_state, it->second); + + while(!working_set.empty()) + { + goto_programt::const_targett l=get_next(working_set); + + visit(l, working_set, *(it->first), goto_functions); + + // the underlying domain must make sure that the final state + // carries all possible values; otherwise we would need to + // merge over each and every state + if(l->is_end_function()) + { + statet &end_state=get_state(l); + new_shared|=merge_shared(shared_state, end_state, sh_target); + } + } + } + } } + diff --git a/src/analyses/static_analysis.h b/src/analyses/static_analysis.h index a4c7c13..c4308e6 100644 --- a/src/analyses/static_analysis.h +++ b/src/analyses/static_analysis.h @@ -26,14 +26,12 @@ public: virtual ~domain_baset() { } - - typedef goto_programt::const_targett locationt; // will go away, // to be replaced by a factory class option to static_analysist virtual void initialize( const namespacet &ns, - locationt l) + goto_programt::const_targett l) { } @@ -47,8 +45,8 @@ public: virtual void transform( const namespacet &ns, - locationt from, - locationt to)=0; + goto_programt::const_targett from, + goto_programt::const_targett to)=0; virtual void output( const namespacet &ns, @@ -70,7 +68,7 @@ public: // also add // - // bool merge(const T &b, locationt to); + // bool merge(const T &b, goto_programt::const_targett to); // // this computes the join between "this" and "b" // return true if "this" has changed @@ -87,7 +85,6 @@ class static_analysis_baset { public: typedef domain_baset statet; - typedef goto_programt::const_targett locationt; explicit static_analysis_baset(const namespacet &_ns): ns(_ns), @@ -144,9 +141,9 @@ public: output(goto_program, "", out); } - virtual bool has_location(locationt l) const=0; + virtual bool has_location(goto_programt::const_targett l) const=0; - void insert(locationt l) + void insert(goto_programt::const_targett l) { generate_state(l); } @@ -154,11 +151,13 @@ public: // utilities // get guard of a conditional edge - static exprt get_guard(locationt from, locationt to); + static exprt get_guard( + goto_programt::const_targett from, + goto_programt::const_targett to); // get lhs that return value is assigned to // for an edge that returns from a function - static exprt get_return_lhs(locationt to); + static exprt get_return_lhs(goto_programt::const_targett to); protected: const namespacet &ns; @@ -168,16 +167,15 @@ protected: const irep_idt &identifier, std::ostream &out) const; - typedef std::map working_sett; + typedef std::map working_sett; - locationt get_next(working_sett &working_set); + goto_programt::const_targett get_next(working_sett &working_set); void put_in_working_set( working_sett &working_set, - locationt l) + goto_programt::const_targett l) { - working_set.insert( - std::pair(l->location_number, l)); + working_set.insert(std::make_pair(l->location_number, l)); } // true = found s.th. new @@ -185,27 +183,30 @@ protected: const goto_programt &goto_program, const goto_functionst &goto_functions); - bool fixedpoint( - goto_functionst::function_mapt::const_iterator it, + virtual void fixedpoint( + const goto_functionst &goto_functions)=0; + + void sequential_fixedpoint( const goto_functionst &goto_functions); - - void fixedpoint( + void concurrent_fixedpoint( const goto_functionst &goto_functions); // true = found s.th. new bool visit( - locationt l, + goto_programt::const_targett l, working_sett &working_set, const goto_programt &goto_program, const goto_functionst &goto_functions); - - static locationt successor(locationt l) - { - l++; - return l; - } - virtual bool merge(statet &a, const statet &b, locationt to)=0; + virtual bool merge( + statet &a, + const statet &b, + goto_programt::const_targett to)=0; + // for concurrent fixedpoint + virtual bool merge_shared( + statet &a, + const statet &b, + goto_programt::const_targett to)=0; typedef std::set functions_donet; functions_donet functions_done; @@ -223,14 +224,16 @@ protected: // function calls void do_function_call_rec( - locationt l_call, locationt l_return, + goto_programt::const_targett l_call, + goto_programt::const_targett l_return, const exprt &function, const exprt::operandst &arguments, statet &new_state, const goto_functionst &goto_functions); void do_function_call( - locationt l_call, locationt l_return, + goto_programt::const_targett l_call, + goto_programt::const_targett l_return, const goto_functionst &goto_functions, const goto_functionst::function_mapt::const_iterator f_it, const exprt::operandst &arguments, @@ -238,15 +241,15 @@ protected: // abstract methods - virtual void generate_state(locationt l)=0; - virtual statet &get_state(locationt l)=0; - virtual const statet &get_state(locationt l) const=0; + virtual void generate_state(goto_programt::const_targett l)=0; + virtual statet &get_state(goto_programt::const_targett l)=0; + virtual const statet &get_state(goto_programt::const_targett l) const=0; virtual statet* make_temporary_state(statet &s)=0; typedef domain_baset::expr_sett expr_sett; virtual void get_reference_set( - locationt l, + goto_programt::const_targett l, const exprt &expr, std::list &dest)=0; }; @@ -262,16 +265,14 @@ public: { } - typedef goto_programt::const_targett locationt; - - inline T &operator[](locationt l) + inline T &operator[](goto_programt::const_targett l) { typename state_mapt::iterator it=state_map.find(l); if(it==state_map.end()) throw "failed to find state"; return it->second; } - inline const T &operator[](locationt l) const + inline const T &operator[](goto_programt::const_targett l) const { typename state_mapt::const_iterator it=state_map.find(l); if(it==state_map.end()) throw "failed to find state"; @@ -284,30 +285,33 @@ public: static_analysis_baset::clear(); } - virtual bool has_location(locationt l) const + virtual bool has_location(goto_programt::const_targett l) const { return state_map.count(l)!=0; } protected: - typedef std::map state_mapt; + typedef std::map state_mapt; state_mapt state_map; - virtual statet &get_state(locationt l) + virtual statet &get_state(goto_programt::const_targett l) { typename state_mapt::iterator it=state_map.find(l); if(it==state_map.end()) throw "failed to find state"; return it->second; } - virtual const statet &get_state(locationt l) const + virtual const statet &get_state(goto_programt::const_targett l) const { typename state_mapt::const_iterator it=state_map.find(l); if(it==state_map.end()) throw "failed to find state"; return it->second; } - virtual bool merge(statet &a, const statet &b, locationt to) + virtual bool merge( + statet &a, + const statet &b, + goto_programt::const_targett to) { return static_cast(a).merge(static_cast(b), to); } @@ -317,22 +321,64 @@ protected: return new T(static_cast(s)); } - virtual void generate_state(locationt l) + virtual void generate_state(goto_programt::const_targett l) { state_map[l].initialize(ns, l); } virtual void get_reference_set( - locationt l, + goto_programt::const_targett l, const exprt &expr, std::list &dest) { state_map[l].get_reference_set(ns, expr, dest); } + virtual void fixedpoint(const goto_functionst &goto_functions) + { + sequential_fixedpoint(goto_functions); + } + private: // to enforce that T is derived from domain_baset void dummy(const T &s) { const statet &x=dummy1(s); (void)x; } + + // not implemented in sequential analyses + virtual bool merge_shared( + statet &a, + const statet &b, + goto_programt::const_targett to) + { + throw "not implemented"; + } +}; + +template +class concurrency_aware_static_analysist:public static_analysist +{ +public: + // constructor + explicit concurrency_aware_static_analysist(const namespacet &_ns): + static_analysist(_ns) + { + } + + virtual bool merge_shared( + static_analysis_baset::statet &a, + const static_analysis_baset::statet &b, + goto_programt::const_targett to) + { + return static_cast(a).merge_shared( + this->ns, + static_cast(b), + to); + } + +protected: + virtual void fixedpoint(const goto_functionst &goto_functions) + { + this->concurrent_fixedpoint(goto_functions); + } }; #endif diff --git a/src/analyses/uninitialized_domain.cpp b/src/analyses/uninitialized_domain.cpp index c5fc067..f1cfefa 100644 --- a/src/analyses/uninitialized_domain.cpp +++ b/src/analyses/uninitialized_domain.cpp @@ -27,8 +27,8 @@ Function: uninitialized_domaint::transform void uninitialized_domaint::transform( const namespacet &ns, - locationt from, - locationt to) + goto_programt::const_targett from, + goto_programt::const_targett to) { switch(from->type) { @@ -115,7 +115,7 @@ Function: uninitialized_domaint::merge bool uninitialized_domaint::merge( const uninitialized_domaint &other, - locationt to) + goto_programt::const_targett to) { unsigned old_uninitialized=uninitialized.size(); diff --git a/src/analyses/uninitialized_domain.h b/src/analyses/uninitialized_domain.h index 4e199bf..b5689a3 100644 --- a/src/analyses/uninitialized_domain.h +++ b/src/analyses/uninitialized_domain.h @@ -19,15 +19,17 @@ public: virtual void transform( const namespacet &ns, - locationt from, - locationt to); + goto_programt::const_targett from, + goto_programt::const_targett to); virtual void output( const namespacet &ns, std::ostream &out) const; // returns true iff there is s.th. new - bool merge(const uninitialized_domaint &other, locationt to); + bool merge( + const uninitialized_domaint &other, + goto_programt::const_targett to); protected: void assign(const exprt &lhs); diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index e6db701..c7e8249 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -12,7 +12,8 @@ SRC = goto_instrument_main.cpp goto_instrument_parseoptions.cpp \ call_sequences.cpp unwind.cpp \ accelerate/accelerate.cpp accelerate/polynomial.cpp \ accelerate/scratch_program.cpp accelerate/polynomial_accelerator.cpp \ - accelerate/util.cpp count_eloc.cpp reachability_slicer.cpp + accelerate/util.cpp count_eloc.cpp reachability_slicer.cpp \ + wmm/static_cycles.cpp OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../linking/linking$(LIBEXT) \ diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp index 9395968..8d71ed2 100644 --- a/src/goto-instrument/dump_c.cpp +++ b/src/goto-instrument/dump_c.cpp @@ -817,10 +817,11 @@ goto_programt::const_targett goto_program2codet::convert_return( to_side_effect_expr(ret.return_value()).get_statement()==ID_nondet) { const cfg_dominatorst &dominators=loops.get_dominator_info(); - cfg_dominatorst::node_mapt::const_iterator i_entry= - dominators.node_map.find(target); - assert(i_entry!=dominators.node_map.end()); - const cfg_dominatorst::nodet &n=i_entry->second; + cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry= + dominators.cfg.entry_map.find(target); + assert(i_entry!=dominators.cfg.entry_map.end()); + const cfg_dominatorst::cfgt::nodet &n= + dominators.cfg[i_entry->second]; if(n.dominators.empty()) { @@ -1057,10 +1058,10 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch( // always use convert_goto_if for dead code as the construction below relies // on effective dominator information - cfg_dominatorst::node_mapt::const_iterator t_entry= - dominators.node_map.find(target); - assert(t_entry!=dominators.node_map.end()); - if(t_entry->second.dominators.empty()) + cfg_dominatorst::cfgt::entry_mapt::const_iterator t_entry= + dominators.cfg.entry_map.find(target); + assert(t_entry!=dominators.cfg.entry_map.end()); + if(dominators.cfg[t_entry->second].dominators.empty()) return convert_goto_if(target, upper_bound, dest); // maybe, let's try some more @@ -1193,10 +1194,11 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch( case_end!=upper_bound; ++case_end) { - cfg_dominatorst::node_mapt::const_iterator i_entry= - dominators.node_map.find(case_end); - assert(i_entry!=dominators.node_map.end()); - const cfg_dominatorst::nodet &n=i_entry->second; + cfg_dominatorst::cfgt::entry_mapt::const_iterator i_entry= + dominators.cfg.entry_map.find(case_end); + assert(i_entry!=dominators.cfg.entry_map.end()); + const cfg_dominatorst::cfgt::nodet &n= + dominators.cfg[i_entry->second]; // ignore dead instructions for the following checks if(n.dominators.empty()) @@ -1256,10 +1258,11 @@ goto_programt::const_targett goto_program2codet::convert_goto_switch( if(processed_locations.find(it->location_number)== processed_locations.end()) { - cfg_dominatorst::node_mapt::const_iterator it_entry= - dominators.node_map.find(it); - assert(it_entry!=dominators.node_map.end()); - const cfg_dominatorst::nodet &n=it_entry->second; + cfg_dominatorst::cfgt::entry_mapt::const_iterator it_entry= + dominators.cfg.entry_map.find(it); + assert(it_entry!=dominators.cfg.entry_map.end()); + const cfg_dominatorst::cfgt::nodet &n= + dominators.cfg[it_entry->second]; if(!n.dominators.empty()) return convert_goto_if(orig_target, upper_bound, dest); diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp index 334622a..2c046bf 100644 --- a/src/goto-instrument/full_slicer.cpp +++ b/src/goto-instrument/full_slicer.cpp @@ -33,33 +33,38 @@ void full_slicert::fixedpoint() e_it=cfg.entry_map.begin(); e_it!=cfg.entry_map.end(); e_it++) + { + cfgt::nodet &node=cfg[e_it->second]; + if(e_it->first->is_assert()) { - get_objects(e_it->first->guard, e_it->second.required_objects); - e_it->second.node_required=true; - queue.push(&e_it->second); + get_objects(e_it->first->guard, node.required_objects); + node.node_required=true; + queue.push(e_it->second); } else if(e_it->first->is_end_function()) - e_it->second.node_required=true; // always retained + node.node_required=true; // always retained + } // process queue until empty while(!queue.empty()) { - cfgt::iterator e=queue.top(); + cfgt::entryt e=queue.top(); + cfgt::nodet &node=cfg[e]; queue.pop(); // look at required_objects - object_id_sett required_objects=transform(e); + object_id_sett required_objects=transform(node); - for(cfgt::entriest::const_iterator - p_it=e->predecessors.begin(); - p_it!=e->predecessors.end(); + for(cfgt::edgest::const_iterator + p_it=node.in.begin(); + p_it!=node.in.end(); p_it++) { - (*p_it)->required_objects.insert( + cfg[p_it->first].required_objects.insert( required_objects.begin(), required_objects.end()); - queue.push(*p_it); + queue.push(p_it->first); } } } @@ -93,7 +98,7 @@ void full_slicert::slice(goto_functionst &goto_functions) Forall_goto_program_instructions(i_it, f_it->second.body) { const cfgt::entryt &e=cfg.entry_map[i_it]; - if(!e.node_required) + if(!cfg[e].node_required) i_it->make_skip(); } } @@ -115,12 +120,12 @@ Function: full_slicert::transform \*******************************************************************/ -object_id_sett full_slicert::transform(cfgt::iterator e) +object_id_sett full_slicert::transform(cfgt::nodet& e) { - const object_id_sett &old_set=e->required_objects; - object_id_sett new_set=e->required_objects; // copy! + const object_id_sett &old_set=e.required_objects; + object_id_sett new_set=e.required_objects; // copy! - const goto_programt::instructiont &instruction=*(e->PC); + const goto_programt::instructiont &instruction=*(e.PC); switch(instruction.type) { @@ -140,7 +145,7 @@ object_id_sett full_slicert::transform(cfgt::iterator e) if(found) { - e->node_required=true; + e.node_required=true; new_set.insert(w.begin(), w.end()); } } @@ -162,7 +167,7 @@ object_id_sett full_slicert::transform(cfgt::iterator e) if(found) { - e->node_required=true; + e.node_required=true; new_set.insert(w.begin(), w.end()); } } @@ -199,7 +204,7 @@ object_id_sett full_slicert::transform(cfgt::iterator e) if(found) { - e->node_required=true; + e.node_required=true; // add what it reads get_objects_r(code_assign, new_set); } @@ -211,7 +216,7 @@ object_id_sett full_slicert::transform(cfgt::iterator e) object_idt object_id(to_symbol_expr(instruction.code.op0())); if(old_set.find(object_id)!=old_set.end()) { - e->node_required=true; + e.node_required=true; new_set.erase(object_id); } } @@ -239,7 +244,7 @@ object_id_sett full_slicert::transform(cfgt::iterator e) if(old_set.find(lhs_id)!=old_set.end()) { new_set.erase(lhs_id); - e->node_required=true; + e.node_required=true; get_objects(code_function_call.arguments()[i], new_set); } } diff --git a/src/goto-instrument/full_slicer_class.h b/src/goto-instrument/full_slicer_class.h index 0bb9c29..ec824cb 100644 --- a/src/goto-instrument/full_slicer_class.h +++ b/src/goto-instrument/full_slicer_class.h @@ -46,11 +46,11 @@ protected: typedef cfg_baset cfgt; cfgt cfg; - typedef std::stack queuet; + typedef std::stack queuet; void fixedpoint(); void slice(goto_functionst &goto_functions); - object_id_sett transform(cfgt::iterator); + object_id_sett transform(cfgt::nodet&); }; #endif diff --git a/src/goto-instrument/goto_instrument_parseoptions.cpp b/src/goto-instrument/goto_instrument_parseoptions.cpp index b624f26..410fa0a 100644 --- a/src/goto-instrument/goto_instrument_parseoptions.cpp +++ b/src/goto-instrument/goto_instrument_parseoptions.cpp @@ -35,7 +35,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include +#include #include #include #include @@ -70,6 +70,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "call_sequences.h" #include "accelerate/accelerate.h" #include "count_eloc.h" +#include "wmm/static_cycles.h" /*******************************************************************\ @@ -164,15 +165,23 @@ int goto_instrument_parseoptionst::doit() status() << "Partial Inlining" << eom; goto_partial_inline(goto_functions, ns, ui_message_handler); - forall_goto_functions(it, goto_functions) - { - local_may_aliast local_may_alias(it->second); - std::cout << ">>>>" << std::endl; - std::cout << ">>>> " << it->first << std::endl; - std::cout << ">>>>" << std::endl; - local_may_alias.output(std::cout, it->second, ns); - std::cout << std::endl; - } + may_aliast may_alias(goto_functions, ns); + may_alias.output(std::cout, goto_functions); + + return 0; + } + + if(cmdline.isset("static-cycles")) + { + namespacet ns(symbol_table); + + status() << "Function Pointer Removal" << eom; + remove_function_pointers(symbol_table, goto_functions, false); + + status() << "Partial Inlining" << eom; + goto_partial_inline(goto_functions, ns, ui_message_handler); + + static_cycles(symbol_table, goto_functions); return 0; } @@ -257,6 +266,9 @@ int goto_instrument_parseoptionst::doit() if(cmdline.isset("show-reaching-definitions")) { + status() << "Function Pointer Removal" << eom; + remove_function_pointers(symbol_table, goto_functions, false); + const namespacet ns(symbol_table); reaching_definitions_analysist rd_analysis(ns); rd_analysis(goto_functions); @@ -574,7 +586,7 @@ void goto_instrument_parseoptionst::instrument_goto_program( // we add the library in some cases, as some analyses benefit - if(cmdline.isset("mm")) + if(cmdline.isset("mm") || cmdline.isset("static-cycles")) { status() << "Adding CPROVER library" << eom; link_to_library(symbol_table, goto_functions, ui_message_handler); @@ -777,7 +789,7 @@ void goto_instrument_parseoptionst::instrument_goto_program( if(cmdline.isset("havoc-loops")) { status() << "Havocing loops" << eom; - havoc_loops(goto_functions); + havoc_loops(goto_functions, ns); } if(cmdline.isset("k-induction")) @@ -798,7 +810,7 @@ void goto_instrument_parseoptionst::instrument_goto_program( status() << "Instrumenting k-induction for k=" << k << ", " << (base_case?"base case":"step case") << eom; - k_induction(goto_functions, base_case, step_case, k); + k_induction(goto_functions, base_case, step_case, k, ns); } if(cmdline.isset("function-enter")) @@ -943,6 +955,7 @@ void goto_instrument_parseoptionst::help() " --no-po-rendering no representation of the threads in the dot\n" " --render-cluster-file clusterises the dot by files\n" " --render-cluster-function clusterises the dot by functions\n" + " --static-cycles identify potentially critical cycles\n" "\n" "Slicing:\n" " --reachability-slicer slice away instructions that can't reach assertions\n" diff --git a/src/goto-instrument/goto_instrument_parseoptions.h b/src/goto-instrument/goto_instrument_parseoptions.h index 3c2141a..9585717 100644 --- a/src/goto-instrument/goto_instrument_parseoptions.h +++ b/src/goto-instrument/goto_instrument_parseoptions.h @@ -54,7 +54,7 @@ Author: Daniel Kroening, kroening@kroening.com "(accelerate)" \ "(k-induction):(step-case)(base-case)" \ "(show-call-sequences)(check-call-sequence)" \ - "(interpreter)(show-reaching-definitions)(count-eloc)" + "(interpreter)(show-reaching-definitions)(count-eloc)(static-cycles)" class goto_instrument_parseoptionst: public parseoptions_baset, diff --git a/src/goto-instrument/havoc_loops.cpp b/src/goto-instrument/havoc_loops.cpp index c85419b..d5ff26c 100644 --- a/src/goto-instrument/havoc_loops.cpp +++ b/src/goto-instrument/havoc_loops.cpp @@ -20,9 +20,11 @@ class havoc_loopst public: typedef goto_functionst::goto_functiont goto_functiont; - explicit havoc_loopst(goto_functiont &_goto_function): + havoc_loopst( + goto_functiont &_goto_function, + const namespacet &ns): goto_function(_goto_function), - local_may_alias(_goto_function), + local_may_alias(_goto_function, ns), natural_loops(_goto_function.body) { havoc_loops(); @@ -283,8 +285,10 @@ Function: havoc_loops \*******************************************************************/ -void havoc_loops(goto_functionst &goto_functions) +void havoc_loops( + goto_functionst &goto_functions, + const namespacet &ns) { Forall_goto_functions(it, goto_functions) - havoc_loopst(it->second); + havoc_loopst(it->second, ns); } diff --git a/src/goto-instrument/havoc_loops.h b/src/goto-instrument/havoc_loops.h index bf58e12..ca04af3 100644 --- a/src/goto-instrument/havoc_loops.h +++ b/src/goto-instrument/havoc_loops.h @@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #include -void havoc_loops(goto_functionst &goto_functions); +void havoc_loops( + goto_functionst &goto_functions, + const namespacet &ns); #endif diff --git a/src/goto-instrument/k_induction.cpp b/src/goto-instrument/k_induction.cpp index 3f8ff5e..6990959 100644 --- a/src/goto-instrument/k_induction.cpp +++ b/src/goto-instrument/k_induction.cpp @@ -24,9 +24,9 @@ public: k_inductiont( goto_functiont &_goto_function, bool _base_case, bool _step_case, - unsigned _k): + unsigned _k, const namespacet &ns): goto_function(_goto_function), - local_may_alias(_goto_function), + local_may_alias(_goto_function, ns), natural_loops(_goto_function.body), base_case(_base_case), step_case(_step_case), k(_k) { @@ -302,8 +302,8 @@ Function: k_induction void k_induction( goto_functionst &goto_functions, bool base_case, bool step_case, - unsigned k) + unsigned k, const namespacet &ns) { Forall_goto_functions(it, goto_functions) - k_inductiont(it->second, base_case, step_case, k); + k_inductiont(it->second, base_case, step_case, k, ns); } diff --git a/src/goto-instrument/k_induction.h b/src/goto-instrument/k_induction.h index 207270d..825fbdf 100644 --- a/src/goto-instrument/k_induction.h +++ b/src/goto-instrument/k_induction.h @@ -14,6 +14,6 @@ Author: Daniel Kroening, kroening@kroening.com void k_induction( goto_functionst &goto_functions, bool base_case, bool step_case, - unsigned k); + unsigned k, const namespacet &ns); #endif diff --git a/src/goto-instrument/points_to.cpp b/src/goto-instrument/points_to.cpp index ead548f..4cc9941 100644 --- a/src/goto-instrument/points_to.cpp +++ b/src/goto-instrument/points_to.cpp @@ -35,7 +35,7 @@ void points_tot::fixedpoint() e_it!=cfg.entry_map.end(); e_it++) { - if(transform(&e_it->second)) + if(transform(cfg[e_it->second])) added=true; } } @@ -87,10 +87,10 @@ Function: points_tot::transform \*******************************************************************/ -bool points_tot::transform(cfgt::iterator e) +bool points_tot::transform(const cfgt::nodet &e) { bool result=false; - const goto_programt::instructiont &instruction=*(e->PC); + const goto_programt::instructiont &instruction=*(e.PC); switch(instruction.type) { diff --git a/src/goto-instrument/points_to.h b/src/goto-instrument/points_to.h index dc1637e..58dca7d 100644 --- a/src/goto-instrument/points_to.h +++ b/src/goto-instrument/points_to.h @@ -57,21 +57,14 @@ public: } protected: - struct cfg_nodet - { - cfg_nodet() - { - } - }; - - typedef cfg_baset cfgt; + typedef cfg_baset cfgt; cfgt cfg; typedef std::map value_mapt; value_mapt value_map; void fixedpoint(); - bool transform(cfgt::iterator); + bool transform(const cfgt::nodet&); const object_id_sett empty_set; }; diff --git a/src/goto-instrument/reachability_slicer.cpp b/src/goto-instrument/reachability_slicer.cpp index 43f1d3c..d2e1d49 100644 --- a/src/goto-instrument/reachability_slicer.cpp +++ b/src/goto-instrument/reachability_slicer.cpp @@ -40,23 +40,24 @@ void reachability_slicert::fixedpoint_assertions( e_it++) if(e_it->first->is_assert() || is_threaded(e_it->first)) - queue.push(&e_it->second); + queue.push(e_it->second); while(!queue.empty()) { - cfgt::iterator e=queue.top(); + cfgt::entryt e=queue.top(); + cfgt::nodet &node=cfg[e]; queue.pop(); - if(e->reaches_assertion) continue; + if(node.reaches_assertion) continue; - e->reaches_assertion=true; + node.reaches_assertion=true; - for(cfgt::entriest::const_iterator - p_it=e->predecessors.begin(); - p_it!=e->predecessors.end(); + for(cfgt::edgest::const_iterator + p_it=node.in.begin(); + p_it!=node.in.end(); p_it++) { - queue.push(*p_it); + queue.push(p_it->first); } } } @@ -83,7 +84,7 @@ void reachability_slicert::slice(goto_functionst &goto_functions) { Forall_goto_program_instructions(i_it, f_it->second.body) { - const cfgt::entryt &e=cfg.entry_map[i_it]; + const cfgt::nodet &e=cfg[cfg.entry_map[i_it]]; if(!e.reaches_assertion && !i_it->is_end_function()) i_it->make_goto(i_it); diff --git a/src/goto-instrument/reachability_slicer_class.h b/src/goto-instrument/reachability_slicer_class.h index f21f39c..fd7a71a 100644 --- a/src/goto-instrument/reachability_slicer_class.h +++ b/src/goto-instrument/reachability_slicer_class.h @@ -46,7 +46,7 @@ protected: typedef cfg_baset cfgt; cfgt cfg; - typedef std::stack queuet; + typedef std::stack queuet; void fixedpoint_assertions(const is_threadedt &is_threaded); diff --git a/src/goto-instrument/wmm/abstract_event.cpp b/src/goto-instrument/wmm/abstract_event.cpp index 485b5d2..0b07561 100644 --- a/src/goto-instrument/wmm/abstract_event.cpp +++ b/src/goto-instrument/wmm/abstract_event.cpp @@ -81,6 +81,9 @@ bool abstract_eventt::unsafe_pair_lwfence_param(const abstract_eventt& next, || (thread!=next.thread && operation==Write && next.operation==Read && variable==next.variable)); + case Static_Weak: + return true; + case Unknown:; } assert(false); @@ -138,6 +141,9 @@ bool abstract_eventt::unsafe_pair_asm(const abstract_eventt& next, || (thread!=next.thread && operation==Write && next.operation==Read && variable==next.variable)); + case Static_Weak: + return true; + case Unknown:; } assert(false); diff --git a/src/goto-instrument/wmm/abstract_event.h b/src/goto-instrument/wmm/abstract_event.h index 7ff6c52..d9a9f31 100644 --- a/src/goto-instrument/wmm/abstract_event.h +++ b/src/goto-instrument/wmm/abstract_event.h @@ -20,7 +20,7 @@ Date: 2012 abstract event \*******************************************************************/ -class abstract_eventt:public graph_nodet +class abstract_eventt:public graph_nodet { protected: bool unsafe_pair_lwfence_param(const abstract_eventt& next, diff --git a/src/goto-instrument/wmm/cycle_collection.cpp b/src/goto-instrument/wmm/cycle_collection.cpp index 12005d3..6098a86 100644 --- a/src/goto-instrument/wmm/cycle_collection.cpp +++ b/src/goto-instrument/wmm/cycle_collection.cpp @@ -91,6 +91,7 @@ void event_grapht::graph_explorert::collect_cycles( order=&egraph.po_order; break; case Power: + case Static_Weak: order=&egraph.poUrfe_order; break; @@ -302,7 +303,8 @@ bool event_grapht::graph_explorert::backtrack( this means that we can have at most 2 consecutive events by po with the same variable, and two variables per thread (fences are not taken into account) */ - if(!point_stack.empty() && egraph.are_po_ordered(point_stack.top(),vertex) + if(egraph.filter_uniproc && + !point_stack.empty() && egraph.are_po_ordered(point_stack.top(),vertex) && this_vertex.operation!=abstract_eventt::Fence && this_vertex.operation!=abstract_eventt::Lwfence && this_vertex.operation!=abstract_eventt::ASMfence @@ -393,7 +395,7 @@ bool event_grapht::graph_explorert::backtrack( const unsigned w = w_it->first; if(w < source) egraph.remove_po_edge(vertex,w); - else if(w == source && point_stack.size()>=4 + else if(w == source && (point_stack.size()>=4 || model==Static_Weak) && (unsafe_met_updated || this_vertex.unsafe_pair(egraph[source],model)) ) { @@ -437,7 +439,7 @@ bool event_grapht::graph_explorert::backtrack( const unsigned w = w_it->first; if(w < source) egraph.remove_com_edge(vertex,w); - else if(w == source && point_stack.size()>=4 + else if(w == source && (point_stack.size()>=4 || model==Static_Weak) && (unsafe_met_updated || this_vertex.unsafe_pair(egraph[source],model)) ) { diff --git a/src/goto-instrument/wmm/event_graph.cpp b/src/goto-instrument/wmm/event_graph.cpp index 5c80ad0..120d15f 100644 --- a/src/goto-instrument/wmm/event_graph.cpp +++ b/src/goto-instrument/wmm/event_graph.cpp @@ -179,6 +179,23 @@ bool event_grapht::critical_cyclet::is_unsafe(memory_modelt model, bool fast) DEBUG_MESSAGE("cycle is safe?"); bool unsafe_met=false; + bool has_memory_access=false; + for(const_iterator it=begin(); + it!=end() && !has_memory_access; + ++it) + { + const abstract_eventt& it_evt=egraph[*it]; + + has_memory_access= + it_evt.operation==abstract_eventt::Read || + it_evt.operation==abstract_eventt::Write; + } + if(!has_memory_access) + return false; + + if(model==Static_Weak) + return size()>=2; + /* critical cycles contain at least 4 events */ if(size()<4) return false; @@ -467,6 +484,23 @@ bool event_grapht::critical_cyclet::is_unsafe_asm(memory_modelt model, bool unsafe_met = false; unsigned char fences_met = 0; + bool has_memory_access=false; + for(const_iterator it=begin(); + it!=end() && !has_memory_access; + ++it) + { + const abstract_eventt& it_evt=egraph[*it]; + + has_memory_access= + it_evt.operation==abstract_eventt::Read || + it_evt.operation==abstract_eventt::Write; + } + if(!has_memory_access) + return false; + + if(model==Static_Weak) + return size()>=2; + /* critical cycles contain at least 4 events */ if(size()<4) return false; @@ -1298,7 +1332,7 @@ std::string event_grapht::critical_cyclet::print_name( const abstract_eventt& succ=egraph[*n_it]; assert(succ.operation == abstract_eventt::Read || succ.operation == abstract_eventt::Write); - name += (model==Power?" Sync":" MFence"); + name += (model==Power||model==Static_Weak?" Sync":" MFence"); name += (prev.variable==succ.variable?"s":"d") + prev.get_operation() + succ.get_operation(); } @@ -1327,7 +1361,7 @@ std::string event_grapht::critical_cyclet::print_name( else if(cand.operation == abstract_eventt::Fence || (cand.operation == abstract_eventt::ASMfence && cand.fence_value()&1)) - cand_name = (model==Power?" Sync":" MFence"); + cand_name = (model==Power||model==Static_Weak?" Sync":" MFence"); if(!wraparound) ++cur_it; if(!wraparound) ++extra_fence_count; } @@ -1343,7 +1377,7 @@ std::string event_grapht::critical_cyclet::print_name( { std::string cand_name; if(cur.fence_value()&1) - cand_name = (model==Power?" Sync":" MFence"); + cand_name = (model==Power||model==Static_Weak?" Sync":" MFence"); else cand_name = " LwSync"; const_iterator n_it=cur_it; @@ -1367,7 +1401,7 @@ std::string event_grapht::critical_cyclet::print_name( else if(cand.operation == abstract_eventt::Fence || (cand.operation == abstract_eventt::ASMfence && cand.fence_value()&1)) - cand_name = (model==Power?" Sync":" MFence"); + cand_name = (model==Power||model==Static_Weak?" Sync":" MFence"); if(!wraparound) ++cur_it; if(!wraparound) ++extra_fence_count; } @@ -1472,7 +1506,7 @@ std::string event_grapht::critical_cyclet::print_name( else if(cand.operation == abstract_eventt::Fence || (cand.operation == abstract_eventt::ASMfence && cand.fence_value()&1)) - cand_name = (model==Power?" Sync":" MFence"); + cand_name = (model==Power||model==Static_Weak?" Sync":" MFence"); } assert(it!=reduced.begin() && it!=reduced.end()); const abstract_eventt& succ=egraph[*it]; @@ -1596,7 +1630,7 @@ void event_grapht::critical_cyclet::print_dot( const abstract_eventt& succ=( n_it!=end() ? egraph[*n_it] : egraph[front()] ); str << succ.id << "[label=\""; - str << (model==Power?"Sync":"MFence"); + str << (model==Power||model==Static_Weak?"Sync":"MFence"); str << (prev.variable==cur.variable?"s":"d"); str << prev.get_operation() << succ.get_operation(); } @@ -1668,7 +1702,7 @@ void event_grapht::critical_cyclet::print_dot( ++next; const abstract_eventt& succ=egraph[*next]; str << succ.id << "[label=\""; - str << (model==Power?"Sync":"MFence"); + str << (model==Power||model==Static_Weak?"Sync":"MFence"); str << (last.variable==first.variable?"s":"d"); str << last.get_operation() << succ.get_operation(); } diff --git a/src/goto-instrument/wmm/event_graph.h b/src/goto-instrument/wmm/event_graph.h index 84a6063..7ed9730 100644 --- a/src/goto-instrument/wmm/event_graph.h +++ b/src/goto-instrument/wmm/event_graph.h @@ -68,7 +68,7 @@ public: bool is_cycle() { /* size check */ - if(size()<4) + if(size()<2) return false; /* po order check */ @@ -193,6 +193,7 @@ public: }; protected: +public: /* graph contains po and com transitions */ graph po_graph; graph com_graph; diff --git a/src/goto-instrument/wmm/goto2graph.cpp b/src/goto-instrument/wmm/goto2graph.cpp index 34e398b..f19c38c 100644 --- a/src/goto-instrument/wmm/goto2graph.cpp +++ b/src/goto-instrument/wmm/goto2graph.cpp @@ -23,7 +23,10 @@ Date: 2012 #include #include -#include "../rw_set.h" +#include + +#include + #include "fence.h" #include "goto2graph.h" @@ -109,7 +112,7 @@ Function: instrumentert::extract_events_rw \*******************************************************************/ void instrumentert::extract_events_rw( - value_setst& value_sets, + may_aliast& may_alias, memory_modelt model, bool no_dependencies, goto_programt::const_targett target, @@ -117,16 +120,17 @@ void instrumentert::extract_events_rw( { const goto_programt::instructiont &instruction=*target; - rw_set_loct rw_set(ns, value_sets, target); + rw_range_set_dereft rw_set(ns, may_alias); + goto_rw(target, rw_set); /* Read (Rb) */ - forall_rw_set_r_entries(r_it, rw_set) + forall_rw_range_set_r_objects(r_it, rw_set) { /* creates Read: read is the irep_id of the read in the code; new_read_event is the corresponding abstract event; new_read_node is the node in the graph */ - const irep_idt& read=r_it->second.object; + const irep_idt& read=r_it->first; /* skip local variables */ if(local(read)) @@ -154,13 +158,13 @@ void instrumentert::extract_events_rw( } /* Write (Wa) */ - forall_rw_set_w_entries(w_it, rw_set) + forall_rw_range_set_w_objects(w_it, rw_set) { /* creates Write: write is the irep_id in the code; new_write_event is the corresponding abstract event; new_write_node is the node in the graph */ - const irep_idt& write = w_it->second.object; + const irep_idt& write = w_it->first; /* skip local variables */ if(local(write)) continue; @@ -191,11 +195,11 @@ void instrumentert::extract_events_rw( if(target->is_assign() && !no_dependencies) { - forall_rw_set_w_entries(write_it, rw_set) - forall_rw_set_r_entries(read_it, rw_set) + forall_rw_range_set_w_objects(write_it, rw_set) + forall_rw_range_set_r_objects(read_it, rw_set) { - const irep_idt& write=write_it->second.object; - const irep_idt& read=read_it->second.object; + const irep_idt& write=write_it->first; + const irep_idt& read=read_it->first; DEBUG_MESSAGE("dp: Write:"<second.object; - const irep_idt& read=read_it->second.object; + const irep_idt& read2=read2_it->first; + const irep_idt& read=read_it->first; if(read2==read) continue; const datat read_p(read,instruction.location); @@ -303,15 +307,15 @@ Function: instrumentert::extract_events \*******************************************************************/ void instrumentert::extract_events( - value_setst& value_sets, + may_aliast& may_alias, memory_modelt model, bool no_dependencies, - cfgt::entryt &cfg_entry) + cfgt::nodet &cfg_entry) { goto_programt::const_targett target=cfg_entry.PC; thread_eventst &dest=cfg_entry.events[thread]; - extract_events_rw(value_sets, model, no_dependencies, target, dest); + extract_events_rw(may_alias, model, no_dependencies, target, dest); extract_events_fence(model, target, dest); } @@ -328,18 +332,18 @@ Function: instrumentert::forward_traverse_once \*******************************************************************/ void instrumentert::forward_traverse_once( - value_setst& value_sets, + may_aliast &may_alias, memory_modelt model, bool no_dependencies, goto_programt::const_targett target) { - cfgt::entryt &cfg_entry=cfg.entry_map[target]; + cfgt::nodet &cfg_entry=cfg[cfg.entry_map[target]]; // we extract events only once per thread; this also means that // we do not track call stacks if(cfg_entry.events.find(thread)==cfg_entry.events.end()) extract_events( - value_sets, + may_alias, model, no_dependencies, cfg_entry); @@ -358,19 +362,19 @@ void instrumentert::forward_traverse_once( thread=++max_thread; assert(instruction.targets.size()==1); forward_traverse_once( - value_sets, + may_alias, model, no_dependencies, instruction.targets.front()); thread=coming_from; - assert(cfg_entry.successors.size()==1 && - cfg_entry.successors.front()->PC==next_PC); + assert(cfg_entry.out.size()==1 && + cfg[cfg_entry.out.begin()->first].PC==next_PC); } else if(instruction.is_end_thread()) { - assert(cfg_entry.successors.empty()); + assert(cfg_entry.out.empty()); } else if(instruction.is_function_call()) { @@ -378,19 +382,19 @@ void instrumentert::forward_traverse_once( const irep_idt& fun_id=to_symbol_expr(fun).get_identifier(); // do not enter recursion and skip __CPROVER_initialize - assert(cfg_entry.successors.size()==1); - if(cfg_entry.successors.front()->PC!=next_PC) + assert(cfg_entry.out.size()==1); + if(cfg[cfg_entry.out.begin()->first].PC!=next_PC) { if(fun_id!=CPROVER_PREFIX "initialize" && functions_met.insert(fun_id).second) forward_traverse_once( - value_sets, + may_alias, model, no_dependencies, - cfg_entry.successors.front()->PC); + cfg[cfg_entry.out.begin()->first].PC); forward_traverse_once( - value_sets, + may_alias, model, no_dependencies, next_PC); @@ -410,15 +414,15 @@ void instrumentert::forward_traverse_once( } else if(instruction.is_goto()) { - for(cfgt::entriest::const_iterator - it=cfg_entry.successors.begin(); - it!=cfg_entry.successors.end(); + for(cfgt::edgest::const_iterator + it=cfg_entry.out.begin(); + it!=cfg_entry.out.end(); ++it) { - const cfgt::entryt &succ_entry=cfg.entry_map[(*it)->PC]; + const cfgt::nodet &succ_entry=cfg[it->first]; if(succ_entry.events.find(thread)==succ_entry.events.end()) forward_traverse_once( - value_sets, + may_alias, model, no_dependencies, succ_entry.PC); @@ -427,19 +431,19 @@ void instrumentert::forward_traverse_once( return; } - if(cfg_entry.successors.empty()) + if(cfg_entry.out.empty()) { /* forward traversal done for this thread or branch */ return; } - assert(cfg_entry.successors.size()==1); + assert(cfg_entry.out.size()==1); forward_traverse_once( - value_sets, + may_alias, model, no_dependencies, - cfg_entry.successors.front()->PC); + cfg[cfg_entry.out.begin()->first].PC); } /*******************************************************************\ @@ -455,7 +459,7 @@ Function: instrumentert::forward_traverse_once \*******************************************************************/ void instrumentert::forward_traverse_once( - value_setst& value_sets, + may_aliast &may_alias, memory_modelt model, bool no_dependencies) { @@ -464,7 +468,7 @@ void instrumentert::forward_traverse_once( if(!goto_program.instructions.empty()) forward_traverse_once( - value_sets, + may_alias, model, no_dependencies, goto_program.instructions.begin()); @@ -490,7 +494,7 @@ void instrumentert::propagate_events_in_po() for(cfgt::entry_mapt::const_iterator it=cfg.entry_map.begin(); it!=cfg.entry_map.end(); ++it) - if(!it->second.events.empty()) + if(!cfg[it->second].events.empty()) worklist.push_back(it->first); while(!worklist.empty()) @@ -498,7 +502,7 @@ void instrumentert::propagate_events_in_po() goto_programt::const_targett target=worklist.back(); worklist.pop_back(); - cfgt::entryt &cfg_entry=cfg.entry_map[target]; + cfgt::nodet &cfg_entry=cfg[cfg.entry_map[target]]; // consistency checks first if(!cfg_entry.events.empty()) @@ -524,23 +528,23 @@ void instrumentert::propagate_events_in_po() { // no events at this instruction -- take the union of all events // propagated to predecessors - for(cfgt::entriest::const_iterator - it=cfg_entry.predecessors.begin(); - it!=cfg_entry.predecessors.end(); + for(cfgt::edgest::const_iterator + it=cfg_entry.in.begin(); + it!=cfg_entry.in.end(); ++it) { const std::set &s= - cfg.entry_map[(*it)->PC].use_events_from; + cfg[it->first].use_events_from; cfg_entry.use_events_from.insert(s.begin(), s.end()); } } if(cfg_entry.use_events_from.size()>size_before) - for(cfgt::entriest::const_iterator - it=cfg_entry.successors.begin(); - it!=cfg_entry.successors.end(); + for(cfgt::edgest::const_iterator + it=cfg_entry.out.begin(); + it!=cfg_entry.out.end(); ++it) - worklist.push_front((*it)->PC); + worklist.push_front(cfg[it->first].PC); } } @@ -596,8 +600,8 @@ Function: instrumentert::add_po_edges void instrumentert::add_po_edges( const unsigned thread_nr, - const cfgt::entryt &from, - const cfgt::entryt &to, + const cfgt::nodet &from, + const cfgt::nodet &to, const unsigned event_node, const unsigned event_gnode) { @@ -635,20 +639,20 @@ Function: instrumentert::add_po_edges \*******************************************************************/ void instrumentert::add_po_edges( - const cfgt::entryt &cfg_entry, + const cfgt::nodet &cfg_entry, const unsigned thread_nr, const unsigned event_node) { assert(map_vertex_gnode.find(event_node)!=map_vertex_gnode.end()); const unsigned event_gnode=map_vertex_gnode[event_node]; - for(cfgt::entriest::const_iterator - it=cfg_entry.predecessors.begin(); - it!=cfg_entry.predecessors.end(); + for(cfgt::edgest::const_iterator + it=cfg_entry.in.begin(); + it!=cfg_entry.in.end(); ++it) { const std::set &s= - cfg.entry_map[(*it)->PC].use_events_from; + cfg[it->first].use_events_from; for(std::set::const_iterator s_it=s.begin(); @@ -658,7 +662,7 @@ void instrumentert::add_po_edges( if(*s_it!=cfg_entry.PC) add_po_edges( thread_nr, - cfg.entry_map[*s_it], + cfg[cfg.entry_map[*s_it]], cfg_entry, event_node, event_gnode); @@ -678,7 +682,7 @@ Function: instrumentert::add_po_edges \*******************************************************************/ void instrumentert::add_po_edges( - const cfgt::entryt &cfg_entry, + const cfgt::nodet &cfg_entry, const unsigned thread_nr, const thread_eventst &thread_events) { @@ -717,7 +721,7 @@ Function: instrumentert::add_edges_assign \*******************************************************************/ void instrumentert::add_edges_assign( - const cfgt::entryt &cfg_entry, + const cfgt::nodet &cfg_entry, const thread_eventst &thread_events) { // anything other than an assignment or a function call containing @@ -764,7 +768,7 @@ Function: instrumentert::add_com_edges \*******************************************************************/ void instrumentert::add_com_edges( - const cfgt::entryt &cfg_entry, + const cfgt::nodet &cfg_entry, const thread_eventst &thread_events) { /* Read (Rb) */ @@ -882,7 +886,7 @@ Function: instrumentert::add_edges \*******************************************************************/ void instrumentert::add_edges( - const cfgt::entryt &cfg_entry, + const cfgt::nodet &cfg_entry, const unsigned thread_nr, const thread_eventst &thread_events) { @@ -918,11 +922,15 @@ void instrumentert::add_edges() for(cfgt::entry_mapt::const_iterator it=cfg.entry_map.begin(); it!=cfg.entry_map.end(); ++it) + { + const cfgt::nodet &n=cfg[it->second]; + for(std::map::const_iterator - t_it=it->second.events.begin(); - t_it!=it->second.events.end(); + t_it=n.events.begin(); + t_it!=n.events.end(); ++t_it) - add_edges(it->second, t_it->first, t_it->second); + add_edges(n, t_it->first, t_it->second); + } } /*******************************************************************\ @@ -940,7 +948,7 @@ Function: instrumentert::build_event_graph \*******************************************************************/ unsigned instrumentert::build_event_graph( - value_setst& value_sets, + may_aliast& may_alias, memory_modelt model, bool no_dependencies) { @@ -950,7 +958,7 @@ unsigned instrumentert::build_event_graph( cfg(goto_functions); forward_traverse_once( - value_sets, + may_alias, model, no_dependencies); diff --git a/src/goto-instrument/wmm/goto2graph.h b/src/goto-instrument/wmm/goto2graph.h index 4a0cd0e..ca3314d 100644 --- a/src/goto-instrument/wmm/goto2graph.h +++ b/src/goto-instrument/wmm/goto2graph.h @@ -24,7 +24,7 @@ Date: 2012 class symbol_tablet; class goto_functionst; -class value_setst; +class may_aliast; class instrumentert { @@ -121,7 +121,7 @@ protected: /* transformers */ void extract_events_rw( - value_setst& value_sets, + may_aliast& may_alias, memory_modelt model, bool no_dependencies, goto_programt::const_targett target, @@ -131,10 +131,10 @@ protected: goto_programt::const_targett target, thread_eventst &dest); void extract_events( - value_setst& value_sets, + may_aliast& may_alias, memory_modelt model, bool no_dependencies, - cfgt::entryt &cfg_entry); + cfgt::nodet &cfg_entry); void add_po_edges( const nodest &from_events, @@ -143,26 +143,26 @@ protected: const bool is_backward); void add_po_edges( const unsigned thread_nr, - const cfgt::entryt &from, - const cfgt::entryt &to, + const cfgt::nodet &from, + const cfgt::nodet &to, const unsigned event_node, const unsigned event_gnode); void add_po_edges( - const cfgt::entryt &cfg_entry, + const cfgt::nodet &cfg_entry, const unsigned thread_nr, const unsigned event_node); void add_po_edges( - const cfgt::entryt &cfg_entry, + const cfgt::nodet &cfg_entry, const unsigned thread_nr, const thread_eventst &thread_events); void add_edges_assign( - const cfgt::entryt &cfg_entry, + const cfgt::nodet &cfg_entry, const thread_eventst &thread_events); void add_com_edges( - const cfgt::entryt &cfg_entry, + const cfgt::nodet &cfg_entry, const thread_eventst &thread_events); void add_edges( - const cfgt::entryt &cfg_entry, + const cfgt::nodet &cfg_entry, const unsigned thread_nr, const thread_eventst &thread_events); @@ -204,12 +204,12 @@ public: unsigned read_counter; void forward_traverse_once( - value_setst& value_sets, + may_aliast &may_alias, memory_modelt model, bool no_dependencies, goto_programt::const_targett target); void forward_traverse_once( - value_setst& value_sets, + may_aliast &may_alias, memory_modelt model, bool no_dependencies); @@ -218,7 +218,7 @@ public: void add_edges(); unsigned build_event_graph( - value_setst& value_sets, + may_aliast& may_alias, memory_modelt model, bool no_dependencies); diff --git a/src/goto-instrument/wmm/static_cycles.cpp b/src/goto-instrument/wmm/static_cycles.cpp new file mode 100644 index 0000000..11c97bb --- /dev/null +++ b/src/goto-instrument/wmm/static_cycles.cpp @@ -0,0 +1,707 @@ +/*******************************************************************\ + +Module: Find cycles even when no entry function is known + +Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk + +\*******************************************************************/ + +#include +#include + +#include +#include +#include + +#include +#include +#include +#include + +#include +#include +#include + +#include "goto2graph.h" + +#include "static_cycles.h" + +typedef hash_set_cont thread_functionst; + +/*******************************************************************\ + +Function: add_thread + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static void add_thread( + const goto_functionst& goto_functions, + const irep_idt &identifier, + thread_functionst &thread_functions) +{ + goto_functionst::function_mapt::const_iterator fn= + goto_functions.function_map.find(identifier); + + if(fn!=goto_functions.function_map.end() && + !fn->second.body.instructions.empty()) + thread_functions.insert(identifier); + else + thread_functions.insert(ID_main); +} + +/*******************************************************************\ + +Function: find_thread_start_thread + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static void find_thread_start_thread( + goto_programt::const_targett start_thread, + const goto_programt &goto_program, + const goto_functionst& goto_functions, + thread_functionst &thread_functions) +{ + assert(start_thread->targets.size()==1); + + add_thread( + goto_functions, + start_thread->function, + thread_functions); + + for(goto_programt::const_targett + target=start_thread->targets.front(); + target!=goto_program.instructions.end() && + !target->is_end_thread() && + !target->is_end_function(); + ++target) + { + if(!target->is_function_call()) + continue; + + const code_function_callt &call=to_code_function_call(target->code); + if(call.function().id()!=ID_symbol) + continue; + + const irep_idt &f_name= + to_symbol_expr(call.function()).get_identifier(); + add_thread(goto_functions, f_name, thread_functions); + } +} + +/*******************************************************************\ + +Function: get_function_symbols + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static void get_function_symbols( + symbol_tablet &symbol_table, + const goto_functionst& goto_functions, + const exprt &fn_ptr, + const exprt &arg, + std::set &functions) +{ + if(fn_ptr.id()==ID_typecast) + { + get_function_symbols( + symbol_table, + goto_functions, + to_typecast_expr(fn_ptr).op(), + arg, + functions); + } + else if(fn_ptr.id()==ID_if) + { + const if_exprt &fn_ptr_if=to_if_expr(fn_ptr); + + get_function_symbols( + symbol_table, + goto_functions, + fn_ptr_if.true_case(), + arg, + functions); + get_function_symbols( + symbol_table, + goto_functions, + fn_ptr_if.false_case(), + arg, + functions); + } + else if(fn_ptr.id()==ID_symbol || + fn_ptr.id()==ID_member || + fn_ptr.id()==ID_index) + { + assert(fn_ptr.type().id()==ID_pointer); + + code_function_callt c; + c.function()=dereference_exprt(fn_ptr, fn_ptr.type().subtype()); + c.arguments().push_back(arg); + + goto_programt tmp; + + goto_programt::targett f=tmp.add_instruction(FUNCTION_CALL); + f->code=c; + + tmp.add_instruction(END_FUNCTION); + + remove_function_pointers(symbol_table, goto_functions, tmp, false); + + forall_goto_program_instructions(it, tmp) + if(it->is_function_call()) + { + const code_function_callt &code= + to_code_function_call(it->code); + + functions.insert(to_symbol_expr(code.function())); + } + } + else + { + const address_of_exprt &address_of=to_address_of_expr(fn_ptr); + + functions.insert(to_symbol_expr(address_of.object())); + } +} + +/*******************************************************************\ + +Function: find_thread_function_call + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static void find_thread_function_call( + symbol_tablet &symbol_table, + const goto_programt::instructiont &function_call, + const goto_functionst& goto_functions, + thread_functionst &thread_functions) +{ + const code_function_callt &call= + to_code_function_call(function_call.code); + + if(call.function().id()!=ID_symbol) + return; + + // pthread_create or kthread_create_on_node + const irep_idt &f_name= + to_symbol_expr(call.function()).get_identifier(); + const code_function_callt::argumentst &args=call.arguments(); + + exprt thread_fn_ptr; + exprt arg; + + if(f_name=="c::pthread_create") + { + assert(args.size()==4); + thread_fn_ptr=args[2]; + arg=args[3]; + } + else if(f_name=="c::kthread_create_on_node") + { + assert(args.size()>=4); + thread_fn_ptr=args.front(); + arg=args[1]; + } + else + return; + + std::set functions; + get_function_symbols( + symbol_table, + goto_functions, + thread_fn_ptr, + arg, + functions); + + for(std::set::const_iterator it=functions.begin(); + it!=functions.end(); + ++it) + { + add_thread( + goto_functions, + it->get_identifier(), + thread_functions); + } + + add_thread( + goto_functions, + function_call.function, + thread_functions); +} + +/*******************************************************************\ + +Function: find_threads + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static void find_threads( + symbol_tablet &symbol_table, + const goto_programt &goto_program, + const goto_functionst& goto_functions, + thread_functionst &thread_functions) +{ + forall_goto_program_instructions(it, goto_program) + if(it->is_start_thread()) + find_thread_start_thread( + it, + goto_program, + goto_functions, + thread_functions); + else if(it->is_function_call()) + find_thread_function_call( + symbol_table, + *it, + goto_functions, + thread_functions); +} + +/*******************************************************************\ + +Function: find_threads + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static void find_threads( + symbol_tablet &symbol_table, + const goto_functionst& goto_functions, + thread_functionst &thread_functions) +{ + forall_goto_functions(f_it, goto_functions) + if(f_it->first!="c::pthread_create" && + f_it->first!="c::kthread_create_on_node") + find_threads( + symbol_table, + f_it->second.body, + goto_functions, + thread_functions); +} + +/*******************************************************************\ + +Function: filter_thread_functions + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static void filter_thread_functions( + const goto_functionst& goto_functions, + const call_grapht &call_map, + thread_functionst &thread_functions) +{ + graph > call_graph; + + hash_map_cont fn_to_node; + for(thread_functionst::const_iterator it=thread_functions.begin(); + it!=thread_functions.end(); + ++it) + { + unsigned n=call_graph.add_node(); + fn_to_node.insert(std::make_pair(*it, n)); + } + + for(std::multimap::const_iterator + it=call_map.graph.begin(); + it!=call_map.graph.end(); + ++it) + { + if(fn_to_node.find(it->first)==fn_to_node.end()) + fn_to_node.insert(std::make_pair(it->first, call_graph.add_node())); + if(fn_to_node.find(it->second)==fn_to_node.end()) + fn_to_node.insert(std::make_pair(it->second, call_graph.add_node())); + + call_graph.add_edge( + fn_to_node[it->first], + fn_to_node[it->second]); + } + + thread_functionst before; + before.swap(thread_functions); + + for(thread_functionst::const_iterator it=before.begin(); + it!=before.end(); + ++it) + { + const irep_idt &identifier=*it; + const unsigned n=fn_to_node[identifier]; + + if(call_graph[n].visited) + continue; + + if(call_graph.in(n).empty()) + { + add_thread( + goto_functions, + identifier, + thread_functions); + call_graph.visit_reachable(n); + continue; + } + + graph >::patht path; + call_graph.shortest_loop(n, path); + if(!path.empty()) + { + add_thread( + goto_functions, + identifier, + thread_functions); + call_graph.visit_reachable(n); + } + } + + std::cout << "Thread entry candidates:" << std::endl; + for(thread_functionst::const_iterator it=thread_functions.begin(); + it!=thread_functions.end(); + ++it) + std::cout << *it << std::endl; +} + +/*******************************************************************\ + +Function: collect_cycles_in_group + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static void collect_cycles_in_group( + may_aliast &may_alias, + symbol_tablet &symbol_table, + goto_functionst& goto_functions, + const irep_idt &identifier) +{ + const namespacet ns(symbol_table); + instrumentert instrumenter(symbol_table, goto_functions); + + fine_timet graph_time_start=current_time(); + { + instrumenter.cfg(goto_functions); + + goto_functionst::function_mapt::const_iterator fn= + goto_functions.function_map.find(identifier); + assert(fn!=goto_functions.function_map.end() && + !fn->second.body.instructions.empty()); + instrumenter.forward_traverse_once( + may_alias, + Static_Weak, + false, + fn->second.body.instructions.begin()); + + instrumenter.propagate_events_in_po(); + + instrumenter.add_edges(); + } + std::cout << "Time event graph construction: " + << current_time()-graph_time_start << std::endl; + + std::cout << "Number of reads: " << instrumenter.read_counter <::const_iterator + it=instrumenter.set_of_cycles.begin(); + it!=instrumenter.set_of_cycles.end(); + ++it) + { + std::cout << "Source: " << it->print_output() << std::endl; + std::cout << "Cycle:" << it->print_name(Static_Weak, false) << std::endl; + } +} + +/*******************************************************************\ + +Function: form_thread_groups + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +static void form_thread_groups( + symbol_tablet &symbol_table, + goto_functionst& goto_functions, + thread_functionst &thread_functions, + may_aliast &may_alias) +{ + forall_goto_functions(it, goto_functions) + add_thread(goto_functions, it->first, thread_functions); + + call_grapht call_map(goto_functions); + + filter_thread_functions(goto_functions, call_map, thread_functions); + + const namespacet ns(symbol_table); + + typedef std::list, thread_functionst> > + thread_groupst; + thread_groupst thread_groups; + + for(thread_functionst::const_iterator it=thread_functions.begin(); + it!=thread_functions.end(); + ++it) + { + const irep_idt &root_fn=*it; + + hash_set_cont called_funcs; + called_funcs.insert(root_fn); + + std::list wl; + wl.push_back(root_fn); + + while(!wl.empty()) + { + irep_idt caller=wl.back(); + wl.pop_back(); + + std::pair::const_iterator, + std::multimap::const_iterator> + eq_iterators=call_map.graph.equal_range(caller); + for( ; + eq_iterators.first!=eq_iterators.second; + ++(eq_iterators.first)) + if(called_funcs.insert(eq_iterators.first->second).second) + wl.push_back(eq_iterators.first->second); + } + + thread_groups.push_back(std::make_pair( + std::set(), + thread_functionst())); + std::set &rw_symbols=thread_groups.back().first; + thread_groups.back().second.insert(root_fn); + + for(hash_set_cont::const_iterator + c_it=called_funcs.begin(); + c_it!=called_funcs.end(); + ++c_it) + { + goto_functionst::function_mapt::const_iterator fn= + goto_functions.function_map.find(*c_it); + + if(fn==goto_functions.function_map.end() || + fn->second.body.instructions.empty()) + continue; + + const goto_programt &goto_program=fn->second.body; + + rw_range_set_dereft rw_set(ns, may_alias); + goto_rw(goto_program, rw_set); + + forall_rw_range_set_w_objects(w_it, rw_set) + { + const irep_idt &identifier=w_it->first; + if(!symbol_table.has_symbol(identifier) || + !ns.lookup(identifier).is_shared()) + continue; + + rw_symbols.insert(identifier); + } + + forall_rw_range_set_r_objects(r_it, rw_set) + { + const irep_idt &identifier=r_it->first; + if(!symbol_table.has_symbol(identifier) || + !ns.lookup(identifier).is_shared()) + continue; + + rw_symbols.insert(identifier); + } + } + } + + for(thread_groupst::iterator it1=thread_groups.begin(); + it1!=thread_groups.end(); + ) // no ++it1 + { + bool merged=it1->first.empty(); + for(thread_groupst::iterator next=it1, it2=++next; + it2!=thread_groups.end() && !merged; + ++it2) + { + std::list intersection; + std::set_intersection( + it1->first.begin(), it1->first.end(), + it2->first.begin(), it2->first.end(), + std::back_inserter(intersection)); + + if(intersection.empty()) + continue; + + std::copy(it1->first.begin(), it1->first.end(), + std::inserter(it2->first, it2->first.begin())); + it2->second.insert(it1->second.begin(), it1->second.end()); + merged=true; + } + + if(merged || + (it1->second.size()==1 && it1->first.empty())) + thread_groups.erase(it1++); + else + ++it1; + } + + if(thread_groups.empty()) + { + std::cout << "No thread groups" << std::endl; + return; + } + + assert(goto_functions.function_map.find("$$thread_dummy")== + goto_functions.function_map.end()); + goto_functionst::goto_functiont &thread_dummy= + goto_functions.function_map["$$thread_dummy"]; + thread_dummy.type=code_typet(); + thread_dummy.body_available=true; + goto_programt &body=thread_dummy.body; + + for(thread_groupst::const_iterator it=thread_groups.begin(); + it!=thread_groups.end(); + ++it) + { + std::cout << "Thread group:" << std::endl; + + body.clear(); + + null_message_handlert mh; + + code_function_callt f; + f.lhs().make_nil(); + + for(thread_functionst::const_iterator + t_it=it->second.begin(); + t_it!=it->second.end(); + ++t_it) + { + const irep_idt identifier=*t_it; + std::cout << identifier << std::endl; + + f.function()=symbol_exprt(identifier, code_typet()); + const code_labelt label("__CPROVER_ASYNC_0", f); + + // add 3 threads executing this function + for(int i=0; i<3; ++i) + goto_convert(label, symbol_table, body, mh); + } + + body.add_instruction(END_FUNCTION); + body.compute_target_numbers(); + remove_skip(body); + body.update(); + + collect_cycles_in_group( + may_alias, + symbol_table, + goto_functions, + "$$thread_dummy"); + } +} + +/*******************************************************************\ + +Function: static_cycles + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +void static_cycles( + symbol_tablet &symbol_table, + goto_functionst& goto_functions) +{ + fine_timet total_time_start=current_time(); + + hash_set_cont thread_functions; + find_threads(symbol_table, goto_functions, thread_functions); + + bool is_linked= + goto_functions.function_map.find(ID_main) + !=goto_functions.function_map.end(); + + if(is_linked && + thread_functions.empty()) + { + std::cout << "No thread spawn found in linked binary" << std::endl; + return; + } + + const namespacet ns(symbol_table); + fine_timet alias_time_start=current_time(); + may_aliast may_alias(goto_functions, ns); + std::cout << "Time alias analysis: " + << current_time()-alias_time_start << std::endl; + + if(!is_linked) + form_thread_groups( + symbol_table, + goto_functions, + thread_functions, + may_alias); + else + collect_cycles_in_group( + may_alias, + symbol_table, + goto_functions, + ID_main); + + std::cout << "Time static cycle search: " + << current_time()-total_time_start << std::endl; +} + diff --git a/src/goto-instrument/wmm/static_cycles.h b/src/goto-instrument/wmm/static_cycles.h new file mode 100644 index 0000000..866789a --- /dev/null +++ b/src/goto-instrument/wmm/static_cycles.h @@ -0,0 +1,20 @@ +/*******************************************************************\ + +Module: Find cycles even when no entry function is known + +Author: Michael Tautschnig, michael.tautschnig@cs.ox.ac.uk + +\*******************************************************************/ + +#ifndef CPROVER_STATIC_CYCLES_H +#define CPROVER_STATIC_CYCLES_H + +class symbol_tablet; +class goto_functionst; + +void static_cycles( + symbol_tablet& symbol_table, + goto_functionst& goto_functions); + +#endif + diff --git a/src/goto-instrument/wmm/weak_memory.cpp b/src/goto-instrument/wmm/weak_memory.cpp index 31d7e54..3639e5f 100644 --- a/src/goto-instrument/wmm/weak_memory.cpp +++ b/src/goto-instrument/wmm/weak_memory.cpp @@ -25,6 +25,8 @@ Date: September 2011 #include +#include + #include "../rw_set.h" #include "weak_memory.h" #include "goto2graph.h" @@ -1976,7 +1978,9 @@ void weak_memory( unsigned max_thds = 0; instrumentert instrumenter(symbol_table, goto_functions); - max_thds=instrumenter.build_event_graph(value_sets, model, no_dependencies); + const namespacet ns(symbol_table); + may_aliast may_alias(goto_functions, ns); + max_thds=instrumenter.build_event_graph(may_alias, model, no_dependencies); std::cout<<"abstraction completed"< +#include #include "goto_functions.h" @@ -21,42 +22,109 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ -template -class cfg_baset +class empty_cfg_nodet +{ +}; + +// these are the CFG nodes +template +struct cfg_base_nodet:public graph_nodet, public T +{ + typedef typename graph_nodet::edget edget; + typedef typename graph_nodet::edgest edgest; + + I PC; +}; + +template +class cfg_baset:public graph< cfg_base_nodet > { public: - // these are the CFG nodes - struct entryt: public T + typedef unsigned entryt; + + struct entry_mapt: + public std::map { - typedef std::list entriest; + graph< cfg_base_nodet > & container; - // we have edges both ways - entriest successors, predecessors; - goto_programt::const_targett PC; - }; - - typedef entryt * iterator; - typedef const entryt * const_iterator; + explicit entry_mapt(graph< cfg_base_nodet > & _container): + container(_container) + { + } - typedef std::list entriest; - - typedef std::map entry_mapt; + entryt& operator[](const goto_programt::const_targett &t) + { + std::pair e=insert(std::make_pair(t, 0)); + + if(e.second) + e.first->second=container.add_node(); + + return e.first->second; + } + }; entry_mapt entry_map; protected: + virtual void compute_edges_goto( + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + entryt &entry); + + virtual void compute_edges_catch( + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + entryt &entry); + + virtual void compute_edges_throw( + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + entryt &entry); + + virtual void compute_edges_start_thread( + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + entryt &entry); + + virtual void compute_edges_function_call( + const goto_functionst &goto_functions, + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + entryt &entry); + + virtual void compute_edges_return( + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + entryt &entry); + void compute_edges( const goto_functionst &goto_functions, const goto_programt &goto_program, - goto_programt::const_targett PC); + I PC); void compute_edges( const goto_functionst &goto_functions, - const goto_programt &goto_program); + P &goto_program); void compute_edges( const goto_functionst &goto_functions); public: + cfg_baset():entry_map(*this) + { + } + + virtual ~cfg_baset() + { + } + void operator()( const goto_functionst &goto_functions) { @@ -64,7 +132,7 @@ public: } void operator()( - const goto_programt &goto_program) + P &goto_program) { goto_functionst goto_functions; compute_edges(goto_functions, goto_program); @@ -74,7 +142,67 @@ public: /*******************************************************************\ -Function: cfg_baset::compute_edges + Class: concurrent_cfg_baset + + Purpose: + +\*******************************************************************/ + +template +class concurrent_cfg_baset:public virtual cfg_baset +{ +protected: + virtual void compute_edges_start_thread( + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + typename cfg_baset::entryt &entry); +}; + +/*******************************************************************\ + + Class: procedure_local_cfg_baset + + Purpose: + +\*******************************************************************/ + +template +class procedure_local_cfg_baset:public virtual cfg_baset +{ +protected: + virtual void compute_edges_function_call( + const goto_functionst &goto_functions, + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + typename cfg_baset::entryt &entry); +}; + +/*******************************************************************\ + + Class: procedure_local_concurrent_cfg_baset + + Purpose: + +\*******************************************************************/ + +template +class procedure_local_concurrent_cfg_baset: + public concurrent_cfg_baset, + public procedure_local_cfg_baset +{ +}; + +/*******************************************************************\ + +Function: cfg_baset::compute_edges_goto Inputs: @@ -84,139 +212,340 @@ Function: cfg_baset::compute_edges \*******************************************************************/ -template -void cfg_baset::compute_edges( - const goto_functionst &goto_functions, +template +void cfg_baset::compute_edges_goto( const goto_programt &goto_program, - goto_programt::const_targett PC) + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + entryt &entry) { - const goto_programt::instructiont &instruction=*PC; - entryt &entry=entry_map[PC]; - entry.PC=PC; - goto_programt::const_targett next_PC(PC); - next_PC++; - - // compute forward edges first - if(instruction.is_goto()) + if(next_PC!=goto_program.instructions.end() && + !instruction.guard.is_true()) + this->add_edge(entry, entry_map[next_PC]); + + for(goto_programt::instructiont::targetst::const_iterator + t_it=instruction.targets.begin(); + t_it!=instruction.targets.end(); + t_it++) { - if(next_PC!=goto_program.instructions.end() && - !instruction.guard.is_true()) - entry.successors.push_back(&entry_map[next_PC]); - - for(goto_programt::instructiont::targetst::const_iterator - t_it=instruction.targets.begin(); - t_it!=instruction.targets.end(); - t_it++) - { - goto_programt::const_targett t=*t_it; - if(t!=goto_program.instructions.end()) - entry.successors.push_back(&entry_map[t]); - } + goto_programt::const_targett t=*t_it; + if(t!=goto_program.instructions.end()) + this->add_edge(entry, entry_map[t]); } - else if(instruction.is_catch()) - { - if(next_PC!=goto_program.instructions.end()) - entry.successors.push_back(&entry_map[next_PC]); +} - // Not ideal, but preserves targets - // Ideally, the throw statements should have those as successors +/*******************************************************************\ - for(goto_programt::instructiont::targetst::const_iterator - t_it=instruction.targets.begin(); - t_it!=instruction.targets.end(); - t_it++) - { - goto_programt::const_targett t=*t_it; - if(t!=goto_program.instructions.end()) - entry.successors.push_back(&entry_map[t]); - } - } - else if(instruction.is_throw()) +Function: cfg_baset::compute_edges_catch + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +template +void cfg_baset::compute_edges_catch( + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + entryt &entry) +{ + if(next_PC!=goto_program.instructions.end()) + this->add_edge(entry, entry_map[next_PC]); + + // Not ideal, but preserves targets + // Ideally, the throw statements should have those as successors + + for(goto_programt::instructiont::targetst::const_iterator + t_it=instruction.targets.begin(); + t_it!=instruction.targets.end(); + t_it++) { - // no (trivial) successors + goto_programt::const_targett t=*t_it; + if(t!=goto_program.instructions.end()) + this->add_edge(entry, entry_map[t]); } - else if(instruction.is_start_thread()) +} + +/*******************************************************************\ + +Function: cfg_baset::compute_edges_throw + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +template +void cfg_baset::compute_edges_throw( + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + entryt &entry) +{ + // no (trivial) successors +} + +/*******************************************************************\ + +Function: cfg_baset::compute_edges_start_thread + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +template +void cfg_baset::compute_edges_start_thread( + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + entryt &entry) +{ + if(next_PC!=goto_program.instructions.end()) + this->add_edge(entry, entry_map[next_PC]); +} + +/*******************************************************************\ + +Function: concurrent_cfg_baset::compute_edges_start_thread + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +template +void concurrent_cfg_baset::compute_edges_start_thread( + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + typename cfg_baset::entryt &entry) +{ + cfg_baset::compute_edges_start_thread( + goto_program, + instruction, + next_PC, + entry); + + for(goto_programt::instructiont::targetst::const_iterator + t_it=instruction.targets.begin(); + t_it!=instruction.targets.end(); + t_it++) { - if(next_PC!=goto_program.instructions.end()) - entry.successors.push_back(&entry_map[PC]); - - for(goto_programt::instructiont::targetst::const_iterator - t_it=instruction.targets.begin(); - t_it!=instruction.targets.end(); - t_it++) - { - goto_programt::const_targett t=*t_it; - if(t!=goto_program.instructions.end()) - entry.successors.push_back(&entry_map[t]); - } + goto_programt::const_targett t=*t_it; + if(t!=goto_program.instructions.end()) + this->add_edge(entry, this->entry_map[t]); } - else if(instruction.is_function_call()) +} + +/*******************************************************************\ + +Function: cfg_baset::compute_edges_function_call + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +template +void cfg_baset::compute_edges_function_call( + const goto_functionst &goto_functions, + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + entryt &entry) +{ + const exprt &function= + to_code_function_call(instruction.code).function(); + + if(function.id()!=ID_symbol) + return; + + const irep_idt &identifier= + to_symbol_expr(function).get_identifier(); + + goto_functionst::function_mapt::const_iterator f_it= + goto_functions.function_map.find(identifier); + + if(f_it!=goto_functions.function_map.end() && + f_it->second.body_available) { - const exprt &function= - to_code_function_call(instruction.code).function(); + // get the first instruction + goto_programt::const_targett i_it= + f_it->second.body.instructions.begin(); - if(function.id()==ID_symbol) + goto_programt::const_targett e_it= + f_it->second.body.instructions.end(); + + goto_programt::const_targett last_it=e_it; last_it--; + + if(i_it!=e_it) { - const irep_idt &identifier= - to_symbol_expr(function).get_identifier(); - - goto_functionst::function_mapt::const_iterator f_it= - goto_functions.function_map.find(identifier); - - if(f_it!=goto_functions.function_map.end() && - f_it->second.body_available) - { - // get the first instruction - goto_programt::const_targett i_it= - f_it->second.body.instructions.begin(); - - goto_programt::const_targett e_it= - f_it->second.body.instructions.end(); - - goto_programt::const_targett last_it=e_it; last_it--; - - if(i_it!=e_it) - { - // nonempty function - entry.successors.push_back(&entry_map[i_it]); - - // add the last instruction as predecessor of the return location - if(next_PC!=goto_program.instructions.end()) - { - entry_map[last_it].successors.push_back(&entry_map[next_PC]); - entry_map[next_PC].predecessors.push_back(&entry_map[last_it]); - } - } - else if(next_PC!=goto_program.instructions.end()) - { - // empty function - entry.successors.push_back(&entry_map[next_PC]); - } - } - else if(next_PC!=goto_program.instructions.end()) - entry.successors.push_back(&entry_map[next_PC]); + // nonempty function + this->add_edge(entry, entry_map[i_it]); + + // add the last instruction as predecessor of the return location + if(next_PC!=goto_program.instructions.end()) + this->add_edge(entry_map[last_it], entry_map[next_PC]); } + else if(next_PC!=goto_program.instructions.end()) + { + // empty function + this->add_edge(entry, entry_map[next_PC]); + } } - else if(instruction.is_return()) - { - // the successor of return is the last instruction of the function, - // normally END_FUNCTION - if(next_PC!=goto_program.instructions.end()) - entry.successors.push_back(&entry_map[--(goto_program.instructions.end())]); - } - else - { - if(next_PC!=goto_program.instructions.end()) - entry.successors.push_back(&entry_map[next_PC]); - } + else if(next_PC!=goto_program.instructions.end()) + this->add_edge(entry, entry_map[next_PC]); +} + +/*******************************************************************\ + +Function: procedure_local_cfg_baset::compute_edges_function_call + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +template +void procedure_local_cfg_baset::compute_edges_function_call( + const goto_functionst &goto_functions, + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + typename cfg_baset::entryt &entry) +{ + const exprt &function= + to_code_function_call(instruction.code).function(); + + if(function.id()!=ID_symbol) + return; + + if(next_PC!=goto_program.instructions.end()) + this->add_edge(entry, this->entry_map[next_PC]); +} + +/*******************************************************************\ + +Function: cfg_baset::compute_edges_return + + Inputs: + + Outputs: - // now do backward edges - for(typename entriest::const_iterator - s_it=entry.successors.begin(); - s_it!=entry.successors.end(); - s_it++) + Purpose: + +\*******************************************************************/ + +template +void cfg_baset::compute_edges_return( + const goto_programt &goto_program, + const goto_programt::instructiont &instruction, + goto_programt::const_targett next_PC, + entryt &entry) +{ + // the successor of return is the last instruction of the function, + // normally END_FUNCTION + if(next_PC!=goto_program.instructions.end()) + this->add_edge(entry, entry_map[--(goto_program.instructions.end())]); +} + +/*******************************************************************\ + +Function: cfg_baset::compute_edges + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +template +void cfg_baset::compute_edges( + const goto_functionst &goto_functions, + const goto_programt &goto_program, + I PC) +{ + const goto_programt::instructiont &instruction=*PC; + entryt entry=entry_map[PC]; + (*this)[entry].PC=PC; + goto_programt::const_targett next_PC(PC); + next_PC++; + + // compute forward edges first + switch(instruction.type) { - (*s_it)->predecessors.push_back(&entry); + case GOTO: + compute_edges_goto(goto_program, instruction, next_PC, entry); + break; + case CATCH: + compute_edges_catch(goto_program, instruction, next_PC, entry); + break; + case THROW: + compute_edges_throw(goto_program, instruction, next_PC, entry); + break; + case START_THREAD: + compute_edges_start_thread( + goto_program, + instruction, + next_PC, + entry); + break; + case FUNCTION_CALL: + compute_edges_function_call( + goto_functions, + goto_program, + instruction, + next_PC, + entry); + break; + case RETURN: + compute_edges_return(goto_program, instruction, next_PC, entry); + break; + case END_THREAD: + case END_FUNCTION: + // no successor + break; + case ASSUME: + // false guard -> no successor + if(instruction.guard.is_false()) + break; + case ASSIGN: + case ASSERT: + case OTHER: + case SKIP: + case LOCATION: + case ATOMIC_BEGIN: + case ATOMIC_END: + case DECL: + case DEAD: + if(next_PC!=goto_program.instructions.end()) + this->add_edge(entry, entry_map[next_PC]); + break; + case NO_INSTRUCTION_TYPE: + assert(false); + break; } } @@ -232,12 +561,14 @@ Function: cfg_baset::compute_edges \*******************************************************************/ -template -void cfg_baset::compute_edges( +template +void cfg_baset::compute_edges( const goto_functionst &goto_functions, - const goto_programt &goto_program) + P &goto_program) { - forall_goto_program_instructions(it, goto_program) + for(I it=goto_program.instructions.begin(); + it!=goto_program.instructions.end(); + ++it) compute_edges(goto_functions, goto_program, it); } @@ -253,8 +584,8 @@ Function: cfg_baset::compute_edges \*******************************************************************/ -template -void cfg_baset::compute_edges( +template +void cfg_baset::compute_edges( const goto_functionst &goto_functions) { forall_goto_functions(it, goto_functions) diff --git a/src/goto-programs/goto_rw.cpp b/src/goto-programs/goto_rw.cpp deleted file mode 100644 index 702c17f..0000000 --- a/src/goto-programs/goto_rw.cpp +++ /dev/null @@ -1,198 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening - -Date: April 2010 - -\*******************************************************************/ - -#include - -#include "goto_rw.h" - -/*******************************************************************\ - -Function: get_objects_rec - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -typedef enum { LHS_W, READ } get_modet; - -void get_objects_rec( - get_modet mode, - const exprt &expr, - std::list &read, - std::list &write) -{ - if(expr.id()==ID_symbol) - { - if(mode==LHS_W) - write.push_back(expr); - else - read.push_back(expr); - } - else if(expr.id()==ID_index) - { - const index_exprt &index_expr=to_index_expr(expr); - - if(mode==READ) - get_objects_rec(READ, index_expr.index(), read, write); - - get_objects_rec(mode, index_expr.array(), read, write); - } - else if(expr.id()==ID_if) - { - const if_exprt &if_expr=to_if_expr(expr); - - if(mode==READ) - get_objects_rec(READ, if_expr.cond(), read, write); - - get_objects_rec(mode, if_expr.true_case(), read, write); - get_objects_rec(mode, if_expr.false_case(), read, write); - } - else if(expr.id()==ID_member) - { - const member_exprt &member_expr=to_member_expr(expr); - - get_objects_rec(mode, member_expr.struct_op(), read, write); - } - else if(expr.id()==ID_dereference) - { - const dereference_exprt &dereference_expr= - to_dereference_expr(expr); - - if(mode==READ) - get_objects_rec(READ, dereference_expr.pointer(), read, write); - - if(mode==LHS_W) - write.push_back(expr); - else - read.push_back(expr); - } - else - { - if(mode==READ) - forall_operands(it, expr) - get_objects_rec(READ, *it, read, write); - } -} - -/*******************************************************************\ - -Function: goto_rw - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void goto_rw(const code_assignt &assign, - std::list &read, std::list &write) -{ - get_objects_rec(LHS_W, assign.lhs(), read, write); - get_objects_rec(READ, assign.rhs(), read, write); -} - -/*******************************************************************\ - -Function: goto_rw - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void goto_rw(const code_function_callt &function_call, - std::list &read, std::list &write) -{ - if(function_call.lhs().is_not_nil()) - get_objects_rec(LHS_W, function_call.lhs(), read, write); - - get_objects_rec(READ, function_call.function(), read, write); - - forall_expr(it, function_call.arguments()) - get_objects_rec(READ, *it, read, write); -} - -/*******************************************************************\ - -Function: goto_rw - - Inputs: - - Outputs: - - Purpose: - -\*******************************************************************/ - -void goto_rw(const goto_programt::instructiont &instruction, - std::list &read, - std::list &write) -{ - switch(instruction.type) - { - case NO_INSTRUCTION_TYPE: - assert(false); - break; - - case GOTO: - case ASSUME: - case ASSERT: - get_objects_rec(READ, instruction.guard, read, write); - break; - - case RETURN: - { - const code_returnt &code_return=to_code_return(instruction.code); - if(code_return.has_return_value()) - get_objects_rec(READ, code_return.return_value(), read, write); - } - break; - - case OTHER: - // don't know - break; - - case DEAD: - case SKIP: - case START_THREAD: - case END_THREAD: - case LOCATION: - case END_FUNCTION: - case ATOMIC_BEGIN: - case ATOMIC_END: - case THROW: - case CATCH: - // these don't read or write anything - break; - - case ASSIGN: - goto_rw(to_code_assign(instruction.code), read, write); - break; - - case DECL: - get_objects_rec(LHS_W, to_code_decl(instruction.code).symbol(), - read, write); - break; - - case FUNCTION_CALL: - goto_rw(to_code_function_call(instruction.code), read, write); - break; - } -} - diff --git a/src/goto-programs/goto_rw.h b/src/goto-programs/goto_rw.h deleted file mode 100644 index 77108cd..0000000 --- a/src/goto-programs/goto_rw.h +++ /dev/null @@ -1,19 +0,0 @@ -/*******************************************************************\ - -Module: - -Author: Daniel Kroening - -Date: April 2010 - -\*******************************************************************/ - -#ifndef CPROVER_GOTO_PROGRAMS_GOTO_RW_H -#define CPROVER_GOTO_PROGRAMS_GOTO_RW_H - -#include "goto_program.h" - -void goto_rw(const goto_programt::instructiont &, - std::list &read, std::list &write); - -#endif diff --git a/src/goto-programs/remove_function_pointers.cpp b/src/goto-programs/remove_function_pointers.cpp index 74e709b..f7128f0 100644 --- a/src/goto-programs/remove_function_pointers.cpp +++ b/src/goto-programs/remove_function_pointers.cpp @@ -34,26 +34,24 @@ Author: Daniel Kroening, kroening@kroening.com class remove_function_pointerst { public: - explicit remove_function_pointerst(symbol_tablet &_symbol_table): - ns(_symbol_table), - symbol_table(_symbol_table) - { - } + remove_function_pointerst( + symbol_tablet &_symbol_table, + bool _add_safety_assertion, + const goto_functionst &goto_functions); void operator()(goto_functionst &goto_functions); - - bool add_safety_assertion; + + bool remove_function_pointers(goto_programt &goto_program); protected: const namespacet ns; symbol_tablet &symbol_table; + bool add_safety_assertion; void remove_function_pointer( goto_programt &goto_program, goto_programt::targett target); - bool remove_function_pointers(goto_programt &goto_program); - std::set address_taken; typedef std::map type_mapt; @@ -76,6 +74,36 @@ protected: /*******************************************************************\ +Function: remove_function_pointerst::remove_function_pointerst + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + +remove_function_pointerst::remove_function_pointerst( + symbol_tablet &_symbol_table, + bool _add_safety_assertion, + const goto_functionst &goto_functions): + ns(_symbol_table), + symbol_table(_symbol_table), + add_safety_assertion(_add_safety_assertion) +{ + compute_address_taken_functions(goto_functions, address_taken); + + // build type map + for(goto_functionst::function_mapt::const_iterator f_it= + goto_functions.function_map.begin(); + f_it!=goto_functions.function_map.end(); + f_it++) + type_map[f_it->first]=f_it->second.type; +} + +/*******************************************************************\ + Function: remove_function_pointerst::new_tmp_symbol Inputs: @@ -424,7 +452,7 @@ void remove_function_pointerst::remove_function_pointer( /*******************************************************************\ -Function: remove_function_pointerst::operator() +Function: remove_function_pointerst::remove_function_pointers Inputs: @@ -477,15 +505,6 @@ void remove_function_pointerst::operator()(goto_functionst &functions) { bool did_something=false; - compute_address_taken_functions(functions, address_taken); - - // build type map - for(goto_functionst::function_mapt::iterator f_it= - functions.function_map.begin(); - f_it!=functions.function_map.end(); - f_it++) - type_map[f_it->first]=f_it->second.type; - for(goto_functionst::function_mapt::iterator f_it= functions.function_map.begin(); f_it!=functions.function_map.end(); @@ -513,13 +532,38 @@ Function: remove_function_pointers \*******************************************************************/ +bool remove_function_pointers( + symbol_tablet &symbol_table, + const goto_functionst &goto_functions, + goto_programt &goto_program, + bool add_safety_assertion) +{ + remove_function_pointerst + rfp(symbol_table, add_safety_assertion, goto_functions); + + return rfp.remove_function_pointers(goto_program); +} + +/*******************************************************************\ + +Function: remove_function_pointers + + Inputs: + + Outputs: + + Purpose: + +\*******************************************************************/ + void remove_function_pointers( symbol_tablet &symbol_table, goto_functionst &goto_functions, bool add_safety_assertion) { - remove_function_pointerst rfp(symbol_table); - rfp.add_safety_assertion=add_safety_assertion; + remove_function_pointerst + rfp(symbol_table, add_safety_assertion, goto_functions); + rfp(goto_functions); } diff --git a/src/goto-programs/remove_function_pointers.h b/src/goto-programs/remove_function_pointers.h index b664878..2931f16 100644 --- a/src/goto-programs/remove_function_pointers.h +++ b/src/goto-programs/remove_function_pointers.h @@ -24,4 +24,10 @@ void remove_function_pointers( goto_functionst &goto_functions, bool add_safety_assertion); +bool remove_function_pointers( + symbol_tablet &symbol_table, + const goto_functionst &goto_functions, + goto_programt &goto_program, + bool add_safety_assertion); + #endif diff --git a/src/pointer-analysis/value_set_analysis.h b/src/pointer-analysis/value_set_analysis.h index 20f6965..5442f34 100644 --- a/src/pointer-analysis/value_set_analysis.h +++ b/src/pointer-analysis/value_set_analysis.h @@ -50,7 +50,7 @@ public: public: // interface value_sets virtual void get_values( - locationt l, + goto_programt::const_targett l, const exprt &expr, value_setst::valuest &dest) { diff --git a/src/pointer-analysis/value_set_domain.cpp b/src/pointer-analysis/value_set_domain.cpp index d2ab783..f711500 100644 --- a/src/pointer-analysis/value_set_domain.cpp +++ b/src/pointer-analysis/value_set_domain.cpp @@ -24,8 +24,8 @@ Function: value_set_domaint::transform void value_set_domaint::transform( const namespacet &ns, - locationt from_l, - locationt to_l) + goto_programt::const_targett from_l, + goto_programt::const_targett to_l) { switch(from_l->type) { diff --git a/src/pointer-analysis/value_set_domain.h b/src/pointer-analysis/value_set_domain.h index d26268b..0622e0d 100644 --- a/src/pointer-analysis/value_set_domain.h +++ b/src/pointer-analysis/value_set_domain.h @@ -20,7 +20,9 @@ public: // overloading - inline bool merge(const value_set_domaint &other, locationt to) + inline bool merge( + const value_set_domaint &other, + goto_programt::const_targett to) { return value_set.make_union(other.value_set); } @@ -34,7 +36,7 @@ public: virtual void initialize( const namespacet &ns, - locationt l) + goto_programt::const_targett l) { value_set.clear(); value_set.location_number=l->location_number; @@ -42,8 +44,8 @@ public: virtual void transform( const namespacet &ns, - locationt from_l, - locationt to_l); + goto_programt::const_targett from_l, + goto_programt::const_targett to_l); virtual void get_reference_set( const namespacet &ns, diff --git a/src/util/graph.h b/src/util/graph.h index b1abcb1..371eb91 100644 --- a/src/util/graph.h +++ b/src/util/graph.h @@ -16,11 +16,11 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -class empty_nodet +class empty_edget { }; -template +template class graph_nodet { public: