Project

General

Profile

« Previous | Next » 

Revision 58fd528a

Added by Pierre-Loïc Garoche over 1 year ago

Added some missing locations in tiny plugin

View differences:

src/tools/tiny/tiny_utils.ml
1 1

  
2 2
module Ast = Tiny.Ast
3 3

  
4

  
5
let lloc_to_tloc loc = Tiny.Location.dummy (*TODO*)
4
let gen_loc () = Tiny.Location.dummy ()
5
               
6
let lloc_to_tloc loc = Tiny.Location.location_of_positions loc.Location.loc_start loc.Location.loc_end
6 7
                     
7
let tloc_to_lloc loc = Location.dummy_loc (*TODO*)
8
let tloc_to_lloc loc = assert false (*Location.dummy_loc (*TODO*) *)
8 9

  
9 10
                     
10 11
let ltyp_to_ttyp t =
......
21 22
        Ast.Cst(Q.of_int 0, "false");
22 23
    expr_loc = loc;
23 24
    expr_type = Ast.BoolT }
25

  
26
let cst_num loc t q =
27
{ Ast.expr_desc =
28
    Ast.Cst(q, Q.to_string q);
29
  expr_loc = loc;
30
  expr_type = t }
24 31
  
25 32
let rec real_to_q man exp =
26 33
  if exp = 0 then
......
34 41

  
35 42
let instr_loc i =
36 43
  match i.Machine_code_types.lustre_eq with
37
  | None -> Tiny.Location.dummy
44
  | None -> gen_loc ()
38 45
  | Some eq -> lloc_to_tloc eq.eq_loc
39 46
             
40 47
let rec lval_to_texpr loc _val =
41 48
  let build d v =
42 49
      Ast.{ expr_desc = d;
43
            expr_loc = loc;
50
            expr_loc = gen_loc ();
44 51
            expr_type = v }
45 52
  in
46 53
  let new_desc =
......
76 83
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Zero)
77 84
       | "!=", [v1;v2] ->
78 85
          Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.NonZero)
86
       | "uminus", [v1] -> Ast.Binop (Ast.Minus, cst_num loc t_arg Q.zero, v1)
79 87
       | _ -> Format.eprintf "No tiny translation for operator %s@.@?" op; assert false    
80 88
  )
81 89
  | _ -> assert false (* no array. access or power *)
......
150 158
    | [i] -> instr_to_stm i
151 159
    | i::il ->
152 160
       let i' = instr_to_stm i in
153
       Ast.Seq (instr_loc i, i', (instrl_to_stm il))
161
       Ast.Seq (gen_loc (), i', (instrl_to_stm il))
154 162
  in
155 163
  instrl_to_stm m.Machine_code_types.mstep.step_instrs 
156 164

  
157
let read_var loc bounds_opt v =
165
let read_var bounds_opt v =
158 166
  let min, max =
159 167
    match bounds_opt with
160 168
      Some (min,max) -> min, max
......
162 170
  in
163 171
  let range = {
164 172
      Ast.expr_desc = Ast.Rand (min,max);
165
      expr_loc = loc;
173
      expr_loc = gen_loc ();
166 174
      expr_type = ltyp_to_ttyp (v.Lustre_types.var_type)
167 175
    }
168 176
  in
169
  Ast.Asn (loc, v.var_id, range)
177
  Ast.Asn (gen_loc (), v.var_id, range)
170 178
  
171
let rec read_vars loc bounds_inputs vl =
179
let rec read_vars bounds_inputs vl =
172 180
  match vl with
173
    [] -> Ast.Nop loc
181
    [] -> Ast.Nop (gen_loc ())
174 182
  | [v] -> read_var
175
             loc
176 183
             (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
177 184
                Some (List.assoc v.Lustre_types.var_id bounds_inputs)
178 185
              else
179 186
                None)
180 187
             v
181 188
  | v::tl ->
182
     Ast.Seq (loc,
189
     Ast.Seq (gen_loc (),
183 190
              read_var
184
                loc
185 191
                (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
186 192
                   Some (List.assoc v.Lustre_types.var_id bounds_inputs)
187 193
                 else
188 194
                   None)
189 195
                v,
190
              read_vars loc bounds_inputs tl
196
              read_vars bounds_inputs tl
191 197
       )
192 198
  
193 199
let machine_to_ast bounds_input m =
194
  let loc = Tiny.Location.dummy in
195
  let read_vars = read_vars loc bounds_input m.Machine_code_types.mstep.step_inputs in
200
  let read_vars = read_vars bounds_input m.Machine_code_types.mstep.step_inputs in
196 201
  let ast_loop_first = machine_body_to_ast true m in
197 202
  let ast_loop_run = machine_body_to_ast false m in
198
  let ast_loop_body = Ast.Seq (loc, read_vars, ast_loop_run) in
199
  let loop = Ast.While(loc, cst_bool loc true, ast_loop_body) in
200
  Ast.Seq (loc, read_vars, (Ast.Seq (loc, ast_loop_first, loop)))
203
  let ast_loop_body = Ast.Seq (gen_loc (), read_vars, ast_loop_run) in
204
  let loop = Ast.While(gen_loc (), cst_bool (gen_loc ()) true, ast_loop_body) in
205
  Ast.Seq (gen_loc (), read_vars, (Ast.Seq (gen_loc (), ast_loop_first, loop)))
201 206
  
202 207
let machine_to_env m =
203 208
  
src/tools/tiny/tiny_verifier.ml
1 1

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

  
5
    
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
  
6 21
let tiny_run ~basename prog machines =
22
  if !tiny_help then (
23
    let _ = print_tiny_help () in
24
    exit 0
25
  );
7 26
  let node_name =
8 27
    match !Options.main_node with
9 28
    | "" -> (
......
39 58
  
40 59
   Format.printf "%a@." Tiny.Ast.fprint_stm ast; 
41 60

  
42
  ()
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
   ()
43 75
  
44 76
  
45 77
module Verifier =
......
48 80
    let name = "tiny"
49 81
    let options =
50 82
      [
51
        "-debug", Arg.Set tiny_debug, "tiny debug"
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)");
119
      (* (\* ("-u", Arg.Set_int unrolling,
120
       *  *  "<n>  Unroll loops <n> times before computing fixpoint (default is 0)"); *\) *)
121
       "-help", Arg.Set tiny_help, "tiny help and usage";
122
        
123
      
52 124
      ]
53 125
      
54 126
    let activate () =

Also available in: Unified diff