Module `Domains.Sig`

exception 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).

exception Memory_Empty

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

module Log : Tracelog.S

module Quadrivalent = Lattices.Quadrivalent

module 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)

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

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

Forward transfer functions

module type With_Boolean_Forward = sig ... end

module type With_Integer_Forward = sig ... end

module type With_Binary_Forward = sig ... end

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

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.

module type Integer_Lattice = Lattices.Sig.INTEGER_LATTICE

module type Enum_Lattice = Lattices.Sig.ENUM_LATTICE

module type Binary_Lattice = Lattices.Sig.BITVECTOR_LATTICE

module type Integer_Query = sig ... end

module type WITH_QUERIES = sig ... end

module type With_Types = sig ... end

Other extensions

module type With_Partitionning = sig ... end

Context

module type With_Context = sig ... end

Guards

module type With_Assume = sig ... end

Fixpoint iteration

Fixpoint iteration, and base for all abstract domains.

module type With_Nondet = sig ... end

module Widening_Id : sig ... end

An integer uniquely identifying a widening point.

module type With_Fixpoint_Computation = sig ... end

module Fresh_id : sig ... end

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

module type With_Boolean = sig ... end

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

module type With_Integer = sig ... end

module type With_Binary = sig ... end

module type With_Enum = sig ... end

Complete instantiations

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

module type Minimal = sig ... end

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

module type BASE = sig ... end

module type Ext = sig ... end

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

module type BASE_WITH_INTEGER = sig ... end

Context conversions

module type Convert_Contexts = sig ... end

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

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

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

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

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

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

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

Module Domains.Sig