@@ -36,7 +36,7 @@ class Guard extends Expr {
3636 * Holds if basic block `bb` is guarded by this expression having value `v`.
3737 */
3838 predicate controlsBasicBlock ( BasicBlock bb , AbstractValue v ) {
39- Internal:: guardControls ( this , _ , bb , v )
39+ Internal:: guardControls ( this , bb , v )
4040 }
4141
4242 /**
@@ -50,6 +50,12 @@ class Guard extends Expr {
5050 polarity = v .getValue ( )
5151 )
5252 }
53+
54+ /**
55+ * Gets a valid value for this guard. For example, if this guard is a test, then
56+ * it can have Boolean values `true` and `false`.
57+ */
58+ AbstractValue getAValue ( ) { isGuard ( this , result ) }
5359}
5460
5561/** An abstract value. */
@@ -967,13 +973,6 @@ module Internal {
967973 e = any ( BinaryArithmeticOperation bao | result = bao .getAnOperand ( ) )
968974 }
969975
970- /** Same as `this.getAChildExpr*()`, but avoids `fastTC`. */
971- private Expr getAChildExprStar ( Guard g ) {
972- result = g
973- or
974- result = getAChildExprStar ( g ) .getAChildExpr ( )
975- }
976-
977976 private Expr stripConditionalExpr ( Expr e ) {
978977 e =
979978 any ( ConditionalExpr ce |
@@ -1009,8 +1008,11 @@ module Internal {
10091008
10101009 /** Holds if pre-basic-block `bb` only is reached when guard `g` has abstract value `v`. */
10111010 predicate preControls ( Guard g , PreBasicBlocks:: PreBasicBlock bb , AbstractValue v ) {
1012- exists ( AbstractValue v0 , Guard g0 | preControlsDirect ( g0 , bb , v0 ) |
1013- preImpliesSteps ( g0 , v0 , g , v )
1011+ preControlsDirect ( g , bb , v )
1012+ or
1013+ exists ( AbstractValue v0 , Guard g0 |
1014+ preControls ( g0 , bb , v0 ) and
1015+ preImpliesStep ( g0 , v0 , g , v )
10141016 )
10151017 }
10161018
@@ -1038,6 +1040,23 @@ module Internal {
10381040 }
10391041 }
10401042
1043+ private predicate canReturnBool ( Callable c , Expr ret ) {
1044+ canReturn ( c , ret ) and
1045+ c .getReturnType ( ) instanceof BoolType
1046+ }
1047+
1048+ private predicate boolReturnImplies ( Expr ret , BooleanValue retVal , Guard g , AbstractValue v ) {
1049+ canReturnBool ( _, ret ) and
1050+ isGuard ( ret , retVal ) and
1051+ g = ret and
1052+ v = retVal
1053+ or
1054+ exists ( Guard g0 , AbstractValue v0 |
1055+ boolReturnImplies ( ret , retVal , g0 , v0 ) and
1056+ preImpliesStep ( g0 , v0 , g , v )
1057+ )
1058+ }
1059+
10411060 /**
10421061 * Holds if `ret` is an expression returned by the callable to which parameter
10431062 * `p` belongs, and `ret` having Boolean value `retVal` allows the conclusion
@@ -1046,14 +1065,14 @@ module Internal {
10461065 private predicate validReturnInCustomNullCheck (
10471066 Expr ret , Parameter p , BooleanValue retVal , boolean isNull
10481067 ) {
1049- exists ( Callable c | canReturn ( c , ret ) |
1050- p . getCallable ( ) = c and
1051- c . getReturnType ( ) instanceof BoolType
1068+ exists ( Callable c |
1069+ canReturnBool ( c , ret ) and
1070+ p . getCallable ( ) = c
10521071 ) and
10531072 exists ( PreSsaImplicitParameterDefinition def | p = def .getParameter ( ) |
10541073 def .nullGuardedReturn ( ret , isNull )
10551074 or
1056- exists ( NullValue nv | preImpliesSteps ( ret , retVal , def .getARead ( ) , nv ) |
1075+ exists ( NullValue nv | boolReturnImplies ( ret , retVal , def .getARead ( ) , nv ) |
10571076 if nv .isNull ( ) then isNull = true else isNull = false
10581077 )
10591078 )
@@ -1691,6 +1710,79 @@ module Internal {
16911710
16921711 import PreCFG
16931712
1713+ private predicate interestingDescendantCandidate ( Expr e ) {
1714+ guardControls ( e , _, _)
1715+ or
1716+ e instanceof AccessOrCallExpr
1717+ }
1718+
1719+ /**
1720+ * An (interesting) descendant of a guard that controls some basic block.
1721+ *
1722+ * This class exists purely for performance reasons: It allows us to big-step
1723+ * through the child hierarchy in `guardControlsSub()` instead of using
1724+ * `getAChildExpr()`.
1725+ */
1726+ private class ControlGuardDescendant extends Expr {
1727+ ControlGuardDescendant ( ) {
1728+ guardControls ( this , _, _)
1729+ or
1730+ any ( ControlGuardDescendant other ) .interestingDescendant ( this )
1731+ }
1732+
1733+ private predicate descendant ( Expr e ) {
1734+ e = this .getAChildExpr ( )
1735+ or
1736+ exists ( Expr mid |
1737+ descendant ( mid ) and
1738+ not interestingDescendantCandidate ( mid ) and
1739+ e = mid .getAChildExpr ( )
1740+ )
1741+ }
1742+
1743+ /** Holds if `e` is an interesting descendant of this descendant. */
1744+ predicate interestingDescendant ( Expr e ) {
1745+ descendant ( e ) and
1746+ interestingDescendantCandidate ( e )
1747+ }
1748+ }
1749+
1750+ /**
1751+ * Holds if `g` controls basic block `bb`, and `sub` is some (interesting)
1752+ * sub expression of `g`.
1753+ *
1754+ * Sub expressions inside nested logical operations that themselve control `bb`
1755+ * are not included, since these will be sub expressions of their immediately
1756+ * enclosing logical operation. (This restriction avoids a quadratic blow-up.)
1757+ *
1758+ * For example, in
1759+ *
1760+ * ```csharp
1761+ * if (a && (b && c))
1762+ * BLOCK
1763+ * ```
1764+ *
1765+ * `a` is included as a sub expression of `a && (b && c)` (which controls `BLOCK`),
1766+ * while `b` and `c` are only included as sub expressions of `b && c` (which also
1767+ * controls `BLOCK`).
1768+ */
1769+ pragma [ nomagic]
1770+ private predicate guardControlsSub ( Guard g , BasicBlock bb , ControlGuardDescendant sub ) {
1771+ guardControls ( g , bb , _) and
1772+ sub = g
1773+ or
1774+ exists ( ControlGuardDescendant mid |
1775+ guardControlsSub ( g , bb , mid ) and
1776+ mid .interestingDescendant ( sub )
1777+ |
1778+ not guardControls ( sub , bb , _)
1779+ or
1780+ not mid instanceof UnaryLogicalOperation and
1781+ not mid instanceof BinaryLogicalOperation and
1782+ not mid instanceof BitwiseOperation
1783+ )
1784+ }
1785+
16941786 /**
16951787 * A helper class for calculating structurally equal access/call expressions.
16961788 */
@@ -1710,13 +1802,13 @@ module Internal {
17101802
17111803 /**
17121804 * Holds if access/call expression `e` (targeting declaration `target`)
1713- * is a sub expression of a condition that controls whether basic block
1805+ * is a sub expression of a guard that controls whether basic block
17141806 * `bb` is reached.
17151807 */
17161808 pragma [ noinline]
17171809 private predicate candidateAux ( AccessOrCallExpr e , Declaration target , BasicBlock bb ) {
17181810 target = e .getTarget ( ) and
1719- exists ( Guard g | e = getAChildExprStar ( g ) | guardControls ( g , _, bb , _ ) )
1811+ guardControlsSub ( _, bb , e )
17201812 }
17211813 }
17221814
@@ -1727,49 +1819,67 @@ module Internal {
17271819
17281820 /**
17291821 * Holds if basic block `bb` only is reached when guard `g` has abstract value `v`.
1730- *
1731- * `cb` records all of the possible condition blocks for `g` that a path from the
1732- * callable entry point to `bb` may go through.
17331822 */
17341823 cached
1735- predicate guardControls ( Guard g , ConditionBlock cb , BasicBlock bb , AbstractValue v ) {
1824+ predicate guardControls ( Guard g , BasicBlock bb , AbstractValue v ) {
1825+ exists ( ControlFlowElement cfe , ConditionalSuccessor cs |
1826+ v .branch ( cfe , cs , g ) and cfe .controlsBlock ( bb , cs , _)
1827+ )
1828+ or
17361829 exists ( AbstractValue v0 , Guard g0 |
1737- impliesSteps ( g0 , v0 , g , v ) and
1738- exists ( ControlFlowElement cfe , ConditionalSuccessor cs |
1739- v0 .branch ( cfe , cs , g0 ) and cfe .controlsBlock ( bb , cs , cb )
1740- )
1830+ guardControls ( g0 , bb , v0 ) and
1831+ impliesStep ( g0 , v0 , g , v )
17411832 )
17421833 }
17431834
1744- pragma [ noinline]
1835+ pragma [ nomagic]
1836+ private predicate guardControlsSubSame ( Guard g , BasicBlock bb , ControlGuardDescendant sub ) {
1837+ guardControlsSub ( g , bb , sub ) and
1838+ any ( ConditionOnExprComparisonConfig c ) .same ( sub , _)
1839+ }
1840+
1841+ pragma [ nomagic]
17451842 private predicate nodeIsGuardedBySameSubExpr0 (
1746- ControlFlow:: Node guardedCfn , AccessOrCallExpr guarded , Guard g , ConditionBlock cb ,
1843+ ControlFlow:: Node guardedCfn , BasicBlock guardedBB , AccessOrCallExpr guarded , Guard g ,
17471844 AccessOrCallExpr sub , AbstractValue v
17481845 ) {
17491846 Stages:: GuardsStage:: forceCachingInSameStage ( ) and
17501847 guardedCfn = guarded .getAControlFlowNode ( ) and
1751- guardControls ( g , cb , guardedCfn .getBasicBlock ( ) , v ) and
1752- exists ( ConditionOnExprComparisonConfig c | c .same ( sub , guarded ) )
1848+ guardedBB = guardedCfn .getBasicBlock ( ) and
1849+ guardControls ( g , guardedBB , v ) and
1850+ guardControlsSubSame ( g , guardedBB , sub ) and
1851+ any ( ConditionOnExprComparisonConfig c ) .same ( sub , guarded )
17531852 }
17541853
1755- pragma [ noinline ]
1854+ pragma [ nomagic ]
17561855 private predicate nodeIsGuardedBySameSubExpr (
1757- ControlFlow:: Node guardedCfn , AccessOrCallExpr guarded , Guard g , ConditionBlock cb ,
1856+ ControlFlow:: Node guardedCfn , BasicBlock guardedBB , AccessOrCallExpr guarded , Guard g ,
17581857 AccessOrCallExpr sub , AbstractValue v
17591858 ) {
1760- nodeIsGuardedBySameSubExpr0 ( guardedCfn , guarded , g , cb , sub , v ) and
1761- sub = getAChildExprStar ( g )
1859+ nodeIsGuardedBySameSubExpr0 ( guardedCfn , guardedBB , guarded , g , sub , v ) and
1860+ guardControlsSub ( g , guardedBB , sub )
17621861 }
17631862
1764- pragma [ noinline]
1863+ pragma [ nomagic]
1864+ private predicate nodeIsGuardedBySameSubExprSsaDef0 (
1865+ ControlFlow:: Node cfn , BasicBlock guardedBB , AccessOrCallExpr guarded , Guard g ,
1866+ ControlFlow:: Node subCfn , BasicBlock subCfnBB , AccessOrCallExpr sub , AbstractValue v ,
1867+ Ssa:: Definition def
1868+ ) {
1869+ nodeIsGuardedBySameSubExpr ( cfn , guardedBB , guarded , g , sub , v ) and
1870+ def = sub .getAnSsaQualifier ( subCfn ) and
1871+ subCfnBB = subCfn .getBasicBlock ( )
1872+ }
1873+
1874+ pragma [ nomagic]
17651875 private predicate nodeIsGuardedBySameSubExprSsaDef (
1766- ControlFlow:: Node cfn , AccessOrCallExpr guarded , Guard g , ControlFlow:: Node subCfn ,
1876+ ControlFlow:: Node guardedCfn , AccessOrCallExpr guarded , Guard g , ControlFlow:: Node subCfn ,
17671877 AccessOrCallExpr sub , AbstractValue v , Ssa:: Definition def
17681878 ) {
1769- exists ( ConditionBlock cb |
1770- nodeIsGuardedBySameSubExpr ( cfn , guarded , g , cb , sub , v ) and
1771- subCfn . getBasicBlock ( ) . dominates ( cb ) and
1772- def = sub . getAnSsaQualifier ( subCfn )
1879+ exists ( BasicBlock guardedBB , BasicBlock subCfnBB |
1880+ nodeIsGuardedBySameSubExprSsaDef0 ( guardedCfn , guardedBB , guarded , g , subCfn , subCfnBB , sub ,
1881+ v , def ) and
1882+ subCfnBB . getASuccessor * ( ) = guardedBB
17731883 )
17741884 }
17751885
@@ -1789,7 +1899,7 @@ module Internal {
17891899 AccessOrCallExpr guarded , Guard g , AccessOrCallExpr sub , AbstractValue v
17901900 ) {
17911901 forex ( ControlFlow:: Node cfn | cfn = guarded .getAControlFlowNode ( ) |
1792- nodeIsGuardedBySameSubExpr ( cfn , guarded , g , _ , sub , v )
1902+ nodeIsGuardedBySameSubExpr ( cfn , _ , guarded , g , sub , v )
17931903 )
17941904 }
17951905
@@ -1814,7 +1924,7 @@ module Internal {
18141924 predicate isGuardedByNode (
18151925 ControlFlow:: Nodes:: ElementNode guarded , Guard g , AccessOrCallExpr sub , AbstractValue v
18161926 ) {
1817- nodeIsGuardedBySameSubExpr ( guarded , _, g , _ , sub , v ) and
1927+ nodeIsGuardedBySameSubExpr ( guarded , _, _ , g , sub , v ) and
18181928 forall ( ControlFlow:: Node subCfn , Ssa:: Definition def |
18191929 nodeIsGuardedBySameSubExprSsaDef ( guarded , _, g , subCfn , sub , v , def )
18201930 |
@@ -1860,40 +1970,6 @@ module Internal {
18601970 }
18611971
18621972 import Cached
1863-
1864- /**
1865- * Holds if the assumption that `g1` has abstract value `v1` implies that
1866- * `g2` has abstract value `v2`, using zero or more steps of reasoning. That is,
1867- * the evaluation of `g2` to `v2` dominates the evaluation of `g1` to `v1`.
1868- *
1869- * This predicate does not rely on the control flow graph.
1870- */
1871- predicate preImpliesSteps ( Guard g1 , AbstractValue v1 , Guard g2 , AbstractValue v2 ) {
1872- g1 = g2 and
1873- v1 = v2 and
1874- isGuard ( g1 , v1 )
1875- or
1876- exists ( Expr mid , AbstractValue vMid | preImpliesSteps ( g1 , v1 , mid , vMid ) |
1877- preImpliesStep ( mid , vMid , g2 , v2 )
1878- )
1879- }
1880-
1881- /**
1882- * Holds if the assumption that `g1` has abstract value `v1` implies that
1883- * `g2` has abstract value `v2`, using zero or more steps of reasoning. That is,
1884- * the evaluation of `g2` to `v2` dominates the evaluation of `g1` to `v1`.
1885- *
1886- * This predicate relies on the control flow graph.
1887- */
1888- predicate impliesSteps ( Guard g1 , AbstractValue v1 , Guard g2 , AbstractValue v2 ) {
1889- g1 = g2 and
1890- v1 = v2 and
1891- isGuard ( g1 , v1 )
1892- or
1893- exists ( Expr mid , AbstractValue vMid | impliesSteps ( g1 , v1 , mid , vMid ) |
1894- impliesStep ( mid , vMid , g2 , v2 )
1895- )
1896- }
18971973}
18981974
18991975private import Internal
0 commit comments