Skip to content

Add Interval Set domain for Interval Set analysis#994

Merged
michael-schwarz merged 140 commits intomasterfrom
IntervalSets
Mar 21, 2023
Merged

Add Interval Set domain for Interval Set analysis#994
michael-schwarz merged 140 commits intomasterfrom
IntervalSets

Conversation

@michael-schwarz
Copy link
Copy Markdown
Member

@michael-schwarz michael-schwarz commented Feb 19, 2023

Copy of #966, as that PR does not allow us to commit directly to it.

Original PR:

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

Closes #901.

BilelGho and others added 30 commits February 16, 2023 16:45
@BilelGho @mfarider @gabryon99
Implement skeleton of IntervalSet
0e916c8 
Co-authored-by: mfarider <mfarider@users.noreply.github.com>
Co-authored-by: Gabriele Pappalardo <leleattolo99@gmail.com>
@mfarider @BilelGho
add helper functions
bf4f2ea
@mfarider @BilelGho
add leq
b9b018d
@BilelGho
Implementing meet and join using sweeping line algorithm
943e7dd
@mfarider @BilelGho
add add
c60c215
@mfarider @BilelGho
add mul
2641114
@mfarider @BilelGho
add sub
44d9c18
@gabryon99 @BilelGho
implement show function for IntervalSetFunctor
b528e06
@BilelGho
implement bottom
7af0cc9
@gabryon99 @BilelGho
fix type error for IntervalSetFunctor.mul function
94449e9 
* code from IntervalFunctor has been reused
@gabryon99 @BilelGho
re-implementing arithmetic operations based on IntervalSet ones
4118f12
@gabryon99 @BilelGho
implements remaining binary and unary operators for IntervalSetFunctor
73671a4
@gabryon99 @BilelGho
add analysis support for interval_set
f228575
@gabryon99 @BilelGho
fix description
63acd73
@BilelGho
fixup! Implement skeleton of IntervalSet
57b333b
@BilelGho
implement canonize
78ced0f
@BilelGho
implement cast_to
a51db3c
@BilelGho
implement refine_with_interval
9b102c3
@BilelGho
implement refine_with_incl_list
6a49d68
@BilelGho
implement refine_with_excl_list
9e9091a
@BilelGho
implement invariant_ikind
2b65e9c
@BilelGho
implement refine with congruence
1b549cd
@BilelGho
implement widen
48f4be5
@BilelGho
implement project
f9aec6f
@BilelGho
implement arbitrary
de2c921
@BilelGho
implement narrow
2280b42
@BilelGho
add TODO
307e8a8
@gabryon99 @BilelGho
Running Interval Set Analysis and fixing bugs
b8e0312
@gabryon99 @BilelGho
Fix and fix
4bcb0de
@BilelGho
remove duplicates
96efa73
@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Feb 19, 2023

I have now cleaned up some things as opposed to #994 w.r.t. to code style and some unnecessary complications such as passing around cast everywhere. Would be great if someone could have a look to ensure I didn't break anything in the process.

sim642
sim642 reviewed Feb 20, 2023
View reviewed changes
@michael-schwarz michael-schwarz requested a review from sim642 March 14, 2023 09:26
@michael-schwarz
Copy link
Copy Markdown
Member Author

michael-schwarz commented Mar 14, 2023

I would propose to merge this soon, in the interest of avoiding having such a huge PR go stale (and this becoming the third attempt at interval sets that ends up not being merged).

This does not prevent us from doing refactoring to maximize reuse at a later point.

jerhard
jerhard reviewed Mar 15, 2023
View reviewed changes
sim642
sim642 approved these changes Mar 21, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@sim642 sim642 left a comment

Choose a reason for hiding this comment

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

All the comments have been resolved, so I guess this should be in good enough state to merge.

I'll adapt #943 accordingly after this is merged.

@michael-schwarz michael-schwarz merged commit a2997db into master Mar 21, 2023
@michael-schwarz michael-schwarz deleted the IntervalSets branch March 21, 2023 12:15
michael-schwarz added a commit that referenced this pull request Mar 21, 2023
@michael-schwarz
Fix indentation #994
724eb54
sim642 added a commit that referenced this pull request Mar 22, 2023
@sim642
Add qcheck-core 0.19 lower bound for tup5 (PR #994)
52ce96d
@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

@jerhard jerhard jerhard left review comments

@sim642 sim642 sim642 approved these changes

Assignees

@michael-schwarz michael-schwarz

Labels

feature practical-course Practical Course at TUM precision

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

@michael-schwarz @sim642 @jerhard @BilelGho @mfarider @gabryon99