package mopsa

  1. Overview
  2. Docs
MOPSA: A Modular and Open Platform for Static Analysis using Abstract Interpretation

Install 

dune-project
 Dependency

gitlab.com Readme Changelog Edit opam file Versions (3)

Authors

  1. A
    Antoine Miné
  2. A
    Abdelraouf Ouadjaout
  3. M
    Matthieu Journault
  4. A
    Aymeric Fromherz
  5. R
    Raphaël Monat
  6. F
    Francesco Parolini
  7. M
    Marco Milanese
  8. J
    Jérôme Boillot

Maintainers

  1. A
    Antoine Miné <antoine.mine@lip6.fr>
  2. A
    Abdelraouf Ouadjaout <ouadjaout@gmail.com>
  3. R
    Raphaël Monat <raphael.monat@inria.fr>

Sources

mopsa-analyzer-v1.0.tar.gz
md5=9f673f79708b44a7effb3b6bb3618d2c
sha512=cb91cb428e43a22f1abbcb8219710d0c10a5b3756d0da392d4084b3b3a6157350776c596983e63def344f617d39964e91f244f60c07958695ee5c8c809a9f0f4

doc/core/Core/Context/index.html

Module Core.ContextSource

Context - Storage for flow-insensitive information

The context is a heterogeneous key-value map that stores non-semantical information, such as a description of the program being currently analyzed, the callstack, etc.

For instance, to create a new kind of entries for storing strings, first generate a new context key:

  module K = GenContextKey
      (struct
        type 'a t = string
        let print pp fmt s = fprintf fmt "string: %s" s
      end)
  let string_key = K.key

Then, given a context 'a ctx, you can add/remove elements as follows:

  let ctx'  = add_ctx string_key "a" ctx in
  let ctx'' = remove_ctx string_key ctx'

Note that the context can contain the abstract state. For instance, to store a cache of input/output states for each function, you can do:

  module K = GenContextKey
      (struct
        type 'a t = (string*'a flow*'a post) list
        let print pp fmt cache =
          fprintf fmt "functions I/O cache:@,  @[<v>%a@]"
            (pp_print_list
              ~pp_sep:(fun fmt () -> fprintf fmt "@,")
              (fun (f,input,output) ->
                 fprintf "%s:@, input:@[%a]@, output:@[%a@]"
                   f
                   (Flow.print pp) input
                   (Post.print pp) output
              )
            ) cache
      end)
  let cache_key = K.key
Sourcetype ('a, _) ctx_key = ..

Key to access an element in the context

Sourcetype 'a ctx

The context

Sourceval empty_ctx : 'a ctx

Empty context

Sourceval singleton_ctx : ('a, 'v) ctx_key -> 'v -> 'a ctx

Context with one element

Sourceval mem_ctx : ('a, 'v) ctx_key -> 'a ctx -> bool

mem_ctx k ctx returns true when an element at key k is in the context ctx.

Sourceval find_ctx : ('a, 'v) ctx_key -> 'a ctx -> 'v

find_ctx k ctx returns the element at key k in the context ctx. Raises Not_found if no element is found.

Sourceval find_ctx_opt : ('a, 'v) ctx_key -> 'a ctx -> 'v option

find_ctx k ctx returns the element of the key k in the context ctx. Returns None if no element is found.

Sourceval add_ctx : ('a, 'v) ctx_key -> 'v -> 'a ctx -> 'a ctx

add_ctx k v ctx add element v at key k in the context ctx. The previous element is overwritten if present.

Sourceval remove_ctx : ('a, 'v) ctx_key -> 'a ctx -> 'a ctx

add_ctx k v ctx removes the element at key k in the context ctx. If key k was not in ctx, ctx is returned unchanged.

Sourceval most_recent_ctx : 'a ctx -> 'a ctx -> 'a ctx

Get the most recent context between two

Sourceval pp_ctx : (Print.printer -> 'a -> unit) -> Stdlib.Format.formatter -> 'a ctx -> unit

Print a context

Sourcetype ctx_pool = {
  1. ctx_pool_equal : 'a 'v 'w. ('a, 'v) ctx_key -> ('a, 'w) ctx_key -> ('v, 'w) Mopsa_utils.Eq.eq option;
  2. ctx_pool_print : 'a 'v. (Print.printer -> 'a -> unit) -> Stdlib.Format.formatter -> ('a, 'v) ctx_key -> 'v -> unit;
}

Pool registered keys

Sourcetype ctx_info = {
  1. ctx_equal : 'a 'v 'w. ctx_pool -> ('a, 'v) ctx_key -> ('a, 'w) ctx_key -> ('v, 'w) Mopsa_utils.Eq.eq option;
  2. ctx_print : 'a 'v. ctx_pool -> (Print.printer -> 'a -> unit) -> Stdlib.Format.formatter -> ('a, 'v) ctx_key -> 'v -> unit;
}

Registration information for a new key

Sourceval register_ctx : ctx_info -> unit

Register a new key

Sourcemodule GenContextKey (Value : sig ... end) : sig ... end

Generate a new key

Sourceval callstack_ctx_key : ('a, Mopsa_utils.Callstack.callstack) ctx_key

Key for storing the callstack