lustrec / src / main_lustre_verifier.ml @ a0c92fa8
History | View | Annotate | Download (5.49 KB)
1 |
(********************************************************************) |
---|---|
2 |
(* *) |
3 |
(* The LustreC compiler toolset / The LustreC Development Team *) |
4 |
(* Copyright 2012 - -- ONERA - CNRS - INPT *) |
5 |
(* *) |
6 |
(* LustreC is free software, distributed WITHOUT ANY WARRANTY *) |
7 |
(* under the terms of the GNU Lesser General Public License *) |
8 |
(* version 2.1. *) |
9 |
(* *) |
10 |
(********************************************************************) |
11 |
|
12 |
open Format |
13 |
open Log |
14 |
open Compiler_common |
15 |
|
16 |
open Utils |
17 |
open Lustre_types |
18 |
|
19 |
|
20 |
let usage = "Usage: lustrev [options] \x1b[4msource file\x1b[0m" |
21 |
|
22 |
let extensions = [".ec"; ".lus"; ".lusi"] |
23 |
|
24 |
|
25 |
(* verify a .lus source file |
26 |
|
27 |
we have multiple "backends" |
28 |
- zustre: linked to z3/spacer. Shall preserve the structure and rely on contracts. Produces both a lustre model with new properties, maybe as a lusi with lustre contract, and a JSON summarizing the results and providing tests cases or counter examples if any |
29 |
|
30 |
- seal: linked to seal. Require global inline and main node |
31 |
focuses only on the selected node (the main) |
32 |
map the machine code into SEAL datastructure and compute invariants |
33 |
- provides the node and its information (typical point of interest for taylor expansion, range for inputs, existing invariants, computation error for the node content) |
34 |
- simplification of program through taylor expansion |
35 |
- scaling when provided with typical ranges (not required to be sound for the moment) |
36 |
- computation of lyapunov invariants |
37 |
- returns an annotated node with invariants and a JSON to explain computation |
38 |
- could also returns plots |
39 |
|
40 |
- tiny: linked to tiny library to perform floating point analyses |
41 |
shall be provided with ranges for inputs or local variables (memories) |
42 |
|
43 |
*) |
44 |
let rec verify dirname basename extension = |
45 |
let source_name = dirname ^ "/" ^ basename ^ extension in |
46 |
Options.compile_header := false; (* to avoid producing .h / .lusic *) |
47 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>"); |
48 |
decr Options.verbose_level; |
49 |
|
50 |
(* Parsing source *) |
51 |
let prog = parse source_name extension in |
52 |
|
53 |
(* Checking which solver is active *) |
54 |
incr Options.verbose_level; |
55 |
let verifier = Verifiers.get_active () in |
56 |
let module Verifier = (val verifier : VerifierType.S) in |
57 |
|
58 |
decr Options.verbose_level; |
59 |
let params = Verifier.get_normalization_params () in |
60 |
(* Normalizing it *) |
61 |
let prog, dependencies = |
62 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,"); |
63 |
try |
64 |
incr Options.verbose_level; |
65 |
decr Options.verbose_level; |
66 |
Compiler_stages.stage1 params prog dirname basename extension |
67 |
with Compiler_stages.StopPhase1 prog -> ( |
68 |
if !Options.print_nodes then ( |
69 |
Format.printf "%a@.@?" Printers.pp_node_list prog; |
70 |
exit 0 |
71 |
) |
72 |
else |
73 |
assert false |
74 |
) |
75 |
in |
76 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@,"); |
77 |
Log.report ~level:3 (fun fmt -> fprintf fmt ".. Normalized program:@ %a@ "Printers.pp_prog prog); |
78 |
|
79 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,"); |
80 |
|
81 |
let prog, machine_code = |
82 |
Compiler_stages.stage2 params prog |
83 |
in |
84 |
|
85 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ "); |
86 |
Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ " |
87 |
Machine_code_common.pp_machines machine_code); |
88 |
|
89 |
if Scopes.Plugin.show_scopes () then |
90 |
begin |
91 |
let all_scopes = Scopes.compute_scopes prog !Options.main_node in |
92 |
(* Printing scopes *) |
93 |
if !Options.verbose_level >= 1 then |
94 |
Format.printf "Possible scopes are:@ "; |
95 |
Format.printf "@[<v>%a@ @]@ @?" Scopes.print_scopes all_scopes; |
96 |
exit 0 |
97 |
|
98 |
end; |
99 |
|
100 |
let machine_code = Plugins.refine_machine_code prog machine_code in |
101 |
|
102 |
(*assert (dependencies = []); (* Do not handle deps yet *)*) |
103 |
incr Options.verbose_level; |
104 |
Verifier.run basename prog machine_code; |
105 |
begin |
106 |
decr Options.verbose_level; |
107 |
Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ "); |
108 |
incr Options.verbose_level; |
109 |
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@."); |
110 |
(* We stop the process here *) |
111 |
exit 0 |
112 |
end |
113 |
|
114 |
|
115 |
let anonymous filename = |
116 |
let ok_ext, ext = List.fold_left |
117 |
(fun (ok, ext) ext' -> |
118 |
if not ok && Filename.check_suffix filename ext' then |
119 |
true, ext' |
120 |
else |
121 |
ok, ext) |
122 |
(false, "") extensions in |
123 |
if ok_ext then |
124 |
let dirname = Filename.dirname filename in |
125 |
let basename = Filename.chop_suffix (Filename.basename filename) ext in |
126 |
verify dirname basename ext |
127 |
else |
128 |
raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files")) |
129 |
|
130 |
let _ = |
131 |
Global.initialize (); |
132 |
Corelang.add_internal_funs (); |
133 |
try |
134 |
Printexc.record_backtrace true; |
135 |
|
136 |
let options = Options_management.lustrev_options @ (Verifiers.options ()) in |
137 |
|
138 |
Arg.parse options anonymous usage |
139 |
with |
140 |
| Parse.Error _ |
141 |
| Types.Error (_,_) | Clocks.Error (_,_) -> exit 1 |
142 |
| Error.Error (loc , kind) (*| Task_set.Error _*) -> |
143 |
Error.pp_error loc (fun fmt -> Error.pp_error_msg fmt kind); |
144 |
exit (Error.return_code kind) |
145 |
(* | Causality.Error _ -> exit (Error.return_code Error.AlgebraicLoop) *) |
146 |
| Sys_error msg -> (eprintf "Failure: %s@." msg); exit 1 |
147 |
| exc -> (track_exception (); raise exc) |
148 |
|
149 |
(* Local Variables: *) |
150 |
(* compile-command:"make -C .." *) |
151 |
(* End: *) |