5
5
6
6
import csharp
7
7
8
+ abstract private class GvnKind extends TGvnKind {
9
+ abstract string toString ( ) ;
10
+ }
11
+
12
+ private class GvnKindExpr extends GvnKind , TGvnKindExpr {
13
+ private int kind ;
14
+
15
+ GvnKindExpr ( ) { this = TGvnKindExpr ( kind ) }
16
+
17
+ override string toString ( ) { result = "Expr(" + kind + ")" }
18
+ }
19
+
20
+ private class GvnKindStmt extends GvnKind , TGvnKindStmt {
21
+ private int kind ;
22
+
23
+ GvnKindStmt ( ) { this = TGvnKindStmt ( kind ) }
24
+
25
+ override string toString ( ) { result = "Stmt(" + kind + ")" }
26
+ }
27
+
28
+ private class GvnKindDeclaration extends GvnKind , TGvnKindDeclaration {
29
+ private int kind ;
30
+ private boolean isTargetThis ;
31
+ private Declaration d ;
32
+
33
+ GvnKindDeclaration ( ) { this = TGvnKindDeclaration ( kind , isTargetThis , d ) }
34
+
35
+ override string toString ( ) { result = "Expr(" + kind + ")," + isTargetThis + "," + d }
36
+ }
37
+
8
38
/** Gets the declaration referenced by the expression `e`, if any. */
9
39
private Declaration referenceAttribute ( Expr e ) {
10
40
result = e .( MethodCall ) .getTarget ( )
@@ -14,17 +44,156 @@ private Declaration referenceAttribute(Expr e) {
14
44
result = e .( Access ) .getTarget ( )
15
45
}
16
46
17
- /** Gets the AST node kind element `e`. */
18
- private int elementKind ( ControlFlowElement e ) {
19
- expressions ( e , result , _ )
47
+ /** Gets a Boolean indicating whether the target of the expression `e` is `this `. */
48
+ private boolean isTargetThis ( Expr e ) {
49
+ result = true and e . ( MemberAccess ) . targetIsThisInstance ( )
20
50
or
21
- exists ( int k | statements ( e , k ) | result = - k )
51
+ result = false and not e .( MemberAccess ) .targetIsThisInstance ( )
52
+ }
53
+
54
+ /**
55
+ * A global value number (GVN) for a control flow element.
56
+ *
57
+ * GVNs are used to map control flow elements to a representation that
58
+ * omits location information, that is, two elements that are structurally
59
+ * equal will be mapped to the same GVN.
60
+ */
61
+ class Gvn extends TGvn {
62
+ /** Gets the string representation of this global value number. */
63
+ string toString ( ) { none ( ) }
64
+ }
65
+
66
+ private class ConstantGvn extends Gvn , TConstantGvn {
67
+ override string toString ( ) { this = TConstantGvn ( result ) }
68
+ }
69
+
70
+ private class GvnNil extends Gvn , TGvnNil {
71
+ private GvnKind kind ;
72
+
73
+ GvnNil ( ) { this = TGvnNil ( kind ) }
74
+
75
+ override string toString ( ) { result = "(kind:" + kind + ")" }
76
+ }
77
+
78
+ private class GvnCons extends Gvn , TGvnCons {
79
+ private Gvn head ;
80
+ private Gvn tail ;
81
+
82
+ GvnCons ( ) { this = TGvnCons ( head , tail ) }
83
+
84
+ override string toString ( ) { result = "(" + head + " :: " + tail + ")" }
22
85
}
23
86
24
- private int getNumberOfActualChildren ( ControlFlowElement e ) {
25
- if e .( MemberAccess ) .targetIsThisInstance ( )
26
- then result = e .getNumberOfChildren ( ) - 1
27
- else result = e .getNumberOfChildren ( )
87
+ pragma [ noinline]
88
+ private predicate gvnKindDeclaration ( Expr e , int kind , boolean isTargetThis , Declaration d ) {
89
+ isTargetThis = isTargetThis ( e ) and
90
+ d = referenceAttribute ( e ) and
91
+ expressions ( e , kind , _)
92
+ }
93
+
94
+ /**
95
+ * Gets the `GvnKind` of the element `cfe`.
96
+ *
97
+ * In case `cfe` is a reference attribute, we encode the entire declaration and whether
98
+ * the target is semantically equivalent to `this`.
99
+ */
100
+ private GvnKind getGvnKind ( ControlFlowElement cfe ) {
101
+ exists ( int kind , boolean isTargetThis , Declaration d |
102
+ gvnKindDeclaration ( cfe , kind , isTargetThis , d ) and
103
+ result = TGvnKindDeclaration ( kind , isTargetThis , d )
104
+ )
105
+ or
106
+ exists ( int kind |
107
+ not exists ( referenceAttribute ( cfe ) ) and
108
+ expressions ( cfe , kind , _) and
109
+ result = TGvnKindExpr ( kind )
110
+ or
111
+ statements ( cfe , kind ) and
112
+ result = TGvnKindStmt ( kind )
113
+ )
114
+ }
115
+
116
+ private Gvn toGvn ( ControlFlowElement cfe , GvnKind kind , int index ) {
117
+ kind = getGvnKind ( cfe ) and
118
+ result = TGvnNil ( kind ) and
119
+ index = - 1
120
+ or
121
+ exists ( Gvn head , Gvn tail |
122
+ toGvnCons ( cfe , kind , index , head , tail ) and
123
+ result = TGvnCons ( head , tail )
124
+ )
125
+ }
126
+
127
+ private int getNumberOfActualChildren ( ControlFlowElement cfe ) {
128
+ if cfe .( MemberAccess ) .targetIsThisInstance ( )
129
+ then result = cfe .getNumberOfChildren ( ) - 1
130
+ else result = cfe .getNumberOfChildren ( )
131
+ }
132
+
133
+ private ControlFlowElement getRankedChild ( ControlFlowElement cfe , int rnk ) {
134
+ result =
135
+ rank [ rnk + 1 ] ( ControlFlowElement child , int j |
136
+ child = cfe .getChild ( j ) and
137
+ (
138
+ j >= 0
139
+ or
140
+ j = - 1 and not cfe .( MemberAccess ) .targetIsThisInstance ( )
141
+ )
142
+ |
143
+ child order by j
144
+ )
145
+ }
146
+
147
+ pragma [ noinline]
148
+ private Gvn toGvnChild ( ControlFlowElement cfe , int index ) {
149
+ result = toGvn ( getRankedChild ( cfe , index ) )
150
+ }
151
+
152
+ pragma [ noinline]
153
+ private predicate toGvnCons ( ControlFlowElement cfe , GvnKind kind , int index , Gvn head , Gvn tail ) {
154
+ tail = toGvn ( cfe , kind , index - 1 ) and
155
+ head = toGvnChild ( cfe , index )
156
+ }
157
+
158
+ cached
159
+ private module Cached {
160
+ cached
161
+ newtype TGvnKind =
162
+ TGvnKindExpr ( int kind ) { expressions ( _, kind , _) } or
163
+ TGvnKindStmt ( int kind ) { statements ( _, kind ) } or
164
+ TGvnKindDeclaration ( int kind , boolean thisTarget , Declaration d ) {
165
+ exists ( Expr e |
166
+ d = referenceAttribute ( e ) and thisTarget = isTargetThis ( e ) and expressions ( e , kind , _)
167
+ )
168
+ }
169
+
170
+ cached
171
+ newtype TGvn =
172
+ TConstantGvn ( string s ) { s = any ( Expr e ) .getValue ( ) } or
173
+ TGvnNil ( GvnKind gkind ) or
174
+ TGvnCons ( Gvn head , Gvn tail ) { toGvnCons ( _, _, _, head , tail ) }
175
+
176
+ /** Gets the global value number of the element `cfe`. */
177
+ cached
178
+ Gvn toGvnCached ( ControlFlowElement cfe ) {
179
+ result = TConstantGvn ( cfe .( Expr ) .getValue ( ) )
180
+ or
181
+ not exists ( cfe .( Expr ) .getValue ( ) ) and
182
+ exists ( GvnKind kind , int index |
183
+ result = toGvn ( cfe , kind , index - 1 ) and
184
+ index = getNumberOfActualChildren ( cfe )
185
+ )
186
+ }
187
+ }
188
+
189
+ private import Cached
190
+
191
+ predicate toGvn = toGvnCached / 1 ;
192
+
193
+ pragma [ inline]
194
+ private predicate sameGvn ( ControlFlowElement x , ControlFlowElement y ) {
195
+ pragma [ only_bind_into ] ( toGvn ( pragma [ only_bind_out ] ( x ) ) ) =
196
+ pragma [ only_bind_into ] ( toGvn ( pragma [ only_bind_out ] ( y ) ) )
28
197
}
29
198
30
199
/**
@@ -57,87 +226,12 @@ abstract class StructuralComparisonConfiguration extends string {
57
226
*/
58
227
abstract predicate candidate ( ControlFlowElement x , ControlFlowElement y ) ;
59
228
60
- private predicate candidateInternal ( ControlFlowElement x , ControlFlowElement y ) {
61
- candidate ( x , y )
62
- or
63
- exists ( ControlFlowElement xParent , ControlFlowElement yParent , int i |
64
- candidateInternalChild ( xParent , i , x , yParent )
65
- |
66
- y = yParent .getChild ( i )
67
- )
68
- }
69
-
70
- pragma [ noinline]
71
- private predicate candidateInternalChild (
72
- ControlFlowElement x , int i , ControlFlowElement xChild , ControlFlowElement y
73
- ) {
74
- candidateInternal ( x , y ) and
75
- xChild = x .getChild ( i )
76
- }
77
-
78
- private predicate sameByValue ( Expr x , Expr y ) { sameByValueAux ( x , y , y .getValue ( ) ) }
79
-
80
- pragma [ nomagic]
81
- private predicate sameByValueAux ( Expr x , Expr y , string value ) {
82
- candidateInternal ( x , y ) and
83
- value = x .getValue ( )
84
- }
85
-
86
- private ControlFlowElement getRankedChild ( ControlFlowElement cfe , int rnk , int i ) {
87
- ( candidateInternal ( cfe , _) or candidateInternal ( _, cfe ) ) and
88
- i =
89
- rank [ rnk ] ( int j |
90
- exists ( ControlFlowElement child | child = cfe .getChild ( j ) |
91
- not ( j = - 1 and cfe .( MemberAccess ) .targetIsThisInstance ( ) )
92
- )
93
- ) and
94
- result = cfe .getChild ( i )
95
- }
96
-
97
- pragma [ nomagic]
98
- private predicate sameByStructure0 (
99
- ControlFlowElement x , ControlFlowElement y , int elementKind , int children
100
- ) {
101
- candidateInternal ( x , y ) and
102
- elementKind = elementKind ( x ) and
103
- children = getNumberOfActualChildren ( x ) and
104
- not ( x .( Expr ) .hasValue ( ) and y .( Expr ) .hasValue ( ) )
105
- }
106
-
107
- pragma [ nomagic]
108
- private predicate sameByStructure ( ControlFlowElement x , ControlFlowElement y , int i ) {
109
- i = 0 and
110
- // At least one of `x` and `y` must not have a value, they must have
111
- // the same kind, and the same number of children
112
- sameByStructure0 ( x , y , elementKind ( y ) , getNumberOfActualChildren ( y ) ) and
113
- // If one of them has a reference attribute, they should both reference
114
- // the same node
115
- ( exists ( referenceAttribute ( x ) ) implies referenceAttribute ( x ) = referenceAttribute ( y ) ) and
116
- // x is a member access on `this` iff y is
117
- ( x .( MemberAccess ) .targetIsThisInstance ( ) implies y .( MemberAccess ) .targetIsThisInstance ( ) ) and
118
- ( y .( MemberAccess ) .targetIsThisInstance ( ) implies x .( MemberAccess ) .targetIsThisInstance ( ) )
119
- or
120
- exists ( int j | sameByStructure ( x , y , i - 1 ) |
121
- sameInternal ( getRankedChild ( x , i , j ) , getRankedChild ( y , i , j ) )
122
- )
123
- }
124
-
125
- pragma [ nomagic]
126
- private predicate sameInternal ( ControlFlowElement x , ControlFlowElement y ) {
127
- sameByValue ( x , y )
128
- or
129
- sameByStructure ( x , y , getNumberOfActualChildren ( x ) )
130
- }
131
-
132
229
/**
133
230
* Holds if elements `x` and `y` structurally equal. `x` and `y` must be
134
231
* flagged as candidates for structural equality, that is,
135
232
* `candidate(x, y)` must hold.
136
233
*/
137
- predicate same ( ControlFlowElement x , ControlFlowElement y ) {
138
- candidate ( x , y ) and
139
- sameInternal ( x , y )
140
- }
234
+ predicate same ( ControlFlowElement x , ControlFlowElement y ) { candidate ( x , y ) and sameGvn ( x , y ) }
141
235
}
142
236
143
237
/**
@@ -183,86 +277,11 @@ module Internal {
183
277
*/
184
278
abstract predicate candidate ( ControlFlowElement x , ControlFlowElement y ) ;
185
279
186
- private predicate candidateInternal ( ControlFlowElement x , ControlFlowElement y ) {
187
- candidate ( x , y )
188
- or
189
- exists ( ControlFlowElement xParent , ControlFlowElement yParent , int i |
190
- candidateInternalChild ( xParent , i , x , yParent )
191
- |
192
- y = yParent .getChild ( i )
193
- )
194
- }
195
-
196
- pragma [ noinline]
197
- private predicate candidateInternalChild (
198
- ControlFlowElement x , int i , ControlFlowElement xChild , ControlFlowElement y
199
- ) {
200
- candidateInternal ( x , y ) and
201
- xChild = x .getChild ( i )
202
- }
203
-
204
- private predicate sameByValue ( Expr x , Expr y ) { sameByValueAux ( x , y , y .getValue ( ) ) }
205
-
206
- pragma [ nomagic]
207
- private predicate sameByValueAux ( Expr x , Expr y , string value ) {
208
- candidateInternal ( x , y ) and
209
- value = x .getValue ( )
210
- }
211
-
212
- private ControlFlowElement getRankedChild ( ControlFlowElement cfe , int rnk , int i ) {
213
- ( candidateInternal ( cfe , _) or candidateInternal ( _, cfe ) ) and
214
- i =
215
- rank [ rnk ] ( int j |
216
- exists ( ControlFlowElement child | child = cfe .getChild ( j ) |
217
- not ( j = - 1 and cfe .( MemberAccess ) .targetIsThisInstance ( ) )
218
- )
219
- ) and
220
- result = cfe .getChild ( i )
221
- }
222
-
223
- pragma [ nomagic]
224
- private predicate sameByStructure0 (
225
- ControlFlowElement x , ControlFlowElement y , int elementKind , int children
226
- ) {
227
- candidateInternal ( x , y ) and
228
- elementKind = elementKind ( x ) and
229
- children = getNumberOfActualChildren ( x ) and
230
- not ( x .( Expr ) .hasValue ( ) and y .( Expr ) .hasValue ( ) )
231
- }
232
-
233
- pragma [ nomagic]
234
- private predicate sameByStructure ( ControlFlowElement x , ControlFlowElement y , int i ) {
235
- i = 0 and
236
- // At least one of `x` and `y` must not have a value, they must have
237
- // the same kind, and the same number of children
238
- sameByStructure0 ( x , y , elementKind ( y ) , getNumberOfActualChildren ( y ) ) and
239
- // If one of them has a reference attribute, they should both reference
240
- // the same node
241
- ( exists ( referenceAttribute ( x ) ) implies referenceAttribute ( x ) = referenceAttribute ( y ) ) and
242
- // x is a member access on `this` iff y is
243
- ( x .( MemberAccess ) .targetIsThisInstance ( ) implies y .( MemberAccess ) .targetIsThisInstance ( ) ) and
244
- ( y .( MemberAccess ) .targetIsThisInstance ( ) implies x .( MemberAccess ) .targetIsThisInstance ( ) )
245
- or
246
- exists ( int j | sameByStructure ( x , y , i - 1 ) |
247
- sameInternal ( getRankedChild ( x , i , j ) , getRankedChild ( y , i , j ) )
248
- )
249
- }
250
-
251
- pragma [ nomagic]
252
- private predicate sameInternal ( ControlFlowElement x , ControlFlowElement y ) {
253
- sameByValue ( x , y )
254
- or
255
- sameByStructure ( x , y , getNumberOfActualChildren ( x ) )
256
- }
257
-
258
280
/**
259
281
* Holds if elements `x` and `y` structurally equal. `x` and `y` must be
260
282
* flagged as candidates for structural equality, that is,
261
283
* `candidate(x, y)` must hold.
262
284
*/
263
- predicate same ( ControlFlowElement x , ControlFlowElement y ) {
264
- candidate ( x , y ) and
265
- sameInternal ( x , y )
266
- }
285
+ predicate same ( ControlFlowElement x , ControlFlowElement y ) { candidate ( x , y ) and sameGvn ( x , y ) }
267
286
}
268
287
}
0 commit comments