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
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2024 OCamlPro *)
(* Written by the Owi programmers *)
open Bos
open Syntax
module Bugs = Prio.Make (Prio.FIFO)
let print_and_count_bugs ~format ~out_file ~no_value
~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure ~results
~with_breadcrumbs =
let test_suite_dir = Fpath.(workspace / "test-suite") in
let* (_created : bool) =
if not no_value then OS.Dir.create test_suite_dir else Ok false
in
let rec aux count results =
match results () with
| Seq.Nil -> Ok count
| Seq.Cons (bug, tl) ->
let* () =
Model.print ~format ~out_file ~id:count ~no_value ~no_stop_at_failure
~no_assert_failure_expression_printing ~with_breadcrumbs bug
in
let* () =
if not no_value then
let testcase = Smtml.Model.get_bindings bug.model |> List.map snd in
Cmd_utils.write_testcase ~dir:test_suite_dir testcase
else Ok ()
in
let count = succ count in
if no_stop_at_failure then aux count tl else Ok count
in
aux 0 results
let compute_number_of_workers workers =
(*
* TODO: try this at some point? It's likely going to make things bad but who knows...
* Domainpc.isolate_current ();
*)
let workers =
match workers with
| None ->
let n = Domainpc.get_available_cores () in
assert (n > 0);
n
| Some n ->
assert (n > 0);
n
in
if workers > 1 then Logs_threaded.enable ();
workers
let run ~exploration_strategy ~workers ~no_worker_isolation ~no_stop_at_failure
~no_value ~no_assert_failure_expression_printing ~deterministic_result_order
~fail_mode ~workspace ~solver ~model_format ~model_out_file ~with_breadcrumbs
~run_time (to_run : unit Symbolic_choice.t) =
(* Various initializations *)
let bug_stack = Bugs.make () in
let path_count = Atomic.make 0 in
let time_before = (Unix.times ()).tms_utime in
let module Scheduler =
( val Symbolic_parameters.Exploration_strategy.to_work_ds_module
exploration_strategy )
in
let sched = Scheduler.make () in
let thread = Thread.init () in
let initial_task = fun () -> Symex.Monad.run to_run thread in
Scheduler.push initial_task Prio.dummy sched;
(* Compute the number of workers *)
let workers = compute_number_of_workers workers in
(* Setup the bug stack so it knows if more bugs may arrive *)
for _i = 1 to workers do
Bugs.new_pledge bug_stack
done;
Solver.solver_to_use := Some solver;
(* Launch workers *)
let domains =
(* Decides what to push in the bug stack and close the scheduler if needed. *)
let at_result v =
Atomic.incr path_count;
match v with
| Ok (), _thread -> ()
| Error bug, _thread ->
let should_be_added =
match fail_mode with
| Symbolic_parameters.Both -> true
| Assertion_only -> Bug.is_assertion bug
| Trap_only -> Bug.is_trap bug
in
if should_be_added then begin
Bugs.push bug Prio.dummy bug_stack;
if not no_stop_at_failure then begin
Scheduler.close sched
end
end
in
(* Handles final values from the monad and reschedule them if needed. *)
let rec at_schedulable (t : _ Symex.Monad.Schedulable.t) write_back =
match t with
| Prune -> ()
| Now x -> at_result x
| Yield (prio, f) -> write_back (prio, f)
| Choice (m1, m2) ->
at_schedulable m1 write_back;
at_schedulable m2 write_back
in
let run_worker () =
Fun.protect
~finally:(fun () -> Bugs.end_pledge bug_stack)
(fun () ->
try
(* Pull work from the queue as long as it's possible *)
Scheduler.work_while
(fun f write_back -> at_schedulable (f ()) write_back)
sched
with
| Z3.Error _ when Solver.was_interrupted () ->
(* it happens regularly that interrupting Z3 makes it crash, in this case, we simply ignore the exception, otherwise it is confusing for the user as it looks like something went wrong when there's nothing to worry about *)
()
| e ->
let e_s = Printexc.to_string e in
let bt = Printexc.get_raw_backtrace () in
let bt_s = Printexc.raw_backtrace_to_string bt in
let bt_s =
if String.equal "" bt_s then
"use OCAMLRUNPARAM=b to get the backtrace"
else bt_s
in
Log.err (fun m ->
m "a worker ended with exception %s, backtrace is: @\n@[<v>%s@]"
e_s bt_s );
Printexc.raise_with_backtrace e bt )
in
let isolated = not no_worker_isolation in
Domainpc.spawn_n ~isolated ~n:workers run_worker
in
(* Handle the bug stack *)
let* count =
let results =
Bugs.read_as_seq bug_stack |> Bug.sort_seq_if deterministic_result_order
in
print_and_count_bugs ~format:model_format ~out_file:model_out_file ~no_value
~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure
~results ~with_breadcrumbs
in
(* We don't want to wait for domain to complete in normal/quiet mode because it may take quite some time (if a solver is running a long query, the interpreter is in a long concrete loop, or if the work queue was not correctly closed for instance) *)
let wait_for_all_domains () =
Array.iter
(fun domain ->
try Domain.join domain with
| Z3.Error msg ->
Log.info (fun m ->
m "one domain exited with the following Z3 exception: %s" msg )
| Smtml.Eval.Eval_error err ->
Log.info (fun m ->
m "one domain exited with the following Smtml exception: %a"
Smtml.Eval.pp_error_kind err )
| exn ->
let backtrace = Printexc.get_raw_backtrace () in
Log.info (fun m ->
m
"one domain exited with the %s exception which was only noticed \
while waiting for all domain to join:@\n\
\ @[<v>%s@]"
(Printexc.to_string exn)
(Printexc.raw_backtrace_to_string backtrace) ) )
domains
in
if Log.is_bench_enabled () then begin
let bench_stats = thread.bench_stats in
let execution_time_b =
let time_after = (Unix.times ()).tms_utime in
time_after -. time_before
in
Benchmark.print_final ~bench_stats ~execution_time_a:run_time
~execution_time_b ~wait_for_all_domains
end
else if
let landmark_profiling_enabled =
Option.is_some @@ Bos.OS.Env.var "OCAML_LANDMARKS"
in
Log.is_debug_enabled () || landmark_profiling_enabled
then begin
(* we only do this in debug mode or when landmarks profiling is on because
otherwise it makes performances very bad *)
wait_for_all_domains ()
end;
Log.info (fun m -> m "Completed paths: %d" (Atomic.get path_count));
if count > 0 then Error (`Found_bug count)
else Ok (Log.app (fun m -> m "All OK!"))