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

Stacked Borrows In Kani -- Extend Feature to handle more code #3475

Open
jsalzbergedu opened this issue Aug 30, 2024 · 2 comments
Open

Stacked Borrows In Kani -- Extend Feature to handle more code #3475

jsalzbergedu opened this issue Aug 30, 2024 · 2 comments
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.

Comments

@jsalzbergedu
Copy link
Contributor

jsalzbergedu commented Aug 30, 2024 •
edited
Loading

Currently, Stacked Borrows is implemented in the feature branch features/stacked_borrows.
However, to merge it into the main code-base, the following updates are needed:

  1. We need to add regression tests for and implement the following syntactic constructs:
  • Function calls
  • Moving pointers
  • Copying pointers
  1. We need to have an extensive suite of regression tests, including
  • Tests on the standard library
  • Some of MIRI's regression tests
  • Complex tests of our own design

And we ought to see if Kani can find aliasing model violations in codebases that MIRI has not yet.
@jsalzbergedu jsalzbergedu added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Aug 30, 2024
@jsalzbergedu
Copy link
Contributor Author

We also need to overcome the following limitations:

  • Model malloc,
  • Model pointer manipulation,
  • Model two phase borrows,
  • Model function calls and closures.

@jsalzbergedu
Copy link
Contributor Author

The stacked borrows model also currently does not handle function contracts; if relational data is checked in the pre and post conditions, then because we only check one byte currently, there is no way to check it. Many function contracts however may work, and so testing will need to confirm these boundaries.

Also it should be possible to disable demonic nondeterminism, and it isn't currently.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@jsalzbergedu