@@ -12,12 +12,92 @@ private import semmle.code.cpp.ir.ValueNumbering
1212module 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
338432SemBasicBlock getSemanticBasicBlock ( IR:: IRBlock block ) { result = block }
339433
0 commit comments