package mopsa

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

Source file syntax.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
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
(****************************************************************************)
(*                                                                          *)
(* 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/>.    *)
(*                                                                          *)
(****************************************************************************)

(** Syntax tree of configuration files *)

open Sig.Abstraction.Stacked
open Sig.Abstraction.Domain
open Sig.Abstraction.Simplified
open Sig.Abstraction.Simplified_functor
open Sig.Abstraction.Stateless
open Sig.Abstraction.Partitioning
open Sig.Abstraction.Value
open Sig.Abstraction.Value_functor
open Sig.Reduction.Exec
open Sig.Reduction.Eval
open Sig.Reduction.Value
open Sig.Reduction.Simplified

open Format


type abstraction = {
  domain: domain;
  language : string;
}

and domain = {
  domain_kind : domain_kind;
  domain_semantic : string option;
}

and domain_kind =
  | D_stacked    of (module STACKED)
  | D_domain     of (module DOMAIN)
  | D_simplified of (module SIMPLIFIED)
  | D_stateless  of (module STATELESS)
  | D_functor    of domain_functor * domain
  | D_nonrel     of value
  | D_switch   of domain list
  | D_compose    of domain list
  | D_product    of domain list * domain_reduction list

and domain_functor =
  | F_simplified of (module SIMPLIFIED_FUNCTOR)
  | F_stacked of domain
  | F_partitioning of (module PARTITIONING)

and value =
  | V_value   of (module VALUE)
  | V_functor of value_functor * value
  | V_union   of value list
  | V_product of value list * value_reduction list

and value_functor = (module VALUE_FUNCTOR)

and domain_reduction =
  | DR_exec       of (module EXEC_REDUCTION)
  | DR_eval       of (module EVAL_REDUCTION)
  | DR_simplified of (module SIMPLIFIED_REDUCTION)

and value_reduction = (module VALUE_REDUCTION)

let mk_domain ?(semantic=None) kind = { domain_kind = kind; domain_semantic = semantic } 

let pp_value_reduction fmt (r:value_reduction) =
  let module R = (val r) in
  pp_print_string fmt R.name

let pp_domain_reduction fmt = function
  | DR_exec r ->
    let module R = (val r) in
    pp_print_string fmt R.name

  | DR_eval r ->
    let module R = (val r) in
    pp_print_string fmt R.name

  | DR_simplified r ->
    let module R = (val r) in
    pp_print_string fmt R.name

let rec pp_value fmt = function
  | V_value v->
    let module V = (val v) in
    pp_print_string fmt V.name

  | V_functor(f,v) ->
    let module F = (val f) in
    fprintf fmt "%s(%a)" F.name pp_value v

  | V_union vl ->
    fprintf fmt "(%a)"
      (pp_print_list
         ~pp_sep:(fun fmt () -> pp_print_string fmt " ∪ ")
         pp_value) vl

  | V_product (vl,[]) ->
    fprintf fmt "(%a)"
      (pp_print_list
         ~pp_sep:(fun fmt () -> pp_print_string fmt " ∩ ")
         pp_value ) vl

  | V_product (vl,rl) ->
    fprintf fmt "(%a ↓ %a)"
      (pp_print_list
         ~pp_sep:(fun fmt () -> pp_print_string fmt " ∩ ")
         pp_value ) vl
      (pp_print_list
         ~pp_sep:(fun fmt () -> pp_print_string fmt " | ")
         pp_value_reduction ) rl



let rec pp_domain_functor fmt = function
  | F_stacked f ->
    pp_domain fmt f

  | F_simplified f ->
    let module F = (val f) in
    pp_print_string fmt F.name

  | F_partitioning f ->
    let module F = (val f) in
    pp_print_string fmt F.name


and pp_domain fmt d =
  match d.domain_semantic with
  | None -> pp_domain_kind fmt d.domain_kind
  | Some semantic -> fprintf fmt "[%s] %a" semantic pp_domain_kind d.domain_kind

and pp_domain_kind fmt = function
  | D_stacked d ->
    let module D = (val d) in
    pp_print_string fmt ("[S]" ^ D.name)

  | D_domain d ->
    let module D = (val d) in
    pp_print_string fmt ("[D]" ^ D.name)

  | D_simplified d ->
    let module D = (val d) in
    pp_print_string fmt ("[L]" ^ D.name)

  | D_stateless d ->
    let module D = (val d) in
    pp_print_string fmt ("[U]" ^ D.name)

  | D_functor(f,d) ->
    fprintf fmt "%a(%a)" pp_domain_functor f pp_domain d

  | D_nonrel v ->
    fprintf fmt "nonrel(%a)" pp_value v

  | D_switch dl ->
    fprintf fmt "(%a)"
      (pp_print_list
         ~pp_sep:(fun fmt () -> pp_print_string fmt " ; ")
         pp_domain) dl

  | D_compose dl ->
    fprintf fmt "(%a)"
      (pp_print_list
         ~pp_sep:(fun fmt () -> pp_print_string fmt " o ")
         pp_domain) dl

  | D_product(dl,[]) ->
    fprintf fmt "(%a)"
      (pp_print_list
         ~pp_sep:(fun fmt () -> pp_print_string fmt " ∧ ")
         pp_domain) dl

  | D_product(dl,rl) ->
    fprintf fmt "(%a ↓ %a)"
      (pp_print_list
         ~pp_sep:(fun fmt () -> pp_print_string fmt " ∧ ")
         pp_domain) dl
      (pp_print_list
         ~pp_sep:(fun fmt () -> pp_print_string fmt " | ")
         pp_domain_reduction) rl
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