@@ -1410,8 +1410,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1410
1410
bindingset [ node, ap, isStoreStep]
1411
1411
predicate stepFilter ( NodeEx node , Ap ap , boolean isStoreStep ) ;
1412
1412
1413
- bindingset [ typ , contentType ]
1414
- predicate typecheckStore ( Typ typ , DataFlowType contentType ) ;
1413
+ bindingset [ t1 , t2 ]
1414
+ predicate typecheck ( Typ t1 , Typ t2 ) ;
1415
1415
1416
1416
default predicate enableTypeFlow ( ) { any ( ) }
1417
1417
}
@@ -1641,7 +1641,9 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
1641
1641
not inBarrier ( node2 , state ) and
1642
1642
PrevStage:: storeStepCand ( node1 , apa1 , c , node2 , contentType , containerType ) and
1643
1643
t2 = getTyp ( containerType ) and
1644
- typecheckStore ( t1 , contentType )
1644
+ // We need to typecheck stores here, since reverse flow through a getter
1645
+ // might have a different type here compared to inside the getter.
1646
+ typecheck ( t1 , getTyp ( contentType ) )
1645
1647
)
1646
1648
}
1647
1649
@@ -3742,8 +3744,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3742
3744
bindingset [ node, ap, isStoreStep]
3743
3745
predicate stepFilter ( NodeEx node , Ap ap , boolean isStoreStep ) { any ( ) }
3744
3746
3745
- bindingset [ typ , contentType ]
3746
- predicate typecheckStore ( Typ typ , DataFlowType contentType ) { any ( ) }
3747
+ bindingset [ t1 , t2 ]
3748
+ predicate typecheck ( Typ t1 , Typ t2 ) { any ( ) }
3747
3749
3748
3750
predicate enableTypeFlow ( ) { none ( ) }
3749
3751
}
@@ -3855,8 +3857,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3855
3857
bindingset [ node, ap, isStoreStep]
3856
3858
predicate stepFilter ( NodeEx node , Ap ap , boolean isStoreStep ) { any ( ) }
3857
3859
3858
- bindingset [ typ , contentType ]
3859
- predicate typecheckStore ( Typ typ , DataFlowType contentType ) { any ( ) }
3860
+ bindingset [ t1 , t2 ]
3861
+ predicate typecheck ( Typ t1 , Typ t2 ) { any ( ) }
3860
3862
}
3861
3863
3862
3864
private module Stage3 = MkStage< Stage2 > :: Stage< Stage3Param > ;
@@ -3975,12 +3977,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
3975
3977
if clearExceptStore ( node , ap ) then isStoreStep = true else any ( )
3976
3978
}
3977
3979
3978
- bindingset [ typ, contentType]
3979
- predicate typecheckStore ( Typ typ , DataFlowType contentType ) {
3980
- // We need to typecheck stores here, since reverse flow through a getter
3981
- // might have a different type here compared to inside the getter.
3982
- compatibleTypesFilter ( typ , contentType )
3983
- }
3980
+ bindingset [ t1, t2]
3981
+ predicate typecheck ( Typ t1 , Typ t2 ) { compatibleTypesFilter ( t1 , t2 ) }
3984
3982
}
3985
3983
3986
3984
private module Stage4 = MkStage< Stage3 > :: Stage< Stage4Param > ;
@@ -4227,10 +4225,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
4227
4225
if clearExceptStore ( node , ap ) then isStoreStep = true else any ( )
4228
4226
}
4229
4227
4230
- bindingset [ typ, contentType]
4231
- predicate typecheckStore ( Typ typ , DataFlowType contentType ) {
4232
- compatibleTypesFilter ( typ , contentType )
4233
- }
4228
+ bindingset [ t1, t2]
4229
+ predicate typecheck ( Typ t1 , Typ t2 ) { compatibleTypesFilter ( t1 , t2 ) }
4234
4230
}
4235
4231
4236
4232
private module Stage5 = MkStage< Stage4 > :: Stage< Stage5Param > ;
@@ -4426,10 +4422,8 @@ module MakeImpl<LocationSig Location, InputSig<Location> Lang> {
4426
4422
if clearExceptStore ( node , ap ) then isStoreStep = true else any ( )
4427
4423
}
4428
4424
4429
- bindingset [ typ, contentType]
4430
- predicate typecheckStore ( Typ typ , DataFlowType contentType ) {
4431
- compatibleTypesFilter ( typ , contentType )
4432
- }
4425
+ bindingset [ t1, t2]
4426
+ predicate typecheck ( Typ t1 , Typ t2 ) { compatibleTypesFilter ( t1 , t2 ) }
4433
4427
}
4434
4428
4435
4429
module Stage6 = MkStage< Stage5 > :: Stage< Stage6Param > ;
0 commit comments