Skip to content

Commit d03dd49

Browse files
authored
Merge pull request github#12622 from MathiasVP/skip-safe-conversions-in-range-analysis
C++: Range analysis on `EquivalenceClass`es
2 parents f5a2853 + 4043aa9 commit d03dd49

File tree

10 files changed

+183
-72
lines changed

10 files changed

+183
-72
lines changed

cpp/ql/lib/experimental/semmle/code/cpp/semantic/SemanticExprSpecific.qll

Lines changed: 137 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -12,12 +12,92 @@ private import semmle.code.cpp.ir.ValueNumbering
1212
module SemanticExprConfig {
1313
class Location = Cpp::Location;
1414

15-
class Expr = IR::Instruction;
15+
/** A `ConvertInstruction` or a `CopyValueInstruction`. */
16+
private class Conversion extends IR::UnaryInstruction {
17+
Conversion() {
18+
this instanceof IR::CopyValueInstruction
19+
or
20+
this instanceof IR::ConvertInstruction
21+
}
22+
23+
/** Holds if this instruction converts a value of type `tFrom` to a value of type `tTo`. */
24+
predicate converts(SemType tFrom, SemType tTo) {
25+
tFrom = getSemanticType(this.getUnary().getResultIRType()) and
26+
tTo = getSemanticType(this.getResultIRType())
27+
}
28+
}
29+
30+
/**
31+
* Gets a conversion-like instruction that consumes `op`, and
32+
* which is guaranteed to not overflow.
33+
*/
34+
private IR::Instruction safeConversion(IR::Operand op) {
35+
exists(Conversion conv, SemType tFrom, SemType tTo |
36+
conv.converts(tFrom, tTo) and
37+
conversionCannotOverflow(tFrom, tTo) and
38+
conv.getUnaryOperand() = op and
39+
result = conv
40+
)
41+
}
42+
43+
/** Holds if `i1 = i2` or if `i2` is a safe conversion that consumes `i1`. */
44+
private predicate idOrSafeConversion(IR::Instruction i1, IR::Instruction i2) {
45+
not i1.getResultIRType() instanceof IR::IRVoidType and
46+
(
47+
i1 = i2
48+
or
49+
i2 = safeConversion(i1.getAUse()) and
50+
i1.getBlock() = i2.getBlock()
51+
)
52+
}
53+
54+
module Equiv = QlBuiltins::EquivalenceRelation<IR::Instruction, idOrSafeConversion/2>;
55+
56+
/**
57+
* The expressions on which we perform range analysis.
58+
*/
59+
class Expr extends Equiv::EquivalenceClass {
60+
/** Gets the n'th instruction in this equivalence class. */
61+
private IR::Instruction getInstruction(int n) {
62+
result =
63+
rank[n + 1](IR::Instruction instr, int i, IR::IRBlock block |
64+
this = Equiv::getEquivalenceClass(instr) and block.getInstruction(i) = instr
65+
|
66+
instr order by i
67+
)
68+
}
69+
70+
/** Gets a textual representation of this element. */
71+
string toString() { result = this.getUnconverted().toString() }
72+
73+
/** Gets the basic block of this expression. */
74+
IR::IRBlock getBlock() { result = this.getUnconverted().getBlock() }
75+
76+
/** Gets the unconverted instruction associated with this expression. */
77+
IR::Instruction getUnconverted() { result = this.getInstruction(0) }
78+
79+
/**
80+
* Gets the final instruction associated with this expression. This
81+
* represents the result after applying all the safe conversions.
82+
*/
83+
IR::Instruction getConverted() {
84+
exists(int n |
85+
result = this.getInstruction(n) and
86+
not exists(this.getInstruction(n + 1))
87+
)
88+
}
89+
90+
/** Gets the type of the result produced by this instruction. */
91+
IR::IRType getResultIRType() { result = this.getConverted().getResultIRType() }
92+
93+
/** Gets the location of the source code for this expression. */
94+
Location getLocation() { result = this.getUnconverted().getLocation() }
95+
}
1696

1797
SemBasicBlock getExprBasicBlock(Expr e) { result = getSemanticBasicBlock(e.getBlock()) }
1898

1999
private predicate anyConstantExpr(Expr expr, SemType type, string value) {
20-
exists(IR::ConstantInstruction instr | instr = expr |
100+
exists(IR::ConstantInstruction instr | getSemanticExpr(instr) = expr |
21101
type = getSemanticType(instr.getResultIRType()) and
22102
value = instr.getValue()
23103
)
@@ -58,41 +138,46 @@ module SemanticExprConfig {
58138
predicate nullLiteral(Expr expr, SemAddressType type) { anyConstantExpr(expr, type, _) }
59139

60140
predicate stringLiteral(Expr expr, SemType type, string value) {
61-
anyConstantExpr(expr, type, value) and expr instanceof IR::StringConstantInstruction
141+
anyConstantExpr(expr, type, value) and
142+
expr.getUnconverted() instanceof IR::StringConstantInstruction
62143
}
63144

64145
predicate binaryExpr(Expr expr, Opcode opcode, SemType type, Expr leftOperand, Expr rightOperand) {
65-
exists(IR::BinaryInstruction instr | instr = expr |
146+
exists(IR::BinaryInstruction instr |
147+
instr = expr.getUnconverted() and
66148
type = getSemanticType(instr.getResultIRType()) and
67-
leftOperand = instr.getLeft() and
68-
rightOperand = instr.getRight() and
149+
leftOperand = getSemanticExpr(instr.getLeft()) and
150+
rightOperand = getSemanticExpr(instr.getRight()) and
69151
// REVIEW: Merge the two `Opcode` types.
70152
opcode.toString() = instr.getOpcode().toString()
71153
)
72154
}
73155

74156
predicate unaryExpr(Expr expr, Opcode opcode, SemType type, Expr operand) {
75-
type = getSemanticType(expr.getResultIRType()) and
76-
(
77-
exists(IR::UnaryInstruction instr | instr = expr |
78-
operand = instr.getUnary() and
79-
// REVIEW: Merge the two operand types.
80-
opcode.toString() = instr.getOpcode().toString()
81-
)
82-
or
83-
exists(IR::StoreInstruction instr | instr = expr |
84-
operand = instr.getSourceValue() and
85-
opcode instanceof Opcode::Store
86-
)
157+
exists(IR::UnaryInstruction instr | instr = expr.getUnconverted() |
158+
type = getSemanticType(instr.getResultIRType()) and
159+
operand = getSemanticExpr(instr.getUnary()) and
160+
// REVIEW: Merge the two operand types.
161+
opcode.toString() = instr.getOpcode().toString()
162+
)
163+
or
164+
exists(IR::StoreInstruction instr | instr = expr.getUnconverted() |
165+
type = getSemanticType(instr.getResultIRType()) and
166+
operand = getSemanticExpr(instr.getSourceValue()) and
167+
opcode instanceof Opcode::Store
87168
)
88169
}
89170

90171
predicate nullaryExpr(Expr expr, Opcode opcode, SemType type) {
91-
type = getSemanticType(expr.getResultIRType()) and
92-
(
93-
expr instanceof IR::LoadInstruction and opcode instanceof Opcode::Load
94-
or
95-
expr instanceof IR::InitializeParameterInstruction and
172+
exists(IR::LoadInstruction load |
173+
load = expr.getUnconverted() and
174+
type = getSemanticType(load.getResultIRType()) and
175+
opcode instanceof Opcode::Load
176+
)
177+
or
178+
exists(IR::InitializeParameterInstruction init |
179+
init = expr.getUnconverted() and
180+
type = getSemanticType(init.getResultIRType()) and
96181
opcode instanceof Opcode::InitializeParameter
97182
)
98183
}
@@ -122,8 +207,10 @@ module SemanticExprConfig {
122207
newtype TSsaVariable =
123208
TSsaInstruction(IR::Instruction instr) { instr.hasMemoryResult() } or
124209
TSsaOperand(IR::Operand op) { op.isDefinitionInexact() } or
125-
TSsaPointerArithmeticGuard(IR::PointerArithmeticInstruction instr) {
126-
exists(Guard g, IR::Operand use | use = instr.getAUse() |
210+
TSsaPointerArithmeticGuard(ValueNumber instr) {
211+
exists(Guard g, IR::Operand use |
212+
use = instr.getAUse() and use.getIRType() instanceof IR::IRAddressType
213+
|
127214
g.comparesLt(use, _, _, _, _) or
128215
g.comparesLt(_, use, _, _, _) or
129216
g.comparesEq(use, _, _, _, _) or
@@ -138,7 +225,7 @@ module SemanticExprConfig {
138225

139226
IR::Instruction asInstruction() { none() }
140227

141-
IR::PointerArithmeticInstruction asPointerArithGuard() { none() }
228+
ValueNumber asPointerArithGuard() { none() }
142229

143230
IR::Operand asOperand() { none() }
144231
}
@@ -156,15 +243,15 @@ module SemanticExprConfig {
156243
}
157244

158245
class SsaPointerArithmeticGuard extends SsaVariable, TSsaPointerArithmeticGuard {
159-
IR::PointerArithmeticInstruction instr;
246+
ValueNumber vn;
160247

161-
SsaPointerArithmeticGuard() { this = TSsaPointerArithmeticGuard(instr) }
248+
SsaPointerArithmeticGuard() { this = TSsaPointerArithmeticGuard(vn) }
162249

163-
final override string toString() { result = instr.toString() }
250+
final override string toString() { result = vn.toString() }
164251

165-
final override Location getLocation() { result = instr.getLocation() }
252+
final override Location getLocation() { result = vn.getLocation() }
166253

167-
final override IR::PointerArithmeticInstruction asPointerArithGuard() { result = instr }
254+
final override ValueNumber asPointerArithGuard() { result = vn }
168255
}
169256

170257
class SsaOperand extends SsaVariable, TSsaOperand {
@@ -179,7 +266,9 @@ module SemanticExprConfig {
179266
final override IR::Operand asOperand() { result = op }
180267
}
181268

182-
predicate explicitUpdate(SsaVariable v, Expr sourceExpr) { v.asInstruction() = sourceExpr }
269+
predicate explicitUpdate(SsaVariable v, Expr sourceExpr) {
270+
getSemanticExpr(v.asInstruction()) = sourceExpr
271+
}
183272

184273
predicate phi(SsaVariable v) { v.asInstruction() instanceof IR::PhiInstruction }
185274

@@ -192,9 +281,9 @@ module SemanticExprConfig {
192281
}
193282

194283
Expr getAUse(SsaVariable v) {
195-
result.(IR::LoadInstruction).getSourceValue() = v.asInstruction()
284+
result.getUnconverted().(IR::LoadInstruction).getSourceValue() = v.asInstruction()
196285
or
197-
result = valueNumber(v.asPointerArithGuard()).getAnInstruction()
286+
result.getUnconverted() = v.asPointerArithGuard().getAnInstruction()
198287
}
199288

200289
SemType getSsaVariableType(SsaVariable v) {
@@ -236,7 +325,7 @@ module SemanticExprConfig {
236325
final override predicate hasRead(SsaVariable v) {
237326
exists(IR::Operand operand |
238327
operand.getDef() = v.asInstruction() or
239-
operand.getDef() = valueNumber(v.asPointerArithGuard()).getAnInstruction()
328+
operand.getDef() = v.asPointerArithGuard().getAnInstruction()
240329
|
241330
not operand instanceof IR::PhiInputOperand and
242331
operand.getUse().getBlock() = block
@@ -257,7 +346,7 @@ module SemanticExprConfig {
257346
final override predicate hasRead(SsaVariable v) {
258347
exists(IR::PhiInputOperand operand |
259348
operand.getDef() = v.asInstruction() or
260-
operand.getDef() = valueNumber(v.asPointerArithGuard()).getAnInstruction()
349+
operand.getDef() = v.asPointerArithGuard().getAnInstruction()
261350
|
262351
operand.getPredecessorBlock() = pred and
263352
operand.getUse().getBlock() = succ
@@ -303,17 +392,21 @@ module SemanticExprConfig {
303392
}
304393

305394
Expr getBoundExpr(Bound bound, int delta) {
306-
result = bound.(IRBound::Bound).getInstruction(delta)
395+
result = getSemanticExpr(bound.(IRBound::Bound).getInstruction(delta))
307396
}
308397

309398
class Guard = IRGuards::IRGuardCondition;
310399

311400
predicate guard(Guard guard, BasicBlock block) { block = guard.getBlock() }
312401

313-
Expr getGuardAsExpr(Guard guard) { result = guard }
402+
Expr getGuardAsExpr(Guard guard) { result = getSemanticExpr(guard) }
314403

315404
predicate equalityGuard(Guard guard, Expr e1, Expr e2, boolean polarity) {
316-
guard.comparesEq(e1.getAUse(), e2.getAUse(), 0, true, polarity)
405+
exists(IR::Instruction left, IR::Instruction right |
406+
getSemanticExpr(left) = e1 and
407+
getSemanticExpr(right) = e2 and
408+
guard.comparesEq(left.getAUse(), right.getAUse(), 0, true, polarity)
409+
)
317410
}
318411

319412
predicate guardDirectlyControlsBlock(Guard guard, BasicBlock controlled, boolean branch) {
@@ -324,16 +417,17 @@ module SemanticExprConfig {
324417
guard.controlsEdge(bb1, bb2, branch)
325418
}
326419

327-
Guard comparisonGuard(Expr e) { result = e }
420+
Guard comparisonGuard(Expr e) { getSemanticExpr(result) = e }
328421

329422
predicate implies_v2(Guard g1, boolean b1, Guard g2, boolean b2) {
330423
none() // TODO
331424
}
332-
}
333425

334-
SemExpr getSemanticExpr(IR::Instruction instr) { result = instr }
426+
/** Gets the expression associated with `instr`. */
427+
SemExpr getSemanticExpr(IR::Instruction instr) { result = Equiv::getEquivalenceClass(instr) }
428+
}
335429

336-
IR::Instruction getCppInstruction(SemExpr e) { e = result }
430+
predicate getSemanticExpr = SemanticExprConfig::getSemanticExpr/1;
337431

338432
SemBasicBlock getSemanticBasicBlock(IR::IRBlock block) { result = block }
339433

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/RangeAnalysisStage.qll

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -495,7 +495,7 @@ module RangeStage<DeltaSig D, BoundSig<D> Bounds, LangSig<D> LangParam, UtilSig<
495495
SemSsaVariable v2, SemGuard guardEq, boolean eqIsTrue, D::Delta d1, D::Delta d2,
496496
D::Delta oldDelta
497497
|
498-
guardEq = semEqFlowCond(v, semSsaRead(v2, d1), d2, true, eqIsTrue) and
498+
guardEq = semEqFlowCond(v, semSsaRead(pragma[only_bind_into](v2), d1), d2, true, eqIsTrue) and
499499
result = boundFlowCond(v2, e, oldDelta, upper, testIsTrue) and
500500
// guardEq needs to control guard
501501
guardEq.directlyControls(result.getBasicBlock(), eqIsTrue) and

cpp/ql/lib/experimental/semmle/code/cpp/semantic/analysis/SignAnalysisCommon.qll

Lines changed: 15 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -198,6 +198,16 @@ module SignAnalysis<DeltaSig D, UtilSig<D> Utils> {
198198
}
199199
}
200200

201+
/** An expression of an unsigned type. */
202+
private class UnsignedExpr extends FlowSignExpr {
203+
UnsignedExpr() { Utils::getTrackedType(this) instanceof SemUnsignedIntegerType }
204+
205+
override Sign getSignRestriction() {
206+
result = TPos() or
207+
result = TZero()
208+
}
209+
}
210+
201211
pragma[nomagic]
202212
private predicate binaryExprOperands(SemBinaryExpr binary, SemExpr left, SemExpr right) {
203213
binary.getLeftOperand() = left and binary.getRightOperand() = right
@@ -328,10 +338,11 @@ module SignAnalysis<DeltaSig D, UtilSig<D> Utils> {
328338
* - `isEq = false` : `v != eqbound`
329339
*/
330340
private predicate eqBound(SemExpr eqbound, SemSsaVariable v, SemSsaReadPosition pos, boolean isEq) {
331-
exists(SemGuard guard, boolean testIsTrue, boolean polarity |
332-
pos.hasReadOfVar(v) and
333-
semGuardControlsSsaRead(guard, pos, testIsTrue) and
334-
guard.isEquality(eqbound, Utils::semSsaRead(v, D::fromInt(0)), polarity) and
341+
exists(SemGuard guard, boolean testIsTrue, boolean polarity, SemExpr e |
342+
pos.hasReadOfVar(pragma[only_bind_into](v)) and
343+
semGuardControlsSsaRead(guard, pragma[only_bind_into](pos), testIsTrue) and
344+
e = Utils::semSsaRead(pragma[only_bind_into](v), D::fromInt(0)) and
345+
guard.isEquality(eqbound, e, polarity) and
335346
isEq = polarity.booleanXor(testIsTrue).booleanNot() and
336347
not unknownSign(eqbound)
337348
)

cpp/ql/src/experimental/Likely Bugs/OverrunWriteProductFlow.ql

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ import DataFlow::PathGraph
2424

2525
pragma[nomagic]
2626
Instruction getABoundIn(SemBound b, IRFunction func) {
27-
result = b.getExpr(0) and
27+
getSemanticExpr(result) = b.getExpr(0) and
2828
result.getEnclosingIRFunction() = func
2929
}
3030

@@ -115,7 +115,7 @@ class StringSizeConfiguration extends ProductFlow::Configuration {
115115
state1 = s1.toString() and
116116
state2 = s2.toString() and
117117
add.hasOperands(node1.asOperand(), op) and
118-
semBounded(op.getDef(), any(SemZeroBound zero), delta, true, _) and
118+
semBounded(getSemanticExpr(op.getDef()), any(SemZeroBound zero), delta, true, _) and
119119
node2.asInstruction() = add and
120120
s1 = s2 + delta
121121
)

cpp/ql/src/experimental/Security/CWE/CWE-193/ConstantSizeArrayOffByOne.ql

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ import PointerArithmeticToDerefFlow::PathGraph
1919

2020
pragma[nomagic]
2121
Instruction getABoundIn(SemBound b, IRFunction func) {
22-
result = b.getExpr(0) and
22+
getSemanticExpr(result) = b.getExpr(0) and
2323
result.getEnclosingIRFunction() = func
2424
}
2525

cpp/ql/src/experimental/Security/CWE/CWE-193/InvalidPointerDeref.ql

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ import semmle.code.cpp.ir.IR
2424

2525
pragma[nomagic]
2626
Instruction getABoundIn(SemBound b, IRFunction func) {
27-
result = b.getExpr(0) and
27+
getSemanticExpr(result) = b.getExpr(0) and
2828
result.getEnclosingIRFunction() = func
2929
}
3030

cpp/ql/test/library-tests/ir/modulus-analysis/ModulusAnalysis.ql

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ import experimental.semmle.code.cpp.semantic.analysis.RangeUtils
55
import experimental.semmle.code.cpp.semantic.analysis.FloatDelta
66
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisSpecific
77
import experimental.semmle.code.cpp.semantic.analysis.RangeAnalysisImpl
8+
import experimental.semmle.code.cpp.semantic.SemanticExprSpecific
89
import semmle.code.cpp.ir.IR as IR
910
import TestUtilities.InlineExpectationsTest
1011

@@ -18,7 +19,7 @@ class ModulusAnalysisTest extends InlineExpectationsTest {
1819

1920
override predicate hasActualResult(Location location, string element, string tag, string value) {
2021
exists(SemExpr e, IR::CallInstruction call |
21-
call.getArgument(0) = e and
22+
getSemanticExpr(call.getArgument(0)) = e and
2223
call.getStaticCallTarget().hasName("mod") and
2324
tag = "mod" and
2425
element = e.toString() and

cpp/ql/test/library-tests/ir/range-analysis/RangeAnalysis.ql

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ class RangeAnalysisTest extends InlineExpectationsTest {
1212

1313
override predicate hasActualResult(Location location, string element, string tag, string value) {
1414
exists(SemExpr e, IR::CallInstruction call |
15-
call.getArgument(0) = e and
15+
getSemanticExpr(call.getArgument(0)) = e and
1616
call.getStaticCallTarget().hasName("range") and
1717
tag = "range" and
1818
element = e.toString() and

0 commit comments

Comments
 (0)