@@ -56,20 +56,23 @@ private cached newtype HCBase =
5656 }
5757 or
5858 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 , _)
6260 }
6361 or
6462 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 , _)
6868 }
6969 or
7070 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 , _)
7376 }
7477 or
7578 HC_Conversion ( Type t , HashCons child ) { mk_Conversion ( t , child , _) }
@@ -368,17 +371,6 @@ private predicate mk_PointerFieldAccess(
368371 qualifier = hashCons ( access .getQualifier ( ) .getFullyConverted ( ) )
369372}
370373
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-
382374private predicate analyzableImplicitThisFieldAccess ( ImplicitThisFieldAccess access ) {
383375 strictcount ( access .getTarget ( ) ) = 1 and
384376 strictcount ( access .getEnclosingFunction ( ) ) = 1
@@ -391,21 +383,6 @@ private predicate mk_ImplicitThisFieldAccess(Function fcn, Field target,
391383 fcn = access .getEnclosingFunction ( )
392384}
393385
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-
409386private predicate analyzableVariable ( VariableAccess access ) {
410387 not ( access instanceof FieldAccess ) and
411388 strictcount ( access .getTarget ( ) ) = 1
@@ -976,12 +953,12 @@ cached HashCons hashCons(Expr e) {
976953 result = HC_FieldAccess ( qualifier , target ) )
977954 or
978955 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 ) )
981958 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 ) )
985962 or
986963 exists ( Function fcn
987964 | mk_ThisExpr ( fcn , e ) and
0 commit comments