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

Refactor setjmp/longjmp analysis #1015

Merged
merged 70 commits into from
Mar 22, 2023
Merged

Refactor setjmp/longjmp analysis #1015

merged 70 commits into from
Mar 22, 2023

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Mar 17, 2023 •
edited
Loading

This is my ongoing attempt to polish #970 for merging. It includes #970 and is currently against master to see the overall diff, but later it might be good to switch this to be against #970 to see the diff only on top of that.

Overall diff between master and this: master...longjmp-refactor. Might be nicer to look at since it reverts some of the changes in #970.

Changes

  1. Remove longjmp-related CFG nodes and create constraint variables for those directly.
  2. Use ControlSpecC instead of context hashes for better type safety.
  3. Extract longjmp logic from FromSpec into LongjmpLifter.
  4. Remove the need for longjmpthrough argument on combine, making the implementation closer to paper.
  5. Fix some failing tests on Analysis of longjmp/setjmp #970.
  6. Use Access events instead of reimplementing that logic.

sim642 added 23 commits March 15, 2023 11:56
@sim642
Add C argument to GVarF
9681d36
@sim642
Add longjmpto and longjmpret to GVarF
e3dc81b
@sim642
Add D argument to GVarG
7c6a154
@sim642
Add local domain to GVarG
d02a85a
@sim642
Replace LongjmpTo node with longjmpto global
dd47104
@sim642
Replace LongjmpFromFunction node with longjmpret global
3125e06
@sim642
Remove now unnecessary LongjmpTo and LongjmpFromFunction nodes
f4ec418
@sim642
Extract ControlSpecC to file module to allow dependency cycle breaking
6d0e55d
@sim642
Don't use hash for longjmp
1f7424f
@sim642
Make longjmpthrough argument non-optional
5511e85 
Fixes witness lifter not passing the argument
@sim642
Do return before longjmpret
3a1a173
@sim642
Add separate longjmp_return variable
4b249c1
@sim642
Remove now unnecessary longjmpthrough
76edb0e
@sim642
Merge branch 'longjmp' into longjmp-refactor
d1c7796
@sim642
Move longjmp modified locals warning to setjmp
3964ccb
@sim642
Fix longjmp modified vars warning locations in test
de36d50
@sim642
Move longjmp poisoning to setjmp
a1f3db3
@sim642
Remove longjmp target node statement matching
3f76a99
@sim642
Clean up longjmp handling in tf_normal_call
47f4287
@sim642
Clean up longjmp handling in tf_special_call
16f5619
@sim642
Clean up setjmp handling in tf_special_call
b5d0548
@sim642
Fixes in tf_normal_call longjmp handling
c0ec4e4
@sim642
Unify normal and longjmp combine
7e70553
@sim642 sim642 added cleanup Refactoring, clean-up bug unsound type-safety Type-safety improvements pr-dependency Depends or builds on another PR, which should be merged before labels Mar 17, 2023
@sim642 sim642 self-assigned this Mar 17, 2023
@sim642 sim642 mentioned this pull request Mar 20, 2023
Merged
10 tasks
@michael-schwarz michael-schwarz linked an issue Mar 21, 2023 that may be closed by this pull request
Exploit malloc uniqueness for assignments of struct members as well #1006
Closed
@sim642 sim642 changed the base branch from master to longjmp March 21, 2023 14:32
@sim642 sim642 marked this pull request as ready for review March 21, 2023 14:54
@sim642 sim642 requested a review from michael-schwarz March 21, 2023 14:54
@michael-schwarz
Copy link
Member

michael-schwarz commented Mar 21, 2023 •
edited
Loading

Impressive refactoring, great job @sim642! 👏 👏 👏

If we manage to fix the issue with combines in longjmps incorrectly modifying the LHS, I think this is ready to be merged into https://github.com/goblint/analyzer/tree/longjmp and that into master.

@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Mar 22, 2023
@sim642 sim642 merged commit 1f38378 into longjmp Mar 22, 2023
@sim642 sim642 deleted the longjmp-refactor branch March 22, 2023 09:32
@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

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

Assignees

@sim642 sim642

Labels
bug cleanup Refactoring, clean-up type-safety Type-safety improvements unsound
Projects
None yet
Milestone
v2.2.0
Development

Successfully merging this pull request may close these issues.

Exploit malloc uniqueness for assignments of struct members as well
2 participants
@sim642 @michael-schwarz