Module Lattices

Our primary way of exchanging and information about the program is using lattices. Lattices should be the abstraction of a set of something (its concretization).

Note that many operations operate over several lattices (notably, transfer functions) are defined in the Single_value_abstraction module. Lattices operation defined here should be concerned only with a single lattice.

TODO: This is probably what we should be exporting for later display.

module Sig : sig ... end

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

module Unimplemented : sig ... end

module Quadrivalent : sig ... end

The quadrivalent lattice for booleans, with four elements: Bottom, True, False, and Top.

module Unit : sig ... end

module Prod : sig ... end

Product lattice is a lattice that pairs two (or more) component lattices

module Known_Bits : Sig.BITVECTOR_LATTICE with type t = Z.t * Z.t

A bitvector lattice based on “known bits”: tracks which bits are definitely 0 or definitely 1, leaving others unknown.

module BVSet : sig ... end

A lattice of finite sets of bitvectors. Best for small domains where explicit enumeration is feasible.

module Congruence : sig ... end

The congruence lattice: abstracts integers by modular constraints of the form x ≡ a (mod n). Captures properties like even/odd or divisibility.

module Signed_Interval : sig ... end

Signed interval lattice: represents ranges of integers with signed semantics (e.g. -10, 42)

module Unsigned_Interval : sig ... end

module Integer : sig ... end

module Bitfield : sig ... end

module Bitvector_Of_Integer : sig ... end