Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/tools/tiny/tiny_verifier.ml
1

  
2 1
let active = ref false
2

  
3 3
let tiny_debug = ref false
4

  
4 5
let tiny_help = ref false
6

  
5 7
let descending = ref 1
6
let unrolling = ref 0
7 8

  
9
let unrolling = ref 0
8 10

  
9
              
10 11
let quiet () = Tiny.Report.verbosity := 0
11
             
12

  
12 13
let print_tiny_help () =
13 14
  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.@]";
15
  Format.eprintf
16
    "@[Tiny verifier plugin produces a simple imperative code output for the \
17
     provided main node, inlining all calls. This code can then be analyzed \
18
     using tiny analyzer options.@]";
17 19
  Format.eprintf "@.@?";
18 20
  flush stdout
19 21

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

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

  
74
   ()
75
  
76
  
77
module Verifier =
78
  (struct
79
    include VerifierType.Default
80
    let name = "tiny"
81
    let options =
82
      [
83
        "-debug", Arg.Set tiny_debug, "tiny debug";
84
        ("-abstract-domain", Arg.String Tiny.Load_domains.decl_domain,
85
         "<domain>  Use abstract domain <domain> " ^ Tiny.Domains.available_domains_str);
86
        (* ("-a", Arg.String Tiny.Load_domains.decl_domain,
87
         *  "<domain>  Use abstract domain <domain> " ^ Tiny.Domains.available_domains_str); *)
88
        ("-param", Arg.String Tiny.Load_domains.set_param,
89
         "<p>  Send <p> to the abstract domain, syntax <dom>:<p> can be used \
90
          to target the (sub)domain <dom>");
91
        (* ("-p", Arg.String Tiny.Load_domains.set_param,
92
         *  "<p>  Send <p> to the abstract domain, syntax <dom>:<p> can be used \
93
         *   to target the (sub)domain <dom>"); *)
94
        ("-help-domain", Arg.String Tiny.Load_domains.help_domain,
95
         "<domain>  Print params of <domain>");
96
        (* ("-h", Arg.String Tiny.Load_domains.help_domain, "<domain>  Print params of <domain>"); *)
97
        (* ("--compile", Arg.Set compile_mode, " Compilation mode: compile to C");
98
      ("-c", Arg.Set compile_mode,             " Compilation mode: compile to C");*)
99
        
100
        ("-quiet", Arg.Unit quiet, " Quiet mode");
101
        (* ("-q", Arg.Unit quiet, " Quiet mode"); *)
102
        ("-verbose", Arg.Set_int Tiny.Report.verbosity,
103
         "<n>  Verbosity level (default is 1)");
104
        (* ("-v", Arg.Set_int Tiny.Report.verbosity, "<n>  Verbosity level (default is 1)"); *)
105
  (*      ("--output", Arg.String set_output_file,
106
         "<filename> Output results to file <filename> (default is \
107
          standard ouput)");
108
        ("-o", Arg.String set_output_file,
109
         "<filename>  Output results to file <filename> (default is standard ouput)");
110
   *)
111
        ("-descending", Arg.Set_int descending,
112
         "<n>  Perform <n> descending iterations after fixpoint of a loop \
113
          is reached (default is 1)");
114
        (* ("-d", Arg.Set_int descending,
115
         *  "<n>  Perform <n> descending iterations after fixpoint of a loop \
116
         * is reached (default is 1)"); *)
117
      ("-unrolling", Arg.Set_int unrolling,
118
       "<n>  Unroll loops <n> times before computing fixpoint (default is 0)");
57

  
58
  Format.printf "%a@." Tiny.Ast.fprint_stm ast;
59

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

  
72
  (* else PrintResults.print_invariants m ast !output_file *)
73
  ()
74

  
75
module Verifier : VerifierType.S = struct
76
  include VerifierType.Default
77

  
78
  let name = "tiny"
79

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

  
129
  let activate () =
130
    active := true;
131
    (* Options.global_inline := true;
132
     * Options.optimization := 0;
133
     * Options.const_unfold := true; *)
134
    ()
135

  
136
  let is_active () = !active
137

  
138
  let run = tiny_run
139
end
138 140

  
139 141
let () =
140
  VerifierList.registered := (module Verifier : VerifierType.S) ::
141
                             !VerifierList.registered
142
  VerifierList.registered :=
143
    (module Verifier : VerifierType.S) :: !VerifierList.registered

Also available in: Unified diff