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
(* SPDX-License-Identifier: AGPL-3.0-or-later *)
(* Copyright © 2021-2024 OCamlPro *)
(* Written by the Owi programmers *)
open Syntax
(* model stuff *)
type output_format =
| Scfg
| Json
let pp format with_breadcrumbs no_value fmt
(model, labels, breadcrumbs, scoped_values) =
match format with
| Json ->
let json = Symbol_scope.to_json ~no_value model scoped_values in
let labels_json =
List.map
(fun (id, name) -> `Assoc [ ("id", `Int id); ("name", `String name) ])
labels
in
let json =
match json with
| `Assoc fields -> `Assoc (("labels", `List labels_json) :: fields)
| _ -> json
in
let json =
if with_breadcrumbs then
let crumbs =
List.rev_map (fun crumb -> `Int crumb) (List.rev breadcrumbs)
in
match json with
| `Assoc fields -> `Assoc (fields @ [ ("breadcrumbs", `List crumbs) ])
| _ -> json
else json
in
Yojson.Basic.pretty_print fmt json
| Scfg ->
let scfg = Symbol_scope.to_scfg ~no_value model scoped_values in
let model = Scfg.Query.get_dir_exn "model" scfg in
let lbls =
{ Scfg.Types.name = "labels"
; params = []
; children =
List.map
(fun (id, lbl_name) ->
{ Scfg.Types.name = "label"
; params = [ string_of_int id; lbl_name ]
; children = []
} )
labels
}
in
let bcrumbs =
if with_breadcrumbs then
[ { Scfg.Types.name = "breadcrumbs"
; params = List.map string_of_int (List.rev breadcrumbs)
; children = []
}
]
else []
in
let ret =
model
:: (if List.length lbls.children > 0 then lbls :: bcrumbs else bcrumbs)
in
Scfg.Pp.config fmt ret
let print ~format ~out_file ~id ~no_value ~no_stop_at_failure
~no_assert_failure_expression_printing ~with_breadcrumbs bug =
let to_file path model labels breadcrumbs symbol_scopes =
let ext = match format with Json -> "json" | Scfg -> "scfg" in
let contains_ext =
Fpath.has_ext ".json" path || Fpath.has_ext ".scfg" path
in
let* path =
let* () =
if contains_ext && (not @@ Fpath.has_ext ext path) then
Fmt.error_msg
"Given model file extension is not compatible with the current \
model format"
else Ok ()
in
let path = Fpath.to_string @@ Fpath.rem_ext path in
let base =
Fpath.v (if no_stop_at_failure then Fmt.str "%s_%d" path id else path)
in
Ok (Fpath.add_ext ext base)
in
Bos.OS.File.writef path "%a"
(pp format with_breadcrumbs no_value)
(model, labels, breadcrumbs, symbol_scopes)
in
let output model labels breadcrumbs symbol_scopes =
match out_file with
| Some path -> to_file path model labels breadcrumbs symbol_scopes
| None -> begin
Log.app (fun m ->
let fmt = m (if no_stop_at_failure then "%a@." else "%a") in
fmt
(pp format with_breadcrumbs no_value)
(model, labels, breadcrumbs, symbol_scopes) );
Ok ()
end
in
match bug with
| `ETrap (tr, model, labels, breadcrumbs, symbol_scopes) ->
Log.err (fun m -> m "Trap: %s" (Result.err_to_string tr));
output model labels breadcrumbs symbol_scopes
| `EAssert (assertion, model, labels, breadcrumbs, symbol_scopes) ->
if no_assert_failure_expression_printing then
Log.err (fun m -> m "Assert failure")
else Log.err (fun m -> m "Assert failure: %a" Smtml.Expr.pp assertion);
output model labels breadcrumbs symbol_scopes