package mopsa

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

Source file ast.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
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
(****************************************************************************)
(*                                                                          *)
(* This file is part of MOPSA, a Modular Open Platform for Static Analysis. *)
(*                                                                          *)
(* Copyright (C) 2018-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/>.    *)
(*                                                                          *)
(****************************************************************************)

(** Extends the simple Universal language with Control Flow Graphs. *)

open Mopsa
open Universal.Ast

   
(*==========================================================================*)
                         (** {2 Graph types} *)
(*==========================================================================*)


module Loc =
struct    
  type t = Location.pos (* maybe add a unique tag? *)
  let compare = Location.compare_pos
  let hash = Hashtbl.hash
  let equal l1 l2 = Location.compare_pos l1 l2 = 0
  let print = Location.pp_position
end

module TagLoc =
struct    
  type t =
    { loc: Loc.t;
      tag: string; (* optional tag (may be "") *)
      id:  int;    (* unique among t with the same log ans tag *)
    }

  let compare (t1:t) (t2:t) : int =
    Compare.triple
      Loc.compare compare compare
      (t1.loc, t1.id, t1.tag) (t2.loc, t2.id, t2.tag)

  let hash : t -> int = Hashtbl.hash

  let equal (t1:t) (t2:t) : bool = compare t1 t2 = 0

  let print fmt (t:t) =
    match t.tag, t.id with
    | "",0 -> Loc.print fmt t.loc
    | "",_ -> Format.fprintf fmt "%a(%i)" Loc.print t.loc t.id
    | _,0  -> Format.fprintf fmt "%a(%s)" Loc.print t.loc t.tag
    | _    -> Format.fprintf fmt "%a(%s:%i)" Loc.print t.loc t.tag t.id

end

module Range =
struct
  type t = range
  let compare = compare_range
  let hash = Hashtbl.hash
  let equal l1 l2 = compare l1 l2 = 0
  let print = pp_range
end

module Port =
struct
  type t = token
  let compare = compare_token
  let hash = Hashtbl.hash
  let equal l1 l2 = compare l1 l2 = 0
  let print = pp_token
end

module LocSet = SetExt.Make(Loc)
module LocMap = MapExt.Make(Loc)
module LocHash = Hashtbl.Make(Loc)

module TagLocSet = SetExt.Make(TagLoc)
module TagLocMap = MapExt.Make(TagLoc)
module TagLocHash = Hashtbl.Make(TagLoc)

module RangeSet = SetExt.Make(Range)
module RangeMap = MapExt.Make(Range)
module RangeHash = Hashtbl.Make(Range)

                 
(** Build CFG module. *)
module CFG_Param =
struct
  module NodeId = TagLoc
  (** Identify nodes by source location. *)
                  
  module EdgeId = Range
  (** Identify edges by source range. *)

  module Port = Port
  (** Edge outputs are distinguished by flow tokens. *)
end
  
module CFG = Graph.Make(CFG_Param)

(** Edges are labelled with a statement.
    Nodes have no information in the graph structure.
    Abstract invariant information will be kept in maps separately
    from the CFG. 
    This way, CFG can be kept immutable.
 *)
type graph = (unit, stmt) CFG.graph
type node  = (unit, stmt) CFG.node
type edge  = (unit, stmt) CFG.edge
          
type node_id = TagLoc.t
type edge_id = Range.t
type port = token

type cfg =
  { cfg_graph: graph;
    mutable cfg_order: node GraphSig.nested_list list;
  }


(*==========================================================================*)
                       (** {2 Graph utilities} *)
(*==========================================================================*)

          
let mk_node_id ?(id=0) ?(tag="") (loc:Loc.t) : node_id =
  TagLoc.{ id; tag; loc; }

let fresh_node_id = LocHash.create 16 
  
let mk_fresh_node_id ?(tag="") (loc:Loc.t) : node_id =
  let id = try LocHash.find fresh_node_id loc with Not_found -> 0 in
  LocHash.replace fresh_node_id loc (id+1);
  mk_node_id ~id ~tag loc
(** Fresh node with some source location information. 
    NOTE: Do not mix mk_fresh_node_id and mk_node_id as it can break 
    uniqueness.
 *)  

let loc_anonymous : Loc.t =
  Location.mk_pos "<anonymous>" (-1) (-1)
  
let mk_anonymous_node_id ?(tag="") () : node_id =
  mk_fresh_node_id ~tag loc_anonymous
(** Fresh node without any source location information. *)  

let copy_node_id (n:node_id) : node_id =
  mk_fresh_node_id ~tag:n.TagLoc.tag n.TagLoc.loc
  
let node_loc (t:node_id) : Loc.t = t.TagLoc.loc

let pp_node_id = TagLoc.print
let pp_node_as_id fmt node = pp_node_id fmt (CFG.node_id node)

let compare_node_id = TagLoc.compare


               
let mk_edge_id ?(tag="") (range:range) : edge_id =
  if tag = "" then range else tag_range range "%s" tag

let fresh_edge_id = RangeHash.create 16
(* we use our own fresh range generator to keep an origin_range information *)
  
let mk_fresh_edge_id ?(tag="") (range:range) : edge_id =
  let id = try RangeHash.find fresh_edge_id range with Not_found -> 0 in
  RangeHash.replace fresh_edge_id range (id+1);
  let tag =
    if id = 0 then tag
    else if tag = "" then string_of_int id
    else tag^":"^(string_of_int id)
  in
  mk_edge_id ~tag range
(** Fresh range with possible some source range information. 
    NOTE: Do not mix mk_fresh_edge_id and mk_edge_id as it can break 
    uniqueness.
*)  

let mk_anonymous_edge_id ?(tag="") () : edge_id =
  mk_edge_id ~tag (mk_fresh_range ())
(** Fresh range without any source range information. *)

let edge_range (t:edge_id) : range = t

let pp_edge_id = Range.print
let pp_edge_as_id fmt edge = pp_edge_id fmt (CFG.edge_id edge)

let compare_edge_id = Range.compare
                
          
(*==========================================================================*)
                           (** {2 Flows} *)
(*==========================================================================*)


(** Associate a flow to each CFG node.
    We can store abstract information for the whole graph in a 
    single abstract state, using node flows.
    We also associate a flow to cache the post-image of each CFG edge.
 *)
type token +=
  | T_cfg_node of node_id
  | T_cfg_edge_post of edge_id * port
  | T_cfg_entry of port

(** Flow for true and false branch of tests. *)            
type token +=
   | T_true
   | T_false

   
(*==========================================================================*)
                           (** {2 Statements} *)
(*==========================================================================*)


type stmt_kind +=
   | S_cfg of cfg              
   | S_test of expr (** test nodes, with a true and a false branch *)
   | S_skip (** empty node *)

   
let mk_skip range =
  mk_stmt S_skip range

let mk_test e range =
  mk_stmt (S_test e) range

let mk_cfg cfg range =
  mk_stmt (S_cfg cfg) range
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