package mopsa

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

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.

type cleaners = Ast.Stmt.StmtSet.t
type 'r case =
  1. | Result of 'r * Effect.teffect * cleaners
    (*

    Actual result of the computation, with effects and cleaners

    *)
  2. | Empty
    (*

    Empty results due to non-terminating computations (e.g. alarms)

    *)
  3. | 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

type ('a, 'r) cases

Cases of results 'r over an abstraction 'a

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

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

Create a case with an empty case.

val 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

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

Return the number of results

Cleaners

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

val opt_clean_cur_only : bool Stdlib.ref

Option to apply cleaners on T_cur only

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

add_cleaners block c adds cleaner statements block to cases c.

val get_case_cleaners : 'r case -> cleaners

Get the set of cleaners attached to a case

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

Set the set of cleaners attached to a case

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

Set the same cleaners for all cases

Context

***********

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

get_ctx c returns the context of cases c.

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

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

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

val 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

***********

val get_case_effects : 'r case -> Effect.teffect

Get the effects attached to a case

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

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

Set the same effects for all cases

Lattice operators

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

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

Join two cases.

val 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

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

val 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

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

Iterate over the flattened list of cases

val 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

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

Check whether a predicate is valid over all cases

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

Check whether a predicate is valid over all results

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

Check whether a predicate is valid for at least one case

val 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

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