package codex

  1. Overview
  2. Docs
The Codex library for building static analysers based on abstract interpretation

Install 

dune-project
 Dependency

codex.top Edit opam file Versions (1)

Authors

  1. M
    Matthieu Lemerre
  2. J
    Julien Simonnet
  3. O
    Olivier Nicole
  4. P
    Paul Robert
  5. D
    Dorian Lesbre
  6. I
    Iker Canut
  7. C
    Corentin Gendreau
  8. G
    Guillaume Girol
  9. C
    Charles Babu
  10. J
    Jérôme Faucheux

Maintainers

  1. M
    Matthieu Lemerre <matthieu.lemerre@cea.fr>

Sources

1.0-rc4.tar.gz
md5=bc7266a140c6886add673ede90e335d3
sha512=8da42c0ff2c1098c5f9cb2b5b43b306faf7ac93b8f5ae00c176918cee761f249ff45b29309f31a05bbcf6312304f86a0d5a000eb3f1094d3d3c2b9b4c7f5c386

doc/codex.domains/Domains/Sig/index.html

Module Domains.SigSource

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

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