Dataflow: Sync.

This commit is contained in:
Anders Schack-Mulligen
2023-07-11 13:42:09 +02:00
parent fd83b6afdb
commit 95d17045c9
45 changed files with 251 additions and 7 deletions

View File

@@ -46,6 +46,14 @@ signature module ConfigSig {
*/
default predicate allowImplicitRead(Node node, ContentSet c) { none() }
/**
* Holds if `node` should never be skipped over in the `PathGraph` and in path
* explanations.
*/
default predicate neverSkip(Node node) {
isAdditionalFlowStep(node, _) or isAdditionalFlowStep(_, node)
}
/**
* Gets the virtual dispatch branching limit when calculating field flow.
* This can be overridden to a smaller value to improve performance (a
@@ -141,6 +149,17 @@ signature module StateConfigSig {
*/
default predicate allowImplicitRead(Node node, ContentSet c) { none() }
/**
* Holds if `node` should never be skipped over in the `PathGraph` and in path
* explanations.
*/
default predicate neverSkip(Node node) {
isAdditionalFlowStep(node, _) or
isAdditionalFlowStep(_, node) or
isAdditionalFlowStep(node, _, _, _) or
isAdditionalFlowStep(_, _, node, _)
}
/**
* Gets the virtual dispatch branching limit when calculating field flow.
* This can be overridden to a smaller value to improve performance (a

View File

@@ -66,6 +66,12 @@ signature module FullStateConfigSig {
*/
predicate allowImplicitRead(Node node, ContentSet c);
/**
* Holds if `node` should never be skipped over in the `PathGraph` and in path
* explanations.
*/
predicate neverSkip(Node node);
/**
* Gets the virtual dispatch branching limit when calculating field flow.
* This can be overridden to a smaller value to improve performance (a
@@ -2024,7 +2030,8 @@ module Impl<FullStateConfigSig Config> {
castNode(this.asNode()) or
clearsContentCached(this.asNode(), _) or
expectsContentCached(this.asNode(), _) or
neverSkipInPathGraph(this.asNode())
neverSkipInPathGraph(this.asNode()) or
Config::neverSkip(this.asNode())
}
}

View File

@@ -313,6 +313,8 @@ private module Config implements FullStateConfigSig {
any(Configuration config).allowImplicitRead(node, c)
}
predicate neverSkip(Node node) { none() }
int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }

View File

@@ -313,6 +313,8 @@ private module Config implements FullStateConfigSig {
any(Configuration config).allowImplicitRead(node, c)
}
predicate neverSkip(Node node) { none() }
int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }

View File

@@ -313,6 +313,8 @@ private module Config implements FullStateConfigSig {
any(Configuration config).allowImplicitRead(node, c)
}
predicate neverSkip(Node node) { none() }
int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }

View File

@@ -313,6 +313,8 @@ private module Config implements FullStateConfigSig {
any(Configuration config).allowImplicitRead(node, c)
}
predicate neverSkip(Node node) { none() }
int fieldFlowBranchLimit() { result = min(any(Configuration config).fieldFlowBranchLimit()) }
FlowFeature getAFeature() { result = any(Configuration config).getAFeature() }