From dcc907a67a62f4c7e4e6dadb0536c7c5e666236a Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 8 May 2018 14:07:51 +0100 Subject: [PATCH] introduce unwindsett for unwinding limits --- src/cbmc/Makefile | 7 +-- src/cbmc/bmc.cpp | 42 +--------------- src/cbmc/bmc.h | 2 - src/cbmc/symex_bmc.cpp | 44 ++++------------- src/cbmc/symex_bmc.h | 45 ++---------------- src/goto-instrument/Makefile | 1 + src/goto-instrument/unwindset.cpp | 79 +++++++++++++++++++++++++++++++ src/goto-instrument/unwindset.h | 53 +++++++++++++++++++++ src/jbmc/Makefile | 7 +-- 9 files changed, 156 insertions(+), 124 deletions(-) create mode 100644 src/goto-instrument/unwindset.cpp create mode 100644 src/goto-instrument/unwindset.h diff --git a/src/cbmc/Makefile b/src/cbmc/Makefile index 9da2d96efc2..e1045b7bc9c 100644 --- a/src/cbmc/Makefile +++ b/src/cbmc/Makefile @@ -30,9 +30,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../pointer-analysis/add_failed_symbols$(OBJEXT) \ ../pointer-analysis/rewrite_index$(OBJEXT) \ ../pointer-analysis/goto_program_dereference$(OBJEXT) \ - ../goto-instrument/reachability_slicer$(OBJEXT) \ - ../goto-instrument/full_slicer$(OBJEXT) \ - ../goto-instrument/nondet_static$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ ../goto-instrument/cover_basic_blocks$(OBJEXT) \ ../goto-instrument/cover_filter$(OBJEXT) \ @@ -43,6 +40,10 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ ../goto-instrument/cover_instrument_other$(OBJEXT) \ ../goto-instrument/cover_util$(OBJEXT) \ + ../goto-instrument/reachability_slicer$(OBJEXT) \ + ../goto-instrument/nondet_static$(OBJEXT) \ + ../goto-instrument/full_slicer$(OBJEXT) \ + ../goto-instrument/unwindset$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \ diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp index ea7b3e17f30..40e552bca71 100644 --- a/src/cbmc/bmc.cpp +++ b/src/cbmc/bmc.cpp @@ -15,8 +15,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include -#include #include @@ -319,7 +317,8 @@ void bmct::setup() symex.last_source_location.make_nil(); - setup_unwind(); + symex.unwindset.parse_unwind(options.get_option("unwind")); + symex.unwindset.parse_unwindset(options.get_option("unwindset")); } safety_checkert::resultt bmct::execute( @@ -549,43 +548,6 @@ safety_checkert::resultt bmct::stop_on_fail(prop_convt &prop_conv) } } -void bmct::setup_unwind() -{ - const std::string &set=options.get_option("unwindset"); - std::vector unwindset_loops; - split_string(set, ',', unwindset_loops, true, true); - - for(auto &val : unwindset_loops) - { - unsigned thread_nr=0; - bool thread_nr_set=false; - - if(!val.empty() && - isdigit(val[0]) && - val.find(":")!=std::string::npos) - { - std::string nr=val.substr(0, val.find(":")); - thread_nr=unsafe_string2unsigned(nr); - thread_nr_set=true; - val.erase(0, nr.size()+1); - } - - if(val.rfind(":")!=std::string::npos) - { - std::string id=val.substr(0, val.rfind(":")); - long uw=unsafe_string2int(val.substr(val.rfind(":")+1)); - - if(thread_nr_set) - symex.set_unwind_thread_loop_limit(thread_nr, id, uw); - else - symex.set_unwind_loop_limit(id, uw); - } - } - - if(options.get_option("unwind")!="") - symex.set_unwind_limit(options.get_unsigned_int_option("unwind")); -} - /// Perform core BMC, using an abstract model to supply GOTO function bodies /// (perhaps created on demand). /// \param opts: command-line options affecting BMC diff --git a/src/cbmc/bmc.h b/src/cbmc/bmc.h index 0e7efe46da9..a61ba9e3e6c 100644 --- a/src/cbmc/bmc.h +++ b/src/cbmc/bmc.h @@ -183,8 +183,6 @@ class bmct:public safety_checkert const goto_functionst &, prop_convt &); - // unwinding - virtual void setup_unwind(); void do_conversion(); virtual void freeze_program_variables(); diff --git a/src/cbmc/symex_bmc.cpp b/src/cbmc/symex_bmc.cpp index 986e368ea45..abdda442a5b 100644 --- a/src/cbmc/symex_bmc.cpp +++ b/src/cbmc/symex_bmc.cpp @@ -25,8 +25,6 @@ symex_bmct::symex_bmct( path_storaget &path_storage) : goto_symext(mh, outer_symbol_table, _target, path_storage), record_coverage(false), - max_unwind(0), - max_unwind_is_set(false), symex_coverage(ns) { } @@ -131,25 +129,12 @@ bool symex_bmct::get_unwind( // / --unwind options to decide: if(abort_unwind_decision.is_unknown()) { - // We use the most specific limit we have, - // and 'infinity' when we have none. + auto limit=unwindset.get_limit(id, source.thread_nr); - loop_limitst &this_thread_limits= - thread_loop_limits[source.thread_nr]; - - loop_limitst::const_iterator l_it=this_thread_limits.find(id); - if(l_it!=this_thread_limits.end()) - this_loop_limit=l_it->second; + if(!limit.has_value()) + abort_unwind_decision = tvt(false); else - { - l_it=loop_limits.find(id); - if(l_it!=loop_limits.end()) - this_loop_limit=l_it->second; - else if(max_unwind_is_set) - this_loop_limit=max_unwind; - } - - abort_unwind_decision = tvt(unwind >= this_loop_limit); + abort_unwind_decision = tvt(unwind >= *limit); } INVARIANT( @@ -187,25 +172,12 @@ bool symex_bmct::get_unwind_recursion( // / --unwind options to decide: if(abort_unwind_decision.is_unknown()) { - // We use the most specific limit we have, - // and 'infinity' when we have none. - - loop_limitst &this_thread_limits= - thread_loop_limits[thread_nr]; + auto limit=unwindset.get_limit(id, thread_nr); - loop_limitst::const_iterator l_it=this_thread_limits.find(id); - if(l_it!=this_thread_limits.end()) - this_loop_limit=l_it->second; + if(!limit.has_value()) + abort_unwind_decision = tvt(false); else - { - l_it=loop_limits.find(id); - if(l_it!=loop_limits.end()) - this_loop_limit=l_it->second; - else if(max_unwind_is_set) - this_loop_limit=max_unwind; - } - - abort_unwind_decision = tvt(unwind>this_loop_limit); + abort_unwind_decision = tvt(unwind > *limit); } INVARIANT( diff --git a/src/cbmc/symex_bmc.h b/src/cbmc/symex_bmc.h index bc43242037b..0808604118c 100644 --- a/src/cbmc/symex_bmc.h +++ b/src/cbmc/symex_bmc.h @@ -18,6 +18,8 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include + #include "symex_coverage.h" class symex_bmct: public goto_symext @@ -32,29 +34,6 @@ class symex_bmct: public goto_symext // To show progress source_locationt last_source_location; - // Control unwinding. - - void set_unwind_limit(unsigned limit) - { - max_unwind=limit; - max_unwind_is_set=true; - } - - void set_unwind_thread_loop_limit( - unsigned thread_nr, - const irep_idt &id, - unsigned limit) - { - thread_loop_limits[thread_nr][id]=limit; - } - - void set_unwind_loop_limit( - const irep_idt &id, - unsigned limit) - { - loop_limits[id]=limit; - } - /// Loop unwind handlers take the function ID and loop number, the unwind /// count so far, and an out-parameter specifying an advisory maximum, which /// they may set. If set the advisory maximum is set it is *only* used to @@ -101,26 +80,12 @@ class symex_bmct: public goto_symext bool record_coverage; -protected: - // We have - // 1) a global limit (max_unwind) - // 2) a limit per loop, all threads - // 3) a limit for a particular thread. - // 4) zero or more handler functions that can special-case particular - // functions or loops - // We use the most specific of the above. - - unsigned max_unwind; - bool max_unwind_is_set; - - typedef std::unordered_map loop_limitst; - loop_limitst loop_limits; - - typedef std::map thread_loop_limitst; - thread_loop_limitst thread_loop_limits; + unwindsett unwindset; +protected: /// Callbacks that may provide an unwind/do-not-unwind decision for a loop std::vector loop_unwind_handlers; + /// Callbacks that may provide an unwind/do-not-unwind decision for a /// recursive call std::vector recursion_unwind_handlers; diff --git a/src/goto-instrument/Makefile b/src/goto-instrument/Makefile index bb4ff425daf..126151d9c03 100644 --- a/src/goto-instrument/Makefile +++ b/src/goto-instrument/Makefile @@ -61,6 +61,7 @@ SRC = accelerate/accelerate.cpp \ undefined_functions.cpp \ uninitialized.cpp \ unwind.cpp \ + unwindset.cpp \ wmm/abstract_event.cpp \ wmm/cycle_collection.cpp \ wmm/data_dp.cpp \ diff --git a/src/goto-instrument/unwindset.cpp b/src/goto-instrument/unwindset.cpp new file mode 100644 index 00000000000..79b296dcf3b --- /dev/null +++ b/src/goto-instrument/unwindset.cpp @@ -0,0 +1,79 @@ +/*******************************************************************\ + +Module: Loop unwinding setup + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "unwindset.h" + +#include +#include + +void unwindsett::parse_unwind(const std::string &unwind) +{ + if(!unwind.empty()) + global_limit = unsafe_string2unsigned(unwind); +} + +void unwindsett::parse_unwindset(const std::string &unwindset) +{ + std::vector unwindset_loops; + split_string(unwindset, ',', unwindset_loops, true, true); + + for(auto &val : unwindset_loops) + { + unsigned thread_nr = 0; + bool thread_nr_set = false; + + if(!val.empty() && isdigit(val[0]) && val.find(":") != std::string::npos) + { + std::string nr = val.substr(0, val.find(":")); + thread_nr = unsafe_string2unsigned(nr); + thread_nr_set = true; + val.erase(0, nr.size() + 1); + } + + if(val.rfind(":") != std::string::npos) + { + std::string id = val.substr(0, val.rfind(":")); + std::string uw_string = val.substr(val.rfind(":") + 1); + + // the below initialisation makes g++-5 happy + optionalt uw(0); + + if(uw_string.empty()) + uw = { }; + else + uw = unsafe_string2unsigned(uw_string); + + if(thread_nr_set) + thread_loop_map[std::pair(id, thread_nr)] = uw; + else + loop_map[id] = uw; + } + } +} + +optionalt +unwindsett::get_limit(const irep_idt &loop_id, unsigned thread_nr) const +{ + // We use the most specific limit we have + + // thread x loop + auto tl_it = + thread_loop_map.find(std::pair(loop_id, thread_nr)); + + if(tl_it != thread_loop_map.end()) + return tl_it->second; + + // loop + auto l_it = loop_map.find(loop_id); + + if(l_it != loop_map.end()) + return l_it->second; + + // global, if any + return global_limit; +} diff --git a/src/goto-instrument/unwindset.h b/src/goto-instrument/unwindset.h new file mode 100644 index 00000000000..5e5146c9597 --- /dev/null +++ b/src/goto-instrument/unwindset.h @@ -0,0 +1,53 @@ +/*******************************************************************\ + +Module: Loop unwinding setup + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +/// \file +/// Loop unwinding + +#ifndef CPROVER_GOTO_INSTRUMENT_UNWINDSET_H +#define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H + +#include +#include + +#include +#include + +class unwindsett +{ +public: + // We have + // 1) a global limit + // 2) a limit per loop, all threads + // 3) a limit for a particular thread. + // We use the most specific of the above. + + // global limit for all loops + void parse_unwind(const std::string &unwind); + + // limit for instances of a loop + void parse_unwindset(const std::string &unwindset); + + // queries + optionalt get_limit(const irep_idt &loop, unsigned thread_id) const; + +protected: + optionalt global_limit; + + // Limit for all instances of a loop. + // This may have 'no value'. + typedef std::map> loop_mapt; + loop_mapt loop_map; + + // separate limits per thread + using thread_loop_mapt = + std::map, optionalt>; + thread_loop_mapt thread_loop_map; +}; + +#endif // CPROVER_GOTO_INSTRUMENT_UNWINDSET_H diff --git a/src/jbmc/Makefile b/src/jbmc/Makefile index 8d649d27731..6bdc5ad2685 100644 --- a/src/jbmc/Makefile +++ b/src/jbmc/Makefile @@ -17,9 +17,6 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../pointer-analysis/add_failed_symbols$(OBJEXT) \ ../pointer-analysis/rewrite_index$(OBJEXT) \ ../pointer-analysis/goto_program_dereference$(OBJEXT) \ - ../goto-instrument/full_slicer$(OBJEXT) \ - ../goto-instrument/reachability_slicer$(OBJEXT) \ - ../goto-instrument/nondet_static$(OBJEXT) \ ../goto-instrument/cover$(OBJEXT) \ ../goto-instrument/cover_basic_blocks$(OBJEXT) \ ../goto-instrument/cover_filter$(OBJEXT) \ @@ -30,6 +27,10 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \ ../goto-instrument/cover_instrument_mcdc$(OBJEXT) \ ../goto-instrument/cover_instrument_other$(OBJEXT) \ ../goto-instrument/cover_util$(OBJEXT) \ + ../goto-instrument/full_slicer$(OBJEXT) \ + ../goto-instrument/nondet_static$(OBJEXT) \ + ../goto-instrument/reachability_slicer$(OBJEXT) \ + ../goto-instrument/unwindset$(OBJEXT) \ ../analyses/analyses$(LIBEXT) \ ../langapi/langapi$(LIBEXT) \ ../xmllang/xmllang$(LIBEXT) \