@@ -12,12 +12,92 @@ private import semmle.code.cpp.ir.ValueNumbering
12
12
module SemanticExprConfig {
13
13
class Location = Cpp:: Location ;
14
14
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
+ }
16
96
17
97
SemBasicBlock getExprBasicBlock ( Expr e ) { result = getSemanticBasicBlock ( e .getBlock ( ) ) }
18
98
19
99
private predicate anyConstantExpr ( Expr expr , SemType type , string value ) {
20
- exists ( IR:: ConstantInstruction instr | instr = expr |
100
+ exists ( IR:: ConstantInstruction instr | getSemanticExpr ( instr ) = expr |
21
101
type = getSemanticType ( instr .getResultIRType ( ) ) and
22
102
value = instr .getValue ( )
23
103
)
@@ -58,41 +138,46 @@ module SemanticExprConfig {
58
138
predicate nullLiteral ( Expr expr , SemAddressType type ) { anyConstantExpr ( expr , type , _) }
59
139
60
140
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
62
143
}
63
144
64
145
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
66
148
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
69
151
// REVIEW: Merge the two `Opcode` types.
70
152
opcode .toString ( ) = instr .getOpcode ( ) .toString ( )
71
153
)
72
154
}
73
155
74
156
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
87
168
)
88
169
}
89
170
90
171
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
96
181
opcode instanceof Opcode:: InitializeParameter
97
182
)
98
183
}
@@ -122,8 +207,10 @@ module SemanticExprConfig {
122
207
newtype TSsaVariable =
123
208
TSsaInstruction ( IR:: Instruction instr ) { instr .hasMemoryResult ( ) } or
124
209
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
+ |
127
214
g .comparesLt ( use , _, _, _, _) or
128
215
g .comparesLt ( _, use , _, _, _) or
129
216
g .comparesEq ( use , _, _, _, _) or
@@ -138,7 +225,7 @@ module SemanticExprConfig {
138
225
139
226
IR:: Instruction asInstruction ( ) { none ( ) }
140
227
141
- IR :: PointerArithmeticInstruction asPointerArithGuard ( ) { none ( ) }
228
+ ValueNumber asPointerArithGuard ( ) { none ( ) }
142
229
143
230
IR:: Operand asOperand ( ) { none ( ) }
144
231
}
@@ -156,15 +243,15 @@ module SemanticExprConfig {
156
243
}
157
244
158
245
class SsaPointerArithmeticGuard extends SsaVariable , TSsaPointerArithmeticGuard {
159
- IR :: PointerArithmeticInstruction instr ;
246
+ ValueNumber vn ;
160
247
161
- SsaPointerArithmeticGuard ( ) { this = TSsaPointerArithmeticGuard ( instr ) }
248
+ SsaPointerArithmeticGuard ( ) { this = TSsaPointerArithmeticGuard ( vn ) }
162
249
163
- final override string toString ( ) { result = instr .toString ( ) }
250
+ final override string toString ( ) { result = vn .toString ( ) }
164
251
165
- final override Location getLocation ( ) { result = instr .getLocation ( ) }
252
+ final override Location getLocation ( ) { result = vn .getLocation ( ) }
166
253
167
- final override IR :: PointerArithmeticInstruction asPointerArithGuard ( ) { result = instr }
254
+ final override ValueNumber asPointerArithGuard ( ) { result = vn }
168
255
}
169
256
170
257
class SsaOperand extends SsaVariable , TSsaOperand {
@@ -179,7 +266,9 @@ module SemanticExprConfig {
179
266
final override IR:: Operand asOperand ( ) { result = op }
180
267
}
181
268
182
- predicate explicitUpdate ( SsaVariable v , Expr sourceExpr ) { v .asInstruction ( ) = sourceExpr }
269
+ predicate explicitUpdate ( SsaVariable v , Expr sourceExpr ) {
270
+ getSemanticExpr ( v .asInstruction ( ) ) = sourceExpr
271
+ }
183
272
184
273
predicate phi ( SsaVariable v ) { v .asInstruction ( ) instanceof IR:: PhiInstruction }
185
274
@@ -192,9 +281,9 @@ module SemanticExprConfig {
192
281
}
193
282
194
283
Expr getAUse ( SsaVariable v ) {
195
- result .( IR:: LoadInstruction ) .getSourceValue ( ) = v .asInstruction ( )
284
+ result .getUnconverted ( ) . ( IR:: LoadInstruction ) .getSourceValue ( ) = v .asInstruction ( )
196
285
or
197
- result = valueNumber ( v .asPointerArithGuard ( ) ) .getAnInstruction ( )
286
+ result . getUnconverted ( ) = v .asPointerArithGuard ( ) .getAnInstruction ( )
198
287
}
199
288
200
289
SemType getSsaVariableType ( SsaVariable v ) {
@@ -236,7 +325,7 @@ module SemanticExprConfig {
236
325
final override predicate hasRead ( SsaVariable v ) {
237
326
exists ( IR:: Operand operand |
238
327
operand .getDef ( ) = v .asInstruction ( ) or
239
- operand .getDef ( ) = valueNumber ( v .asPointerArithGuard ( ) ) .getAnInstruction ( )
328
+ operand .getDef ( ) = v .asPointerArithGuard ( ) .getAnInstruction ( )
240
329
|
241
330
not operand instanceof IR:: PhiInputOperand and
242
331
operand .getUse ( ) .getBlock ( ) = block
@@ -257,7 +346,7 @@ module SemanticExprConfig {
257
346
final override predicate hasRead ( SsaVariable v ) {
258
347
exists ( IR:: PhiInputOperand operand |
259
348
operand .getDef ( ) = v .asInstruction ( ) or
260
- operand .getDef ( ) = valueNumber ( v .asPointerArithGuard ( ) ) .getAnInstruction ( )
349
+ operand .getDef ( ) = v .asPointerArithGuard ( ) .getAnInstruction ( )
261
350
|
262
351
operand .getPredecessorBlock ( ) = pred and
263
352
operand .getUse ( ) .getBlock ( ) = succ
@@ -303,17 +392,21 @@ module SemanticExprConfig {
303
392
}
304
393
305
394
Expr getBoundExpr ( Bound bound , int delta ) {
306
- result = bound .( IRBound:: Bound ) .getInstruction ( delta )
395
+ result = getSemanticExpr ( bound .( IRBound:: Bound ) .getInstruction ( delta ) )
307
396
}
308
397
309
398
class Guard = IRGuards:: IRGuardCondition ;
310
399
311
400
predicate guard ( Guard guard , BasicBlock block ) { block = guard .getBlock ( ) }
312
401
313
- Expr getGuardAsExpr ( Guard guard ) { result = guard }
402
+ Expr getGuardAsExpr ( Guard guard ) { result = getSemanticExpr ( guard ) }
314
403
315
404
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
+ )
317
410
}
318
411
319
412
predicate guardDirectlyControlsBlock ( Guard guard , BasicBlock controlled , boolean branch ) {
@@ -324,16 +417,17 @@ module SemanticExprConfig {
324
417
guard .controlsEdge ( bb1 , bb2 , branch )
325
418
}
326
419
327
- Guard comparisonGuard ( Expr e ) { result = e }
420
+ Guard comparisonGuard ( Expr e ) { getSemanticExpr ( result ) = e }
328
421
329
422
predicate implies_v2 ( Guard g1 , boolean b1 , Guard g2 , boolean b2 ) {
330
423
none ( ) // TODO
331
424
}
332
- }
333
425
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
+ }
335
429
336
- IR :: Instruction getCppInstruction ( SemExpr e ) { e = result }
430
+ predicate getSemanticExpr = SemanticExprConfig :: getSemanticExpr / 1 ;
337
431
338
432
SemBasicBlock getSemanticBasicBlock ( IR:: IRBlock block ) { result = block }
339
433
0 commit comments