llvm-project
73ded458 - [Liveness][analyzer] Fix handling of [[assume]] attributes (#198618)

Commit
4 hours ago
[Liveness][analyzer] Fix handling of [[assume]] attributes (#198618) Before this commit, if the analyzer encountered code like ``` int f(int a, int b) { [[assume(a == 2), assume(b == 3)]]; return a + b; } ``` it performed the following steps: 1. It visited the expression `a == 2` with `ExprEngine::Visit` (after visiting its sub-expressions, within the regular visitation that visits each statement of the `CFGBlock`). This triggered the `EagerlyAssume` logic and separated two execution paths. 2. It discarded the result bound to `a == 2` from the `Environment` because `a == 2` is not a direct child of the `AttributedStmt`. 3. Analogously, it visited an evaluated `b == 3`. 4. Analogously, it discarded the result bound to `b == 3`. 5. On each execution path `VisitAttributedStmt` was reached, it ran the `PreStmt<AttributedStmt>` checkers and stored their results in `CheckerPreStmt`. As there are AFAIK no such checkers, after this step the only element of `CheckerPreStmt` was the node `Pred`. 6. It constructed a `NodeBuilder`, which was unused, but its constructor inserted the nodes in `CheckerPreStmt` into `EvalSet`. This was essentially a shortcut that skipped the handling of the assumptions -- but ultimately its effects were absorbed and negated by the tricky side effects of `ExprEngine::Visit`. 7. For each node `N` in `CheckerPreStmt` (i.e. for `N == Pred`) and for each assume attribute, it created a child node of `N` where the assumption of **that one attribute** was visited again with `ExprEngine::Visit`. (I.e. it separated execution paths and implicitly placed "OR" relationships between the assumptions.) 8. It **completely ignored** the value produced by the assumption expression: did not update the state and did not discard execution paths where the [[assume]] assumption contradicted earlier knowledge. This commit fixes all four logic errors: 1. The liveness analysis is updated to ensure that an `AttributedStmt` keeps alive the assumption expressions of its [[assume]] attributes. This ensured that their results remain in the `Environment`. 2. Now there is no `NodeBuilder` that skips the handling the assumptions. 3. The invocation of `ExprEngine::Visit` is removed from `VisitAttributedStmt`: there is no reason to revisit those statements (now that we don't lose the evaluation results). 4. The state is updated to record that the values of the assumption expressions are ALL assumed to be true. If the assumption leads to a contradiction, the execution path is discarded (by not generating a node). This commit also adds a few new testcases and resolves some FIXME comments in previously existing tests.
Author
Parents
Loading