Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / plugins / tiny / tiny_verifier.ml @ 9b0432bc

History | View | Annotate | Download (6.66 KB)

1 9c4cc944 Corentin Lauverjat
open Lustrec
2 9b0432bc Corentin Lauverjat
open Backends
3 f0195e96 ploc
4
let active = ref false
5
let tiny_debug = ref false
6 9b0432bc Corentin Lauverjat
let tiny_output = ref false
7 58fd528a ploc
let tiny_help = ref false
8
let descending = ref 1
9 9b0432bc Corentin Lauverjat
let unrolling = ref 1
10
let bounds_file = ref ""
11 f0195e96 ploc
12 58fd528a ploc
13
              
14
let quiet () = Tiny.Report.verbosity := 0
15
             
16
let print_tiny_help () =
17
  let open Format in
18
  Format.eprintf "@[Tiny verifier plugin produces a simple imperative code \
19
          output for the provided main node, inlining all calls. This \
20
          code can then be analyzed using tiny analyzer options.@]";
21
  Format.eprintf "@.@?";
22
  flush stdout
23
24 9b0432bc Corentin Lauverjat
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
32 f0195e96 ploc
let tiny_run ~basename prog machines =
33 58fd528a ploc
  if !tiny_help then (
34
    let _ = print_tiny_help () in
35
    exit 0
36
  );
37 9b0432bc Corentin Lauverjat
  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 
45 f0195e96 ploc
  let node_name =
46 9c4cc944 Corentin Lauverjat
    match !Lustrec.Options.main_node with
47 f0195e96 ploc
    | "" -> (
48
      Format.eprintf "Tiny verifier requires a main node.@.";
49
      Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
50 9c4cc944 Corentin Lauverjat
        (Lustrec.Utils.fprintf_list ~sep:"@ "
51 f0195e96 ploc
           (fun fmt m ->
52 9c4cc944 Corentin Lauverjat
             Format.fprintf fmt "%s" m.Lustrec.Machine_code_types.mname.node_id
53 f0195e96 ploc
           )
54
        )
55
        machines; 
56
      exit 1
57
    )
58
    | s -> ( (* should have been addessed before *)
59 9c4cc944 Corentin Lauverjat
      match Lustrec.Machine_code_common.get_machine_opt machines s with
60 f0195e96 ploc
      | None -> begin
61 9c4cc944 Corentin Lauverjat
          Lustrec.Global.main_node := s;
62
          Format.eprintf "Code generation error: %a@."Lustrec.Error.pp_error_msg Lustrec.Error.Main_not_found;
63
          raise (Error.Error (Lustrec.Location.dummy_loc,Lustrec.Error.Main_not_found))
64 f0195e96 ploc
        end
65
      | Some _ -> s
66
    )
67
  in
68 9c4cc944 Corentin Lauverjat
  let m = Lustrec.Machine_code_common.get_machine machines node_name in
69 f0195e96 ploc
  let env = (* We add each variables of the node the Tiny env *)
70
    Tiny_utils.machine_to_env m in
71
  let nd = m.mname in
72 9b0432bc Corentin Lauverjat
  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
78 f0195e96 ploc
  let mems = m.mmemory in
79
  
80 9b0432bc Corentin Lauverjat
   Format.printf "%a@." Tiny.Ast.fprint_stm tiny_encoding.ast; 
81 f0195e96 ploc
82 58fd528a ploc
   let dom =
83
     let open Tiny.Load_domains in
84
     prepare_domains (List.map get_domain !domains)
85
   in
86 9b0432bc Corentin Lauverjat
   let results = Tiny.Analyze.analyze dom !descending !unrolling env tiny_encoding.ast in
87 58fd528a ploc
   let module Results = (val results: Tiny.Analyze.Results) in
88
   let module Dom = Results.Dom in
89 9b0432bc Corentin Lauverjat
   let module JsonResults = Tiny_results.Make (Dom) in
90 58fd528a ploc
   let m = Results.results in
