Skip to content
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

Add option to store local results of Apron-Analysis for comparison #433

Merged
merged 30 commits into from
Nov 5, 2021

Conversation

jerhard
Copy link
Member

@jerhard jerhard commented Nov 4, 2021

This PR adds an option to store apron analysis results in a file, such that different analysis runs can be compared using the apronPrivPrecCompare program that is introduced and based on privPrecCompare.

Storing the results of the Apron analysis is activated by setting the string option for "exp.apron-prec-dump" to a non-empty string, which will be used as the file name.

Apron does not offer serialization for its Intervals ("Boxes") and Polyhedra ("Polka").
We thus convert the Apron domain used in the analysis to the octagon domain before serialization. This is done via a conjunction of linear constraints(see here and here, i.e. with to_lincons_array and of_lincons_array).

What is stored / compared

The results for the analysis are stored per program node. Results for different contexts but the same node are joined together. Results of global unknowns are not stored.

What still needs to be done

Storing the results (done in finalize) should only be done in the postsolving stage.
However, when adding such a check, the code is not called. Maybe one needs to change some configuration?

How to test

The comparison program apronPrivPrecCompare apronPrecCompare is built with:

make apronPrecCompare 

The comparison then can be tested on a simple example as follows:

./regtest.sh 36 71 --set ana.apron.domain "octagon" --set exp.apron.prec-dump apron_oct.save
./regtest.sh 36 71 --set ana.apron.domain "interval" --set exp.apron.prec-dump apron_int.save

./apronPrecCompare apron_oct.save apron_int.save

Closes #423

@jerhard jerhard changed the title Add option to store local results for Apron-Analysis and comparison Add option to store local results of Apron-Analysis for comparison Nov 4, 2021
@jerhard jerhard requested a review from sim642 November 4, 2021 16:26
@sim642
Copy link
Member

sim642 commented Nov 4, 2021

Storing the results (done in finalize) should only be done in the postsolving stage.
However, when adding such a check, the code is not called. Maybe one needs to change some configuration?

finalize is called at the very end of Control anyway and nowhere else (AFAIK), so there doesn't need to be any condition in there. "Postsolving" only refers to the single final evaluation of the entire constraint system and the boolean is actually disabled after that.

@sim642
Copy link
Member

sim642 commented Nov 5, 2021

Currently the CI fails for all non-apron builds because some util module depends on the Apron stuff. That probably should be separated.

src/apronPrivPrecCompare.ml Outdated Show resolved Hide resolved
@jerhard
Copy link
Member Author

jerhard commented Nov 5, 2021

Currently the CI fails for all non-apron builds because some util module depends on the Apron stuff. That probably should be separated.

The utility module for the apron precision comparison is now moved to a separate module using an optional apron dependency, so that should be fixed.

.gitignore Outdated Show resolved Hide resolved
src/util/defaults.ml Outdated Show resolved Hide resolved
src/analyses/apron/apronAnalysis.apron.ml Outdated Show resolved Hide resolved
src/analyses/apron/apronAnalysis.apron.ml Outdated Show resolved Hide resolved
src/cdomains/apron/apronDomain.apron.ml Outdated Show resolved Hide resolved
src/cdomains/apron/apronDomain.apron.ml Outdated Show resolved Hide resolved
src/cdomains/apron/apronDomain.apron.ml Outdated Show resolved Hide resolved
src/privPrecCompare.ml Outdated Show resolved Hide resolved
src/util/PrecCompareUtil.ml Outdated Show resolved Hide resolved
jerhard and others added 5 commits November 5, 2021 13:13
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
…ron manager in Goblint.

Deserialization of apron results is not performed in Goblint itself, but only in apronPrecCompare. The deserialization manager is getting intialized there already, so this code is no longer needed.
… used there. Explain why name () is overriden.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Allow serialization and deserialization of Apron Analysis results for precision comparison
2 participants