Documentation
¶
Overview ¶
Package dfa provides types and functions for implementing data-flow analyses.
Index ¶
- func BinaryTable[S comparable](default_ S, m map[[2]S]S) func(S, S) S
- func Dot[S comparable](fn Join[S], states []S, bottom, top S) string
- func MapCartesianProduct[S constraints.Integer](x, y S, fn func(S, S) S) S
- func MapSet[S constraints.Integer](set S, fn func(S) S) S
- func PowerSet[S constraints.Integer](all S) []S
- type Decision
- type Framework
- type Instance
- func (ins *Instance[S]) Decision(v ir.Value) Decision
- func (ins *Instance[S]) Forward(fn *ir.Function)
- func (ins *Instance[S]) Propagate(dst, src ir.Value, desc string) Mapping[S]
- func (ins *Instance[S]) Set(v ir.Value, d S)
- func (ins *Instance[S]) Transform(dst ir.Value, s S, src ir.Value, desc string) Mapping[S]
- func (ins *Instance[S]) Value(v ir.Value) S
- type Join
- type Mapping
Constants ¶
This section is empty.
Variables ¶
This section is empty.
Functions ¶
func BinaryTable ¶
func BinaryTable[S comparable](default_ S, m map[[2]S]S) func(S, S) S
BinaryTable returns a binary operator based on the provided mapping. For missing pairs of values, the default value will be returned.
func Dot ¶
func Dot[S comparable](fn Join[S], states []S, bottom, top S) string
Dot returns a directed graph in Graphviz format that represents the finite join-semilattice ⟨S, ≤⟩. Vertices represent elements in S and edges represent the ≤ relation between elements. We map from ⟨S, ∨⟩ to ⟨S, ≤⟩ by computing x ∨ y for all elements in [S]², where x ≤ y iff x ∨ y == y.
The resulting graph can be filtered through tred to compute the transitive reduction of the graph, the visualisation of which corresponds to the Hasse diagram of the semilattice.
The set of states should not include the ⊥ and ⊤ elements.
func MapCartesianProduct ¶
func MapCartesianProduct[S constraints.Integer](x, y S, fn func(S, S) S) S
func MapSet ¶
func MapSet[S constraints.Integer](set S, fn func(S) S) S
func PowerSet ¶
func PowerSet[S constraints.Integer](all S) []S
Types ¶
type Decision ¶
type Decision struct {
// The relevant values that the transfer function used to make the decision.
Inputs []ir.Value
// A human-readable description of the decision.
Description string
// Whether this is the source of an abstract state. For example, in a taint analysis, the call to a function that
// produces a tainted value would be the source of the taint state, and any instructions that operate on
// and propagate tainted values would not be sources.
Source bool
}
Decision describes how a mapping from an ir.Value to an abstract state came to be. Decisions are provided by transfer functions when they create mappings.
type Framework ¶
type Framework[S comparable] struct { Join Join[S] Transfer func(*Instance[S], ir.Instruction) []Mapping[S] Bottom S Top S }
Framework describes a monotone data-flow framework ⟨S, ∨, Transfer⟩ using a bounded join-semilattice ⟨S, ∨⟩ and a monotonic transfer function.
Transfer implements the transfer function. Given an instruction, it should return zero or more mappings from IR values to abstract values, i.e. values from the semilattice. Transfer must be monotonic. ϕ instructions are handled automatically and do not cause Transfer to be called.
The set S is defined implicitly by the values returned by Join and Transfer and needn't be finite. In addition, it contains the elements ⊥ and ⊤ (Bottom and Top) with Join(x, ⊥) = x and Join(x, ⊤) = ⊤. The provided Join function is wrapped to handle these elements automatically. All IR values start in the ⊥ state.
Abstract states are associated with IR values. As such, the analysis is sparse and favours the partitioned variable lattice (PVL) property.
func (*Framework[S]) Forward ¶
Forward runs an intraprocedural forward data flow analysis, using an iterative fixed-point algorithm, given the functions specified in the framework. It combines Framework.Start and Instance.Forward.
func (*Framework[S]) Start ¶
Start returns a new instance of the framework. See also Framework.Forward.
type Instance ¶
type Instance[S comparable] struct { Framework *Framework[S] // Mapping is the result of the analysis. Consider using Instance.Value instead of accessing Mapping // directly, as it correctly returns ⊥ for missing values. Mapping map[ir.Value]Mapping[S] }
Instance is an instance of a data-flow analysis. It is created by Framework.Forward.
func (*Instance[S]) Propagate ¶
Propagate is a helper for creating a Mapping that propagates the abstract state of src to dst. The desc parameter is used as the value of Decision.Description.
func (*Instance[S]) Set ¶
Set maps v to the abstract value d. It does not apply any checks. This should only be used before calling Instance.Forward, to set initial states of values.
type Join ¶
type Join[S comparable] func(S, S) S
Join defines the ∨ operation for a join-semilattice. It must implement a commutative and associative binary operation that returns the least upper bound of two states from S.
Code that calls Join functions is expected to handle the ⊥ and ⊤ elements, as well as implement idempotency. That is, the following properties will be enforced:
- x ∨ ⊥ = x
- x ∨ ⊤ = ⊤
- x ∨ x = x
Simple table-based join functions can be created using JoinTable.
func JoinTable ¶
func JoinTable[S comparable](top S, m map[[2]S]S) Join[S]
JoinTable returns a Join function based on the provided mapping. For missing pairs of values, the default value will be returned.
type Mapping ¶
type Mapping[S comparable] struct { Value ir.Value State S Decision Decision }
Mapping maps a single ir.Value to an abstract state.
func M ¶
func M[S comparable](v ir.Value, s S, d Decision) Mapping[S]
M is a helper for constructing instances of Mapping.
func Ms ¶
func Ms[S comparable](ms ...Mapping[S]) []Mapping[S]
Ms is a helper for constructing slices of mappings.
Example:
Ms(M(v1, d1, ...), M(v2, d2, ...))
Source Files