Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/main_lustre_verifier.ml
11 11

  
12 12
open Format
13 13
open Compiler_common
14

  
15 14
open Utils
16 15

  
17

  
18 16
let usage = "Usage: lustrev [options] \x1b[4msource file\x1b[0m"
19 17

  
20
let extensions = [".ec"; ".lus"; ".lusi"]
21

  
18
let extensions = [ ".ec"; ".lus"; ".lusi" ]
22 19

  
23
(* verify a .lus source file 
20
(* verify a .lus source file
24 21

  
25
we have multiple "backends"
26
- 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
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
27 26

  
28
- seal: linked to seal. Require global inline and main node
29
  focuses only on the selected node (the main)
30
  map the machine code into SEAL datastructure and compute invariants
31
  - provides the node and its information (typical point of interest for taylor expansion, range for inputs, existing invariants, computation error for the node content)
32
  - simplification of program through taylor expansion
33
  - scaling when provided with typical ranges (not required to be sound for the moment)
34
  - computation of lyapunov invariants
35
  - returns an annotated node with invariants and a JSON to explain computation
36
  - could also returns plots
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
37 36

  
38
- tiny: linked to tiny library to perform floating point analyses
39
  shall be provided with ranges for inputs or local variables (memories)
40
  
41
*)
37
   - tiny: linked to tiny library to perform floating point analyses shall be
38
   provided with ranges for inputs or local variables (memories) *)
42 39
let verify dirname basename extension =
43 40
  let source_name = dirname ^ "/" ^ basename ^ extension in
44
  Options.compile_header := false; (* to avoid producing .h / .lusic *)
41
  Options.compile_header := false;
42
  (* to avoid producing .h / .lusic *)
45 43
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");
46 44
  decr Options.verbose_level;
47 45

  
......
52 50
  incr Options.verbose_level;
53 51
  let verifier = Verifiers.get_active () in
54 52
  let module Verifier = (val verifier : VerifierType.S) in
55

  
56 53
  decr Options.verbose_level;
57 54
  let params = Verifier.get_normalization_params () in
58 55
  (* Normalizing it *)
59 56
  let prog, _ =
60
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
57
    Log.report ~level:1 (fun fmt ->
58
        fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
61 59
    try
62 60
      incr Options.verbose_level;
63 61
      decr Options.verbose_level;
64 62
      Compiler_stages.stage1 params prog dirname basename extension
65
    with Compiler_stages.StopPhase1 prog -> (
63
    with Compiler_stages.StopPhase1 prog ->
66 64
      if !Options.print_nodes then (
67 65
        Format.printf "%a@.@?" Printers.pp_node_list prog;
68
        exit 0
69
      )
70
      else
71
        assert false
72
    )
66
        exit 0)
67
      else assert false
73 68
  in
74 69
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@,");
75
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Normalized program:@ %a@ "Printers.pp_prog prog);
70
  Log.report ~level:3 (fun fmt ->
71
      fprintf fmt ".. Normalized program:@ %a@ " Printers.pp_prog prog);
76 72

  
77
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
73
  Log.report ~level:1 (fun fmt ->
74
      fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
78 75

  
79
  let prog, machine_code = 
80
    Compiler_stages.stage2 params prog 
81
  in
76
  let prog, machine_code = Compiler_stages.stage2 params prog in
82 77

  
83 78
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
84
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ "
85
                                    Machine_code_common.pp_machines machine_code);
86
  
87
  if Scopes.Plugin.show_scopes () then
88
    begin
89
      let all_scopes = Scopes.compute_scopes prog !Options.main_node in
90
      (* Printing scopes *)
91
      if !Options.verbose_level >= 1 then
92
	Format.printf "Possible scopes are:@   ";
93
      Format.printf "@[<v>%a@ @]@ @?" Scopes.print_scopes all_scopes;
94
      exit 0
95
	
96
    end;
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);
97 89

  
98 90
  let machine_code = Plugins.refine_machine_code prog machine_code in
99 91

  
100 92
  (*assert (dependencies = []); (* Do not handle deps yet *)*)
101 93
  incr Options.verbose_level;
102 94
  Verifier.run ~basename prog machine_code;
103
  begin
104
    decr Options.verbose_level;
105
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ ");
106
    incr Options.verbose_level;
107
    Log.report ~level:1 (fun fmt -> fprintf fmt "@]@.");
108
    (* We stop the process here *)
109
    exit 0
110
  end
111

  
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
112 101

  
113 102
let anonymous filename =
114
  let ok_ext, ext = List.fold_left
115
    (fun (ok, ext) ext' ->
116
      if not ok && Filename.check_suffix filename ext' then
117
	true, ext'
118
      else
119
	ok, ext)
120
    (false, "") extensions in
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
121 110
  if ok_ext then
122 111
    let dirname = Filename.dirname filename in
123 112
    let basename = Filename.chop_suffix (Filename.basename filename) ext in
124 113
    verify dirname basename ext
125
  else
126
    raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
114
  else raise (Arg.Bad "Can only compile *.lusi, *.lus or *.ec files")
127 115

  
128 116
let _ =
129 117
  Global.initialize ();
......
131 119
  try
132 120
    Printexc.record_backtrace true;
133 121

  
134
    let options = Options_management.lustrev_options @ (Verifiers.options ()) in
135
    
122
    let options = Options_management.lustrev_options @ Verifiers.options () in
123

  
136 124
    Arg.parse options anonymous usage
137 125
  with
138
  | Parse.Error | Types.Error (_,_) | Clocks.Error (_,_) ->
126
  | Parse.Error | Types.Error (_, _) | Clocks.Error (_, _) ->
139 127
    exit 1
140
  | Error.Error (loc , kind) (*| Task_set.Error _*) -> 
128
  | Error.Error (loc, kind) (*| Task_set.Error _*) ->
141 129
    Error.pp_error loc (fun fmt -> Error.pp_error_msg fmt kind);
142 130
    exit (Error.return_code kind)
143
  (* | Causality.Error _  -> exit (Error.return_code Error.AlgebraicLoop) *)
131
  (* | Causality.Error _ -> exit (Error.return_code Error.AlgebraicLoop) *)
144 132
  | Sys_error msg ->
145
    (eprintf "Failure: %s@." msg); exit 1
133
    eprintf "Failure: %s@." msg;
134
    exit 1
146 135
  | exc ->
147
    (track_exception (); raise exc)
136
    track_exception ();
137
    raise exc
148 138

  
149
             (* Local Variables: *)
150
             (* compile-command:"make -C .." *)
151
             (* End: *)
139
(* Local Variables: *)
140
(* compile-command:"make -C .." *)
141
(* End: *)

Also available in: Unified diff