@@ -36,7 +36,7 @@ class Guard extends Expr {
36
36
* Holds if basic block `bb` is guarded by this expression having value `v`.
37
37
*/
38
38
predicate controlsBasicBlock ( BasicBlock bb , AbstractValue v ) {
39
- Internal:: guardControls ( this , _ , bb , v )
39
+ Internal:: guardControls ( this , bb , v )
40
40
}
41
41
42
42
/**
@@ -50,6 +50,12 @@ class Guard extends Expr {
50
50
polarity = v .getValue ( )
51
51
)
52
52
}
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 ) }
53
59
}
54
60
55
61
/** An abstract value. */
@@ -967,13 +973,6 @@ module Internal {
967
973
e = any ( BinaryArithmeticOperation bao | result = bao .getAnOperand ( ) )
968
974
}
969
975
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
-
977
976
private Expr stripConditionalExpr ( Expr e ) {
978
977
e =
979
978
any ( ConditionalExpr ce |
@@ -1009,8 +1008,11 @@ module Internal {
1009
1008
1010
1009
/** Holds if pre-basic-block `bb` only is reached when guard `g` has abstract value `v`. */
1011
1010
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 )
1014
1016
)
1015
1017
}
1016
1018
@@ -1038,6 +1040,23 @@ module Internal {
1038
1040
}
1039
1041
}
1040
1042
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
+
1041
1060
/**
1042
1061
* Holds if `ret` is an expression returned by the callable to which parameter
1043
1062
* `p` belongs, and `ret` having Boolean value `retVal` allows the conclusion
@@ -1046,14 +1065,14 @@ module Internal {
1046
1065
private predicate validReturnInCustomNullCheck (
1047
1066
Expr ret , Parameter p , BooleanValue retVal , boolean isNull
1048
1067
) {
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
1052
1071
) and
1053
1072
exists ( PreSsaImplicitParameterDefinition def | p = def .getParameter ( ) |
1054
1073
def .nullGuardedReturn ( ret , isNull )
1055
1074
or
1056
- exists ( NullValue nv | preImpliesSteps ( ret , retVal , def .getARead ( ) , nv ) |
1075
+ exists ( NullValue nv | boolReturnImplies ( ret , retVal , def .getARead ( ) , nv ) |
1057
1076
if nv .isNull ( ) then isNull = true else isNull = false
1058
1077
)
1059
1078
)
@@ -1691,6 +1710,79 @@ module Internal {
1691
1710
1692
1711
import PreCFG
1693
1712
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
+
1694
1786
/**
1695
1787
* A helper class for calculating structurally equal access/call expressions.
1696
1788
*/
@@ -1710,13 +1802,13 @@ module Internal {
1710
1802
1711
1803
/**
1712
1804
* 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
1714
1806
* `bb` is reached.
1715
1807
*/
1716
1808
pragma [ noinline]
1717
1809
private predicate candidateAux ( AccessOrCallExpr e , Declaration target , BasicBlock bb ) {
1718
1810
target = e .getTarget ( ) and
1719
- exists ( Guard g | e = getAChildExprStar ( g ) | guardControls ( g , _, bb , _ ) )
1811
+ guardControlsSub ( _, bb , e )
1720
1812
}
1721
1813
}
1722
1814
@@ -1727,49 +1819,67 @@ module Internal {
1727
1819
1728
1820
/**
1729
1821
* 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.
1733
1822
*/
1734
1823
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
1736
1829
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 )
1741
1832
)
1742
1833
}
1743
1834
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]
1745
1842
private predicate nodeIsGuardedBySameSubExpr0 (
1746
- ControlFlow:: Node guardedCfn , AccessOrCallExpr guarded , Guard g , ConditionBlock cb ,
1843
+ ControlFlow:: Node guardedCfn , BasicBlock guardedBB , AccessOrCallExpr guarded , Guard g ,
1747
1844
AccessOrCallExpr sub , AbstractValue v
1748
1845
) {
1749
1846
Stages:: GuardsStage:: forceCachingInSameStage ( ) and
1750
1847
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 )
1753
1852
}
1754
1853
1755
- pragma [ noinline ]
1854
+ pragma [ nomagic ]
1756
1855
private predicate nodeIsGuardedBySameSubExpr (
1757
- ControlFlow:: Node guardedCfn , AccessOrCallExpr guarded , Guard g , ConditionBlock cb ,
1856
+ ControlFlow:: Node guardedCfn , BasicBlock guardedBB , AccessOrCallExpr guarded , Guard g ,
1758
1857
AccessOrCallExpr sub , AbstractValue v
1759
1858
) {
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 )
1762
1861
}
1763
1862
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]
1765
1875
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 ,
1767
1877
AccessOrCallExpr sub , AbstractValue v , Ssa:: Definition def
1768
1878
) {
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
1773
1883
)
1774
1884
}
1775
1885
@@ -1789,7 +1899,7 @@ module Internal {
1789
1899
AccessOrCallExpr guarded , Guard g , AccessOrCallExpr sub , AbstractValue v
1790
1900
) {
1791
1901
forex ( ControlFlow:: Node cfn | cfn = guarded .getAControlFlowNode ( ) |
1792
- nodeIsGuardedBySameSubExpr ( cfn , guarded , g , _ , sub , v )
1902
+ nodeIsGuardedBySameSubExpr ( cfn , _ , guarded , g , sub , v )
1793
1903
)
1794
1904
}
1795
1905
@@ -1814,7 +1924,7 @@ module Internal {
1814
1924
predicate isGuardedByNode (
1815
1925
ControlFlow:: Nodes:: ElementNode guarded , Guard g , AccessOrCallExpr sub , AbstractValue v
1816
1926
) {
1817
- nodeIsGuardedBySameSubExpr ( guarded , _, g , _ , sub , v ) and
1927
+ nodeIsGuardedBySameSubExpr ( guarded , _, _ , g , sub , v ) and
1818
1928
forall ( ControlFlow:: Node subCfn , Ssa:: Definition def |
1819
1929
nodeIsGuardedBySameSubExprSsaDef ( guarded , _, g , subCfn , sub , v , def )
1820
1930
|
@@ -1860,40 +1970,6 @@ module Internal {
1860
1970
}
1861
1971
1862
1972
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
- }
1897
1973
}
1898
1974
1899
1975
private import Internal
0 commit comments