Merge pull request #12420 from kaspersv/kaspersv/dataflow-remove-alias-preds

Dataflow: Remove revFlowAlias and revFlowApAlias predicates
This commit is contained in:
Anders Schack-Mulligen
2023-03-20 16:30:15 +01:00
committed by GitHub
8 changed files with 96 additions and 224 deletions

View File

@@ -1145,19 +1145,13 @@ module Impl<FullStateConfigSig Config> {
import Param
/* Begin: Stage logic. */
// use an alias as a workaround for bad functionality-induced joins
pragma[nomagic]
private predicate revFlowApAlias(NodeEx node, ApApprox apa) {
PrevStage::revFlowAp(node, apa)
}
pragma[nomagic]
private predicate flowIntoCallApa(
DataFlowCall call, ArgNodeEx arg, ParamNodeEx p, boolean allowsFieldFlow, ApApprox apa
) {
flowIntoCall(call, arg, p, allowsFieldFlow) and
PrevStage::revFlowAp(p, pragma[only_bind_into](apa)) and
revFlowApAlias(arg, pragma[only_bind_into](apa))
PrevStage::revFlowAp(arg, pragma[only_bind_into](apa))
}
pragma[nomagic]
@@ -1167,7 +1161,7 @@ module Impl<FullStateConfigSig Config> {
) {
flowOutOfCall(call, ret, kind, out, allowsFieldFlow) and
PrevStage::revFlowAp(out, pragma[only_bind_into](apa)) and
revFlowApAlias(ret, pragma[only_bind_into](apa))
PrevStage::revFlowAp(ret, pragma[only_bind_into](apa))
}
pragma[nomagic]
@@ -1695,16 +1689,6 @@ module Impl<FullStateConfigSig Config> {
pragma[nomagic]
predicate revFlowAp(NodeEx node, Ap ap) { revFlow(node, _, _, _, ap) }
// use an alias as a workaround for bad functionality-induced joins
pragma[nomagic]
additional predicate revFlowAlias(NodeEx node) { revFlow(node, _, _, _, _) }
// use an alias as a workaround for bad functionality-induced joins
pragma[nomagic]
additional predicate revFlowAlias(NodeEx node, FlowState state, Ap ap) {
revFlow(node, state, ap)
}
private predicate fwdConsCand(TypedContent tc, Ap ap) { storeStepFwd(_, ap, tc, _, _) }
private predicate revConsCand(TypedContent tc, Ap ap) { storeStepCand(_, ap, tc, _, _) }
@@ -1978,7 +1962,7 @@ module Impl<FullStateConfigSig Config> {
) {
flowOutOfCallNodeCand1(call, node1, kind, node2, allowsFieldFlow) and
Stage2::revFlow(node2) and
Stage2::revFlowAlias(node1)
Stage2::revFlow(node1)
}
pragma[nomagic]
@@ -1987,7 +1971,7 @@ module Impl<FullStateConfigSig Config> {
) {
flowIntoCallNodeCand1(call, node1, node2, allowsFieldFlow) and
Stage2::revFlow(node2) and
Stage2::revFlowAlias(node1)
Stage2::revFlow(node1)
}
private module LocalFlowBigStep {
@@ -2069,11 +2053,11 @@ module Impl<FullStateConfigSig Config> {
additionalLocalFlowStepNodeCand1(node1, node2) and
state1 = state2 and
Stage2::revFlow(node1, pragma[only_bind_into](state1), false) and
Stage2::revFlowAlias(node2, pragma[only_bind_into](state2), false)
Stage2::revFlow(node2, pragma[only_bind_into](state2), false)
or
additionalLocalStateStep(node1, state1, node2, state2) and
Stage2::revFlow(node1, state1, false) and
Stage2::revFlowAlias(node2, state2, false)
Stage2::revFlow(node2, state2, false)
}
/**
@@ -2266,7 +2250,7 @@ module Impl<FullStateConfigSig Config> {
) {
localFlowBigStep(node1, state1, node2, state2, preservesValue, ap.getType(), _) and
PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and
PrevStage::revFlowAlias(node2, pragma[only_bind_into](state2), _) and
PrevStage::revFlow(node2, pragma[only_bind_into](state2), _) and
exists(lcc)
}
@@ -2277,7 +2261,7 @@ module Impl<FullStateConfigSig Config> {
exists(FlowState state |
flowOutOfCallNodeCand2(call, node1, kind, node2, allowsFieldFlow) and
PrevStage::revFlow(node2, pragma[only_bind_into](state), _) and
PrevStage::revFlowAlias(node1, pragma[only_bind_into](state), _)
PrevStage::revFlow(node1, pragma[only_bind_into](state), _)
)
}
@@ -2288,7 +2272,7 @@ module Impl<FullStateConfigSig Config> {
exists(FlowState state |
flowIntoCallNodeCand2(call, node1, node2, allowsFieldFlow) and
PrevStage::revFlow(node2, pragma[only_bind_into](state), _) and
PrevStage::revFlowAlias(node1, pragma[only_bind_into](state), _)
PrevStage::revFlow(node1, pragma[only_bind_into](state), _)
)
}
@@ -2590,7 +2574,7 @@ module Impl<FullStateConfigSig Config> {
) {
localFlowBigStep(node1, state1, node2, state2, preservesValue, ap.getType(), lcc) and
PrevStage::revFlow(node1, pragma[only_bind_into](state1), _) and
PrevStage::revFlowAlias(node2, pragma[only_bind_into](state2), _)
PrevStage::revFlow(node2, pragma[only_bind_into](state2), _)
}
pragma[nomagic]
@@ -2600,7 +2584,7 @@ module Impl<FullStateConfigSig Config> {
exists(FlowState state |
flowOutOfCallNodeCand2(call, node1, kind, node2, allowsFieldFlow) and
PrevStage::revFlow(node2, pragma[only_bind_into](state), _) and
PrevStage::revFlowAlias(node1, pragma[only_bind_into](state), _)
PrevStage::revFlow(node1, pragma[only_bind_into](state), _)
)
}
@@ -2611,7 +2595,7 @@ module Impl<FullStateConfigSig Config> {
exists(FlowState state |
flowIntoCallNodeCand2(call, node1, node2, allowsFieldFlow) and
PrevStage::revFlow(node2, pragma[only_bind_into](state), _) and
PrevStage::revFlowAlias(node1, pragma[only_bind_into](state), _)
PrevStage::revFlow(node1, pragma[only_bind_into](state), _)
)
}