@@ -18,65 +18,71 @@ private module Cached {
1818
1919 pragma [ nomagic]
2020 private TypeTracker noContentTypeTracker ( boolean hasCall ) {
21- result = MkTypeTracker ( hasCall , noContent ( ) )
21+ result = MkTypeTracker ( hasCall , noContentSet ( ) )
2222 }
2323
2424 /** Gets the summary resulting from appending `step` to type-tracking summary `tt`. */
2525 cached
2626 TypeTracker append ( TypeTracker tt , StepSummary step ) {
27- exists ( Boolean hasCall , OptionalTypeTrackerContent currentContent |
28- tt = MkTypeTracker ( hasCall , currentContent )
27+ exists ( Boolean hasCall , OptionalTypeTrackerContentSet currentContents |
28+ tt = MkTypeTracker ( hasCall , currentContents )
2929 |
3030 step = LevelStep ( ) and result = tt
3131 or
32- step = CallStep ( ) and result = MkTypeTracker ( true , currentContent )
32+ step = CallStep ( ) and result = MkTypeTracker ( true , currentContents )
3333 or
3434 step = ReturnStep ( ) and hasCall = false and result = tt
3535 or
3636 step = JumpStep ( ) and
37- result = MkTypeTracker ( false , currentContent )
37+ result = MkTypeTracker ( false , currentContents )
3838 )
3939 or
40- exists ( TypeTrackerContentSet contents , boolean hasCall |
41- step = LoadStep ( pragma [ only_bind_into ] ( contents ) ) and
42- tt = MkTypeTracker ( hasCall , contents .getAReadContent ( ) ) and
43- result = noContentTypeTracker ( hasCall )
40+ exists ( TypeTrackerContentSet storeContents , boolean hasCall |
41+ exists ( TypeTrackerContentSet loadContents |
42+ step = LoadStep ( pragma [ only_bind_into ] ( loadContents ) ) and
43+ tt = MkTypeTracker ( hasCall , storeContents ) and
44+ storeContents .getAStoreContent ( ) = loadContents .getAReadContent ( ) and
45+ result = noContentTypeTracker ( hasCall )
46+ )
4447 or
45- step = StoreStep ( pragma [ only_bind_into ] ( contents ) ) and
48+ step = StoreStep ( pragma [ only_bind_into ] ( storeContents ) ) and
4649 tt = noContentTypeTracker ( hasCall ) and
47- result = MkTypeTracker ( hasCall , contents . getAStoreContent ( ) )
50+ result = MkTypeTracker ( hasCall , storeContents )
4851 )
4952 }
5053
5154 pragma [ nomagic]
5255 private TypeBackTracker noContentTypeBackTracker ( boolean hasReturn ) {
53- result = MkTypeBackTracker ( hasReturn , noContent ( ) )
56+ result = MkTypeBackTracker ( hasReturn , noContentSet ( ) )
5457 }
5558
5659 /** Gets the summary resulting from prepending `step` to this type-tracking summary. */
5760 cached
5861 TypeBackTracker prepend ( TypeBackTracker tbt , StepSummary step ) {
59- exists ( Boolean hasReturn , OptionalTypeTrackerContent content |
60- tbt = MkTypeBackTracker ( hasReturn , content )
62+ exists ( Boolean hasReturn , OptionalTypeTrackerContentSet contents |
63+ tbt = MkTypeBackTracker ( hasReturn , contents )
6164 |
6265 step = LevelStep ( ) and result = tbt
6366 or
6467 step = CallStep ( ) and hasReturn = false and result = tbt
6568 or
66- step = ReturnStep ( ) and result = MkTypeBackTracker ( true , content )
69+ step = ReturnStep ( ) and result = MkTypeBackTracker ( true , contents )
6770 or
6871 step = JumpStep ( ) and
69- result = MkTypeBackTracker ( false , content )
72+ result = MkTypeBackTracker ( false , contents )
7073 )
7174 or
72- exists ( TypeTrackerContentSet contents , boolean hasReturn |
73- step = StoreStep ( pragma [ only_bind_into ] ( contents ) ) and
74- tbt = MkTypeBackTracker ( hasReturn , contents .getAReadContent ( ) ) and
75- result = noContentTypeBackTracker ( hasReturn )
75+ exists ( TypeTrackerContentSet loadContents , boolean hasReturn |
76+ exists ( TypeTrackerContentSet storeContents |
77+ step = StoreStep ( pragma [ only_bind_into ] ( storeContents ) ) and
78+ tbt = MkTypeBackTracker ( hasReturn , loadContents ) and
79+ storeContents .getAStoreContent ( ) = loadContents .getAReadContent ( ) and
80+ result = noContentTypeBackTracker ( hasReturn )
81+ )
7682 or
77- step = LoadStep ( pragma [ only_bind_into ] ( contents ) ) and
83+ step = LoadStep ( pragma [ only_bind_into ] ( loadContents ) ) and
7884 tbt = noContentTypeBackTracker ( hasReturn ) and
79- result = MkTypeBackTracker ( hasReturn , contents . getAStoreContent ( ) )
85+ result = MkTypeBackTracker ( hasReturn , loadContents )
8086 )
8187 }
8288
@@ -216,7 +222,8 @@ module StepSummary {
216222 }
217223}
218224
219- private newtype TTypeTracker = MkTypeTracker ( Boolean hasCall , OptionalTypeTrackerContent content )
225+ private newtype TTypeTracker =
226+ MkTypeTracker ( Boolean hasCall , OptionalTypeTrackerContentSet contents )
220227
221228/**
222229 * A summary of the steps needed to track a value to a given dataflow node.
@@ -247,9 +254,9 @@ private newtype TTypeTracker = MkTypeTracker(Boolean hasCall, OptionalTypeTracke
247254 */
248255class TypeTracker extends TTypeTracker {
249256 Boolean hasCall ;
250- OptionalTypeTrackerContent content ;
257+ OptionalTypeTrackerContentSet contents ;
251258
252- TypeTracker ( ) { this = MkTypeTracker ( hasCall , content ) }
259+ TypeTracker ( ) { this = MkTypeTracker ( hasCall , contents ) }
253260
254261 /** Gets the summary resulting from appending `step` to this type-tracking summary. */
255262 TypeTracker append ( StepSummary step ) { result = append ( this , step ) }
@@ -259,8 +266,8 @@ class TypeTracker extends TTypeTracker {
259266 exists ( string withCall , string withContent |
260267 ( if hasCall = true then withCall = "with" else withCall = "without" ) and
261268 (
262- if content != noContent ( )
263- then withContent = " with content " + content
269+ if contents != noContentSet ( )
270+ then withContent = " with content " + contents
264271 else withContent = ""
265272 ) and
266273 result = "type tracker " + withCall + " call steps" + withContent
@@ -270,26 +277,26 @@ class TypeTracker extends TTypeTracker {
270277 /**
271278 * Holds if this is the starting point of type tracking.
272279 */
273- predicate start ( ) { hasCall = false and content = noContent ( ) }
280+ predicate start ( ) { hasCall = false and contents = noContentSet ( ) }
274281
275282 /**
276283 * Holds if this is the starting point of type tracking, and the value starts in the content named `contentName`.
277284 * The type tracking only ends after the content has been loaded.
278285 */
279- predicate startInContent ( TypeTrackerContent contentName ) {
280- hasCall = false and content = contentName
286+ predicate startInContent ( TypeTrackerContentSet contentName ) {
287+ hasCall = false and contents = contentName
281288 }
282289
283290 /**
284291 * Holds if this is the starting point of type tracking
285292 * when tracking a parameter into a call, but not out of it.
286293 */
287- predicate call ( ) { hasCall = true and content = noContent ( ) }
294+ predicate call ( ) { hasCall = true and contents = noContentSet ( ) }
288295
289296 /**
290297 * Holds if this is the end point of type tracking.
291298 */
292- predicate end ( ) { content = noContent ( ) }
299+ predicate end ( ) { contents = noContentSet ( ) }
293300
294301 /**
295302 * INTERNAL. DO NOT USE.
@@ -303,15 +310,15 @@ class TypeTracker extends TTypeTracker {
303310 *
304311 * Gets the content associated with this type tracker.
305312 */
306- OptionalTypeTrackerContent getContent ( ) { result = content }
313+ OptionalTypeTrackerContentSet getContent ( ) { result = contents }
307314
308315 /**
309316 * Gets a type tracker that starts where this one has left off to allow continued
310317 * tracking.
311318 *
312319 * This predicate is only defined if the type is not associated to a piece of content.
313320 */
314- TypeTracker continue ( ) { content = noContent ( ) and result = this }
321+ TypeTracker continue ( ) { contents = noContentSet ( ) and result = this }
315322
316323 /**
317324 * Gets the summary that corresponds to having taken a forwards
@@ -370,7 +377,7 @@ module TypeTracker {
370377}
371378
372379private newtype TTypeBackTracker =
373- MkTypeBackTracker ( Boolean hasReturn , OptionalTypeTrackerContent content )
380+ MkTypeBackTracker ( Boolean hasReturn , OptionalTypeTrackerContentSet contents )
374381
375382/**
376383 * A summary of the steps needed to back-track a use of a value to a given dataflow node.
@@ -404,9 +411,9 @@ private newtype TTypeBackTracker =
404411 */
405412class TypeBackTracker extends TTypeBackTracker {
406413 Boolean hasReturn ;
407- OptionalTypeTrackerContent content ;
414+ OptionalTypeTrackerContentSet contents ;
408415
409- TypeBackTracker ( ) { this = MkTypeBackTracker ( hasReturn , content ) }
416+ TypeBackTracker ( ) { this = MkTypeBackTracker ( hasReturn , contents ) }
410417
411418 /** Gets the summary resulting from prepending `step` to this type-tracking summary. */
412419 TypeBackTracker prepend ( StepSummary step ) { result = prepend ( this , step ) }
@@ -416,8 +423,8 @@ class TypeBackTracker extends TTypeBackTracker {
416423 exists ( string withReturn , string withContent |
417424 ( if hasReturn = true then withReturn = "with" else withReturn = "without" ) and
418425 (
419- if content != noContent ( )
420- then withContent = " with content " + content
426+ if contents != noContentSet ( )
427+ then withContent = " with content " + contents
421428 else withContent = ""
422429 ) and
423430 result = "type back-tracker " + withReturn + " return steps" + withContent
@@ -427,12 +434,12 @@ class TypeBackTracker extends TTypeBackTracker {
427434 /**
428435 * Holds if this is the starting point of type tracking.
429436 */
430- predicate start ( ) { hasReturn = false and content = noContent ( ) }
437+ predicate start ( ) { hasReturn = false and contents = noContentSet ( ) }
431438
432439 /**
433440 * Holds if this is the end point of type tracking.
434441 */
435- predicate end ( ) { content = noContent ( ) }
442+ predicate end ( ) { contents = noContentSet ( ) }
436443
437444 /**
438445 * INTERNAL. DO NOT USE.
@@ -447,7 +454,7 @@ class TypeBackTracker extends TTypeBackTracker {
447454 *
448455 * This predicate is only defined if the type has not been tracked into a piece of content.
449456 */
450- TypeBackTracker continue ( ) { content = noContent ( ) and result = this }
457+ TypeBackTracker continue ( ) { contents = noContentSet ( ) and result = this }
451458
452459 /**
453460 * Gets the summary that corresponds to having taken a backwards
@@ -504,7 +511,7 @@ class TypeBackTracker extends TTypeBackTracker {
504511 * also flow to `sink`.
505512 */
506513 TypeTracker getACompatibleTypeTracker ( ) {
507- exists ( boolean hasCall | result = MkTypeTracker ( hasCall , content ) |
514+ exists ( boolean hasCall | result = MkTypeTracker ( hasCall , contents ) |
508515 hasCall = false or this .hasReturn ( ) = false
509516 )
510517 }
0 commit comments