Skip to content

master thesis: Taming Recursion with Three Context-Sensitive Analyses (Callstring, LoopfreeCallstring, Context Gas)#1340

Merged
michael-schwarz merged 176 commits intogoblint:masterfrom
SchiJoha:master
Apr 23, 2024
Merged

master thesis: Taming Recursion with Three Context-Sensitive Analyses (Callstring, LoopfreeCallstring, Context Gas)#1340
michael-schwarz merged 176 commits intogoblint:masterfrom
SchiJoha:master

Conversation

@SchiJoha
Copy link
Copy Markdown
Contributor

@SchiJoha SchiJoha commented Jan 26, 2024 •
edited by michael-schwarz
Loading

Implementation of three context-sensitive approaches to tame recursion:

  • call string approach in the Sharir and Pnueli sense: a call stack tracking the last k function calls is simulated and used as context. As elements on the call stack, the function definitions (classical call string) or the statements (similar to call site) are used. We also enable the choice of k = infinity.
  • Loopfree Callstring: similar to call string but with (1) the callee stored in the call stack and (2) loops of the call stack stored in a set. Consequently, the stack elements are function definitions and sets containing function definitions. Overall no function is stored twice in the stack.
  • Context Gas: analyzes the first k calls on the call stack context-sensitive. The remaining calls receive no context information.

For the call-sequence main -> f -> g -> f -> g the approaches would have the following context (and gas):

  • Callstring: (main)-> (main, f) -> (main, f, g) -> (main, f, g, f) -> (main, f, g, f, g)
  • Loopfree: (main)-> (main, f) -> (main, f, g) -> (main, {f, g}) -> (main, {f, g})
  • Context Gas (gas = 2): (Some (main-context)) gas 2 -> (Some (f context)) gas 1 -> (None) gas 0 -> (None) gas 0 -> (None) gas 0

Johanna Schinabeck and others added 30 commits October 19, 2023 10:59
added a new lifter in constraints, converted C to an option and tried…
51b197f 
… to update transfer functions (may still need some updates)
added lifter to control, added context gas in lifter, with this chang…
163123f 
…e 13 tests are failing
@SchiJoha
Merge branch 'goblint:master' into master
e7610f3
changed constraints, added test case, not working if context gas = 0
7f6f3e0
Merge branch 'master' of https://github.com/SchiJoha/GobContextGas
8109fbb
just checking if the tests in github actions are now working :)), not…
9347703 
…hing major new happend
added two testcases; fixed a copy paste error in query; deleted debug…
c861d29 
…ging prints; made it compact and nice
@SchiJoha
Merge branch 'goblint:master' into master
2334b73
removed prints for clean output
badfe3b
status after the 2. meeting with supervisor
4b89cd1
changed module C, no compiler errors, but implementations are not com…
e5de165 
…plete yet
converted D to a Product with an Int, same for C, changed the transfe…
ac289ee 
…r functions; code is running for simple example, improvement for the int modules need still to be done
@SchiJoha
Merge branch 'goblint:master' into master
9d80e8f
moved int Printable and lattice to the corresponding file; added and…
4fdb9bc 
… improved testcases
Merge branch 'master' of https://github.com/SchiJoha/GobContextGas
aea2345
adapted to changes from Master: added multiple
6fb946b
fixed small error at enter transfer function; now decrement should wo…
b72e941 
…rk properly; only issue:1 decrement too much
@SchiJoha
Merge branch 'goblint:master' into master
85cf293
Merge branch 'master' of https://github.com/SchiJoha/GobContextGas
c346894
test if not working github tests are due to longjmpLifter
fb5642f
Longjump enabled, working
faab50f
moved contextGasLifter upwards, hopefully fixes some of the regressio…
f5b5af1 
…n tests
made context lifter optional; added option to test cases
47e7577
adapted the hardcoded path in test-gobview to match with this reposit…
9aa8a5e 
…ory (this should make the gobview test work); changed the testcase recursion depth (this should make the regression tests work)
used Chain for ctxGasLifter (deleted Int module in Printable and Latt…
a9eaeb4 
…ice), ana.opt.ctx_gas -> ana.context.ctx_gas; made html output of context gas prettier (by overwriting Prod), added and adapted testcases
fixed indentation, added kCallstring module, just a first draft
80eee49
pulled Master, resolved merge conflict
daac0cd
added kCallstring to goblint_lib; fixed indentation
df56220
fixed typo in file name; added new testcases; adapted existing ones
fe41d6b
@SchiJoha
Merge branch 'goblint:master' into master
b82cd6b
@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Apr 17, 2024 •
edited
Loading

Is this ready for a new review (and merging) or are there still things you're working on?

@SchiJoha
Copy link
Copy Markdown
Contributor Author

SchiJoha commented Apr 17, 2024

Is this ready for a new review (and merging) or are there still things you're working on?

Yes! It should be ready for review :)

michael-schwarz
michael-schwarz reviewed Apr 17, 2024
View reviewed changes
michael-schwarz
michael-schwarz reviewed Apr 17, 2024
View reviewed changes
update description: callString_length is only effective with activate…
cefc1e2 
…d analysis; fixed typo in loopfree callstring comment
sim642
sim642 approved these changes Apr 18, 2024
View reviewed changes
@sim642 sim642 added this to the v2.4.0 milestone Apr 18, 2024
@michael-schwarz @sim642
Formatting suggestion by Simmo
97d5ad2 
Co-authored-by: Simmo Saan <simmo.saan@gmail.com>
@michael-schwarz
Copy link
Copy Markdown
Member

michael-schwarz commented Apr 19, 2024

@jerhard @DrMichaelPetter do you still want to review this or should we merge it?

@michael-schwarz michael-schwarz removed the request for review from DrMichaelPetter April 19, 2024 12:39
@michael-schwarz michael-schwarz mentioned this pull request Apr 21, 2024
Open
@sim642 sim642 mentioned this pull request Apr 22, 2024
Merged
jerhard
jerhard reviewed Apr 22, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jerhard jerhard left a comment

Choose a reason for hiding this comment

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

Looks good! I only have some cosmetical suggestions for the code.

@michael-schwarz michael-schwarz merged commit 5a389f4 into goblint:master Apr 23, 2024
michael-schwarz added a commit that referenced this pull request Apr 23, 2024
@michael-schwarz
Indentation PR #1340
ea1ec43
@michael-schwarz michael-schwarz mentioned this pull request Jun 12, 2024
Merged
2 tasks
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

@jerhard jerhard jerhard left review comments

@sim642 sim642 sim642 approved these changes

@michael-schwarz michael-schwarz michael-schwarz approved these changes

Assignees

No one assigned

Labels

feature performance Analysis time, memory usage precision student-job

Projects

None yet

Milestone

v2.4.0

Development

Successfully merging this pull request may close these issues.

Support for k-callstring & Evaluate different approaches to context-sensitivity

5 participants

@SchiJoha @michael-schwarz @sim642 @jerhard @github-advanced-security