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
|
(****************************************************************************)
(* the diy toolsuite *)
(* *)
(* Jade Alglave, University College London, UK. *)
(* Luc Maranget, INRIA Paris-Rocquencourt, France. *)
(* *)
(* Copyright 2012-present Institut National de Recherche en Informatique et *)
(* en Automatique and the authors. All rights reserved. *)
(* *)
(* This software is governed by the CeCILL-B license under French law and *)
(* abiding by the rules of distribution of free software. You can use, *)
(* modify and/ or redistribute the software under the terms of the CeCILL-B *)
(* license as circulated by CEA, CNRS and INRIA at the following URL *)
(* "http://www.cecill.info". We also give a copy in LICENSE.txt. *)
(****************************************************************************)
open Printf
open LogState
let verbose = ref 0
let logs = ref []
let forall = ref false
let optcond = ref false
let acceptempty = ref false
let hexa = ref false
let int32 = ref true
let faulttype = ref true
let neg = ref false
let options =
[
("-q", Arg.Unit (fun _ -> verbose := -1),
"<non-default> be silent");
("-v", Arg.Unit (fun _ -> incr verbose),
"<non-default> show various diagnostics, repeat to increase verbosity");
("-forall", Arg.Bool (fun b -> forall := b),
sprintf
"<bool> use forall quantifier in place of exists, default %b" !forall);
("-optcond", Arg.Bool (fun b -> optcond := b),
sprintf
"<bool> optimise conditions, default %b" !optcond);
("-acceptempty", Arg.Bool (fun b -> acceptempty := b),
sprintf
"<bool> output empty conditions, default %b" !acceptempty);
("-neg", Arg.Bool (fun b -> neg := b),
"<bool> negate final condition (default false)");
CheckName.parse_hexa hexa;
CheckName.parse_int32 int32;
CheckName.parse_faulttype faulttype;
]
let prog =
if Array.length Sys.argv > 0 then (Filename.basename Sys.argv.(0))
else "mlog2cond"
let usage = String.concat "\n" [
Printf.sprintf "Usage: %s [options] [path/to/log]" prog ;
"" ;
"Extract the condition from a single log file. If one is not provided on the" ;
"command-line, it will be read from stdin." ;
"" ;
"Options:" ;
]
let () =
Arg.parse options
(fun s -> logs := !logs @ [s])
usage
let verbose = !verbose
let hexa = !hexa
let int32 = !int32
let log = match !logs with
| [log;] -> Some log
| [] -> None
| _ ->
eprintf "%s takes one argument\n" prog ;
exit 2
module Verbose = struct let verbose = verbose end
let do_rename name = name
let select_name = fun _ -> true
module LS = LogState.Make(Verbose)
module LL =
LexLog_tools.Make
(struct
let verbose = verbose
let rename = do_rename
let ok = select_name
let hexa = hexa
let int32 = int32
let acceptBig = false
let faulttype = !faulttype
end)
let acceptempty = !acceptempty
let quant = if !forall then "forall" else "exists"
let negate = if !neg then "~" else ""
let zyva log =
let test = match log with
| None -> LL.read_chan "stdin" stdin
| Some log -> LL.read_name log in
(* Dumping of condition *)
let pp_cond =
if !optcond then CondPP.pp_opt
else CondPP.pp_simple in
let pp_cond name bdss =
let pp = pp_cond bdss in
sprintf "%s \"%s%s %s\"" name negate quant pp in
let dump_test chan t =
let bdss = LS.get_bindings t.states in
match bdss with
| [] ->
if acceptempty then
fprintf chan "%s \"%s%s false\"\n" t.tname negate quant
| _ ->
fprintf chan "%s\n" (pp_cond t.tname bdss) in
let dump_log chan = Array.iter (dump_test chan) in
dump_log stdout test.tests ;
flush stdout ;
()
let () =
try zyva log
with Misc.Fatal msg|Misc.UserError msg ->
eprintf "Fatal error: %s\n%!" msg
|
