Revision 58fd528a
Added by Pierre-Loïc Garoche almost 5 years ago
| 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
Added some missing locations in tiny plugin