package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Library
Module
Module type
Parameter
Class
Class type

Generic non-relational abstraction.

This combiner lifts a non-relational value abstraction 𝒱 into an abstract domain of partial environments 𝐕↛𝒱 from variables to values.

The concretization of the domain is: γ(X) = ρ | dom(ρ) ⊆ dom(X) ∧ ∀ v ∈ dom(ρ): ρ(v) ∈ γᵥ(X(v))

Identifier for the non-relation domain

******************************************

type Core.All.id +=
  1. | D_nonrel : (module Sig.Abstraction.Value.VALUE with type t = 'v) -> (Core.All.var, 'v) Lattices.Partial_map.map Core.All.id

Identifier of a non-relational domain

Variable's context

**********************

The context of a variable keeps (flow-insensitive) information about the variable that can pushed by external domains and consumed by the value abstraction.

This is useful to implement a widening with thresholds: external heuristics discover the theresholds and put them in the context of the variable. When widen is called on a the value of a variable, it is enriched with its context.

Access key to the map of variables contexts

val add_var_ctx : Core.All.var -> ('a, 'v) Core.All.ctx_key -> 'v -> 'a Core.All.ctx -> 'a Core.All.ctx

Add a context to a variable

val find_var_ctx_opt : Core.All.var -> ('a, 'v) Core.All.ctx_key -> 'a Core.All.ctx -> 'v option

Find the context attached to a variable

val find_var_ctx : Core.All.var -> ('a, 'v) Core.All.ctx_key -> 'a Core.All.ctx -> 'v

Find the context attached to a variable

val remove_var_ctx : Core.All.var -> ('a, 'v) Core.All.ctx_key -> 'a Core.All.ctx -> 'a Core.All.ctx

Remove the context attached to a variable

Variable bounds

*******************

The bounds of a variable is an invariant about its value that is always valid. It is put in the context of the variable and is used to refine its value whenever it changes.

val var_bounds_ctx : ('a, Core.All.constant) Core.All.ctx_key

Context for saving the bounds of a variable

val add_var_bounds_ctx : Core.All.var -> Core.All.constant -> 'a Core.All.ctx -> 'a Core.All.ctx

Add the bounds of a variable to a context

val add_var_bounds_flow : Core.All.var -> Core.All.constant -> 'a Core.All.flow -> 'a Core.All.flow

Add the bounds of a variable to a flow

val remove_var_bounds_ctx : Core.All.var -> 'a Core.All.ctx -> 'a Core.All.ctx

Remove the bounds of a variable from a context

val remove_var_bounds_flow : Core.All.var -> 'a Core.All.flow -> 'a Core.All.flow

Remove the bounds of a variable from a flow

val find_var_bounds_ctx_opt : Core.All.var -> 'a Core.All.ctx -> Core.All.constant option

Find the bounds of a variable in a context

Non-relational domain

*************************

Create a non-relational domain from a value abstraction

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct