package mopsa

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

Module Core.CasesSource

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 changes and cleaner statements. To represent suspended computations, the result of a case can be empty.

Sourcetype cleaners = Ast.Stmt.StmtSet.t
Sourcetype 'r case =
  1. | Result of 'r * Change.change_map * cleaners
    (*

    Actual result of the computation, with changes 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

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.

Sourceval return : ?changes:Change.change_map -> ?cleaners:Ast.Stmt.stmt list -> 'r -> 'a Flow.flow -> ('a, 'r) cases
Sourceval singleton : ?changes:Change.change_map -> ?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

Sourceval remove_duplicates : ?equal:('r case -> 'r case -> bool) -> 'a Lattice.lattice -> ('a, 'r) cases -> ('a, 'r) cases
Sourceval remove_duplicate_results : ?equal:('r -> 'r -> bool) -> 'a Lattice.lattice -> ('a, 'r) cases -> ('a, 'r) cases

Remove duplicate results

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

Return the number of results

Sourceval is_singleton : ('a, 'r) cases -> bool
Sourceval choose : ('a, 'r) cases -> 'r case * 'a Flow.flow
Sourceval choose_result : ('a, 'r) cases -> 'r * 'a Flow.flow

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.

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

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

Changes

***********

Sourceval get_case_changes : 'r case -> Change.change_map

Get the changes attached to a case

Sourceval set_case_changes : Change.change_map -> 'r case -> 'r case

Set the changes attached to a case

Sourceval map_changes : (Change.change_map -> 'a Flow.flow -> Change.change_map) -> ('a, 'r) cases -> ('a, 'r) cases

map_changes f c replaces each changes l in c with f l.

Sourceval set_changes : Change.change_map -> ('a, 'r) cases -> ('a, 'r) cases

Set the same changes 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.

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

Join a list of cases.

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

Meet a list of cases.

Iterators

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

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

Sourceval 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

Sourceval 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

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

Sourceval 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

Sourceval 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

Sourceval 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

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

Pretty printer of cases

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

Pretty printer of results

Monadic binders

Sourceval 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. Changes and cleaners returned by f are concatenated with the previous ones in cases.

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

Bind operator for bind_opt

Sourceval 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. Changes and cleaners returned by f are concatenated with the previous ones in cases.

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

Bind operator for bind

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

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

Bind operator for bind_result_opt

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

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

Bind operator for bind_result

Sourceval 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. Changes and cleaners returned by f are concatenated with the previous ones in cases.

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

Sourceval 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. Changes and cleaners returned by f are concatenated with the previous ones in cases.

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

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

Sourceval 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