Skip to content

Pass ctx to context & Simplify callstring-based approaches #1427

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
Merged
merged 8 commits into from
May 20, 2024
Merged

Pass ctx to context & Simplify callstring-based approaches #1427

merged 8 commits into from
May 20, 2024

Conversation

@michael-schwarz
Copy link
Member

@michael-schwarz michael-schwarz commented Apr 23, 2024 •
edited
Loading

  • Pass ctx as additional argument to context
  • Simplify callstring-based approaches to not track callstring in local state
  • Simplify loopfree callstring
  • Investigate how this works with context failing for startvars

Closes #1379.

@michael-schwarz michael-schwarz added cleanup Refactoring, clean-up in progress performance Analysis time, memory usage labels Apr 23, 2024
@michael-schwarz
Copy link
Member Author

michael-schwarz commented Apr 23, 2024

This changes the behavior for function calls somewhat, in the sense that new threads start with an empty callstring.

@michael-schwarz michael-schwarz marked this pull request as ready for review April 23, 2024 08:02
sim642
sim642 reviewed Apr 23, 2024
View reviewed changes
jerhard
jerhard reviewed Apr 23, 2024
View reviewed changes
@michael-schwarz michael-schwarz added this to the v2.4.0 milestone Apr 26, 2024
sim642
sim642 approved these changes May 20, 2024
View reviewed changes
@michael-schwarz @sim642
Rm spurious comments
9084ba4 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@michael-schwarz michael-schwarz merged commit ede09b8 into master May 20, 2024
@michael-schwarz michael-schwarz deleted the issue_1379 branch May 20, 2024 10:56
This was referenced May 21, 2024
Closed
Merged
sim642 added a commit to sim642/opam-repository that referenced this pull request Aug 2, 2024
@sim642
[new release] goblint (2.4.0)
38186e2 
CHANGES:

* Remove unmaintained analyses: spec, file (goblint/analyzer#1281).
* Add linear two-variable equalities analysis (goblint/analyzer#1297, goblint/analyzer#1412, goblint/analyzer#1466).
* Add callstring, loopfree callstring and context gas analyses (goblint/analyzer#1038, goblint/analyzer#1340, goblint/analyzer#1379, goblint/analyzer#1427, goblint/analyzer#1439).
* Add non-relational thread-modular value analyses with thread IDs (goblint/analyzer#1366, goblint/analyzer#1398, goblint/analyzer#1399).
* Add NULL byte array domain (goblint/analyzer#1076).
* Fix spurious overflow warnings from internal evaluations (goblint/analyzer#1406, goblint/analyzer#1411, goblint/analyzer#1511).
* Refactor non-definite mutex handling to fix unsoundness (goblint/analyzer#1430, goblint/analyzer#1500, goblint/analyzer#1503, goblint/analyzer#1409).
* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (goblint/analyzer#1457, goblint/analyzer#1458).
* Fix mutex type analysis unsoundness and enable it by default (goblint/analyzer#1414, goblint/analyzer#1416, goblint/analyzer#1510).
* Add points-to set refinement on mutex path splitting (goblint/analyzer#1287, goblint/analyzer#1343, goblint/analyzer#1374, goblint/analyzer#1396, goblint/analyzer#1407).
* Improve narrowing operators (goblint/analyzer#1502, goblint/analyzer#1540, goblint/analyzer#1543).
* Extract automatic configuration tuning for soundness (goblint/analyzer#1369).
* Fix many locations in witnesses (goblint/analyzer#1355, goblint/analyzer#1372, goblint/analyzer#1400, goblint/analyzer#1403).
* Improve output readability (goblint/analyzer#1294, goblint/analyzer#1312, goblint/analyzer#1405, goblint/analyzer#1497).
* Refactor logging (goblint/analyzer#1117).
* Modernize all library function specifications (goblint/analyzer#1029, goblint/analyzer#688, goblint/analyzer#1174, goblint/analyzer#1289, goblint/analyzer#1447, goblint/analyzer#1487).
* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (goblint/analyzer#1448).
@sim642 sim642 mentioned this pull request Aug 2, 2024
Merged
avsm pushed a commit to avsm/opam-repository that referenced this pull request Sep 5, 2024
@sim642 @avsm
[new release] goblint (2.4.0)
2afe816 
CHANGES:

* Remove unmaintained analyses: spec, file (goblint/analyzer#1281).
* Add linear two-variable equalities analysis (goblint/analyzer#1297, goblint/analyzer#1412, goblint/analyzer#1466).
* Add callstring, loopfree callstring and context gas analyses (goblint/analyzer#1038, goblint/analyzer#1340, goblint/analyzer#1379, goblint/analyzer#1427, goblint/analyzer#1439).
* Add non-relational thread-modular value analyses with thread IDs (goblint/analyzer#1366, goblint/analyzer#1398, goblint/analyzer#1399).
* Add NULL byte array domain (goblint/analyzer#1076).
* Fix spurious overflow warnings from internal evaluations (goblint/analyzer#1406, goblint/analyzer#1411, goblint/analyzer#1511).
* Refactor non-definite mutex handling to fix unsoundness (goblint/analyzer#1430, goblint/analyzer#1500, goblint/analyzer#1503, goblint/analyzer#1409).
* Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (goblint/analyzer#1457, goblint/analyzer#1458).
* Fix mutex type analysis unsoundness and enable it by default (goblint/analyzer#1414, goblint/analyzer#1416, goblint/analyzer#1510).
* Add points-to set refinement on mutex path splitting (goblint/analyzer#1287, goblint/analyzer#1343, goblint/analyzer#1374, goblint/analyzer#1396, goblint/analyzer#1407).
* Improve narrowing operators (goblint/analyzer#1502, goblint/analyzer#1540, goblint/analyzer#1543).
* Extract automatic configuration tuning for soundness (goblint/analyzer#1369).
* Fix many locations in witnesses (goblint/analyzer#1355, goblint/analyzer#1372, goblint/analyzer#1400, goblint/analyzer#1403).
* Improve output readability (goblint/analyzer#1294, goblint/analyzer#1312, goblint/analyzer#1405, goblint/analyzer#1497).
* Refactor logging (goblint/analyzer#1117).
* Modernize all library function specifications (goblint/analyzer#1029, goblint/analyzer#688, goblint/analyzer#1174, goblint/analyzer#1289, goblint/analyzer#1447, goblint/analyzer#1487).
* Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (goblint/analyzer#1448).
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

@jerhard jerhard jerhard approved these changes

Assignees

No one assigned

Labels

cleanup Refactoring, clean-up performance Analysis time, memory usage

Projects

None yet

Milestone

v2.4.0

Development

Successfully merging this pull request may close these issues.

First-Class Support for Callstring-derived Contexts

4 participants

@michael-schwarz @sim642 @jerhard