Monotone_framework (stanc.Analysis_and_optimization.Monotone

val free_vars_expr : Middle.Expr.Typed.t -> string Std.Set.Poly.t

Calculate the free (non-bound) variables in an expression

val free_vars_idx : Middle.Expr.Typed.t Middle.Index.t -> string Std.Set.Poly.t

Calculate the free (non-bound) variables in an index

val free_vars_fnapp : 
  Middle.Expr.Typed.t Middle.Fun_kind.t ->
  Middle.Expr.Typed.t list ->
  string Std.Set.Poly.t

val free_vars_lval : 
  Middle.Expr.Typed.t Middle.Stmt.Pattern.lvalue ->
  string Std.Set.Poly.t

val free_vars_stmt : 
  (Middle.Expr.Typed.t, Middle.Stmt.Located.t) Middle.Stmt.Pattern.t ->
  string Std.Set.Poly.t

Calculate the free (non-bound) variables in a statement

val top_free_vars_stmt : 
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  (Middle.Expr.Typed.t, int) Middle.Stmt.Pattern.t ->
  string Std.Set.Poly.t

A variation on free_vars_stmt, where we do not recursively count free variables in sub statements

val inverse_flowgraph_of_stmt : 
  ?flatten_loops:??? ->
  ?blocks_after_body:??? ->
  Middle.Stmt.Located.t ->
  (module Monotone_framework_sigs.FLOWGRAPH
  with type labels = int)
  * Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t

Compute the inverse flowgraph of a Stan statement (for reverse analyses)

val reverse : 
  (module Monotone_framework_sigs.FLOWGRAPH with type labels = int) ->
  (module Monotone_framework_sigs.FLOWGRAPH
  with type labels = int)

Reverse flowgraphs to be used for reverse analyses. Observe that this respects the invariants listed for a FLOWGRAPH

val make_circular_flowgraph : 
  (module Monotone_framework_sigs.FLOWGRAPH with type labels = int) ->
  (module Monotone_framework_sigs.FLOWGRAPH with type labels = int) ->
  (module Monotone_framework_sigs.FLOWGRAPH
  with type labels = int)

Modify the end nodes of a flowgraph to depend on its inits To force the monotone framework to run until the program never changes this function modifies the input Flowgraph so that it's end nodes depend on it's initial nodes. The inits of the reverse flowgraph are used for this since we normally have both the forward and reverse flowgraphs available.

parameter l
Type of the label for each flowgraph, most commonly an int

parameter Flowgraph
The flowgraph to modify

parameter RevFlowgraph
The same flowgraph as Flowgraph but reversed.

val forward_flowgraph_of_stmt : 
  ?flatten_loops:??? ->
  ?blocks_after_body:??? ->
  Middle.Stmt.Located.t ->
  (module Monotone_framework_sigs.FLOWGRAPH
  with type labels = int)
  * Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t

Compute the forward flowgraph of a Stan statement (for forward analyses)

val powerset_lattice : 
  (module Monotone_framework_sigs.INITIALTYPE with type vals = 'v) ->
  (module Monotone_framework_sigs.LATTICE
  with type properties = 'v Std.Set.Poly.t)

The lattice of sets of some values, with the inclusion order, set union and the empty set

val dual_powerset_lattice : 
  (module Monotone_framework_sigs.INITIALTOTALTYPE with type vals = 'v) ->
  (module Monotone_framework_sigs.LATTICE
  with type properties = 'v Std.Set.Poly.t)

The lattice of subsets of some set, with the inverse inclusion order, set intersection and the total set

val powerset_lattice_expressions : 
  Dataflow_types.ExprSet.t ->
  (module Monotone_framework_sigs.LATTICE
  with type properties = Dataflow_types.ExprSet.t)

val dual_powerset_lattice_expressions : 
  Dataflow_types.ExprSet.t ->
  Dataflow_types.ExprSet.t ->
  (module Monotone_framework_sigs.LATTICE
  with type properties = Dataflow_types.ExprSet.t)

val new_bot : 
  (module Monotone_framework_sigs.LATTICE_NO_BOT with type properties = 'p) ->
  (module Monotone_framework_sigs.LATTICE
  with type properties = 'p option)

Add a fresh bottom element to a lattice (possibly without bottom)

val dual_partial_function_lattice : 
  (module Monotone_framework_sigs.TOTALTYPE with type vals = string) ->
  (module Monotone_framework_sigs.TYPE with type vals = 'cv) ->
  (module Monotone_framework_sigs.LATTICE_NO_BOT
  with type properties = 'cv Std.String.Map.t)

The lattice (without bottom) of partial functions, ordered under inverse graph inclusion, with intersection

val dual_partial_function_lattice_with_bot : 
  (module Monotone_framework_sigs.TOTALTYPE with type vals = string) ->
  (module Codom : Monotone_framework_sigs.TYPE
  with type vals = 'cv)
  ->
  (module Monotone_framework_sigs.LATTICE
  with type properties = Codom.vals Std.String.Map.t option)

The lattice of partial functions, where we add a fresh bottom element, to represent an inconsistent combination of functions

val dual_powerset_lattice_empty_initial : 
  (module T : Monotone_framework_sigs.TOTALTYPE
  with type vals = 'v)
  ->
  (module Monotone_framework_sigs.LATTICE
  with type properties = T.vals Std.Set.Poly.t)

A dual powerset lattice, where we set the initial set to be empty

val powerset_lattice_empty_initial : 
  (module T : Monotone_framework_sigs.TYPE
  with type vals = 'v)
  ->
  (module Monotone_framework_sigs.LATTICE
  with type properties = T.vals Std.Set.Poly.t)

A powerset lattice, where we set the initial set to be empty

val reaching_definitions_lattice : 
  (module Variables : Monotone_framework_sigs.INITIALTYPE
  with type vals = 'v)
  ->
  (module Labels : Monotone_framework_sigs.TYPE
  with type vals = 'l)
  ->
  (module Monotone_framework_sigs.LATTICE
  with type properties = (Variables.vals * Labels.vals option) Std.Set.Poly.t)

The specific powerset lattice we use for reaching definitions analysis

val minimal_variables_lattice : 
  string Std.Set.Poly.t ->
  (module Monotone_framework_sigs.LATTICE
  with type properties = string Std.Set.Poly.t)

Lattice for finding the smallest set that satisfies some criterion

val constant_propagation_transfer : 
  ?preserve_stability:??? ->
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  (module Monotone_framework_sigs.TRANSFER_FUNCTION
  with type labels = int
   and type properties = Middle.Expr.Typed.t Std.String.Map.t option)

val label_top_decls : 
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  Dataflow_types.LabelMap.key ->
  string Std.Set.Poly.t

val expression_propagation_transfer : 
  ?preserve_stability:??? ->
  (Middle.Expr.Typed.t -> bool) ->
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  (module Monotone_framework_sigs.TRANSFER_FUNCTION
  with type labels = int
   and type properties = Middle.Expr.Typed.t Std.String.Map.t option)

The transfer function for an expression propagation analysis, AKA forward substitution (see page 396 of Muchnick)

val copy_propagation_transfer : 
  string Std.Set.Poly.t ->
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  (module Monotone_framework_sigs.TRANSFER_FUNCTION
  with type labels = int
   and type properties = Middle.Expr.Typed.t Std.String.Map.t option)

The transfer function for a copy propagation analysis

val transfer_gen_kill : 
  'a Std.Set.Poly.t ->
  'a Std.Set.Poly.t ->
  'a Std.Set.Poly.t ->
  'a Std.Set.Poly.t

A helper function for building transfer functions from gen and kill sets

val assigned_vars_stmt : 
  (Middle.Expr.Typed.t, 'a) Middle.Stmt.Pattern.t ->
  string Std.Set.Poly.t

Calculate the set of variables that a statement can assign to

val declared_vars_stmt : 
  (Middle.Expr.Typed.t, 'a) Middle.Stmt.Pattern.t ->
  string Std.Set.Poly.t

Calculate the set of variables that a statement can declare

val assigned_or_declared_vars_stmt : 
  (Middle.Expr.Typed.t, 'a) Middle.Stmt.Pattern.t ->
  string Std.Set.Poly.t

Calculate the set of variables that a statement can assign to or declare

val reaching_definitions_transfer : 
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  (module Monotone_framework_sigs.TRANSFER_FUNCTION
  with type labels = int
   and type properties = (string * int option) Std.Set.Poly.t)

The transfer function for a reaching definitions analysis

val initialized_vars_transfer : 
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  (module Monotone_framework_sigs.TRANSFER_FUNCTION
  with type labels = int
   and type properties = string Std.Set.Poly.t)

The transfer function for an initialized variables analysis

val live_variables_transfer : 
  string Std.Set.Poly.t ->
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  (module Monotone_framework_sigs.TRANSFER_FUNCTION
  with type labels = int
   and type properties = string Std.Set.Poly.t)

The transfer function for a live variables analysis

val used_subexpressions_expr : Middle.Expr.Typed.t -> Dataflow_types.ExprSet.t

Calculate the set of sub-expressions of an expression

val used_expressions_idx_help : 
  (Middle.Expr.Typed.t -> Dataflow_types.ExprSet.t) ->
  Middle.Expr.Typed.t Middle.Index.t ->
  Dataflow_types.ExprSet.t

val used_expressions_lval : 
  (Middle.Expr.Typed.t -> Dataflow_types.ExprSet.t) ->
  Middle.Expr.Typed.t Middle.Stmt.Pattern.lvalue ->
  Dataflow_types.ExprSet.t

val used_expressions_expr : 
  Dataflow_types.ExprSet.elt ->
  Dataflow_types.ExprSet.t

Calculate the set of expressions of an expression

val used_expressions_stmt_help : 
  (Middle.Expr.Typed.t -> Dataflow_types.ExprSet.t) ->
  (Middle.Expr.Typed.t, Middle.Stmt.Located.t) Middle.Stmt.Pattern.t ->
  Dataflow_types.ExprSet.t

val used_subexpressions_stmt : 
  (Middle.Expr.Typed.t, Middle.Stmt.Located.t) Middle.Stmt.Pattern.t ->
  Dataflow_types.ExprSet.t

Calculate the set of sub-expressions in a statement

val used_expressions_stmt : 
  (Middle.Expr.Typed.t, Middle.Stmt.Located.t) Middle.Stmt.Pattern.t ->
  Dataflow_types.ExprSet.t

Calculate the set of expressions in a statement

val top_used_expressions_stmt_help : 
  (Middle.Expr.Typed.t -> Dataflow_types.ExprSet.t) ->
  (Middle.Expr.Typed.t, int) Middle.Stmt.Pattern.t ->
  Dataflow_types.ExprSet.t

val top_used_subexpressions_stmt : 
  (Middle.Expr.Typed.t, int) Middle.Stmt.Pattern.t ->
  Dataflow_types.ExprSet.t

Calculate the set of sub-expressions at the top level in a statement

val top_used_expressions_stmt : 
  (Middle.Expr.Typed.t, int) Middle.Stmt.Pattern.t ->
  Dataflow_types.ExprSet.t

Calculate the set of expressions at the top level in a statement

val killed_expressions_stmt : 
  Dataflow_types.ExprSet.t ->
  (Middle.Expr.Typed.t, int) Middle.Stmt.Pattern.t ->
  Dataflow_types.ExprSet.t

Calculate the subset (of p) of expressions that will need to be recomputed as a consequence of evaluating the statement s (because of writes to variables performed by s)

val used : 
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  Dataflow_types.ExprSet.t Dataflow_types.LabelMap.t

Calculate the set of subexpressions that needs to be computed at each node in the flowgraph

val anticipated_expressions_transfer : 
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  Dataflow_types.ExprSet.t Dataflow_types.LabelMap.t ->
  (module Monotone_framework_sigs.TRANSFER_FUNCTION
  with type labels = int
   and type properties = Dataflow_types.ExprSet.t)

The transfer function for an anticipated expressions analysis (as a part of lazy code motion)

val transfer_gen_kill_alt : 
  Dataflow_types.ExprSet.t ->
  Dataflow_types.ExprSet.t ->
  Dataflow_types.ExprSet.t ->
  Dataflow_types.ExprSet.t

A helper function for defining transfer functions in terms of gen and kill sets in an alternative way, that is used in some of the subanalyses of lazy code motion

val available_expressions_transfer : 
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  Dataflow_types.ExprSet.t Monotone_framework_sigs.entry_exit
    Dataflow_types.LabelMap.t ->
  (module Monotone_framework_sigs.TRANSFER_FUNCTION
  with type labels = int
   and type properties = Dataflow_types.ExprSet.t)

An available expressions analysis, to be used in lazy code motion

val earliest : 
  Dataflow_types.ExprSet.t Monotone_framework_sigs.entry_exit
    Dataflow_types.LabelMap.t ->
  Dataflow_types.ExprSet.t Monotone_framework_sigs.entry_exit
    Dataflow_types.LabelMap.t ->
  Dataflow_types.ExprSet.t Dataflow_types.LabelMap.t

Calculates the set of expressions that can be calculated for the first time at each node in the flow graph

val postponable_expressions_transfer : 
  Dataflow_types.ExprSet.t Dataflow_types.LabelMap.t ->
  Dataflow_types.ExprSet.t Dataflow_types.LabelMap.t ->
  (module Monotone_framework_sigs.TRANSFER_FUNCTION
  with type labels = int
   and type properties = Dataflow_types.ExprSet.t)

The transfer function for a postponable expressions analysis (as a part of lazy code motion)

val latest : 
  int Std.Set.Poly.t Dataflow_types.LabelMap.t ->
  Dataflow_types.ExprSet.t Dataflow_types.LabelMap.t ->
  Dataflow_types.ExprSet.t Monotone_framework_sigs.entry_exit
    Dataflow_types.LabelMap.t ->
  Dataflow_types.ExprSet.t Dataflow_types.LabelMap.t ->
  Dataflow_types.ExprSet.t Dataflow_types.LabelMap.t

Calculates the set of expressions that can be computed at the latest at each node

val used_not_latest_expressions_transfer : 
  Dataflow_types.ExprSet.t Dataflow_types.LabelMap.t ->
  Dataflow_types.ExprSet.t Dataflow_types.LabelMap.t ->
  (module Monotone_framework_sigs.TRANSFER_FUNCTION
  with type labels = int
   and type properties = Dataflow_types.ExprSet.t)

The transfer function for a used-not-latest expressions analysis, as a part of lazy code motion

val minimal_variables_fwd_transfer : 
  (Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
    int ->
    string Std.Set.Poly.t ->
    string Std.Set.Poly.t) ->
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  (module Monotone_framework_sigs.TRANSFER_FUNCTION
  with type labels = int
   and type properties = string Std.Set.Poly.t)

The transfer function for the first forward analysis part of determining optimal ad-levels for variables

val monotone_framework : 
  (module Monotone_framework_sigs.FLOWGRAPH with type labels = int) ->
  (module Monotone_framework_sigs.LATTICE with type properties = 'p) ->
  (module Monotone_framework_sigs.TRANSFER_FUNCTION
    with type labels = int
     and type properties = 'p) ->
  (module Monotone_framework_sigs.MONOTONE_FRAMEWORK
  with type properties = 'p)

The central definition of a monotone dataflow analysis framework. Given a compatible flowgraph, lattice and transfer function, we can run the mfp (maximal fixed point) algorithm, which computes a maximal fixed point (MFP) for the set of equations/inequalities of properties at the entry and exit of each node in the flow graph, as defined by the triple. Note that this gives a safe approximation to the MOP (meet over all paths) solution that we would really be interested in, but which is often incomputable. In case of a distributive lattice of properties, the MFP and MOP solutions coincide.

val declared_variables_stmt : 
  (Middle.Expr.Typed.t, Middle.Stmt.Located.t) Middle.Stmt.Pattern.t ->
  string Std.Set.Poly.t

val propagation_mfp : 
  Middle.Program.Typed.t ->
  (module Monotone_framework_sigs.FLOWGRAPH with type labels = int) ->
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  (Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
    (module Monotone_framework_sigs.TRANSFER_FUNCTION
    with type labels = int
     and type properties = Middle.Expr.Typed.t Std.String.Map.t option)) ->
  Middle.Expr.Typed.t Std.String.Map.t option
    Analysis_and_optimization__Monotone_framework_sigs.entry_exit
    Dataflow_types.LabelMap.t

val reaching_definitions_mfp : 
  Middle.Program.Typed.t ->
  (module Monotone_framework_sigs.FLOWGRAPH with type labels = int) ->
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  (string * int option) Std.Set.Poly.t
    Analysis_and_optimization__Monotone_framework_sigs.entry_exit
    Dataflow_types.LabelMap.t

val initialized_vars_mfp : 
  string Std.Set.Poly.t ->
  (module Monotone_framework_sigs.FLOWGRAPH with type labels = int) ->
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  string Std.Set.Poly.t
    Analysis_and_optimization__Monotone_framework_sigs.entry_exit
    Dataflow_types.LabelMap.t

val globals : Middle.Program.Typed.t -> string Std.Set.Poly.t

val live_variables_mfp : 
  Middle.Program.Typed.t ->
  (module Monotone_framework_sigs.FLOWGRAPH with type labels = int) ->
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  string Std.Set.Poly.t
    Analysis_and_optimization__Monotone_framework_sigs.entry_exit
    Dataflow_types.LabelMap.t

Monotone framework instance for live_variables analysis. Expects reverse flowgraph.

val lazy_expressions_mfp : 
  (module Monotone_framework_sigs.FLOWGRAPH with type labels = int) ->
  (module Monotone_framework_sigs.FLOWGRAPH with type labels = int) ->
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  Dataflow_types.ExprSet.t Dataflow_types.LabelMap.t
  * Dataflow_types.ExprSet.t
      Analysis_and_optimization__Monotone_framework_sigs.entry_exit
      Dataflow_types.LabelMap.t

Instantiate all four instances of the monotone framework for lazy code motion, reusing code between them

val minimal_variables_mfp : 
  (module Monotone_framework_sigs.FLOWGRAPH with type labels = int) ->
  Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
  string Std.Set.Poly.t ->
  (Middle.Stmt.Located.Non_recursive.t Dataflow_types.LabelMap.t ->
    int ->
    string Std.Set.Poly.t ->
    string Std.Set.Poly.t) ->
  string Std.Set.Poly.t
    Analysis_and_optimization__Monotone_framework_sigs.entry_exit
    Dataflow_types.LabelMap.t

Run the minimal fixed point algorithm to deduce the smallest set of variables that satisfy a set of conditions.

parameter Flowgraph
The set of nodes to analyze

parameter flowgraph_to_mir
Map of nodes to their actual values in the MIR

parameter initial_variables
The set of variables to start in the set

parameter gen_variable
Used in the transfer function to deduce variables that should be in the set