Add a check-rif tools, that performs post-mortem oracle checking using ecexe.

source/Makefile

@@ -250,6 +250,16 @@ lurette_ml_exec: $(OBJDIR)
 include $(LURETTE_PATH)/source/Makefile.release
 
 
+##############################################################################"
+.PHONY: check-rif
+check-rif:$(OBJDIR)
+	cd $(OBJDIR) && $(MAKE) -f ../misc/Makefile.check_rif  ln && \
+		        $(MAKE) -f ../misc/Makefile.check_rif  nc
+
+
+check-rif_clean:$(OBJDIR)
+	cd $(OBJDIR)  && $(MAKE) -k -f ../misc/Makefile.check_rif clean
+
 ##############################################################################"
 .PHONY: gnuplot-rif
 gnuplot-rif:$(OBJDIR)
@@ -575,7 +585,7 @@ strtopwin:
 	ocamlmktop  -o strtop.win  unix.cma
 
 strtop:
-	ocamlmktop -o strtop str.cma unix.cma graph.cma
+	ocamlmktop -o strtop str.cma 
 unixtop:
 	ocamlmktop -o unixtop unix.cma str.cma 
 

source/misc/Makefile.check_rif

+#
+
+######################################################################
+
+
+OCAMLNCFLAGS =  -inline 10
+
+
+LIBS = unix str
+CLIBS = 
+
+USE_CAMLP4 = yes
+
+-include ../Makefile.ln
+
+SOURCES_OCAML = \
+          $(OBJDIR)/version.ml \
+          $(OBJDIR)/genlex.mli \
+          $(OBJDIR)/genlex.ml \
+          $(OBJDIR)/util.ml \
+          $(OBJDIR)/rif_base.mli \
+          $(OBJDIR)/rif_base.ml \
+          $(OBJDIR)/checkRif.ml 
+
+SOURCES = $(SOURCES_OCAML)
+
+RESULT  = check-rif$(EXE)
+ln: $(OBJDIR) $(SOURCES)
+
+
+OCAMLMAKEFILE = ../../OcamlMakefile
+-include $(OCAMLMAKEFILE)
+

source/misc/checkRif.ml

