-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Handling of foreign functions that may execute local code (#164)
## What Changed? - Adds checks which ensure that if foreign functions may call local code, it is sound, e.g. the code they can call cannot attach markers. - Adds a basic flow-model whitelist, which can be used to replace foreign calls with specific methods of the traits they are parameterized over. ## Why Does It Need To? The main use case here is if the local code calls a higher-order function, then we should ensure that we don't miss any markers as a result. Here is a simple example from out test cases. ```rs #[paralegal::marker(attached, return)] fn attach() -> usize { 0 } #[paralegal::analyze] fn main() { std::thread::spawn(|| attach()); } ``` Our analysis would miss the `attached` marker, because it doesn't know the body of `thread::spawn` (and even if it did, it wouldn't help but more on that later). But there is a more general pattern here, which is if any foreign function `foo` is parameterized by a trait `T` which we locally implement, then a method on that trait might attach markers. So step one is to reject such calls to foreign function. If we did that for all of them however that would cause a lot of false rejection. Instead we should only reject this if the trait implementation that it might target is known to attach a marker and therefore cause an unsoundness issue. But, as mentioned before we wouldn't be able to actually analyze `thread::spawn`, even if we had access to be body. Underneath it does some low-level stuff that Paralegal can't actually handle. However semantically it's quite simple we could basically replace `thread::spawn(foo)` with `foo()` (and `join` with `identity`). So step two is to add an interface to whitelist a set of commonly used higher order function and define some simple rewrite rules, e.g. `thread::spawn(foo) => foo()`. ## Checklist - [x] Above description has been filled out so that upon quash merge we have a good record of what changed. - [x] New functions, methods, types are documented. Old documentation is updated if necessary - [ ] Documentation in Notion has been updated - [x] Tests for new behaviors are provided - [x] New test suites (if any) ave been added to the CI tests (in `.github/workflows/rust.yml`) either as compiler test or integration test. *Or* justification for their omission from CI has been provided in this PR description.
- Loading branch information
1 parent
a4ca7a0
commit df19b1e
Showing
27 changed files
with
1,063 additions
and
264 deletions.
There are no files selected for viewing
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.