Dataflow: Remove revFlowAlias trick

This commit is contained in:
Kasper Svendsen
2023-03-20 09:04:35 +01:00
parent 540542ceb5
commit 9630feb5e4
8 changed files with 80 additions and 160 deletions

View File

@@ -1695,16 +1695,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 +1968,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 +1977,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 +2059,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 +2256,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 +2267,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 +2278,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 +2580,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 +2590,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 +2601,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), _)
)
}