@@ -278,10 +278,9 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
278278 )
279279 or
280280 // read
281- exists ( Node mid , Content f |
282- nodeCandFwd1 ( mid , true , config ) and
283- read ( mid , f , node ) and
284- storeCandFwd1 ( f , unbind ( config ) ) and
281+ exists ( Content f |
282+ nodeCandFwd1Read ( f , node , config ) and
283+ storeCandFwd1 ( f , config ) and
285284 ( stored = false or stored = true ) and
286285 not inBarrier ( node , config )
287286 )
@@ -308,9 +307,18 @@ private predicate nodeCandFwd1(Node node, boolean stored, Configuration config)
308307 )
309308}
310309
310+ pragma [ nomagic]
311+ private predicate nodeCandFwd1Read ( Content f , Node node , Configuration config ) {
312+ exists ( Node mid |
313+ nodeCandFwd1 ( mid , true , config ) and
314+ read ( mid , f , node )
315+ )
316+ }
317+
311318/**
312319 * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd1`.
313320 */
321+ pragma [ noinline]
314322private predicate storeCandFwd1 ( Content f , Configuration config ) {
315323 exists ( Node mid , Node node |
316324 not fullBarrier ( node , config ) and
@@ -358,10 +366,9 @@ private predicate nodeCand1(Node node, boolean stored, Configuration config) {
358366 )
359367 or
360368 // store
361- exists ( Node mid , Content f |
362- store ( node , f , mid ) and
363- readCand1 ( f , unbind ( config ) ) and
364- nodeCand1 ( mid , true , config ) and
369+ exists ( Content f |
370+ nodeCand1Store ( f , node , config ) and
371+ readCand1 ( f , config ) and
365372 ( stored = false or stored = true )
366373 )
367374 or
@@ -398,6 +405,7 @@ private predicate nodeCand1(Node node, boolean stored, Configuration config) {
398405/**
399406 * Holds if `f` is the target of a read in the flow covered by `nodeCand1`.
400407 */
408+ pragma [ noinline]
401409private predicate readCand1 ( Content f , Configuration config ) {
402410 exists ( Node mid , Node node |
403411 useFieldFlow ( config ) and
@@ -408,6 +416,15 @@ private predicate readCand1(Content f, Configuration config) {
408416 )
409417}
410418
419+ pragma [ nomagic]
420+ private predicate nodeCand1Store ( Content f , Node node , Configuration config ) {
421+ exists ( Node mid |
422+ nodeCand1 ( mid , true , config ) and
423+ storeCandFwd1 ( f , unbind ( config ) ) and
424+ store ( node , f , mid )
425+ )
426+ }
427+
411428private predicate throughFlowNodeCand ( Node node , Configuration config ) {
412429 nodeCand1 ( node , false , config ) and
413430 not fullBarrier ( node , config ) and
@@ -669,10 +686,9 @@ private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Confi
669686 )
670687 or
671688 // read
672- exists ( Node mid , Content f |
673- nodeCandFwd2 ( mid , fromArg , true , config ) and
674- read ( mid , f , node ) and
675- storeCandFwd2 ( f , unbind ( config ) ) and
689+ exists ( Content f |
690+ nodeCandFwd2Read ( f , node , fromArg , config ) and
691+ storeCandFwd2 ( f , config ) and
676692 ( stored = false or stored = true )
677693 )
678694 or
@@ -695,6 +711,7 @@ private predicate nodeCandFwd2(Node node, boolean fromArg, boolean stored, Confi
695711/**
696712 * Holds if `f` is the target of a store in the flow covered by `nodeCandFwd2`.
697713 */
714+ pragma [ noinline]
698715private predicate storeCandFwd2 ( Content f , Configuration config ) {
699716 exists ( Node mid , Node node |
700717 useFieldFlow ( config ) and
@@ -705,6 +722,15 @@ private predicate storeCandFwd2(Content f, Configuration config) {
705722 )
706723}
707724
725+ pragma [ nomagic]
726+ private predicate nodeCandFwd2Read ( Content f , Node node , boolean fromArg , Configuration config ) {
727+ exists ( Node mid |
728+ nodeCandFwd2 ( mid , fromArg , true , config ) and
729+ read ( mid , f , node ) and
730+ readCand1 ( f , unbind ( config ) )
731+ )
732+ }
733+
708734/**
709735 * Holds if `node` is part of a path from a source to a sink in the given
710736 * configuration taking simple call contexts into consideration.
@@ -742,10 +768,9 @@ private predicate nodeCand2(Node node, boolean toReturn, boolean stored, Configu
742768 )
743769 or
744770 // store
745- exists ( Node mid , Content f |
746- store ( node , f , mid ) and
747- readCand2 ( f , unbind ( config ) ) and
748- nodeCand2 ( mid , toReturn , true , config ) and
771+ exists ( Content f |
772+ nodeCand2Store ( f , node , toReturn , config ) and
773+ readCand2 ( f , config ) and
749774 ( stored = false or stored = true )
750775 )
751776 or
@@ -776,6 +801,7 @@ private predicate nodeCand2(Node node, boolean toReturn, boolean stored, Configu
776801/**
777802 * Holds if `f` is the target of a read in the flow covered by `nodeCand2`.
778803 */
804+ pragma [ noinline]
779805private predicate readCand2 ( Content f , Configuration config ) {
780806 exists ( Node mid , Node node |
781807 useFieldFlow ( config ) and
@@ -786,25 +812,30 @@ private predicate readCand2(Content f, Configuration config) {
786812 )
787813}
788814
815+ pragma [ noinline]
816+ private predicate nodeCand2Store ( Content f , Node node , boolean toReturn , Configuration config ) {
817+ exists ( Node mid |
818+ store ( node , f , mid ) and
819+ nodeCand2 ( mid , toReturn , true , config )
820+ )
821+ }
822+
789823pragma [ nomagic]
790824private predicate storeCand ( Content f , Configuration conf ) {
791- exists ( Node n1 , Node n2 |
792- store ( n1 , f , n2 ) and
793- nodeCand2 ( n1 , _, _, conf ) and
794- nodeCand2 ( n2 , _, _, unbind ( conf ) )
825+ exists ( Node node |
826+ nodeCand2Store ( f , node , _, conf ) and
827+ nodeCand2 ( node , _, _, conf )
795828 )
796829}
797830
798- private predicate readCand ( Content f , Configuration conf ) { readCand2 ( f , conf ) }
799-
800831/**
801832 * Holds if `f` is the target of both a store and a read in the path graph
802833 * covered by `nodeCand2`.
803834 */
804835pragma [ noinline]
805836private predicate readStoreCand ( Content f , Configuration conf ) {
806837 storeCand ( f , conf ) and
807- readCand ( f , conf )
838+ readCand2 ( f , conf )
808839}
809840
810841private predicate nodeCand ( Node node , Configuration config ) { nodeCand2 ( node , _, _, config ) }
@@ -1030,15 +1061,13 @@ private predicate flowCandFwd0(Node node, boolean fromArg, AccessPathFront apf,
10301061 apf .headUsesContent ( f )
10311062 )
10321063 or
1033- exists ( Node mid , Content f , AccessPathFront apf0 |
1034- flowCandFwd ( mid , fromArg , apf0 , config ) and
1035- read ( mid , f , node ) and
1036- nodeCand ( node , config ) and
1037- apf0 .headUsesContent ( f ) and
1038- consCandFwd ( f , apf , unbind ( config ) )
1064+ exists ( Content f |
1065+ flowCandFwdRead ( f , node , fromArg , config ) and
1066+ consCandFwd ( f , apf , config )
10391067 )
10401068}
10411069
1070+ pragma [ noinline]
10421071private predicate consCandFwd ( Content f , AccessPathFront apf , Configuration config ) {
10431072 exists ( Node mid , Node n |
10441073 flowCandFwd ( mid , _, apf , config ) and
@@ -1049,6 +1078,16 @@ private predicate consCandFwd(Content f, AccessPathFront apf, Configuration conf
10491078 )
10501079}
10511080
1081+ pragma [ nomagic]
1082+ private predicate flowCandFwdRead ( Content f , Node node , boolean fromArg , Configuration config ) {
1083+ exists ( Node mid , AccessPathFront apf |
1084+ flowCandFwd ( mid , fromArg , apf , config ) and
1085+ read ( mid , f , node ) and
1086+ apf .headUsesContent ( f ) and
1087+ nodeCand ( node , unbind ( config ) )
1088+ )
1089+ }
1090+
10521091/**
10531092 * Holds if data can flow from a source to `node` with the given `apf` and
10541093 * from there flow to a sink.
@@ -1139,6 +1178,7 @@ private predicate flowCandRead(
11391178 )
11401179}
11411180
1181+ pragma [ nomagic]
11421182private predicate flowCandStore (
11431183 Node node , Content f , boolean toReturn , AccessPathFront apf0 , Configuration config
11441184) {
@@ -1148,6 +1188,7 @@ private predicate flowCandStore(
11481188 )
11491189}
11501190
1191+ pragma [ noinline]
11511192private predicate consCand ( Content f , AccessPathFront apf , Configuration config ) {
11521193 consCandFwd ( f , apf , config ) and
11531194 exists ( Node n , AccessPathFront apf0 |
@@ -1672,6 +1713,7 @@ private predicate pathStep(PathNodeMid mid, Node node, CallContext cc, AccessPat
16721713 valuePathThroughCallable ( mid , node , cc ) and ap = mid .getAp ( )
16731714}
16741715
1716+ pragma [ noinline]
16751717private predicate contentReadStep ( PathNodeMid mid , Node node , AccessPath ap ) {
16761718 exists ( Content f , AccessPath ap0 |
16771719 ap0 = mid .getAp ( ) and
0 commit comments