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

Match statements do not propagate control flow #105

Open
livia01px2019 opened this issue Nov 7, 2023 · 0 comments
Open

Match statements do not propagate control flow #105

livia01px2019 opened this issue Nov 7, 2023 · 0 comments
Labels
bug Something isn't working flow-analysis Concerns the PDG construction component

Comments

@livia01px2019
Copy link
Collaborator

livia01px2019 commented Nov 7, 2023

Paralegal doesn't correctly propagate control flow relations when match statements are involved.

This is causing the Atomic property to fail: the add_resource_opts call here does not see the control-flow influence from the check_write call here due to the fact that it is wrapped in an if let.

Consider the following minimal examples:

#[paralegal::analyze]
pub fn minimal_match(&self, i: AtomicResult<i64>, j: i64, k: bool) {
    if self.is_ok(j).is_ok() {
        match Some(k) {
            Some(k) => self.store(j),
            None => (),
        };
    }
}

#[paralegal::analyze]
pub fn minimal_no_match(&self, i: AtomicResult<i64>, j: i64, k: bool) {
    if self.is_ok(j).is_ok() {
        if k {
            self.store(j);
        }
    }
}

We expect that in both examples is_ok has control-flow influence on store. However, these are the corresponding graphs:

With match:
minimal_match_76201e.inlined-pruned.gv.pdf

Without match:
minimal_no_let_a24bcc.inlined-pruned.gv.pdf

With match, there is no control-flow influence anywhere.

Here is the MIR for the code with the match -- I believe the control-flow influence is there, but it's not captured in our SPDG.
minimal_match.mir.gv.pdf

@livia01px2019 livia01px2019 added the bug Something isn't working label Nov 8, 2023
@JustusAdam JustusAdam added the flow-analysis Concerns the PDG construction component label Nov 19, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working flow-analysis Concerns the PDG construction component
Projects
None yet
Development

No branches or pull requests

2 participants