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