package mopsa

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

Source file unittest.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
(****************************************************************************)
(*                                                                          *)
(* 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/>.    *)
(*                                                                          *)
(****************************************************************************)

(** Unit tests iterator. *)

open Mopsa
open Sig.Abstraction.Stateless
open Ast


let name = "universal.iterators.unittest"

(* Command line options
   ====================

   - The flag -unittest activates the mode of unit testing. In this
   mode, every function starting with test_* is called. At the end,
   statistics about failed/safe assertions are collected.

   - The option -unittest-filter = f1,f2,... selects the functions
   to be tested.
*)

let unittest_flag = ref false
let unittest_filter = ref []

let () =
  register_domain_option name {
    key = "-unittest";
    category = "Unit tests";
    spec = ArgExt.Set unittest_flag;
    doc = " activate unittest mode";
    default = "";
  };
  register_domain_option name {
    key = "-unittest-filter";
    category = "Unit tests";
    doc = " list of test functions (separated by comma) to analyze";
    spec = ArgExt.String(fun s ->
        unittest_filter := Str.split (Str.regexp "[ ]*,[ ]*") s
      );
    default = "";
  };
  ()


(* Flow tokens
   ===========

   Safe assertions are saved in the flow so that we can compute
   statistics at the end of the analysis. Note that failed assertions
   are kept in the T_alarm token.
*)

type token +=
  | T_safe_assert of range (* location of the assert statement *)

let () =
  register_token {
    compare = (fun next tk1 tk2 ->
        match tk1, tk2 with
        | T_safe_assert(r1), T_safe_assert(r2) -> compare_range r1 r2
        | _ -> next tk1 tk2
      );
    print = (fun next fmt tk ->
        match tk with
        | T_safe_assert(r) -> Format.fprintf fmt "safe@%a" pp_range r
        | _ -> next fmt tk
      );
  };
  ()


(* Analysis alarms *)
type check      += CHK_ASSERT_FAIL
type alarm_kind += A_assert_fail of expr (** condition *)


let () =
  register_check (fun next fmt -> function
      | CHK_ASSERT_FAIL -> Format.fprintf fmt "Assertion failure"
      | a -> next fmt a
    );
  register_alarm {
    check = (fun next -> function
        | A_assert_fail _ -> CHK_ASSERT_FAIL
        | a -> next a
      );
    compare = (fun next a1 a2 ->
        match a1, a2 with
        | A_assert_fail(c1), A_assert_fail(c2) -> compare_expr c1 c2
        | _ -> next a1 a2
      );
    print = (fun next fmt -> function
        | A_assert_fail(cond) ->
          Format.fprintf fmt "Assertion '%a' violated" (Debug.bold pp_expr) cond
        | a -> next fmt a
      );
    join = (fun next a1 a2 -> next a1 a2)
  };
  ()


let raise_assert_fail ?(force=false) cond man flow =
  let cs = Flow.get_callstack flow in
  let alarm = mk_alarm (A_assert_fail cond) cs cond.erange in
  Flow.raise_alarm alarm ~bottom:true ~force man.lattice flow

let safe_assert_check range man flow =
  Flow.add_safe_check CHK_ASSERT_FAIL range flow


module Domain =
struct


  (* Domain identification *)
  (* ===================== *)

  include GenStatelessDomainId(struct
      let name = name
    end)
  let summary fmt = Debug.debug ~channel:"unittest" fmt


  let checks = [CHK_ASSERT_FAIL]

  (* Initialization *)
  (* ============== *)

  let init prog man flow = flow


  (* Computation of post-conditions *)
  (* ============================== *)

  let execute_test_functions ?(flow_cleaner = fun man flow -> Flow.remove T_cur flow) tests man flow =
    let tests = match !unittest_filter with
      | [] | ["all"] -> tests
      | _ -> List.filter (fun (t, _) -> List.mem t !unittest_filter) tests
    in
    let ctx = Flow.get_ctx flow in
    let report = Flow.get_report flow in
    List.fold_left (fun acc (name, test) ->
        debug "Executing %s" name;
        (* Fold the context *)
        let flow = Flow.copy_ctx acc flow in
        (* Call the function *)
        let flow1 = man.exec test flow |> post_to_flow man in
        let flow1 = flow_cleaner man flow1 in
        (* let info_flow1 = Flow.bottom (Flow.get_ctx flow1) (Flow.get_report flow1) in *)
        Flow.join man.lattice acc flow1
      )
      (Flow.bottom ctx report)
      tests

  let rec exec stmt man flow  =
    match skind stmt with
    | S_unit_tests(tests) ->
      debug "Starting tests";
      let flow1 = execute_test_functions tests man flow in
      Post.return flow1 |>
      OptionExt.return

    | S_assert(cond) ->
      assume
        cond
        ~fthen:(fun safe_flow ->
            safe_assert_check cond.erange man safe_flow |>
            Post.return)
        ~felse:(fun fail_flow ->
            raise_assert_fail cond man fail_flow |>
            Post.return
        )
        man flow
      |> OptionExt.return

    | S_satisfy(cond) ->
      man.exec (mk_assume cond stmt.srange) flow >>%? fun flow' ->
      if not @@ man.lattice.is_bottom @@ Flow.get T_cur man.lattice flow' then
        safe_assert_check cond.erange man flow |>
        Post.return |>
        OptionExt.return
      else
        raise_assert_fail cond man flow |>
        Post.return |>
        OptionExt.return


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