@@ -289,7 +289,7 @@ private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config)
289
289
exists ( Node mid |
290
290
useFieldFlow ( config ) and
291
291
nodeCandFwd1 ( mid , fromArg , config ) and
292
- store ( mid , _, node ) and
292
+ store ( mid , _, node , _ ) and
293
293
not outBarrier ( mid , config )
294
294
)
295
295
or
@@ -337,7 +337,7 @@ private predicate nodeCandFwd1IsStored(Content c, Configuration config) {
337
337
not fullBarrier ( node , config ) and
338
338
useFieldFlow ( config ) and
339
339
nodeCandFwd1 ( mid , config ) and
340
- store ( mid , tc , node ) and
340
+ store ( mid , tc , node , _ ) and
341
341
c = tc .getContent ( )
342
342
)
343
343
}
@@ -469,7 +469,7 @@ private predicate nodeCand1Store(Content c, Node node, boolean toReturn, Configu
469
469
exists ( Node mid , TypedContent tc |
470
470
nodeCand1 ( mid , toReturn , config ) and
471
471
nodeCandFwd1IsStored ( c , unbind ( config ) ) and
472
- store ( node , tc , mid ) and
472
+ store ( node , tc , mid , _ ) and
473
473
c = tc .getContent ( )
474
474
)
475
475
}
@@ -571,11 +571,11 @@ private predicate parameterThroughFlowNodeCand1(ParameterNode p, Configuration c
571
571
}
572
572
573
573
pragma [ nomagic]
574
- private predicate store ( Node n1 , Content c , Node n2 , Configuration config ) {
574
+ private predicate storeCand1 ( Node n1 , Content c , Node n2 , Configuration config ) {
575
575
exists ( TypedContent tc |
576
576
nodeCand1IsReadAndStored ( c , config ) and
577
577
nodeCand1 ( n2 , unbind ( config ) ) and
578
- store ( n1 , tc , n2 ) and
578
+ store ( n1 , tc , n2 , _ ) and
579
579
c = tc .getContent ( )
580
580
)
581
581
}
@@ -758,7 +758,7 @@ private predicate nodeCandFwd2(
758
758
// store
759
759
exists ( Node mid |
760
760
nodeCandFwd2 ( mid , fromArg , argStored , _, config ) and
761
- store ( mid , _, node , config ) and
761
+ storeCand1 ( mid , _, node , config ) and
762
762
stored = true
763
763
)
764
764
or
@@ -797,7 +797,7 @@ private predicate nodeCandFwd2IsStored(Content c, boolean stored, Configuration
797
797
useFieldFlow ( config ) and
798
798
nodeCand1 ( node , unbind ( config ) ) and
799
799
nodeCandFwd2 ( mid , _, _, stored , config ) and
800
- store ( mid , c , node , config )
800
+ storeCand1 ( mid , c , node , config )
801
801
)
802
802
}
803
803
@@ -957,7 +957,7 @@ private predicate nodeCand2Store(
957
957
Configuration config
958
958
) {
959
959
exists ( Node mid |
960
- store ( node , c , mid , config ) and
960
+ storeCand1 ( node , c , mid , config ) and
961
961
nodeCand2 ( mid , toReturn , returnRead , true , config ) and
962
962
nodeCandFwd2 ( node , _, _, stored , unbind ( config ) )
963
963
)
@@ -1066,7 +1066,7 @@ private module LocalFlowBigStep {
1066
1066
additionalJumpStep ( _, node , config ) or
1067
1067
node instanceof ParameterNode or
1068
1068
node instanceof OutNodeExt or
1069
- store ( _, _, node ) or
1069
+ store ( _, _, node , _ ) or
1070
1070
read ( _, _, node ) or
1071
1071
node instanceof CastNode
1072
1072
)
@@ -1082,7 +1082,7 @@ private module LocalFlowBigStep {
1082
1082
additionalJumpStep ( node , next , config ) or
1083
1083
flowIntoCallNodeCand1 ( _, node , next , config ) or
1084
1084
flowOutOfCallNodeCand1 ( _, node , next , config ) or
1085
- store ( node , _, next ) or
1085
+ store ( node , _, next , _ ) or
1086
1086
read ( node , _, next )
1087
1087
)
1088
1088
or
@@ -1170,8 +1170,10 @@ private predicate readCand2(Node node1, Content c, Node node2, Configuration con
1170
1170
}
1171
1171
1172
1172
pragma [ nomagic]
1173
- private predicate storeCand2 ( Node node1 , TypedContent tc , Node node2 , Configuration config ) {
1174
- store ( node1 , tc , node2 ) and
1173
+ private predicate storeCand2 (
1174
+ Node node1 , TypedContent tc , Node node2 , DataFlowType contentType , Configuration config
1175
+ ) {
1176
+ store ( node1 , tc , node2 , contentType ) and
1175
1177
nodeCand2 ( node1 , config ) and
1176
1178
nodeCand2 ( node2 , _, _, true , unbind ( config ) ) and
1177
1179
nodeCand2IsReadAndStored ( tc .getContent ( ) , unbind ( config ) )
@@ -1235,11 +1237,12 @@ private predicate flowCandFwd0(
1235
1237
)
1236
1238
or
1237
1239
// store
1238
- exists ( Node mid , TypedContent tc |
1239
- flowCandFwd ( mid , fromArg , argApf , _ , config ) and
1240
- storeCand2 ( mid , tc , node , config ) and
1240
+ exists ( Node mid , TypedContent tc , AccessPathFront apf0 , DataFlowType contentType |
1241
+ flowCandFwd ( mid , fromArg , argApf , apf0 , config ) and
1242
+ storeCand2 ( mid , tc , node , contentType , config ) and
1241
1243
nodeCand2 ( node , _, _, true , unbind ( config ) ) and
1242
- apf .headUsesContent ( tc )
1244
+ apf .headUsesContent ( tc ) and
1245
+ compatibleTypes ( apf0 .getType ( ) , contentType )
1243
1246
)
1244
1247
or
1245
1248
// read
@@ -1270,11 +1273,11 @@ private predicate flowCandFwd0(
1270
1273
1271
1274
pragma [ nomagic]
1272
1275
private predicate flowCandFwdConsCand ( TypedContent tc , AccessPathFront apf , Configuration config ) {
1273
- exists ( Node mid , Node n |
1276
+ exists ( Node mid , Node n , DataFlowType contentType |
1274
1277
flowCandFwd ( mid , _, _, apf , config ) and
1275
- storeCand2 ( mid , tc , n , config ) and
1278
+ storeCand2 ( mid , tc , n , contentType , config ) and
1276
1279
nodeCand2 ( n , _, _, true , unbind ( config ) ) and
1277
- compatibleTypes ( apf .getType ( ) , mid . getTypeBound ( ) )
1280
+ compatibleTypes ( apf .getType ( ) , contentType )
1278
1281
)
1279
1282
}
1280
1283
@@ -1454,7 +1457,7 @@ private predicate flowCandStore(
1454
1457
) {
1455
1458
exists ( Node mid |
1456
1459
flowCandFwd ( node , _, _, apf , config ) and
1457
- storeCand2 ( node , tc , mid , unbind ( config ) ) and
1460
+ storeCand2 ( node , tc , mid , _ , unbind ( config ) ) and
1458
1461
flowCand ( mid , toReturn , returnApf , TFrontHead ( tc ) , unbind ( config ) )
1459
1462
)
1460
1463
}
@@ -1737,7 +1740,7 @@ private predicate storeCand(
1737
1740
Node mid , TypedContent tc , Node node , AccessPathFront apf0 , AccessPathFront apf ,
1738
1741
Configuration config
1739
1742
) {
1740
- storeCand2 ( mid , tc , node , config ) and
1743
+ storeCand2 ( mid , tc , node , _ , config ) and
1741
1744
flowCand ( mid , _, _, apf0 , config ) and
1742
1745
apf .headUsesContent ( tc )
1743
1746
}
@@ -1919,7 +1922,7 @@ pragma[nomagic]
1919
1922
private predicate storeFlowFwd (
1920
1923
Node node1 , TypedContent tc , Node node2 , AccessPath ap , AccessPath ap0 , Configuration config
1921
1924
) {
1922
- storeCand2 ( node1 , tc , node2 , config ) and
1925
+ storeCand2 ( node1 , tc , node2 , _ , config ) and
1923
1926
flowFwdStore ( node2 , tc , ap , _, _, _, config ) and
1924
1927
ap0 = push ( tc , ap )
1925
1928
}
@@ -2307,7 +2310,7 @@ private predicate pathReadStep(
2307
2310
2308
2311
pragma [ nomagic]
2309
2312
private predicate storeCand ( Node node1 , TypedContent tc , Node node2 , Configuration config ) {
2310
- storeCand2 ( node1 , tc , node2 , config ) and
2313
+ storeCand2 ( node1 , tc , node2 , _ , config ) and
2311
2314
flow ( node2 , config )
2312
2315
}
2313
2316
@@ -2799,13 +2802,13 @@ private module FlowExploration {
2799
2802
PartialPathNodePriv mid , PartialAccessPath ap1 , TypedContent tc , Node node ,
2800
2803
PartialAccessPath ap2
2801
2804
) {
2802
- exists ( Node midNode |
2805
+ exists ( Node midNode , DataFlowType contentType |
2803
2806
midNode = mid .getNode ( ) and
2804
2807
ap1 = mid .getAp ( ) and
2805
- store ( midNode , tc , node ) and
2808
+ store ( midNode , tc , node , contentType ) and
2806
2809
ap2 .getHead ( ) = tc and
2807
2810
ap2 .len ( ) = unbindInt ( ap1 .len ( ) + 1 ) and
2808
- compatibleTypes ( ap1 .getType ( ) , getErasedNodeTypeBound ( midNode ) )
2811
+ compatibleTypes ( ap1 .getType ( ) , contentType )
2809
2812
)
2810
2813
}
2811
2814
@@ -2830,8 +2833,7 @@ private module FlowExploration {
2830
2833
read ( midNode , tc .getContent ( ) , node ) and
2831
2834
ap .getHead ( ) = tc and
2832
2835
config = mid .getConfiguration ( ) and
2833
- cc = mid .getCallContext ( ) and
2834
- compatibleTypes ( tc .getContainerType ( ) , getErasedNodeTypeBound ( midNode ) )
2836
+ cc = mid .getCallContext ( )
2835
2837
)
2836
2838
}
2837
2839
0 commit comments