-
Notifications
You must be signed in to change notification settings - Fork 273
move setup_unwind to parse_unwindset_options to prevent duplication #2167
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
2 commits
Select commit
Hold shift + click to select a range
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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 hidden or 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
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Since the very same code exists twice: how about adding a
tvt unwindsett::limit_reached(id, thread_nr, unwind)?There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Not easy, "this_loop_limit" is used later, and those handlers want the function name, not the loop ID
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
(I want to get rid of the handlers, BTW, that is the whole point of overloading those methods in goto-symex)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't really understand. Lines 132...137 are, except for
source.thread_nrvsthread_nr, exactly the same as lines 175..180.There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Which, btw, changes the behaviour: in the previous code, one used
>=in the comparison, while the other used>. (I'm not sure they actually should be different...)