Module dialectic_compiler::flow[][src]

Control flow analysis for the session type CFG.

Structs

Dnf

A disjunction of conjunctions of constraints: true if any of the clauses contain constraints all of which are true.

FlowAnalysis

The output of a flow analysis is two sets: the “passable” set, indicating which nodes have a possible path “through” them to their continuation - and the “haltable” set, indicating which nodes can possibly be run all the way to Done.

Implication

An implication in normal form: a set of preconditions which prove a consequence.

Solver

The current state of the flow analysis solver.

Enums

Constraint

Flow analysis works by using a constraint solver: we try to solve for whether every node in the graph is “passable”, and in the process of doing so, we also solve “haltable” and “breaks from within some node or its children to some given parent loop node” constraints.

Validity

A result from breaking apart a DNF and attempting to determine whether it holds.

Functions

analyze

Analyze a CFG for passability of every contained node.

Type Definitions

Conjunction

A conjunction of constraints: true if all are true.