Dataflow: Refactor forward store step relation.

This commit is contained in:
Anders Schack-Mulligen
2020-11-09 14:56:08 +01:00
parent b6f1ab6429
commit c5a2c261dc

View File

@@ -1142,6 +1142,17 @@ private module Stage2 {
)
}
pragma[nomagic]
predicate storeStepCand(
Node node1, Ap ap1, TypedContent tc, Node node2, DataFlowType contentType, Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType) and
revFlowStore(ap2, c, ap1, node1, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
}
predicate revFlow(Node node, Configuration config) { revFlow(node, _, _, _, config) }
/* End: Stage 2 logic. */
}
@@ -1292,16 +1303,6 @@ private predicate readCand2(Node node1, Content c, Node node2, Configuration con
Stage2::revFlowIsReadAndStored(c, unbind(config))
}
pragma[nomagic]
private predicate storeCand2(
Node node1, TypedContent tc, Node node2, DataFlowType contentType, Configuration config
) {
store(node1, tc, node2, contentType) and
Stage2::revFlow(node1, config) and
Stage2::revFlow(node2, _, _, true, unbind(config)) and
Stage2::revFlowIsReadAndStored(tc.getContent(), unbind(config))
}
private module Stage3 {
class ApApprox = Stage2::Ap;
@@ -1451,7 +1452,7 @@ private module Stage3 {
) {
exists(DataFlowType contentType |
fwdFlow(node1, cc, argAp, ap1, config) and
storeCand2(node1, tc, node2, contentType, config) and
Stage2::storeStepCand(node1, getApprox(ap1), tc, node2, contentType, config) and
// We need to typecheck stores here, since reverse flow through a getter
// might have a different type here compared to inside the getter.
compatibleTypes(ap1.getType(), contentType)
@@ -1691,6 +1692,17 @@ private module Stage3 {
)
}
pragma[nomagic]
predicate storeStepCand(
Node node1, Ap ap1, TypedContent tc, Node node2, DataFlowType contentType, Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType) and
revFlowStore(ap2, c, ap1, node1, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
}
predicate readStepCand(Node node1, Content c, Node node2, Configuration config) {
exists(Ap ap |
revFlow(node2, _, _, ap, config) and
@@ -2060,8 +2072,10 @@ private module Stage4 {
private predicate fwdFlowStore(
Node node1, Ap ap1, TypedContent tc, Node node2, Cc cc, ApOption argAp, Configuration config
) {
fwdFlow(node1, cc, argAp, ap1, config) and
fwdFlowStore0(node1, tc, node2, ap1.getFront(), config)
exists(DataFlowType contentType |
fwdFlow(node1, cc, argAp, ap1, config) and
Stage3::storeStepCand(node1, getApprox(ap1), tc, node2, contentType, config)
)
}
pragma[nomagic]
@@ -2073,27 +2087,6 @@ private module Stage4 {
)
}
pragma[nomagic]
private predicate storeCand(
Node mid, TypedContent tc, Node node, AccessPathFront apf0, AccessPathFront apf,
Configuration config
) {
storeCand2(mid, tc, node, _, config) and
flowCand(mid, apf0, config) and
apf.headUsesContent(tc)
}
pragma[noinline]
private predicate fwdFlowStore0(
Node mid, TypedContent tc, Node node, AccessPathFront apf0, Configuration config
) {
exists(AccessPathFront apf |
storeCand(mid, tc, node, apf0, apf, config) and
stage3consCand(tc, apf0, config) and
flowCand(node, apf, unbind(config))
)
}
pragma[nomagic]
private predicate fwdFlowRead(
Ap ap, Content c, Node node1, Node node2, Cc cc, ApOption argAp, Configuration config
@@ -2316,6 +2309,17 @@ private module Stage4 {
)
}
pragma[nomagic]
predicate storeStepCand(
Node node1, Ap ap1, TypedContent tc, Node node2, DataFlowType contentType, Configuration config
) {
exists(Ap ap2, Content c |
store(node1, tc, node2, contentType) and
revFlowStore(ap2, c, ap1, node1, tc, node2, _, _, config) and
revFlowConsCand(ap2, c, ap1, config)
)
}
predicate revFlow(Node n, Configuration config) { revFlow(n, _, _, _, config) }
/* End: Stage 4 logic. */
}
@@ -2929,18 +2933,12 @@ private predicate pathReadStep(
cc = mid.getCallContext()
}
pragma[nomagic]
private predicate storeCand(Node node1, TypedContent tc, Node node2, Configuration config) {
storeCand2(node1, tc, node2, _, config) and
Stage4::revFlow(node2, config)
}
pragma[nomagic]
private predicate pathStoreStep(
PathNodeMid mid, Node node, AccessPath ap0, TypedContent tc, CallContext cc
) {
ap0 = mid.getAp() and
storeCand(mid.getNode(), tc, node, mid.getConfiguration()) and
Stage4::storeStepCand(mid.getNode(), _, tc, node, _, mid.getConfiguration()) and
cc = mid.getCallContext()
}