@@ -105,7 +105,7 @@ module SemanticExprConfig {
105
105
SemBasicBlock getExprBasicBlock ( Expr e ) { result = getSemanticBasicBlock ( e .getBlock ( ) ) }
106
106
107
107
private predicate anyConstantExpr ( Expr expr , SemType type , string value ) {
108
- exists ( IR:: ConstantInstruction instr | instr = expr |
108
+ exists ( IR:: ConstantInstruction instr | getSemanticExpr ( instr ) = expr |
109
109
type = getSemanticType ( instr .getResultIRType ( ) ) and
110
110
value = instr .getValue ( )
111
111
)
@@ -146,41 +146,46 @@ module SemanticExprConfig {
146
146
predicate nullLiteral ( Expr expr , SemAddressType type ) { anyConstantExpr ( expr , type , _) }
147
147
148
148
predicate stringLiteral ( Expr expr , SemType type , string value ) {
149
- anyConstantExpr ( expr , type , value ) and expr instanceof IR:: StringConstantInstruction
149
+ anyConstantExpr ( expr , type , value ) and
150
+ expr .getUnconverted ( ) instanceof IR:: StringConstantInstruction
150
151
}
151
152
152
153
predicate binaryExpr ( Expr expr , Opcode opcode , SemType type , Expr leftOperand , Expr rightOperand ) {
153
- exists ( IR:: BinaryInstruction instr | instr = expr |
154
+ exists ( IR:: BinaryInstruction instr |
155
+ instr = expr .getUnconverted ( ) and
154
156
type = getSemanticType ( instr .getResultIRType ( ) ) and
155
- leftOperand = instr .getLeft ( ) and
156
- rightOperand = instr .getRight ( ) and
157
+ leftOperand = getSemanticExpr ( instr .getLeft ( ) ) and
158
+ rightOperand = getSemanticExpr ( instr .getRight ( ) ) and
157
159
// REVIEW: Merge the two `Opcode` types.
158
160
opcode .toString ( ) = instr .getOpcode ( ) .toString ( )
159
161
)
160
162
}
161
163
162
164
predicate unaryExpr ( Expr expr , Opcode opcode , SemType type , Expr operand ) {
163
- type = getSemanticType ( expr .getResultIRType ( ) ) and
164
- (
165
- exists ( IR:: UnaryInstruction instr | instr = expr |
166
- operand = instr .getUnary ( ) and
167
- // REVIEW: Merge the two operand types.
168
- opcode .toString ( ) = instr .getOpcode ( ) .toString ( )
169
- )
170
- or
171
- exists ( IR:: StoreInstruction instr | instr = expr |
172
- operand = instr .getSourceValue ( ) and
173
- opcode instanceof Opcode:: Store
174
- )
165
+ exists ( IR:: UnaryInstruction instr | instr = expr .getUnconverted ( ) |
166
+ type = getSemanticType ( instr .getResultIRType ( ) ) and
167
+ operand = getSemanticExpr ( instr .getUnary ( ) ) and
168
+ // REVIEW: Merge the two operand types.
169
+ opcode .toString ( ) = instr .getOpcode ( ) .toString ( )
170
+ )
171
+ or
172
+ exists ( IR:: StoreInstruction instr | instr = expr .getUnconverted ( ) |
173
+ type = getSemanticType ( instr .getResultIRType ( ) ) and
174
+ operand = getSemanticExpr ( instr .getSourceValue ( ) ) and
175
+ opcode instanceof Opcode:: Store
175
176
)
176
177
}
177
178
178
179
predicate nullaryExpr ( Expr expr , Opcode opcode , SemType type ) {
179
- type = getSemanticType ( expr .getResultIRType ( ) ) and
180
- (
181
- expr instanceof IR:: LoadInstruction and opcode instanceof Opcode:: Load
182
- or
183
- expr instanceof IR:: InitializeParameterInstruction and
180
+ exists ( IR:: LoadInstruction load |
181
+ load = expr .getUnconverted ( ) and
182
+ type = getSemanticType ( load .getResultIRType ( ) ) and
183
+ opcode instanceof Opcode:: Load
184
+ )
185
+ or
186
+ exists ( IR:: InitializeParameterInstruction init |
187
+ init = expr .getUnconverted ( ) and
188
+ type = getSemanticType ( init .getResultIRType ( ) ) and
184
189
opcode instanceof Opcode:: InitializeParameter
185
190
)
186
191
}
@@ -267,7 +272,9 @@ module SemanticExprConfig {
267
272
final override IR:: Operand asOperand ( ) { result = op }
268
273
}
269
274
270
- predicate explicitUpdate ( SsaVariable v , Expr sourceExpr ) { v .asInstruction ( ) = sourceExpr }
275
+ predicate explicitUpdate ( SsaVariable v , Expr sourceExpr ) {
276
+ getSemanticExpr ( v .asInstruction ( ) ) = sourceExpr
277
+ }
271
278
272
279
predicate phi ( SsaVariable v ) { v .asInstruction ( ) instanceof IR:: PhiInstruction }
273
280
@@ -280,9 +287,9 @@ module SemanticExprConfig {
280
287
}
281
288
282
289
Expr getAUse ( SsaVariable v ) {
283
- result .( IR:: LoadInstruction ) .getSourceValue ( ) = v .asInstruction ( )
290
+ result .getUnconverted ( ) . ( IR:: LoadInstruction ) .getSourceValue ( ) = v .asInstruction ( )
284
291
or
285
- result = valueNumber ( v .asPointerArithGuard ( ) ) .getAnInstruction ( )
292
+ result . getUnconverted ( ) = valueNumber ( v .asPointerArithGuard ( ) ) .getAnInstruction ( )
286
293
}
287
294
288
295
SemType getSsaVariableType ( SsaVariable v ) {
@@ -391,17 +398,21 @@ module SemanticExprConfig {
391
398
}
392
399
393
400
Expr getBoundExpr ( Bound bound , int delta ) {
394
- result = bound .( IRBound:: Bound ) .getInstruction ( delta )
401
+ result = getSemanticExpr ( bound .( IRBound:: Bound ) .getInstruction ( delta ) )
395
402
}
396
403
397
404
class Guard = IRGuards:: IRGuardCondition ;
398
405
399
406
predicate guard ( Guard guard , BasicBlock block ) { block = guard .getBlock ( ) }
400
407
401
- Expr getGuardAsExpr ( Guard guard ) { result = guard }
408
+ Expr getGuardAsExpr ( Guard guard ) { result = getSemanticExpr ( guard ) }
402
409
403
410
predicate equalityGuard ( Guard guard , Expr e1 , Expr e2 , boolean polarity ) {
404
- guard .comparesEq ( e1 .getAUse ( ) , e2 .getAUse ( ) , 0 , true , polarity )
411
+ exists ( IR:: Instruction left , IR:: Instruction right |
412
+ getSemanticExpr ( left ) = e1 and
413
+ getSemanticExpr ( right ) = e2 and
414
+ guard .comparesEq ( left .getAUse ( ) , right .getAUse ( ) , 0 , true , polarity )
415
+ )
405
416
}
406
417
407
418
predicate guardDirectlyControlsBlock ( Guard guard , BasicBlock controlled , boolean branch ) {
@@ -412,16 +423,17 @@ module SemanticExprConfig {
412
423
guard .controlsEdge ( bb1 , bb2 , branch )
413
424
}
414
425
415
- Guard comparisonGuard ( Expr e ) { result = e }
426
+ Guard comparisonGuard ( Expr e ) { getSemanticExpr ( result ) = e }
416
427
417
428
predicate implies_v2 ( Guard g1 , boolean b1 , Guard g2 , boolean b2 ) {
418
429
none ( ) // TODO
419
430
}
420
- }
421
431
422
- SemExpr getSemanticExpr ( IR:: Instruction instr ) { result = instr }
432
+ /** Gets the expression associated with `instr`. */
433
+ SemExpr getSemanticExpr ( IR:: Instruction instr ) { result = Equiv:: getEquivalenceClass ( instr ) }
434
+ }
423
435
424
- IR :: Instruction getCppInstruction ( SemExpr e ) { e = result }
436
+ predicate getSemanticExpr = SemanticExprConfig :: getSemanticExpr / 1 ;
425
437
426
438
SemBasicBlock getSemanticBasicBlock ( IR:: IRBlock block ) { result = block }
427
439
0 commit comments