Dataflow: Eliminate TypedContent.

This commit is contained in:
Anders Schack-Mulligen
2023-03-28 09:50:00 +02:00
parent 5373b4d466
commit 4f2d2361a4
2 changed files with 8 additions and 41 deletions

View File

@@ -392,7 +392,7 @@ module Impl<FullStateConfigSig Config> {
pragma[nomagic] pragma[nomagic]
private predicate storeEx(NodeEx node1, Content c, NodeEx node2, DataFlowType contentType, DataFlowType containerType) { private predicate storeEx(NodeEx node1, Content c, NodeEx node2, DataFlowType contentType, DataFlowType containerType) {
store(pragma[only_bind_into](node1.asNode()), _, c, pragma[only_bind_into](node2.asNode()), store(pragma[only_bind_into](node1.asNode()), c, pragma[only_bind_into](node2.asNode()),
contentType, containerType) and contentType, containerType) and
hasReadStep(c) and hasReadStep(c) and
stepFilter(node1, node2) stepFilter(node1, node2)

View File

@@ -815,26 +815,20 @@ private module Cached {
) )
} }
private predicate store(
Node node1, Content c, Node node2, DataFlowType contentType, DataFlowType containerType
) {
exists(ContentSet cs |
c = cs.getAStoreContent() and storeSet(node1, cs, node2, contentType, containerType)
)
}
/** /**
* Holds if data can flow from `node1` to `node2` via a direct assignment to * Holds if data can flow from `node1` to `node2` via a direct assignment to
* `f`. * `c`.
* *
* This includes reverse steps through reads when the result of the read has * This includes reverse steps through reads when the result of the read has
* been stored into, in order to handle cases like `x.f1.f2 = y`. * been stored into, in order to handle cases like `x.f1.f2 = y`.
*/ */
cached cached
predicate store(Node node1, TypedContent tc, Content c, Node node2, DataFlowType contentType, DataFlowType containerType) { predicate store(
tc.getContent() = c and Node node1, Content c, Node node2, DataFlowType contentType, DataFlowType containerType
tc.getContainerType() = containerType and ) {
store(node1, c, node2, contentType, containerType) exists(ContentSet cs |
c = cs.getAStoreContent() and storeSet(node1, cs, node2, contentType, containerType)
)
} }
/** /**
@@ -934,9 +928,6 @@ private module Cached {
TReturnCtxNoFlowThrough() or TReturnCtxNoFlowThrough() or
TReturnCtxMaybeFlowThrough(ReturnPosition pos) TReturnCtxMaybeFlowThrough(ReturnPosition pos)
cached
newtype TTypedContent = MkTypedContent(Content c, DataFlowType t) { store(_, c, _, _, t) }
cached cached
newtype TAccessPathFront = newtype TAccessPathFront =
TFrontNil() or TFrontNil() or
@@ -1415,30 +1406,6 @@ class ApproxAccessPathFrontOption extends TApproxAccessPathFrontOption {
} }
} }
/** A `Content` tagged with the type of a containing object. */
class TypedContent extends MkTypedContent {
private Content c;
private DataFlowType t;
TypedContent() { this = MkTypedContent(c, t) }
/** Gets the content. */
Content getContent() { result = c }
/** Gets the container type. */
DataFlowType getContainerType() { result = t }
/** Gets a textual representation of this content. */
string toString() { result = c.toString() }
/**
* Holds if access paths with this `TypedContent` at their head always should
* be tracked at high precision. This disables adaptive access path precision
* for such access paths.
*/
predicate forceHighPrecision() { forceHighPrecision(c) }
}
/** /**
* The front of an access path. This is either a head or a nil. * The front of an access path. This is either a head or a nil.
*/ */