Commit 6b8c3cbb authored by Erwan Jahier's avatar Erwan Jahier
Browse files

A 14th step towards a Morphine lutin/lustre debugger for lurette/lutin/lustre.

Make sure everything is reproductible during time traveling, or when
starting back from any stored event, by reseting the random seed
using the event number each time the event number changes.

Add time travelling support (à la appel/Tolmach) in Ldbg_utils.
parent b556e7b2
......@@ -21,6 +21,7 @@ print_string (dump_profile_info());;
exit 0;;
(*
let e = nexti e 10;;
......@@ -28,3 +29,18 @@ let e = nexti e 10;;
break ""
*)
time_travel true;;
ckpt_rate:=200;;
let e = run ();;
let e = nexti e 105;;
let e = back e ;;
let stop_at i e = e.nb = i;;
let e = rev_cond e (stop_at 42);;
let e = rev_cond e (stop_at 0);;
let e = rev_cond e (fun e -> stop_at 42 e || stop_at 48 e );;
......@@ -27,7 +27,7 @@ test1.rif: heater_control$(EXE) $(EXPDIR)
test1: test1.rif $(EXPDIR)
rm -f test1.res
diff -B -u -i $(EXPDIR)/test1.rif.exp test1.rif > test1.res || true
diff -u -i $(EXPDIR)/test1.rif.exp test1.rif > test1.res || true
ifneq (,$(findstring $(HOSTTYPE),win32))
taskkill /F /IM ecexe.exe || true
taskkill /F /IM heater_control.exe || true
......@@ -46,7 +46,7 @@ test2.rif:
grep -v "The execution lasted"| sed -e "s/^M//" > test2.rif
test2:test2.rif $(EXPDIR)
rm -f test2.res diff -B -u -i $(EXPDIR)/test2.rif.exp test2.rif > test2.res || true
rm -f test2.res diff -u -i $(EXPDIR)/test2.rif.exp test2.rif > test2.res || true
ifneq (,$(findstring $(HOSTTYPE),win32))
taskkill /F /IM ecexe.exe || true
endif
......@@ -66,7 +66,7 @@ test3.rif: heater_control.cmxs
test3:test3.rif $(EXPDIR)
rm -f test3.res
diff -B -u -i $(EXPDIR)/test3.rif.exp test3.rif > test3.res || true
diff -u -i $(EXPDIR)/test3.rif.exp test3.rif > test3.res || true
cat test3.res
[ ! -s test3.res ] && make clean
......@@ -83,7 +83,7 @@ test4.rif: heater_control$(EXE)
test4:test4.rif $(EXPDIR)/
rm -f test4.res
diff -B -u -i $(EXPDIR)/test4.rif.exp test4.rif > test4.res || true
diff -u -i $(EXPDIR)/test4.rif.exp test4.rif > test4.res || true
ifneq (,$(findstring $(HOSTTYPE),win32))
taskkill /F /IM heater_control.exe || true
endif
......@@ -99,7 +99,7 @@ test5.rif: heater_control$(EXE)
test5:test5.rif $(EXPDIR)/
rm -f test5.res
diff -B -u -i $(EXPDIR)/test4.rif.exp test5.rif > test5.res || true
diff -u -i $(EXPDIR)/test4.rif.exp test5.rif > test5.res || true
ifneq (,$(findstring $(HOSTTYPE),win32))
taskkill /F /IM heater_control.exe || true
endif
......@@ -173,7 +173,7 @@ test_dontgo:
$(LURETTETOP) --output test.rif0 env.lut && \
grep -v "lurette chronogram" test.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif &&\
rm -f test.res && diff -B -u -i $(EXPDIR)/test.rif.exp test.rif > test.res
rm -f test.res && diff -u -i $(EXPDIR)/test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
......
......@@ -3,13 +3,13 @@ LTOP=/usr/local/tools/lustre-misc/lurette/i386-linux-gcc3/bin/lurettetop
LTOP=../../../../bin/lurettetop
LURETTETOP=$(LTOP) --precision 2 \
LURETTETOP=$(LTOP) --precision 2 --seed 3\
-rp "sut:v6:heater_control.lus:heater_control" \
-rp "oracle:v6:heater_control.lus:not_a_sauna" \
-rp "env:lutin:env.lut:main" \
--thick-draw 1 \
--draw-inside 0 --draw-edges 0 --draw-vertices 0 --draw-all-vertices \
--step-mode Inside --local-var --no-gnuplot --no-sim2chro --seed 3 \
--step-mode Inside --local-var --no-gnuplot --no-sim2chro \
--do-not-show-step
EXPDIR=`$(LTOP) --ocaml-version`
......
......@@ -31,8 +31,8 @@ type node_info = {
port : port;
name : string;
lang : string;
inputs : string list;
outputs : string list;
inputs : string list; (* static info *)
outputs : string list; (* static info *)
}
type kind =
......@@ -62,9 +62,15 @@ let (next : t -> t) = fun e -> e.next ()
let (terminate : t -> unit) = fun e -> e.terminate ()
let (data : t -> Data.subst list) = fun e -> e.data
let seed = ref 42
let set_seed s = seed := s
let event_nb = ref 0
let set_nb i = event_nb := i
let get_nb () = !event_nb
let incr_nb() =
Random.init (!seed + !event_nb); (* make sure everything is reproductible *)
incr event_nb
......@@ -118,10 +118,10 @@ let (show_luc : string -> bool) =
(my_create_process
(Filename.concat lurette_bin ("show_luc"))
(luc_file::(
match args.pp with
None -> []
| Some p -> if p = "" then [] else ["-pp"; p]
)
match args.pp with
None -> []
| Some p -> if p = "" then [] else ["-pp"; p]
)
)
stdin args.ocr args.ecr
)
......
......@@ -77,6 +77,12 @@ let (del_hooks : string -> unit) =
fun str ->
hooks := List.remove_assoc str !hooks
let (run : unit -> Event.t) =
fun () ->
let e = Ldbg.run () in
List.iter (fun (_,f) -> f e) !hooks;
e
(******************************************************************)
(* Moving forward *)
......@@ -92,7 +98,7 @@ let rec (nexti : Event.t -> int -> Event.t) =
let rec (next_cond : Event.t -> (Event.t -> bool) -> Event.t) =
fun e p ->
let ne = next e in
if p ne then (print_event ne;ne) else (
if p ne then ne else (
next_cond ne p
)
......@@ -181,7 +187,7 @@ let (break_matches : Event.t -> string -> bool) =
| _ -> false
)
let (goto : Event.t -> string -> Event.t) =
let (goto_brk : Event.t -> string -> Event.t) =
fun e b ->
next_cond e (fun e -> break_matches e b)
......@@ -269,3 +275,86 @@ let (dump_profile_info : unit -> string) =
(String.concat "" str_l) ^
("|---------+-------------+------+------------------------------------------+------------+ \n")
(******************************************************************)
(* Going backwards *)
let ckpt_rate = ref 10
let ckpt_tbl = Hashtbl.create 100
let check_point e =
if e.nb mod !ckpt_rate = 0 || e.nb = 1 then
let x = (e.nb / !ckpt_rate) in
(* Printf.printf "Add entry nb %i (event nb %i)\n" x e.nb; *)
(* flush stdout; *)
Hashtbl.add ckpt_tbl x e
let (time_travel : bool -> unit) =
fun on ->
if on then add_hooks ("time_travel",check_point)
else del_hooks "time_travel"
(* move backwards until a cond is reached *)
let (rev_cond : Event.t -> (Event.t -> bool) -> Event.t) =
fun e p ->
let rec rev_aux e i =
(* search if there exist an event e' in ]e.nb;i[ s.t. p e *)
(* let _ = *)
(* Printf.printf "rev_aux e.nb=%i i=%i\n" e.nb i; *)
(* assert (e.nb <= i); *)
(* flush stdout; *)
(* in *)
let e = if p e then e else next_cond e (fun e -> p e || e.nb = i) in
if p e then
rev_aux_last e e i (* search for a more recent one *)
else (* e.nb = i *)
let x = (e.nb / !ckpt_rate - 1) in
if x < 0 then
(print_string "No suitable event found\n";
Event.set_nb 1;
Hashtbl.find ckpt_tbl 0)
else
let e = Hashtbl.find ckpt_tbl x in
Event.set_nb e.nb;
rev_aux e ((x+1) * !ckpt_rate -1)
and rev_aux_last e e_good i =
(* search if there exist an event e in ]e_good.n;i[ s.t. p e *)
(* let _ = *)
(* Printf.printf "rev_aux_last e.nb=%i e_good.nb=%i i=%i\n" e.nb e_good.nb i; *)
(* flush stdout; *)
(* in *)
if e.nb = i then e_good else
let e = next_cond e (fun e -> p e || e.nb = i) in
let e_good = if p e then e else e_good in
rev_aux_last e e_good i
in
if e.nb = 1 then
failwith "Cannot move backwards from the first event.\n"
else
let x = ((e.nb - 1)/ !ckpt_rate) in
let last_e = Hashtbl.find ckpt_tbl x in
Event.set_nb last_e.nb;
rev_aux last_e (e.nb-1)
(* move backwards until a breakpoint is reached *)
let (rev : Event.t -> Event.t) =
fun e ->
let stop e = List.exists (break_matches e) !breakpoints in
rev_cond e stop
let stop_at i e = e.nb = i;;
let (back : Event.t -> Event.t) =
fun e ->
let stop ce = (ce.nb = e.nb - 1) in
let e = rev_cond e stop in
e
let (goto : Event.t -> int -> Event.t) =
fun e i ->
if i > e.nb then goto_i e i else if e.nb = i then e else
rev_cond e (fun e -> e.nb = i)
......@@ -71,7 +71,7 @@ val delete : unit -> unit
val continue : Event.t -> Event.t
(** Goto to a specific explicit breakpoint (cf 'break' for breakpoints syntax) *)
val goto : Event.t -> string -> Event.t
val goto_brk : Event.t -> string -> Event.t
(** set on/off the profiler *)
......@@ -82,3 +82,16 @@ val reset_profiler : unit -> unit
(** Dump profiling info *)
val dump_profile_info : unit -> string
(** move backwards *)
val time_travel : bool -> unit
val ckpt_rate:int ref
val rev : Event.t -> Event.t
val rev_cond : Event.t -> (Event.t -> bool) -> Event.t
val run : unit -> Event.t
(** move one step back *)
val back : Event.t -> Event.t
(** go to event nb i (backward or forward) *)
val goto : Event.t -> int -> Event.t
......@@ -379,12 +379,21 @@ let (parse_rp_string : string -> unit) =
let rp =
match rp_args with
| ["lutin";prog; node] ->
(* for backward compatibility *)
let rp_args = Array.of_list("lutin"::prog::"-main"::node::[]) in
Lutin(rp_args)
(* for backward compatibility, i add the 'main' in necessary... *)
let rp_args = ("lutin"::prog::"-main"::node::[]) in
let rp_args =
(match args.seed with
None -> rp_args
| Some i -> rp_args@["-seed";string_of_int i])
in
Lutin(Array.of_list rp_args )
| "lutin"::_ ->
let rp_args = Array.of_list rp_args in
Lutin(rp_args)
let rp_args =
(match args.seed with
None -> rp_args
| Some i -> rp_args@["-seed";string_of_int i])
in
Lutin(Array.of_list rp_args )
(*
for lutin programs we accept:
......
......@@ -232,7 +232,7 @@ let make opt infile mnode = (
let mainprg =
assert (infile <> []);
Parsers.reinit_parser ();
Parsers.read_lut infile
Parsers.read_lut infile
in
Verbose.put ~flag:dbg "LutExe.make: Parsers.read_lut infile [%s] OK\n"
(String.concat ";" infile);
......@@ -260,7 +260,8 @@ Verbose.put ~flag:dbg "LutExe.make: CheckType.check_pack OK\n";
let exped = Expand.make tlenv mainprg mnode in
Verbose.put ~flag:dbg "LutExe.make: Expand.make %s OK\n" mnode;
(* actual result .... *)
(* Printf.printf "Event.set_seed %i\n"(MainArg.seed opt);flush stdout; *)
Event.set_seed (MainArg.seed opt); (* transmit the seed to the event handler *)
if MainArg.run opt then
of_expanded_code opt exped
else
......@@ -865,6 +866,7 @@ let rec genpath
| Some e' -> e'
| None -> TE_eps
in
Event.incr_nb ();
rec_genpath ({br with br_ctrl=ec})
)
)
......@@ -1358,7 +1360,7 @@ and to_reactive_prg (it:t) (curstate:internal_state) (invals: Value.t list) = (
let addin acc invar inval = Value.OfIdent.add acc (Var.name invar,inval) in
let ins = List.fold_left2 addin Value.OfIdent.empty (in_var_list it) invals in
let data = { curs = ins; pres=pres } in
let b = genpath it data cstate in
let b = Event.incr_nb (); genpath it data cstate in
match b with
| Raise x -> raise (Exception x)
| Vanish -> raise Stop
......@@ -2143,7 +2145,7 @@ and (to_reactive_prg_ldbg : Event.ctx -> string -> t -> internal_state -> Value.
Event.depth = ctx.Event.ctx_depth;
Event.kind =
Event.Node {
Event.lang = "lutin";
Event.lang = "lutin";
Event.port = Event.Call;
Event.name = rid;
Event.inputs = ctx.Event.ctx_inputs;
......@@ -2209,6 +2211,7 @@ let (step: t -> control_state -> data_state -> control_state * data_state) =
*)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
Event.incr_nb ();
in
let bg = get_behavior_gen prog data.ins data.mems ctrl in
match bg () with
......
Supports Markdown
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