Rust: Propagate data flow through a few expression types

This commit is contained in:
Simon Friis Vindum
2024-11-01 16:11:40 +01:00
parent 2bab29d31b
commit 82076ee0b8
2 changed files with 38 additions and 0 deletions

View File

@@ -146,6 +146,31 @@ module SsaFlow {
}
}
/**
* Holds for expressions `e` that evaluate to the value of any last (in
* evaluation order) subexpressions within it. E.g., expressions that propagate
* a values from a subexpression.
*
* For instance, the predicate holds for if expressions as `if b { e1 } else {
* e2 }` evalates to the value of one of the subexpressions `e1` or `e2`.
*/
predicate propagatesValue(Expr e) {
e instanceof IfExpr or
e instanceof LoopExpr or
e instanceof ReturnExpr or
e instanceof BreakExpr or
e.(BlockExpr).getStmtList().hasTailExpr() or
e instanceof MatchExpr
}
module LocalFlow {
pragma[nomagic]
predicate localFlowStepCommon(Node nodeFrom, Node nodeTo) {
propagatesValue(nodeTo.(Node::ExprNode).asExpr()) and
nodeFrom.getCfgNode().getASuccessor() = nodeTo.getCfgNode()
}
}
module RustDataFlow implements InputSig<Location> {
/**
* An element, viewed as a node in a data flow graph. Either an expression
@@ -359,6 +384,8 @@ private module Cached {
/** This is the local flow predicate that is exposed. */
cached
predicate localFlowStepImpl(Node::Node nodeFrom, Node::Node nodeTo) {
LocalFlow::localFlowStepCommon(nodeFrom, nodeTo)
or
SsaFlow::localFlowStep(_, nodeFrom, nodeTo, _)
}
}

View File

@@ -0,0 +1,11 @@
| main.rs:9:21:11:5 | BlockExpr | main.rs:9:13:13:5 | IfExpr |
| main.rs:10:9:10:9 | a | main.rs:9:21:11:5 | BlockExpr |
| main.rs:11:12:13:5 | BlockExpr | main.rs:9:13:13:5 | IfExpr |
| main.rs:12:9:12:9 | b | main.rs:11:12:13:5 | BlockExpr |
| main.rs:14:5:14:5 | c | main.rs:6:37:15:1 | BlockExpr |
| main.rs:20:9:20:15 | BreakExpr | main.rs:19:13:21:5 | LoopExpr |
| main.rs:20:15:20:15 | a | main.rs:20:9:20:15 | BreakExpr |
| main.rs:22:5:22:5 | b | main.rs:17:29:23:1 | BlockExpr |
| main.rs:26:5:29:5 | MatchExpr | main.rs:25:60:30:1 | BlockExpr |
| main.rs:27:20:27:20 | a | main.rs:26:5:29:5 | MatchExpr |
| main.rs:28:17:28:17 | b | main.rs:26:5:29:5 | MatchExpr |