Module Value.NonrelSource

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

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

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

Sourceval 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

Sourceval 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

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

Find the context attached to a variable

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

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

Context for saving the bounds of a variable

Sourceval 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

Sourceval 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

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

Remove the bounds of a variable from a context

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

Remove the bounds of a variable from a flow

Sourceval 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