Module Make
Provides an SSA implementation.
The SSA construction is pruned based on liveness. That is, SSA definitions are only constructed for Input::variableWrites when it is possible to reach an Input::variableRead, without going through a certain write (the same goes for phi nodes). Whenever a variable is both read and written at the same index in some basic block, the read is assumed to happen before the write.
The result of invoking this parameterized module is not meant to be exposed directly; instead, one should define a language-specific layer on top, and make sure to cache all exposed predicates marked with
NB: If this predicate is exposed, it should be cached.Import path
Predicates
| adjacentUseUse | Holds if the certain read at index i1 in basic block bb1 reaches the certain read at index i2 in basic block bb2 without going through any other certain read. The boolean samevar indicates whether the two reads are of the same SSA variable. |
| firstUse | Holds if def reaches the certain read at index i in basic block bb without going through any other certain read. The boolean samevar indicates whether the read is a use of def or whether some number of phi nodes and/or uncertain reads occur between def and the read. |
| phiHasInputFromBlock | NB: If this predicate is exposed, it should be cached. |
| ssaDefReachesRead | NB: If this predicate is exposed, it should be cached. |
Classes
| Definition | A static single assignment (SSA) definition. |
| PhiNode | A phi node. |
| UncertainWriteDefinition | An SSA definition that represents an uncertain update of the underlying source variable. |
| WriteDefinition | An SSA definition that corresponds to a write. |
Modules
| Consistency | Provides a set of consistency queries. |
| DataFlowIntegration | Constructs the type Node and associated value step relations, which are intended to be included in the DataFlow::Node type and local step relations. |
| MakeSsa | |
| TestAdjacentRefs | Provides query predicates for testing adjacent SSA references and insertion of phi reads. |
Module signatures
| DataFlowIntegrationInputSig | Provides the input to DataFlowIntegration. |
| SsaInputSig |
Aliases
| ssaDefReachesEndOfBlock | NB: If this predicate is exposed, it should be cached. |
| uncertainWriteDefinitionInput | NB: If this predicate is exposed, it should be cached. |