Project

General

Profile

Revision 9b0432bc plugins/tiny/tiny_verifier.ml

View differences:

plugins/tiny/tiny_verifier.ml
1 1
open Lustrec
2
open Backends
2 3

  
3 4
let active = ref false
4 5
let tiny_debug = ref false
6
let tiny_output = ref false
5 7
let tiny_help = ref false
6 8
let descending = ref 1
7
let unrolling = ref 0
9
let unrolling = ref 1
10
let bounds_file = ref ""
8 11

  
9 12

  
10 13
              
......
18 21
  Format.eprintf "@.@?";
19 22
  flush stdout
20 23

  
21
  
24
let generate_tiny_analysis_file basename json_tiny_analysis = 
25
  let path = !Lustrec.Options.dest_dir ^ "/" ^ basename in
26
  let destname = path ^ "_tiny.json" in 
27
  let file = open_out destname in
28
  let file_fmt = Format.formatter_of_out_channel file in
29
  Yojson.pretty_print file_fmt json_tiny_analysis;
30
  close_out file;;
31

  
22 32
let tiny_run ~basename prog machines =
23 33
  if !tiny_help then (
24 34
    let _ = print_tiny_help () in
25 35
    exit 0
26 36
  );
37
  if !bounds_file = "" then 
38
    failwith "-tiny-bounds-file <filepath> need to be set";
39
  let bound_input_file_path = !Lustrec.Options.dest_dir ^ "/" ^ !bounds_file in 
40
  let in_chan_bounds = try
41
  open_in bound_input_file_path
42
  with 
43
  | Sys_error _ -> (Format.printf "%s is not a valid path to the JSON formatted bounds constraint" bound_input_file_path; exit 2)
44
  in 
27 45
  let node_name =
28 46
    match !Lustrec.Options.main_node with
29 47
    | "" -> (
......
51 69
  let env = (* We add each variables of the node the Tiny env *)
52 70
    Tiny_utils.machine_to_env m in
53 71
  let nd = m.mname in
54
  (* Building preamble with some bounds on inputs *)
55
  (* TODO: deal woth contracts, asserts, ... *)
56
  let bounds_inputs = [] in
57
  let ast = Tiny_utils.machine_to_ast bounds_inputs m in
72
  let json_input = Yojson.Safe.from_channel in_chan_bounds in
73
  let bounds_inputs = Tiny_utils.bounds_of_yojson json_input in
74
  let bounds_inputs  = match bounds_inputs with 
75
  | Error e -> failwith e 
76
  | Ok v -> v in
77
  let tiny_encoding = Tiny_utils.machine_to_tiny_encoding bounds_inputs m in
58 78
  let mems = m.mmemory in
59 79
  
60
   Format.printf "%a@." Tiny.Ast.fprint_stm ast; 
80
   Format.printf "%a@." Tiny.Ast.fprint_stm tiny_encoding.ast; 
61 81

  
62 82
   let dom =
63 83
     let open Tiny.Load_domains in
64 84
     prepare_domains (List.map get_domain !domains)
65 85
   in
66
   let results = Tiny.Analyze.analyze dom !descending !unrolling env ast in
86
   let results = Tiny.Analyze.analyze dom !descending !unrolling env tiny_encoding.ast in
67 87
   let module Results = (val results: Tiny.Analyze.Results) in
68 88
   let module Dom = Results.Dom in
69
   let module PrintResults = Tiny.PrintResults.Make (Dom) in
89
   let module JsonResults = Tiny_results.Make (Dom) in
70 90
   let m = Results.results in
71 91
   (* if !Tiny.Report.verbosity > 1 then *)
72
   PrintResults.print m ast None (* no !output_file *);
73
        (* else PrintResults.print_invariants m ast !output_file *)
92
   (* PrintResults.print m tiny_encoding.ast None (* no !output_file *); *)
93
  (* Print result analysis in JSON format on stdout *)
94
  let json_result = JsonResults.to_json m tiny_encoding in 
95
  begin 
96
    Yojson.pretty_print Format.std_formatter json_result;
97
    if !tiny_output then generate_tiny_analysis_file basename json_result;
98
  end;
99

  
74 100

  
75
   ()
76
  
77 101
  
78 102
module Verifier =
79 103
  (struct
......
97 121
        (* ("-h", Arg.String Tiny.Load_domains.help_domain, "<domain>  Print params of <domain>"); *)
98 122
        (* ("--compile", Arg.Set compile_mode, " Compilation mode: compile to C");
99 123
      ("-c", Arg.Set compile_mode,             " Compilation mode: compile to C");*)
100
        
124
        ("-bounds-file", Arg.Set_string bounds_file,
125
        "Path to the file containing constraints on input of the lustre code. The content of the file \
126
        must be a valid JSON containing an array of object with the following prototype : \
127
         {\"var_name\": string, \"type\": string, \"inf\": string, \"sup\": string}");
128
        "-output", Arg.Set tiny_output, "generate a __tiny_analysis.json";
101 129
        ("-quiet", Arg.Unit quiet, " Quiet mode");
102 130
        (* ("-q", Arg.Unit quiet, " Quiet mode"); *)
103 131
        ("-verbose", Arg.Set_int Tiny.Report.verbosity,
......
109 137
        ("-o", Arg.String set_output_file,
110 138
         "<filename>  Output results to file <filename> (default is standard ouput)");
111 139
   *)
112
        ("-descending", Arg.Set_int descending,
140
      (*  ("-descending", Arg.Set_int descending,
113 141
         "<n>  Perform <n> descending iterations after fixpoint of a loop \
114
          is reached (default is 1)");
142
          is reached (default is 1)");*)
115 143
        (* ("-d", Arg.Set_int descending,
116 144
         *  "<n>  Perform <n> descending iterations after fixpoint of a loop \
117 145
         * is reached (default is 1)"); *)
118
      ("-unrolling", Arg.Set_int unrolling,
119
       "<n>  Unroll loops <n> times before computing fixpoint (default is 0)");
146
      ("-duration", Arg.Set_int unrolling,
147
       "<n>  Duration, the number of steps of the simulation");
120 148
      (* (\* ("-u", Arg.Set_int unrolling,
121 149
       *  *  "<n>  Unroll loops <n> times before computing fixpoint (default is 0)"); *\) *)
122 150
       "-help", Arg.Set tiny_help, "tiny help and usage";
......
126 154
      
127 155
    let activate () =
128 156
      active := true;
129
      (* Lustrec.Options.global_inline := true;
130
       * Lustrec.Options.optimization := 0;
131
       * Lustrec.Options.const_unfold := true; *)
157
      Lustrec.Options.output := "tiny";
158
      Lustrec.Options.global_inline := true;
159
      Lustrec.Options.optimization := 0;
160
      Lustrec.Options.const_unfold := true;
132 161
      ()
133 162
      
134 163
    let is_active () = !active

Also available in: Unified diff