@@ -119,7 +119,15 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
119119 }
120120
121121 // TODO: support setters
122- predicate storeStep ( Node n1 , Node n2 , Content f ) { storeSet ( n1 , f , n2 , _, _) }
122+ predicate storeStep ( Node n1 , Node n2 , Content f ) {
123+ storeSet ( n1 , f , n2 )
124+ or
125+ exists ( Node pre1 , Node pre2 |
126+ pre1 = n1 .( PostUpdateNode ) .getPreUpdateNode ( ) and
127+ pre2 = n2 .( PostUpdateNode ) .getPreUpdateNode ( ) and
128+ argumentValueFlowsThrough ( pre2 , TReadStepTypesSome ( _, f , _) , pre1 , _)
129+ )
130+ }
123131
124132 private predicate loadStep0 ( Node n1 , Node n2 , Content f ) {
125133 readSet ( n1 , f , n2 )
@@ -872,7 +880,6 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
872880 or
873881 exists ( Node n | this .isImplicitReadNode ( n ) | result = n .toString ( ) + " [Ext]" )
874882 or
875- // exists(boolean b | result = this.asNodeReverse(b).toString() + " [Reverse, " + b + "]")
876883 result = this .asNodeReverse ( _) .toString ( ) + " [Reverse]"
877884 }
878885
@@ -968,46 +975,41 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
968975 }
969976 }
970977
971- final class ArgNodeEx extends NodeEx {
978+ abstract class ArgNodeEx extends NodeEx {
979+ abstract predicate argumentOf ( DataFlowCallEx call , ArgumentPositionEx pos ) ;
980+
981+ DataFlowCallEx getCall ( ) { this .argumentOf ( result , _) }
982+ }
983+
984+ final class NormalArgNodeEx extends ArgNodeEx {
972985 private DataFlowCallEx call_ ;
973986 private ArgumentPositionEx pos_ ;
974987
975- ArgNodeEx ( ) {
988+ NormalArgNodeEx ( ) {
976989 this .asNode ( ) .( ArgNode ) .argumentOf ( call_ .asDataFlowCall ( true ) , pos_ .asArgumentPosition ( ) )
977- or
978- exists ( boolean allowFwdFlowOut |
979- pragma [ only_bind_into ] ( this .asNodeReverse ( allowFwdFlowOut ) ) =
980- getAnOutNode ( call_ .asDataFlowCall ( allowFwdFlowOut ) ,
981- pos_ .asReturnKind ( ) .( ValueReturnKind ) .getKind ( ) )
982- )
983990 }
984991
985- predicate argumentOf ( DataFlowCallEx call , ArgumentPositionEx pos ) {
992+ override predicate argumentOf ( DataFlowCallEx call , ArgumentPositionEx pos ) {
986993 call = call_ and
987994 pos = pos_
988995 }
996+ }
989997
990- DataFlowCallEx getCall ( ) { this .argumentOf ( result , _) }
998+ abstract class ParamNodeEx extends NodeEx {
999+ abstract predicate isParameterOf ( DataFlowCallable c , ParameterPositionEx pos ) ;
1000+
1001+ ParameterPositionEx getPosition ( ) { this .isParameterOf ( _, result ) }
9911002 }
9921003
993- final class ParamNodeEx extends NodeEx {
1004+ final class NormalParamNodeEx extends ParamNodeEx {
9941005 private DataFlowCallable c_ ;
9951006 private ParameterPositionEx pos_ ;
9961007
997- ParamNodeEx ( ) {
998- this .asNode ( ) .( ParamNode ) .isParameterOf ( c_ , pos_ .asParameterPosition ( ) )
999- or
1000- // todo: returnkindext?
1001- exists ( ReturnPosition pos |
1002- pos = getValueReturnPosition ( this .asNodeReverse ( true ) ) and
1003- c_ = pos .getCallable ( ) and
1004- pos_ .asReturnKind ( ) = pos .getKind ( )
1005- )
1006- }
1008+ NormalParamNodeEx ( ) { this .asNode ( ) .( ParamNode ) .isParameterOf ( c_ , pos_ .asParameterPosition ( ) ) }
10071009
1008- predicate isParameterOf ( DataFlowCallable c , ParameterPositionEx pos ) { c = c_ and pos = pos_ }
1009-
1010- ParameterPositionEx getPosition ( ) { this . isParameterOf ( _ , result ) }
1010+ override predicate isParameterOf ( DataFlowCallable c , ParameterPositionEx pos ) {
1011+ c = c_ and pos = pos_
1012+ }
10111013 }
10121014
10131015 /**
@@ -1017,11 +1019,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
10171019 final class RetNodeEx extends NodeEx {
10181020 private ReturnPosition pos ;
10191021
1020- RetNodeEx ( ) {
1021- pos = getReturnPositionEx ( this ) //and
1022- // this.toString() = "this [Reverse]" and
1023- // this.getLocation().getStartLine() = 71
1024- }
1022+ RetNodeEx ( ) { pos = getReturnPositionEx ( this ) }
10251023
10261024 ReturnPosition getReturnPosition ( ) { result = pos }
10271025
@@ -1044,6 +1042,104 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
10441042 not exists ( getSecondLevelScope ( n ) )
10451043 }
10461044
1045+ private module ReverseFlow {
1046+ /**
1047+ * Holds if the local step from `arg` to `out` actually models a flow-through
1048+ * step.
1049+ */
1050+ pragma [ nomagic]
1051+ private predicate isFlowThroughLocalStep ( ArgNode arg , OutNode out , string model ) {
1052+ exists ( DataFlowCall c |
1053+ out = getAnOutNode ( c , _) and
1054+ arg .argumentOf ( c , _) and
1055+ simpleLocalFlowStep ( arg , out , model )
1056+ )
1057+ }
1058+
1059+ predicate localFlowStep ( NodeEx node1 , NodeEx node2 , string model ) {
1060+ // as soon as we take a reverse local step, forward out flow must be prohibited
1061+ // in order to prevent time travelling
1062+ exists ( Node n1 , Node n2 |
1063+ node1 .asNodeReverse ( _) = n1 and
1064+ node2 .asNodeReverse ( false ) = n2 and
1065+ simpleLocalFlowStep ( pragma [ only_bind_into ] ( n2 ) , pragma [ only_bind_into ] ( n1 ) , model ) and
1066+ validParameterAliasStep ( n2 , n1 ) and
1067+ not isFlowThroughLocalStep ( n2 , n1 , model )
1068+ )
1069+ or
1070+ exists ( Node n1 , Node n2 , boolean allowFwdFlowOut |
1071+ node1 .asNodeReverse ( pragma [ only_bind_into ] ( allowFwdFlowOut ) ) = n1 and
1072+ isFlowThroughLocalStep ( n2 , n1 , model ) and
1073+ validParameterAliasStep ( n2 , n1 )
1074+ |
1075+ node2 .asNodeReverse ( pragma [ only_bind_into ] ( allowFwdFlowOut ) ) = n2
1076+ or
1077+ allowFwdFlowOut = true and
1078+ node2 .asNode ( ) .( PostUpdateNode ) .getPreUpdateNode ( ) = n2
1079+ )
1080+ or
1081+ node1 .asNode ( ) .( PostUpdateNode ) .getPreUpdateNode ( ) = node2 .asNodeReverse ( true ) and
1082+ model = ""
1083+ }
1084+
1085+ predicate storeStep ( NodeEx node1 , Content c , NodeEx node2 ) {
1086+ exists ( ContentSet cs | c = cs .getAStoreContent ( ) |
1087+ exists ( Node n1 , Node n2 , boolean allowFwdFlowOut |
1088+ n1 = pragma [ only_bind_into ] ( node1 .asNodeReverse ( allowFwdFlowOut ) ) and
1089+ n2 = pragma [ only_bind_into ] ( node2 .asNodeReverse ( allowFwdFlowOut ) ) and
1090+ Lang:: readStep ( n2 , cs , n1 ) and
1091+ // avoid overlap with `storeSet`
1092+ not exists ( PostUpdateNode pn1 , PostUpdateNode pn2 |
1093+ n1 = pn1 .getPreUpdateNode ( ) and
1094+ n2 = pn2 .getPreUpdateNode ( )
1095+ )
1096+ )
1097+ )
1098+ }
1099+
1100+ predicate readStep ( NodeEx node1 , ContentSet c , NodeEx node2 ) {
1101+ exists ( boolean allowFwdFlowOut |
1102+ Lang:: storeStep ( pragma [ only_bind_into ] ( node2 .asNodeReverse ( allowFwdFlowOut ) ) , c ,
1103+ pragma [ only_bind_into ] ( node1 .asNodeReverse ( allowFwdFlowOut ) ) )
1104+ )
1105+ }
1106+
1107+ final class ReverseArgNodeEx extends ArgNodeEx {
1108+ private DataFlowCallEx call_ ;
1109+ private ArgumentPositionEx pos_ ;
1110+
1111+ ReverseArgNodeEx ( ) {
1112+ exists ( boolean allowFwdFlowOut |
1113+ pragma [ only_bind_into ] ( this .asNodeReverse ( allowFwdFlowOut ) ) =
1114+ getAnOutNode ( call_ .asDataFlowCall ( allowFwdFlowOut ) ,
1115+ pos_ .asReturnKind ( ) .( ValueReturnKind ) .getKind ( ) )
1116+ )
1117+ }
1118+
1119+ override predicate argumentOf ( DataFlowCallEx call , ArgumentPositionEx pos ) {
1120+ call = call_ and
1121+ pos = pos_
1122+ }
1123+ }
1124+
1125+ final class ReverseParamNodeEx extends ParamNodeEx {
1126+ private DataFlowCallable c_ ;
1127+ private ParameterPositionEx pos_ ;
1128+
1129+ ReverseParamNodeEx ( ) {
1130+ exists ( ReturnPosition pos |
1131+ pos = getValueReturnPosition ( this .asNodeReverse ( true ) ) and
1132+ c_ = pos .getCallable ( ) and
1133+ pos_ .asReturnKind ( ) = pos .getKind ( )
1134+ )
1135+ }
1136+
1137+ override predicate isParameterOf ( DataFlowCallable c , ParameterPositionEx pos ) {
1138+ c = c_ and pos = pos_
1139+ }
1140+ }
1141+ }
1142+
10471143 cached
10481144 private module Cached {
10491145 /**
@@ -1776,29 +1872,17 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
17761872 predicate readEx ( NodeEx node1 , ContentSet c , NodeEx node2 ) {
17771873 readSet ( pragma [ only_bind_into ] ( node1 .asNode ( ) ) , c , pragma [ only_bind_into ] ( node2 .asNode ( ) ) )
17781874 or
1779- exists ( boolean allowFwdFlowOut |
1780- storeSet ( pragma [ only_bind_into ] ( node2 .asNodeReverse ( allowFwdFlowOut ) ) , c ,
1781- pragma [ only_bind_into ] ( node1 .asNodeReverse ( allowFwdFlowOut ) ) , _, _)
1782- )
1875+ ReverseFlow:: readStep ( node1 , c , node2 )
17831876 }
17841877
17851878 cached
1786- predicate storeSet (
1787- Node node1 , ContentSet c , Node node2 , DataFlowType contentType , DataFlowType containerType
1788- ) {
1789- storeStep ( node1 , c , node2 ) and
1790- contentType = getNodeDataFlowType ( node1 ) and
1791- containerType = getNodeDataFlowType ( node2 )
1879+ predicate storeSet ( Node node1 , ContentSet c , Node node2 ) {
1880+ storeStep ( node1 , c , node2 )
17921881 or
17931882 exists ( Node n1 , Node n2 |
17941883 n1 = node1 .( PostUpdateNode ) .getPreUpdateNode ( ) and
1795- n2 = node2 .( PostUpdateNode ) .getPreUpdateNode ( )
1796- |
1797- // argumentValueFlowsThrough(n2, TReadStepTypesSome(containerType, c, contentType), n1, _) // TODO
1798- // or
1799- readSet ( n2 , c , n1 ) and
1800- contentType = getNodeDataFlowType ( n1 ) and
1801- containerType = getNodeDataFlowType ( n2 )
1884+ n2 = node2 .( PostUpdateNode ) .getPreUpdateNode ( ) and
1885+ readSet ( n2 , c , n1 )
18021886 )
18031887 }
18041888
@@ -1813,23 +1897,14 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
18131897 predicate storeEx (
18141898 NodeEx node1 , Content c , NodeEx node2 , DataFlowType contentType , DataFlowType containerType
18151899 ) {
1816- exists ( ContentSet cs | c = cs .getAStoreContent ( ) |
1817- storeSet ( pragma [ only_bind_into ] ( node1 .asNode ( ) ) , cs , pragma [ only_bind_into ] ( node2 .asNode ( ) ) ,
1818- contentType , containerType )
1900+ exists ( ContentSet cs |
1901+ c = cs .getAStoreContent ( ) and
1902+ contentType = node1 .getDataFlowType ( ) and
1903+ containerType = node2 .getDataFlowType ( )
1904+ |
1905+ storeSet ( pragma [ only_bind_into ] ( node1 .asNode ( ) ) , cs , pragma [ only_bind_into ] ( node2 .asNode ( ) ) )
18191906 or
1820- exists ( Node n1 , Node n2 , boolean allowFwdFlowOut |
1821- n1 = pragma [ only_bind_into ] ( node1 .asNodeReverse ( allowFwdFlowOut ) ) and
1822- n2 = pragma [ only_bind_into ] ( node2 .asNodeReverse ( allowFwdFlowOut ) ) and
1823- readSet ( n2 , cs , n1 ) and
1824- contentType = getNodeDataFlowType ( n1 ) and
1825- containerType = getNodeDataFlowType ( n2 ) and
1826- not exists (
1827- PostUpdateNode pn1 , PostUpdateNode pn2 // why?
1828- |
1829- n1 = pn1 .getPreUpdateNode ( ) and
1830- n2 = pn2 .getPreUpdateNode ( )
1831- )
1832- )
1907+ ReverseFlow:: storeStep ( node1 , c , node2 )
18331908 )
18341909 }
18351910
@@ -1992,19 +2067,6 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
19922067 TNodeImplicitRead ( Node n ) or // will be restricted to nodes with actual implicit reads in `DataFlowImpl.qll`
19932068 TNodeReverse ( Node n , Boolean allowFwdFlowOut )
19942069
1995- /**
1996- * Holds if the local step from `arg` to `out` actually models a flow-through
1997- * step.
1998- */
1999- pragma [ nomagic]
2000- private predicate isFlowThroughLocalStep ( ArgNode arg , OutNode out , string model ) {
2001- exists ( DataFlowCall c |
2002- out = getAnOutNode ( c , _) and
2003- arg .argumentOf ( c , _) and
2004- simpleLocalFlowStep ( arg , out , model )
2005- )
2006- }
2007-
20082070 /**
20092071 * Holds if data can flow in one local step from `node1` to `node2`.
20102072 */
@@ -2016,29 +2078,7 @@ module MakeImplCommon<LocationSig Location, InputSig<Location> Lang> {
20162078 simpleLocalFlowStep ( pragma [ only_bind_into ] ( n1 ) , pragma [ only_bind_into ] ( n2 ) , model )
20172079 )
20182080 or
2019- // as soon as we take a reverse local step, forward out flow must be prohibited
2020- // in order to prevent time travelling
2021- exists ( Node n1 , Node n2 |
2022- node1 .asNodeReverse ( _) = n1 and
2023- node2 .asNodeReverse ( false ) = n2 and
2024- simpleLocalFlowStep ( pragma [ only_bind_into ] ( n2 ) , pragma [ only_bind_into ] ( n1 ) , model ) and
2025- validParameterAliasStep ( n2 , n1 ) and
2026- not isFlowThroughLocalStep ( n2 , n1 , model )
2027- )
2028- or
2029- exists ( Node n1 , Node n2 , boolean allowFwdFlowOut |
2030- node1 .asNodeReverse ( pragma [ only_bind_into ] ( allowFwdFlowOut ) ) = n1 and
2031- isFlowThroughLocalStep ( n2 , n1 , model ) and
2032- validParameterAliasStep ( n2 , n1 )
2033- |
2034- node2 .asNodeReverse ( pragma [ only_bind_into ] ( allowFwdFlowOut ) ) = n2
2035- or
2036- allowFwdFlowOut = true and
2037- node2 .asNode ( ) .( PostUpdateNode ) .getPreUpdateNode ( ) = n2
2038- )
2039- or
2040- node1 .asNode ( ) .( PostUpdateNode ) .getPreUpdateNode ( ) = node2 .asNodeReverse ( true ) and
2041- model = ""
2081+ ReverseFlow:: localFlowStep ( node1 , node2 , model )
20422082 }
20432083
20442084 cached
0 commit comments