package mopsa

  1. Overview
  2. Docs
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.