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.

Sign up for GitHub

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

Jump to bottom

Add Interval Set domain for Interval Set analysis #966

Closed
wants to merge 104 commits into from
Closed

Add Interval Set domain for Interval Set analysis #966

wants to merge 104 commits into from

Conversation

gabryon99
Copy link
Contributor

@gabryon99 gabryon99 commented Jan 13, 2023 •
edited by michael-schwarz
Loading

The following pull request will include the Interval Set Analysis into Goblint, as described by the issue #901.

Closes #901.

sim642
sim642 requested changes Jan 16, 2023
View reviewed changes
Copy link
Member

@sim642 sim642 left a comment •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the implementation with lots of tests!
It would be good to have an SV-COMP run with this enabled as well, if that hasn't already been done. That could help identify possible unsoundness errors.

I just had a quick look right now, didn't look at the actual domain implementation yet.

src/analyses/tutorials/signs.ml Outdated Show resolved Hide resolved
src/util/precisionUtil.ml Outdated Show resolved Hide resolved
tests/regression/61-interval-set-one/0-was_problematic_2.c Outdated Show resolved Hide resolved
goblint.opam Outdated Show resolved Hide resolved
@gabryon99 gabryon99 mentioned this pull request Jan 17, 2023
Merged
1 task
@jerhard jerhard self-requested a review January 18, 2023 15:50
@michael-schwarz
Copy link
Member

It would be good to have an SV-COMP run with this enabled as well, if that hasn't already been done. That could help identify possible unsoundness errors.

Indeed, I will start such a run once some of the issues we already identified (e.g. missing threshold widening) are addressed.

@michael-schwarz michael-schwarz self-requested a review January 18, 2023 19:31
michael-schwarz
michael-schwarz requested changes Jan 18, 2023
View reviewed changes
Copy link
Member

@michael-schwarz michael-schwarz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you for the PR, it is nice to see progress here!

I left a few comments, I think there are some places where we can make things easier to follow by restructuring/reuse, and in a few other places I think we can do better than quadratic complexity.

src/util/options.schema.json Outdated Show resolved Hide resolved
src/util/precisionUtil.ml Outdated Show resolved Hide resolved
src/util/processPool.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
jerhard
jerhard reviewed Jan 19, 2023
View reviewed changes
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 21, 2023
@gabryon99
Re-use of Interval.leq and Interval.join
8eacb08 
Edit suggested from the following reference: goblint#966 (comment)
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 21, 2023
@gabryon99
Re-use of Interval.invariant_ikind
b8762a8 
As suggested from the conversation: goblint#966 (comment)
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 21, 2023
@gabryon99
Remove _functor suffix from Interval_functor
6b1b5f8 
See discussion: goblint#966 (comment)
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 21, 2023
@gabryon99
Optimize getting last list element
f6041ce 
See: goblint#966 (comment), goblint#966 (comment),
goblint#966 (comment)
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 21, 2023
@gabryon99
Replace custom cartesian_product with BatList.cartesian_product
c219218 
See discussion: goblint#966 (comment)
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 23, 2023
@gabryon99
Move set_overflow_flag at the top of intdDomain.ml
f950bfe 
The modification allows the re-use of the function between IntervalFunctor and IntervalSetFunctor. See
the discussion: goblint#966 (comment)
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 23, 2023
@gabryon99
Improving running time complexity for two_interval_sets_to_events
fe1ada7 
See discussion: goblint#966 (comment)
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 23, 2023
@gabryon99
Define refine_with_congruence_interval within refine_with_congruence
dfb7b26 
See discussion: goblint#966 (comment)
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 23, 2023
@gabryon99
Move excl_to_intervalset within refine_with_excli_list
323803d 
See discussion: goblint#966 (comment)
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 23, 2023
@gabryon99
Add comment on IntervalSets elements
0476a9c 
See discussion: goblint#966 (comment)
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 24, 2023
@gabryon99
Renaming norm function into norm_interval
f000e6c 
See discussion: goblint#966 (comment)
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 24, 2023
@gabryon99
Rename remove_gaps into remove_empty_gaps
7af285e 
See discussion: goblint#966 (comment)
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 24, 2023
@gabryon99
Rename norm function into norm_interval
f2f75ec 
See discussion: goblint#966 (comment)
gabryon99 added a commit to BilelGho/analyzer that referenced this pull request Jan 24, 2023
@gabryon99
Rename remove_gaps into remove_empty_gaps
dd6b8ee 
See discussion: goblint#966 (comment)
BilelGho pushed a commit to BilelGho/analyzer that referenced this pull request Jan 26, 2023
@gabryon99 @BilelGho
Re-use of Interval.leq and Interval.join
f76da67 
Edit suggested from the following reference: goblint#966 (comment)
BilelGho pushed a commit to BilelGho/analyzer that referenced this pull request Jan 26, 2023
@gabryon99 @BilelGho
Re-use of Interval.invariant_ikind
1d18378 
As suggested from the conversation: goblint#966 (comment)
BilelGho pushed a commit to BilelGho/analyzer that referenced this pull request Jan 26, 2023
@gabryon99 @BilelGho
Remove _functor suffix from Interval_functor
0b0dfca 
See discussion: goblint#966 (comment)
BilelGho pushed a commit to BilelGho/analyzer that referenced this pull request Jan 26, 2023
@gabryon99 @BilelGho
Optimize getting last list element
6a0abcf 
See: goblint#966 (comment), goblint#966 (comment),
goblint#966 (comment)
BilelGho pushed a commit to BilelGho/analyzer that referenced this pull request Jan 26, 2023
@gabryon99 @BilelGho
Replace custom cartesian_product with BatList.cartesian_product
1345436 
See discussion: goblint#966 (comment)
jerhard
jerhard reviewed Feb 16, 2023
View reviewed changes
src/cdomains/intDomain.ml Outdated Show resolved Hide resolved
@michael-schwarz michael-schwarz self-assigned this Feb 19, 2023
@michael-schwarz michael-schwarz mentioned this pull request Feb 19, 2023
Merged
@michael-schwarz
Copy link
Member

