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

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

Trace also the SUT if it is a Lutin program.

Attach the event number to the Deadlock exception in non debug mode
to ease the debugging when an unexpected deadlock is raised at
top-level.
parent c89314bd
let abs(x : real) : real =
if x > 0.0 then x else -x
let between(x, min, max : real) : bool =
((min < x) and (x < max))
node draw_temp(h:bool; t:real) returns (nt:real) =
assert (abs(t - nt) < 1.0 ) in
loop { if h then nt >= t else nt <= t }
node temp(Heat_on : bool)
returns (T,T1, T2, T3 : real) =
assert abs(T-T1) < 0.5 in
assert abs(T-T2) < 0.5 in
assert abs(T-T3) < 0.5 in
between(T, 6.0, 9.0)
fby
loop
run T := draw_temp(Heat_on, pre T)
-----------------------------------------------------------------
let FAILURE = -999.0 -- a fake temperature given when all sensors are broken
let TMIN = 6.0
let TMAX = 9.0
let DELTA = 0.5
-- returns the average values of 2 reals
let average(a, b : real) : real =
(a+b)/2.0
-- returns the maximum values of 2 reals
let max3 (a,b,c : real) : real =
if a<b then (if b < c then c else b) else
if a<c then c else a
let min3 (a,b,c : real) : real =
if a>b then (if b > c then c else b) else
if a>c then c else a
-- returns the median values of 3 reals
let median(a, b, c : real) : real =
a + b + c - min3(a,b,c) - max3 (a,b,c)
let noneoftree (f1, f2, f3 : bool) : bool =
((not f1) and (not f2) and (not f3))
let alloftree (f1, f2, f3 : bool) : bool =
(f1 and f2 and f3)
let oneoftree (f1, f2, f3 : bool) : bool =
((f1 and (not f2) and (not f3)) or
(f2 and (not f1) and (not f3)) or
(f3 and (not f1) and (not f2)))
node ctrl (T,T1, T2, T3 : real)
returns (Heat_on : bool;
V12, V13, V23 : bool;
Tguess : real) =
-- exist V12, V13, V23 : bool in
-- exist Tguess : real in
Heat_on = true fby
loop
(V12 = (abs(T1-T2) < DELTA)) and -- Are T1 and T2 valid?
(V13 = (abs(T1-T3) < DELTA)) and -- Are T1 and T3 valid?
(V23 = (abs(T2-T3) < DELTA)) and -- Are T2 and T3 valid?
(Tguess =
if noneoftree(V12, V13, V23) then FAILURE else
if oneoftree(V12, V13, V23) then median(T1, T2, T3) else
if alloftree(V12, V13, V23) then median(T1, T2, T3) else
-- 2 among V1, V2, V3 are false
if V12 then average(T1, T2) else
if V13 then average(T1, T3) else
-- V23 is necessarily true, hence T1 is wrong *)
average(T2, T3)
)
and
(Heat_on =
if Tguess = FAILURE then false else
if Tguess < TMIN then true else
if Tguess > TMAX then false else
pre Heat_on)
open Event;;
open Ldbg;;
open Ldbg_utils;;
ltop "set_seed 1";;
add_rp "sut:lutin:heater.lut:temp" ;;
add_rp "env:lutin:heater.lut:ctrl" ;;
set_sim2chro false;;
set_gnuplot false;;
stl 1000;;
i();;
(* The =Event.t= definition *)
let e = run ();;
let e = e.next();;
print_event e;;
(* Step forward *)
let e = next e;;
let e = nexti e 20;;
let e = goto_i e 42;;
let e = goto_s e 42;;
(* Conditional breakpoints *)
vb "Heat_on" e;;
let heat_on e =
List.mem_assoc "Heat_on" e.data &&
(vb "Heat_on" e);;
let heat_off e =
List.mem_assoc "Heat_on" e.data &&
not (vb "Heat_on" e);;
let e = next_cond e heat_off;;
let e = next_cond e heat_on;;
(* gdb like Breakpoints *)
reset_rp();;
add_rp "env:lutin:ex1.lut:main2" ;;
i();;
set_sim2chro false;;
set_gnuplot false;;
show_src:=true;;
let e = run();;
break "ex1.lut::34" ;;
let e = continue e;;
(* hooks and custom traces *)
let my_print_event e =
match e.kind with
| Node n ->
print_string (n()).name
| _ -> ()
;;
del_hooks "print_event";;
add_hooks ("print_event",my_print_event);;
let e = nexti e 20;;
let src =
let Node n = e.kind in
List.iter (fun si -> print_string si.str) (n()).src;
n();;
(* Profiler *)
profiler true;;
let e = run();;
show_trace:=false;;
nexti e 1000;;
print_string (dump_profile_info());;
man();;
help "base";;
help "utils";;
help "run";;
apropos "";;
apropos "show";;
help "profiler";;
(* XXX *)
let src =
let Node n = e.kind in
List.iter (fun si -> print_string si.str) (n()).src;
n();;
(* recuperation des valeurs directes (sans passer par vi/vb/vf : string -> int/bool/float *)
open Data
let var_to_string v =
match v with
| B true -> "true"
| B false -> "false"
| I i -> string_of_int i
| F f -> string_of_float f
;;
let get_state st =
let nl,vl = List.split st in
let vstrl = List.map var_to_string vl in
let nl = List.map String.lowercase nl in
let str =
"let " ^ (String.concat "," nl) ^
" = " ^ (String.concat "," vstrl) ^ ";;\n"
in
print_string (str);
str
;;
print_string (get_state e.data);;
exit 0
open Event;;
open Ldbg;;
open Ldbg_utils;;
set_sim2chro false;;
set_gnuplot false;;
ltop "set_seed 1";;
add_rp "env:lutin:choice.lut:main" ;;
stl 1000;;
show_trace := true;;
profiler true;;
let e = run ();;
let e = nexti e 1000;;
print_string (dump_profile_info());;
exit 0;;
(*
break ""
*)
node within(min,max:int) returns (res:int) =
loop min <= res and res <= max
node more(x:int) returns (y:int) =
exist delta : int in
run delta := within(0,10) in
loop y = x+delta
node less(y:int) returns (x:int) =
exist delta : int in
run delta := within(0,10) in
x = 0 fby loop x = y-delta
-----------------------------------------------------------------
LTOP=../../../bin/lurettetop
LDBG=../../../bin/ldbg
LURETTETOP=$(LTOP) \
--test-length 100 --thick-draw 1 \
......@@ -87,7 +88,23 @@ ifneq (,$(findstring $(HOSTTYPE),win32))
taskkill /F /IM heater_control.exe || true
endif
cat test4.res
[ ! -s test4.res ] && make clean
[ ! -s test4.res ]
# check that lurettetop and ldbg produce the same rif
test5.rif: heater_control$(EXE)
rm -f test5.rif0 .lurette_rc
$(LDBG) -init test5.ml
grep -v "This is lurette Version" test5.rif0 > test5.rif
test5:test5.rif $(EXPDIR)/
rm -f test5.res
diff -B -u -i $(EXPDIR)/test4.rif.exp test5.rif > test5.res || true
ifneq (,$(findstring $(HOSTTYPE),win32))
taskkill /F /IM heater_control.exe || true
endif
cat test5.res
[ ! -s test5.res ] && make clean
......@@ -101,9 +118,12 @@ utest2:test2.rif
utest4:test4.rif
cp test4.rif $(EXPDIR)/test4.rif.exp
# nb : pas de utest5 car je me sert du test4 pour vérifier que je genere bien la meme
# trace en mode ldbg !!
utest: utest1 utest2 utest4
test: test1 test2 test4
test: test1 test2 test4 test5
%.ec: %.lus
../../../bin/lus2lic$(EXE) -ec $^ -n $* -o $@
......
......@@ -52,7 +52,9 @@ let check_rif_name () =
try
let i = Str.search_forward (Str.regexp "-[0-9]+\.rif") args.output 0 in
String.sub args.output 0 i
with Not_found -> Filename.chop_extension args.output
with Not_found ->
try Filename.chop_extension args.output
with _ -> args.output
in
args.output <- find_free_name base_name 1
......
......@@ -52,7 +52,8 @@ let (terminate : t -> unit) = fun e -> e.terminate ()
let (data : t -> Data.subst list) = fun e -> e.data
let event_nb = ref 0
let get_nb () =
incr event_nb; !event_nb
let get_nb () = !event_nb
let incr_nb() =
incr event_nb
......@@ -108,6 +108,27 @@ exception SutStop of cov_opt
let gnuplot_time = ref 0.0
(* Transform a map on a function list into CPS *)
let (step_dbg_sl :
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) list ->
's list -> 'ctx -> ('s list -> 'e) -> 'e) =
fun step_dbg_sl_l sl ctx cont ->
(* ouch! Celle-la est chevelue...
La difficulté, c'est de passer un 'List.map step' en CPS.
Suis-je aller au plus simple ? En tout cas j'ai réussit :)
*)
let rec (iter_step :
('s list -> 'ctx -> ('s list -> 'ctx -> 'e) -> 'e) list ->
's list list -> 's list -> 'e) =
fun stepl res_stepl sl ->
match stepl with
| [] -> cont (List.flatten (res_stepl))
| step::stepl -> step sl ctx (fun res_sl ctx -> iter_step stepl (res_sl::res_stepl) sl)
in
iter_step step_dbg_sl_l [] sl
let (start : unit -> Event.t) =
fun () ->
gnuplot_time := 0.0;
......@@ -117,7 +138,6 @@ let (start : unit -> Event.t) =
sut_init_in_l, sut_init_out_l = make_rp_list args.suts
in
let sut_kill msg = List.iter (fun f -> f msg) sut_kill_l in
let sut_step_sl sl = List.flatten (List.map (fun f -> f sl) sut_step_sl_l) in
let sut_init_in = List.flatten sut_init_in_l in
let sut_init_out = List.flatten sut_init_out_l in
......@@ -132,22 +152,6 @@ let (start : unit -> Event.t) =
env_init_in_l, env_init_out_l = make_rp_list args.envs
in
let env_kill msg = List.iter (fun f -> f msg) env_kill_l in
let (env_step_dbg_sl : 's list -> 'ctx -> ('s list -> 'e) -> 'e) =
fun sl ctx cont ->
(* ouch! Celle-la est chevelue...
La difficulté, c'est de passer un 'List.map step' en CPS.
Suis-je aller au plus simple ? En tout cas j'ai réussit :)
*)
let rec (iter_step :
('s list -> 'ctx -> ('s list -> 'ctx -> 'e) -> 'e) list ->
's list list -> 's list -> 'e) =
fun stepl res_stepl sl ->
match stepl with
| [] -> cont (List.flatten (res_stepl))
| step::stepl -> step sl ctx (fun res_sl ctx -> iter_step stepl (res_sl::res_stepl) sl)
in
iter_step env_step_dbg_sl_l [] sl
in
let _env_init_in = List.flatten env_init_in_l in
let _env_init_out = List.flatten env_init_out_l in
......@@ -298,9 +302,9 @@ let (start : unit -> Event.t) =
}
in
let cont = loop2 cov env_in_vals pre_env_out_vals ctx i luciole_outs in
env_step_dbg_sl env_in_vals ctx cont
step_dbg_sl env_step_dbg_sl_l env_in_vals ctx cont
else
let env_step_sl sl = List.flatten (List.map (fun f -> f sl) env_step_sl_l) in
let env_step_sl sl = List.flatten (List.map (fun f -> f sl) env_step_sl_l) in
let env_out_vals = env_step_sl env_in_vals in
loop2 cov env_in_vals pre_env_out_vals ctx i luciole_outs env_out_vals
(*
......@@ -318,11 +322,22 @@ let (start : unit -> Event.t) =
with Not_found -> env_out_vals
in
let env_out_vals = luciole_outs @ env_out_vals in
let sut_in_vals = filter env_out_vals flat_sut_in in
let sut_out_vals =
try sut_step_sl sut_in_vals
with Rif_base.Bye -> raise (SutStop cov)
in
let sut_in_vals = filter env_out_vals flat_sut_in in
if args.ldbg then
let edata = sut_in_vals@ env_out_vals in
let ctx = { ctx with
Event.ctx_step = i;
Event.ctx_depth = 1;
Event.ctx_data = edata;
}
in
let cont = loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i luciole_outs in
step_dbg_sl sut_step_dbg_sl_l sut_in_vals ctx cont
else
let sut_step_sl sl = List.flatten (List.map (fun f -> f sl) sut_step_sl_l) in
let sut_out_vals = sut_step_sl sut_in_vals in
loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i luciole_outs sut_out_vals
and loop3 cov env_in_vals pre_env_out_vals env_out_vals ctx i luciole_outs sut_out_vals =
let sut_out_vals =
try List.map (fun (v,vt) -> v,List.assoc v sut_out_vals) flat_sut_out
with Not_found -> sut_out_vals
......@@ -369,6 +384,7 @@ let (start : unit -> Event.t) =
(cf Lutin/main.ml also)
*)
then gnuplot_oc := Util2.gnuplotrif_dyn (args.verbose>1) args.output;
Event.incr_nb ();
if args.ldbg then
let edata = sut_out_vals@ env_out_vals@oracle_out_vals in
let ctx = { ctx with
......
......@@ -387,7 +387,8 @@ contextual_lutexp2exp (it:t) data e = (
(** exceptions and type *)
exception Deadlock
exception Deadlock of int (* Attach the event nb to ease debugging when this exc
is raised at top-level *)
exception Stop
exception Exception of string
type internal_state = control_state * Var.env
......@@ -494,6 +495,7 @@ let (cstr_src_info_of_val_exp : Syntaxe.val_exp -> int * int * int * int) =
| Syntaxe.CALL_n (_,vel) -> List.fold_left aux acc vel
| Syntaxe.ERUN_n(_, ve1, ve2) -> aux (aux acc ve1) ve2
| Syntaxe.RUN_n (_, ve1, _) -> aux acc ve1
| Syntaxe.ASSERT_n (_, ve1, _) -> aux acc ve1
| _ -> acc
in
aux (e.Lexeme.src.Lexeme.line, e.Lexeme.src.Lexeme.line,
......@@ -502,7 +504,7 @@ let (cstr_src_info_of_val_exp : Syntaxe.val_exp -> int * int * int * int) =
exception No_src_info
let rec (to_src_info: CoIdent.src_stack -> Event.src_info) =
fun l ->
fun l ->
match l with
| [] -> raise No_src_info
| (lxm, _,None)::tl ->
......@@ -517,15 +519,15 @@ let rec (to_src_info: CoIdent.src_stack -> Event.src_info) =
let line_b, line_e, char_b, char_e = cstr_src_info_of_val_exp ve in
let file = lxm.Lexeme.file in
let filecontent = Util.readfile file in
{
Event.str =
{
Event.str =
(try String.sub filecontent char_b (char_e - char_b + 1)
with _ ->
with _ ->
Printf.sprintf "%s: fail to get chars %i-%i" file char_b char_e);
Event.file = file;
Event.file = file;
Event.line = line_b, line_e;
Event.char = char_b, char_e;
Event.stack = if tl=[] then None else Some (to_src_info tl) ;
Event.stack = if tl=[] then None else Some (to_src_info tl);
}
......@@ -553,7 +555,7 @@ let add_to_guard it data (e:CoAlgExp.t) (acc:guard) (si:CoTraceExp.src_info) = (
}
in
if (check_satisfiablity it res) then res
else raise Deadlock
else raise (Deadlock !Event.event_nb)
)
(** Tries to compute a value in a context *)
......@@ -587,7 +589,7 @@ let string_of_behavior = function
| Raise x -> Printf.sprintf "Raise %s" x
type behavior_gen =
| NoMoreBehavior
| NoMoreBehavior of int
| SomeBehavior of behavior * (unit -> behavior_gen)
......@@ -796,7 +798,7 @@ let rec genpath
Verbose.put ~flag:dbg "-- noeps_cont (%s)\n in context %s\n"
(string_of_behavior a) (string_of_control_state x);
match a with
| Vanish -> raise Deadlock
| Vanish -> raise (Deadlock !Event.event_nb)
| z -> cont.doit z
(*
| Vanish -> raise Deadlock
......@@ -828,11 +830,11 @@ let rec genpath
(** Priority:
Deadlock is catched HERE
*)
| TE_prio [] -> raise Deadlock
| TE_prio [] -> raise (Deadlock !Event.event_nb)
| TE_prio (te::tel) -> (
try (
rec_genpath ({br with br_ctrl=te})
) with Deadlock -> (
) with Deadlock _ -> (
rec_genpath ({br with br_ctrl=(TE_prio tel)})
)
)
......@@ -848,7 +850,7 @@ let rec genpath
) (Ctry eco) cont in
try (
rec_genpath ({br with br_ctrl=e; br_cont=try_cont})
) with Deadlock -> (
) with Deadlock _ -> (
let ec = match eco with
| Some e' -> e'
| None -> TE_eps
......@@ -951,7 +953,7 @@ let rec genpath
(* others vanish, 1st continue *)
| Vanish -> ( cont.doit (Goto (cl,n)) )
(* others raise -> forbidden *)
| Raise s -> ( raise Deadlock )
| Raise s -> ( raise (Deadlock !Event.event_nb) )
| Goto (tcl, tn) -> (
(* N.B. cl IS ALREADY accumulated in tcl *)
cont.doit (Goto (tcl, put_in_para n tn))
......@@ -963,9 +965,9 @@ let rec genpath
SHOULD BE THE ONE REACHED WHEN THE Goto (cl,n) WAS GENERATED !!!
***)
rec_genpath ({br with br_ctrl= TE_para(el); br_acc=tail_acc; br_cont=para_tail_cont})
) with Deadlock -> (
) with Deadlock nb -> (
(* HERE: nothing to do ? *)
raise Deadlock
raise (Deadlock nb)
)
)
) (Cpara_head (TE_para el)) cont in
......@@ -1014,7 +1016,7 @@ let rec genpath
) in
let (sum, cel) = List.fold_left weval (0, []) wtel in
let e' = match cel with
| [] -> raise Deadlock
| [] -> raise (Deadlock !Event.event_nb)
| [(_,e)] -> e
| _ -> TE_dyn_choice (sum, cel)
in rec_genpath ({br with br_ctrl=e'})
......@@ -1056,7 +1058,7 @@ let rec genpath
*)
let (gw, sw) = getweights cpt in