Sync files

This commit is contained in:
Tom Hvitved
2022-10-03 20:29:39 +02:00
parent bc3e9339dc
commit e57c3bec63

View File

@@ -16,6 +16,32 @@ private module Cached {
LoadStep(TypeTrackerContent content) { basicLoadStep(_, _, content) } or
JumpStep()
cached
newtype TTypeTracker =
MkTypeTracker(Boolean hasCall, OptionalTypeTrackerContent content) {
content = noContent()
or
// Restrict `content` to those that might eventually match a load.
// We can't rely on `basicStoreStep` since `startInContent` might be used with
// a content that has no corresponding store.
exists(TypeTrackerContent loadContents |
basicLoadStep(_, _, loadContents) and
compatibleContents(content, loadContents)
)
}
cached
newtype TTypeBackTracker =
MkTypeBackTracker(Boolean hasReturn, OptionalTypeTrackerContent content) {
content = noContent()
or
// As in MkTypeTracker, restrict `content` to those that might eventually match a store.
exists(TypeTrackerContent storeContent |
basicStoreStep(_, _, storeContent) and
compatibleContents(storeContent, content)
)
}
pragma[nomagic]
private TypeTracker noContentTypeTracker(boolean hasCall) {
result = MkTypeTracker(hasCall, noContent())
@@ -105,10 +131,65 @@ private module Cached {
predicate stepCall(TypeTrackingNode nodeFrom, TypeTrackingNode nodeTo, StepSummary summary) {
exists(Node mid | nodeFrom.flowsTo(mid) and smallstepCall(mid, nodeTo, summary))
}
cached
predicate smallstepNoCall(Node nodeFrom, TypeTrackingNode nodeTo, StepSummary summary) {
jumpStep(nodeFrom, nodeTo) and
summary = JumpStep()
or
levelStep(nodeFrom, nodeTo) and
summary = LevelStep()
or
exists(TypeTrackerContent content |
flowsToStoreStep(nodeFrom, nodeTo, content) and
summary = StoreStep(content)
or
basicLoadStep(nodeFrom, nodeTo, content) and summary = LoadStep(content)
)
}
cached
predicate smallstepCall(Node nodeFrom, TypeTrackingNode nodeTo, StepSummary summary) {
callStep(nodeFrom, nodeTo) and summary = CallStep()
or
returnStep(nodeFrom, nodeTo) and
summary = ReturnStep()
}
}
private import Cached
/**
* Holds if `nodeFrom` is being written to the `content` of the object in `nodeTo`.
*
* Note that `nodeTo` will always be a local source node that flows to the place where the content
* is written in `basicStoreStep`. This may lead to the flow of information going "back in time"
* from the point of view of the execution of the program.
*
* For instance, if we interpret attribute writes in Python as writing to content with the same
* name as the attribute and consider the following snippet
*
* ```python
* def foo(y):
* x = Foo()
* bar(x)
* x.attr = y
* baz(x)
*
* def bar(x):
* z = x.attr
* ```
* for the attribute write `x.attr = y`, we will have `content` being the literal string `"attr"`,
* `nodeFrom` will be `y`, and `nodeTo` will be the object `Foo()` created on the first line of the
* function. This means we will track the fact that `x.attr` can have the type of `y` into the
* assignment to `z` inside `bar`, even though this attribute write happens _after_ `bar` is called.
*/
private predicate flowsToStoreStep(
Node nodeFrom, TypeTrackingNode nodeTo, TypeTrackerContent content
) {
exists(Node obj | nodeTo.flowsTo(obj) and basicStoreStep(nodeFrom, obj, content))
}
/**
* INTERNAL: Use `TypeTracker` or `TypeBackTracker` instead.
*
@@ -131,30 +212,6 @@ class StepSummary extends TStepSummary {
}
}
pragma[noinline]
private predicate smallstepNoCall(Node nodeFrom, TypeTrackingNode nodeTo, StepSummary summary) {
jumpStep(nodeFrom, nodeTo) and
summary = JumpStep()
or
levelStep(nodeFrom, nodeTo) and
summary = LevelStep()
or
exists(TypeTrackerContent content |
StepSummary::localSourceStoreStep(nodeFrom, nodeTo, content) and
summary = StoreStep(content)
or
basicLoadStep(nodeFrom, nodeTo, content) and summary = LoadStep(content)
)
}
pragma[noinline]
private predicate smallstepCall(Node nodeFrom, TypeTrackingNode nodeTo, StepSummary summary) {
callStep(nodeFrom, nodeTo) and summary = CallStep()
or
returnStep(nodeFrom, nodeTo) and
summary = ReturnStep()
}
/** Provides predicates for updating step summaries (`StepSummary`s). */
module StepSummary {
/**
@@ -188,49 +245,9 @@ module StepSummary {
smallstepCall(nodeFrom, nodeTo, summary)
}
/**
* Holds if `nodeFrom` is being written to the `content` of the object in `nodeTo`.
*
* Note that `nodeTo` will always be a local source node that flows to the place where the content
* is written in `basicStoreStep`. This may lead to the flow of information going "back in time"
* from the point of view of the execution of the program.
*
* For instance, if we interpret attribute writes in Python as writing to content with the same
* name as the attribute and consider the following snippet
*
* ```python
* def foo(y):
* x = Foo()
* bar(x)
* x.attr = y
* baz(x)
*
* def bar(x):
* z = x.attr
* ```
* for the attribute write `x.attr = y`, we will have `content` being the literal string `"attr"`,
* `nodeFrom` will be `y`, and `nodeTo` will be the object `Foo()` created on the first line of the
* function. This means we will track the fact that `x.attr` can have the type of `y` into the
* assignment to `z` inside `bar`, even though this attribute write happens _after_ `bar` is called.
*/
predicate localSourceStoreStep(Node nodeFrom, TypeTrackingNode nodeTo, TypeTrackerContent content) {
exists(Node obj | nodeTo.flowsTo(obj) and basicStoreStep(nodeFrom, obj, content))
}
deprecated predicate localSourceStoreStep = flowsToStoreStep/3;
}
private newtype TTypeTracker =
MkTypeTracker(Boolean hasCall, OptionalTypeTrackerContent content) {
content = noContent()
or
// Restrict `content` to those that might eventually match a load.
// We can't rely on `basicStoreStep` since `startInContent` might be used with
// a content that has no corresponding store.
exists(TypeTrackerContent loadContents |
basicLoadStep(_, _, loadContents) and
compatibleContents(content, loadContents)
)
}
/**
* A summary of the steps needed to track a value to a given dataflow node.
*
@@ -382,17 +399,6 @@ module TypeTracker {
TypeTracker end() { result.end() }
}
private newtype TTypeBackTracker =
MkTypeBackTracker(Boolean hasReturn, OptionalTypeTrackerContent content) {
content = noContent()
or
// As in MkTypeTracker, restrict `content` to those that might eventually match a store.
exists(TypeTrackerContent storeContent |
basicStoreStep(_, _, storeContent) and
compatibleContents(storeContent, content)
)
}
/**
* A summary of the steps needed to back-track a use of a value to a given dataflow node.
*