Remove dependence of the incremental analysis on Git #358
Conversation
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
The previous implementation with List.assoc_opt used the polymorphic compare, which might lead to out of memory exceptions when used with unmarshalled objects
Add the possibility for solver to now additionally return their state for serialization (as an Obj.t option), that later might be reused for incremental analysis. Currently TD3 is the only solver making use of this. The idea is to move the serialization and deserialization logic out of TD3, so that it later can more easily be adapted, in particular for the following two purposes: 1. making the serialization no longer dependent on Git-Commit-IDs 2. allowing to keep the data needed for incremental runs in memory, i.e. so that data does not need to be stored to disk and read from there.
…sults. No longer require that the current version of the incrementally analyzed software is a committed version. Analysis results are no longer stored in a directory named after the commit, but in some temporary results dir. After the analysis completed, the temporary results are renamed so they will be reused in the next incremental analysis run.
…Goblint. Incremental analysis results are now stored inside the current working directory, and not within the git-directory of the analyzed source files. This also removes the dependenceof the incremental analysis on git.
Move exp.incremental.* options to incremental.* and introduce options incremental.load, incremental.save instead of exp.incremental.mode to configure whether data necessary for incremental analysis is loaded and stored.
sim642
reviewed
Sep 27, 2021
Solver now return, besides the solution, an object for serialization. For now, this object is a dummy object for all solvers besides TD3.
sim642
approved these changes
Sep 28, 2021
There was a problem hiding this comment.
I think this can be merged now, so we can try integrating this with Magpie and see how interactive it feels.
I'm guessing this should be run with incremental.save first and incremental.load the second time and that's all, or is there anything else that needs to be done to use it now?
And the loading run may also specify saving for subsequent incremental runs, I suppose.
The incremental analysis does currently not work for now with the hashconsing. The one known problem is that the check, whether start states of queried functions changed does not work with hashconsing, because different objects (one from the previous and current run) have the same tag. Thus hashconsing is disabled when incremental.load or incremental.save is enabled. The incremental config is changed accordingly.
jerhard
force-pushed
the
incremental/no-git
branch
from
e88ec81
to
8ea94c5
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.
Removes the dependence of the incremental analysis on Git, and thus closes #350. Now:
incremental_data.The last bullet point also implies that the feature that would allow to base an incremental analysis on the most-recent ancestor of the current commit that needs to be analyzed, is no longer supported. (E.g. Imagine that you had three commits
a->b->c, and that you already have analysis results foraandc. Previously the incremental analysis of commitbwould be based on the analysis of commita. This is no longer the case. Instead it will base the incremental analysis on whichever version one analyzed last).This PR also move the storing of the solver from
TD3toControl, where the handling for the (unrelated) serialization ofload_run,save_runis done. The idea is that passing the solver state back will make it easier to perform an incremental run in a server mode scenario, because it should make it easier to feed the solver the old results back.