Module Lattices.Sig

Signature for lattices, semi-lattices, and type-specific lattices.

Common lattice signatures

Minimal signature

module type JOIN_SEMI_LATTICE = sig ... end

A JOIN_SEMI_LATTICE is the minimal structure needed for abstract interpretation. It represents a mathematical join semi-lattice: i.e. a set (type t) with an inclusion order (includes : t -> t -> bool) that orders those values. The key operation is join : t -> t -> t, which merges information from two elements to form their least upper bound (an over-approximation of both).

Optional, standard, operations on lattices

module type WITH_INTER = sig ... end

Equips lattices with the ability to compute intersections: inter : t -> t -> t, also called meet, the greatest lower bound.

module type WITH_BOTTOM = sig ... end

Equips lattices with a bottom: t and test if the lattice element is a Bottom.

module type WITH_TOP = sig ... end

Equips lattices with a top: t.

module type JOIN_SEMI_LATTICE_WITH_BOTTOM = sig ... end

A join-semilattice with bottom.

module type JOIN_SEMI_LATTICE_WITH_INTER_BOTTOM = sig ... end

A join-semilattice with bottom and intersection.

Lattice with all operations

module type LATTICE = sig ... end

A mathematical lattice: join, meet, bottom, and top all available.

Type specific lattices

The lattices represent abstract set of common types (boolean, integers, bitvectors).

module type BOOLEAN_LATTICE = sig ... end

A boolean lattice: a LATTICE with elements representing truth values. Provides singleton to build from a concrete bool, and a conversion to the standard 4-element quadrivalent lattice.

module type INTEGER_LATTICE = sig ... end

a LATTICE for integers.

module type BITVECTOR_STANDARD_CONVERSIONS = sig ... end

This helps communicating information between lattices by converting to a common representation.

module type BITVECTOR_LATTICE_NO_CONVERSION = sig ... end

Bitvector Lattice: a LATTICE representing fixed sized bitvectors. The size isn't stored in the lattice, instead lattice operations take it as an extra argument.

module type BITVECTOR_QUERIES = sig ... end

module type BITVECTOR_LATTICE = sig ... end

A full bitvector lattice, combining core operations and queries. Also allows conversion to standard domains like known-bits or intervals.

module type ENUM_LATTICE = sig ... end

Enum Lattice: i.e. a LATTICE representing a set of enum values. Like BITVECTOR_LATTICE, they don't store the size in them. Thus, some functions take the size has argument.