Commit 2d1cd4ed authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Some work on check-rif.

Try to push the reusable part of the code in the coverage and
LustreRun modules, so that chekRif.ml only contains administration
stuff (dealing with options) plus a simple top-level loop.

The rationale would be to be able to reuse that stuff from lutin for
instance.
parent fe231062
......@@ -31,16 +31,30 @@ The \key{node}\footnote{used to be called \key{system} in the earlier
nodes.} interface declares the set of input and output variables;
they are called the {\em support variables}. During the node
execution, actual input values are provided by the program
environment.
environment. Output variable ranges can specified (or not) in the
declaration. By default, numeric value ranges from -10000 to 10000.
%% \begin{example}
%% \begin{program}
%% \key{node} foo(x:bool) \key{returns} (t:real; i:\key{int}) = \syn{NodeBodyStatement}
%% \end{program}
%% \end{example}
\begin{example}
\begin{program}
\key{node} foo(x: bool) \key{returns} (t: real; i: \key{int}) = \syn{NodeBodyStatement}
\key{node} foo(x:bool) \key{returns} (t:real [0.0;100.0]; i:\key{int}) =\\
\syn{NodeBodyStatement}
\end{program}
\end{example}
The node body is made of statements that we describe below.
\subsubsection{Local variables}
Node body statements can be made of a local variable
......@@ -49,7 +63,8 @@ keyword.
\begin{example}
\begin{program}
\key{exist} \syn{ident} \key{:} \syn{type} \key{in} \syn{st}\\
\key{exist} y \key{:} real \key{in} \syn{st}\\
\key{exist} z \key{:} int [-100000; 100000] \key{in} \syn{st}
\end{program}
\end{example}
......
......@@ -645,6 +645,7 @@ cp-verimag:
cp $(PRE_RELEASE_DIR)/bin/call-via-socket$(EXE) $(BIN_VERIMAG_INSTALL_DIR) ; \
cp $(PRE_RELEASE_DIR)/bin/gen_stubs_exe$(EXE) $(BIN_VERIMAG_INSTALL_DIR) ; \
cp $(PRE_RELEASE_DIR)/bin/gen_fake_lucky$(EXE) $(BIN_VERIMAG_INSTALL_DIR) ; \
cp $(PRE_RELEASE_DIR)/bin/check-rif$(EXE) $(BIN_VERIMAG_INSTALL_DIR) ; \
cp $(PRE_RELEASE_DIR)/bin/lucky$(EXE) $(BIN_VERIMAG_INSTALL_DIR) ; \
cp $(PRE_RELEASE_DIR)/bin/lutin$(EXE) $(BIN_VERIMAG_INSTALL_DIR) ; \
cp $(PRE_RELEASE_DIR)/bin/show_luc$(EXE) $(BIN_VERIMAG_INSTALL_DIR) ; \
......
......@@ -2,14 +2,49 @@
open Util
type t = bool StringMap.t
type t = bool StringMap.t * string
let (init : (string * bool) list -> t) =
let (init_t : (string * bool) list -> bool StringMap.t) =
List.fold_left (fun acc (vn,value) -> StringMap.add vn value acc) StringMap.empty
let (init : string list -> string -> bool -> t) =
fun oracle_names cov_file reinit_cov ->
if not (Sys.file_exists cov_file) then
init_t (List.map (fun x -> x,false) oracle_names), ""
else
let str = Util.readfile cov_file 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
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
loop_var ((var_name, if reinit_cov then false else status= "t")::cov) (j+1)
with
Not_found -> cov
| Invalid_argument _ -> failwith ("File " ^ cov_file ^ " is not correctly formatted.
It should looks like:
VAR: var_name1 t
VAR: var_name2 t
VAR: var_name3 f
")
in
init_t (loop_var [] 0), if reinit_cov then "" else (loop_rif "" 0)
let (compute_stat : t -> int * int * float ) =
fun cov ->
fun (cov ,_) ->
let i,n =
StringMap.fold
(fun vn value (i,n) -> if value then (i+1,n+1) else (i,n+1))
......@@ -24,11 +59,11 @@ let (update_cov : Rif_base.subst list -> t -> t) =
fun substs cov ->
let cov =
List.fold_left
(fun cov (vn, value) ->
(fun (cov, str) (vn, value) ->
if value <> Rif_base.B true || not (StringMap.mem vn cov) then
cov
(cov, str)
else
StringMap.add vn true cov
StringMap.add vn true cov, str
)
cov
substs
......@@ -37,11 +72,11 @@ let (update_cov : Rif_base.subst list -> t -> t) =
let (dump : string -> string -> string -> string -> t -> unit) =
fun str ecfile riffile covfile cov ->
let (dump : string -> string -> string -> t -> unit) =
fun ecfile riffile covfile cov ->
let oc = open_out covfile in
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))
......@@ -55,12 +90,12 @@ let (dump : string -> string -> string -> string -> t -> unit) =
)
and hostname = Unix.gethostname ()
in
output_string oc str;
output_string oc (snd cov);
Printf.fprintf oc "ORACLE: %s\n" ecfile;
Printf.fprintf oc "RIF: %s - generated at %s on %s\n" riffile time_str hostname;
Printf.fprintf oc "RIF: %s - generated at %s the %s on %s\n" riffile time_str date hostname;
StringMap.iter
(fun vn st -> Printf.fprintf oc "VAR: %s %s\n" vn (if st then "t" else "f"))
cov;
(fst cov);
flush oc;
close_out oc;
Printf.printf "\n The coverage file %s has been generated\n" covfile
......
type vars = (string * string) list
let (make_ec : string -> vars * vars * (unit -> unit) *
(Rif_base.subst list -> Rif_base.subst list)) =
fun ec_file ->
let oracle_in, oracle_out = Util.get_io_from_lustre ec_file None in
let (oracle_stdin_in, oracle_stdin_out) = Unix.pipe () in
let (oracle_stdout_in, oracle_stdout_out) = Unix.pipe () in
let oracle_ic = Unix.in_channel_of_descr oracle_stdout_in in
let oracle_oc = Unix.out_channel_of_descr oracle_stdin_out in
let _ =
set_binary_mode_in oracle_ic false;
set_binary_mode_out oracle_oc false
in
let pid_oracle =
let arg_list = ["ecexe"; "-r"; "-rif"; ec_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)
in
let kill () =
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
let step sl =
let in_vals_str =
List.fold_left2
(fun acc (name, value) (name2, _)->
if name = name2 then
acc ^ " "^ (Rif_base.rif_val_to_string value)
else (
assert false
(* should be in the same order. Sort it here or in the caller? *)
)
)
""
sl
oracle_in
in
let res =
output_string oracle_oc (in_vals_str ^"\n");
flush oracle_oc;
Rif_base.read oracle_ic oracle_out
in
res
in
oracle_in, oracle_out, kill, step
(* Somewhat similar to Oracle, but more dynamic in the sense
that it takes an oracle file in input.
*)
(* Currently implemented with pipes and fork, but could be compiled
and dynamically linked !! *)
type vars = (string * string) list
(* Take an ec file and returns:
- the list of the ec file inputs variable names and types
- ditto for the outputs
- a termination function (for a clean exit)
- a step function
*)
val make_ec : string ->
vars * vars * (unit -> unit) * (Rif_base.subst list -> Rif_base.subst list)
......@@ -18,9 +18,12 @@ SOURCES_OCAML = \
$(OBJDIR)/genlex.mli \
$(OBJDIR)/genlex.ml \
$(OBJDIR)/util.ml \
$(OBJDIR)/coverage.mli \
$(OBJDIR)/coverage.ml \
$(OBJDIR)/rif_base.mli \
$(OBJDIR)/rif_base.ml \
$(OBJDIR)/lustreRun.mli \
$(OBJDIR)/lustreRun.ml \
$(OBJDIR)/checkRif.ml
SOURCES = $(SOURCES_OCAML)
......
(*
Se plugger sur l'API c de l'oracle ?
lire le rif sur stdin ?
*)
open Format
(**************************************************************************)
type argT = {
mutable rif : string;
mutable rif : string option;
mutable ec : string;
mutable cov : string;
mutable debug : bool;
mutable reinit_cov : bool;
mutable stop_at_error : bool;
}
let arg = {
rif = "";
rif = None;
ec = "";
cov = "";
debug = false;
reinit_cov = false;
stop_at_error = false;
}
(**************************************************************************)
let usage = "Usage: \n\t" ^
Sys.argv.(0) ^ " [options]* -ec <file>.ec <Rif File name to check>
......@@ -53,6 +60,9 @@ let rec speclist =
"-reinit-cov", Arg.Unit (fun _ -> (arg.reinit_cov <- true)),
"\treset the coverage rate (to 0%)";
"-stop-at-error", Arg.Unit (fun _ -> (arg.stop_at_error <- true)),
"\tStop processing when the oracle is violated";
"-debug", Arg.Unit (fun _ -> (arg.debug <- true)),
"\tset on the debug mode";
......@@ -62,14 +72,10 @@ let rec speclist =
"";
"-h", Arg.Unit (fun _ -> (Arg.usage speclist usage ; exit 0)),
""
]
(**************************************************************************)
let _ =
( try Arg.parse speclist (fun str -> arg.rif <- str) usage
( try Arg.parse speclist (fun str -> arg.rif <- Some str) usage
with
Failure(e) ->
output_string stderr e;
......@@ -84,59 +90,24 @@ let _ =
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 = 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 ()
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"; 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 arg.rif
let rif_ic : in_channel =
match arg.rif with
Some f -> open_in f
| None -> stdin
let rif_in, rif_out = Rif_base.read_interface rif_ic
let rif_all = rif_in @ rif_out
(**************************************************************************)
(* Oracle launching *)
let _ =
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";
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 oracle_in, oracle_out, kill_oracle, step_oracle =
LustreRun.make_ec arg.ec
(**************************************************************************)
(* Check that the set of oracle Inputs is included in the set of the
RIF file inputs/outputs. *)
let _ =
......@@ -144,7 +115,7 @@ let _ =
(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 '"^ arg.rif^"'\n");
") is not present in the RIF data\n");
print_string "Rif Inputs:\n";
List.iter (fun (n,t) -> print_string ("\t"^n^":"^t^"\n")) rif_in;
print_string "Rif Outputs:\n";
......@@ -161,58 +132,18 @@ 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 cov_init =
let cov_file = if arg.cov = "" then
((Filename.chop_extension arg.ec)^".cov")
else
arg.cov
in
Coverage.init oracle_names cov_file arg.reinit_cov
(**************************************************************************)
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 main () =
let ok = ref true in
let t = ref (Sys.time ()) in
let i = ref 0 in
......@@ -234,57 +165,49 @@ let _ =
print_string str;
decr i;
print_cov !cov;
Coverage.dump previous_run_info arg.ec arg.rif
Coverage.dump arg.ec (match arg.rif with Some f -> f | None -> "stdin")
(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;
(match arg.rif with Some f -> f | None -> "stdin") 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
kill_oracle ();
in
try
printf "\nAnalysed step number: " ;
let rec loop () =
let ti = (Sys.time ()) in
incr i;
if ti -. !t > 0.2 then (
t:=ti;
print_cov !cov;
);
(* lire le rif *)
if ti -. !t > 0.2 then (t:=ti; print_cov !cov);
(* 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
output_string oracle_oc (in_vals_str ^"\n"); flush oracle_oc;
oracle_vals := Rif_base.read oracle_ic oracle_out;
(* ... et l'envoyer a l'oracle *)
oracle_vals := step_oracle in_vals ;
cov := Coverage.update_cov !oracle_vals !cov;
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 ()
let msg = sprintf "The oracle is violated at step %i\n" !i in
ok := false;
if arg.stop_at_error then (
finish msg
) else (
printf "The oracle is violated at step %i\n" !i;
loop ()
)
| _ ->
ok := false;
finish "The oracle first output ougth to be a Boolean\n";
finish "*** Error: the oracle first output ougth to be a Boolean\n";
in
loop ()
with
| End_of_file -> finish ""
| e ->
finish ("\n"^(Printexc.to_string e)^"\n")
let _ =
main ()
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment