diff options
| -rw-r--r-- | src/ir/analysis.rs | 40 | ||||
| -rw-r--r-- | src/ir/named.rs | 60 |
2 files changed, 50 insertions, 50 deletions
diff --git a/src/ir/analysis.rs b/src/ir/analysis.rs index 28425a2c..e12f890f 100644 --- a/src/ir/analysis.rs +++ b/src/ir/analysis.rs @@ -1,4 +1,42 @@ -//! Fix-point analyses on the IR using the monotone framework. +//! Fix-point analyses on the IR using the "monotone framework". +//! +//! A lattice is a set with a partial ordering between elements, where there is +//! a single least upper bound and a single greatest least bound for every +//! subset. We are dealing with finite lattices, which means that it has a +//! finite number of elements, and it follows that there exists a single top and +//! a single bottom member of the lattice. For example, the power set of a +//! finite set forms a finite lattice where partial ordering is defined by set +//! inclusion, that is `a <= b` if `a` is a subset of `b`. Here is the finite +//! lattice constructed from the set {0,1,2}: +//! +//! ```text +//! .----- Top = {0,1,2} -----. +//! / | \ +//! / | \ +//! / | \ +//! {0,1} -------. {0,2} .--------- {1,2} +//! | \ / \ / | +//! | / \ | +//! | / \ / \ | +//! {0} --------' {1} `---------- {2} +//! \ | / +//! \ | / +//! \ | / +//! `------ Bottom = {} ------' +//! ``` +//! +//! A monotone function `f` is a function where if `x <= y`, then it holds that +//! `f(x) <= f(y)`. It should be clear that running a monotone function to a +//! fix-point on a finite lattice will always terminate: `f` can only "move" +//! along the lattice in a single direction, and therefore can only either find +//! a fix-point in the middle of the lattice or continue to the top or bottom +//! depending if it is ascending or descending the lattice respectively. +//! +//! For a deeper introduction to the general form of this kind of analysis, see +//! [Static Program Analysis by Anders Møller and Michael I. Schwartzbach][spa]. +//! +//! [spa]: https://cs.au.dk/~amoeller/spa/spa.pdf + use std::fmt; /// An analysis in the monotone framework. diff --git a/src/ir/named.rs b/src/ir/named.rs index 5351f309..6176faf1 100644 --- a/src/ir/named.rs +++ b/src/ir/named.rs @@ -75,56 +75,18 @@ //! union of its sub-item's used template parameters) and iterate to a //! fixed-point. //! -//! We use the "monotone framework" for this fix-point analysis where our -//! lattice is the mapping from each IR item to the powerset of the template -//! parameters that appear in the input C++ header, our join function is set -//! union, and we use the `ir::traversal::Trace` trait to implement the -//! work-list optimization so we don't have to revisit every node in the graph -//! when for every iteration towards the fix-point. +//! We use the `ir::analysis::MonotoneFramework` infrastructure for this +//! fix-point analysis, where our lattice is the mapping from each IR item to +//! the powerset of the template parameters that appear in the input C++ header, +//! our join function is set union. The set of template parameters appearing in +//! the program is finite, as is the number of IR items. We start at our +//! lattice's bottom element: every item mapping to an empty set of template +//! parameters. Our analysis only adds members to each item's set of used +//! template parameters, never removes them, so it is monotone. Because our +//! lattice is finite and our constraint function is monotone, iteration to a +//! fix-point will terminate. //! -//! A lattice is a set with a partial ordering between elements, where there is -//! a single least upper bound and a single greatest least bound for every -//! subset. We are dealing with finite lattices, which means that it has a -//! finite number of elements, and it follows that there exists a single top and -//! a single bottom member of the lattice. For example, the power set of a -//! finite set forms a finite lattice where partial ordering is defined by set -//! inclusion, that is `a <= b` if `a` is a subset of `b`. Here is the finite -//! lattice constructed from the set {0,1,2}: -//! -//! ```text -//! .----- Top = {0,1,2} -----. -//! / | \ -//! / | \ -//! / | \ -//! {0,1} -------. {0,2} .--------- {1,2} -//! | \ / \ / | -//! | / \ | -//! | / \ / \ | -//! {0} --------' {1} `---------- {2} -//! \ | / -//! \ | / -//! \ | / -//! `------ Bottom = {} ------' -//! ``` -//! -//! A monotone function `f` is a function where if `x <= y`, then it holds that -//! `f(x) <= f(y)`. It should be clear that running a monotone function to a -//! fix-point on a finite lattice will always terminate: `f` can only "move" -//! along the lattice in a single direction, and therefore can only either find -//! a fix-point in the middle of the lattice or continue to the top or bottom -//! depending if it is ascending or descending the lattice respectively. -//! -//! For our analysis, we are collecting the set of template parameters used by -//! any given IR node. The set of template parameters appearing in the program -//! is finite. Our lattice is their powerset. We start at the bottom element, -//! the empty set. Our analysis only adds members to the set of used template -//! parameters, never removes them, so it is monotone, and therefore iteration -//! to a fix-point will terminate. -//! -//! For a deeper introduction to the general form of this kind of analysis, see -//! [Static Program Analysis by Anders Møller and Michael I. Schwartzbach][spa]. -//! -//! [spa]: https://cs.au.dk/~amoeller/spa/spa.pdf +//! See `src/ir/analysis.rs` for more. use super::analysis::MonotoneFramework; use super::context::{BindgenContext, ItemId}; |