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.operator/Operator/index.html

Module OperatorSource

Operator defines the syntax and semantics of the expressions of the internal languages used by the Codex analyzers. It defines operations such as addition (on bitvectors or integers), logical/bitwise and (on booleans, integers and bitvectors), etc. In addition, it contains several utility modules (such as pretty-printers) for code dealing with these operators.

Most of our passes do not use a term representation of an AST, but instead calls "constructor functions" manipulating expressions, similarly to the Tagless-final of Carette, Kiselyov and Shan (2009). Thus, syntax means here that we define signatures (see Syntax: signature of operators) .

We do also provide a tag that can be used in an AST representation of the language (module Function_symbol).

We define a concrete semantics of these operators in module Concrete, which can be used to interpret constant terms.

Finally, Conversions contain helpers when doing domain transformations.

Unique identifiers

Sourcemodule Malloc_id : sig ... end

Unique identifier for malloc sites, which eventually includes all allocations in a C program. We also give string as a convenient name for these allocations.

Sourcemodule MakeId () : sig ... end

Generative functor to create unique ids.

Sourcemodule Condition : sig ... end

We want a choose operation on sets (which normally selects an arbitrary elements in a set) but we want to tell whether two distinct choose(S) operations selected the same element or not.

Sourcemodule Choice : sig ... end

Alarms

Sourcemodule Alarm : sig ... end

In the concrete, an alarm would correspond to an exception/panic due to a partial operator.

Sourcemodule Flags : sig ... end

Syntax: signature of operators

Sourcemodule Sig : sig ... end
include module type of struct include Sig end

This defines the syntax for the operators usable in the internal languages of Codex, expressed as signatures as in the Tagless final approach.

The signatures are grouped by type of values manipulated (boolean, integer, bitvector, binary, memory, enum). We define two set of functions: the forward are the normal operations, and the backward exclude the functions of arity 0 (for which a backward operation is meaningless).

Sourcetype access_type =
  1. | Read
    (*

    Loading from memory.

    *)
  2. | Write
    (*

    Storing into memory.

    *)
Sourcetype arith_type =
  1. | Plus
    (*

    Addition operation

    *)
  2. | Minus
    (*

    Substraction operation

    *)
Sourcemodule type ARITY = Sig.ARITY

Arity of function symbols. 'r represents the result type and 'a, 'b, 'c the arguments.

Sourcemodule Forward_Arity = Sig.Forward_Arity

Standard arities for forward transfer functions: given the arguments, return the results. These match the arities of the concrete functions they represent (but with concrete types substituted for their abstract counterparts).

Sourcemodule Backward_Arity = Sig.Backward_Arity

Standard arities for backward transfer functions (used to refined the arguments from information on the result values). These take the result value 'r as argument and return a new-improved value for each argument. They return None when no improvement is possible for that argument.

Note: in the following, we distinguish between backward and forward because there is no need to implement backward transfer functions for symbols with arity 0.

Boolean transfer functions

Transfer functions for boolean values: not, and (&&), or (||), as well as contants true_ and false_.

Sourcemodule type BOOLEAN_BACKWARD = Sig.BOOLEAN_BACKWARD
Sourcemodule type BOOLEAN_FORWARD = Sig.BOOLEAN_FORWARD

Integer transfer functions

Transfer functions for unbounded integers:

  • addition (iadd); subtraction (isub);
  • multiplication (imul, in general, itimes when multiplying by a constant);
  • division (idiv), remainder (imod);
  • comparisons (ieq for ==, ile for <=);
  • shifts (left ishl and right ishr)
  • bitwise operations (ior, iand, ixor).

For the bitwise operation, we assume an infinite two-complement representation: i.e. -1 is represented by an infinite sequence of 1, and 0 by an infinite sequence of 0.

Sourcemodule type INTEGER_BACKWARD = Sig.INTEGER_BACKWARD
Sourcemodule type INTEGER_FORWARD_MIN = Sig.INTEGER_FORWARD_MIN
Sourcemodule type INTEGER_FORWARD = Sig.INTEGER_FORWARD

Bitvector transfer functions

Purely numerical operations on fixed-size bitvectors. Includes bitwise operations and arithmetic, but not pointer arithmetic.

Note: the size argument is generally the size of both arguments and the result.

Sourcemodule type BITVECTOR_BACKWARD = Sig.BITVECTOR_BACKWARD
Sourcemodule type BITVECTOR_FORWARD = Sig.BITVECTOR_FORWARD
Sourcemodule type BITVECTOR_FORWARD_WITH_BIMUL_ADD = Sig.BITVECTOR_FORWARD_WITH_BIMUL_ADD

Binary transfer functions

Binary is the name of values handled by C or machine-level programs, i.e. either numeric bitvectors or pointers.

Sourcemodule type BINARY_BACKWARD = Sig.BINARY_BACKWARD
Sourcemodule type BINARY_FORWARD = Sig.BINARY_FORWARD
Sourcemodule type OFFSET_BACKWARD = Sig.OFFSET_BACKWARD
Sourcemodule type OFFSET_FORWARD = Sig.OFFSET_FORWARD
Sourcemodule type BLOCK_BACKWARD = Sig.BLOCK_BACKWARD
Sourcemodule type BLOCK_FORWARD = Sig.BLOCK_FORWARD

Enum transfer functions

Transfer function for enum values. Enums are types with a fixed (small) number of possible cases.

Sourcemodule type ENUM_BACKWARD = Sig.ENUM_BACKWARD
Sourcemodule type ENUM_FORWARD = Sig.ENUM_FORWARD

Memory transfer functions

Sourcemodule type MEMORY_BACKWARD = Sig.MEMORY_BACKWARD
Sourcemodule type MEMORY_FORWARD = Sig.MEMORY_FORWARD

Concrete (reference) implementation giving a meaning to operators

Sourcemodule Concrete : sig ... end

Concrete interpreter using OCaml boolean and Z.t for values.

Function symbols

Sourcemodule Function_symbol : sig ... end

Conversions

Sourcemodule Conversions : sig ... end

Functors to change arities of transfer functions signatures (i.e. replace ar0 with a new ar0). "Conversions"; i.e. passing the same transfer function (currently: with same types for dimension identifiers) with minimal changes.

Automatic logging

Similar to conversion, converts transfer functions to the same thing but that logs its call.

Sourcemodule Autolog : sig ... end

These functors allows automatic logging of transfer functions. You define how to handle functions of different arities, and how to print values of different types, and then you can automatically log transfer functions of a given signature (the functor names correspond to this signature).