Shortest path search heuristic #5
Open
Conversation
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
polgreen
force-pushed
the
shortest_path_search_heuristic
branch
from
23854dc to
d7796f0
Compare
polgreen
requested review from
cesaro,
kroening and
peterschrammel
as code owners
Randomized DFS shuffles the queue of successor states
Also fixes indentation and whitespace in the output function, and replaces unsigned with std::size_t, based on feedback from tautschn
Builds CFG of all program locations and computes the shortest distance from all locations in the graph to a single property. WARNING: if more than one property is given, we use the first one only. Writes these distances to the corresponding node in a locs structure passed as argument to the constructor, in order for this to be used to guide the symex search
Builds a CFG for every goto_program in goto_functions, and computes the distance for every location in the CFGs to the property, if one exists in taht CFG, or to the end of the function Writes these numbers to locst passed as argument to the constructor, in order to use numbers to guide symex search
Shortest path search heuristic computes the shortest path from all program locations to a single property. This metric is used to guide the symex search. We also introduce randomized shortest path based search, which makes a random choice when picking the next state every 1000 choices in order to avoid local minima
Computes the shortest path per function on the shortest path graph and uses this heuristic to guide the symex search
polgreen
force-pushed
the
shortest_path_search_heuristic
branch
from
d7796f0 to
68e6eed
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Introduces shortest_path_grapht class, which computes the shortest path from every program location to a single property (note this only works with 1 property, and a warning is given if more than one property is present in the program), stores these numbers in locst.
These numbers are then used to guide the symex search heuristic (this is why i only implemented this for one property, the search heuristic becomes less effective with multiple properties).
The shortest path per function computes either the shortest path to the property, if the property is within that function, or the shortest path to the end of the function.