Commit 421bcc4d authored by erwan's avatar erwan

Fix: This time, the rdbg time traveling work!

It was due to the event_incr function in MainArg, that is using a
reference to count event numbers, and that was not saved and restored
by LutinRun.

And this counter was used to set the PRGS! which is actually useless
as it is handled in LutinRun via save_state/restore_state now.

It is not clear if my monadisation work was really necessary. In
theory, it is, but not in the examples I've tried. Sigh.
parent 4f5a18d5
...@@ -16,7 +16,7 @@ $(EXPDIR): ...@@ -16,7 +16,7 @@ $(EXPDIR):
# several oracles # several oracles
test1.rif: heater_control$(EXE) $(EXPDIR) test1.rif: heater_control$(EXE) $(EXPDIR)
rm -f test1.rif0 .lurette_rc rm -f test1.rif0 .lurette_rc
$(LURETTETOP) -go --output test1.rif0 \ $(LURETTETOP) -go --output test1.rif0 --seed 42 \
-rp "sut:ec_exe:./heater_control.ec:" \ -rp "sut:ec_exe:./heater_control.ec:" \
-rp "oracle:v6:heater_control.lus:not_a_sauna" \ -rp "oracle:v6:heater_control.lus:not_a_sauna" \
-rp "oracle:v6:heater_control.lus:not_a_fridge" \ -rp "oracle:v6:heater_control.lus:not_a_fridge" \
...@@ -75,10 +75,10 @@ test3:test3.rif $(EXPDIR) ...@@ -75,10 +75,10 @@ test3:test3.rif $(EXPDIR)
# several env # several env
test4.rif: heater_control$(EXE) test4.rif: heater_control$(EXE)
rm -f test4.rif0 .lurette_rc rm -f test4.rif0 .lurette_rc
$(LURETTETOP) -go --output test4.rif0 \ $(LURETTETOP) -go --output test4.rif0 --seed 3 \
-rp "sut:ec_exe:./heater_control.ec:" \ -rp "sut:ec_exe:./heater_control.ec:" \
-rp "env:lutin:env.lut:-m:main1:-seed:3" \ -rp "env:lutin:env.lut:-m:main1" \
-rp "env:lutin:env.lut:-m:main2:-seed:3" && \ -rp "env:lutin:env.lut:-m:main2" && \
grep -v "lurette chronogram" test4.rif0 | \ grep -v "lurette chronogram" test4.rif0 | \
grep -v "This is lurette Version" test4.rif0 | grep -v "#seed" | \ grep -v "This is lurette Version" test4.rif0 | grep -v "#seed" | \
grep -v "The execution lasted"| sed -e "s/^M//" > test4.rif grep -v "The execution lasted"| sed -e "s/^M//" > test4.rif
......
...@@ -24,7 +24,7 @@ utest:test.rif ...@@ -24,7 +24,7 @@ utest:test.rif
clean: clean:
rm -rf $(OBJDIR) rm -rf *.res *.log *~ *.rif0 *.rif *.gp *.plot rm -rf $(OBJDIR) rm -rf *.res *.log *~ *.rif0 *.rif *.gp *.plot *.dro *.dot
......
...@@ -347,7 +347,8 @@ let (to_string : t -> (string * string * string) list) = ...@@ -347,7 +347,8 @@ let (to_string : t -> (string * string * string) list) =
let gen_lurette_rc () = let gen_lurette_rc () =
let oc = open_out ".lurette_rc" in let oc = open_out ".lurette_rc" in
let l = List.filter (fun (cmd,opt,arg) -> cmd<>"" || arg<>"" || opt <> "") (to_string args) in let l = List.filter (fun (cmd,opt,arg) -> cmd<>"" || arg<>"" || opt <> "")
(to_string args) in
let l = List.map (fun (cmd, _, arg) -> cmd ^ " " ^ arg ^ "\n") l in let l = List.map (fun (cmd, _, arg) -> cmd ^ " " ^ arg ^ "\n") l in
List.iter (output_string oc) l; List.iter (output_string oc) l;
flush oc; flush oc;
...@@ -356,7 +357,8 @@ let gen_lurette_rc () = ...@@ -356,7 +357,8 @@ let gen_lurette_rc () =
close_out oc close_out oc
let gen_lurettetop_call args = let gen_lurettetop_call args =
let l = List.filter (fun (cmd,opt,arg) -> cmd<>"" || arg<>"" || opt <> "") (to_string args) in let l = List.filter (fun (cmd,opt,arg) -> cmd<>"" || arg<>"" || opt <> "")
(to_string args) in
let l = List.map (fun (_, opt, arg) -> opt ^ " " ^ arg ^ " ") l in let l = List.map (fun (_, opt, arg) -> opt ^ " " ^ arg ^ " ") l in
String.concat "" l String.concat "" l
...@@ -403,7 +405,7 @@ let (parse_rp_string : string -> unit) = ...@@ -403,7 +405,7 @@ let (parse_rp_string : string -> unit) =
None -> rp_args None -> rp_args
| Some i -> rp_args@["-seed";string_of_int i]) | Some i -> rp_args@["-seed";string_of_int i])
in in
Lutin(Array.of_list rp_args ) Lutin(Array.of_list rp_args )
(* (*
for lutin programs we accept: for lutin programs we accept:
...@@ -578,6 +580,9 @@ let rec speclist = ...@@ -578,6 +580,9 @@ let rec speclist =
"--cov-file", Arg.String (fun s -> args.cov_file <- s), "--cov-file", Arg.String (fun s -> args.cov_file <- s),
"<string>\tfile name coverage info will be put into"; "<string>\tfile name coverage info will be put into";
"--seed", Arg.Int (fun s -> args.seed <- Some s),
"<string>\tSet the seed provided to Lutin programs";
"--reset-cov-file", Arg.Unit (fun _ -> args.reset_cov_file <- true), "--reset-cov-file", Arg.Unit (fun _ -> args.reset_cov_file <- true),
""; "";
......
...@@ -446,8 +446,8 @@ and ...@@ -446,8 +446,8 @@ and
Util.sort_list_string_pair local_var_name_and_type_list_unsorted Util.sort_list_string_pair local_var_name_and_type_list_unsorted
in in
set_luciole_mode_if_necessary init_state sut_i_vntl sut_o_vntl [] []; set_luciole_mode_if_necessary init_state sut_i_vntl sut_o_vntl [] [];
Random.init seed ; (* Random.init seed ; *)
output_msg ("\nThe random engine was initialized with the seed "^(soi seed)^"\n"); (* output_msg ("\nThe random engine was initialized with the seed "^(soi seed)^"\n"); *)
(* Initialisation of the sut and the oracle *) (* Initialisation of the sut and the oracle *)
Sut.init (); Sut.init ();
......
...@@ -208,19 +208,21 @@ let lurettetop_quit msg () = ...@@ -208,19 +208,21 @@ let lurettetop_quit msg () =
let main_loop_start () = let main_loop_start () =
output_string args.ocr ("This is Lurette Version "^(Version.str)^" (\""^Version.sha^"\") \n"); output_string args.ocr ("This is Lurette Version "^(Version.str)^
" (\""^Version.sha^"\") \n");
flush args.ocr; flush args.ocr;
if not (args.go) then (main_loop 1; Unix.chdir args.sut_dir) else if not (args.go) then (main_loop 1; Unix.chdir args.sut_dir) else
(if args.direct_mode || Build.f args then ( (if args.direct_mode || Build.f args then (
Unix.chdir args.sut_dir; Unix.chdir args.sut_dir;
let res = Run.f () in let res = Run.f () in
if (res) <> 0 then ( if (res) <> 0 then (
Printf.fprintf args.ocr "\nLurette launched a process that failed (exit %d).\n \n" res; Printf.fprintf args.ocr
flush args.ocr; "\nLurette launched a process that failed (exit %d).\n \n" res;
Sys.catch_break false; flush args.ocr;
exit res Sys.catch_break false;
); exit res
) );
)
else else
( (
output_string args.ocr "Can not build lurette, sorry\n \n \n"; output_string args.ocr "Can not build lurette, sorry\n \n \n";
......
...@@ -248,11 +248,11 @@ let (start : unit -> Event.t) = ...@@ -248,11 +248,11 @@ let (start : unit -> Event.t) =
(LustreRun.make_luciole "./lurette_luciole.dro" luciole_in luciole_out), (LustreRun.make_luciole "./lurette_luciole.dro" luciole_in luciole_out),
luciole_out luciole_out
in in
let seed = (* let seed = *)
match args.seed with (* match args.seed with *)
| None -> random_seed () (* | None -> random_seed () *)
| Some seed -> seed (* | Some seed -> seed *)
in (* in *)
let cov_init = (* XXX faut-il renommer les sorties de l'oracle ou raler en let cov_init = (* XXX faut-il renommer les sorties de l'oracle ou raler en
cas de clash ? *) cas de clash ? *)
if List.flatten oracle_out_l = [] then NO else if List.flatten oracle_out_l = [] then NO else
...@@ -512,7 +512,7 @@ let (start : unit -> Event.t) = ...@@ -512,7 +512,7 @@ let (start : unit -> Event.t) =
let loc = None in let loc = None in
let _ = let _ =
Random.init seed; (* Random.init seed; *)
Rif.write oc ("# This is lurette Version " ^ Version.str ^ Rif.write oc ("# This is lurette Version " ^ Version.str ^
" (\"" ^Version.sha^"\")\n"); " (\"" ^Version.sha^"\")\n");
......
...@@ -179,29 +179,29 @@ let rec (num_is_an_int : num -> bool) = ...@@ -179,29 +179,29 @@ let rec (num_is_an_int : num -> bool) =
Util.hfind type_num_tbl e Util.hfind type_num_tbl e
with Not_found -> with Not_found ->
let res = let res =
match e with match e with
Sum(e1, e2) -> num_is_an_int e1 Sum(e1, e2) -> num_is_an_int e1
| Diff(e1, e2) -> num_is_an_int e1 | Diff(e1, e2) -> num_is_an_int e1
| Prod(e1, e2) -> num_is_an_int e1 | Prod(e1, e2) -> num_is_an_int e1
| Quot(e1, e2) -> num_is_an_int e1 | Quot(e1, e2) -> num_is_an_int e1
| Mod(e1, e2) -> num_is_an_int e1 | Mod(e1, e2) -> num_is_an_int e1
| Uminus(e) -> num_is_an_int e | Uminus(e) -> num_is_an_int e
| Div(e1, e2) -> num_is_an_int e1 | Div(e1, e2) -> num_is_an_int e1
| Ivar(var) -> true | Ivar(var) -> true
| Fvar(var) -> false | Fvar(var) -> false
| Ival(i) -> true | Ival(i) -> true
| Fval(f) -> false | Fval(f) -> false
| Ite(f,e1,e2) -> num_is_an_int e1 | Ite(f,e1,e2) -> num_is_an_int e1
| Inf_int -> true | Inf_int -> true
| FFC _ -> false | FFC _ -> false
| IFC _ -> true | IFC _ -> true
| Gcont(_,_,_) -> true | Gcont(_,_,_) -> true
| Gstop(_,_,_) -> true | Gstop(_,_,_) -> true
| Icont(_,_,_) -> true | Icont(_,_,_) -> true
| Istop(_,_,_) -> true | Istop(_,_,_) -> true
in in
Hashtbl.add type_num_tbl e res; Hashtbl.add type_num_tbl e res;
res res
(* exported *) (* exported *)
......
...@@ -266,7 +266,7 @@ let make opt infile mnode = ( ...@@ -266,7 +266,7 @@ let make opt infile mnode = (
Verbose.put ~flag:dbg "LutExe.make: Expand.make %s OK\n" mnode; Verbose.put ~flag:dbg "LutExe.make: Expand.make %s OK\n" mnode;
(* actual result .... *) (* actual result .... *)
(* Verbose.put ~flag:dbg "Event.set_seed %i\n"(MainArg.seed opt); *) (* Verbose.put ~flag:dbg "Event.set_seed %i\n"(MainArg.seed opt); *)
(* Event.set_seed (MainArg.seed opt); (* transmit the seed to the event handler *) *) MainArg.set_seed opt (Some (MainArg.seed opt));
if MainArg.run opt then if MainArg.run opt then
of_expanded_code opt exped of_expanded_code opt exped
else else
...@@ -798,7 +798,10 @@ let rec genpath (t : t) (data : store) (* data env = inputs + pres *) ...@@ -798,7 +798,10 @@ let rec genpath (t : t) (data : store) (* data env = inputs + pres *)
let id2trace s = let id2trace s =
(Util.StringMap.find s (Expand.trace_tab xenv)).Expand.ti_def_exp (Util.StringMap.find s (Expand.trace_tab xenv)).Expand.ti_def_exp
in in
let it = ref t in (* it's too much work to make it a monad *) let it = ref t in
(* it's too much work to make it a monad.
well, i've did it for genpath_ldbg!
*)
(*-------------------------------------------* (*-------------------------------------------*
* Fonction récursive : * Fonction récursive :
* --------------------------------------------*) * --------------------------------------------*)
......
(* Time-stamp: <modified the 25/04/2019 (at 10:21) by Erwan Jahier> *) (* Time-stamp: <modified the 29/04/2019 (at 15:22) by Erwan> *)
(**********************************************************************************) (**********************************************************************************)
type vars = (string * Data.t) list type vars = (string * Data.t) list
...@@ -34,6 +34,7 @@ let make argv = ...@@ -34,6 +34,7 @@ let make argv =
and node = MainArg.main_node opt and node = MainArg.main_node opt
in in
let seed = MainArg.seed opt in let seed = MainArg.seed opt in
(* MainArg.set_seed opt (Some seed); *)
let lut_mach = LutExe.make opt prog node in let lut_mach = LutExe.make opt prog node in
let lut_in = List.map var_to_var_pair (LutExe.in_var_list lut_mach) in let lut_in = List.map var_to_var_pair (LutExe.in_var_list lut_mach) in
let lut_out = List.map var_to_var_pair (LutExe.out_var_list lut_mach) in let lut_out = List.map var_to_var_pair (LutExe.out_var_list lut_mach) in
...@@ -103,12 +104,14 @@ let make argv = ...@@ -103,12 +104,14 @@ let make argv =
if List.mem "-seed" argv_list then argv_str else if List.mem "-seed" argv_list then argv_str else
argv_str ^ " -seed " ^ (string_of_int seed) argv_str ^ " -seed " ^ (string_of_int seed)
in in
let version = Printf.sprintf "with lutin Version %s (\"%s\")" Version.str Version.sha in let version = Printf.sprintf "with lutin Version %s (\"%s\")"
Version.str Version.sha in
{ {
id = Printf.sprintf "%s (%s)" id version; id = Printf.sprintf "%s (%s)" id version;
inputs = lut_in; inputs = lut_in;
outputs= lut_out; outputs= lut_out;
reset = (fun () -> ( reset = (fun () -> (
tables := lut_mach;
ctrl_state := (LutExe.get_init_state lut_mach); ctrl_state := (LutExe.get_init_state lut_mach);
data_state := data_state :=
{ LutExe.ins = Value.OfIdent.empty; { LutExe.ins = Value.OfIdent.empty;
...@@ -120,17 +123,19 @@ let make argv = ...@@ -120,17 +123,19 @@ let make argv =
save_state = (fun i -> save_state = (fun i ->
let prgs = Random.get_state () in let prgs = Random.get_state () in
if Verbose.level() > 0 then ( if Verbose.level() > 0 then (
Printf.eprintf "Save state %i from Lutin (%i)\n" i Printf.eprintf "Save state %i from Lutin %s (%i)\n" i node
(Random.State.bits (Random.State.copy prgs)); (Random.State.bits (Random.State.copy prgs));
flush stderr); flush stderr);
Hashtbl.replace ss_table i (!ctrl_state, !data_state, prgs) Hashtbl.replace ss_table (i,node)
(!tables, !ctrl_state, !data_state, prgs)
); );
restore_state = (fun i -> restore_state = (fun i ->
match Hashtbl.find_opt ss_table i with match Hashtbl.find_opt ss_table (i,node) with
| Some (cs, ds, prgs) -> | Some (tbl,cs, ds, prgs) ->
if Verbose.level() > 0 then ( if Verbose.level() > 0 then (
Printf.eprintf Printf.eprintf
"Restore state %i from Lutin\n\tPRGS:%i\n\tins:%s\n\touts:%s\n\tmems:%s\n" i "Restore state %i from %s:%s\n\tPRGS:%i\n\tins:%s\n\touts:%s\n\tmems:%s\n"
i (String.concat "+" prog) node
(Random.State.bits (Random.State.copy prgs)) (Random.State.bits (Random.State.copy prgs))
(compact (Value.OfIdent.to_string "" ds.LutExe.ins)) (compact (Value.OfIdent.to_string "" ds.LutExe.ins))
(compact (Value.OfIdent.to_string "" ds.LutExe.outs)) (compact (Value.OfIdent.to_string "" ds.LutExe.outs))
...@@ -139,6 +144,7 @@ let make argv = ...@@ -139,6 +144,7 @@ let make argv =
; ;
flush stderr flush stderr
); );
tables := tbl;
ctrl_state := cs; data_state := ds; ctrl_state := cs; data_state := ds;
Random.set_state prgs; Random.set_state prgs;
| None -> Printf.eprintf "Cannot restore state %i from Lutin\n" i; flush stderr | None -> Printf.eprintf "Cannot restore state %i from Lutin\n" i; flush stderr
......
...@@ -95,6 +95,7 @@ let set_seed opt s = ...@@ -95,6 +95,7 @@ let set_seed opt s =
(match s with (match s with
| Some i -> | Some i ->
Printf.fprintf stderr "The random engine seed is set to %i\n" i; Printf.fprintf stderr "The random engine seed is set to %i\n" i;
Random.init i;
flush stderr; flush stderr;
| None -> ()); | None -> ());
opt._seed <- s opt._seed <- s
...@@ -108,7 +109,7 @@ let reset_the_seed_to_last opt = ...@@ -108,7 +109,7 @@ let reset_the_seed_to_last opt =
try try
let ic = open_in f in let ic = open_in f in
let seed = int_of_string (input_line ic) in let seed = int_of_string (input_line ic) in
set_seed opt (Some seed); opt._seed <- Some seed;
true true
with _ -> with _ ->
Printf.eprintf "W: cannot recover the seed in %s\n" f; Printf.eprintf "W: cannot recover the seed in %s\n" f;
...@@ -139,10 +140,7 @@ let rec seed opt = match opt._seed with ...@@ -139,10 +140,7 @@ let rec seed opt = match opt._seed with
*) *)
(* let event_nb = ref 0 *) (* let event_nb = ref 0 *)
let event_incr opt = let event_incr opt =
let seed = seed opt in
opt._event_nb <- opt._event_nb + 1; opt._event_nb <- opt._event_nb + 1;
(* To make sure everything can be reproduced with and without rdbg *)
Random.full_init [|seed; opt._event_nb|];
() ()
......
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