@@ -294,9 +294,9 @@ private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config)
294
294
)
295
295
or
296
296
// read
297
- exists ( Content f |
298
- nodeCandFwd1Read ( f , node , fromArg , config ) and
299
- nodeCandFwd1IsStored ( f , config ) and
297
+ exists ( Content c |
298
+ nodeCandFwd1Read ( c , node , fromArg , config ) and
299
+ nodeCandFwd1IsStored ( c , config ) and
300
300
not inBarrier ( node , config )
301
301
)
302
302
or
@@ -321,10 +321,10 @@ private predicate nodeCandFwd1(Node node, boolean fromArg, Configuration config)
321
321
private predicate nodeCandFwd1 ( Node node , Configuration config ) { nodeCandFwd1 ( node , _, config ) }
322
322
323
323
pragma [ nomagic]
324
- private predicate nodeCandFwd1Read ( Content f , Node node , boolean fromArg , Configuration config ) {
324
+ private predicate nodeCandFwd1Read ( Content c , Node node , boolean fromArg , Configuration config ) {
325
325
exists ( Node mid |
326
326
nodeCandFwd1 ( mid , fromArg , config ) and
327
- read ( mid , f , node )
327
+ read ( mid , c , node )
328
328
)
329
329
}
330
330
@@ -421,15 +421,15 @@ private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config)
421
421
)
422
422
or
423
423
// store
424
- exists ( Content f |
425
- nodeCand1Store ( f , node , toReturn , config ) and
426
- nodeCand1IsRead ( f , config )
424
+ exists ( Content c |
425
+ nodeCand1Store ( c , node , toReturn , config ) and
426
+ nodeCand1IsRead ( c , config )
427
427
)
428
428
or
429
429
// read
430
- exists ( Node mid , Content f |
431
- read ( node , f , mid ) and
432
- nodeCandFwd1IsStored ( f , unbind ( config ) ) and
430
+ exists ( Node mid , Content c |
431
+ read ( node , c , mid ) and
432
+ nodeCandFwd1IsStored ( c , unbind ( config ) ) and
433
433
nodeCand1 ( mid , toReturn , config )
434
434
)
435
435
or
@@ -451,15 +451,15 @@ private predicate nodeCand1_0(Node node, boolean toReturn, Configuration config)
451
451
}
452
452
453
453
/**
454
- * Holds if `f ` is the target of a read in the flow covered by `nodeCand1`.
454
+ * Holds if `c ` is the target of a read in the flow covered by `nodeCand1`.
455
455
*/
456
456
pragma [ nomagic]
457
- private predicate nodeCand1IsRead ( Content f , Configuration config ) {
457
+ private predicate nodeCand1IsRead ( Content c , Configuration config ) {
458
458
exists ( Node mid , Node node |
459
459
useFieldFlow ( config ) and
460
460
nodeCandFwd1 ( node , unbind ( config ) ) and
461
- read ( node , f , mid ) and
462
- nodeCandFwd1IsStored ( f , unbind ( config ) ) and
461
+ read ( node , c , mid ) and
462
+ nodeCandFwd1IsStored ( c , unbind ( config ) ) and
463
463
nodeCand1 ( mid , _, config )
464
464
)
465
465
}
@@ -475,12 +475,12 @@ private predicate nodeCand1Store(Content c, Node node, boolean toReturn, Configu
475
475
}
476
476
477
477
/**
478
- * Holds if `f ` is the target of both a read and a store in the flow covered
478
+ * Holds if `c ` is the target of both a read and a store in the flow covered
479
479
* by `nodeCand1`.
480
480
*/
481
- private predicate nodeCand1IsReadAndStored ( Content f , Configuration conf ) {
482
- nodeCand1IsRead ( f , conf ) and
483
- nodeCand1Store ( f , _, _, conf )
481
+ private predicate nodeCand1IsReadAndStored ( Content c , Configuration conf ) {
482
+ nodeCand1IsRead ( c , conf ) and
483
+ nodeCand1Store ( c , _, _, conf )
484
484
}
485
485
486
486
pragma [ nomagic]
@@ -581,10 +581,10 @@ private predicate store(Node n1, Content c, Node n2, Configuration config) {
581
581
}
582
582
583
583
pragma [ nomagic]
584
- private predicate read ( Node n1 , Content f , Node n2 , Configuration config ) {
585
- nodeCand1IsReadAndStored ( f , config ) and
584
+ private predicate read ( Node n1 , Content c , Node n2 , Configuration config ) {
585
+ nodeCand1IsReadAndStored ( c , config ) and
586
586
nodeCand1 ( n2 , unbind ( config ) ) and
587
- read ( n1 , f , n2 )
587
+ read ( n1 , c , n2 )
588
588
}
589
589
590
590
pragma [ noinline]
@@ -756,16 +756,16 @@ private predicate nodeCandFwd2(
756
756
)
757
757
or
758
758
// store
759
- exists ( Node mid , Content f |
759
+ exists ( Node mid |
760
760
nodeCandFwd2 ( mid , fromArg , argStored , _, config ) and
761
- store ( mid , f , node , config ) and
761
+ store ( mid , _ , node , config ) and
762
762
stored = true
763
763
)
764
764
or
765
765
// read
766
- exists ( Content f |
767
- nodeCandFwd2Read ( f , node , fromArg , argStored , config ) and
768
- nodeCandFwd2IsStored ( f , stored , config )
766
+ exists ( Content c |
767
+ nodeCandFwd2Read ( c , node , fromArg , argStored , config ) and
768
+ nodeCandFwd2IsStored ( c , stored , config )
769
769
)
770
770
or
771
771
// flow into a callable
@@ -789,25 +789,25 @@ private predicate nodeCandFwd2(
789
789
}
790
790
791
791
/**
792
- * Holds if `f ` is the target of a store in the flow covered by `nodeCandFwd2`.
792
+ * Holds if `c ` is the target of a store in the flow covered by `nodeCandFwd2`.
793
793
*/
794
794
pragma [ noinline]
795
- private predicate nodeCandFwd2IsStored ( Content f , boolean stored , Configuration config ) {
795
+ private predicate nodeCandFwd2IsStored ( Content c , boolean stored , Configuration config ) {
796
796
exists ( Node mid , Node node |
797
797
useFieldFlow ( config ) and
798
798
nodeCand1 ( node , unbind ( config ) ) and
799
799
nodeCandFwd2 ( mid , _, _, stored , config ) and
800
- store ( mid , f , node , config )
800
+ store ( mid , c , node , config )
801
801
)
802
802
}
803
803
804
804
pragma [ nomagic]
805
805
private predicate nodeCandFwd2Read (
806
- Content f , Node node , boolean fromArg , BooleanOption argStored , Configuration config
806
+ Content c , Node node , boolean fromArg , BooleanOption argStored , Configuration config
807
807
) {
808
808
exists ( Node mid |
809
809
nodeCandFwd2 ( mid , fromArg , argStored , true , config ) and
810
- read ( mid , f , node , config )
810
+ read ( mid , c , node , config )
811
811
)
812
812
}
813
813
@@ -904,15 +904,15 @@ private predicate nodeCand2(
904
904
)
905
905
or
906
906
// store
907
- exists ( Content f |
908
- nodeCand2Store ( f , node , toReturn , returnRead , read , config ) and
909
- nodeCand2IsRead ( f , read , config )
907
+ exists ( Content c |
908
+ nodeCand2Store ( c , node , toReturn , returnRead , read , config ) and
909
+ nodeCand2IsRead ( c , read , config )
910
910
)
911
911
or
912
912
// read
913
- exists ( Node mid , Content f , boolean read0 |
914
- read ( node , f , mid , config ) and
915
- nodeCandFwd2IsStored ( f , unbindBool ( read0 ) , unbind ( config ) ) and
913
+ exists ( Node mid , Content c , boolean read0 |
914
+ read ( node , c , mid , config ) and
915
+ nodeCandFwd2IsStored ( c , unbindBool ( read0 ) , unbind ( config ) ) and
916
916
nodeCand2 ( mid , toReturn , returnRead , read0 , config ) and
917
917
read = true
918
918
)
@@ -938,51 +938,51 @@ private predicate nodeCand2(
938
938
}
939
939
940
940
/**
941
- * Holds if `f ` is the target of a read in the flow covered by `nodeCand2`.
941
+ * Holds if `c ` is the target of a read in the flow covered by `nodeCand2`.
942
942
*/
943
943
pragma [ noinline]
944
- private predicate nodeCand2IsRead ( Content f , boolean read , Configuration config ) {
944
+ private predicate nodeCand2IsRead ( Content c , boolean read , Configuration config ) {
945
945
exists ( Node mid , Node node |
946
946
useFieldFlow ( config ) and
947
947
nodeCandFwd2 ( node , _, _, true , unbind ( config ) ) and
948
- read ( node , f , mid , config ) and
949
- nodeCandFwd2IsStored ( f , unbindBool ( read ) , unbind ( config ) ) and
948
+ read ( node , c , mid , config ) and
949
+ nodeCandFwd2IsStored ( c , unbindBool ( read ) , unbind ( config ) ) and
950
950
nodeCand2 ( mid , _, _, read , config )
951
951
)
952
952
}
953
953
954
954
pragma [ nomagic]
955
955
private predicate nodeCand2Store (
956
- Content f , Node node , boolean toReturn , BooleanOption returnRead , boolean stored ,
956
+ Content c , Node node , boolean toReturn , BooleanOption returnRead , boolean stored ,
957
957
Configuration config
958
958
) {
959
959
exists ( Node mid |
960
- store ( node , f , mid , config ) and
960
+ store ( node , c , mid , config ) and
961
961
nodeCand2 ( mid , toReturn , returnRead , true , config ) and
962
962
nodeCandFwd2 ( node , _, _, stored , unbind ( config ) )
963
963
)
964
964
}
965
965
966
966
/**
967
- * Holds if `f ` is the target of a store in the flow covered by `nodeCand2`.
967
+ * Holds if `c ` is the target of a store in the flow covered by `nodeCand2`.
968
968
*/
969
969
pragma [ nomagic]
970
- private predicate nodeCand2IsStored ( Content f , boolean stored , Configuration conf ) {
970
+ private predicate nodeCand2IsStored ( Content c , boolean stored , Configuration conf ) {
971
971
exists ( Node node |
972
- nodeCand2Store ( f , node , _, _, stored , conf ) and
972
+ nodeCand2Store ( c , node , _, _, stored , conf ) and
973
973
nodeCand2 ( node , _, _, stored , conf )
974
974
)
975
975
}
976
976
977
977
/**
978
- * Holds if `f ` is the target of both a store and a read in the path graph
978
+ * Holds if `c ` is the target of both a store and a read in the path graph
979
979
* covered by `nodeCand2`.
980
980
*/
981
981
pragma [ noinline]
982
- private predicate nodeCand2IsReadAndStored ( Content f , Configuration conf ) {
982
+ private predicate nodeCand2IsReadAndStored ( Content c , Configuration conf ) {
983
983
exists ( boolean apNonEmpty |
984
- nodeCand2IsStored ( f , apNonEmpty , conf ) and
985
- nodeCand2IsRead ( f , apNonEmpty , conf )
984
+ nodeCand2IsStored ( c , apNonEmpty , conf ) and
985
+ nodeCand2IsRead ( c , apNonEmpty , conf )
986
986
)
987
987
}
988
988
@@ -1162,11 +1162,11 @@ private module LocalFlowBigStep {
1162
1162
private import LocalFlowBigStep
1163
1163
1164
1164
pragma [ nomagic]
1165
- private predicate readCand2 ( Node node1 , Content f , Node node2 , Configuration config ) {
1166
- read ( node1 , f , node2 , config ) and
1165
+ private predicate readCand2 ( Node node1 , Content c , Node node2 , Configuration config ) {
1166
+ read ( node1 , c , node2 , config ) and
1167
1167
nodeCand2 ( node1 , _, _, true , unbind ( config ) ) and
1168
1168
nodeCand2 ( node2 , config ) and
1169
- nodeCand2IsReadAndStored ( f , unbind ( config ) )
1169
+ nodeCand2IsReadAndStored ( c , unbind ( config ) )
1170
1170
}
1171
1171
1172
1172
pragma [ nomagic]
0 commit comments