package mopsa

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

Source file intraproc.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
316
317
318
319
320
321
322
323
324
325
326
327
(****************************************************************************)
(*                                                                          *)
(* 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/>.    *)
(*                                                                          *)
(****************************************************************************)

(** Intra-procedural iterator for blocks, assignments and tests *)

open Mopsa
open Sig.Abstraction.Stateless
open Ast
open Numeric.Common

(******************)
(** Trace markers *)
(******************)

type marker += M_if of bool * expr

let () = register_marker {
    marker_print = (fun next fmt -> function
        | M_if(true, cond) ->
          Format.fprintf fmt "if (%a)" pp_expr cond
        | M_if(false, cond) ->
          Format.fprintf fmt "if (!%a)" pp_expr cond
        | m ->
          next fmt m
      );
    marker_compare = (fun next m1 m2 ->
        match m1, m2 with
        | M_if(branch1, cond1), M_if(branch2, cond2) ->
          Compare.pair Bool.compare compare_expr
            (branch1, cond1) (branch2, cond2)
        | _ ->
          next m1 m2
      );
    marker_print_name = (fun next -> function
        | M_if _ -> "if"
        | m -> next m
      );
    marker_name = "if";
  }

(**********************)
(** Domain definition *)
(**********************)

module Domain =
struct

  include GenStatelessDomainId(
    struct
      let name = "universal.iterators.intraproc"
    end
    )

  let checks = []

  let init prog man flow = None

  let rec negate_bool_expr e =
    match ekind e with
    | E_constant (C_bool true) -> mk_false e.erange
    | E_constant (C_bool false) -> mk_true e.erange
    | E_constant (C_top T_bool) -> e
    | E_unop(O_log_not, ee) -> ee
    | E_binop(O_log_and,e1,e2) -> mk_log_or (negate_bool_expr e1) (negate_bool_expr e2) e.erange
    | E_binop(O_log_or,e1,e2) -> mk_log_and (negate_bool_expr e1) (negate_bool_expr e2) e.erange
    | E_binop(O_log_xor, e1, e2) -> mk_log_xor (negate_bool_expr e1) e2 e.erange
    | E_binop(op,e1,e2) when is_comparison_op op -> mk_binop e1 (negate_comparison_op op) e2 e.erange ~etyp:T_bool
    | _ -> mk_not e e.erange

  let rec to_bool_expr e =
    match ekind e with
    | E_constant (C_bool _) -> e
    | E_constant (C_top T_bool) -> e
    | E_var _ -> e
    | E_unop(O_log_not,e) -> negate_bool_expr (to_bool_expr e)
    | E_unop(op,_) when is_predicate_op op -> e
    | E_binop(op,_,_) when is_comparison_op op -> e
    | E_binop(op,e1,e2) when is_logic_op op -> mk_binop (to_bool_expr e1) op (to_bool_expr e2) e.erange ~etyp:T_bool
    | _ -> assert false

  let rec eval_bool_expr e ~ftrue ~ffalse ~fboth range man flow =
    let ee =
      match expr_to_const e with
      | Some c -> { e with ekind = E_constant c }
      | None -> e
    in
    match ekind ee with
    | E_constant (C_bool true) -> ftrue flow
    | E_constant (C_bool false) -> ffalse flow
    | E_constant (C_int n) -> if Z.(n <> zero) then ftrue flow else ffalse flow
    | E_constant (C_top T_bool) -> fboth flow
    | E_constant (C_top T_int) -> fboth flow
    | E_unop(O_log_not,ee) -> eval_bool_expr ee ~ftrue:ffalse ~ffalse:ftrue ~fboth range man flow
    | _ ->
      assume (to_bool_expr ee) man flow ~route:(Below name) ~translate:"Universal"
        ~fthen:ftrue
        ~felse:ffalse

  let exec stmt man flow =
    match skind stmt with
    | S_expression e ->
      man.eval e flow >>$? fun e flow ->
      Post.return flow |>
      OptionExt.return

    | S_assign(x,e) when is_universal_type (etyp x) ->
      man.eval e flow ~translate:"Universal" >>$? fun e flow ->
      man.exec (mk_assign x e stmt.srange) flow ~route:(Below name) |>
      OptionExt.return

    | S_assume{ekind = E_constant (C_bool b)} ->
      Post.return (if b then flow else Flow.remove T_cur flow) |>
      OptionExt.return

    | S_assume{ekind = E_unop(O_log_not, {ekind = E_constant (C_bool b)})} ->
      Post.return (if not b then flow else Flow.remove T_cur flow) |>
      OptionExt.return

    | S_assume{ekind = E_constant (C_int n)} ->
      Post.return (if Z.(n <> zero) then flow else Flow.remove T_cur flow) |>
      OptionExt.return

    | S_assume{ekind = E_unop(O_log_not, {ekind = E_constant (C_int n)})} ->
      Post.return (if Z.(n = zero) then flow else Flow.remove T_cur flow) |>
      OptionExt.return

    | S_assume e when is_universal_type (etyp e) ->
      man.eval e flow ~translate:"Universal" >>$? fun e' flow ->
      man.exec (mk_assume e' stmt.srange) flow ~route:(Below name) |>
      OptionExt.return

    (* Skip the analysis of the block if there is no indirect flow and the
       current environment is empty *)
    | S_block (b, cleaner)
      when Flow.is_empty flow ||
           (* no indirect flow *)
           ( Flow.is_singleton flow && Flow.mem T_cur flow &&
             (* empty environment *)
             man.lattice.is_bottom (Flow.get T_cur man.lattice flow) ) ->
      Post.return flow |>
      OptionExt.return


    | S_block(block,local_vars) ->
      Some (
        let post = List.fold_left (fun acc stmt -> acc >>% man.exec stmt) (Post.return flow) block in
        let end_range =
          if is_orig_range stmt.srange
          then set_range_start stmt.srange (get_range_end stmt.srange)
          else stmt.srange in
        let post = List.fold_left (fun acc var -> acc >>% man.exec (mk_remove_var var end_range)) post local_vars in
        post
      )

    (* Skip the analysis of if there is no flow *)
    | S_if(cond, s1, s2) when Flow.is_empty flow ->
      Post.return flow |>
      OptionExt.return

    (* Use [assume], that skips the analyis of a branch if its input environment is empty. *)
    (* This is sound if there is no inderct flow, because [assume] will not
       execute the branch if its [cur] environment is empty, while an indirect
       flow may have an empty [cur] environment. *)
    | S_if(cond, s1, s2) when Flow.is_singleton flow && Flow.mem T_cur flow ->
      assume cond man flow
        ~fthen:(fun flow ->
            man.exec (mk_add_marker (M_if(true, cond)) stmt.srange) flow >>%
            man.exec s1)
        ~felse:(fun flow ->
            man.exec (mk_add_marker (M_if(false, cond)) stmt.srange) flow >>%
            man.exec s2)
      |> OptionExt.return

    | S_if(cond, s1, s2) ->
      (* Use this function to execute a branch when the other one is not
         reachable. In addition to the execution of the body of the reachable branch,
         this function executes the unreachable branch with an empty T_cur
         environment. This ensures that indirect flows in the branch are
         executed. *)
      let exec_one_branch stmt other branch flow =
        let post1 =
          man.exec (mk_add_marker (M_if(branch, cond)) stmt.srange) flow >>%
          man.exec stmt
        in
        let ctx1 = Cases.get_ctx post1 in
        let flow2 = Flow.set_ctx ctx1 flow |>
                    Flow.remove T_cur
        in
        let post2 = man.exec other flow2 in
        Post.join post1 post2
      in
      (* Execute both branches and ensure proper propagation of the context *)
      let exec_both_branches flow1 flow2 =
        let post1 =
          man.exec (mk_add_marker (M_if(true, cond)) stmt.srange) flow1 >>%
          man.exec s1
        in
        let ctx1 = Cases.get_ctx post1 in
        let flow2 = Flow.set_ctx ctx1 flow2 in
        let post2 =
          man.exec (mk_add_marker (M_if(false, cond)) stmt.srange) flow2 >>%
          man.exec s2
        in
        Post.join post1 post2
      in
      assume cond man flow
        ~fthen:(exec_one_branch s1 s2 true)
        ~felse:(exec_one_branch s2 s1 false)
        ~fboth:(exec_both_branches)
        (* When both environment are empty, we still need to execute both
           branches because of eventual indirect flows *)
        ~fnone:(exec_both_branches)
      |>
      OptionExt.return

    | S_print_state ->
      let printer = empty_printer () in
      Flow.print man.lattice.print printer flow;
      Framework.Output.Factory.print printer (srange stmt);
      Some (Post.return flow)

    | S_print_expr el ->
      let printer = empty_printer () in
      List.iter (man.print_expr flow printer) el;
      Framework.Output.Factory.print printer (srange stmt);
      Some (Post.return flow)


    | _ -> None

  let is_not_universal e = not (is_universal_type e.etyp)

  let eval exp man flow =
    match ekind exp with
    | E_binop (O_log_and, e1, e2)
      when is_universal_type exp.etyp ->
      assume_num e1 man flow
        ~fthen:(fun flow ->
            (* Since we didn't check the type of the sub-expression [e1], we
               need to translate to Universal (if this isn't the case already).
               That way, we can handle expressions from other semantics, as long
               as they can be translated to Universal.
               Note that we need to do that because we checked that the type of
               the whole expression is Universal. *)
            man.eval e2 flow ~translate:"Universal"
          )
        ~felse:(fun flow -> Eval.singleton (mk_false exp.erange) flow)
      |> OptionExt.return

    | E_binop (O_log_or, e1, e2)
      when is_universal_type exp.etyp ->
      assume_num e1 man flow
        ~fthen:(fun flow -> Eval.singleton (mk_true exp.erange) flow)
        ~felse:(fun flow -> man.eval e2 flow ~translate:"Universal")
      |> OptionExt.return

    | E_binop (O_log_xor, e1, e2)
      when is_universal_type exp.etyp ->
      let s1 =
        assume_num e1 man flow
          ~fthen:(fun flow -> man.eval (mk_not e2 exp.erange) ~translate:"Universal" flow)
          ~felse:(fun flow -> man.eval e2 flow ~translate:"Universal")
      in
      let s2 =
        assume_num (mk_not e1 exp.erange) man flow
          ~fthen:(fun flow -> man.eval e2 flow ~translate:"Universal")
          ~felse:(fun flow -> man.eval (mk_not e2 exp.erange) ~translate:"Universal" flow)
      in
      Eval.join s1 s2 |>
      OptionExt.return

    | E_unop (O_log_not, { ekind = E_binop (O_log_and, e1, e2) })
      when is_universal_type exp.etyp ->
      man.eval (mk_log_or (mk_not e1 e1.erange) (mk_not e2 e2.erange) exp.erange) flow |>
      OptionExt.return

    | E_unop (O_log_not, { ekind = E_binop (O_log_or, e1, e2) })
      when is_universal_type exp.etyp ->
      man.eval (mk_log_and (mk_not e1 e1.erange) (mk_not e2 e2.erange) exp.erange) flow |>
      OptionExt.return

    | E_binop(op,e1,e2)
      when is_comparison_op op  &&
           is_universal_type exp.etyp ->
      eval_bool_expr exp exp.erange man flow
        ~ftrue:(fun flow -> Eval.singleton (mk_true exp.erange) flow)
        ~ffalse:(fun flow -> Eval.singleton (mk_false exp.erange) flow)
        ~fboth:(fun flow -> Eval.singleton (mk_top T_bool exp.erange) flow) |>
      OptionExt.return

    | E_unop(op,ee) when is_predicate_op op  &&
                         is_universal_type exp.etyp ->
      eval_bool_expr exp exp.erange man flow
        ~ftrue:(fun flow -> Eval.singleton (mk_true exp.erange) flow)
        ~ffalse:(fun flow -> Eval.singleton (mk_false exp.erange) flow)
        ~fboth:(fun flow -> Eval.singleton (mk_top T_bool exp.erange) flow) |>
      OptionExt.return

    | _ -> 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