@@ -146,6 +146,31 @@ module SsaFlow {
146146 }
147147}
148148
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+
149174module RustDataFlow implements InputSig< Location > {
150175 /**
151176 * An element, viewed as a node in a data flow graph. Either an expression
@@ -359,6 +384,8 @@ private module Cached {
359384 /** This is the local flow predicate that is exposed. */
360385 cached
361386 predicate localFlowStepImpl ( Node:: Node nodeFrom , Node:: Node nodeTo ) {
387+ LocalFlow:: localFlowStepCommon ( nodeFrom , nodeTo )
388+ or
362389 SsaFlow:: localFlowStep ( _, nodeFrom , nodeTo , _)
363390 }
364391}
0 commit comments