@@ -109,7 +109,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
109109 }
110110
111111 predicate simpleLocalSmallStep ( Node node1 , Node node2 ) {
112- simpleLocalFlowStepExt ( node1 , node2 , _)
112+ simpleLocalFlowStepCached ( node1 , node2 , _)
113113 }
114114
115115 predicate levelStepNoCall ( Node n1 , LocalSourceNode n2 ) { none ( ) }
@@ -878,7 +878,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
878878
879879 Node asNode ( ) { this = TNodeNormal ( result ) }
880880
881- Node asNodeReverse ( boolean b ) { this = TNodeReverse ( result , b ) }
881+ Node asNodeReverse ( boolean allowFwdFlowOut ) { this = TNodeReverse ( result , allowFwdFlowOut ) }
882882
883883 /** Gets the corresponding Node if this is a normal node or its post-implicit read node. */
884884 Node asNodeOrImplicitRead ( ) { this = TNodeNormal ( result ) or this = TNodeImplicitRead ( result ) }
@@ -926,18 +926,18 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
926926 }
927927
928928 final class DataFlowCallEx extends MkDataFlowCallEx {
929- DataFlowCall asDataFlowCall ( boolean b ) { this = MkDataFlowCallEx ( result , b ) }
929+ DataFlowCall asDataFlowCall ( boolean allowFwdFlowOut ) {
930+ this = MkDataFlowCallEx ( result , allowFwdFlowOut )
931+ }
930932
931- // DataFlowCall asDataFlowCallReverse(boolean b) { this = TReverseDataFlowCall(result, b) }
932- // DataFlowCall projectToCall() { result = [this.asDataFlowCall(), this.asDataFlowCallReverse(_)] }
933933 DataFlowCallable getEnclosingCallable ( ) {
934934 result = this .asDataFlowCall ( _) .getEnclosingCallable ( )
935935 }
936936
937937 string toString ( ) {
938- exists ( boolean b , string s |
939- s = this .asDataFlowCall ( b ) .toString ( ) and
940- if b = true then result = s else result = s + " (no flow out to post )"
938+ exists ( boolean allowFwdFlowOut , string s |
939+ s = this .asDataFlowCall ( allowFwdFlowOut ) .toString ( ) and
940+ if allowFwdFlowOut = true then result = s else result = s + " (no fwd flow out)"
941941 )
942942 }
943943
@@ -975,9 +975,10 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
975975 ArgNodeEx ( ) {
976976 this .asNode ( ) .( ArgNode ) .argumentOf ( call_ .asDataFlowCall ( true ) , pos_ .asArgumentPosition ( ) )
977977 or
978- exists ( boolean b |
979- pragma [ only_bind_into ] ( this .asNodeReverse ( b ) ) =
980- getAnOutNode ( call_ .asDataFlowCall ( b ) , pos_ .asReturnKind ( ) .( ValueReturnKind ) .getKind ( ) )
978+ exists ( boolean allowFwdFlowOut |
979+ pragma [ only_bind_into ] ( this .asNodeReverse ( allowFwdFlowOut ) ) =
980+ getAnOutNode ( call_ .asDataFlowCall ( allowFwdFlowOut ) ,
981+ pos_ .asReturnKind ( ) .( ValueReturnKind ) .getKind ( ) )
981982 )
982983 }
983984
@@ -1054,9 +1055,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
10541055 predicate forceCachingInSameStage ( ) { any ( ) }
10551056
10561057 cached
1057- newtype TDataFlowCallEx =
1058- // NormalDataFlowCall(DataFlowCall call) or
1059- MkDataFlowCallEx ( DataFlowCall call , Boolean b )
1058+ newtype TDataFlowCallEx = MkDataFlowCallEx ( DataFlowCall call , Boolean allowFwdFlowOut )
10601059
10611060 cached
10621061 newtype TArgumentPositionEx =
@@ -1148,16 +1147,16 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
11481147
11491148 cached
11501149 OutNodeEx getAnOutNodeEx ( DataFlowCallEx call , ReturnKindExt k ) {
1151- exists ( DataFlowCall c , boolean b | c = call .asDataFlowCall ( b ) |
1150+ exists ( DataFlowCall c , boolean allowFwdFlowOut | c = call .asDataFlowCall ( allowFwdFlowOut ) |
11521151 result .asNode ( ) = getAnOutNode ( c , k .( ValueReturnKind ) .getKind ( ) )
11531152 or
11541153 exists ( ArgNode arg |
11551154 arg .argumentOf ( c , k .( ParamUpdateReturnKind ) .getAMatchingArgumentPosition ( ) )
11561155 |
1157- b = false and
1156+ allowFwdFlowOut = false and
11581157 result .asNodeReverse ( _) = arg
11591158 or
1160- b = true and
1159+ allowFwdFlowOut = true and
11611160 result .asNode ( ) .( PostUpdateNode ) .getPreUpdateNode ( ) = arg
11621161 )
11631162 )
@@ -1778,9 +1777,9 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
17781777 predicate readEx ( NodeEx node1 , ContentSet c , NodeEx node2 ) {
17791778 readSet ( pragma [ only_bind_into ] ( node1 .asNode ( ) ) , c , pragma [ only_bind_into ] ( node2 .asNode ( ) ) )
17801779 or
1781- exists ( boolean b |
1782- storeSet ( pragma [ only_bind_into ] ( node2 .asNodeReverse ( b ) ) , c ,
1783- pragma [ only_bind_into ] ( node1 .asNodeReverse ( b ) ) , _, _)
1780+ exists ( boolean allowFwdFlowOut |
1781+ storeSet ( pragma [ only_bind_into ] ( node2 .asNodeReverse ( allowFwdFlowOut ) ) , c ,
1782+ pragma [ only_bind_into ] ( node1 .asNodeReverse ( allowFwdFlowOut ) ) , _, _)
17841783 )
17851784 }
17861785
@@ -1819,49 +1818,25 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
18191818 storeSet ( pragma [ only_bind_into ] ( node1 .asNode ( ) ) , cs , pragma [ only_bind_into ] ( node2 .asNode ( ) ) ,
18201819 contentType , containerType )
18211820 or
1822- exists ( Node n1 , Node n2 , boolean b |
1823- n1 = pragma [ only_bind_into ] ( node1 .asNodeReverse ( b ) ) and
1824- n2 = pragma [ only_bind_into ] ( node2 .asNodeReverse ( b ) ) and
1821+ exists ( Node n1 , Node n2 , boolean allowFwdFlowOut |
1822+ n1 = pragma [ only_bind_into ] ( node1 .asNodeReverse ( allowFwdFlowOut ) ) and
1823+ n2 = pragma [ only_bind_into ] ( node2 .asNodeReverse ( allowFwdFlowOut ) ) and
18251824 readSet ( n2 , cs , n1 ) and
1826- contentType = getNodeDataFlowType ( node1 .asNodeReverse ( b ) ) and
1827- containerType = getNodeDataFlowType ( node2 .asNodeReverse ( b ) ) and
1828- not exists ( PostUpdateNode pn1 , PostUpdateNode pn2 |
1825+ contentType = getNodeDataFlowType ( n1 ) and
1826+ containerType = getNodeDataFlowType ( n2 ) and
1827+ not exists (
1828+ PostUpdateNode pn1 , PostUpdateNode pn2 // why?
1829+ |
18291830 n1 = pn1 .getPreUpdateNode ( ) and
18301831 n2 = pn2 .getPreUpdateNode ( )
18311832 )
18321833 )
18331834 )
18341835 }
18351836
1836- /**
1837- * Holds if data can flow from `fromNode` to `toNode` because they are the post-update
1838- * nodes of some function output and input respectively, where the output and input
1839- * are aliases. A typical example is a function returning `this`, implementing a fluent
1840- * interface.
1841- */
1842- private predicate reverseStepThroughInputOutputAlias (
1843- PostUpdateNode fromNode , PostUpdateNode toNode , string model
1844- ) {
1845- exists ( Node fromPre , Node toPre |
1846- fromPre = fromNode .getPreUpdateNode ( ) and
1847- toPre = toNode .getPreUpdateNode ( )
1848- |
1849- exists ( DataFlowCall c |
1850- // Does the language-specific simpleLocalFlowStep already model flow
1851- // from function input to output?
1852- fromPre = getAnOutNode ( c , _) and
1853- toPre .( ArgNode ) .argumentOf ( c , _) and
1854- simpleLocalFlowStep ( toPre .( ArgNode ) , fromPre , model )
1855- )
1856- or
1857- argumentValueFlowsThrough ( toPre , TReadStepTypesNone ( ) , fromPre , model )
1858- )
1859- }
1860-
18611837 cached
1862- predicate simpleLocalFlowStepExt ( Node node1 , Node node2 , string model ) {
1863- simpleLocalFlowStep ( node1 , node2 , model ) or
1864- reverseStepThroughInputOutputAlias ( node1 , node2 , model )
1838+ predicate simpleLocalFlowStepCached ( Node node1 , Node node2 , string model ) {
1839+ simpleLocalFlowStep ( node1 , node2 , model )
18651840 }
18661841
18671842 cached
@@ -2016,7 +1991,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
20161991 newtype TNodeEx =
20171992 TNodeNormal ( Node n ) or
20181993 TNodeImplicitRead ( Node n ) or
2019- TNodeReverse ( Node n , Boolean b )
1994+ TNodeReverse ( Node n , Boolean allowFwdFlowOut )
20201995
20211996 /**
20221997 * Holds if data can flow in one local step from `node1` to `node2`.
@@ -2026,13 +2001,15 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
20262001 exists ( Node n1 , Node n2 |
20272002 node1 .asNode ( ) = n1 and
20282003 node2 .asNode ( ) = n2 and
2029- simpleLocalFlowStepExt ( pragma [ only_bind_into ] ( n1 ) , pragma [ only_bind_into ] ( n2 ) , model )
2004+ simpleLocalFlowStep ( pragma [ only_bind_into ] ( n1 ) , pragma [ only_bind_into ] ( n2 ) , model )
20302005 )
20312006 or
2007+ // as soon as we take a reverse local step, forward out flow must be prohibited
2008+ // in order to prevent time travelling
20322009 exists ( Node n1 , Node n2 |
20332010 node1 .asNodeReverse ( _) = n1 and
20342011 node2 .asNodeReverse ( false ) = n2 and
2035- simpleLocalFlowStepExt ( pragma [ only_bind_into ] ( n2 ) , pragma [ only_bind_into ] ( n1 ) , model )
2012+ simpleLocalFlowStep ( pragma [ only_bind_into ] ( n2 ) , pragma [ only_bind_into ] ( n1 ) , model )
20362013 )
20372014 or
20382015 node1 .asNode ( ) .( PostUpdateNode ) .getPreUpdateNode ( ) = node2 .asNodeReverse ( true ) and
0 commit comments