@@ -146,6 +146,31 @@ module SsaFlow {
146
146
}
147
147
}
148
148
149
+ /**
150
+ * Holds for expressions `e` that evaluate to the value of any last (in
151
+ * evaluation order) subexpressions within it. E.g., expressions that propagate
152
+ * a values from a subexpression.
153
+ *
154
+ * For instance, the predicate holds for if expressions as `if b { e1 } else {
155
+ * e2 }` evalates to the value of one of the subexpressions `e1` or `e2`.
156
+ */
157
+ predicate propagatesValue ( Expr e ) {
158
+ e instanceof IfExpr or
159
+ e instanceof LoopExpr or
160
+ e instanceof ReturnExpr or
161
+ e instanceof BreakExpr or
162
+ e .( BlockExpr ) .getStmtList ( ) .hasTailExpr ( ) or
163
+ e instanceof MatchExpr
164
+ }
165
+
166
+ module LocalFlow {
167
+ pragma [ nomagic]
168
+ predicate localFlowStepCommon ( Node nodeFrom , Node nodeTo ) {
169
+ propagatesValue ( nodeTo .( Node:: ExprNode ) .asExpr ( ) ) and
170
+ nodeFrom .getCfgNode ( ) .getASuccessor ( ) = nodeTo .getCfgNode ( )
171
+ }
172
+ }
173
+
149
174
module RustDataFlow implements InputSig< Location > {
150
175
/**
151
176
* An element, viewed as a node in a data flow graph. Either an expression
@@ -359,6 +384,8 @@ private module Cached {
359
384
/** This is the local flow predicate that is exposed. */
360
385
cached
361
386
predicate localFlowStepImpl ( Node:: Node nodeFrom , Node:: Node nodeTo ) {
387
+ LocalFlow:: localFlowStepCommon ( nodeFrom , nodeTo )
388
+ or
362
389
SsaFlow:: localFlowStep ( _, nodeFrom , nodeTo , _)
363
390
}
364
391
}
0 commit comments