Source file log.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
open Lang
open Sl
open Print
open Util.Source
let rec log_case ?(level = 0) ?(index = 0) (cover : Multi.t) (case : case) :
string =
let indent = String.make (level * 2) ' ' in
let order = Format.asprintf "%s%d. " indent index in
let = " " ^ order in
let guard, block = case in
Format.asprintf "%sCase %s\n\n%s" header (string_of_guard guard)
(log_block ~level:(level + 1) cover block)
and log_cases ?(level = 0) (cover : Multi.t) (cases : case list) : string =
cases
|> List.mapi (fun idx case -> log_case ~level ~index:(idx + 1) cover case)
|> String.concat "\n\n"
and log_instr ?(level = 0) ?(index = 0) (cover : Multi.t) (instr : instr) :
string =
let indent = String.make (level * 2) ' ' in
let hit = Multi.is_hit cover instr.note.iid in
let order = Format.asprintf "%s%d. " indent index in
let = (if hit then "+ " else "- ") ^ order in
let = " " ^ order in
match instr.it with
| IfI (exp_cond, iterexps, block_then, _) ->
Format.asprintf "%sIf (%s)%s, then\n\n%s" header (string_of_exp exp_cond)
(string_of_iterexps iterexps)
(log_block ~level:(level + 1) cover block_then)
| HoldI (id, notexp, iterexps, holdcase) -> (
match holdcase with
| BothH (block_hold, block_nothold) ->
Format.asprintf "%sIf (%s: %s)%s holds, then\n\n%s\n\n%sElse,\n\n%s"
header (string_of_relid id) (string_of_notexp notexp)
(string_of_iterexps iterexps)
(log_block ~level:(level + 1) cover block_hold)
header_trailing
(log_block ~level:(level + 1) cover block_nothold)
| HoldH (block_hold, _) ->
Format.asprintf "%sIf (%s: %s)%s holds, then\n\n%s" header
(string_of_relid id) (string_of_notexp notexp)
(string_of_iterexps iterexps)
(log_block ~level:(level + 1) cover block_hold)
| NotHoldH (block_nothold, _) ->
Format.asprintf "%sIf (%s: %s)%s does not hold, then\n\n%s" header
(string_of_relid id) (string_of_notexp notexp)
(string_of_iterexps iterexps)
(log_block ~level:(level + 1) cover block_nothold))
| CaseI (exp, cases, _) ->
Format.asprintf "%sCase analysis on %s\n\n%s" header (string_of_exp exp)
(log_cases ~level:(level + 1) cover cases)
| GroupI (id_group, rel_signature, exps_group, block_group) ->
Format.asprintf "%sGroup %s: %s\n\n%s" header (string_of_relid id_group)
(string_of_relinput rel_signature exps_group)
(log_block ~level:(level + 1) cover block_group)
| LetI (exp_l, exp_r, iterinstrs, block) ->
Format.asprintf "%s(Let %s be %s)%s\n\n%s" header (string_of_exp exp_l)
(string_of_exp exp_r)
(string_of_iterinstrs iterinstrs)
(log_block ~level:(level + 1) ~index cover block)
| RuleI (id_rel, notexp, _inputs, iterinstrs, block) ->
Format.asprintf "%s(%s: %s)%s\n\n%s" header (string_of_relid id_rel)
(string_of_notexp notexp)
(string_of_iterinstrs iterinstrs)
(log_block ~level:(level + 1) ~index cover block)
| ResultI (_, []) -> Format.asprintf "%sThe relation holds" header
| ResultI (rel_signature, exps) ->
Format.asprintf "%sResult in: %s" header
(string_of_reloutput rel_signature exps)
| ReturnI exp -> Format.asprintf "%sReturn %s" header (string_of_exp exp)
| DebugI (exp, instr) ->
Format.asprintf "%sDebug: %s\n%s" header (string_of_exp exp)
(log_instr ~level ~index:(index + 1) cover instr)
and log_block ?(level = 0) ?(index = 0) (cover : Multi.t) (block : block) :
string =
block
|> List.mapi (fun idx instr ->
log_instr ~level ~index:(index + idx + 1) cover instr)
|> String.concat "\n\n"
and log_elseblock ?(level = 0) ?(index = 0) (cover : Multi.t)
(elseblock : elseblock) : string =
Format.asprintf "%s%d. Otherwise,\n\n%s"
(String.make (level * 2) ' ')
(index + 1)
(log_block ~level:(level + 1) cover elseblock)
and log_elseblock_opt ?(level = 0) ?(index = 0) (cover : Multi.t)
(elseblock_opt : elseblock option) : string =
match elseblock_opt with
| Some elseblock -> log_elseblock ~level ~index cover elseblock
| None -> ""
let log_defined_rel (cover : Multi.t) (rel : rel) : string =
let relid, rel_signature, exps_match, block, elseblock_opt, _hints = rel in
string_of_relid relid ^ ": "
^ string_of_relinput rel_signature exps_match
^ "\n\n" ^ log_block cover block
^ log_elseblock_opt ~index:(List.length block) cover elseblock_opt
let log_tablerow (cover : Multi.t) (tablerow : tablerow) : string =
let exps_match, exp_result, block = tablerow in
"\n Row : "
^ string_of_exps ", " exps_match
^ " -> " ^ string_of_exp exp_result ^ "\n\n"
^ log_block ~level:2 cover block
let log_tablerows (cover : Multi.t) (tablerows : tablerow list) : string =
tablerows |> List.map (log_tablerow cover) |> String.concat "\n"
let log_table_func (cover : Multi.t) (tablefunc : tablefunc) : string =
let defid, params, _typ_ret, tablerows, _hints = tablefunc in
string_of_defid defid ^ string_of_params params ^ "\n=\n"
^ log_tablerows cover tablerows
let log_defined_func (cover : Multi.t) (func : definedfunc) : string =
let defid, tparams, params, _typ_ret, block, elseblock_opt, _hints = func in
string_of_defid defid ^ string_of_tparams tparams ^ string_of_params params
^ "\n\n" ^ log_block cover block
^ log_elseblock_opt ~index:(List.length block) cover elseblock_opt
let log_def (cover : Multi.t) (def : def) : string =
(";; " ^ string_of_region def.at ^ "\n")
^
match def.it with
| ExternTypD (typid, _) -> "extern syntax " ^ string_of_typid typid
| TypD (typid, tparams, deftyp, _) ->
"syntax " ^ string_of_typid typid ^ string_of_tparams tparams ^ " = "
^ string_of_deftyp deftyp
| VarD (id, typ, _) -> "var " ^ string_of_varid id ^ ": " ^ string_of_typ typ
| ExternRelD externrel -> "extern relation " ^ string_of_extern_rel externrel
| RelD rel -> "rel " ^ log_defined_rel cover rel
| ExternDecD externfunc -> "extern def " ^ string_of_extern_func externfunc
| BuiltinDecD builtinfunc ->
"builtin def " ^ string_of_builtin_func builtinfunc
| TableDecD tablefunc -> "tbl def " ^ log_table_func cover tablefunc
| FuncDecD func -> "def " ^ log_defined_func cover func
let log_defs (cover : Multi.t) (defs : def list) : string =
String.concat "\n\n" (List.map (log_def cover) defs)
let log_spec ~(path_cov_opt : string option) (cover : Multi.t) (spec : spec) :
unit =
let output oc_opt =
match oc_opt with Some oc -> output_string oc | None -> print_string
in
let oc_opt = Option.map open_out path_cov_opt in
let output = output oc_opt in
let total, hits, coverage = Multi.measure_coverage cover in
Format.asprintf ";; Instruction coverage: %d/%d (%.2f%%)\n" hits total
coverage
|> output;
log_defs cover spec |> output;
match oc_opt with Some oc -> close_out oc | None -> ()