Project

General

Profile

Download (5.17 KB) Statistics
| Branch: | Tag: | Revision:
1
open Lustrec
2

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

    
9

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

    
21
  
22
let tiny_run ~basename prog machines =
23
  if !tiny_help then (
24
    let _ = print_tiny_help () in
25
    exit 0
26
  );
27
  let node_name =
28
    match !Lustrec.Options.main_node with
29
    | "" -> (
30
      Format.eprintf "Tiny verifier requires a main node.@.";
31
      Format.eprintf "@[<v 2>Available ones are:@ %a@]@.@?"
32
        (Lustrec.Utils.fprintf_list ~sep:"@ "
33
           (fun fmt m ->
34
             Format.fprintf fmt "%s" m.Lustrec.Machine_code_types.mname.node_id
35
           )
36
        )
37
        machines; 
38
      exit 1
39
    )
40
    | s -> ( (* should have been addessed before *)
41
      match Lustrec.Machine_code_common.get_machine_opt machines s with
42
      | None -> begin
43
          Lustrec.Global.main_node := s;
44
          Format.eprintf "Code generation error: %a@."Lustrec.Error.pp_error_msg Lustrec.Error.Main_not_found;
45
          raise (Error.Error (Lustrec.Location.dummy_loc,Lustrec.Error.Main_not_found))
46
        end
47
      | Some _ -> s
48
    )
49
  in
50
  let m = Lustrec.Machine_code_common.get_machine machines node_name in
51
  let env = (* We add each variables of the node the Tiny env *)
52
    Tiny_utils.machine_to_env m in
53
  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
58
  let mems = m.mmemory in
59
  
60
   Format.printf "%a@." Tiny.Ast.fprint_stm ast; 
61

    
62
   let dom =
63
     let open Tiny.Load_domains in
64
     prepare_domains (List.map get_domain !domains)
65
   in
66
   let results = Tiny.Analyze.analyze dom !descending !unrolling env ast in
67
   let module Results = (val results: Tiny.Analyze.Results) in
68
   let module Dom = Results.Dom in
69
   let module PrintResults = Tiny.PrintResults.Make (Dom) in
70
   let m = Results.results in
71
   (* if !Tiny.Report.verbosity > 1 then *)
72
   PrintResults.print m ast None (* no !output_file *);
73
        (* else PrintResults.print_invariants m ast !output_file *)
74

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