Module Analysis_and_optimization.Monotone_framework_sigs

The API for a monotone framework, as described in 2.3-2.4 of Nielson, Nielson, and Hankin or 9.3 of Aho et al.. This gives a modular way of implementing many static analyses.

module type FLOWGRAPH = sig ... end

The API for a flowgraph, needed for the mfp algorithm in the monotone framework. Assumed invariants: successors contains all graph nodes as keys initials is a subset of the graph nodes

module type TYPE = sig ... end

The minimal data we need to use a type in forming a lattice of various kinds

module type INITIALTYPE = sig ... end

The data we need to form a powerset lattice

module type TOTALTYPE = sig ... end

The data we need to form e.g. an available xpressions lattice

module type INITIALTOTALTYPE = sig ... end

The data we need to form a dual powerset lattice

module type LATTICE_NO_BOT = sig ... end
module type LATTICE = sig ... end

The API for a complete (possibly non-distributive) lattice, needed for the mfp algorithm in the monotone framework

module type TRANSFER_FUNCTION = sig ... end

The API for a transfer function, needed for the mfp algorithm in the monotone framework. This describes how output properties are computed from input properties at a given node in the flow graph.

type 'a entry_exit = {
  1. entry : 'a;
  2. exit : 'a;
}
module type MONOTONE_FRAMEWORK = sig ... end

The API for a monotone framework. mfp computes the minimal fixed point of the equations/inequalities defined between property lattice elements at the entry and exit of different flowgraph nodes, where these equations/inequalities are generated from the transfer function. Returns a map of the (input_properties, output_properties) for each node l in the flow graph. The analysis performed is always a forward analysis. For a reverse analysis, supply the reverse flow graph.