@@ -55,13 +55,13 @@ private cached newtype HCBase =
55
55
mk_Variable ( x , _)
56
56
}
57
57
or
58
- HC_FieldAccess ( HC s , Field f ) {
58
+ HC_FieldAccess ( HashCons s , Field f ) {
59
59
mk_DotFieldAccess ( s , f , _) or
60
60
mk_PointerFieldAccess_with_deref ( s , f , _) or
61
61
mk_ImplicitThisFieldAccess_with_deref ( s , f , _)
62
62
}
63
63
or
64
- HC_Deref ( HC p ) {
64
+ HC_Deref ( HashCons p ) {
65
65
mk_Deref ( p , _) or
66
66
mk_PointerFieldAccess ( p , _, _) or
67
67
mk_ImplicitThisFieldAccess_with_qualifier ( p , _, _)
@@ -72,23 +72,23 @@ private cached newtype HCBase =
72
72
mk_ImplicitThisFieldAccess ( fcn , _, _)
73
73
}
74
74
or
75
- HC_Conversion ( Type t , HC child ) { mk_Conversion ( t , child , _) }
75
+ HC_Conversion ( Type t , HashCons child ) { mk_Conversion ( t , child , _) }
76
76
or
77
- HC_BinaryOp ( HC lhs , HC rhs , string opname ) {
77
+ HC_BinaryOp ( HashCons lhs , HashCons rhs , string opname ) {
78
78
mk_BinaryOp ( lhs , rhs , opname , _)
79
79
}
80
80
or
81
- HC_UnaryOp ( HC child , string opname ) { mk_UnaryOp ( child , opname , _) }
81
+ HC_UnaryOp ( HashCons child , string opname ) { mk_UnaryOp ( child , opname , _) }
82
82
or
83
- HC_ArrayAccess ( HC x , HC i ) {
83
+ HC_ArrayAccess ( HashCons x , HashCons i ) {
84
84
mk_ArrayAccess ( x , i , _)
85
85
}
86
86
or
87
87
HC_NonmemberFunctionCall ( Function fcn , HC_Args args ) {
88
88
mk_NonmemberFunctionCall ( fcn , args , _)
89
89
}
90
90
or
91
- HC_MemberFunctionCall ( Function trg , HC qual , HC_Args args ) {
91
+ HC_MemberFunctionCall ( Function trg , HashCons qual , HC_Args args ) {
92
92
mk_MemberFunctionCall ( trg , qual , args , _)
93
93
}
94
94
or
@@ -101,11 +101,11 @@ private cached newtype HC_Args =
101
101
HC_EmptyArgs ( Function fcn ) {
102
102
any ( )
103
103
}
104
- or HC_ArgCons ( Function fcn , HC hc , int i , HC_Args list ) {
104
+ or HC_ArgCons ( Function fcn , HashCons hc , int i , HC_Args list ) {
105
105
mk_ArgCons ( fcn , hc , i , list , _)
106
106
}
107
107
/**
108
- * HC is the hash-cons of an expression. The relationship between `Expr`
108
+ * HashCons is the hash-cons of an expression. The relationship between `Expr`
109
109
* and `HC` is many-to-one: every `Expr` has exactly one `HC`, but multiple
110
110
* expressions can have the same `HC`. If two expressions have the same
111
111
* `HC`, it means that they are structurally equal. The `HC` is an opaque
@@ -118,9 +118,7 @@ private cached newtype HC_Args =
118
118
* expression with this `HC` and using its `toString` and `getLocation`
119
119
* methods.
120
120
*/
121
- class HC extends HCBase {
122
- HC ( ) { this instanceof HCBase }
123
-
121
+ class HashCons extends HCBase {
124
122
/** Gets an expression that has this HC. */
125
123
Expr getAnExpr ( ) {
126
124
this = hashCons ( result )
@@ -234,7 +232,7 @@ private predicate analyzableDotFieldAccess(DotFieldAccess access) {
234
232
}
235
233
236
234
private predicate mk_DotFieldAccess (
237
- HC qualifier , Field target , DotFieldAccess access ) {
235
+ HashCons qualifier , Field target , DotFieldAccess access ) {
238
236
analyzableDotFieldAccess ( access ) and
239
237
target = access .getTarget ( ) and
240
238
qualifier = hashCons ( access .getQualifier ( ) .getFullyConverted ( ) )
@@ -246,9 +244,9 @@ private predicate analyzablePointerFieldAccess(PointerFieldAccess access) {
246
244
}
247
245
248
246
private predicate mk_PointerFieldAccess (
249
- HC qualifier , Field target ,
247
+ HashCons qualifier , Field target ,
250
248
PointerFieldAccess access ) {
251
- analyzablePointerFieldAccess ( access ) and
249
+ analyzablePointerFieldAccess ( access ) and
252
250
target = access .getTarget ( ) and
253
251
qualifier = hashCons ( access .getQualifier ( ) .getFullyConverted ( ) )
254
252
}
@@ -257,38 +255,35 @@ private predicate mk_PointerFieldAccess(
257
255
* `obj->field` is equivalent to `(*obj).field`, so we need to wrap an
258
256
* extra `HC_Deref` around the qualifier.
259
257
*/
260
- private predicate mk_PointerFieldAccess_with_deref (
261
- HC new_qualifier , Field target , PointerFieldAccess access ) {
262
- exists ( HC qualifier
258
+ private predicate mk_PointerFieldAccess_with_deref ( HashCons new_qualifier , Field target ,
259
+ PointerFieldAccess access ) {
260
+ exists ( HashCons qualifier
263
261
| mk_PointerFieldAccess ( qualifier , target , access ) and
264
262
new_qualifier = HC_Deref ( qualifier ) )
265
263
}
266
264
267
- private predicate analyzableImplicitThisFieldAccess (
268
- ImplicitThisFieldAccess access ) {
265
+ private predicate analyzableImplicitThisFieldAccess ( ImplicitThisFieldAccess access ) {
269
266
strictcount ( access .getTarget ( ) ) = 1 and
270
267
strictcount ( access .getEnclosingFunction ( ) ) = 1
271
268
}
272
269
273
- private predicate mk_ImplicitThisFieldAccess (
274
- Function fcn , Field target ,
270
+ private predicate mk_ImplicitThisFieldAccess ( Function fcn , Field target ,
275
271
ImplicitThisFieldAccess access ) {
276
272
analyzableImplicitThisFieldAccess ( access ) and
277
273
target = access .getTarget ( ) and
278
274
fcn = access .getEnclosingFunction ( )
279
275
}
280
276
281
- private predicate mk_ImplicitThisFieldAccess_with_qualifier (
282
- HC qualifier , Field target ,
277
+ private predicate mk_ImplicitThisFieldAccess_with_qualifier ( HashCons qualifier , Field target ,
283
278
ImplicitThisFieldAccess access ) {
284
279
exists ( Function fcn
285
280
| mk_ImplicitThisFieldAccess ( fcn , target , access ) and
286
281
qualifier = HC_ThisExpr ( fcn ) )
287
282
}
288
283
289
- private predicate mk_ImplicitThisFieldAccess_with_deref (
290
- HC new_qualifier , Field target , ImplicitThisFieldAccess access ) {
291
- exists ( HC qualifier
284
+ private predicate mk_ImplicitThisFieldAccess_with_deref ( HashCons new_qualifier , Field target ,
285
+ ImplicitThisFieldAccess access ) {
286
+ exists ( HashCons qualifier
292
287
| mk_ImplicitThisFieldAccess_with_qualifier (
293
288
qualifier , target , access ) and
294
289
new_qualifier = HC_Deref ( qualifier ) )
@@ -309,7 +304,7 @@ private predicate analyzableConversion(Conversion conv) {
309
304
strictcount ( conv .getExpr ( ) ) = 1
310
305
}
311
306
312
- private predicate mk_Conversion ( Type t , HC child , Conversion conv ) {
307
+ private predicate mk_Conversion ( Type t , HashCons child , Conversion conv ) {
313
308
analyzableConversion ( conv ) and
314
309
t = conv .getType ( ) .getUnspecifiedType ( ) and
315
310
child = hashCons ( conv .getExpr ( ) )
@@ -321,8 +316,7 @@ private predicate analyzableBinaryOp(BinaryOperation op) {
321
316
strictcount ( op .getOperator ( ) ) = 1
322
317
}
323
318
324
- private predicate mk_BinaryOp (
325
- HC lhs , HC rhs , string opname , BinaryOperation op ) {
319
+ private predicate mk_BinaryOp ( HashCons lhs , HashCons rhs , string opname , BinaryOperation op ) {
326
320
analyzableBinaryOp ( op ) and
327
321
lhs = hashCons ( op .getLeftOperand ( ) .getFullyConverted ( ) ) and
328
322
rhs = hashCons ( op .getRightOperand ( ) .getFullyConverted ( ) ) and
@@ -335,7 +329,7 @@ private predicate analyzableUnaryOp(UnaryOperation op) {
335
329
strictcount ( op .getOperator ( ) ) = 1
336
330
}
337
331
338
- private predicate mk_UnaryOp ( HC child , string opname , UnaryOperation op ) {
332
+ private predicate mk_UnaryOp ( HashCons child , string opname , UnaryOperation op ) {
339
333
analyzableUnaryOp ( op ) and
340
334
child = hashCons ( op .getOperand ( ) .getFullyConverted ( ) ) and
341
335
opname = op .getOperator ( )
@@ -355,40 +349,36 @@ private predicate analyzableArrayAccess(ArrayExpr ae) {
355
349
strictcount ( ae .getArrayOffset ( ) .getFullyConverted ( ) ) = 1
356
350
}
357
351
358
- private predicate mk_ArrayAccess (
359
- HC base , HC offset , ArrayExpr ae ) {
352
+ private predicate mk_ArrayAccess ( HashCons base , HashCons offset , ArrayExpr ae ) {
360
353
analyzableArrayAccess ( ae ) and
361
354
base = hashCons ( ae .getArrayBase ( ) .getFullyConverted ( ) ) and
362
355
offset = hashCons ( ae .getArrayOffset ( ) .getFullyConverted ( ) )
363
356
}
364
357
365
- private predicate analyzablePointerDereferenceExpr (
366
- PointerDereferenceExpr deref ) {
358
+ private predicate analyzablePointerDereferenceExpr ( PointerDereferenceExpr deref ) {
367
359
strictcount ( deref .getOperand ( ) .getFullyConverted ( ) ) = 1
368
360
}
369
361
370
- private predicate mk_Deref (
371
- HC p , PointerDereferenceExpr deref ) {
362
+ private predicate mk_Deref ( HashCons p , PointerDereferenceExpr deref ) {
372
363
analyzablePointerDereferenceExpr ( deref ) and
373
364
p = hashCons ( deref .getOperand ( ) .getFullyConverted ( ) )
374
365
}
375
366
376
- private predicate analyzableNonmemberFunctionCall (
377
- FunctionCall fc ) {
378
- forall ( int i | exists ( fc .getArgument ( i ) ) | strictcount ( fc .getArgument ( i ) .getFullyConverted ( ) ) = 1 ) and
367
+ private predicate analyzableNonmemberFunctionCall ( FunctionCall fc ) {
368
+ forall ( int i |
369
+ exists ( fc .getArgument ( i ) ) |
370
+ strictcount ( fc .getArgument ( i ) .getFullyConverted ( ) ) = 1
371
+ ) and
379
372
strictcount ( fc .getTarget ( ) ) = 1 and
380
373
not exists ( fc .getQualifier ( ) )
381
374
}
382
375
383
- private predicate mk_NonmemberFunctionCall (
384
- Function fcn ,
385
- HC_Args args ,
386
- FunctionCall fc
376
+ private predicate mk_NonmemberFunctionCall ( Function fcn , HC_Args args , FunctionCall fc
387
377
) {
388
378
fc .getTarget ( ) = fcn and
389
379
analyzableNonmemberFunctionCall ( fc ) and
390
380
(
391
- exists ( HC head , HC_Args tail |
381
+ exists ( HashCons head , HC_Args tail |
392
382
args = HC_ArgCons ( fcn , head , fc .getNumberOfArguments ( ) - 1 , tail ) and
393
383
mk_ArgCons ( fcn , head , fc .getNumberOfArguments ( ) - 1 , tail , fc )
394
384
)
@@ -400,22 +390,25 @@ private predicate mk_NonmemberFunctionCall(
400
390
401
391
private predicate analyzableMemberFunctionCall (
402
392
FunctionCall fc ) {
403
- forall ( int i | exists ( fc .getArgument ( i ) ) | strictcount ( fc .getArgument ( i ) .getFullyConverted ( ) ) = 1 ) and
393
+ forall ( int i |
394
+ exists ( fc .getArgument ( i ) ) |
395
+ strictcount ( fc .getArgument ( i ) .getFullyConverted ( ) ) = 1
396
+ ) and
404
397
strictcount ( fc .getTarget ( ) ) = 1 and
405
398
strictcount ( fc .getQualifier ( ) .getFullyConverted ( ) ) = 1
406
399
}
407
400
408
401
private predicate mk_MemberFunctionCall (
409
402
Function fcn ,
410
- HC qual ,
403
+ HashCons qual ,
411
404
HC_Args args ,
412
405
FunctionCall fc
413
406
) {
414
407
fc .getTarget ( ) = fcn and
415
408
analyzableMemberFunctionCall ( fc ) and
416
409
hashCons ( fc .getQualifier ( ) .getFullyConverted ( ) ) = qual and
417
410
(
418
- exists ( HC head , HC_Args tail |
411
+ exists ( HashCons head , HC_Args tail |
419
412
args = HC_ArgCons ( fcn , head , fc .getNumberOfArguments ( ) - 1 , tail ) and
420
413
mk_ArgCons ( fcn , head , fc .getNumberOfArguments ( ) - 1 , tail , fc )
421
414
)
@@ -434,15 +427,15 @@ private predicate analyzableFunctionCall(
434
427
}
435
428
436
429
/**
437
- * Holds if `fc` is a call to `fcn`, `fc`'s first `i-1 ` arguments have hash-cons
438
- * `list`, and `fc`'s `i`th argument has hash-cons `hc`
430
+ * Holds if `fc` is a call to `fcn`, `fc`'s first `i` arguments have hash-cons
431
+ * `list`, and `fc`'s argument at index `i` has hash-cons `hc`.
439
432
*/
440
- private predicate mk_ArgCons ( Function fcn , HC hc , int i , HC_Args list , FunctionCall fc ) {
433
+ private predicate mk_ArgCons ( Function fcn , HashCons hc , int i , HC_Args list , FunctionCall fc ) {
441
434
analyzableFunctionCall ( fc ) and
442
435
fc .getTarget ( ) = fcn and
443
436
hc = hashCons ( fc .getArgument ( i ) .getFullyConverted ( ) ) and
444
437
(
445
- exists ( HC head , HC_Args tail |
438
+ exists ( HashCons head , HC_Args tail |
446
439
list = HC_ArgCons ( fcn , head , i - 1 , tail ) and
447
440
mk_ArgCons ( fcn , head , i - 1 , tail , fc ) and
448
441
i > 0
@@ -454,7 +447,7 @@ private predicate mk_ArgCons(Function fcn, HC hc, int i, HC_Args list, FunctionC
454
447
}
455
448
456
449
/** Gets the hash-cons of expression `e`. */
457
- cached HC hashCons ( Expr e ) {
450
+ cached HashCons hashCons ( Expr e ) {
458
451
exists ( int val , Type t
459
452
| mk_IntLiteral ( val , t , e ) and
460
453
result = HC_IntLiteral ( val , t ) )
@@ -471,44 +464,43 @@ cached HC hashCons(Expr e) {
471
464
| mk_StringLiteral ( val , t , e ) and
472
465
result = HC_StringLiteral ( val , t ) )
473
466
or
474
- // Variable with no SSA information.
475
467
exists ( Variable x
476
468
| mk_Variable ( x , e ) and
477
469
result = HC_Variable ( x ) )
478
470
or
479
- exists ( HC qualifier , Field target
471
+ exists ( HashCons qualifier , Field target
480
472
| mk_DotFieldAccess ( qualifier , target , e ) and
481
473
result = HC_FieldAccess ( qualifier , target ) )
482
474
or
483
- exists ( HC qualifier , Field target
475
+ exists ( HashCons qualifier , Field target
484
476
| mk_PointerFieldAccess_with_deref ( qualifier , target , e ) and
485
477
result = HC_FieldAccess ( qualifier , target ) )
486
478
or
487
- exists ( HC qualifier , Field target
479
+ exists ( HashCons qualifier , Field target
488
480
| mk_ImplicitThisFieldAccess_with_deref ( qualifier , target , e ) and
489
481
result = HC_FieldAccess ( qualifier , target ) )
490
482
or
491
483
exists ( Function fcn
492
484
| mk_ThisExpr ( fcn , e ) and
493
485
result = HC_ThisExpr ( fcn ) )
494
486
or
495
- exists ( Type t , HC child
487
+ exists ( Type t , HashCons child
496
488
| mk_Conversion ( t , child , e ) and
497
489
result = HC_Conversion ( t , child ) )
498
490
or
499
- exists ( HC lhs , HC rhs , string opname
491
+ exists ( HashCons lhs , HashCons rhs , string opname
500
492
| mk_BinaryOp ( lhs , rhs , opname , e ) and
501
493
result = HC_BinaryOp ( lhs , rhs , opname ) )
502
494
or
503
- exists ( HC child , string opname
495
+ exists ( HashCons child , string opname
504
496
| mk_UnaryOp ( child , opname , e ) and
505
497
result = HC_UnaryOp ( child , opname ) )
506
498
or
507
- exists ( HC x , HC i
499
+ exists ( HashCons x , HashCons i
508
500
| mk_ArrayAccess ( x , i , e ) and
509
501
result = HC_ArrayAccess ( x , i ) )
510
502
or
511
- exists ( HC p
503
+ exists ( HashCons p
512
504
| mk_Deref ( p , e ) and
513
505
result = HC_Deref ( p ) )
514
506
or
@@ -517,7 +509,7 @@ cached HC hashCons(Expr e) {
517
509
result = HC_NonmemberFunctionCall ( fcn , args )
518
510
)
519
511
or
520
- exists ( Function fcn , HC qual , HC_Args args
512
+ exists ( Function fcn , HashCons qual , HC_Args args
521
513
| mk_MemberFunctionCall ( fcn , qual , args , e ) and
522
514
result = HC_MemberFunctionCall ( fcn , qual , args )
523
515
)
0 commit comments