-
Notifications
You must be signed in to change notification settings - Fork 2
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.
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
When should type markers be attached? #129
Comments
JustusAdam
added
markers
Concerns the assignment logic for markers
semantics
Clarification on what is "correct behavior" is needed or improvement of its implementation
labels
Feb 24, 2024
JustusAdam
added a commit
that referenced
this issue
Apr 6, 2024
## What Changed? Updates the marker assignment algorithm. It now attaches to a node `n` 1. all markers for `typeof(n)` 2. If `children(n).is_empty()` (determined by flowistry’s `PlaceInfo`) then we must be a terminal place where subplaces aren’t tracked, meaning that they won’t be marked via rule 1 and we have to overtaint, so include all markers from `subtypes(typeof(n))` 3. Add all markers from `n.iter_projections().map(typeof)` to mark ourselves if we are a field of a tainted type. ## Why Does It Need To? This implements an updated marker policy. It simplifies the semantics and makes them sound hopefully. This is possible now because we have much better field sensitivity. Markers are now attached to every node of the marked type as well as - nodes which are children (e.g. fields) of a marked type - nodes which are parents of the marked type **if** it the children of this node are not separately tracked (overapproximation) Mostly implements #129 ## 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 - [ ] 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. --------- Co-authored-by: Will Crichton <[email protected]>
This was referenced May 1, 2024
Merged
JustusAdam
added a commit
that referenced
this issue
May 2, 2024
## What Changed? - Improves soundness of marker assignment logic. - Refactors the graph constructor into it's own file - The Graph query API is now accessible as methods on nodes - Implements adaptive inlining optimization - Improves error messages from parse failures for the annotations - Switches output serialization format to bincode by default - Adds a new framework and suite of tests based on the policy framework - Adds tracing to always_happens_before - Generics on entry points are now handled by providing arguments of type `dyn <constraints>` - Adds statistics on runtime to flow analyzer and policies - Materialized `flows_to` relations are now optional - Diagnostics are now deduplicated ## Why Does It Need To? Improves soundness, ergonomics and speed. Fixes #129 Fixes #130 ## Checklist - [x] Above description has been filled out so that upon quash merge we have a good record of what changed. - [ ] New functions, methods, types are documented. Old documentation is updated if necessary - [ ] Documentation in Notion has been updated - [ ] Tests for new behaviors are provided - [ ] 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. --------- Co-authored-by: Carolyn Zech <[email protected]> Co-authored-by: Will Crichton <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
In #119 we decided to restore the old behavior on when markers are attached to types. This means a value only gets marked with it's type if it the return value of an external or marked function or if it is input to a controller.
Update: The old policy was unsound. Marker semantics have been made consistent and simplified. This is made possible by improved field sensitivity. Markers are now attached to every node of the marked type as well as
There are some residual questions as to how references are handled. For instance in the following case, should
c
be considered marked?The text was updated successfully, but these errors were encountered: