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.

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

[PDG] Field-precision lost on function entry. #94

Open
JustusAdam opened this issue Feb 13, 2024 · 0 comments
Open

[PDG] Field-precision lost on function entry. #94

JustusAdam opened this issue Feb 13, 2024 · 0 comments

Comments

@JustusAdam
Copy link
Contributor

JustusAdam commented Feb 13, 2024

Entering a function causes the field-level precision to be lost if the child function does not access the fields. The following example illustrates this

fn id_fun<T, G>(obj: (T, G)) -> (T, G) {
    obj
}

fn no_overtaint_over_fn_call() {
    let p = input();
    let q = input();
    let t = id_fun((p, q));
    read(t.0);
    read2(t.1);
}

// external functions
fn input() -> usize;
fn read<T>(recv1: T);
fn read2<T>(recv2: T);

The PDG shows paths p -> recv2 and q -> recv1, which are caused because obj is tracked as a single object. E.g. there are edges p -> obj and q -> obj as well as obj -> revc1 and obj -> recv2.

That is to say the PDG for id_fun does not track obj.0 and obj.1 as separate nodes and as a result the caller loses that precision also.

The same effect can be observed for nested functions, e.g.

fn main() {
    let p = input();
    let q = input();
    forwarder((p, q));
}

fn forwarder(t: (usize, usize)) {
    acceptor(t)
}

fn acceptor(b: (usize, usize)) {
    read(b.0);
    read2(b.1);
}

Here we observe p -> t and q -> t as well as t -> b.0 and t -> b.1. What we would expect is p -> t.0 -> b.0 and q -> t.1 -> b.1.

JustusAdam added a commit to brownsys/paralegal that referenced this issue Feb 14, 2024
Unified test template with skip template, now uses #[ignore]
Test template instantiations now simply forward fragments
Marker tests are skipped completely for now
Debugged last tests cases, issues are reported in willcrichton/flowistry#93 and willcrichton/flowistry#94
Fixed propagating marker skip from async function to their generators
Added new test cases for discovered issues
JustusAdam added a commit to brownsys/paralegal that referenced this issue Feb 14, 2024
JustusAdam added a commit to brownsys/paralegal that referenced this issue Feb 21, 2024
## What Changed?

- Data and control flow graph construction moves into the Flowistry
crate.
- Removes `df`, inlining logic and the algebra.
- Entails an update of the rustc toolchain (to achieve parity with
flowistry).
- Graph contains all program locations, not just function calls.
- Control flow is non-transitive
- The PDG now tracks individual places instead of abstract function
arguments. This improves field sensitivity across function calls.
- Forge output is gone

## Why Does It Need To?

Field sensitivity is now handled as the initial analysis constructs the
PDG and in fewer lines of code.

## Caveats

At the time of this merge, the following regressions in the PDG have not
been fixed yet

- willcrichton/flowistry#95
- willcrichton/flowistry#94
- willcrichton/flowistry#93
- And while Will fixed the strong updates
willcrichton/flowistry#90 the second issue
mentioned there is still present.

## 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
- [ ] 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant