Dataflow: Fix some perf issues.

This commit is contained in:
Anders Schack-Mulligen
2023-03-03 11:45:32 +01:00
parent b34f99f716
commit 0addcfa7c5
9 changed files with 36 additions and 0 deletions

View File

@@ -565,6 +565,7 @@ module Impl<FullStateConfigSig Config> {
/**
* Holds if `c` is the target of a store in the flow covered by `fwdFlow`.
*/
pragma[assume_small_delta]
pragma[nomagic]
private predicate fwdFlowConsCand(Content c) {
exists(NodeEx mid, NodeEx node, TypedContent tc |
@@ -784,6 +785,7 @@ module Impl<FullStateConfigSig Config> {
)
}
pragma[nomagic]
additional predicate revFlowState(FlowState state) {
exists(NodeEx node |
sinkNode(node, state) and
@@ -1187,6 +1189,7 @@ module Impl<FullStateConfigSig Config> {
fwdFlow(node, state, cc, summaryCtx, argAp, ap, _)
}
pragma[assume_small_delta]
pragma[nomagic]
private predicate fwdFlow0(
NodeEx node, FlowState state, Cc cc, ParamNodeOption summaryCtx, ApOption argAp, Ap ap,
@@ -3512,6 +3515,7 @@ module Impl<FullStateConfigSig Config> {
)
}
pragma[assume_small_delta]
pragma[nomagic]
private predicate pathThroughCallable0(
DataFlowCall call, PathNodeMid mid, ReturnKindExt kind, FlowState state, CallContext cc,