Revision ca7ff3f7
Added by Lélio Brun 8 months 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