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
(* SPDX-License-Identifier: MIT *)
(* Copyright (C) 2023-2026 formalsec *)
(* Written by the Smtml programmers *)
let run_and_time_call ~use f =
let start = Unix.gettimeofday () in
let result = f () in
let stop = Unix.gettimeofday () in
use (stop -. start);
result
let query_log_path : Fpath.t option =
let env_var = "QUERY_LOG_PATH" in
match Bos.OS.Env.var env_var with Some p -> Some (Fpath.v p) | None -> None
let[@inline never] protect m f =
Mutex.lock m;
match f () with
| x ->
Mutex.unlock m;
x
| exception e ->
Mutex.unlock m;
let bt = Printexc.get_raw_backtrace () in
Printexc.raise_with_backtrace e bt
(* If the environment variable [QUERY_LOG_PATH] is set, stores and writes
all queries sent to the solver (with their timestamps) to the given file *)
let write =
match query_log_path with
| None -> fun ~model:_ _ _ _ _ -> ()
| Some path ->
let log_entries :
(string * Expr.t list * bool * int64 * [ `Sat | `Unknown | `Unsat ]) list
ref =
ref []
in
let close () =
if List.compare_length_with !log_entries 0 <> 0 then
try
let oc =
(* open with wr/r/r rights, create if it does not exit and append to
it if it exists. *)
Out_channel.open_gen
[ Open_creat; Open_binary; Open_append ]
0o644 (Fpath.to_string path)
in
Marshal.to_channel oc !log_entries [];
Out_channel.close oc
with e ->
Fmt.failwith "Failed to write log: %s@." (Printexc.to_string e)
in
at_exit close;
Sys.set_signal Sys.sigterm (Sys.Signal_handle (fun _ -> close ()));
(* write *)
let mutex = Mutex.create () in
fun ~model solver_name assumptions time status ->
let entry = (solver_name, assumptions, model, time, status) in
protect mutex (fun () -> log_entries := entry :: !log_entries)
let check_log_query (f : unit -> [ `Sat | `Unknown | `Unsat ]) name assumptions
=
match query_log_path with
| Some _ ->
let counter = Mtime_clock.counter () in
let res = f () in
write ~model:false name assumptions
(Mtime.Span.to_uint64_ns (Mtime_clock.count counter))
res;
res
| None -> f ()
let model_log_query f name assumptions =
match query_log_path with
| Some _ ->
let counter = Mtime_clock.counter () in
let res = f () in
(* TODO: can no model actually mean `Unsat? *)
write ~model:true name assumptions
(Mtime.Span.to_uint64_ns (Mtime_clock.count counter))
(if Option.is_some res then `Sat else `Unknown);
res
| None -> f ()