@@ -128,8 +128,69 @@ private class GvnCons extends GvnList, TGvnCons {
128
128
override string toString ( ) { result = head .toString ( ) + " :: " + tail .toString ( ) }
129
129
}
130
130
131
+ /**
132
+ * Gets the `GvnKind` of the element `cfe`.
133
+ * In case `cfe` is a reference attribute, we encode the entire declaration and whether
134
+ * the target is semantically equivalent to `this`.
135
+ */
136
+ private GvnKind getGvnKind ( ControlFlowElement cfe ) {
137
+ exists ( GvnKind kind |
138
+ kind = getKind ( cfe ) and
139
+ (
140
+ result = TGvnKindDeclaration ( kind , isTargetThis ( cfe ) , referenceAttribute ( cfe ) )
141
+ or
142
+ not exists ( referenceAttribute ( cfe ) ) and
143
+ result = kind
144
+ )
145
+ )
146
+ }
147
+
148
+ private GvnList gvnConstructed ( ControlFlowElement cfe , GvnKind kind , int index ) {
149
+ kind = getGvnKind ( cfe ) and
150
+ result = TGvnNil ( kind ) and
151
+ index = - 1
152
+ or
153
+ exists ( Gvn head , GvnList tail |
154
+ gvnConstructedCons ( cfe , kind , index , head , tail ) and
155
+ result = TGvnCons ( head , tail )
156
+ )
157
+ }
158
+
159
+ private int getNumberOfActualChildren ( ControlFlowElement cfe ) {
160
+ if cfe .( MemberAccess ) .targetIsThisInstance ( )
161
+ then result = cfe .getNumberOfChildren ( ) - 1
162
+ else result = cfe .getNumberOfChildren ( )
163
+ }
164
+
165
+ private ControlFlowElement getRankedChild ( ControlFlowElement cfe , int rnk ) {
166
+ result =
167
+ rank [ rnk + 1 ] ( ControlFlowElement child , int j |
168
+ child = cfe .getChild ( j ) and
169
+ (
170
+ j >= 0
171
+ or
172
+ j = - 1 and not cfe .( MemberAccess ) .targetIsThisInstance ( )
173
+ )
174
+ |
175
+ child order by j
176
+ )
177
+ }
178
+
131
179
private predicate gvnConstructedCons (
132
180
ControlFlowElement e , GvnKind kind , int index , Gvn head , GvnList tail
133
181
) {
134
- none ( )
182
+ tail = gvnConstructed ( e , kind , index - 1 ) and
183
+ head = toGvn ( getRankedChild ( e , index ) )
184
+ }
185
+
186
+ /** Gets the global value number of the element `cfe` */
187
+ Gvn toGvn ( ControlFlowElement cfe ) {
188
+ result = TConstantGvn ( cfe .( Expr ) .getValue ( ) )
189
+ or
190
+ not exists ( cfe .( Expr ) .getValue ( ) ) and
191
+ exists ( GvnList l , GvnKind kind , int index |
192
+ l = gvnConstructed ( cfe , kind , index - 1 ) and
193
+ index = getNumberOfActualChildren ( cfe ) and
194
+ result = TListGvn ( l )
195
+ )
135
196
}
0 commit comments