Skip to content

Only pass stable reluctant_vs to postsolver#960

Merged
jerhard merged 3 commits intomasterfrom
issue_959
Dec 27, 2022
Merged

Only pass stable reluctant_vs to postsolver#960
jerhard merged 3 commits intomasterfrom
issue_959

Conversation

@jerhard
Copy link
Copy Markdown
Member

@jerhard jerhard commented Dec 23, 2022

This ensures that only those unknowns that were collected in reluctant_vs are passed to the postsolver, that are stable. This is necessary because it may happen that unknowns that were reluctantly destabilized and didn't cause further destabilization are actually not reachable after the final solve.

This set of stable reluctant_vs is now also used for computing reachable_and_superstable.

Closes #959

@jerhard
Reluctant incremental analysis: only pass stable reluctant_vs to post…
5b9503d 
…solver.

Previously, the postsolver reported unreached fixpoints when also unstable unknowns from reluctant_vs were passed to it.
@jerhard
Use stable_reluctant_vs also for reachable and superstable.
9093218
@jerhard jerhard added the bug label Dec 23, 2022
@jerhard
Copy link
Copy Markdown
Member Author

jerhard commented Dec 23, 2022

I started some runs to check whether this fixes all of the 15 cases with a "Fixpoint" issue and/or "BotValue" exception on chrony.

@jerhard
Copy link
Copy Markdown
Member Author

jerhard commented Dec 25, 2022 •
edited
Loading

This indeed fixes all occurrences of "Fixpoint" issues and "BotValue" in the efficiency results for chrony and zstd.

@jerhard jerhard merged commit 6312dd4 into master Dec 27, 2022
@jerhard jerhard deleted the issue_959 branch December 27, 2022 17:53
@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

@sim642 sim642 sim642 approved these changes

Assignees

No one assigned

Labels

bug

Projects

None yet

Milestone

v2.2.0

Development

Successfully merging this pull request may close these issues.

Reluctant incremental Goblint does not reach fixpoint on some commits of chrony

2 participants

@jerhard @sim642