11/**
2- * Provides the implementation of a summary type tracker, that is type tracking through flow summaries.
2+ * Provides the implementation of type tracking steps through flow summaries.
33 * To use this, you must implement the `Input` signature. You can then use the predicates in the `Output`
44 * signature to implement the predicates of the same names inside `TypeTrackerSpecific.qll`.
55 */
66
7- /** The classes and predicates needed to generate a summary type tracker . */
7+ /** The classes and predicates needed to generate type-tracking steps from summaries . */
88signature module Input {
99 // Dataflow nodes
1010 class Node ;
@@ -80,13 +80,6 @@ signature module Input {
8080 /** Gets a dataflow node respresenting the return of `callable` indicated by `return`. */
8181 Node returnOf ( Node callable , SummaryComponent return ) ;
8282
83- // Specific summary handling
84- /** Holds if component should be treated as a level step by type tracking. */
85- predicate componentLevelStep ( SummaryComponent component ) ;
86-
87- /** Holds if the given component can't be evaluated by `evaluateSummaryComponentStackLocal`. */
88- predicate isNonLocal ( SummaryComponent component ) ;
89-
9083 // Relating callables to nodes
9184 /** Gets a dataflow node respresenting a call to `callable`. */
9285 Node callTo ( SummarizedCallable callable ) ;
@@ -146,17 +139,17 @@ module SummaryFlow<Input I> implements Output<I> {
146139 I:: SummaryComponentStack output
147140 ) {
148141 callable .propagatesFlow ( I:: push ( I:: content ( contents ) , input ) , output , true ) and
149- not I :: isNonLocal ( input .head ( ) ) and
150- not I :: isNonLocal ( output .head ( ) )
142+ not isNonLocal ( input .head ( ) ) and
143+ not isNonLocal ( output .head ( ) )
151144 }
152145
153146 pragma [ nomagic]
154147 private predicate hasStoreSummary (
155148 I:: SummarizedCallable callable , I:: TypeTrackerContent contents , I:: SummaryComponentStack input ,
156149 I:: SummaryComponentStack output
157150 ) {
158- not I :: isNonLocal ( input .head ( ) ) and
159- not I :: isNonLocal ( output .head ( ) ) and
151+ not isNonLocal ( input .head ( ) ) and
152+ not isNonLocal ( output .head ( ) ) and
160153 (
161154 callable .propagatesFlow ( input , I:: push ( I:: content ( contents ) , output ) , true )
162155 or
@@ -178,8 +171,8 @@ module SummaryFlow<Input I> implements Output<I> {
178171 callable
179172 .propagatesFlow ( I:: push ( I:: content ( loadContents ) , input ) ,
180173 I:: push ( I:: content ( storeContents ) , output ) , true ) and
181- not I :: isNonLocal ( input .head ( ) ) and
182- not I :: isNonLocal ( output .head ( ) )
174+ not isNonLocal ( input .head ( ) ) and
175+ not isNonLocal ( output .head ( ) )
183176 }
184177
185178 pragma [ nomagic]
@@ -190,8 +183,8 @@ module SummaryFlow<Input I> implements Output<I> {
190183 exists ( I:: TypeTrackerContent content |
191184 callable .propagatesFlow ( I:: push ( I:: withoutContent ( content ) , input ) , output , true ) and
192185 filter = I:: getFilterFromWithoutContentStep ( content ) and
193- not I :: isNonLocal ( input .head ( ) ) and
194- not I :: isNonLocal ( output .head ( ) ) and
186+ not isNonLocal ( input .head ( ) ) and
187+ not isNonLocal ( output .head ( ) ) and
195188 input != output
196189 )
197190 }
@@ -204,12 +197,26 @@ module SummaryFlow<Input I> implements Output<I> {
204197 exists ( I:: TypeTrackerContent content |
205198 callable .propagatesFlow ( I:: push ( I:: withContent ( content ) , input ) , output , true ) and
206199 filter = I:: getFilterFromWithContentStep ( content ) and
207- not I :: isNonLocal ( input .head ( ) ) and
208- not I :: isNonLocal ( output .head ( ) ) and
200+ not isNonLocal ( input .head ( ) ) and
201+ not isNonLocal ( output .head ( ) ) and
209202 input != output
210203 )
211204 }
212205
206+ private predicate componentLevelStep ( I:: SummaryComponent component ) {
207+ exists ( I:: TypeTrackerContent content |
208+ component = I:: withoutContent ( content ) and
209+ not exists ( I:: getFilterFromWithoutContentStep ( content ) )
210+ )
211+ }
212+
213+ pragma [ nomagic]
214+ private predicate isNonLocal ( I:: SummaryComponent component ) {
215+ component = I:: content ( _)
216+ or
217+ component = I:: withContent ( _)
218+ }
219+
213220 /**
214221 * Gets a data flow I::Node corresponding an argument or return value of `call`,
215222 * as specified by `component`.
@@ -255,7 +262,7 @@ module SummaryFlow<Input I> implements Output<I> {
255262 I:: SummarizedCallable callable , I:: SummaryComponent head , I:: SummaryComponentStack tail
256263 ) {
257264 dependsOnSummaryComponentStackCons ( callable , head , tail ) and
258- not I :: isNonLocal ( head )
265+ not isNonLocal ( head )
259266 }
260267
261268 pragma [ nomagic]
@@ -290,7 +297,7 @@ module SummaryFlow<Input I> implements Output<I> {
290297 or
291298 result = I:: returnOf ( prev , head )
292299 or
293- I :: componentLevelStep ( head ) and
300+ componentLevelStep ( head ) and
294301 result = prev
295302 )
296303 }
0 commit comments