package mopsa

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

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
149
150
151
152
153
(****************************************************************************)
(*                                                                          *)
(* 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 : path -> t -> t * change_map -> t * change_map -> 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 path pre (a1,m1) (a2,m2) =
    let e1 = get_change path m1 in
    let e2 = get_change path m2 in
    if compare_change e1 e2 = 0 then a1 else
    if is_empty_change e1 then a2 else
    if is_empty_change 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 = singleton_change_map empty_path e1 in
    let te2 = singleton_change_map empty_path e2 in
    T.merge empty_path 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 |>
    Option.some

  let routing_table = empty_routing_table

  let checks = []

  let simplified_man man flow = {
    exec = (fun stmt ->
        let flow = man.Core.Manager.exec stmt flow |>
                   post_to_flow man
        in
        let cases = get_env T_cur man flow in
        Cases.reduce_result
          (fun a _ -> a)
          ~join:D.join ~meet:D.meet ~bottom:(fun () -> D.bottom)
          cases
      );
    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 ->
       get_env T_cur man flow >>$? fun a flow ->
       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
         in
         if is_change_tracker_enabled () then
           post |> Cases.map_changes (fun changes flow ->
               man.add_change stmt [] flow changes
             )
         else
           post
    )

  let eval domains exp man flow = None

  let ask domains =
    let f = D.ask domains in
    (fun query man flow ->
       get_env T_cur man flow >>$? fun a flow ->
       match f query (simplified_man man flow) (Flow.get_ctx flow) a 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 ->
       get_env T_cur man flow |>
       Cases.iter_result
         (fun a flow ->
            if D.is_bottom a
            then ()
            else f (simplified_man man flow) (Flow.get_ctx flow) a printer e
         )
    )
end
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