Shared: Define getNode inside cached module

This commit is contained in:
Simon Friis Vindum
2025-01-22 09:45:02 +01:00
parent 9a4bf7513d
commit e5f419ce75

View File

@@ -89,7 +89,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
BasicBlock getAPredecessor(SuccessorType t) { result.getASuccessor(t) = this }
/** Gets the control flow node at a specific (zero-indexed) position in this basic block. */
Node getNode(int pos) { bbIndex(this.getFirstNode(), result, pos) }
Node getNode(int pos) { result = getNode(this, pos) }
/** Gets a control flow node in this basic block. */
Node getANode() { result = this.getNode(_) }
@@ -308,10 +308,12 @@ module Make<LocationSig Location, InputSig<Location> Input> {
* Holds if `bbStart` is the first node in a basic block and `cfn` is the
* `i`th node in the same basic block.
*/
cached
predicate bbIndex(Node bbStart, Node cfn, int i) =
private predicate bbIndex(Node bbStart, Node cfn, int i) =
shortestDistances(startsBB/1, intraBBSucc/2)(bbStart, cfn, i)
cached
Node getNode(BasicBlock bb, int pos) { bbIndex(bb.getFirstNode(), result, pos) }
/**
* Holds if the first node of basic block `succ` is a control flow
* successor of the last node of basic block `pred`.