Closing in favor of #994.

@sim642 sim642 added this to the v2.2.0 milestone Apr 5, 2023
@sim642 sim642 mentioned this pull request Sep 13, 2023
Closed
sim642 added a commit to sim642/opam-repository that referenced this pull request Sep 13, 2023
@sim642
[new release] goblint (2.2.0)
eb80bce 
CHANGES:

* Add `setjmp`/`longjmp` analysis (goblint/analyzer#887, goblint/analyzer#970, goblint/analyzer#1015, goblint/analyzer#1019).
* Refactor race analysis to lazy distribution (goblint/analyzer#1084, goblint/analyzer#1089, goblint/analyzer#1136, goblint/analyzer#1016).
* Add thread-unsafe library function call analysis (goblint/analyzer#723, goblint/analyzer#1082).
* Add mutex type analysis and mutex API analysis (goblint/analyzer#800, goblint/analyzer#839, goblint/analyzer#1073).
* Add interval set domain and string literals domain (goblint/analyzer#901, goblint/analyzer#966, goblint/analyzer#994, goblint/analyzer#1048).
* Add affine equalities analysis (goblint/analyzer#592).
* Add use-after-free analysis (goblint/analyzer#1050, goblint/analyzer#1114).
* Add dead code elimination transformation (goblint/analyzer#850, goblint/analyzer#979).
* Add taint analysis for partial contexts (goblint/analyzer#553, goblint/analyzer#952).
* Add YAML witness validation via unassume (goblint/analyzer#796, goblint/analyzer#977, goblint/analyzer#1044, goblint/analyzer#1045, goblint/analyzer#1124).
* Add incremental analysis rename detection (goblint/analyzer#774, goblint/analyzer#777).
* Fix address sets unsoundness (goblint/analyzer#822, goblint/analyzer#967, goblint/analyzer#564, goblint/analyzer#1032, goblint/analyzer#998, goblint/analyzer#1031).
* Fix thread escape analysis unsoundness (goblint/analyzer#939, goblint/analyzer#984, goblint/analyzer#1074, goblint/analyzer#1078).
* Fix many incremental analysis issues (goblint/analyzer#627, goblint/analyzer#836, goblint/analyzer#835, goblint/analyzer#841, goblint/analyzer#932, goblint/analyzer#678, goblint/analyzer#942, goblint/analyzer#949, goblint/analyzer#950, goblint/analyzer#957, goblint/analyzer#955, goblint/analyzer#954, goblint/analyzer#960, goblint/analyzer#959, goblint/analyzer#1004, goblint/analyzer#558, goblint/analyzer#1010, goblint/analyzer#1091).
* Fix server mode for abstract debugging (goblint/analyzer#983, goblint/analyzer#990, goblint/analyzer#997, goblint/analyzer#1000, goblint/analyzer#1001, goblint/analyzer#1013, goblint/analyzer#1018, goblint/analyzer#1017, goblint/analyzer#1026, goblint/analyzer#1027).
* Add documentation for configuration JSON schema and OCaml API (goblint/analyzer#999, goblint/analyzer#1054, goblint/analyzer#1055, goblint/analyzer#1053).
* Add many library function specifications (goblint/analyzer#962, goblint/analyzer#996, goblint/analyzer#1028, goblint/analyzer#1079, goblint/analyzer#1121, goblint/analyzer#1135, goblint/analyzer#1138).
* Add OCaml 5.0 support (goblint/analyzer#1003, goblint/analyzer#945, goblint/analyzer#1162).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@BilelGho BilelGho BilelGho left review comments

@jerhard jerhard jerhard left review comments

@sim642 sim642 Awaiting requested review from sim642

@michael-schwarz michael-schwarz Awaiting requested review from michael-schwarz

Assignees

@michael-schwarz michael-schwarz

Labels
feature practical-course Practical Course at TUM precision student-job
Projects
None yet
Milestone
v2.2.0
Development

Successfully merging this pull request may close these issues.

Add a new intDomain that deals with sets of intervals
6 participants
@gabryon99 @michael-schwarz @sim642 @jerhard @BilelGho @mfarider