Added some missing locations in tiny plugin

src/tools/tiny/tiny_utils.ml

 
 module Ast = Tiny.Ast
 
-
-let lloc_to_tloc loc = Tiny.Location.dummy (*TODO*)
+let gen_loc () = Tiny.Location.dummy ()
+               
+let lloc_to_tloc loc = Tiny.Location.location_of_positions loc.Location.loc_start loc.Location.loc_end
                      
-let tloc_to_lloc loc = Location.dummy_loc (*TODO*)
+let tloc_to_lloc loc = assert false (*Location.dummy_loc (*TODO*) *)
 
                      
 let ltyp_to_ttyp t =
@@ -21,6 +22,12 @@ let cst_bool loc b =
         Ast.Cst(Q.of_int 0, "false");
     expr_loc = loc;
     expr_type = Ast.BoolT }
+
+let cst_num loc t q =
+{ Ast.expr_desc =
+    Ast.Cst(q, Q.to_string q);
+  expr_loc = loc;
+  expr_type = t }
   
 let rec real_to_q man exp =
   if exp = 0 then
@@ -34,13 +41,13 @@ let rec real_to_q man exp =
 
 let instr_loc i =
   match i.Machine_code_types.lustre_eq with
-  | None -> Tiny.Location.dummy
+  | None -> gen_loc ()
   | Some eq -> lloc_to_tloc eq.eq_loc
              
 let rec lval_to_texpr loc _val =
   let build d v =
       Ast.{ expr_desc = d;
-            expr_loc = loc;
+            expr_loc = gen_loc ();
             expr_type = v }
   in
   let new_desc =
@@ -76,6 +83,7 @@ let rec lval_to_texpr loc _val =
           Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.Zero)
        | "!=", [v1;v2] ->
           Ast.Cond (build (Ast.Binop (Ast.Minus, v2, v1)) t_arg, Ast.NonZero)
+       | "uminus", [v1] -> Ast.Binop (Ast.Minus, cst_num loc t_arg Q.zero, v1)
        | _ -> Format.eprintf "No tiny translation for operator %s@.@?" op; assert false    
   )
   | _ -> assert false (* no array. access or power *)
@@ -150,11 +158,11 @@ let machine_body_to_ast init m =
     | [i] -> instr_to_stm i
     | i::il ->
        let i' = instr_to_stm i in
