You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: docs/explanation/infrastructure.md
+34-4Lines changed: 34 additions & 4 deletions
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -204,8 +204,38 @@ The fixed point rewriter transforms a pass by iteratively applying the pass till
204
204
///
205
205
///
206
206
207
-
## Dataflow
208
-
`dataflow` defines a reusable forward dataflow analysis framework.
209
-
210
207
## Lattice
211
-
`lattice` defines ordering and merge semantics used by analysis states. Use `LatticeBase` to model the state domain, then use `ForwardDataflowAnalysis` to run transfer and merge over a graph. This keeps transfer logic in the analysis class and ordering logic in the lattice class.
208
+
209
+
The `Lattice` class in [`lattice.py`](../../src/oqd_compiler_infrastructure/lattice.py) defines a generic lattice interface with all the methods it requires. The following methods are defined:
210
+
- top(): Returns the top element of the lattice.
211
+
- bottom(): Returns the bottom element of the lattice.
212
+
- leq(): Returns True if `t1 <= t2` in the lattice.
213
+
- join(): Returns the least upper bound of `t1` and `t2`.
214
+
- meet(): Returns the greatest lower bound of `t1` and `t2`.
215
+
216
+
These methods allow analysis to be done on a concrete instance of the lattice.
217
+
218
+
The `LatticeBase` class defines a simple concrete implementation of a `Lattice`. It stores a dictionary that maps each node of the lattice to its immediate parent(s). It defines `LatticeTop` as the top element, and `LatticeBottom` as the bottom element of the lattice. This class defines the following helper methods:
219
+
- is_class_node(t): Returns True if `t` is a valid lattice node.
220
+
- add_node(t, parent): Adds a node to the lattice, by tracking the parent(s) of the node.
221
+
- atomic_ancestors(t): Returns the atomic ancestors of a given node.
222
+
223
+
These helper methods are used in the concrete implementation of the lattice operation methods: `leq`, `join`, and `meet`.
224
+
225
+
You can define your own lattice using the `LatticeBase` class.
226
+
227
+
## Dataflow
228
+
229
+
The `GraphProtocol` class in [`dataflow.py`](../../src/oqd_compiler_infrastructure/dataflow.py) defines a generic Graph Protocol interface that provides the nodes in the graph, the predecessors of a given node, and the successors of a given node. This protocol can be applied on any graph object for analysis: control flow graphs, dependency graphs, IR graphs, etc.
230
+
231
+
The `DataflowAnalysis` class requires a Lattice to implement the analysis on. This class provides a dataflow analysis framework that can be used to implement a specific dataflow analysis The following methods are defined:
232
+
- transfer(node, state_in): Returns the state of a given node after transfer.
233
+
- bottom(): Returns the default starting state for all nodes.
234
+
- merge(states): Joins incoming states using the lattice's join operation.
235
+
- states_equal(t1, t2): Returns True if two states are equal in the lattice.
236
+
237
+
The `ForwardDataflowAnalysis` class implements the forward dataflow analysis using the worklist algorithm with the `analyze` method. The output of the analysis is an instance of the `DataflowResult` class which contains the `in_states`, `out_states`, and the `iterations`.
238
+
239
+
The `MapForwardDataflowAnalysis` is a helper instance of `ForwardDataflowAnalysis` for states that use a `dict[str, LatticeType]` type for analysis.
0 commit comments