Commit 4743771d authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Some work on check-rif.

- Split check-rif.ml into check-rif.ml and coverage.ml.
- Add a section dedicated to check-rif in the Lutin manual, in the tool section.
- Use the ocaml Arg module to deal with command-line args.
- Take advantage of the fact that an ec file only have one node.
- Store/update the corevage info in a .cov file
parent 3a04bd10
......@@ -10,7 +10,7 @@ SRCS=./commands.tex \
./lutin_examples.tex \
./objs/lutyacc.tex \
./objs/version.tex \
./objs/lutin.tex ./objs/gnuplotrif.tex \
./objs/lutin.tex ./objs/gnuplotrif.tex ./objs/checkrif.tex \
./objs/foo.c.tex \
./objs/call_external_c_code.lut.tex \
./objs/polar.lut.tex \
......@@ -51,7 +51,10 @@ lutin-man.pdf: objs/main.pdf
./objs/gnuplotrif.tex:objs
gnuplot-rif --help 2> $@
gnuplot-rif --help &> $@
./objs/checkrif.tex:objs
check-rif --help &> $@
touch.tex:
......
......@@ -83,6 +83,8 @@
\newcommand{\simtochrogtk}{{\sc Sim2chrogtk}\xspace}
\newcommand{\luciole}{{\sc Luciole}\xspace}
\newcommand{\gnuplotrif}{{\sc Gnuplot-rif}\xspace}
\newcommand{\checkrif}{{\sc check-rif}\xspace}
\newcommand{\ecexe}{{\sc ecexe}\xspace}
\newcommand{\Ocaml}{{\sc Ocaml}\xspace}
\newcommand{\ocaml}{{\sc Ocaml}\xspace}
......@@ -90,6 +90,16 @@ inputs. From a lutin-centric point of view, a \lutin program could use
A complete example can be found in {\tt examples/lutin/xlurette}.
\subsubsection{\checkrif}
A tool that performs post-mortem oracle checking using the
Lustre expanded code (.ec) interpreter \ecexe.
Here is the output of {\tt check-rif --help}:
\begin{alltt}
\input{checkrif}
\end{alltt}
\subsubsection{\simtochro}
\simtochro is a program written par Yann R\'emond that displays
......
......@@ -566,11 +566,11 @@ ifeq ($(HOSTTYPE),cygwin)
LUCKY_DEF=lucky.def
endif
compile_all: gen_version $(OBJDIR) lurette_ml_exec libnc lucky ltop show stubs gnuplot-rif gnuplot-socket call-via-socket gen_luc luc2c luc2luciole luc4c libluc4c_nc.a draw-all luc4ocaml-all $(LUCKY_DEF) lutin
compile_all: gen_version $(OBJDIR) lurette_ml_exec libnc lucky ltop show stubs gnuplot-rif gnuplot-socket call-via-socket gen_luc luc2c luc2luciole luc4c libluc4c_nc.a draw-all luc4ocaml-all $(LUCKY_DEF) lutin check-rif
rest: luc2luciole luc4c libluc4c_nc.a draw-all luc4ocaml-all $(LUCKY_DEF) lutin
allnc: clean lurette_ml_exec lucky libncnc ltop show stubs gnuplot-rif gnuplot-socket call-via-socket gen_luc luc2c luc2luciole luc4c libluc4c_nc.a draw-all luc4ocaml-all
allnc: clean lurette_ml_exec lucky libncnc ltop show stubs gnuplot-rif gnuplot-socket call-via-socket gen_luc luc2c luc2luciole luc4c libluc4c_nc.a draw-all luc4ocaml-all check-rif
static: libnc lucky_static ltop_static show_static stubs_static gen_luc_static
......@@ -611,6 +611,7 @@ cp:
cp $(OBJDIR)/lutin$(EXE) $(BIN_INSTALL_DIR) ;\
cp $(OBJDIR)/show_luc_exe$(EXE) $(BIN_INSTALL_DIR) ; \
cp $(OBJDIR)/luc2c$(EXE) $(BIN_INSTALL_DIR) ; \
cp $(OBJDIR)/check-rif$(EXE) $(BIN_INSTALL_DIR) ; \
cp $(OBJDIR)/luc2luciole$(EXE) $(BIN_INSTALL_DIR) ; \
cp $(OBJDIR)/lurettetop_exe$(EXE) $(BIN_INSTALL_DIR) ; \
cp $(OBJDIR)/liblurette_nc.a $(LIB_INSTALL_DIR) ;\
......
open Util
type t = bool StringMap.t
let (init : (string * bool) list -> t) =
List.fold_left (fun acc (vn,value) -> StringMap.add vn value acc) StringMap.empty
let (compute_stat : t -> int * int * float ) =
fun cov ->
let i,n =
StringMap.fold
(fun vn value (i,n) -> if value then (i+1,n+1) else (i,n+1))
cov
(0,0)
in
let cov_rate = 100. *. (float_of_int i) /. (float_of_int n) in
n, i, cov_rate
let (update_cov : Rif_base.subst list -> t -> t) =
fun substs cov ->
let cov =
List.fold_left
(fun cov (vn, value) ->
if value <> Rif_base.B true || not (StringMap.mem vn cov) then
cov
else
StringMap.add vn true cov
)
cov
substs
in
cov
let (dump : string -> string -> string -> string -> t -> unit) =
fun str ecfile riffile covfile cov ->
let oc = open_out covfile in
let time = Unix.localtime (Unix.time ()) in
let date = (
(string_of_int time.Unix.tm_mday) ^ "/" ^
(string_of_int (time.Unix.tm_mon+1)) ^ "/" ^
(string_of_int (1900+time.Unix.tm_year))
)
and time_str = (
(string_of_int time.Unix.tm_hour) ^ ":" ^
(if time.Unix.tm_min < 10 then "0" else "") ^
(string_of_int time.Unix.tm_min) ^ ":" ^
(if time.Unix.tm_sec < 10 then "0" else "") ^
(string_of_int time.Unix.tm_sec)
)
and hostname = Unix.gethostname ()
in
output_string oc str;
Printf.fprintf oc "ORACLE: %s\n" ecfile;
Printf.fprintf oc "RIF: %s - generated at %s on %s\n" riffile time_str hostname;
StringMap.iter
(fun vn st -> Printf.fprintf oc "VAR: %s %s\n" vn (if st then "t" else "f"))
cov;
flush oc;
close_out oc;
Printf.printf "\n The coverage file %s has been generated\n" covfile
......@@ -847,8 +847,7 @@ let safe_remove_file file =
let entete comment =
let time = Unix.localtime (Unix.time ()) in
let
date = (
let date = (
(string_of_int time.Unix.tm_mday) ^ "/" ^
(string_of_int (time.Unix.tm_mon+1)) ^ "/" ^
(string_of_int (1900+time.Unix.tm_year))
......@@ -912,3 +911,72 @@ let (rm_dir : out_channel -> string -> unit) =
)
else
()
(* get the io name and type from a ec or a lustre file *)
let (get_io_from_lustre : string -> string option -> (string * string) list * (string * string) list) =
fun file node_opt ->
try
let str = readfile file in
let i =
match node_opt with
None ->
(* If no node is specified, we take the first one *)
Str.search_forward (Str.regexp ("node[ \n\t]+")) str 0
| Some node -> 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 remove_comment str =
let comment1 = Str.regexp "--[.]*\n"
and comment2 = Str.regexp "(\*[^\*]*\*)"
in
let str = Str.global_replace comment1 "" str in
let str = Str.global_replace comment2 "" str in
str
in
let input_str = String.sub str i1 (j1-i1) in
(* let input_str = remove_comment input_str in *)
let output_str = String.sub str i2 (j2-i2) in
(* let output_str = remove_comment output_str 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 decls = List.filter (is_substring ":") decls 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 "^
(match node_opt with None -> "" | Some node -> " of node "^node) ^
" in file '"^file^
"'\n Is '"^file ^"' a syntactically correct file?\n");
flush stdout;
exit 2
......@@ -18,6 +18,7 @@ SOURCES_OCAML = \
$(OBJDIR)/genlex.mli \
$(OBJDIR)/genlex.ml \
$(OBJDIR)/util.ml \
$(OBJDIR)/coverage.ml \
$(OBJDIR)/rif_base.mli \
$(OBJDIR)/rif_base.ml \
$(OBJDIR)/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)
type argT = {
mutable rif : string;
mutable ec : string;
mutable cov : string;
mutable debug : bool;
mutable reinit_cov : bool;
}
let arg = {
rif = "";
ec = "";
cov = "";
debug = false;
reinit_cov = false;
}
let usage = "Usage: \n\t" ^
Sys.argv.(0) ^ " [options]* -ec <file>.ec <Rif File name to check>
Performs post-mortem oracle checking using ecexe.
The set of oracle Inputs should be included in the set of the RIF
file inputs/outputs.
At the first run, the coverage information is stored/updated in the
coverage file (cf the -cov option to set its name). The variables
declared in this file should be a subset of the oracle outputs. If
the coverage file does not exist, one is is created using all the
oracle outputs. If not all those outputs are meaningfull to compute
the coverage rate, one just need to delete corresponding lines in the
coverage file. The format of the coverage file is straightforward,
but deserves respect.
Options are:
"
let rec speclist =
[
"-ec", Arg.String
(fun str -> arg.ec <- str),
"<string>\tec file name containing the RIF file checker (a.k.a., the oracle)" ;
"-cov", Arg.String
(fun str -> arg.cov <- str),
"<string>\tOverride the default coverage file name (<oracle name>.cov by default).";
"-reinit-cov", Arg.Unit (fun _ -> (arg.reinit_cov <- true)),
"\treset the coverage rate (to 0%)";
"-debug", Arg.Unit (fun _ -> (arg.debug <- true)),
"\tset on the debug mode";
"--help", Arg.Unit (fun _ -> (Arg.usage speclist usage ; exit 0)),
"\tDisplay this list of options." ;
"-help", Arg.Unit (fun _ -> (Arg.usage speclist usage ; exit 0)),
"";
"-h", Arg.Unit (fun _ -> (Arg.usage speclist usage ; exit 0)),
""
]
(* 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 _ =
( try Arg.parse speclist (fun str -> arg.rif <- str) usage
with
Failure(e) ->
output_string stderr e;
flush stderr;
exit 2
| e ->
output_string stderr (Printexc.to_string e);
flush stderr;
exit 2
);
if arg.ec = "" then (
output_string stderr "*** It is mandatory to set an oracle (cf -ec option)\n";
Arg.usage speclist usage;
flush stderr;
exit 2);
if arg.rif = "" then (
output_string stderr "*** It is mandatory to set a rif file\n";
Arg.usage speclist usage;
flush stderr;
exit 2)
(**************************************************************************)
let oracle_in, oracle_out = get_io_from_lustre oracle_file oracle_node
let oracle_in, oracle_out = Util.get_io_from_lustre arg.ec None
let (oracle_stdin_in, oracle_stdin_out) = Unix.pipe ()
let (oracle_stdout_in, oracle_stdout_out) = Unix.pipe ()
......@@ -113,21 +110,21 @@ let _ =
set_binary_mode_out oracle_oc false
let pid_oracle =
let arg_list = ["ecexe"; "-r"; "-rif"; oracle_file] in
let arg_list = ["ecexe"; "-r"; "-rif"; arg.ec] 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_ic = open_in arg.rif
let rif_in, rif_out = Rif_base.read_interface rif_ic
let rif_all = rif_in @ rif_out
let _ =
if debug then (
if arg.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";
......@@ -140,12 +137,14 @@ let _ =
(**************************************************************************)
(* Check that the set of oracle Inputs is included in the set of the
RIF file inputs/outputs. *)
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");
") is not present in '"^ arg.rif^"'\n");
print_string "Rif Inputs:\n";
List.iter (fun (n,t) -> print_string ("\t"^n^":"^t^"\n")) rif_in;
print_string "Rif Outputs:\n";
......@@ -157,24 +156,52 @@ let _ =
oracle_in
let rif_all_names = fst (List.split rif_all)
let oracle_names = fst (List.split oracle_in)
let oracle_names = fst (List.split oracle_out)
(**************************************************************************)
(* Coverage stuff initilisation *)
let cov_init, previous_run_info =
if
(arg.cov = "" && not (Sys.file_exists ((Filename.chop_extension arg.ec)^".cov")))
|| not (Sys.file_exists arg.cov)
then
Coverage.init (List.map (fun x -> x,false) oracle_names), ""
else
let str = Util.readfile arg.cov in
let rec loop_rif acc i =
try
let i = Str.search_forward (Str.regexp "RIF: ") str i in
let j = Str.search_forward (Str.regexp "\n") str i in
loop_rif (acc ^ (String.sub str i (j-i+1))) (j+1)
with
Not_found -> acc
in
let rec loop_var cov i =
try
(*
VAR: var1 t
VAR: var2 f
*)
let i = 5+Str.search_forward (Str.regexp "VAR: ") str i in
let j = Str.search_forward (Str.regexp " ") str i in
let var_name = String.sub str i (j-i) in
let status = (String.sub str (j+1) 1) in
(* printf "var_name='%s' ; status='%s'\n" var_name status; *)
loop_var ((var_name, if arg.reinit_cov then false else status= "t")::cov) (j+1)
with
Not_found -> cov
| Invalid_argument _ -> failwith ("File " ^ arg.cov ^ " is not correctly formatted.
It should looks like:
VAR: var_name1 t
VAR: var_name2 t
VAR: var_name3 f
")
in
Coverage.init (loop_var [] 0), if arg.reinit_cov then "" else (loop_rif "" 0)
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
)
(**************************************************************************)
......@@ -189,64 +216,75 @@ let _ =
let ok = ref true in
let t = ref (Sys.time ()) in
let i = ref 0 in
let oracle_vals = ref [] in
let cov = ref cov_init in
let print_cov cov =
let (to_cov, covered, cov_rate)= Coverage.compute_stat cov in
if to_cov > 0 then (
if cov_rate=100.0 then printf "\b";
printf "\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b\b%6i The coverage rate is %.1f%s"
!i cov_rate "%"
)
else
printf "\b\b\b\b\b\b%6i" !i;
flush stdout;
in
let finish str =
print_string str;
decr i;
print_cov !cov;
Coverage.dump previous_run_info arg.ec arg.rif
(if arg.cov="" then (Filename.chop_extension arg.ec)^".cov" else arg.cov) !cov;
if !ok then
printf
"\nData in %s are ok with respect to %s\n"
arg.rif arg.ec;
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 _ -> () )
in
try
(* Rif_base.open_rif_file "toto.rif"; *)
printf "Analysed step number: " ;
printf "\nAnalysed 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
print_cov !cov;
);
(* lire le rif *)
(* 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