@@ -22,20 +22,38 @@ module DataFlowInput implements InputSig<Location> {
2222 //
2323 // Parameter, argument, return, and out nodes and their positions/kinds
2424 //
25+ private predicate isReturnNode ( Node n , ReturnKind kind ) {
26+ // TODO: Handle short-hand returns such as `func foo() -> Int { 5 }`
27+ n .asExpr ( ) = any ( ReturnExpr r ) .getValue ( ) and kind .isStandardReturnValue ( )
28+ or
29+ FlowSummaryOutput:: summaryReturnNode ( getSummaryNode ( n ) , kind )
30+ }
31+
2532 class ReturnNode extends Node {
26- ReturnNode ( ) {
27- // TODO: Handle short-hand returns such as `func foo() -> Int { 5 }`
28- this .asExpr ( ) = any ( ReturnExpr r ) .getValue ( )
29- }
33+ ReturnNode ( ) { isReturnNode ( this , _) }
3034
31- ReturnKind getKind ( ) { exists ( result ) }
35+ ReturnKind getKind ( ) { isReturnNode ( this , result ) }
36+ }
37+
38+ private predicate isOutNode ( Node n , DataFlowCall call , ReturnKind kind ) {
39+ n .asExpr ( ) = call .asExplicitCall ( ) and kind .isStandardReturnValue ( )
40+ or
41+ exists ( FlowSummaryOutput:: SummaryNode callee |
42+ FlowSummaryOutput:: summaryOutNode ( callee , getSummaryNode ( n ) , kind ) and
43+ call .isSummaryCall ( _, callee )
44+ )
3245 }
3346
3447 class OutNode extends Node {
35- OutNode ( ) { this . asExpr ( ) instanceof CallExpr }
48+ OutNode ( ) { isOutNode ( this , _ , _ ) }
3649 }
3750
38- class ReturnKind = Unit ;
51+ OutNode getAnOutNode ( DataFlowCall call , ReturnKind kind ) { isOutNode ( result , call , kind ) }
52+
53+ class ReturnKind extends Unit {
54+ /** Holds if this is the standard return value */
55+ predicate isStandardReturnValue ( ) { any ( ) }
56+ }
3957
4058 import ParameterPositions
4159 //
@@ -58,6 +76,9 @@ module DataFlowInput implements InputSig<Location> {
5876 )
5977 or
6078 p .( BuilderNode ) .isImplicitParameter ( c , pos )
79+ or
80+ FlowSummaryOutput:: summaryParameterNode ( getSummaryNode ( p ) , pos ) and
81+ c = p .getEnclosingCallableEx ( )
6182 }
6283
6384 class ParameterNode extends Node {
@@ -80,6 +101,11 @@ module DataFlowInput implements InputSig<Location> {
80101 )
81102 or
82103 n .( BuilderNode ) .isImplicitArgument ( call , pos , false )
104+ or
105+ exists ( FlowSummaryOutput:: SummaryNode callee |
106+ FlowSummaryOutput:: summaryArgumentNode ( callee , getSummaryNode ( n ) , pos ) and
107+ call .isSummaryCall ( _, callee )
108+ )
83109 }
84110
85111 class ArgumentNode extends Node {
@@ -91,10 +117,6 @@ module DataFlowInput implements InputSig<Location> {
91117 isArgumentNodeImpl ( n , call , pos )
92118 }
93119
94- OutNode getAnOutNode ( DataFlowCall call , ReturnKind kind ) {
95- result .asExpr ( ) = call .asExplicitCall ( ) and exists ( kind )
96- }
97-
98120 //
99121 // Post-update nodes
100122 //
@@ -129,6 +151,8 @@ module DataFlowInput implements InputSig<Location> {
129151 private Step valueStepEx ( ) {
130152 result .value ( )
131153 or
154+ result .valueMustFlow ( )
155+ or
132156 exists ( ContentSet contents | bypassContentSet ( contents ) |
133157 result .read ( contents )
134158 or
@@ -142,15 +166,29 @@ module DataFlowInput implements InputSig<Location> {
142166 localSsaStep ( node1 , node2 , _) and model = ""
143167 or
144168 captureSsaLocalFlowStep ( node1 , node2 ) and model = ""
169+ or
170+ FlowSummaryOutput:: summaryLocalStep ( node1 , node2 , true , model )
171+ or
172+ model = "" and
173+ exists ( ContentSet contents | bypassContentSet ( contents ) |
174+ FlowSummaryOutput:: summaryReadStep ( getSummaryNode ( node1 ) , contents , getSummaryNode ( node2 ) )
175+ or
176+ FlowSummaryOutput:: summaryStoreStep ( getSummaryNode ( node1 ) , contents , getSummaryNode ( node2 ) )
177+ )
145178 }
146179
147- predicate jumpStep ( Node node1 , Node node2 ) { step ( node1 , any ( Step s | s .jump ( ) ) , node2 ) }
180+ predicate jumpStep ( Node node1 , Node node2 ) {
181+ step ( node1 , any ( Step s | s .jump ( ) ) , node2 ) or
182+ FlowSummaryOutput:: summaryJumpStep ( node1 , node2 )
183+ }
148184
149185 predicate readStep ( Node node1 , ContentSet c , Node node2 ) {
150186 (
151187 step ( node1 , any ( Step s | s .read ( c ) ) , node2 )
152188 or
153189 captureSsaReadStep ( node1 , c , node2 )
190+ or
191+ FlowSummaryOutput:: summaryReadStep ( getSummaryNode ( node1 ) , c , getSummaryNode ( node2 ) )
154192 ) and
155193 not bypassContentSet ( c )
156194 }
@@ -160,15 +198,29 @@ module DataFlowInput implements InputSig<Location> {
160198 step ( node1 , any ( Step s | s .store ( c ) ) , node2 )
161199 or
162200 captureSsaStoreStep ( node1 , c , node2 )
201+ or
202+ FlowSummaryOutput:: summaryStoreStep ( getSummaryNode ( node1 ) , c , getSummaryNode ( node2 ) )
163203 ) and
164204 not bypassContentSet ( c )
165205 }
166206
167- predicate clearsContent ( Node n , ContentSet c ) { captureSsaClearsContent ( n , c ) } // TODO
207+ predicate clearsContent ( Node n , ContentSet c ) {
208+ captureSsaClearsContent ( n , c )
209+ or
210+ FlowSummaryOutput:: summaryClearsContent ( getSummaryNode ( n ) , c ) and
211+ not bypassContentSet ( c )
212+ }
168213
169- predicate expectsContent ( Node n , ContentSet c ) { none ( ) } // TODO
214+ predicate expectsContent ( Node n , ContentSet c ) {
215+ FlowSummaryOutput:: summaryExpectsContent ( getSummaryNode ( n ) , c ) and
216+ not bypassContentSet ( c )
217+ }
170218
171- predicate localMustFlowStep ( Node node1 , Node node2 ) { localSsaMustFlowStep ( node1 , node2 ) } // TODO
219+ predicate localMustFlowStep ( Node node1 , Node node2 ) {
220+ step ( node1 , any ( Step s | s .valueMustFlow ( ) ) , node2 ) or
221+ localSsaMustFlowStep ( node1 , node2 ) or
222+ FlowSummaryOutput:: summaryLocalMustFlowStep ( getSummaryNode ( node1 ) , getSummaryNode ( node2 ) )
223+ }
172224
173225 //
174226 // Misc
@@ -207,7 +259,14 @@ module DataFlowInput implements InputSig<Location> {
207259
208260 predicate isUnreachableInCall ( NodeRegion nr , DataFlowCall call ) { none ( ) } // TODO
209261
210- predicate allowParameterReturnInSelf ( ParameterNode p ) { captureSsaAllowParameterReturnInSelf ( p ) }
262+ predicate allowParameterReturnInSelf ( ParameterNode p ) {
263+ captureSsaAllowParameterReturnInSelf ( p )
264+ or
265+ exists ( DataFlowCallable c , ParameterPosition pos |
266+ FlowSummaryOutput:: summaryAllowParameterReturnInSelf ( c .asSummarizedCallable ( ) , pos ) and
267+ isParameterNodeImpl ( p , c , pos )
268+ )
269+ }
211270
212271 class LambdaCallKind extends Unit { }
213272
@@ -216,9 +275,11 @@ module DataFlowInput implements InputSig<Location> {
216275 exists ( kind )
217276 }
218277
219- predicate lambdaCall ( DataFlowCall call , LambdaCallKind kind , Node receiver ) {
220- receiver .( BuilderNode ) .isImplicitArgument ( call , any ( ArgumentPosition p | p .isCallee ( ) ) , false ) and
278+ predicate lambdaCall ( DataFlowCall call , LambdaCallKind kind , Node callee ) {
279+ callee .( BuilderNode ) .isImplicitArgument ( call , any ( ArgumentPosition p | p .isCallee ( ) ) , false ) and
221280 exists ( kind )
281+ or
282+ call .isSummaryCall ( _, getSummaryNode ( callee ) ) and exists ( kind )
222283 }
223284
224285 predicate additionalLambdaFlowStep ( Node nodeFrom , Node nodeTo , boolean preservesValue ) {
0 commit comments