package mopsa

You can search for identifiers within the package.

in-package search v0.2.0

On This Page

Cleaners
Context
Effects
Lattice operators
Iterators
1. Monadic binders

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

Maintainers

Sources

mopsa-analyzer-v1.0.tar.gz

md5=9f673f79708b44a7effb3b6bb3618d2c

sha512=cb91cb428e43a22f1abbcb8219710d0c10a5b3756d0da392d4084b3b3a6157350776c596983e63def344f617d39964e91f244f60c07958695ee5c8c809a9f0f4

doc/core/Core/Cases/index.html

Module `Core.Cases`Source

Cases - data structure for case-based transfer functions.

Transfer functions use Cases to return partitioned results. Cases are encoded as DNF formulas. Each individual case comes with a flow, a set of alarms, computation effects and cleaner statements. To represent suspended computations, the result of a case can be empty.

Sourcetype cleaners = Ast.Stmt.StmtSet.t

Sourcetype 'r case =

| Result of 'r * Effect.teffect * cleaners
(*
Actual result of the computation, with effects and cleaners
*)
| Empty
(*
Empty results due to non-terminating computations (e.g. alarms)
*)
| NotHandled
(*
This means that the domain can't process this case. The analyzer can ask other domains to handle it.
*)

A single case of a computation

Sourcetype ('a, 'r) cases

Cases of results 'r over an abstraction 'a

Sourceval case : 'r case -> 'a Flow.flow -> ('a, 'r) cases

Create a case.

val return : 
  ?effects:Effect.teffect ->
  ?cleaners:Ast.Stmt.stmt list ->
  'r ->
  'a Flow.flow ->
  ('a, 'r) cases

val singleton : 
  ?effects:Effect.teffect ->
  ?cleaners:Ast.Stmt.stmt list ->
  'r ->
  'a Flow.flow ->
  ('a, 'r) cases

Create a case with a single non-empty result.

Sourceval empty : 'a Flow.flow -> ('a, 'r) cases

Create a case with an empty case.

Sourceval not_handled : 'a Flow.flow -> ('a, 'r) cases

Create a non-handled case to be forwarded to other domains

val remove_duplicates : 
  ('r case -> 'r case -> int) ->
  'a Lattice.lattice ->
  ('a, 'r) cases ->
  ('a, 'r) cases

val remove_duplicate_results : 
  ('r -> 'r -> int) ->
  'a Lattice.lattice ->
  ('a, 'r) cases ->
  ('a, 'r) cases

Remove duplicate results

Sourceval cardinal : ('a, 'r) cases -> int

Return the number of results

Cleaners

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

Sourceval opt_clean_cur_only : bool Stdlib.ref

Option to apply cleaners on T_cur only

Sourceval add_cleaners : Ast.Stmt.stmt list -> ('a, 'r) cases -> ('a, 'r) cases

add_cleaners block c adds cleaner statements block to cases c.

Sourceval get_case_cleaners : 'r case -> cleaners

Get the set of cleaners attached to a case

Sourceval set_case_cleaners : cleaners -> 'r case -> 'r case

Set the set of cleaners attached to a case

Sourceval set_cleaners : Ast.Stmt.stmt list -> ('a, 'r) cases -> ('a, 'r) cases

Set the same cleaners for all cases

Context

***********

Sourceval get_ctx : ('a, 'r) cases -> 'a Context.ctx

get_ctx c returns the context of cases c.

Sourceval set_ctx : 'a Context.ctx -> ('a, 'r) cases -> ('a, 'r) cases

set_ctx ctx c changes the context of cases c to ctx.

Sourceval copy_ctx : ('a, 'r) cases -> ('a, 's) cases -> ('a, 's) cases

copy_ctx c1 c2 changes the context of cases c2 to the context of c1.

Sourceval get_callstack : ('a, 'r) cases -> Mopsa_utils.Callstack.callstack

get_callstack c returns the callstack of cases c.

val set_callstack : 
  Mopsa_utils.Callstack.callstack ->
  ('a, 'r) cases ->
  ('a, 'r) cases

set_callstack cs c returns a copy of c with callstack cs.

Effects

***********

Sourceval get_case_effects : 'r case -> Effect.teffect

