Merge pull request #13455 from owen-mc/dataflow/add-flowCheckNodeSpecific

Dataflow: add language-specific hook for breaking up big step relation
This commit is contained in:
Owen Mansel-Chan
2023-06-20 13:24:26 +01:00
committed by GitHub
16 changed files with 71 additions and 13 deletions

View File

@@ -2021,7 +2021,8 @@ module Impl<FullStateConfigSig Config> {
FlowCheckNode() {
castNode(this.asNode()) or
clearsContentCached(this.asNode(), _) or
expectsContentCached(this.asNode(), _)
expectsContentCached(this.asNode(), _) or
neverSkipInPathGraph(this.asNode())
}
}

View File

@@ -235,6 +235,12 @@ class CastNode extends Node {
CastNode() { none() } // stub implementation
}
/**
* Holds if `n` should never be skipped over in the `PathGraph` and in path
* explanations.
*/
predicate neverSkipInPathGraph(Node n) { none() }
class DataFlowCallable = Function;
class DataFlowExpr = Expr;

View File

@@ -2021,7 +2021,8 @@ module Impl<FullStateConfigSig Config> {
FlowCheckNode() {
castNode(this.asNode()) or
clearsContentCached(this.asNode(), _) or
expectsContentCached(this.asNode(), _)
expectsContentCached(this.asNode(), _) or
neverSkipInPathGraph(this.asNode())
}
}

View File

@@ -783,6 +783,12 @@ class CastNode extends Node {
CastNode() { none() } // stub implementation
}
/**
* Holds if `n` should never be skipped over in the `PathGraph` and in path
* explanations.
*/
predicate neverSkipInPathGraph(Node n) { none() }
/**
* A function that may contain code or a variable that may contain itself. When
* flow crosses from one _enclosing callable_ to another, the interprocedural