package mopsa

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

Source file iterator.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
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
(****************************************************************************)
(*                                                                          *)
(* 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/>.    *)
(*                                                                          *)
(****************************************************************************)

(** General intraprocedural iterator on Control Flow Graphs. *)

open Mopsa
open Sig.Abstraction.Stateless
open Universal.Ast
open Ast


let name = "cfg.iterators.intraproc"


(*==========================================================================*)
(**                       {2 Command line options}                          *)
(*==========================================================================*)

             
let opt_decreasing_iter : int ref = ref 1
(** Number of decreasing iterations after widening stabilisation. *)

                                        
let () =
  register_domain_option name {
    key = "-decreasing-iter";
    category = "Loops";
    doc = " number of decreasing iterations after stabilization";
    spec = Set_int (opt_decreasing_iter, ArgExt.empty);
    default = "1";
  }
 
                                        
(*==========================================================================*)
                       (** {2 Iterator} *)
(*==========================================================================*)


module Domain =
struct

  include GenStatelessDomainId(struct
      let name = name
    end)

  let checks = []

  let init prog man flow = None


  (* flow iterator for CFG *)                         
  let cfg_iterator cfg man flow =

    
    (* update the node abstract value as the join of incoming
       edge posts and entries;
       if weak=true, join with the previous value (for widened nodes)
    *)
    let update_node weak flow node =
      (* post edge flows *)
      let vs =
        List.map
          (fun (port,edge) ->
             Flow.get (T_cfg_edge_post (CFG.edge_id edge,port)) man.lattice flow
          )
          (CFG.node_in node)
      in
      (* entry flow *)
      let vs =
        match CFG.node_entry_port cfg.cfg_graph node with
        | None -> vs
        | Some port -> (Flow.get (T_cfg_entry port) man.lattice flow)::vs
      in
      (* old, if weak *)
      let nid = CFG.node_id node in
      let old = Flow.get (T_cfg_node nid) man.lattice flow in
      let vs = if weak then old::vs else vs in
      (* join *)
      let ctx = Flow.get_ctx flow in
      let v = List.fold_left (man.lattice.join ctx) man.lattice.bottom vs in
      debug "update node value %a: abs = @[%a@]@."
        pp_node_as_id node (format man.lattice.print) v;
      Flow.set (T_cfg_node nid) v man.lattice flow
    in
    
    (* apply a transfer function, update the edge post *)
    let apply_edge edge flow =
      let stmt = CFG.edge_data edge in
      debug "applying edge %a: @[%a@]" pp_edge_as_id edge pp_stmt stmt;
      let src, dst = CFG.edge_src edge, CFG.edge_dst edge in
      (* shift source node value into the expected port flow *)
      let flow =
        List.fold_left
          (fun flow (port,node) ->
             let v = Flow.get (T_cfg_node (CFG.node_id node)) man.lattice flow in
             debug "input node %a -> port %a, abs = @[%a@]"
               pp_node_as_id node pp_token port (format man.lattice.print) v;
             Flow.add port v man.lattice flow
          )
          flow src
      in
      (* apply edge transfer function *)
      man.exec stmt flow >>% fun flow ->
      (* dispatch flow values into nodes *)
      let flow =
        List.fold_left
          (fun flow (port,_) ->
             let v = Flow.get port man.lattice flow in
             debug "edge post %a %a: abs = @[%a@]"
               pp_edge_as_id edge pp_token port (format man.lattice.print) v;
             Flow.set (T_cfg_edge_post (CFG.edge_id edge,port)) v man.lattice flow
          )
          flow dst
      in
      (* clean-up flows used by transfer function *)
      let flow =
        List.fold_left
          (fun flow (port,_) -> Flow.remove port flow)
          flow (src@dst)
      in
      Post.return flow
    in
    
    (* recompute the node value and call apply_edge for all edges out 
       of this node
    *)
    let propagate_node weak node flow =
      (* update node value *)
      let flow = update_node weak flow node in
      (* reompute all edges from this node *)
      List.fold_left
        (fun post (_,e) -> post >>% apply_edge e)
        (Post.return flow) (CFG.node_out node)
    in

    (* get the widening node id for a component *)
    let get_widening_node lst =
      match lst with
      | (GraphSig.Simple node)::_ -> CFG.node_id node
      | _ -> Exceptions.panic "node expected at the head of a component"
    in
    
    (* analyze a component until its head is stable, with widening *)
    let rec fix_component count lst flow =
      let wid = get_widening_node lst in
      let old = Flow.get (T_cfg_node wid) man.lattice flow in
      debug "analyzing component @[%a@], widen=%a, count=%i, abs=@[%a@]"
            (Graph.pp_nested_list_list pp_node_as_id) lst
            pp_node_id wid count (format man.lattice.print) old;
      (* analyze the component *)
      analyze_component true lst flow >>% fun flow ->
      let v = Flow.get (T_cfg_node wid) man.lattice flow in
      (* check stability *)
      if man.lattice.subset (Flow.get_ctx flow) v old
      then (
        debug "component head stable %a" pp_node_id wid;
        refine_component 0 lst flow
      )
      else
        (* apply widening *)
        let widened =
          if count < !Universal.Iterators.Loops.opt_loop_widening_delay
          then v
          else man.lattice.widen (Flow.get_ctx flow) old v
        in
        debug "component head not stable %a" pp_node_id wid;
        let flow = Flow.set (T_cfg_node wid) widened man.lattice flow in
        fix_component (count+1) lst flow

    (* decreasing iterations *)
    and refine_component count lst flow =
      let wid = get_widening_node lst in
      if count >= !opt_decreasing_iter then (
        (* finished *)
        debug "component analysis finished @[%a@], head=%a, abs=@[%a@]"
          (Graph.pp_nested_list_list pp_node_as_id) lst
          pp_node_id wid (format man.lattice.print)
          (Flow.get (T_cfg_node wid) man.lattice flow);
        Post.return flow
      )
      else (
        (* iter *)
        debug "decreasing iteration at head %a, count=%i" pp_node_id wid count;
        analyze_component false lst flow >>%
        refine_component (count+1) lst
      )

                      
    (* analyze a list of components *)
    and analyze_component weak lst flow : 'a post =
      match lst with
      | (GraphSig.Simple node)::rest ->
        flow |> propagate_node weak node >>% analyze_component false rest
      | (GraphSig.Composed l)::rest ->
        flow |> fix_component 0 l >>% analyze_component false rest
      | [] -> Post.return flow
    in
    
    (* shift the current flow into the entry *)
    let flow_in flow =
      (* set cfg_entry information *)
      let flow =
        List.fold_left
          (fun flow (port,node) ->
             debug "set entry node %a, port %a" pp_node_as_id node pp_token port;
             let v = Flow.get port man.lattice flow in
             Flow.set (T_cfg_entry port) v man.lattice flow
          )
          flow (CFG.entries cfg.cfg_graph)
      in
      (* remove cur flow *)
      Flow.remove T_cur flow
    in
      
    (* gather the flows from the exit nodes *)
    let flow_out flow =
      List.fold_left
        (fun flow (port,node) ->
          debug "get exit node %a, port %a" pp_node_as_id node pp_token port;
          let v = Flow.get (T_cfg_node (CFG.node_id node)) man.lattice flow in
          Flow.add port v man.lattice flow
        )
        flow
        (CFG.exits cfg.cfg_graph)
    in
    
    (* remove all node-related flows (keeping cur, etc.) *)
    let cleanup flow =
      (* clean node info *)
      let flow =
        CFG.fold_nodes
          (fun id _ flow -> Flow.remove (T_cfg_node id) flow)
          cfg.cfg_graph flow
      in
      (* clean edge post info *)
      let flow =
        CFG.fold_edges
          (fun id edge flow ->
             List.fold_left
               (fun flow (port,_) ->
                  Flow.remove (T_cfg_edge_post (id,port)) flow
               ) flow (CFG.edge_dst edge)
          ) cfg.cfg_graph flow
      in
      (* clean entry info *)
      List.fold_left
        (fun flow (port,_) -> Flow.remove (T_cfg_entry port) flow)
        flow (CFG.entries cfg.cfg_graph)
    in
    
    (* all together now *)
    let flow = flow_in flow in
    analyze_component false cfg.cfg_order flow >>% fun flow ->
    let flow = flow |> flow_out |> cleanup in
    Post.return flow


  (* atomic test function *)
  let test_iterator man cond flow =
    let range = erange cond in
    debug "CFG test [%a] at %a" pp_expr cond pp_range range;
    man.eval cond flow >>$ fun cond flow ->
    man.exec (mk_assume cond range) flow >>% fun tflow -> 
    man.exec (mk_assume (mk_not cond range) range) flow >>% fun fflow -> 
    let tflow = Flow.set T_true  (Flow.get T_cur man.lattice tflow) man.lattice tflow
    and fflow = Flow.set T_false (Flow.get T_cur man.lattice fflow) man.lattice fflow in
    Flow.join man.lattice tflow fflow |>
    Post.return

    
  let exec stmt man flow =
    match skind stmt with

    | S_cfg cfg ->
       Some (cfg_iterator cfg man flow)

    | S_test expr ->
       Some (test_iterator man expr flow)

    | S_skip ->
       Some (Post.return flow)
      
    | _ ->
       (* S_expression, S_block and S_print are handled by universal's intraproc *)
       None
   
  let eval exp man flow = None

  let ask query man flow = None

  let print_expr man flow printer exp = ()

end


let () =
  register_stateless_domain (module Domain)
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