Get the effects attached to a case

Sourceval set_case_effects : Effect.teffect -> 'r case -> 'r case

Set the effects attached to a case

val map_effects : 
  (Effect.teffect -> Effect.teffect) ->
  ('a, 'r) cases ->
  ('a, 'r) cases

map_effects f c replaces each effects l in c with f l.

Sourceval set_effects : Effect.teffect -> ('a, 'r) cases -> ('a, 'r) cases

Set the same effects for all cases

Lattice operators

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

Sourceval join : ('a, 'r) cases -> ('a, 'r) cases -> ('a, 'r) cases

Join two cases.

Sourceval meet : ('a, 'r) cases -> ('a, 'r) cases -> ('a, 'r) cases

Meet two cases.

val join_list : 
  empty:(unit -> ('a, 'r) cases) ->
  ('a, 'r) cases list ->
  ('a, 'r) cases

Join a list of cases.

val meet_list : 
  empty:(unit -> ('a, 'r) cases) ->
  ('a, 'r) cases list ->
  ('a, 'r) cases

Meet a list of cases.

Iterators

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

val map : 
  ('r case -> 'a Flow.flow -> 's case * 'a Flow.flow) ->
  ('a, 'r) cases ->
  ('a, 's) cases

map f c replaces each case ci*flow in c with f ci flow

Sourceval map_result : ('r -> 's) -> ('a, 'r) cases -> ('a, 's) cases

map_result f c is similar to map f c, except that empty and not-handled cases are kept unmodified.

val map_conjunction : 
  (('r case * 'a Flow.flow) list -> ('s case * 'a Flow.flow) list) ->
  ('a, 'r) cases ->
  ('a, 's) cases

map_conjunction f c replaces each conjunction conj in c with f conj

val map_disjunction : 
  (('r case * 'a Flow.flow) list -> ('s case * 'a Flow.flow) list) ->
  ('a, 'r) cases ->
  ('a, 's) cases

map_disjunction f c replaces each disjunction disj in c with f disj