-       Ast.Seq (instr_loc i, i', (instrl_to_stm il))
+       Ast.Seq (gen_loc (), i', (instrl_to_stm il))
   in
   instrl_to_stm m.Machine_code_types.mstep.step_instrs 
 
-let read_var loc bounds_opt v =
+let read_var bounds_opt v =
   let min, max =
     match bounds_opt with
       Some (min,max) -> min, max
@@ -162,42 +170,39 @@ let read_var loc bounds_opt v =
   in
   let range = {
       Ast.expr_desc = Ast.Rand (min,max);
-      expr_loc = loc;
+      expr_loc = gen_loc ();
       expr_type = ltyp_to_ttyp (v.Lustre_types.var_type)
     }
   in
-  Ast.Asn (loc, v.var_id, range)
+  Ast.Asn (gen_loc (), v.var_id, range)
   
-let rec read_vars loc bounds_inputs vl =
+let rec read_vars bounds_inputs vl =
   match vl with
-    [] -> Ast.Nop loc
+    [] -> Ast.Nop (gen_loc ())
   | [v] -> read_var
-             loc
              (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
                 Some (List.assoc v.Lustre_types.var_id bounds_inputs)
               else
                 None)
              v
   | v::tl ->
-     Ast.Seq (loc,
+     Ast.Seq (gen_loc (),
               read_var
-                loc
                 (if List.mem_assoc v.Lustre_types.var_id bounds_inputs then
                    Some (List.assoc v.Lustre_types.var_id bounds_inputs)
                  else
                    None)
                 v,
-              read_vars loc bounds_inputs tl
+              read_vars bounds_inputs tl
        )
   
 let machine_to_ast bounds_input m =
-  let loc = Tiny.Location.dummy in
-  let read_vars = read_vars loc bounds_input m.Machine_code_types.mstep.step_inputs in
+  let read_vars = read_vars bounds_input m.Machine_code_types.mstep.step_inputs in
   let ast_loop_first = machine_body_to_ast true m in
   let ast_loop_run = machine_body_to_ast false m in
-  let ast_loop_body = Ast.Seq (loc, read_vars, ast_loop_run) in
-  let loop = Ast.While(loc, cst_bool loc true, ast_loop_body) in
-  Ast.Seq (loc, read_vars, (Ast.Seq (loc, ast_loop_first, loop)))
+  let ast_loop_body = Ast.Seq (gen_loc (), read_vars, ast_loop_run) in
+  let loop = Ast.While(gen_loc (), cst_bool (gen_loc ()) true, ast_loop_body) in
+  Ast.Seq (gen_loc (), read_vars, (Ast.Seq (gen_loc (), ast_loop_first, loop)))
   
 let machine_to_env m =
   

src/tools/tiny/tiny_verifier.ml

 
 let active = ref false
 let tiny_debug = ref false
+let tiny_help = ref false
+let descending = ref 1
+let unrolling = ref 0
 
-    
+
+              
+let quiet () = Tiny.Report.verbosity := 0
+             
+let print_tiny_help () =
+  let open Format in
+  Format.eprintf "@[Tiny verifier plugin produces a simple imperative code \
+          output for the provided main node, inlining all calls. This \
+          code can then be analyzed using tiny analyzer options.@]";
+  Format.eprintf "@.@?";
+  flush stdout
+
+  
 let tiny_run ~basename prog machines =
+  if !tiny_help then (
+    let _ = print_tiny_help () in
+    exit 0
+  );
   let node_name =
     match !Options.main_node with
     | "" -> (
@@ -39,7 +58,20 @@ let tiny_run ~basename prog machines =
   
    Format.printf "%a@." Tiny.Ast.fprint_stm ast; 
 
-  ()
+   let dom =
+     let open Tiny.Load_domains in
+     prepare_domains (List.map get_domain !domains)
+   in
+   let results = Tiny.Analyze.analyze dom !descending !unrolling env ast in
+   let module Results = (val results: Tiny.Analyze.Results) in
+   let module Dom = Results.Dom in
+   let module PrintResults = Tiny.PrintResults.Make (Dom) in
+   let m = Results.results in
+   (* if !Tiny.Report.verbosity > 1 then *)
+   PrintResults.print m ast None (* no !output_file *);
+        (* else PrintResults.print_invariants m ast !output_file *)
+
+   ()
   
   
 module Verifier =
@@ -48,7 +80,47 @@ module Verifier =
     let name = "tiny"
     let options =
       [
-        "-debug", Arg.Set tiny_debug, "tiny debug"
+        "-debug", Arg.Set tiny_debug, "tiny debug";
+        ("-abstract-domain", Arg.String Tiny.Load_domains.decl_domain,
+         "<domain>  Use abstract domain <domain> " ^ Tiny.Domains.available_domains_str);
+        (* ("-a", Arg.String Tiny.Load_domains.decl_domain,
+         *  "<domain>  Use abstract domain <domain> " ^ Tiny.Domains.available_domains_str); *)
+        ("-param", Arg.String Tiny.Load_domains.set_param,
+         "<p>  Send <p> to the abstract domain, syntax <dom>:<p> can be used \
+          to target the (sub)domain <dom>");
+        (* ("-p", Arg.String Tiny.Load_domains.set_param,
+         *  "<p>  Send <p> to the abstract domain, syntax <dom>:<p> can be used \
+         *   to target the (sub)domain <dom>"); *)
+        ("-help-domain", Arg.String Tiny.Load_domains.help_domain,
+         "<domain>  Print params of <domain>");
+        (* ("-h", Arg.String Tiny.Load_domains.help_domain, "<domain>  Print params of <domain>"); *)
+        (* ("--compile", Arg.Set compile_mode, " Compilation mode: compile to C");
+      ("-c", Arg.Set compile_mode,             " Compilation mode: compile to C");*)
+        
+        ("-quiet", Arg.Unit quiet, " Quiet mode");
+        (* ("-q", Arg.Unit quiet, " Quiet mode"); *)
+        ("-verbose", Arg.Set_int Tiny.Report.verbosity,
+         "<n>  Verbosity level (default is 1)");
+        (* ("-v", Arg.Set_int Tiny.Report.verbosity, "<n>  Verbosity level (default is 1)"); *)
+  (*      ("--output", Arg.String set_output_file,
+         "<filename> Output results to file <filename> (default is \
+          standard ouput)");
+        ("-o", Arg.String set_output_file,
+         "<filename>  Output results to file <filename> (default is standard ouput)");
+   *)
+        ("-descending", Arg.Set_int descending,
+         "<n>  Perform <n> descending iterations after fixpoint of a loop \
+          is reached (default is 1)");
+        (* ("-d", Arg.Set_int descending,
+         *  "<n>  Perform <n> descending iterations after fixpoint of a loop \
+         * is reached (default is 1)"); *)
+      ("-unrolling", Arg.Set_int unrolling,
+       "<n>  Unroll loops <n> times before computing fixpoint (default is 0)");
+      (* (\* ("-u", Arg.Set_int unrolling,
+       *  *  "<n>  Unroll loops <n> times before computing fixpoint (default is 0)"); *\) *)
+       "-help", Arg.Set tiny_help, "tiny help and usage";
+        
+      
       ]
       
     let activate () =