forked from diffblue/cbmc
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
introduce unwindsett for unwinding limits
- Loading branch information
Daniel Kroening
committed
May 18, 2018
1 parent
da61186
commit dcc907a
Showing
9 changed files
with
156 additions
and
124 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -15,8 +15,6 @@ Author: Daniel Kroening, [email protected] | |
| #include <iostream> | ||
|
|
||
| #include <util/exit_codes.h> | ||
| #include <util/string2int.h> | ||
| #include <util/string_utils.h> | ||
|
|
||
| #include <langapi/language_util.h> | ||
|
|
||
|
|
@@ -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<std::string> 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 | ||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -18,6 +18,8 @@ Author: Daniel Kroening, [email protected] | |
| #include <goto-symex/path_storage.h> | ||
| #include <goto-symex/goto_symex.h> | ||
|
|
||
| #include <goto-instrument/unwindset.h> | ||
|
|
||
| #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<irep_idt, unsigned> loop_limitst; | ||
| loop_limitst loop_limits; | ||
|
|
||
| typedef std::map<unsigned, loop_limitst> 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_handlert> loop_unwind_handlers; | ||
|
|
||
| /// Callbacks that may provide an unwind/do-not-unwind decision for a | ||
| /// recursive call | ||
| std::vector<recursion_unwind_handlert> recursion_unwind_handlers; | ||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,79 @@ | ||
| /*******************************************************************\ | ||
| Module: Loop unwinding setup | ||
| Author: Daniel Kroening, [email protected] | ||
| \*******************************************************************/ | ||
|
|
||
| #include "unwindset.h" | ||
|
|
||
| #include <util/string2int.h> | ||
| #include <util/string_utils.h> | ||
|
|
||
| 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<std::string> 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<unsigned> uw(0); | ||
|
|
||
| if(uw_string.empty()) | ||
| uw = { }; | ||
| else | ||
| uw = unsafe_string2unsigned(uw_string); | ||
|
|
||
| if(thread_nr_set) | ||
| thread_loop_map[std::pair<irep_idt, unsigned>(id, thread_nr)] = uw; | ||
| else | ||
| loop_map[id] = uw; | ||
| } | ||
| } | ||
| } | ||
|
|
||
| optionalt<unsigned> | ||
| 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<irep_idt, unsigned>(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; | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,53 @@ | ||
| /*******************************************************************\ | ||
| Module: Loop unwinding setup | ||
| Author: Daniel Kroening, [email protected] | ||
| \*******************************************************************/ | ||
|
|
||
| /// \file | ||
| /// Loop unwinding | ||
|
|
||
| #ifndef CPROVER_GOTO_INSTRUMENT_UNWINDSET_H | ||
| #define CPROVER_GOTO_INSTRUMENT_UNWINDSET_H | ||
|
|
||
| #include <map> | ||
| #include <string> | ||
|
|
||
| #include <util/irep.h> | ||
| #include <util/optional.h> | ||
|
|
||
| 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<unsigned> get_limit(const irep_idt &loop, unsigned thread_id) const; | ||
|
|
||
| protected: | ||
| optionalt<unsigned> global_limit; | ||
|
|
||
| // Limit for all instances of a loop. | ||
| // This may have 'no value'. | ||
| typedef std::map<irep_idt, optionalt<unsigned>> loop_mapt; | ||
| loop_mapt loop_map; | ||
|
|
||
| // separate limits per thread | ||
| using thread_loop_mapt = | ||
| std::map<std::pair<irep_idt, unsigned>, optionalt<unsigned>>; | ||
| thread_loop_mapt thread_loop_map; | ||
| }; | ||
|
|
||
| #endif // CPROVER_GOTO_INSTRUMENT_UNWINDSET_H |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters