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