@@ -56,20 +56,23 @@ private cached newtype HCBase =
56
56
}
57
57
or
58
58
HC_FieldAccess ( HashCons s , Field f ) {
59
- mk_DotFieldAccess ( s , f , _) or
60
- mk_PointerFieldAccess_with_deref ( s , f , _) or
61
- mk_ImplicitThisFieldAccess_with_deref ( s , f , _)
59
+ mk_DotFieldAccess ( s , f , _)
62
60
}
63
61
or
64
62
HC_Deref ( HashCons p ) {
65
- mk_Deref ( p , _) or
66
- mk_PointerFieldAccess ( p , _, _) or
67
- mk_ImplicitThisFieldAccess_with_qualifier ( p , _, _)
63
+ mk_Deref ( p , _)
64
+ }
65
+ or
66
+ HC_PointerFieldAccess ( HashCons qual , Field target ) {
67
+ mk_PointerFieldAccess ( qual , target , _)
68
68
}
69
69
or
70
70
HC_ThisExpr ( Function fcn ) {
71
- mk_ThisExpr ( fcn , _) or
72
- mk_ImplicitThisFieldAccess ( fcn , _, _)
71
+ mk_ThisExpr ( fcn , _)
72
+ }
73
+ or
74
+ HC_ImplicitThisFieldAccess ( Function fcn , Field target ) {
75
+ mk_ImplicitThisFieldAccess ( fcn , target , _)
73
76
}
74
77
or
75
78
HC_Conversion ( Type t , HashCons child ) { mk_Conversion ( t , child , _) }
@@ -368,17 +371,6 @@ private predicate mk_PointerFieldAccess(
368
371
qualifier = hashCons ( access .getQualifier ( ) .getFullyConverted ( ) )
369
372
}
370
373
371
- /*
372
- * `obj->field` is equivalent to `(*obj).field`, so we need to wrap an
373
- * extra `HC_Deref` around the qualifier.
374
- */
375
- private predicate mk_PointerFieldAccess_with_deref ( HashCons new_qualifier , Field target ,
376
- PointerFieldAccess access ) {
377
- exists ( HashCons qualifier
378
- | mk_PointerFieldAccess ( qualifier , target , access ) and
379
- new_qualifier = HC_Deref ( qualifier ) )
380
- }
381
-
382
374
private predicate analyzableImplicitThisFieldAccess ( ImplicitThisFieldAccess access ) {
383
375
strictcount ( access .getTarget ( ) ) = 1 and
384
376
strictcount ( access .getEnclosingFunction ( ) ) = 1
@@ -391,21 +383,6 @@ private predicate mk_ImplicitThisFieldAccess(Function fcn, Field target,
391
383
fcn = access .getEnclosingFunction ( )
392
384
}
393
385
394
- private predicate mk_ImplicitThisFieldAccess_with_qualifier ( HashCons qualifier , Field target ,
395
- ImplicitThisFieldAccess access ) {
396
- exists ( Function fcn
397
- | mk_ImplicitThisFieldAccess ( fcn , target , access ) and
398
- qualifier = HC_ThisExpr ( fcn ) )
399
- }
400
-
401
- private predicate mk_ImplicitThisFieldAccess_with_deref ( HashCons new_qualifier , Field target ,
402
- ImplicitThisFieldAccess access ) {
403
- exists ( HashCons qualifier
404
- | mk_ImplicitThisFieldAccess_with_qualifier (
405
- qualifier , target , access ) and
406
- new_qualifier = HC_Deref ( qualifier ) )
407
- }
408
-
409
386
private predicate analyzableVariable ( VariableAccess access ) {
410
387
not ( access instanceof FieldAccess ) and
411
388
strictcount ( access .getTarget ( ) ) = 1
@@ -976,12 +953,12 @@ cached HashCons hashCons(Expr e) {
976
953
result = HC_FieldAccess ( qualifier , target ) )
977
954
or
978
955
exists ( HashCons qualifier , Field target
979
- | mk_PointerFieldAccess_with_deref ( qualifier , target , e ) and
980
- result = HC_FieldAccess ( qualifier , target ) )
956
+ | mk_PointerFieldAccess ( qualifier , target , e ) and
957
+ result = HC_PointerFieldAccess ( qualifier , target ) )
981
958
or
982
- exists ( HashCons qualifier , Field target
983
- | mk_ImplicitThisFieldAccess_with_deref ( qualifier , target , e ) and
984
- result = HC_FieldAccess ( qualifier , target ) )
959
+ exists ( Function fcn , Field target
960
+ | mk_ImplicitThisFieldAccess ( fcn , target , e ) and
961
+ result = HC_ImplicitThisFieldAccess ( fcn , target ) )
985
962
or
986
963
exists ( Function fcn
987
964
| mk_ThisExpr ( fcn , e ) and
0 commit comments