@@ -1500,22 +1500,6 @@ module Make<
15001500 */
15011501 default predicate allowFlowIntoUncertainDef ( UncertainWriteDefinition def ) { none ( ) }
15021502
1503- /**
1504- * Holds if the post-update node corresponding to the given `read` occurs at `bb,i`, meaning
1505- * it will propagate to the next use (strictly) after that point in the CFG.
1506- *
1507- * The default is to use the CFG node associated with the read itself, meaning the post-update
1508- * always flows to the next use. The default can however lead to spurious flow in cases like:
1509- * ```
1510- * x.f = foo(x)
1511- * ```
1512- * where the post-update node for `x` on the left-hand side flows into the `x` on the right-hand side.
1513- *
1514- * NOTE: When implementing this predicate, you must ensure that `variableRead` is defined to contain
1515- * a synthetic read of this variable at `bb,i`.
1516- */
1517- default predicate postUpdateCfgNode ( Expr read , BasicBlock bb , int i ) { read .hasCfgNode ( bb , i ) }
1518-
15191503 /** An abstract value that a `Guard` may evaluate to. */
15201504 class GuardValue {
15211505 /** Gets a textual representation of this value. */
@@ -1651,7 +1635,8 @@ module Make<
16511635 private predicate phiInputIsGuardEquivalentWithPreviousRef ( SsaPhiExt phi , BasicBlock input ) {
16521636 exists ( BasicBlock prev |
16531637 phiInputHasRead ( phi , input ) and
1654- AdjacentSsaRefs:: adjacentRefPhi ( prev , _, input , phi .getBasicBlock ( ) , phi .getSourceVariable ( ) ) and
1638+ AdjacentSsaRefs:: adjacentRefPhiSkipPostUpd ( prev , _, input , phi .getBasicBlock ( ) ,
1639+ phi .getSourceVariable ( ) ) and
16551640 prev = getGuardEquivalentImmediateDominator * ( input )
16561641 )
16571642 }
@@ -1693,7 +1678,7 @@ module Make<
16931678 // An equivalent, but less performant, way to express this is as follows:
16941679 // ```
16951680 // exists(BasicBlock prev |
1696- // AdjacentSsaRefs::adjacentRefPhi (prev, _, input, phi.getBasicBlock(),
1681+ // AdjacentSsaRefs::adjacentRefPhiSkipPostUpd (prev, _, input, phi.getBasicBlock(),
16971682 // phi.getSourceVariable()) and
16981683 // prev != input and
16991684 // exists(DfInput::Guard g, DfInput::GuardValue val |
@@ -1715,7 +1700,7 @@ module Make<
17151700 ) {
17161701 exists ( BasicBlock bb1 , int i , SourceVariable v , BasicBlock bb2 |
17171702 phi .definesAt ( pragma [ only_bind_into ] ( v ) , bb1 , i ) and
1718- AdjacentSsaRefs:: adjacentRefPhi ( bb1 , i , input , bb2 , v ) and
1703+ AdjacentSsaRefs:: adjacentRefPhiSkipPostUpd ( bb1 , i , input , bb2 , v ) and
17191704 phi2 .definesAt ( pragma [ only_bind_into ] ( v ) , bb2 , _) and
17201705 if relevantPhiInputNode ( phi2 , input ) then relevant = true else relevant = false
17211706 )
@@ -1729,7 +1714,7 @@ module Make<
17291714 private predicate phiStepsToRef ( SsaPhiExt phi , BasicBlock bb , int i , boolean isUse ) {
17301715 exists ( SourceVariable v , BasicBlock bb1 , int i1 |
17311716 phi .definesAt ( v , bb1 , i1 ) and
1732- AdjacentSsaRefs:: adjacentRefRead ( bb1 , i1 , bb , i , v )
1717+ AdjacentSsaRefs:: adjacentRefReadSkipPostUpd ( bb1 , i1 , bb , i , v )
17331718 |
17341719 isUse = true and
17351720 variableRead ( bb , i , v , true )
@@ -1761,15 +1746,22 @@ module Make<
17611746 cached
17621747 private newtype TNode =
17631748 TWriteDefSource ( WriteDefinition def ) { DfInput:: ssaDefHasSource ( def ) } or
1764- TExprNode ( DfInput:: Expr e , SourceVariable v , Boolean isPost ) {
1765- exists ( BasicBlock bb , int i |
1766- e .hasCfgNode ( bb , i ) and
1749+ TExprNode ( DfInput:: Expr e , SourceVariable v , boolean isPost ) {
1750+ exists ( BasicBlock bb , int i | e .hasCfgNode ( bb , i ) |
17671751 variableRead ( bb , i , v , true ) and
1768- // Only materialise if 'expr' has a reaching definition.
1769- // Note that the read may correspond to a different variable than 'v', but the C++
1770- // instantiation currently expects this particular behaviour.
1771- DfInput:: getARead ( _) = e
1772- )
1752+ isPost = false
1753+ or
1754+ not postUpdate ( _, _, _) and
1755+ variableRead ( bb , i , v , true ) and
1756+ isPost = true
1757+ or
1758+ postUpdate ( bb , i , v ) and
1759+ isPost = true
1760+ ) and
1761+ // Only materialise if 'expr' has a reaching definition.
1762+ // Note that the read may correspond to a different variable than 'v', but the C++
1763+ // instantiation currently expects this particular behaviour.
1764+ DfInput:: getARead ( _) = e
17731765 } or
17741766 TSsaDefinitionNode ( DefinitionExt def ) {
17751767 not phiHasUniqNextNode ( def ) and
@@ -1857,7 +1849,17 @@ module Make<
18571849 ExprPostUpdateNodeImpl ( ) { isPost = true }
18581850
18591851 /** Gets the pre-update expression node. */
1860- ExprNode getPreUpdateNode ( ) { result = TExprNode ( e , v_ , false ) }
1852+ ExprNode getPreUpdateNode ( ) {
1853+ not postUpdate ( _, _, _) and
1854+ result = TExprNode ( e , v_ , false )
1855+ or
1856+ exists ( DfInput:: Expr e1 , BasicBlock bb1 , int i1 , BasicBlock bb2 , int i2 |
1857+ result = TExprNode ( e1 , v_ , false ) and
1858+ e1 .hasCfgNode ( bb1 , i1 ) and
1859+ variableReadWithPostUpdate ( bb1 , i1 , v_ , bb2 , i2 ) and
1860+ e .hasCfgNode ( bb2 , i2 )
1861+ )
1862+ }
18611863
18621864 override string toString ( ) { result = e .toString ( ) + " [postupdate]" }
18631865 }
@@ -1868,7 +1870,6 @@ module Make<
18681870 private predicate exprReadAt (
18691871 DfInput:: Expr e , BasicBlock bb , int i , SourceVariable v , boolean isPost , TExprNode node
18701872 ) {
1871- variableRead ( bb , i , v , true ) and
18721873 e .hasCfgNode ( bb , i ) and
18731874 node = TExprNode ( e , v , isPost )
18741875 }
@@ -2007,13 +2008,6 @@ module Make<
20072008 override string toString ( ) { result = "[input] " + def_ .toString ( ) }
20082009 }
20092010
2010- private predicate postUpdateNodeAt (
2011- ExprPostUpdateNode node , BasicBlock bb , int i , SourceVariable v
2012- ) {
2013- node .getPreUpdateNode ( ) .( ReadNode ) .readsAt ( _, _, v ) and
2014- DfInput:: postUpdateCfgNode ( node .getExpr ( ) , bb , i )
2015- }
2016-
20172011 /**
20182012 * Holds if `nodeFrom` corresponds to the reference to `v` at index `i` in
20192013 * `bb`. The boolean `isUseStep` indicates whether `nodeFrom` is an actual
@@ -2029,10 +2023,7 @@ module Make<
20292023 isUseStep = false
20302024 )
20312025 or
2032- nodeFrom .( ReadNode ) .readsAt ( bb , i , v ) and
2033- isUseStep = true
2034- or
2035- postUpdateNodeAt ( nodeFrom , bb , i , v ) and
2026+ exprReadAt ( _, bb , i , v , _, nodeFrom ) and
20362027 isUseStep = true
20372028 }
20382029
@@ -2053,6 +2044,15 @@ module Make<
20532044 )
20542045 )
20552046 or
2047+ // Flow from definition/read via post-update node
2048+ exists ( BasicBlock bb2 , int i2 |
2049+ AdjacentSsaRefs:: adjacentRefRead ( bb1 , i1 , bb2 , i2 , v ) and
2050+ postUpdate ( bb2 , i2 , v ) and
2051+ not any ( ReadNode r ) .readsAt ( bb2 , i2 , v ) and
2052+ not any ( UncertainWriteDefinition def2 ) .definesAt ( v , bb2 , i2 ) and
2053+ flowFromRefToNode ( v , bb2 , i2 , nodeTo )
2054+ )
2055+ or
20562056 // Flow from definition/read to phi input
20572057 exists ( BasicBlock input , BasicBlock bbPhi , DefinitionExt phi |
20582058 AdjacentSsaRefs:: adjacentRefPhi ( bb1 , i1 , input , bbPhi , v ) and
0 commit comments