Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / tiny / tiny_verifier.ml @ 25537a17

History | View | Annotate | Download (5.63 KB)

1

    
2
let active = ref false
3
let tiny_debug = ref false
4
let tiny_help = ref false
5
let descending = ref 1
6
let unrolling = ref 0
7
let output = ref false
8

    
9
              
10
let quiet () = Tiny.Report.verbosity := 0
11
             
12
let print_tiny_help () =
13
  let open Format in
14
  Format.eprintf "@[Tiny verifier plugin produces a simple imperative code \
15
          output for the provided main node, inlining all calls. This \
16
          code can then be analyzed using tiny analyzer options.@]";
17
  Format.eprintf "@.@?";
18
  flush stdout
19

    
20
  
21
let tiny_run ~basename prog machines =
22
  if !tiny_help then (
23
    let _ = print_tiny_help () in
24
    exit 0
25
  );
26
  let node_name =
27
    match !Options.main_node with
28
    | "" -> (
29
      Format.eprintf "Tiny verifier requires a main node.@.";
30
      Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
31
        (Utils.fprintf_list ~sep:"@ "
32
           (fun fmt m ->
33
             Format.fprintf fmt "%s" m.Machine_code_types.mname.node_id
34
           )
35
        )
36
        machines; 
37
      exit 1
38
    )
39
    | s -> ( (* should have been addessed before *)
40
      match Machine_code_common.get_machine_opt machines s with
41
      | None -> begin
42
          Global.main_node := s;
43
          Format.eprintf "Code generation error: %a@." Error.pp_error_msg Error.Main_not_found;
44
          raise (Error.Error (Location.dummy_loc, Error.Main_not_found))
45
        end
46
      | Some _ -> s
47
    )
48
  in
49
  let m = Machine_code_common.get_machine machines node_name in
50
  let env = (* We add each variables of the node the Tiny env *)
51
    Tiny_utils.machine_to_env m in
52
  let nd = m.mname in
53
  (* Building preamble with some bounds on inputs *)
54
  (* TODO: deal woth contracts, asserts, ... *)
55
  let bounds_inputs = [] in
56
  let ast = Tiny_utils.machine_to_ast bounds_inputs m in
57
  let mems = m.mmemory in
58
  if !output then (
59
    let destname = !Options.dest_dir ^ "/" ^ basename ^ "_" ^ node_name ^ ".tiny" in
60
    Log.report ~plugin:"tiny" ~level:1 (fun fmt -> Format.fprintf fmt "Exporting resulting tiny source as %s@ " destname);
61
    let out = open_out destname in
62
    let fmt = Format.formatter_of_out_channel out in
63
    Format.fprintf fmt "%a@." Tiny.Ast.VarSet.pp env; 
64
    Format.fprintf fmt "%a@." Tiny.Ast.fprint_stm ast; 
65
    close_out out;
66
  
67
  
68
  );
69
  Format.printf "%a@." Tiny.Ast.fprint_stm ast; 
70
  
71
  let dom =
72
     let open Tiny.Load_domains in
73
     prepare_domains (List.map get_domain !domains)
74
   in
75
   let results = Tiny.Analyze.analyze dom !descending !unrolling env ast in
76
   let module Results = (val results: Tiny.Analyze.Results) in
77
   let module Dom = Results.Dom in
78
   let module PrintResults = Tiny.PrintResults.Make (Dom) in
79
   let m = Results.results in
80
   (* if !Tiny.Report.verbosity > 1 then *)
81
   PrintResults.print m env ast None (* no !output_file *);
82
        (* else PrintResults.print_invariants m ast !output_file *)
83

    
84
   ()
85
  
86
  
87
module Verifier =
88
  (struct
89
    include VerifierType.Default
90
    let name = "tiny"
91
    let options =
92
      [
93
        "-debug", Arg.Set tiny_debug, "tiny debug";
94
        ("-abstract-domain", Arg.String Tiny.Load_domains.decl_domain,
95
         "<domain>  Use abstract domain <domain> " ^ Tiny.Domains.available_domains_str);
96
        (* ("-a", Arg.String Tiny.Load_domains.decl_domain,
97
         *  "<domain>  Use abstract domain <domain> " ^ Tiny.Domains.available_domains_str); *)
98
        ("-param", Arg.String Tiny.Load_domains.set_param,
99
         "<p>  Send <p> to the abstract domain, syntax <dom>:<p> can be used \
100
          to target the (sub)domain <dom>");
101
        (* ("-p", Arg.String Tiny.Load_domains.set_param,
102
         *  "<p>  Send <p> to the abstract domain, syntax <dom>:<p> can be used \
103
         *   to target the (sub)domain <dom>"); *)
104
        ("-help-domain", Arg.String Tiny.Load_domains.help_domain,
105
         "<domain>  Print params of <domain>");
106
        (* ("-h", Arg.String Tiny.Load_domains.help_domain, "<domain>  Print params of <domain>"); *)
107
        (* ("--compile", Arg.Set compile_mode, " Compilation mode: compile to C");
108
      ("-c", Arg.Set compile_mode,             " Compilation mode: compile to C");*)
109
        
110
        ("-quiet", Arg.Unit quiet, " Quiet mode");
111
        (* ("-q", Arg.Unit quiet, " Quiet mode"); *)
112
        ("-verbose", Arg.Set_int Tiny.Report.verbosity,
113
         "<n>  Verbosity level (default is 1)");
114
        (* ("-v", Arg.Set_int Tiny.Report.verbosity, "<n>  Verbosity level (default is 1)"); *)
115
  (*      ("--output", Arg.String set_output_file,
116
         "<filename> Output results to file <filename> (default is \
117
          standard ouput)");
118
        ("-o", Arg.String set_output_file,
119
         "<filename>  Output results to file <filename> (default is standard ouput)");
120
   *)
121
        ("-descending", Arg.Set_int descending,
122
         "<n>  Perform <n> descending iterations after fixpoint of a loop \
123
          is reached (default is 1)");
124
        (* ("-d", Arg.Set_int descending,
125
         *  "<n>  Perform <n> descending iterations after fixpoint of a loop \
126
         * is reached (default is 1)"); *)
127
      ("-unrolling", Arg.Set_int unrolling,
128
       "<n>  Unroll loops <n> times before computing fixpoint (default is 0)");
129
      ("-output", Arg.Set output,
130
       "<n>  Export resulting tiny file as <name>_<mainnode>.tiny");
131
      (* (\* ("-u", Arg.Set_int unrolling,
132
       *  *  "<n>  Unroll loops <n> times before computing fixpoint (default is 0)"); *\) *)
133
       "-help", Arg.Set tiny_help, "tiny help and usage";
134
        
135
      
136
      ]
137
      
138
    let activate () =
139
      active := true;
140
      (* Options.global_inline := true;
141
       * Options.optimization := 0;
142
       * Options.const_unfold := true; *)
143
      ()
144
      
145
    let is_active () = !active
146
    let run = tiny_run
147
            
148
            
149
  end: VerifierType.S)
150