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