Source file `simplified.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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
(****************************************************************************)
(*                                                                          *)
(* 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/>.    *)
(*                                                                          *)
(****************************************************************************)

(** Extended domains signatures used by combiners *)

open Core.All
open Abstraction.Simplified
open Mopsa_utils

module type SIMPLIFIED_COMBINER =
sig
  include SIMPLIFIED
  val domains : DomainSet.t
  val semantics : SemanticSet.t
  val routing_table : routing_table
  val merge : t -> t * teffect -> t * teffect -> t
  val exec : DomainSet.t option -> stmt -> ('a,t) simplified_man -> 'a ctx -> t -> t option
  val ask  : DomainSet.t option -> ('a,'r) query -> ('a,t) simplified_man -> 'a ctx -> t -> 'r option
  val print_state : DomainSet.t option -> printer -> t -> unit
  val print_expr  : DomainSet.t option -> ('a,t) simplified_man -> 'a ctx -> t -> printer -> expr -> unit
end



module SimplifiedToCombiner(D:SIMPLIFIED) : SIMPLIFIED_COMBINER with type t = D.t =
struct
  include D
  let domains = DomainSet.singleton D.name
  let semantics = SemanticSet.empty
  let routing_table = empty_routing_table
  let merge pre (a1,te1) (a2,te2) =
    let e1 = get_root_effect te1 in
    let e2 = get_root_effect te2 in
    if compare_effect e1 e2 = 0 then a1 else
    if is_empty_effect e1 then a2 else
    if is_empty_effect e2 then a1
    else D.merge pre (a1,e1) (a2,e2)
  let exec domains = D.exec
  let ask domains  = D.ask
  let print_state targets = D.print_state
  let print_expr  targets = D.print_expr
end

module CombinerToSimplified(T:SIMPLIFIED_COMBINER) : SIMPLIFIED with type t = T.t =
struct
  include T
  let merge pre (a1,e1) (a2,e2) =
    let te1 = mk_teffect e1 empty_teffect empty_teffect in
    let te2 = mk_teffect e2 empty_teffect empty_teffect in
    T.merge pre (a1,te1) (a2,te2)
  let exec stmt man ctx a = T.exec None stmt man ctx a
  let ask query man ctx a = T.ask None query man ctx a
  let print_state printer a = T.print_state None printer a
  let print_expr man ctx a printer e = T.print_expr None man ctx a printer e
end



module SimplifiedToStandard(D: SIMPLIFIED_COMBINER) : Domain.DOMAIN_COMBINER with type t = D.t =
struct

  include D

  let subset _ _ (a,_) (a',_) = D.subset a a'
  let join _ _ (a,_) (a',_) = D.join a a'
  let meet _ _ (a,_) (a',_) = D.meet a a'
  let widen _ ctx (a,_) (a',_) = D.widen ctx a a'

  let init prog man flow =
    let a' = D.init prog in
    set_env T_cur a' man flow

  let routing_table = empty_routing_table

  let checks = []

  let simplified_man man flow = {
    exec = (fun stmt -> man.Core.Manager.exec stmt flow |>
                        post_to_flow man |>
                        get_env T_cur man
           );
    ask = (fun query -> ask_and_reduce man.Core.Manager.ask query flow);
  }

  let exec domains =
    let f = D.exec domains in
    (fun stmt man flow ->
       let a = get_env T_cur man flow in
       if D.is_bottom a
       then
         Post.return flow |>
         OptionExt.return
       else
         f stmt (simplified_man man flow) (Flow.get_ctx flow) a |>
         OptionExt.lift @@ fun a' ->
         let post =
           set_env T_cur a' man flow |>
           Post.return
         in
         if are_effects_enabled () then
           post |> Cases.map_effects (fun effects ->
               man.set_effects (
                 man.get_effects effects |>
                 add_stmt_to_teffect stmt
               ) effects
             )
         else
           post
    )

  let eval domains exp man flow = None

  let ask domains =
    let f = D.ask domains in
    (fun query man flow ->
       match f query (simplified_man man flow) (Flow.get_ctx flow) (get_env T_cur man flow) with
       | None -> None
       | Some r -> Some (Cases.singleton r flow)
    )

  let print_expr domains =
    let f = D.print_expr domains in
    (fun man flow printer e ->
       let a = get_env T_cur man flow in
       if D.is_bottom a
       then ()
       else f (simplified_man man flow) (Flow.get_ctx flow) a printer e
    )
end