1
|
|
2
|
let active = ref false
|
3
|
let tiny_debug = ref false
|
4
|
let tiny_help = ref false
|
5
|
let descending = ref 1
|
6
|
let unrolling = ref 0
|
7
|
let output = ref false
|
8
|
|
9
|
|
10
|
let quiet () = Tiny.Report.verbosity := 0
|
11
|
let report = Tiny_utils.report
|
12
|
|
13
|
let print_tiny_help () =
|
14
|
let open Format in
|
15
|
Format.eprintf "@[Tiny verifier plugin produces a simple imperative code \
|
16
|
output for the provided main node, inlining all calls. This \
|
17
|
code can then be analyzed using tiny analyzer options.@]";
|
18
|
Format.eprintf "@.@?";
|
19
|
flush stdout
|
20
|
|
21
|
|
22
|
let tiny_run ~basename prog machines =
|
23
|
if !tiny_help then (
|
24
|
let _ = print_tiny_help () in
|
25
|
exit 0
|
26
|
);
|
27
|
let node_name =
|
28
|
match !Options.main_node with
|
29
|
| "" -> (
|
30
|
Format.eprintf "Tiny verifier requires a main node.@.";
|
31
|
Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
|
32
|
(Utils.fprintf_list ~sep:"@ "
|
33
|
(fun fmt m ->
|
34
|
Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id
|
35
|
)
|
36
|
)
|
37
|
machines;
|
38
|
exit 1
|
39
|
)
|
40
|
| s -> ( (* should have been addessed before *)
|
41
|
match Machine_code_common.get_machine_opt machines s with
|
42
|
| None -> begin
|
43
|
Global.main_node := s;
|
44
|
Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
|
45
|
raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
|
46
|
end
|
47
|
| Some _ -> s
|
48
|
)
|
49
|
in
|
50
|
let m = Machine_code_common.get_machine machines node_name in
|
51
|
let env = (* We add each variables of the node the Tiny env *)
|
52
|
Tiny_utils.machine_to_env m in
|
53
|
let nd = m.mname in
|
54
|
(* Building preamble with some bounds on inputs *)
|
55
|
(* TODO: deal woth contracts, asserts, ... *)
|
56
|
let bounds_inputs = [] in
|
57
|
let ast = Tiny_utils.machine_to_ast bounds_inputs m in
|
58
|
let mems = m.mmemory in
|
59
|
if !output then (
|
60
|
let destname = !Options.dest_dir ^ "/" ^ basename ^ "_" ^ node_name ^ ".tiny" in
|
61
|
report ~level:2 (fun fmt -> Format.fprintf fmt "Exporting resulting tiny source as %s@ " destname);
|
62
|
let out = open_out destname in
|
63
|
let fmt = Format.formatter_of_out_channel out in
|
64
|
Format.fprintf fmt "%a@." Tiny.Ast.Var.Set.pp env;
|
65
|
Format.fprintf fmt "%a@." Tiny.Ast.fprint_stm ast;
|
66
|
close_out out;
|
67
|
|
68
|
|
69
|
);
|
70
|
report ~level:1 (fun fmt -> Format.fprintf fmt "%a@." Tiny.Ast.fprint_stm ast);
|
71
|
|
72
|
let dom =
|
73
|
let open Tiny.Load_domains in
|
74
|
prepare_domains (List.map get_domain !domains)
|
75
|
in
|
76
|
let results = Tiny.Analyze.analyze dom !descending !unrolling env ast in
|
77
|
let module Results = (val results: Tiny.Analyze.Results) in
|
78
|
let module Dom = Results.Dom in
|
79
|
let module PrintResults = Tiny.PrintResults.Make (Dom) in
|
80
|
let m = Results.results in
|
81
|
(* if !Tiny.Report.verbosity > 1 then *)
|
82
|
report ~level:1 (PrintResults.print m env ast)
|
83
|
(* no !output_file *);
|
84
|
(* else PrintResults.print_invariants m ast !output_file *)
|
85
|
|
86
|
()
|
87
|
|
88
|
|
89
|
module Verifier =
|
90
|
(struct
|
91
|
include VerifierType.Default
|
92
|
let name = "tiny"
|
93
|
let options =
|
94
|
[
|
95
|
"-debug", Arg.Set tiny_debug, "tiny debug";
|
96
|
("-abstract-domain", Arg.String Tiny.Load_domains.decl_domain,
|
97
|
"<domain> Use abstract domain <domain> " ^ Tiny.Domains.available_domains_str);
|
98
|
(* ("-a", Arg.String Tiny.Load_domains.decl_domain,
|
99
|
* "<domain> Use abstract domain <domain> " ^ Tiny.Domains.available_domains_str); *)
|
100
|
("-param", Arg.String Tiny.Load_domains.set_param,
|
101
|
"<p> Send <p> to the abstract domain, syntax <dom>:<p> can be used \
|
102
|
to target the (sub)domain <dom>");
|
103
|
(* ("-p", Arg.String Tiny.Load_domains.set_param,
|
104
|
* "<p> Send <p> to the abstract domain, syntax <dom>:<p> can be used \
|
105
|
* to target the (sub)domain <dom>"); *)
|
106
|
("-help-domain", Arg.String Tiny.Load_domains.help_domain,
|
107
|
"<domain> Print params of <domain>");
|
108
|
(* ("-h", Arg.String Tiny.Load_domains.help_domain, "<domain> Print params of <domain>"); *)
|
109
|
(* ("--compile", Arg.Set compile_mode, " Compilation mode: compile to C");
|
110
|
("-c", Arg.Set compile_mode, " Compilation mode: compile to C");*)
|
111
|
|
112
|
("-quiet", Arg.Unit quiet, " Quiet mode");
|
113
|
(* ("-q", Arg.Unit quiet, " Quiet mode"); *)
|
114
|
("-verbose", Arg.Set_int Tiny.Report.verbosity,
|
115
|
"<n> Verbosity level (default is 1)");
|
116
|
(* ("-v", Arg.Set_int Tiny.Report.verbosity, "<n> Verbosity level (default is 1)"); *)
|
117
|
(* ("--output", Arg.String set_output_file,
|
118
|
"<filename> Output results to file <filename> (default is \
|
119
|
standard ouput)");
|
120
|
("-o", Arg.String set_output_file,
|
121
|
"<filename> Output results to file <filename> (default is standard ouput)");
|
122
|
*)
|
123
|
("-descending", Arg.Set_int descending,
|
124
|
"<n> Perform <n> descending iterations after fixpoint of a loop \
|
125
|
is reached (default is 1)");
|
126
|
(* ("-d", Arg.Set_int descending,
|
127
|
* "<n> Perform <n> descending iterations after fixpoint of a loop \
|
128
|
* is reached (default is 1)"); *)
|
129
|
("-unrolling", Arg.Set_int unrolling,
|
130
|
"<n> Unroll loops <n> times before computing fixpoint (default is 0)");
|
131
|
("-output", Arg.Set output,
|
132
|
"<n> Export resulting tiny file as <name>_<mainnode>.tiny");
|
133
|
(* (\* ("-u", Arg.Set_int unrolling,
|
134
|
* * "<n> Unroll loops <n> times before computing fixpoint (default is 0)"); *\) *)
|
135
|
"-help", Arg.Set tiny_help, "tiny help and usage";
|
136
|
|
137
|
|
138
|
]
|
139
|
|
140
|
let activate () =
|
141
|
active := true;
|
142
|
(* Options.global_inline := true;
|
143
|
* Options.optimization := 0;
|
144
|
* Options.const_unfold := true; *)
|
145
|
()
|
146
|
|
147
|
let is_active () = !active
|
148
|
let run = tiny_run
|
149
|
|
150
|
|
151
|
end: VerifierType.S)
|
152
|
|