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
|
|
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
|
(* Normalizing it *)
|
60
|
let prog, dependencies =
|
61
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
|
62
|
try
|
63
|
incr Options.verbose_level;
|
64
|
let params = Verifier.get_normalization_params () in
|
65
|
decr Options.verbose_level;
|
66
|
Compiler_stages.stage1 params prog dirname basename extension
|
67
|
with Compiler_stages.StopPhase1 prog -> (
|
68
|
assert false
|
69
|
)
|
70
|
in
|
71
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@,");
|
72
|
Log.report ~level:3 (fun fmt -> fprintf fmt ".. Normalized program:@ %a@ "Printers.pp_prog prog);
|
73
|
|
74
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
|
75
|
|
76
|
let machine_code =
|
77
|
Compiler_stages.stage2 prog
|
78
|
in
|
79
|
|
80
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
|
81
|
Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ "Machine_code_common.pp_machines machine_code);
|
82
|
|
83
|
if Scopes.Plugin.show_scopes () then
|
84
|
begin
|
85
|
let all_scopes = Scopes.compute_scopes prog !Options.main_node in
|
86
|
(* Printing scopes *)
|
87
|
if !Options.verbose_level >= 1 then
|
88
|
Format.printf "Possible scopes are:@ ";
|
89
|
Format.printf "@[<v>%a@ @]@ @?" Scopes.print_scopes all_scopes;
|
90
|
exit 0
|
91
|
|
92
|
end;
|
93
|
|
94
|
let machine_code = Plugins.refine_machine_code prog machine_code in
|
95
|
|
96
|
assert (dependencies = []); (* Do not handle deps yet *)
|
97
|
incr Options.verbose_level;
|
98
|
Verifier.run basename prog machine_code;
|
99
|
begin
|
100
|
decr Options.verbose_level;
|
101
|
Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ ");
|
102
|
incr Options.verbose_level;
|
103
|
Log.report ~level:1 (fun fmt -> fprintf fmt "@]@.");
|
104
|
(* We stop the process here *)
|
105
|
exit 0
|
106
|
end
|
107
|
|
108
|
|
109
|
let anonymous filename =
|
110
|
let ok_ext, ext = List.fold_left
|
111
|
(fun (ok, ext) ext' ->
|
112
|
if not ok && Filename.check_suffix filename ext' then
|
113
|
true, ext'
|
114
|
else
|
115
|
ok, ext)
|
116
|
(false, "") extensions in
|
117
|
if ok_ext then
|
118
|
let dirname = Filename.dirname filename in
|
119
|
let basename = Filename.chop_suffix (Filename.basename filename) ext in
|
120
|
verify dirname basename ext
|
121
|
else
|
122
|
raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
|
123
|
|
124
|
let _ =
|
125
|
Global.initialize ();
|
126
|
Corelang.add_internal_funs ();
|
127
|
try
|
128
|
Printexc.record_backtrace true;
|
129
|
|
130
|
let options = Options_management.lustrev_options @ (Verifiers.options ()) in
|
131
|
|
132
|
Arg.parse options anonymous usage
|
133
|
with
|
134
|
| Parse.Error _
|
135
|
| Types.Error (_,_) | Clocks.Error (_,_) -> exit 1
|
136
|
| Corelang.Error (_ (* loc *), kind) (*| Task_set.Error _*) -> exit (Error.return_code kind)
|
137
|
(* | Causality.Error _ -> exit (Error.return_code Error.AlgebraicLoop) *)
|
138
|
| Sys_error msg -> (eprintf "Failure: %s@." msg); exit 1
|
139
|
| exc -> (track_exception (); raise exc)
|
140
|
|
141
|
(* Local Variables: *)
|
142
|
(* compile-command:"make -C .." *)
|
143
|
(* End: *)
|