Remove Git dependency from incremental analysis

[sim642]

Any saved (marshaled) and loaded (unmarshaled) run should be able to run using incremental analysis.

[jerhard]

There is no Makefile dependency in the incremental version, but there is indeed the requirement that the code that is analyzed is contained in a Git repository and that this repo is in a clean state. I changed the issue title accordingly.

[jerhard]

As of now, the incremental results are stored in a folder with the hash-code of the current commit of the analyzed repo as the name.
If there are already multiple previous analysis results for the repo, Goblint will pick the analysis results of the last commit preceding the current commit of the repo as the baseline for the analysis.

I would completely get rid of this mechanic and only store one – the latest – analysis result.

[sim642]

There is no Makefile dependency in the incremental version, but there is indeed the requirement that the code that is analyzed is contained in a Git repository and that this repo is in a clean state. I changed the issue title accordingly.

There is MakefileUtil in src/incremental/ though. Is that actually independent from incrementality then, despite being in that directory?

As of now, the incremental results are stored in a folder with the hash-code of the current commit of the analyzed repo as the name.
If there are already multiple previous analysis results for the repo, Goblint will pick the analysis results of the last commit preceding the current commit of the repo as the baseline for the analysis.

I would completely get rid of this mechanic and only store one – the latest – analysis result.

Just having an option for a single directory to use would probably be enough, but if you want to get rid of the versioning thing inside Goblint, then I'm not opposed either. I suppose if such functionality is needed, it could easily be achieved using a wrapper script.

---

Also, what's the relationship between incremental and save_run/load_run? Now looking at the code, it seems like you could use incrementality without load_run.
I'm confused because incremental analysis added the relift etc stuff, but load_run uses them and both seem to have been introduced at a similar time.
If they're independent, then a problem using incremental analysis and changing options? Because save_run stores a copy of the config used by the marshaled results, such that load_run would use the same exact config for the unmarshaled data to be valid at all. Surely the unmarshaling by incremental analysis requires the same?

And what's the point of exp.incremental.mode being complete? The description just says complete (discard loaded data and start fresh), but isn't that just the same as disabling incremental altogether?

[jerhard]

Is that actually independent from incrementality then, despite being in that directory?

It is actually independent, yes. It should probably be moved to ./src/util.

Also, what's the relationship between incremental and save_run/load_run? Now looking at the code, it seems like you could use incrementality without load_run.

These are independent options. save_run, load_run was introduced by @vogler to be able to compare different runs of Goblint on the same analyzed source code.

If they're independent, then a problem using incremental analysis and changing options?

Yes, this is a problem.

Because save_run stores a copy of the config used by the marshaled results, such that load_run would use the same exact config for the unmarshaled data to be valid at all. Surely the unmarshaling by incremental analysis requires the same

It does require that the options stay the same, yes. This is currently not checked however; only a warning is printed to the user that it will crash if the options have changed.

And what's the point of exp.incremental.mode being complete? The description just says complete (discard loaded data and start fresh), but isn't that just the same as disabling incremental altogether?

The "complete" option starts off fresh, but the results are stored to disc, so that a subsequent incremental run can use them.

[sim642]

It does require that the options stay the same, yes. This is currently not checked however; only a warning is printed to the user that it will crash if the options have changed.

It's out of the scope of this issue, but we should probably have a check for this for interactive analysis indeed, i.e. the previous config gets stored. Because the user might want to change the config and then we should be able to detect them not being equal and also do a full reanalysis.

The "complete" option starts off fresh, but the results are stored to disc, so that a subsequent incremental run can use them.

I'm now thinking that maybe it would also be better to have separate options like exp.incremental.save and exp.incremental.load such that all four combinations are possible. This would also allow loading for incremental analysis, but not saving the new results.