Skip to content

Commit 06dbec7

Browse files
hvitvedtamasvajk
hvitved
authored and
tamasvajk
committed
C#: Add Guard::controlsBasicBlock() and simplify Guard::isEquality() 
1 parent 8bf4a42 commit 06dbec7

File tree

5 files changed

+75
-63
lines changed

5 files changed

+75
-63
lines changed

‎csharp/ql/src/semmle/code/csharp/controlflow/Guards.qll‎

Lines changed: 67 additions & 58 deletions
Original file line numberDiff line numberDiff line change
@@ -33,29 +33,21 @@ class Guard extends Expr {
3333
}
3434

3535
/**
36-
* Holds if guard is an equality test between `e1` and `e2`. If the test is
36+
* Holds if basic block `bb` is guarded by this expression having value `v`.
37+
*/
38+
predicate controlsBasicBlock(BasicBlock bb, AbstractValue v) {
39+
Internal::guardControls(this, bb, v)
40+
}
41+
42+
/**
43+
* Holds if this guard is an equality test between `e1` and `e2`. If the test is
3744
* negated, that is `!=`, then `polarity` is false, otherwise `polarity` is
3845
* true.
3946
*/
4047
predicate isEquality(Expr e1, Expr e2, boolean polarity) {
41-
exists(Expr exp1, Expr exp2 | equalityGuard(exp1, exp2, polarity) |
42-
e1 = exp1 and e2 = exp2
43-
or
44-
e2 = exp1 and e1 = exp2
45-
)
46-
}
47-
48-
private predicate equalityGuard(Expr e1, Expr e2, boolean polarity) {
49-
exists(ComparisonTest eqtest |
50-
eqtest.getExpr() = this and
51-
eqtest.getAnArgument() = e1 and
52-
eqtest.getAnArgument() = e2 and
53-
not e1 = e2 and
54-
(
55-
polarity = true and eqtest.getComparisonKind().isEquality()
56-
or
57-
polarity = false and eqtest.getComparisonKind().isInequality()
58-
)
48+
exists(BooleanValue v |
49+
this = Internal::getAnEqualityCheck(e1, v, e2) and
50+
polarity = v.getValue()
5951
)
6052
}
6153
}
@@ -970,31 +962,28 @@ module Internal {
970962
e = any(BinaryArithmeticOperation bao | result = bao.getAnOperand())
971963
}
972964