+
+(*
+prend un .rif et un oracle.lus qui
+   - dump un joli diagnostic (idéalement, de facon graphique)
+   - sache lire un fichier rif en cours de modification
+   - affiche la couverture en temps réel
+
+recuperer le code qui gere la courverture dans 
+  ~/lurette/source/common/lurette.ml
+le mettre dans un module a part
+
++ lire en 
+
+  try
+    loop
+      Rif_base.read
+      print_cov
+    with eof  
+  -> 
+  the end
+
++ un mode text 
+
+
+*)
+
+open Format
+let debug = false
+
+(**************************************************************************)
+  
+let usage = Sys.argv.(0) ^ " rif_file.rif oracle_file.lus oracle_node
+"
+
+let _ =
+  let s = Array.length Sys.argv in
+  if s <> 4 then (
+    print_string ("*** Bad argument number ("^(string_of_int (s-1)) ^
+                    " instead of 3). The usage is \n"^ usage^"");
+    flush stdout;
+    exit 2)
+
+let rif_file = Sys.argv.(1)
+let oracle_file = Sys.argv.(2)
+let oracle_node = Sys.argv.(3)
+
+(* let rec speclist =  *)
+(*   ["-rif", Arg.String  (fun file -> rif_f := file), "A rif file"; *)
+(*    "-oracle", Arg.String  (fun file -> oracle_f :=  file), "A rif file"; *)
+(*   ] *)
+
+(**************************************************************************)
+(* get the io name and type from a lustre file *)
+let (get_io_from_lustre : string -> string ->  (string * string) list * (string * string) list) =
+  fun file node -> 
+    try
+      let str = Util.readfile file in
+      let i = Str.search_forward (Str.regexp ("node[ \n\t]+"^node)) str 0 in
+      let i1 = 1+Str.search_forward (Str.regexp "(") str (i+(String.length (Str.matched_string str))) in
+      let j1 = Str.search_forward (Str.regexp ")") str i1 in
+      let i2 = 1+Str.search_forward (Str.regexp "(") str j1 in
+      let j2 = Str.search_forward (Str.regexp ")") str i2 in
+      let input_str = String.sub str i1 (j1-i1) in
+      let output_str = String.sub str i2 (j2-i2) in
+      let get_io_from_str s =
+        let decls = Str.split (Str.regexp ";") s in
+        let rm_blank s = 
+          let buff = ref "" in
+            for i = 0 to String.length s - 1 do
+              match s.[i] with
+                | ' ' | '\t' | '\n' -> ()
+                | c -> buff:=!buff^(String.make 1 c)
+            done;
+            !buff        
+        in
+        let decl_to_pair s = 
+          match Str.split (Str.regexp ":") s with
+            | [n;t] -> rm_blank n, rm_blank t
+            | _ -> failwith ("Cannot split "^s)
+        in
+        let io = List.map decl_to_pair decls in
+        let expand_decl (n,t) =
+          let lv = Str.split (Str.regexp ",") n in
+            List.map (fun v -> v,t) lv
+        in
+        let _ = assert (
+          expand_decl ("T,T1,T2","real") = ["T","real"; "T1","real"; "T2","real"])
+        in
+        let io = List.flatten (List.map expand_decl io) in
+          io
+      in
+        get_io_from_str input_str, get_io_from_str output_str
+
+    with Not_found -> 
+      print_string ("Error when searching for the I/O of node "^node^" in file '"^file^
+                      "'\n  Is '"^file ^"' a valid lustre file?\n  Is "^node^" a node of '"^ file^"'?\n");
+      flush stdout;
+      exit 2
+
+
+(**************************************************************************)
+
+let oracle_in, oracle_out = get_io_from_lustre oracle_file oracle_node 
+
+let (oracle_stdin_in,  oracle_stdin_out) = Unix.pipe () 
+let (oracle_stdout_in, oracle_stdout_out) = Unix.pipe ()
+  
+let oracle_ic = Unix.in_channel_of_descr oracle_stdout_in 
+let oracle_oc = Unix.out_channel_of_descr oracle_stdin_out 
+
+let _ = 
+  set_binary_mode_in  oracle_ic false;
+  set_binary_mode_out oracle_oc false
+  
+let pid_oracle = 
+  let arg_list = ["ecexe"; "-r"; "-rif"; oracle_file] in
+  let arg_array = Array.of_list arg_list in
+  let prog = List.hd arg_list in
+    Unix.create_process prog arg_array 
+      oracle_stdin_in oracle_stdout_out (Unix.descr_of_out_channel stderr)
+
+(**************************************************************************)
+let rif_ic = open_in rif_file
+
+let rif_in, rif_out = Rif_base.read_interface rif_ic
+let rif_all = rif_in @ rif_out
+
+
+let _ = 
+  if debug then (
+    print_string "Rif Inputs:\n";
+    List.iter (fun (n,t) -> print_string ("\t"^n^":"^t^"\n")) rif_in;
+    print_string "Rif Outputs:\n";
+    List.iter (fun (n,t) -> print_string ("\t"^n^":"^t^"\n")) rif_out;
+    print_string "Oracle Inputs:\n";
+    List.iter (fun (n,t) -> print_string ("\t"^n^":"^t^"\n")) oracle_in;
+    print_string "Oracle Outputs:\n";
+    List.iter (fun (n,t) -> print_string ("\t"^n^":"^t^"\n")) oracle_out
+  )
+
+(**************************************************************************)
+
+let _ =
+  List.iter 
+    (fun (n,t) -> 
+       if not (List.mem (n,t) rif_all) then (
+         print_string ("The oracle input variable '"^n^"' (of type "^t^
+                         ") is not present in '"^ rif_file^"'\n");
+         print_string "Rif Inputs:\n";
+         List.iter (fun (n,t) -> print_string ("\t"^n^":"^t^"\n")) rif_in;
+         print_string "Rif Outputs:\n";
+         List.iter (fun (n,t) -> print_string ("\t"^n^":"^t^"\n")) rif_out;
+         flush stdout;
+         exit 2
+       )
+    )
+    oracle_in 
+
+let rif_all_names = fst (List.split rif_all)
+let oracle_names =  fst (List.split oracle_in)
+
+
+let _ = 
+  if rif_all <> oracle_in then (
+    print_string "*** ERROR: Rif Inputs and Rif outputs should exactly match the oracle inputs ";
+    print_string " (Same name, same type, in the same order)\n";
+    print_string "Rif Inputs:\n";
+    List.iter (fun (n,t) -> print_string ("\t"^n^":"^t^"\n")) rif_in;
+    print_string "Rif Outputs:\n";
+    List.iter (fun (n,t) -> print_string ("\t"^n^":"^t^"\n")) rif_out;
+    print_string "Oracle Inputs:\n";
+    List.iter (fun (n,t) -> print_string ("\t"^n^":"^t^"\n")) oracle_in;
+    print_string "Oracle Outputs:\n";
+    List.iter (fun (n,t) -> print_string ("\t"^n^":"^t^"\n")) oracle_out;
+    exit 2
+  )
+  
+
+(**************************************************************************)
+
+let print_vals vals =
+  List.iter 
+    (fun (name, value) -> 
+       Format.printf "%s=%s\n" name (Rif_base.rif_val_to_string value)) 
+    vals
+
+
+let _ =
+  let ok = ref true in
+  let t = ref (Sys.time ()) in
+  let i = ref 0 in
+    try
+(*       Rif_base.open_rif_file "toto.rif"; *)
+      printf "Analysed step number:      " ;
+      let rec loop () =
+        let ti =  (Sys.time ()) in
+          incr i;
+          if ti -. !t > 0.2  then (
+            t:=ti;
+            printf "\b\b\b\b\b\b%6i" !i;
+            flush stdout
+          );
+        (* lire le rif *)
+          let in_vals : Rif_base.subst list = Rif_base.read ~pragma:["outs"] rif_ic rif_all in
+
+        (* l'envoyer a l'oracle *)
+        let in_vals_str =
+          List.fold_left
+            (fun acc (name, value) -> acc ^ " "^ (Rif_base.rif_val_to_string value))
+            "" 
+            in_vals          
+        in
+          (*       let _ = output_string stdout (in_vals_str ^"\n"); flush stdout in *)
+        let _ = output_string oracle_oc (in_vals_str ^"\n"); flush oracle_oc in
+
+        (* lire la reponse de l'oracle *)
+        let oracle_vals = Rif_base.read oracle_ic oracle_out in
+          
+
+          (* afficher des stats *)
+
+          match oracle_vals with
+            | [] -> assert false
+            | (_, Rif_base.B true)::_ -> loop ()
+            | (_, Rif_base.B false)::_ -> 
+                printf "The oracle is violated at step %i\n" !i;
+                ok := false;
+                loop ()
+
+      in
+        loop ()
+    with e  ->
+      decr i;
+      printf "\b\b\b\b\b\b%6i\n" !i;
+      flush stdout;
+      
+      if !ok then 
+        printf 
+          "\nData in %s are ok with respect to %s:%s\n"
+          rif_file oracle_file oracle_node;
+
+      print_string ("\n"^(Printexc.to_string e)^"\n");
+      close_in rif_ic; 
+      Unix.close oracle_stdin_in;
+      Unix.close oracle_stdin_out;
+      Unix.close oracle_stdout_in;
+      Unix.close oracle_stdout_out;
+
+      (try Unix.kill pid_oracle Sys.sigkill with _ -> () );
+      print_string "The end\n";
+      flush stdout
+