Module `Domains.Memory_sig`

Signature for the parts of memory domain.

The general idea is this. A memory maps adresses to values. Memories are built hierarchically: a part of a memory may be represented by another memory (e.g. whole memory can be parametrized by how memory is represented in each region, arrays can be parametrized by how memory is represented inside single cells, etc.). Ultimately, memories contain scalar /values/.

The fact that the value at the bottom of the hierarchy in the memory may contain parts of the adresses used at the top of the hierarchy requires a particular instantiation of functors. In general, a functor use the adresses of its parameter to build its own adresses. The adress of the top-level functor can be used as the value for the whole chain of functors, and is passed as an argument to build the memories.

So memory "domains" contains two parts: a part used to build adresses and the final value, which is passed as an argument to the second part, to build memories.

type 'a precision =

| Empty
| Singleton of 'a
| Imprecise

Used to distinguish cases for weak updates, strong updates, or completely invalid destinations.

module type AADT = sig ... end

An Abstract Abstract Datatype (AADT) is just a data structure that can contains symbolic values constrainted by a base domain, named Scalar.

module type WITH_BOOLEAN_REDEFINITION = sig ... end

For AADTs that redefine the notion of boolean.

module type AADT_WITH_BOOLEAN = sig ... end

module type VALUE = sig ... end

A scalar value stored inside a memory region. Should be a subset of Sig.MINIMAL + Sig.WITH_BINARY.

module type WITH_OFFSET = sig ... end

Abstraction of an offset in a contiguous memory region.

module type OFFSET = sig ... end

An AADT of offsets.

module type WITH_ADDRESS = sig ... end

Abstraction of an address, pointing to a region in a C-like memory model. The type adress is named binary for historical reasons, and also to help sharing with bitvectors in whole.

module type ADDRESS = sig ... end

Representation of pointers inside some memory regions.

module type WITH_MEMORY_QUERIES = sig ... end

module type WITH_FIXED_SIZE_VALUE = sig ... end

A fixed-size value is the type of values returned by C expressions or held in machine code registers, i.e. it is a bitvector containing an integer, pointer, floating point value, or contenation or extraction of other fixed-size values.

module type FIXED_SIZE_VALUE_DOMAIN = sig ... end

An abstract domain handling fixed-size values.

Base module types describing operations on terms of block types

module type BLOCK = sig ... end

module type MEMORY = sig ... end

Memory map adresses to values. These types may differ (for instance, an array functor can takes integer as adresses, but can contain any value).

Those are the canonical signatures of memory domains; however many domains provide a more specialized signature (with additional Context and type equalities, and sometimes also ask for more specialized signature (but that wil improve)

module type OFFSET_AND_MAKE_BLOCK = sig ... end

The idea is to match a BLOCK with the representation of an OFFSET within that BLOCK. But we delay the creation of the Block using a Make_Block functor, as the OFFSET can be used to create the VALUE that the BLOCK contains.

module type ADDRESS_AND_MAKE_MEMORY = sig ... end

The idea is to match a MEMORY with the representation of an ADDRESS referencing cells in that MEMORY. But we delay the creation of the MEMORY using a Make_Memory functor, as the ADDRESS can be used to create the VALUE and BLOCK that MEMORY cells contain.

module type WHOLE_MEMORY_DOMAIN = sig ... end

Like ADDRESS_AND_MAKE_MEMORY, but we can do bitvector operations on addresses. This module is not fully instantiated as module MEMORY still a functor waiting for parameter of module type BLOCK

module type COMPLETE_DOMAIN = sig ... end

This is a fully instantiated version of WHOLE_MEMORY_DOMAIN. It is used to break the recursion of the stack of recursive domains (containing uninitiated functors) in modules Codex_register and Dba2Codex

Base module types describing operations on one or several types of terms including memory ones

module type WITH_BLOCK_FORWARD = sig ... end

module type WITH_BLOCK = sig ... end

module type WITH_MEMORY_FORWARD = sig ... end

module type WITH_BLOCK_OFFSET = sig ... end

module type WITH_MEMORY = sig ... end

module type WITH_QUERIES = sig ... end

module type Base = sig ... end

Module Domains.Memory_sig

Base module types describing operations on terms of block types

Base module types describing operations on one or several types of terms including memory ones

Module `Domains.Memory_sig`