973-
/** Holds if basic block `bb` only is reached when guard `g` has abstract value `v`. */
974-
private predicate guardControls(Guard g, BasicBlock bb, AbstractValue v) {
975-
exists(ControlFlowElement cfe, ConditionalSuccessor s, AbstractValue v0, Guard g0 |
976-
cfe.controlsBlock(bb, s)
977-
|
978-
v0.branch(cfe, s, g0) and
979-
impliesSteps(g0, v0, g, v)
965+
pragma[noinline]
966+
private predicate assertionControlsNodeInSameBasicBlock0(
967+
Guard g, AbstractValue v, BasicBlock bb, int i
968+
) {
969+
exists(Assertion a, Guard g0, AbstractValue v0 |
970+
asserts(a, g0, v0) and
971+
impliesSteps(g0, v0, g, v) and
972+
bb.getNode(i) = a.getAControlFlowNode()
980973
)
981974
}
982975

983976
/**
984977
* Holds if control flow node `cfn` only is reached when guard `g` evaluates to `v`,
985978
* because of an assertion.
986979
*/
987-
private predicate guardAssertionControlsNode(Guard g, ControlFlow::Node cfn, AbstractValue v) {
988-
exists(Assertion a, Guard g0, AbstractValue v0 |
989-
asserts(a, g0, v0) and
990-
impliesSteps(g0, v0, g, v)
991-
|
992-
a.strictlyDominates(cfn.getBasicBlock())
993-
or
994-
exists(BasicBlock bb, int i, int j | bb.getNode(i) = a.getAControlFlowNode() |
995-
bb.getNode(j) = cfn and
996-
j > i
997-
)
980+
private predicate assertionControlsNodeInSameBasicBlock(
981+
Guard g, ControlFlow::Node cfn, AbstractValue v
982+
) {
983+
exists(BasicBlock bb, int i, int j |
984+
assertionControlsNodeInSameBasicBlock0(g, v, bb, i) and
985+
bb.getNode(j) = cfn and
986+
j > i
998987
)
999988
}
1000989

@@ -1004,7 +993,7 @@ module Internal {
1004993
*/
1005994
private predicate guardAssertionControlsElement(Guard g, ControlFlowElement cfe, AbstractValue v) {
1006995
forex(ControlFlow::Node cfn | cfn = cfe.getAControlFlowNode() |
1007-
guardAssertionControlsNode(g, cfn, v)
996+
assertionControlsNodeInSameBasicBlock(g, cfn, v)
1008997
)
1009998
}
1010999

@@ -1318,24 +1307,6 @@ module Internal {
13181307
)
13191308
}
13201309

1321-
/**
1322-
* Gets an expression that tests whether expression `e1` is equal to
1323-
* expression `e2`.
1324-
*
1325-
* If the returned expression has abstract value `v`, then expression `e1` is
1326-
* guaranteed to be equal to `e2`, and if the returned expression has abstract
1327-
* value `v.getDualValue()`, then this expression is guaranteed to be
1328-
* non-equal to `e`.
1329-
*
1330-
* For example, if the expression `x != ""` evaluates to `false` then the
1331-
* expression `x` is guaranteed to be equal to `""`.
1332-
*/
1333-
Expr getAnEqualityCheck(Expr e1, AbstractValue v, Expr e2) {
1334-
result = getABooleanEqualityCheck(e1, v, e2)
1335-
or
1336-
result = getAMatchingEqualityCheck(e1, v, e2)
1337-
}
1338-
13391310
private Expr getAnEqualityCheckVal(Expr e, AbstractValue v, AbstractValue vExpr) {
13401311
result = getAnEqualityCheck(e, v, vExpr.getAnExpr())
13411312
}
@@ -1491,6 +1462,29 @@ module Internal {
14911462
not e = any(LocalVariableDeclStmt s).getAVariableDeclExpr()
14921463
}
14931464

1465+
/**
1466+
* Gets an expression that tests whether expression `e1` is equal to
1467+
* expression `e2`.
1468+
*
1469+
* If the returned expression has abstract value `v`, then expression `e1` is
1470+
* guaranteed to be equal to `e2`, and if the returned expression has abstract
1471+
* value `v.getDualValue()`, then this expression is guaranteed to be
1472+
* non-equal to `e`.
1473+
*
1474+
* For example, if the expression `x != ""` evaluates to `false` then the
1475+
* expression `x` is guaranteed to be equal to `""`.
1476+
*/
1477+
cached
1478+
Expr getAnEqualityCheck(Expr e1, AbstractValue v, Expr e2) {
1479+
result = getABooleanEqualityCheck(e1, v, e2)
1480+
or
1481+
result = getABooleanEqualityCheck(e2, v, e1)
1482+
or
1483+
result = getAMatchingEqualityCheck(e1, v, e2)
1484+
or
1485+
result = getAMatchingEqualityCheck(e2, v, e1)
1486+
}
1487+
14941488
cached
14951489
predicate isCustomNullCheck(Call call, Expr arg, BooleanValue v, boolean isNull) {
14961490
exists(Callable callable, Parameter p |
@@ -1776,7 +1770,7 @@ module Internal {
17761770
exists(Guard g | e = getAChildExprStar(g) |
17771771
guardControls(g, bb, _)
17781772
or
1779-
guardAssertionControlsNode(g, bb.getANode(), _)
1773+
assertionControlsNodeInSameBasicBlock(g, bb.getANode(), _)
17801774
)
17811775
}
17821776
}
@@ -1785,6 +1779,21 @@ module Internal {
17851779
private module Cached {
17861780
private import semmle.code.csharp.Caching
17871781

1782+
/** Holds if basic block `bb` only is reached when guard `g` has abstract value `v`. */
1783+
cached
1784+
predicate guardControls(Guard g, BasicBlock bb, AbstractValue v) {
1785+
exists(AbstractValue v0, Guard g0 | impliesSteps(g0, v0, g, v) |
1786+
exists(ControlFlowElement cfe, ConditionalSuccessor s |
1787+
v0.branch(cfe, s, g0) and cfe.controlsBlock(bb, s)
1788+
)
1789+
or
1790+
exists(Assertion a |
1791+
asserts(a, g0, v0) and
1792+
a.strictlyDominates(bb)
1793+
)
1794+
)
1795+
}
1796+
17881797
pragma[noinline]
17891798
private predicate isGuardedByNode0(
17901799
ControlFlow::Node cfn, AccessOrCallExpr guarded, Guard g, AccessOrCallExpr sub,
@@ -1840,7 +1849,7 @@ module Internal {
18401849
) {
18411850
isGuardedByNode0(guarded, _, g, sub, v)
18421851
or
1843-
guardAssertionControlsNode(g, guarded, v) and
1852+
assertionControlsNodeInSameBasicBlock(g, guarded, v) and
18441853
exists(ConditionOnExprComparisonConfig c | c.same(sub, guarded.getElement()))
18451854
}
18461855

‎csharp/ql/src/semmle/code/csharp/dataflow/internal/rangeanalysis/SignAnalysisSpecific.qll‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -243,7 +243,7 @@ private module Impl {
243243
*/
244244
predicate guardControlsSsaRead(Guard guard, SsaReadPosition controlled, boolean testIsTrue) {
245245
exists(BooleanValue b | b.getValue() = testIsTrue |
246-
guard.controlsNode(controlled.(SsaReadPositionBlock).getBlock().getANode(), _, b)
246+
guard.controlsBasicBlock(controlled.(SsaReadPositionBlock).getBlock(), b)
247247
)
248248
}
249249

‎csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.cs‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -155,7 +155,7 @@ int Guards(int x, int y)
155155

156156
if (y is -1)
157157
{
158-
return y; // strictly negative [MISSING]
158+
return y; // strictly negative
159159
}
160160

161161
if (x < y)
@@ -289,7 +289,7 @@ void Loop(int i, int j, int k)
289289
void Assert(int i, bool b)
290290
{
291291
Debug.Assert(i > 0);
292-
System.Console.WriteLine(i); // strictly positive
292+
System.Console.WriteLine(i); // strictly positive [MISSING]
293293

294294
if (b)
295295
System.Console.WriteLine(i); // strictly positive

‎csharp/ql/test/library-tests/dataflow/signanalysis/SignAnalysis.expected‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,7 @@
106106
| SignAnalysis.cs:153:20:153:20 | access to parameter y | strictlyPositive |
107107
| SignAnalysis.cs:156:18:156:19 | -... | strictlyNegative |
108108
| SignAnalysis.cs:156:19:156:19 | 1 | strictlyPositive |
109+
| SignAnalysis.cs:158:20:158:20 | access to parameter y | strictlyNegative |
109110
| SignAnalysis.cs:161:13:161:13 | access to parameter x | positive |
110111
| SignAnalysis.cs:163:20:163:20 | access to parameter y | strictlyPositive |
111112
| SignAnalysis.cs:166:22:166:22 | 1 | strictlyPositive |
@@ -154,8 +155,6 @@
154155
| SignAnalysis.cs:278:42:278:42 | access to parameter k | positive |
155156
| SignAnalysis.cs:280:21:280:21 | access to parameter k | positive |
156157
| SignAnalysis.cs:280:26:280:26 | 5 | strictlyPositive |
157-
| SignAnalysis.cs:291:22:291:22 | access to parameter i | strictlyPositive |
158-
| SignAnalysis.cs:292:34:292:34 | access to parameter i | strictlyPositive |
159158
| SignAnalysis.cs:295:38:295:38 | access to parameter i | strictlyPositive |
160159
| SignAnalysis.cs:300:27:300:28 | -... | strictlyNegative |
161160
| SignAnalysis.cs:300:28:300:28 | 1 | strictlyPositive |

‎csharp/ql/test/query-tests/Nullness/EqualityCheck.expected‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -191,8 +191,11 @@
191191
| E.cs:85:18:85:29 | ... != ... | false | E.cs:85:18:85:21 | access to parameter vals | E.cs:85:26:85:29 | null |
192192
| E.cs:85:18:85:29 | ... != ... | false | E.cs:85:26:85:29 | null | E.cs:85:18:85:21 | access to parameter vals |
193193
| E.cs:90:17:90:27 | access to local variable switchguard | match access to constant MY_CONST_A | E.cs:90:17:90:27 | access to local variable switchguard | E.cs:92:18:92:27 | access to constant MY_CONST_A |
194+
| E.cs:90:17:90:27 | access to local variable switchguard | match access to constant MY_CONST_A | E.cs:92:18:92:27 | access to constant MY_CONST_A | E.cs:90:17:90:27 | access to local variable switchguard |
194195
| E.cs:90:17:90:27 | access to local variable switchguard | match access to constant MY_CONST_B | E.cs:90:17:90:27 | access to local variable switchguard | E.cs:97:18:97:27 | access to constant MY_CONST_B |
196+
| E.cs:90:17:90:27 | access to local variable switchguard | match access to constant MY_CONST_B | E.cs:97:18:97:27 | access to constant MY_CONST_B | E.cs:90:17:90:27 | access to local variable switchguard |
195197
| E.cs:90:17:90:27 | access to local variable switchguard | match access to constant MY_CONST_C | E.cs:90:17:90:27 | access to local variable switchguard | E.cs:95:18:95:27 | access to constant MY_CONST_C |
198+
| E.cs:90:17:90:27 | access to local variable switchguard | match access to constant MY_CONST_C | E.cs:95:18:95:27 | access to constant MY_CONST_C | E.cs:90:17:90:27 | access to local variable switchguard |
196199
| E.cs:126:21:126:29 | ... == ... | true | E.cs:126:21:126:24 | access to local variable step | E.cs:126:29:126:29 | 0 |
197200
| E.cs:126:21:126:29 | ... == ... | true | E.cs:126:29:126:29 | 0 | E.cs:126:21:126:24 | access to local variable step |
198201
| E.cs:153:13:153:24 | ... != ... | false | E.cs:153:13:153:16 | access to local variable obj2 | E.cs:153:21:153:24 | null |
@@ -216,6 +219,7 @@
216219
| E.cs:293:13:293:24 | ... == ... | true | E.cs:293:15:293:19 | call to method M2 | E.cs:293:24:293:24 | (...) ... |
217220
| E.cs:293:13:293:24 | ... == ... | true | E.cs:293:24:293:24 | (...) ... | E.cs:293:15:293:19 | call to method M2 |
218221
| E.cs:321:13:321:30 | ... is ... | true | E.cs:321:14:321:21 | ... ?? ... | E.cs:321:27:321:30 | null |
222+
| E.cs:321:13:321:30 | ... is ... | true | E.cs:321:27:321:30 | null | E.cs:321:14:321:21 | ... ?? ... |
219223
| E.cs:355:13:355:21 | dynamic call to operator != | false | E.cs:355:13:355:13 | access to local variable x | E.cs:355:18:355:21 | null |
220224
| E.cs:355:13:355:21 | dynamic call to operator != | false | E.cs:355:18:355:21 | null | E.cs:355:13:355:13 | access to local variable x |
221225
| E.cs:362:13:362:29 | ... != ... | false | E.cs:362:13:362:13 | access to local variable x | E.cs:362:18:362:29 | (...) ... |

0 commit comments

Comments
 (0)