Commit 610b710d authored by Erwan Jahier's avatar Erwan Jahier
Browse files

In the rif file, and the the main program of Lurettetop/RunDirect do not flatten oracle outputs.

Indeed, there is no reason to have clashes between oracle outputs.

Also, expand var types in LustreRun (as done in SocExec).
parent 472c46b7
......@@ -16,7 +16,7 @@ $(EXPDIR):
# several oracles
test1.rif: heater_control$(EXE) $(EXPDIR)
rm -f test1.rif0 .lurette_rc
$(LURETTETOP) -go --output test1.rif0 \
$(LURETTETOP) -go --output test1.rif0 \
-rp "sut:ec_exe:./heater_control.ec:" \
-rp "oracle:v6:heater_control.lus:not_a_sauna" \
-rp "oracle:v6:heater_control.lus:not_a_fridge" \
......
......@@ -253,8 +253,8 @@ set xlabel \"steps\"
bool_nb="^(string_of_int bool_nb)^ "
# Initialise the global vars
max=-1e38
min=1e38
max=-1e36
min=1e36
range=0
range_10=1
delta=1
......
......@@ -740,253 +740,256 @@ let (read : string -> bool) =
if args.verbose > 1 then
(output_string args.ocr("ltop : " ^ str ^ "\n"); flush args.ocr);
(match (parse str) with
| Nop -> true
| Sut(sut0, node) ->
let sut =
if Filename.is_implicit sut0 then
sut0
else
(
args.sut_dir <- (Filename.dirname sut0);
Filename.basename sut0
)
in
let old_sut = args.sut
and old_node = args.sut_node
in
if (sut <> old_sut || node <> old_node) then
(
args.sut <- sut ;
args.sut_node <- node
(* output_string args.ecr ("The sut node has changed.\n "); *)
(* flush args.ecr; *)
);
true
| Oracle(oracle, node) ->
let old_oracle = args.oracle
and old_node = args.oracle_node
in
let oracle2 = match oracle with "" -> None | x -> Some x in
if (oracle2 <> old_oracle || node <> old_node) then
(
if oracle = "" then (
args.oracle <- None ;
args.oracle_node <- ""
)
else
(
args.oracle <- Some oracle ;
args.oracle_node <- node
)
);
true
| ResetCovFile(b) -> args.reset_cov_file <- b; true
| CovFile(f) -> args.cov_file <- f; true
| Info -> info(); true
| StopOnOracleError(b) -> args.stop_on_oracle_error <- b ; true
| RootNode(node) -> args.root_node <- node; true
| PP(pp) -> args.pp <- pp ; true
| SutCmd(cmd) -> args.sut_cmd <- cmd ; true
| OracleCmd(cmd) -> args.oracle_cmd <- cmd ; true
| StepMode(str) ->
let step_mode = string_to_step_mode str in
args.step_mode <- step_mode; true
(* | MakeOpt(str) -> *)
(* args.make_opt <- str; true *)
| Env(str) -> args.env <- LtopArg.explicit_the_file str; true
| StepNb(i) -> args.step_nb <- i; true
| DrawNb(i) -> args.draw_nb <- i; true
| DisplaySim2chro(b) -> args.display_sim2chro <- b; true
| DisplayLocalVar(b) -> args.display_local_var <- b; true
| SetSutCompiler(comp) -> args.sut_compiler <- comp; true
| SetOracleCompiler(comp) -> args.oracle_compiler <- comp; true
| StdinMode(b) -> if b then args.sut_compiler <- Stdin; true
| StepByStep(b) -> args.step_by_step <- b; true
| Seed(i) -> args.seed <- Some i; true
| Precision(i) -> args.precision <- i; true
| ComputeVolume(b) -> args.compute_volume <- b; true
| RandomSeed -> args.seed <- None; true
| Verbose(b) -> args.verbose <- b; true
| Reactive(b) -> args.reactive <- b; true
| ShowStep(b) -> args.show_step <- b; true
| Prompt(p) -> args.prompt <- Some p; true
| Prefix(p) -> args.prefix <- p; true
| DrawInside i -> args.draw_inside <- i; true
| DrawEdges i -> args.draw_edges <- i; true
| DrawVertices i-> args.draw_vertices <- i; true
| AllFormula b -> args.all_formula <- b; true
| AllVertices b -> args.all_vertices <- b; true
| Output(str) -> args.output <- str; true
| OverwriteOutput(b) -> args.overwrite_output <- b; true
| Log -> args.log <- true; true
| Clean ->
| Nop -> true
| Sut(sut0, node) ->
let sut =
if Filename.is_implicit sut0 then
sut0
else
(
args.sut_dir <- (Filename.dirname sut0);
Filename.basename sut0
)
in
let old_sut = args.sut
and old_node = args.sut_node
in
if (sut <> old_sut || node <> old_node) then
(
args.sut <- sut ;
args.sut_node <- node
(* output_string args.ecr ("The sut node has changed.\n "); *)
(* flush args.ecr; *)
);
true
| Oracle(oracle, node) ->
let old_oracle = args.oracle
and old_node = args.oracle_node
in
let oracle2 = match oracle with "" -> None | x -> Some x in
if (oracle2 <> old_oracle || node <> old_node) then
(
if oracle = "" then (
args.oracle <- None ;
args.oracle_node <- ""
)
else
(
args.oracle <- Some oracle ;
args.oracle_node <- node
)
);
true
| ResetCovFile(b) -> args.reset_cov_file <- b; true
| CovFile(f) -> args.cov_file <- f; true
| Info -> info(); true
| StopOnOracleError(b) -> args.stop_on_oracle_error <- b ; true
| RootNode(node) -> args.root_node <- node; true
| PP(pp) -> args.pp <- pp ; true
| SutCmd(cmd) -> args.sut_cmd <- cmd ; true
| OracleCmd(cmd) -> args.oracle_cmd <- cmd ; true
| StepMode(str) ->
let step_mode = string_to_step_mode str in
args.step_mode <- step_mode; true
(* | MakeOpt(str) -> *)
(* args.make_opt <- str; true *)
| Env(str) -> args.env <- LtopArg.explicit_the_file str; true
| StepNb(i) -> args.step_nb <- i; true
| DrawNb(i) -> args.draw_nb <- i; true
| DisplaySim2chro(b) -> args.display_sim2chro <- b; true
| DisplayLocalVar(b) -> args.display_local_var <- b; true
| SetSutCompiler(comp) -> args.sut_compiler <- comp; true
| SetOracleCompiler(comp) -> args.oracle_compiler <- comp; true
| StdinMode(b) -> if b then args.sut_compiler <- Stdin; true
| StepByStep(b) -> args.step_by_step <- b; true
| Seed(i) -> args.seed <- Some i; true
| Precision(i) -> args.precision <- i; true
| ComputeVolume(b) -> args.compute_volume <- b; true
| RandomSeed -> args.seed <- None; true
| Verbose(b) -> args.verbose <- b; true
| Reactive(b) -> args.reactive <- b; true
| ShowStep(b) -> args.show_step <- b; true
| Prompt(p) -> args.prompt <- Some p; true
| Prefix(p) -> args.prefix <- p; true
| DrawInside i -> args.draw_inside <- i; true
| DrawEdges i -> args.draw_edges <- i; true
| DrawVertices i-> args.draw_vertices <- i; true
| AllFormula b -> args.all_formula <- b; true
| AllVertices b -> args.all_vertices <- b; true
| Output(str) -> args.output <- str; true
| OverwriteOutput(b) -> args.overwrite_output <- b; true
| Log -> args.log <- true; true
| Clean ->
(* XXX Not portable !! *)
(* Clean up intermediary files *)
if args.scade_gui then (
let make = ExtTools.make in
let makefile = (Filename.concat args.tmp_dir "Makefile") in
let make_arg_list = (List.tl make) @ [ "-f"; makefile; "lurette_clean"] in
Unix.chdir args.tmp_dir;
Unix.putenv "SUT_DIR" args.tmp_dir;
Unix.putenv "SUT" args.sut_node;
Unix.putenv "USER_TESTING_DIR" (args.sut_dir);
Unix.putenv "LURETTE_TMP_DIR" (args.tmp_dir);
if args.luciole_mode then Unix.putenv "LURETTE_DRO" "lurette.dro";
ignore (Util.my_create_process ~std_out:(Unix.descr_of_out_channel args.ocr)
~std_err:(Unix.descr_of_out_channel args.ecr)
(List.hd make) make_arg_list)
)
else
if args.scade_gui then (
let make = ExtTools.make in
let makefile = (Filename.concat args.tmp_dir "Makefile") in
let make_arg_list = (List.tl make) @ [ "-f"; makefile; "lurette_clean"] in
Unix.chdir args.tmp_dir;
Unix.putenv "SUT_DIR" args.tmp_dir;
Unix.putenv "SUT" args.sut_node;
Unix.putenv "USER_TESTING_DIR" (args.sut_dir);
Unix.putenv "LURETTE_TMP_DIR" (args.tmp_dir);
if args.luciole_mode then Unix.putenv "LURETTE_DRO" "lurette.dro";
ignore (Util.my_create_process ~std_out:(Unix.descr_of_out_channel args.ocr)
~std_err:(Unix.descr_of_out_channel args.ecr)
(List.hd make) make_arg_list)
)
else
(* XXX comme pour scade_gui ci dessus, je devrais faire ca via le makefile *)
(Util2.del (Filename.concat args.tmp_dir ("lurette")) args.ocr args.ecr;
Util2.del (Filename.concat args.tmp_dir ("*.*")) args.ocr args.ecr)
;
true
| Batch(file) -> LtopArg.gen_batch file; true
| ChDir(dir) ->
output_string args.ocr
(" The current directory for lurette is now " ^ dir ^
(Util2.del (Filename.concat args.tmp_dir ("lurette")) args.ocr args.ecr;
Util2.del (Filename.concat args.tmp_dir ("*.*")) args.ocr args.ecr)
;
true
| Batch(file) -> LtopArg.gen_batch file; true
| ChDir(dir) ->
output_string args.ocr
(" The current directory for lurette is now " ^ dir ^
(* "\n cygpath_dir = " ^ (Util.cygpath dir) ^ *)
"\n");
flush args.ocr ;
args.sut_dir <- dir;
true
| ChTmpDir(dir) ->
output_string args.ecr
(" The current temporary directory for lurette is now "^dir^"\n");
flush args.ecr ;
args.tmp_dir <- dir;
true
| BuildEnv ->
true
| Build ->
let build_ok = Build.f args in
if not build_ok then (
output_string args.ocr "\n*** Cannot build lurette, sorry.\n \n \n";
flush args.ocr
);
true
| Run -> (
check_rif_name ();
if not args.direct_mode then remove_outdated_files ();
if ( args.direct_mode || Build.f args) then (
Unix.chdir args.sut_dir;
let result = Run.f () in
if result <> 0
then (
output_string args.ocr "\n*** lurette has terminated abnormally.\n \n";
RunDirect.clean_terminate()
)
else output_string args.ocr "\nLurette has terminated normally.\n"
)
else
output_string args.ocr "\n*** Cannot build lurette, sorry.\n \n \n";
flush args.ocr;
Unix.chdir args.tmp_dir;
args.reset_cov_file <- false;
true
)
| Show ->
let sdir = Unix.getcwd () in
Unix.chdir args.sut_dir;
ignore (ExtTools.show_luc args.env);
Unix.chdir sdir;
true
| CallSim2chro ->
let sdir = Unix.getcwd () in
Unix.chdir args.sut_dir;
ignore (Util2.sim2chro args.output);
Unix.chdir sdir;
true
| CallGnuplot ->
let sdir = Unix.getcwd () in
Unix.chdir args.sut_dir;
Util2.gnuplot (args.verbose>1) args.output;
Unix.chdir sdir;
true
| CallGnuplotPs ->
let sdir = Unix.getcwd () in
Unix.chdir args.sut_dir;
ignore (Util2.gnuplot_ps args.output);
Unix.chdir sdir;
true
| Quit -> false
| Save -> LtopArg.gen_lurette_rc ();true
| HelpSimple ->
output_string args.ocr usage; flush args.ocr; true
| Help -> display (); true
| HelpMore -> display2 (); true
| Man -> output_string args.ocr man ; flush args.ocr; true
| LurettePdfMan -> Util2.lurette_man (); true
| LutinPdfMan -> Util2.lutin_man (); true
| LutinPdfTuto -> Util2.lutin_tuto (); true
| CGeneratorFlag(str) ->
args.c_generator <- str; true
| Pack(file) -> (* not working *)
assert false
(* let *)
(* cmd = ("mv " ^ args.tmp_dir ^ " /tmp/" ^ file ^ *)
(* "; cd " ^ args.sut_dir ^ "; tar cvfz " ^ *)
(* file ^ ".tgz /tmp/" ^ file ^ *)
(* " > tar.log; mv /tmp/" ^ *)
(* file ^ " " ^ args.tmp_dir ^ " >> tar.log " ) *)
(* in *)
(* let tar_res = *)
(* output_string args.ecr (cmd ^ "\n") ; *)
(* flush args.ecr; *)
(* Sys.command cmd *)
(* in *)
(* if tar_res <> 0 *)
(* then *)
(* ( *)
(* output_string args.ocr ("*** <<" ^ cmd ^ *)
(* ">> failed. Is gnu-tar in your path ?\n"); *)
(* flush args.ocr; *)
(* true *)
(* ) *)
(* else *)
(* true *)
| ExtraCFiles(str) ->
Unix.putenv "EXTRA_SOURCE_FILES" (String.escaped (get_full_path args.sut_dir str));
let cfiles = get_full_path args.sut_dir str in
args.extra_cfiles <- if cfiles = "" then None else Some cfiles;
true
| ExtraLibs(str) ->
Unix.putenv "EXTRA_LIBS" (String.escaped str);
args.extra_libs <- if str = "" then None else Some str;
true
| ExtraLibDirs(str) ->
Unix.putenv "EXTRA_LIBDIRS" (String.escaped str);
args.extra_libdirs <- if str = "" then None else Some str;
true
| ExtraIncludeDirs(str) ->
Unix.putenv "EXTRA_INCLUDEDIRS" (String.escaped str);
args.extra_includedirs <- if str = "" then None else Some str;
true
| Error(errmsg) ->
output_string args.ocr errmsg;
flush args.ocr;
output_string args.ocr usage;
flush args.ocr;
true
"\n");
flush args.ocr ;
args.sut_dir <- dir;
true
| ChTmpDir(dir) ->
output_string args.ecr
(" The current temporary directory for lurette is now "^dir^"\n");
flush args.ecr ;
args.tmp_dir <- dir;
true
| BuildEnv ->
true
| Build ->
let build_ok = Build.f args in
if not build_ok then (
output_string args.ocr "\n*** Cannot build lurette, sorry.\n \n \n";
flush args.ocr
);
true
| Run -> (
check_rif_name ();
if not args.direct_mode then remove_outdated_files ();
if ( args.direct_mode || Build.f args) then (
Unix.chdir args.sut_dir;
let result = Run.f () in
if result <> 0
then (
output_string args.ocr "\n*** lurette has terminated abnormally.\n \n";
RunDirect.clean_terminate()
)
else output_string args.ocr "\nLurette has terminated normally.\n"
)
else
output_string args.ocr "\n*** Cannot build lurette, sorry.\n \n \n";
flush args.ocr;
Unix.chdir args.tmp_dir;
args.reset_cov_file <- false;
true
)
| Show ->
let sdir = Unix.getcwd () in
Unix.chdir args.sut_dir;
ignore (ExtTools.show_luc args.env);
Unix.chdir sdir;
true
| CallSim2chro ->
let sdir = Unix.getcwd () in
Unix.chdir args.sut_dir;
ignore (Util2.sim2chro args.output);
Unix.chdir sdir;
true
| CallGnuplot ->
let sdir = Unix.getcwd () in
Unix.chdir args.sut_dir;
Util2.gnuplot (args.verbose>1) args.output;
Unix.chdir sdir;
true
| CallGnuplotPs ->
let sdir = Unix.getcwd () in
Unix.chdir args.sut_dir;
ignore (Util2.gnuplot_ps args.output);
Unix.chdir sdir;
true
| Quit ->
RunDirect.clean_terminate();
false
| Save -> LtopArg.gen_lurette_rc ();true
| HelpSimple ->
output_string args.ocr usage; flush args.ocr; true
| Help -> display (); true
| HelpMore -> display2 (); true
| Man -> output_string args.ocr man ; flush args.ocr; true
| LurettePdfMan -> Util2.lurette_man (); true
| LutinPdfMan -> Util2.lutin_man (); true
| LutinPdfTuto -> Util2.lutin_tuto (); true
| CGeneratorFlag(str) ->
args.c_generator <- str; true
| Pack(file) -> (* not working *)
assert false
(* let *)
(* cmd = ("mv " ^ args.tmp_dir ^ " /tmp/" ^ file ^ *)
(* "; cd " ^ args.sut_dir ^ "; tar cvfz " ^ *)
(* file ^ ".tgz /tmp/" ^ file ^ *)
(* " > tar.log; mv /tmp/" ^ *)
(* file ^ " " ^ args.tmp_dir ^ " >> tar.log " ) *)
(* in *)
(* let tar_res = *)
(* output_string args.ecr (cmd ^ "\n") ; *)
(* flush args.ecr; *)
(* Sys.command cmd *)
(* in *)
(* if tar_res <> 0 *)
(* then *)
(* ( *)
(* output_string args.ocr ("*** <<" ^ cmd ^ *)
(* ">> failed. Is gnu-tar in your path ?\n"); *)
(* flush args.ocr; *)
(* true *)
(* ) *)
(* else *)
(* true *)
| ExtraCFiles(str) ->
Unix.putenv "EXTRA_SOURCE_FILES" (String.escaped (get_full_path args.sut_dir str));
let cfiles = get_full_path args.sut_dir str in
args.extra_cfiles <- if cfiles = "" then None else Some cfiles;
true
| ExtraLibs(str) ->
Unix.putenv "EXTRA_LIBS" (String.escaped str);
args.extra_libs <- if str = "" then None else Some str;
true
| ExtraLibDirs(str) ->
Unix.putenv "EXTRA_LIBDIRS" (String.escaped str);
args.extra_libdirs <- if str = "" then None else Some str;
true
| ExtraIncludeDirs(str) ->
Unix.putenv "EXTRA_INCLUDEDIRS" (String.escaped str);
args.extra_includedirs <- if str = "" then None else Some str;
true
| Error(errmsg) ->
output_string args.ocr errmsg;
flush args.ocr;
output_string args.ocr usage;
flush args.ocr;
true
)
with
e ->
RunDirect.clean_terminate();
output_string args.ocr ("Bad lurette command: "
^ (Printexc.to_string e) ^ " ("^str^") \n") ;
output_string args.ocr usage ;
......
......@@ -561,10 +561,10 @@ let rec speclist =
"<string>\tfile name coverage info will be put into";
"--reset-cov-file", Arg.Unit (fun _ -> args.reset_cov_file <- true),
"<bool>\t";
"";
"--stop-on-oracle-error", Arg.Unit (fun _ -> args.stop_on_oracle_error <- true),
"<bool>\t";
"";
"--test-length", Arg.Int (fun i -> args.step_nb <- i),
"<int>\tNumber of steps to be done";
......
......@@ -206,8 +206,9 @@ let lurettetop_quit msg () =
Sys.remove tmp_file ;
Unix.chdir args.sut_dir;
flush args.ecr;
output_string args.ecr (msg^"\nlurettetop: bye!\n");
flush args.ecr
flush args.ocr
let main_loop_start () =
......@@ -243,6 +244,7 @@ let _ =
with e ->
print_string ("*** lurettetop: " ^ (Printexc.to_string e) ^ "\n");
flush stdout;
lurettetop_quit "" ()
lurettetop_quit "" ();
exit 0
;;
......@@ -38,8 +38,10 @@ let make argv =
in
let soc = try Soc.SocMap.find sk soc_tbl with Not_found -> assert false in
let vntl_of_profile = List.map (fun (x,t) -> x,SocUtils.string_of_type_ref t) in
let (vntl_i:Data.vntl) = vntl_of_profile (fst soc.profile) in
let (vntl_o:Data.vntl) = vntl_of_profile (snd soc.profile) in
let soc_inputs = (SocExec.expand_profile (fst soc.profile)) in
let soc_outputs = (SocExec.expand_profile (snd soc.profile)) in
let (vntl_i:Data.vntl) = vntl_of_profile soc_inputs in
let (vntl_o:Data.vntl) = vntl_of_profile soc_outputs in
let oc = stdout in
(* Lv6util.dump_entete oc; *)
(* Rif_base.write_interface oc vntl_i vntl_o None None; *)
......@@ -47,17 +49,25 @@ let make argv =
let (to_soc_subst : SocExecValue.ctx -> Soc.var list -> Data.subst list) =
fun ctx vl ->
List.map (fun var -> fst var, SocExecValue.get_value ctx (Var var)) vl
(* let sl = List.map (fun var -> fst var, SocExecValue.get_value ctx (Var var)) vl in *)
let sl = SocExecValue.filter_top_subst ctx.s in
let sl = List.flatten (List.map SocExec.expand_subst sl) in
(* If the order ever matters, I could try the following. :
try List.map (fun v -> fst v,
List.assoc (fst v) sl) vl with Not_found -> assert false
*)
sl
in
let (add_subst : Data.subst list -> SocExecValue.substs -> SocExecValue.substs) =
fun s ctx_s ->
fun s ctx_s ->
let s = SocExec.unexpand_profile s (fst soc.profile) in
List.fold_left (fun acc (id,v) -> SocExecValue.sadd acc [id] v) ctx_s s
in
let ctx_ref = ref (SocExecValue.create_ctx soc_tbl soc) in
let step sl_in =