SSA: Add an alternative to ssaDefAssigns/ssaDefInitializesParam.

This commit is contained in:
Anders Schack-Mulligen
2025-03-27 11:35:38 +01:00
parent 0c74f21107
commit 1ded4df3fd

View File

@@ -1459,6 +1459,15 @@ module Make<LocationSig Location, InputSig<Location> Input> {
)
}
/**
* Holds if `def` has some form of input flow. For example, the right-hand
* side of an assignment or a parameter of an SSA entry definition.
*
* For such definitions, a flow step is added from a synthetic node
* representing the source to the definition.
*/
default predicate ssaDefHasSource(WriteDefinition def) { any() }
/** Holds if SSA definition `def` assigns `value` to the underlying variable. */
predicate ssaDefAssigns(WriteDefinition def, Expr value);
@@ -1665,6 +1674,7 @@ module Make<LocationSig Location, InputSig<Location> Input> {
cached
private newtype TNode =
TWriteDefSource(WriteDefinition def) { DfInput::ssaDefHasSource(def) } or
TParamNode(DfInput::Parameter p) {
exists(WriteDefinition def | DfInput::ssaDefInitializesParam(def, p))
} or
@@ -1696,6 +1706,22 @@ module Make<LocationSig Location, InputSig<Location> Input> {
final class Node = NodeImpl;
/** A source of a write definition. */
private class WriteDefSourceNodeImpl extends NodeImpl, TWriteDefSource {
private WriteDefinition def;
WriteDefSourceNodeImpl() { this = TWriteDefSource(def) }
/** Gets the underlying definition. */
WriteDefinition getDefinition() { result = def }
override string toString() { result = def.toString() }
override Location getLocation() { result = def.getLocation() }
}
final class WriteDefSourceNode = WriteDefSourceNodeImpl;
/** A parameter node. */
private class ParameterNodeImpl extends NodeImpl, TParamNode {
private DfInput::Parameter p;
@@ -1976,6 +2002,9 @@ module Make<LocationSig Location, InputSig<Location> Input> {
*/
predicate localFlowStep(SourceVariable v, Node nodeFrom, Node nodeTo, boolean isUseStep) {
exists(Definition def |
// Flow from write definition source into SSA definition
nodeFrom = TWriteDefSource(def)
or
// Flow from assignment into SSA definition
DfInput::ssaDefAssigns(def, nodeFrom.(ExprNode).getExpr())
or
@@ -2012,6 +2041,9 @@ module Make<LocationSig Location, InputSig<Location> Input> {
/** Holds if the value of `nodeTo` is given by `nodeFrom`. */
predicate localMustFlowStep(SourceVariable v, Node nodeFrom, Node nodeTo) {
exists(Definition def |
// Flow from write definition source into SSA definition
nodeFrom = TWriteDefSource(def)
or
// Flow from assignment into SSA definition
DfInput::ssaDefAssigns(def, nodeFrom.(ExprNode).getExpr())
or