Sig (p.codex.1.0~rc4.doc.codex.domains.Domains.Sig)

Sourceexception Bottom

The Bottom exception can be raised by any transfer function that realises the state is empty. This should mainly be WithAssume.assume, but it can also forward transfer function (for instance, division by zero).

Sourceexception Memory_Empty

Raised e.g. when storing to an invalid location.

Sourcemodule Log : Tracelog.S

Sourcemodule Quadrivalent = Lattices.Quadrivalent

Sourcemodule type Context = sig ... end

A Context represent a set of paths leading to the current state (it corresponds to a path condition in symbolic execution)

Sourcemodule Context_Arity_Forward (Context : Context) : sig ... end

Sourcemodule Monadic_Context (Context : Context) : sig ... end

Forward transfer functions

Sourcemodule type With_Boolean_Forward = sig ... end

Sourcemodule type With_Integer_Forward = sig ... end

Sourcemodule type With_Binary_Forward = sig ... end

Sourcemodule type With_Enum_Forward = sig ... end

Queries

Queries allow to ask the domain an overapproximation of the set of concrete objects to which a dimension concretizes. This set of object must be finitely represented, but the choice of this representation is left to the domain. It is required that these objects can be converted to some standard representations.

In addition, we require this set of object to be represented by a lattice, so that it is possible to test inclusion and perform approximation of union on these set of objects.

Source

module type Boolean_Lattice =
  Lattices.Sig.BOOLEAN_LATTICE with type t = Lattices.Quadrivalent.t

Note: since Lattices.Quadrivalent exactly represents the powerset of {true,false}, there is no point in using another type.

Sourcemodule type Integer_Lattice = Lattices.Sig.INTEGER_LATTICE

Sourcemodule type Enum_Lattice = Lattices.Sig.ENUM_LATTICE

Sourcemodule type Binary_Lattice = Lattices.Sig.BITVECTOR_LATTICE

Sourcemodule type Integer_Query = sig ... end

Sourcemodule type WITH_QUERIES = sig ... end

Sourcemodule type With_Types = sig ... end

Other extensions

Sourcemodule type With_Partitionning = sig ... end

Context

Sourcemodule type With_Context = sig ... end

Guards

Sourcemodule type With_Assume = sig ... end

Fixpoint iteration

Fixpoint iteration, and base for all abstract domains.

Sourcemodule type With_Nondet = sig ... end

Sourcemodule Widening_Id : sig ... end

An integer uniquely identifying a widening point.

Sourcemodule type With_Fixpoint_Computation = sig ... end

Sourcemodule Fresh_id : sig ... end

Sourcemodule type With_Id = sig ... end

Identifying domains.

Optional types that can be used in the domain

BASE module types describing operations on one or several types of terms.

Notes on the base operations:

Pretty is required everywhere, and used for debugging.

Equality refers to equality of the concretization. It can be approximate, i.e. it is ok to return false when we cannot detect that elements are equal; however when used as keys of datastructures, equality should probably at least return true for elements that are (==).

TODO: Do compare and hash have to respect equality? Map and Set do not need "equal", but Hashtbl does. So it seems that at least hash should respect equality, i.e. equal elements should have the same hash; which is not obvious when structurally different elements are detected as equal (e.g. different representations of empty). Or maybe it does not need, but in this case it is undefined whether different abstract values with same concretization represent different binding in the table (if by chance the hash is the same, they will share a binding; else they may have different bindings).

compare and hash do not need to be implemented if the datastructures are not used.

Sourcemodule type With_Boolean = sig ... end

We document the boolean cases, as integer are pretty similar.

Sourcemodule type With_Integer = sig ... end

Sourcemodule type With_Binary = sig ... end

Sourcemodule type With_Enum = sig ... end

Complete instantiations

Sourcemodule type Minimal_No_Boolean = sig ... end

This signature is useful when we don't have any new flow-sensitive state and just need all the things on the top of the stack to stay the same.

Sourcemodule type Minimal = sig ... end

This signature does not have pre-built values, except booleans.

Sourcemodule type BASE = sig ... end

Sourcemodule type Ext = sig ... end

These are functions that can be implemented using the base signatures. See Domain_extend for instantiation.

Sourcemodule type BASE_WITH_INTEGER = sig ... end

Context conversions

Sourcemodule type Convert_Contexts = sig ... end

Context conversion procedures: pass through the values by just changing the context.

Sourcemodule Make_Convert (C : Convert_Contexts) : sig ... end

Source

module Convert_Boolean_Forward
  (C : Convert_Contexts)
  (D : With_Boolean_Forward with module Context = C.To) : 
  sig ... end

Source

module Convert_Integer_Forward
  (C : Convert_Contexts)
  (D : With_Integer_Forward with module Context = C.To) : 
  sig ... end

Source

module Convert_Binary_Forward
  (C : Convert_Contexts)
  (D : With_Binary_Forward with module Context = C.To) : 
  sig ... end

Source

module Convert_Enum_Forward
  (C : Convert_Contexts)
  (D : With_Enum_Forward with module Context = C.To) : 
  sig ... end

Sourcemodule Convert_to_monadic (D : BASE) : sig ... end

This will help to the transition in a top-down manner, starting from the translation and top-level domain to the lower-level domain.