91
   (* if !Tiny.Report.verbosity > 1 then *)
92 9b0432bc Corentin Lauverjat
   (* 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
100 58fd528a ploc
101 f0195e96 ploc
  
102
module Verifier =
103
  (struct
104
    include VerifierType.Default
105
    let name = "tiny"
106
    let options =
107
      [
108 58fd528a ploc
        "-debug", Arg.Set tiny_debug, "tiny debug";
109
        ("-abstract-domain", Arg.String Tiny.Load_domains.decl_domain,
110
         "<domain>  Use abstract domain <domain> " ^ Tiny.Domains.available_domains_str);
111
        (* ("-a", Arg.String Tiny.Load_domains.decl_domain,
112
         *  "<domain>  Use abstract domain <domain> " ^ Tiny.Domains.available_domains_str); *)
113
        ("-param", Arg.String Tiny.Load_domains.set_param,
114
         "<p>  Send <p> to the abstract domain, syntax <dom>:<p> can be used \
115
          to target the (sub)domain <dom>");
116
        (* ("-p", Arg.String Tiny.Load_domains.set_param,
117
         *  "<p>  Send <p> to the abstract domain, syntax <dom>:<p> can be used \
118
         *   to target the (sub)domain <dom>"); *)
119
        ("-help-domain", Arg.String Tiny.Load_domains.help_domain,
120
         "<domain>  Print params of <domain>");
121
        (* ("-h", Arg.String Tiny.Load_domains.help_domain, "<domain>  Print params of <domain>"); *)
122
        (* ("--compile", Arg.Set compile_mode, " Compilation mode: compile to C");
123
      ("-c", Arg.Set compile_mode,             " Compilation mode: compile to C");*)
124 9b0432bc Corentin Lauverjat
        ("-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";
129 58fd528a ploc
        ("-quiet", Arg.Unit quiet, " Quiet mode");
130
        (* ("-q", Arg.Unit quiet, " Quiet mode"); *)
131
        ("-verbose", Arg.Set_int Tiny.Report.verbosity,
132
         "<n>  Verbosity level (default is 1)");
133
        (* ("-v", Arg.Set_int Tiny.Report.verbosity, "<n>  Verbosity level (default is 1)"); *)
134
  (*      ("--output", Arg.String set_output_file,
135
         "<filename> Output results to file <filename> (default is \
136
          standard ouput)");
137
        ("-o", Arg.String set_output_file,
138
         "<filename>  Output results to file <filename> (default is standard ouput)");
139
   *)
140 9b0432bc Corentin Lauverjat
      (*  ("-descending", Arg.Set_int descending,
141 58fd528a ploc
         "<n>  Perform <n> descending iterations after fixpoint of a loop \
142 9b0432bc Corentin Lauverjat
          is reached (default is 1)");*)
143 58fd528a ploc
        (* ("-d", Arg.Set_int descending,
144
         *  "<n>  Perform <n> descending iterations after fixpoint of a loop \
145
         * is reached (default is 1)"); *)
146 9b0432bc Corentin Lauverjat
      ("-duration", Arg.Set_int unrolling,
147
       "<n>  Duration, the number of steps of the simulation");
148 58fd528a ploc
      (* (\* ("-u", Arg.Set_int unrolling,
149
       *  *  "<n>  Unroll loops <n> times before computing fixpoint (default is 0)"); *\) *)
150
       "-help", Arg.Set tiny_help, "tiny help and usage";
151
        
152
      
153 f0195e96 ploc
      ]
154
      
155
    let activate () =
156
      active := true;
157 9b0432bc Corentin Lauverjat
      Lustrec.Options.output := "tiny";
158
      Lustrec.Options.global_inline := true;
159
      Lustrec.Options.optimization := 0;
160
      Lustrec.Options.const_unfold := true;
161 f0195e96 ploc
      ()
162
      
163
    let is_active () = !active
164
    let run = tiny_run
165
            
166
            
167
  end: VerifierType.S)
168