Skip to content

Commit 97461d1

Browse files
committed
add var unused in disjunct query
1 parent 112cd9d commit 97461d1

File tree

4 files changed

+388
-0
lines changed

4 files changed

+388
-0
lines changed
Lines changed: 212 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,212 @@
1+
/**
2+
* @name Var only used in one side of disjunct.
3+
* @description Only using a variable on one side of a disjunction can cause a cartesian product.
4+
* @kind problem
5+
* @problem.severity warning
6+
* @id ql/var-unused-in-disjunct
7+
* @tags maintainability
8+
* performance
9+
* @precision high
10+
*/
11+
12+
import ql
13+
14+
/**
15+
* Holds if `node` bind `var` in a (transitive) child node.
16+
* Is a practical approximation that ignores `not` and many other features.
17+
*/
18+
pragma[noinline]
19+
predicate alwaysBindsVar(VarDef var, AstNode node) {
20+
// base case
21+
node.(VarAccess).getDeclaration() = var and
22+
not isSmallType(var.getType()) // <- early pruning
23+
or
24+
// recursive cases
25+
alwaysBindsVar(var, node.getAChild(_)) and // the recursive step, go one step up to the parent.
26+
not node.(FullAggregate).getAnArgument() = var and // except if the parent defines the variable, then we stop.
27+
not node.(Quantifier).getAnArgument() = var and
28+
not node instanceof EffectiveDisjunction // for disjunctions, we need to check both sides.
29+
or
30+
exists(EffectiveDisjunction disj | disj = node |
31+
alwaysBindsVar(var, disj.getLeft()) and
32+
alwaysBindsVar(var, disj.getRight())
33+
)
34+
or
35+
exists(EffectiveDisjunction disj | disj = node |
36+
alwaysBindsVar(var, disj.getAnOperand()) and
37+
disj.getAnOperand() instanceof NoneCall
38+
)
39+
or
40+
exists(IfFormula ifForm | ifForm = node | alwaysBindsVar(var, ifForm.getCondition()))
41+
}
42+
43+
/**
44+
* Holds if we assume `t` is a small type, and
45+
* variables of this type are therefore not an issue in cartesian products.
46+
*/
47+
predicate isSmallType(Type t) {
48+
t.getName() = "string" // DataFlow::Configuration and the like
49+
or
50+
exists(NewType newType | newType = t.getDeclaration() |
51+
forex(NewTypeBranch branch | branch = newType.getABranch() | branch.getArity() = 0)
52+
)
53+
or
54+
t.getName() = "boolean"
55+
or
56+
exists(NewType newType | newType = t.getDeclaration() |
57+
forex(NewTypeBranch branch | branch = newType.getABranch() |
58+
isSmallType(branch.getReturnType())
59+
)
60+
)
61+
or
62+
exists(NewTypeBranch branch | t = branch.getReturnType() |
63+
forall(Type param | param = branch.getParameterType(_) | isSmallType(param))
64+
)
65+
or
66+
isSmallType(t.getASuperType())
67+
}
68+
69+
/**
70+
* Holds if `pred` is inlined.
71+
*/
72+
predicate isInlined(Predicate pred) {
73+
exists(Annotation inline |
74+
inline = pred.getAnAnnotation() and
75+
inline.getName() = "pragma" and
76+
inline.getArgs(0).getValue() = "inline"
77+
)
78+
or
79+
pred.getAnAnnotation().getName() = "bindingset"
80+
}
81+
82+
/**
83+
* An AstNode that acts like a disjunction.
84+
*/
85+
class EffectiveDisjunction extends AstNode {
86+
EffectiveDisjunction() {
87+
this instanceof IfFormula
88+
or
89+
this instanceof Disjunction
90+
}
91+
92+
/** Gets the left operand of this disjunction. */
93+
AstNode getLeft() {
94+
result = this.(IfFormula).getThenPart()
95+
or
96+
result = this.(Disjunction).getLeft()
97+
}
98+
99+
/** Gets the right operand of this disjunction. */
100+
AstNode getRight() {
101+
result = this.(IfFormula).getElsePart()
102+
or
103+
result = this.(Disjunction).getRight()
104+
}
105+
106+
/** Gets any of the operands of this disjunction. */
107+
AstNode getAnOperand() { result = [this.getLeft(), this.getRight()] }
108+
}
109+
110+
/**
111+
* Holds if `disj` only uses `var` in one of its branches.
112+
*/
113+
pragma[noinline]
114+
predicate onlyUseInOneBranch(EffectiveDisjunction disj, VarDef var) {
115+
alwaysBindsVar(var, disj.getLeft()) and
116+
not alwaysBindsVar(var, disj.getRight())
117+
or
118+
not alwaysBindsVar(var, disj.getLeft()) and
119+
alwaysBindsVar(var, disj.getRight())
120+
}
121+
122+
/**
123+
* Holds if `comp` is an equality comparison that has a low number of results.
124+
*/
125+
predicate isTinyAssignment(ComparisonFormula comp) {
126+
comp.getOperator() = "=" and
127+
(
128+
isSmallType(comp.getAnOperand().getType())
129+
or
130+
comp.getAnOperand() instanceof Literal
131+
)
132+
}
133+
134+
/**
135+
* An AstNode that acts like a conjunction.
136+
*/
137+
class EffectiveConjunction extends AstNode {
138+
EffectiveConjunction() {
139+
this instanceof Conjunction
140+
or
141+
this instanceof Exists
142+
}
143+
144+
/** Gets the left operand of this conjunction */
145+
Formula getLeft() {
146+
result = this.(Conjunction).getLeft()
147+
or
148+
result = this.(Exists).getRange()
149+
}
150+
151+
/** Gets the right operand of this conjunction */
152+
Formula getRight() {
153+
result = this.(Conjunction).getRight()
154+
or
155+
result = this.(Exists).getFormula()
156+
}
157+
}
158+
159+
/**
160+
* Holds if `node` is a sub-node of a node that always binds `var`.
161+
*/
162+
predicate varIsAlwaysBound(VarDef var, AstNode node) {
163+
// base case
164+
alwaysBindsVar(var, node) and
165+
onlyUseInOneBranch(_, var) // <- manual magic
166+
or
167+
// recursive cases
168+
exists(AstNode parent | node.getParent() = parent | varIsAlwaysBound(var, parent))
169+
or
170+
exists(EffectiveConjunction parent |
171+
varIsAlwaysBound(var, parent.getLeft()) and
172+
node = parent.getRight()
173+
or
174+
varIsAlwaysBound(var, parent.getRight()) and
175+
node = parent.getLeft()
176+
)
177+
or
178+
exists(IfFormula ifForm | varIsAlwaysBound(var, ifForm.getCondition()) |
179+
node = [ifForm.getThenPart(), ifForm.getElsePart()]
180+
)
181+
or
182+
exists(Forall for | varIsAlwaysBound(var, for.getRange()) | node = for.getFormula())
183+
}
184+
185+
/**
186+
* Holds if `disj` only uses `var` in one of its branches.
187+
* And we should report it as being a bad thing.
188+
*/
189+
predicate badDisjunction(EffectiveDisjunction disj, VarDef var) {
190+
onlyUseInOneBranch(disj, var) and
191+
// it's fine if it's always bound further up
192+
not varIsAlwaysBound(var, disj) and
193+
// none() on one side makes everything fine. (this happens, it's a type-system hack)
194+
not disj.getAnOperand() instanceof NoneCall and
195+
// inlined predicates might bind unused variables in the context they are used in.
196+
not (
197+
isInlined(disj.getEnclosingPredicate()) and
198+
var = disj.getEnclosingPredicate().getParameter(_)
199+
) and
200+
// recursion prevention never runs, it's a compile-time check, so we remove those results here
201+
not disj.getEnclosingPredicate().getParent().(Class).getName().matches("%RecursionPrevention") and // these are by design
202+
// not a small type
203+
not isSmallType(var.getType()) and
204+
// one of the branches is a tiny assignment. These are usually intentional cartesian products (and not too big).
205+
not isTinyAssignment(disj.getAnOperand())
206+
}
207+
208+
from EffectiveDisjunction disj, VarDef var
209+
where
210+
badDisjunction(disj, var) and
211+
not badDisjunction(disj.getParent(), var) // avoid duplicate reporting of the same error
212+
select disj, "The variable " + var.getName() + " is only used in one side of disjunct."
Lines changed: 167 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,167 @@
1+
import ql
2+
3+
class Big = Expr;
4+
5+
class Small extends boolean {
6+
Small() { this = [true, false] }
7+
}
8+
9+
class MyStr extends string {
10+
MyStr() { this = ["foo", "bar"] }
11+
}
12+
13+
predicate bad1(Big b) {
14+
b.toString().matches("%foo")
15+
or
16+
any()
17+
}
18+
19+
int bad2() {
20+
exists(Big big, Small small |
21+
result = big.toString().toInt()
22+
or
23+
result = small.toString().toInt()
24+
)
25+
}
26+
27+
float bad3(Big t) {
28+
result = [1 .. 10].toString().toFloat() or
29+
result = [11 .. 20].toString().toFloat() or
30+
result = t.toString().toFloat() or
31+
result = [21 .. 30].toString().toFloat()
32+
}
33+
34+
string good1(Big t) {
35+
(
36+
result = t.toString()
37+
or
38+
result instanceof MyStr // <- t unused here, but that's ok because of the conjunct that binds t.
39+
) and
40+
t.toString().regexpMatch(".*foo")
41+
}
42+
43+
predicate helper(Big a, Big b) {
44+
a = b and
45+
a.toString().matches("%foo")
46+
}
47+
48+
predicate bad4(Big fromType, Big toType) {
49+
helper(fromType, toType)
50+
or
51+
fromType.toString().matches("%foo")
52+
or
53+
helper(toType, fromType)
54+
}
55+
56+
predicate good2(Big t) {
57+
exists(Small other |
58+
t.toString().matches("%foo")
59+
or
60+
other.toString().matches("%foo") // <- t unused here, but that's ok because of the conjunct (exists) that binds t.
61+
|
62+
t.toString().regexpMatch(".*foo")
63+
)
64+
}
65+
66+
predicate mixed1(Big good, Small small) {
67+
good.toString().matches("%foo")
68+
or
69+
good =
70+
any(Big bad |
71+
small.toString().matches("%foo") and
72+
// the use of good is fine, the comparison futher up binds it.
73+
// the same is not true for bad.
74+
(bad.toString().matches("%foo") or good.toString().regexpMatch("foo.*")) and
75+
small.toString().regexpMatch(".*foo")
76+
)
77+
}
78+
79+
newtype OtherSmall =
80+
Small1() or
81+
Small2(boolean b) { b = true } or
82+
Small3(boolean b, Small o) {
83+
b = true and
84+
o.toString().matches("%foo")
85+
}
86+
87+
predicate good3(OtherSmall small) {
88+
small = Small1()
89+
or
90+
1 = 1
91+
}
92+
93+
predicate good4(Big big, Small small) {
94+
big.toString().matches("%foo")
95+
or
96+
// assignment to small type, intentional cartesian product
97+
small = any(Small s | s.toString().matches("%foo"))
98+
}
99+
100+
predicate good5(Big bb, Big v, boolean certain) {
101+
exists(Big read |
102+
read = bb and
103+
read = v and
104+
certain = true
105+
)
106+
or
107+
v =
108+
any(Big lsv |
109+
lsv.getEnclosingPredicate() = bb.(Expr).getEnclosingPredicate() and
110+
(lsv.toString().matches("%foo") or v.toString().matches("%foo")) and
111+
certain = false
112+
)
113+
}
114+
115+
predicate bad5(Big bb) { if none() then bb.toString().matches("%foo") else any() }
116+
117+
pragma[inline]
118+
predicate good5(Big a, Big b) {
119+
// fine. Assumes it's used somewhere where `a` and `b` are bound.
120+
b = any(Big bb | bb.toString().matches("%foo"))
121+
or
122+
a = any(Big bb | bb.toString().matches("%foo"))
123+
}
124+
125+
predicate bad6(Big a) {
126+
(
127+
a.toString().matches("%foo") // bad
128+
or
129+
any()
130+
) and
131+
(
132+
a.toString().matches("%foo") // also bad
133+
or
134+
any()
135+
)
136+
}
137+
138+
predicate good6(Big a) {
139+
a.toString().matches("%foo") and
140+
(
141+
a.toString().matches("%foo") // good, `a` is bound on the branch of the conjunction.
142+
or
143+
any()
144+
)
145+
}
146+
147+
predicate good7() {
148+
exists(Big l, Big r |
149+
l.toString().matches("%foo1") and
150+
r.toString().matches("%foo2")
151+
or
152+
l.toString().matches("%foo3") and
153+
r.toString().matches("%foo4")
154+
|
155+
not (l.toString().regexpMatch("%foo5") or r.toString().regexpMatch("%foo6")) and
156+
(l.toString().regexpMatch("%foo7") or r.toString().regexpMatch("%foo8"))
157+
)
158+
}
159+
160+
// TOOD: Next test, this one is
161+
string good8(int bitSize) {
162+
if bitSize != 0
163+
then bitSize = 1 and result = bitSize.toString()
164+
else (
165+
if 1 = 0 then result = "foo" else result = "bar"
166+
)
167+
}
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
| Test.qll:14:3:16:7 | Disjunction | The variable b is only used in one side of disjunct. |
2+
| Test.qll:21:5:23:37 | Disjunction | The variable big is only used in one side of disjunct. |
3+
| Test.qll:28:3:30:33 | Disjunction | The variable t is only used in one side of disjunct. |
4+
| Test.qll:49:3:53:26 | Disjunction | The variable toType is only used in one side of disjunct. |
5+
| Test.qll:74:8:74:77 | Disjunction | The variable bad is only used in one side of disjunct. |
6+
| Test.qll:115:26:115:80 | IfFormula | The variable bb is only used in one side of disjunct. |
7+
| Test.qll:127:5:129:9 | Disjunction | The variable a is only used in one side of disjunct. |
8+
| Test.qll:132:5:134:9 | Disjunction | The variable a is only used in one side of disjunct. |
Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
queries/performance/VarUnusedInDisjunct.ql

0 commit comments

Comments
 (0)