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