val reduce : 
  ('r case -> 'a Flow.flow -> 'b) ->
  join:('b -> 'b -> 'b) ->
  meet:('b -> 'b -> 'b) ->
  ('a, 'r) cases ->
  'b

reduce f ~join ~meet c collapses cases in c to a single value by applying f on each case and merging outputs using join and meet.

val reduce_result : 
  ('r -> 'a Flow.flow -> 'b) ->
  join:('b -> 'b -> 'b) ->
  meet:('b -> 'b -> 'b) ->
  bottom:(unit -> 'b) ->
  ('a, 'r) cases ->
  'b

reduce_result f ~join ~meet bottom c is similar to reduce f join meet c, except that empty and not-handled cases are replaced with bottom.

Sourceval fold : ('b -> 'r case -> 'a Flow.flow -> 'b) -> 'b -> ('a, 'r) cases -> 'b

Fold over the flattened list of cases

val fold_result : 
  ('b -> 'r -> 'a Flow.flow -> 'b) ->
  'b ->
  ('a, 'r) cases ->
  'b

Fold over the flattened list of results

Sourceval iter : ('r case -> 'a Flow.flow -> unit) -> ('a, 'r) cases -> unit

Iterate over the flattened list of cases

Sourceval iter_result : ('r -> 'a Flow.flow -> unit) -> ('a, 'r) cases -> unit

Iterate over the flattened list of results

val partition : 
  ('r case -> 'a Flow.flow -> bool) ->
  ('a, 'r) cases ->
  ('a, 'r) cases option * ('a, 'r) cases option

partition f cases separates cases that verify or not predicate f

Sourceval for_all : ('r case -> 'a Flow.flow -> bool) -> ('a, 'r) cases -> bool

Check whether a predicate is valid over all cases

Sourceval for_all_result : ('r -> 'a Flow.flow -> bool) -> ('a, 'r) cases -> bool

Check whether a predicate is valid over all results

Sourceval exists : ('r case -> 'a Flow.flow -> bool) -> ('a, 'r) cases -> bool

Check whether a predicate is valid for at least one case

Sourceval exists_result : ('r -> 'a Flow.flow -> bool) -> ('a, 'r) cases -> bool

Check whether a predicate is valid for at least one result

val print : 
  (Stdlib.Format.formatter -> 'r case -> 'a Flow.flow -> unit) ->
  Stdlib.Format.formatter ->
  ('a, 'r) cases ->
  unit

Pretty printer of cases

val print_result : 
  (Stdlib.Format.formatter -> 'r -> 'a Flow.flow -> unit) ->
  Stdlib.Format.formatter ->
  ('a, 'r) cases ->
  unit

Pretty printer of results

Monadic binders

val bind_opt : 
  ('r case -> 'a Flow.flow -> ('a, 's) cases option) ->
  ('a, 'r) cases ->
  ('a, 's) cases option

bind_opt f cases substitutes each case (c,flow) in cases with f c flow. If the function returns None, the case becomes NotHandled. Effects and cleaners returned by f are concatenated with the previous ones in cases.

val (>>=?) : 
  ('a, 'r) cases ->
  ('r case -> 'a Flow.flow -> ('a, 's) cases option) ->
  ('a, 's) cases option

Bind operator for bind_opt

val bind : 
  ('r case -> 'a Flow.flow -> ('a, 's) cases) ->
  ('a, 'r) cases ->
  ('a, 's) cases

bind f cases substitutes each case (c,flow) in cases with f c flow. Effects and cleaners returned by f are concatenated with the previous ones in cases.

val (>>=) : 
  ('a, 'r) cases ->
  ('r case -> 'a Flow.flow -> ('a, 's) cases) ->
  ('a, 's) cases

Bind operator for bind

val bind_result_opt : 
  ('r -> 'a Flow.flow -> ('a, 's) cases option) ->
  ('a, 'r) cases ->
  ('a, 's) cases option

Same as bind_opt, but empty and not-handled cases are preserved and are not passed to f.

val (>>$?) : 
  ('a, 'r) cases ->
  ('r -> 'a Flow.flow -> ('a, 's) cases option) ->
  ('a, 's) cases option

Bind operator for bind_result_opt

val bind_result : 
  ('r -> 'a Flow.flow -> ('a, 's) cases) ->
  ('a, 'r) cases ->
  ('a, 's) cases

Same as bind, but empty and not-handled cases are preserved and are not passed to f.

val (>>$) : 
  ('a, 'r) cases ->
  ('r -> 'a Flow.flow -> ('a, 's) cases) ->
  ('a, 's) cases

Bind operator for bind_result

val bind_conjunction : 
  (('r case * 'a Flow.flow) list -> ('a, 's) cases) ->
  ('a, 'r) cases ->
  ('a, 's) cases

bind_conjunction f cases substitutes each conjunction of cases conj in cases with f conj. Effects and cleaners returned by f are concatenated with the previous ones in cases.

val bind_conjunction_result : 
  ('r list -> 'a Flow.flow -> ('a, 's) cases) ->
  'a Lattice.lattice ->
  ('a, 'r) cases ->
  ('a, 's) cases

Same as bind_conjunction f cases] but empty and not-handled cases are preserved and are not passed to f.

val bind_disjunction : 
  (('r case * 'a Flow.flow) list -> ('a, 's) cases) ->
  ('a, 'r) cases ->
  ('a, 's) cases

bind_disjunction f cases substitutes each disjunction of cases disj in cases with f disj. Effects and cleaners returned by f are concatenated with the previous ones in cases.

val bind_disjunction_result : 
  ('r list -> 'a Flow.flow -> ('a, 's) cases) ->
  'a Lattice.lattice ->
  ('a, 'r) cases ->
  ('a, 's) cases

Same as bind_disjunction f cases] but empty and not-handled cases are preserved and are not passed to f.

val bind_list_opt : 
  'r list ->
  ('r -> 'a Flow.flow -> ('a, 's) cases option) ->
  'a Flow.flow ->
  ('a, 's list) cases option

Bind a list of results with a partial transfer function.

val bind_list : 
  'r list ->
  ('r -> 'a Flow.flow -> ('a, 's) cases) ->
  'a Flow.flow ->
  ('a, 's list) cases

Bind a list of results with a transfer function

On This Page

Cleaners
Context
Effects
Lattice operators
Iterators
1. Monadic binders