package codex

  1. Overview
  2. Docs
package codex
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module LatticesSource

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.

Sourcemodule Unimplemented : sig ... end
Sourcemodule Quadrivalent : sig ... end

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

Sourcemodule Unit : sig ... end
Sourcemodule Prod : sig ... end

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

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

Sourcemodule BVSet : sig ... end

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

Sourcemodule 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.

Sourcemodule Signed_Interval : sig ... end

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

Sourcemodule Unsigned_Interval : sig ... end
Sourcemodule Integer : sig ... end
Sourcemodule Bitfield : sig ... end
Sourcemodule Bitvector_Of_Integer : sig ... end