Project

General

Profile

Download (5.35 KB) Statistics
| Branch: | Tag: | Revision:
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: *)
(38-38/66)