package mopsa

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

Source file manager.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
(****************************************************************************)
(*                                                                          *)
(* This file is part of MOPSA, a Modular Open Platform for Static Analysis. *)
(*                                                                          *)
(* Copyright (C) 2017-2019 The MOPSA Project.                               *)
(*                                                                          *)
(* This program is free software: you can redistribute it and/or modify     *)
(* it under the terms of the GNU Lesser General Public License as published *)
(* by the Free Software Foundation, either version 3 of the License, or     *)
(* (at your option) any later version.                                      *)
(*                                                                          *)
(* This program is distributed in the hope that it will be useful,          *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of           *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the            *)
(* GNU Lesser General Public License for more details.                      *)
(*                                                                          *)
(* You should have received a copy of the GNU Lesser General Public License *)
(* along with this program.  If not, see <http://www.gnu.org/licenses/>.    *)
(*                                                                          *)
(****************************************************************************)


(** Manager - access to the top-level lattice and transfer functions *)


open Ast.Stmt
open Ast.Expr
open Ast.Semantic
open Lattice
open Flow
open Eval
open Post
open Cases
open Route
open Query
open Print
open Token
open Path
open Change


(*==========================================================================*)
(**                             {2 Managers}                                *)
(*==========================================================================*)


(** Managers provide access to full analyzer.

    ['a] is the type of the toplevel abstract element, and ['t] is the type of
    local abstract element (that is, the type of the domain that calls the
    manager). *)
type ('a, 't) man = {
  lattice : 'a lattice;
  (** Access to lattice operators on the toplevel abstract element ['a]. *)

  (** {3 Accessors to domain's abstract element}

      Each domain can get and set its abstract element in the transfer functions
      with [get] and [set].  *)

  get : token -> 'a flow -> ('a, 't) cases;
  (** Returns the domain's abstract element ['t]. A disjunction of cases is
      returned when partitioning is used. *)

  set : token -> 't -> 'a flow -> 'a post;
  (** Sets the domain's abstract element ['t]. *)

  (** {3 Toplevel Transfer Functions}

      The domains access the top-level lattice transfer function through the
      manager with these functions. It is possible to ask the manager to route
      the transfer functions (e.g. [eval]) to different domains with the
      optional [?route] parameter. If [?route] is not set, the routing starts
      from the root of the domains DAG. *)

  exec : ?route:route -> stmt -> 'a flow -> 'a post;
  (** [man.exec stmt flow] executes [stmt] in [flow] and returns the post state. *)

  eval : ?route:route -> ?translate:semantic -> ?translate_when:(semantic*(expr->bool)) list -> expr -> 'a flow -> 'a eval;
  (** [man.eval expr flow] evaluates [expr] in [flow] and returns the result
      expression.

      There are two kinds of evaluations: within the same semantic
      (simplifications), or to another semantic (translations). Calling
      [man.eval expr flow] performs both kinds of evaluations. The result [e']
      of [man.eval expr flow] is a {i simplification} of [e] within the same
      semantic. To retrieve a translation to another semantic, one can use
      the [?translate] parameter: [man.eval expr flow ~translate:semantic] is a
      {i translation} of the {i simplification} of [e] in [semantic]. A common
      use case is to translate expressions to Universal with
      [man.eval expr flow ~translate:"Universal"]. It is possible to control
      when the translation is applied with [?translate_when]. *)

  ask : 'r. ?route:route -> ('a,'r) query -> 'a flow -> ('a, 'r) cases;
 (** [man.ask query flow] performs a query to other domains. If no domain can
      answer the query, [man.ask query flow] results in a runtime error. *)

  print_expr : ?route:route -> 'a flow -> (printer -> expr -> unit);
  (** [man.print_expr flow] is the expression printer for the type ['a]. *)

  (** {3 Changes Management} *)

  add_change : stmt -> path -> 'a flow -> change_map -> change_map;
  (** Add a statement to the changes map. *)
}
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