Skip to content

GitLab

Commit bd7fcae5 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

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

Add Events when an elected contraint fails (backtrack).

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 6a203864
Hide whitespace changes
Inline Side-by-side
examples/lutin/ldbg/choice.lut
View file @ bd7fcae5
......@@ -6,12 +6,13 @@ let within(min,v,max:int) : bool =
node main () returns ( x : int) =
exist px:int in
exist ppx:int in
exist ppx:int in
within(0,x,10) fby
within(0,x,10) and px = pre x fby
assert (px = pre x and ppx = pre px) in
loop {
loop [100] {
| 100: within(px,x, ppx)
| 100: within(ppx,x, px)
| 1: within(0,x,10)
}
fby false
examples/lutin/ldbg/test3.ml
View file @ bd7fcae5
......@@ -68,6 +68,8 @@ let heat_off e =
List.mem_assoc "Heat_on" e.data &&
not (vb "Heat_on" e);;
(* set_sim2chro true;; *)
let e =run ();;
let e = next_cond e heat_off;;
let e = next_cond e heat_on;;
......@@ -75,15 +77,8 @@ 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;;
reset_rp();add_rp "env:lutin:ex1.lut:main2" ;set_sim2chro false;set_gnuplot false;show_src:=true;;
let e = run();;
break "ex1.lut::34" ;;
let e = continue e;;
......@@ -91,6 +86,7 @@ let e = continue e;;
(* hooks and custom traces *)
let my_print_event e =
match e.kind with
......@@ -101,6 +97,7 @@ let my_print_event e =
del_hooks "print_event";;
add_hooks ("print_event",my_print_event);;
let e = nexti e 20;;
del_hooks "print_event";;
let src =
let Node n = e.kind in
......
examples/lutin/ldbg/test4.ml
View file @ bd7fcae5
......@@ -2,7 +2,7 @@ open Event;;
open Ldbg;;
open Ldbg_utils;;
set_sim2chro false;;
set_sim2chro true;;
set_gnuplot false;;
ltop "set_seed 1";;
......@@ -22,6 +22,7 @@ print_string (dump_profile_info());;
exit 0;;
(*
let e = nexti e 10;;
break ""
......
source/Lurettetop/event.ml
View file @ bd7fcae5
type ctx = (* herited debug info *)
{
ctx_step :int;
ctx_depth :int;
ctx_name :string;
ctx_depth:int;
ctx_data: Data.subst list;
ctx_terminate: unit -> unit;
}
......@@ -30,10 +31,15 @@ type kind =
| Ltop
| Noinfo
type port =
| Exit
| Fail (* when an elected constraint is unsatisfiable *)
type t = {
nb:int;
step : int;
depth : int;
port : port;
kind : kind;
data : Data.subst list;
other : string;
......
source/Lurettetop/ldbg_utils.ml
View file @ bd7fcae5
......@@ -39,17 +39,22 @@ let (print_cstr : Event.t -> unit) =
| Node node -> print_string (" \"" ^(node()).cstr ^ "\"")
|_ -> ();;
let (port2str: Event.port -> string) =
function
Exit -> "exit"
| Fail -> "fail"
let print_event (e:t) =
let l = List.map (fun (vn,v) -> vn^"="^Data.val_to_string v) e.data in
let vals = if !show_data then String.concat "," l else "" in
let blanks = String.make e.depth ' ' in
(match e.kind with
(match e.kind with
| Node n ->
Printf.printf "%3i %3i %s%-15s\t[%s]" e.nb e.step blanks (n()).name vals;
Printf.printf "%3i %3i %s%s %-15s\t[%s]" e.nb e.step blanks (port2str e.port) (n()).name vals;
| Ltop ->
Printf.printf "%3i %3i %s%-15s\t[%s]" e.nb e.step blanks "ltop" vals;
Printf.printf "%3i %3i %s%s %-15s\t[%s]" e.nb e.step blanks (port2str e.port) "ltop" vals;
| Noinfo ->
Printf.printf "%3i %3i %s%-15s\t[%s]" e.nb e.step blanks "??" vals;
Printf.printf "%3i %3i %s%s %-15s\t[%s]" e.nb e.step blanks (port2str e.port) "??" vals;
);
if !show_constraint then print_cstr e;
print_string "\n";
......@@ -242,16 +247,17 @@ let (dump_profile_info : unit -> string) =
let str_l =
Hashtbl.fold
(fun si cpt acc->
(Printf.sprintf "| %5i | %5i | %4i | %40s | %10s | \n"
(fst si.char) (snd si.char) cpt si.str (Filename.basename si.file))::acc
(Printf.sprintf "| %3i-%-3i | %5i-%-5i | %4i | %40s | %10s | \n"
(fst si.line) (snd si.line) (fst si.char) (snd si.char)
cpt si.str (Filename.basename si.file))::acc
)
prof_tbl
[]
in
let str_l = Sort.list (fun a b -> compare a b < 0) str_l in
("|-------+-------+------+------------------------------------------+------------+ \n") ^
("| c_beg | c_end | hits | source code | file name |\n") ^
("|-------+-------+------+------------------------------------------+------------+ \n") ^
("\n|---------+-------------+------+------------------------------------------+------------+ \n") ^
("| lines | chars | hits + source code | file name |\n") ^
("|---------+-------------+------+------------------------------------------+------------+ \n") ^
(String.concat "" str_l) ^
("|-------+-------+------+------------------------------------------+------------+ \n")
("|---------+-------------+------+------------------------------------------+------------+ \n")
source/Lurettetop/runDirect.ml
View file @ bd7fcae5
......@@ -286,7 +286,6 @@ let (start : unit -> Event.t) =
else
let luciole_outs = luciole_step (env_in_vals@pre_env_out_vals) in
let env_in_vals = List.rev_append luciole_outs env_in_vals in
if args.ldbg then (* XXX l'idéal serait de faire ce test à
l'exterieur de la boucle en passant la
fonction qui va bien selon le
......@@ -296,6 +295,7 @@ let (start : unit -> Event.t) =
let ctx =
{
Event.ctx_step = i;
Event.ctx_name = "ltop";
Event.ctx_depth = 1;
Event.ctx_data = edata;
Event.ctx_terminate = (fun () -> killem_all cov)
......@@ -327,6 +327,7 @@ let (start : unit -> Event.t) =
let edata = sut_in_vals@ env_out_vals in
let ctx = { ctx with
Event.ctx_step = i;
Event.ctx_name = "ltop";
Event.ctx_depth = 1;
Event.ctx_data = edata;
}
......@@ -389,6 +390,7 @@ let (start : unit -> Event.t) =
let edata = sut_out_vals@ env_out_vals@oracle_out_vals in
let ctx = { ctx with
Event.ctx_step = i;
Event.ctx_name = "ltop";
Event.ctx_depth = 1;
Event.ctx_data = edata;
}
......@@ -398,6 +400,7 @@ let (start : unit -> Event.t) =
Event.step = i;
Event.kind = Event.Ltop;
Event.depth = 1;
Event.port = Event.Exit;
Event.data = edata;
Event.other = "";
Event.next =
......@@ -434,6 +437,7 @@ let (start : unit -> Event.t) =
let ctx =
{
Event.ctx_step = 1;
Event.ctx_name = "ltop";
Event.ctx_depth = 1;
Event.ctx_data = [];
Event.ctx_terminate = (fun () -> killem_all cov_init)
......
source/Lutin/lutExe.ml
View file @ bd7fcae5
......@@ -389,6 +389,9 @@ contextual_lutexp2exp (it:t) data e = (
exception Deadlock of int (* Attach the event nb to ease debugging when this exc
is raised at top-level *)
exception DeadlockE of Event.t
exception Stop
exception Exception of string
type internal_state = control_state * Var.env
......@@ -485,13 +488,17 @@ let check_satisfiablity (it:t) (g: guard) = (
let (cstr_src_info_of_val_exp : Syntaxe.val_exp -> int * int * int * int) =
fun e ->
let rec aux (bl,el,bc,ec) e =
let acc =
(min bl e.Lexeme.src.Lexeme.line,
max el e.Lexeme.src.Lexeme.line,
min bc e.Lexeme.src.Lexeme.chstart,
max ec e.Lexeme.src.Lexeme.chend)
in
let bl = min bl e.Lexeme.src.Lexeme.line
and el = max el e.Lexeme.src.Lexeme.line
and bc = min bc e.Lexeme.src.Lexeme.chstart
and ec = max ec e.Lexeme.src.Lexeme.chend in
let acc = (bl,el,bc,ec) in
match e.Lexeme.it with
| Syntaxe.PRE_n id ->
(min bl id.Lexeme.src.Lexeme.line,
max el id.Lexeme.src.Lexeme.line,
min bc id.Lexeme.src.Lexeme.chstart,
max ec id.Lexeme.src.Lexeme.chend)
| 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
......@@ -531,29 +538,31 @@ let rec (to_src_info: CoIdent.src_stack -> Event.src_info) =
}
(** Add a new constraint to an existing guard *)
let add_to_guard it data (e:CoAlgExp.t) (acc:guard) (si:CoTraceExp.src_info) = (
let add_to_guard_nc it data (e:CoAlgExp.t) (acc:guard) (si:CoTraceExp.src_info) =
(* translate e into an Exp.t using lucky_exp_of with an id2exp:
- that performs unalias
- that replace input/pre values
*)
(* necessarily a formula (bool exp), if we rely on type checking ! *)
(* let xenv = it.expanded_code in *)
let le = contextual_lutexp2exp it data e in
let f = match le with
| Exp.Formu f -> f
| _ -> assert false
in
let nf = match acc.g_form with
| Exp.True -> f
| x -> Exp.And (f, x)
in
let res = {
g_form = nf;
g_sol = None;
g_src = if snd si = [] then acc.g_src else (snd si)::acc.g_src
}
in
let le = contextual_lutexp2exp it data e in
let f = match le with
| Exp.Formu f -> f
| _ -> assert false
in
let nf = match acc.g_form with
| Exp.True -> f
| x -> Exp.And (f, x)
in
{
g_form = nf;
g_sol = None;
g_src = if snd si = [] then acc.g_src else (snd si)::acc.g_src
}
(** Add a new constraint to an existing guard *)
let add_to_guard it data (e:CoAlgExp.t) (acc:guard) (si:CoTraceExp.src_info) = (
let res = add_to_guard_nc it data e acc si in
if (check_satisfiablity it res) then res
else raise (Deadlock !Event.event_nb)
)
......@@ -835,6 +844,7 @@ let rec genpath
try (
rec_genpath ({br with br_ctrl=te})
) with Deadlock _ -> (
Event.incr_nb ();
rec_genpath ({br with br_ctrl=(TE_prio tel)})
)
)
......@@ -1420,12 +1430,11 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
)
(** Constraint: ~same but solve the conjunction first *)
| TE_constraint (ae,si) -> (
let new_acc = add_to_guard it data ae acc si in
br_cont.doit_ldbg (Goto (new_acc, TE_eps)) cont
(*
let edata = (Value.OfIdent.content data.curs)
in
let new_acc = add_to_guard_nc it data ae acc si in
if (check_satisfiablity it new_acc) then
br_cont.doit_ldbg (Goto (new_acc, TE_eps)) cont
else
let edata = (Value.OfIdent.content data.curs) in
let edata =
List.map (fun (n,v) -> n, Value.to_data_val v) edata
in
......@@ -1433,37 +1442,33 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
let predata =
List.map (fun (n,v) -> "pre_" ^ n, Value.to_data_val v) predata
in
let enb = Event.incr_nb (); Event.get_nb () in
let event =
{
Event.step = ctx.Event.ctx_step;
Event.nb = enb;
Event.nb = Event.get_nb ();
Event.depth = ctx.Event.ctx_depth;
Event.port = Event.Fail;
Event.kind = (* compute it if necessary only *)
Event.Node (* CstrUnsat ? *)
(fun () -> {
Event.lang = "lutin";
Event.name = "XXX get it from ctx !";
Event.src =
Event.name = ctx.Event.ctx_name;
Event.src =
List.map to_src_info (
if snd si = [] then acc.g_src else (snd si)::acc.g_src);
if snd si = [] then acc.g_src else (snd si)::acc.g_src);
Event.cstr = CoAlgExp.lus_dumps ae;
Event.inputs = []; (* get it from ctx ? *)
Event.outputs = [];
});
Event.other = "Backtrack";
Event.other = "";
Event.data = edata @ predata;
Event.next =
(* n.b. raise Deadlock if impossible *)
(fun () ->
Event.event_nb := enb ;
raise (Deadlock enb));
(fun () -> failwith "dead code");
Event.terminate = ctx.Event.ctx_terminate;
}
in
event
*)
raise (DeadlockE event)
)
(** Sequence *)
| TE_fby (te1, te2) -> (
......@@ -1489,22 +1494,33 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
*)
| TE_prio [] -> raise (Deadlock !Event.event_nb)
| TE_prio (te::tel) -> (
try (
rec_genpath_ldbg ({br with br_ctrl_ldbg=te}) cont
) with Deadlock _ -> (
rec_genpath_ldbg ({br with br_ctrl_ldbg=(TE_prio tel)}) cont
)
try rec_genpath_ldbg ({br with br_ctrl_ldbg=te}) cont
with
| DeadlockE e ->
{ e with
Event.nb = (Event.incr_nb (); Event.get_nb ());
Event.next =
(fun () ->
rec_genpath_ldbg ({br with br_ctrl_ldbg=(TE_prio tel)}) cont
)
}
)
(** Try similar to a recurse priority *)
| TE_try (e,eco) -> (
let cont2 try_cont =
try rec_genpath_ldbg ({br with br_ctrl_ldbg=e; br_cont_ldbg=try_cont}) cont
with Deadlock _ -> (
let ec = match eco with
| Some e' -> e'
| None -> TE_eps
in
rec_genpath_ldbg ({br with br_ctrl_ldbg=ec}) cont
with DeadlockE e -> (
{ e with
Event.nb = (Event.incr_nb (); Event.get_nb ());
Event.next =
(fun () ->
let ec = match eco with
| Some e' -> e'
| None -> TE_eps
in
rec_genpath_ldbg ({br with br_ctrl_ldbg=ec}) cont
)
}
)
in
mk_cont_ldbg
......@@ -1612,18 +1628,15 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
(* 1st do a trans ... *)
| Goto (cl,n) -> (
let cont3 para_tail_cont =
try (
(* N.B. cl CONTAINS incoming acc, thus it becomes the whole rec_acc *)
let tail_acc = cl in
(*** BIG BUG: the other_brs IS NOT THE RIGHT ONE ->
SHOULD BE THE ONE REACHED WHEN THE Goto (cl,n) WAS GENERATED !!!
***)
rec_genpath_ldbg ({br with
br_ctrl_ldbg= TE_para(el);
br_acc_ldbg=tail_acc;
br_cont_ldbg=para_tail_cont}) lcont
) with Deadlock i -> raise (Deadlock i)
(* HERE: nothing to do ? *)
(* N.B. cl CONTAINS incoming acc, thus it becomes the whole rec_acc *)
let tail_acc = cl in
(*** BIG BUG: the other_brs IS NOT THE RIGHT ONE ->
SHOULD BE THE ONE REACHED WHEN THE Goto (cl,n) WAS GENERATED !!!
***)
rec_genpath_ldbg ({br with
br_ctrl_ldbg= TE_para(el);
br_acc_ldbg=tail_acc;
br_cont_ldbg=para_tail_cont}) lcont
in
mk_cont_ldbg
(fun a lcont ->
......@@ -2087,8 +2100,9 @@ and (to_reactive_prg_ldbg : Event.ctx -> string -> t -> internal_state -> Value.
Value.to_data_val (Value.OfIdent.get locs (Var.name x)))
(loc_var_list it)
in
let nctx = { ctx with (* ??? *)
let nctx = { ctx with
Event.ctx_step = ctx.Event.ctx_step+1;
Event.ctx_name = rid;
}
in
let enb = Event.incr_nb (); Event.get_nb () in
......@@ -2097,6 +2111,7 @@ and (to_reactive_prg_ldbg : Event.ctx -> string -> t -> internal_state -> Value.
Event.step = ctx.Event.ctx_step;
Event.nb = enb;
Event.depth = ctx.Event.ctx_depth;
Event.port = Event.Exit;
Event.kind = (* compute it if necessary only *)
Event.Node
(fun () -> {
......@@ -2141,7 +2156,7 @@ let get_behavior_gen : t -> Var.env_in -> Var.env -> control_state -> (unit -> b
try (
let b = genpath it data cstate in
SomeBehavior (b, and_thats_all)
) with Deadlock i -> NoMoreBehavior i
) with Deadlock i -> NoMoreBehavior (i+1)
)
)
......@@ -2154,12 +2169,9 @@ let get_behavior_gen_ldbg : t -> Var.env_in -> Var.env -> control_state -> Event
let data = { curs = ins; pres=pres } in
let cont2 (b:behavior) =
let and_thats_all () = NoMoreBehavior 0 in
cont(
try SomeBehavior (b, and_thats_all)
with Deadlock i -> NoMoreBehavior i)
cont(SomeBehavior (b, and_thats_all))
in
genpath_ldbg it data cstate ctx cont2
genpath_ldbg it data cstate ctx cont2
(***************************************************************************************)
......@@ -2216,7 +2228,11 @@ let (step_ldbg: Event.ctx -> string -> t -> control_state -> data_state ->
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
in
let ctx = { ctx with Event.ctx_depth = 2 } in
let ctx = { ctx with
Event.ctx_depth = 2;
Event.ctx_name = node
}
in
let cont2 = fun bg ->
match bg with
| NoMoreBehavior i -> raise (Deadlock i) (* failwith "NoMoreBehavior" *)
......@@ -2256,6 +2272,7 @@ let (step_ldbg: Event.ctx -> string -> t -> control_state -> data_state ->
Event.step = ctx.Event.ctx_step;
Event.nb = enb;
Event.depth = ctx.Event.ctx_depth;
Event.port = Event.Exit;
Event.kind =
Event.Node (fun () -> {
Event.lang = "lutin";
......@@ -2274,8 +2291,14 @@ let (step_ldbg: Event.ctx -> string -> t -> control_state -> data_state ->
)
in
(* XXX Tout de meme, cette fonction ressemble beaucoup à to_reactive_prg_ldbg... *)
get_behavior_gen_ldbg prog data.ins data.mems ctrl ctx cont2
try
get_behavior_gen_ldbg prog data.ins data.mems ctrl ctx cont2
with
DeadlockE e ->
{ e with
Event.nb = (Event.incr_nb (); Event.get_nb ());
Event.next = (fun () -> raise (Deadlock (Event.get_nb ())));
}
(***************************************************************************************)
(*** DEBUG ***)
......
source/common/lustreRun.ml
View file @ bd7fcae5
......@@ -92,6 +92,7 @@ let (make_ec : string -> vars * vars * (string -> unit) *
Event.nb = Event.get_nb ();
Event.step = ctx.Event.ctx_step;
Event.depth = ctx.Event.ctx_depth;
Event.port = Event.Exit;
Event.kind = Event.Node (fun () ->
{
Event.lang = "lustre";
......@@ -215,6 +216,7 @@ let (make_socket_do : string -> int -> in_channel *
Event.step = ctx.Event.ctx_step;
Event.data = ctx.Event.ctx_data;
Event.depth = ctx.Event.ctx_depth;
Event.port = Event.Exit;
Event.nb = Event.get_nb ();
Event.kind = Event.Node (fun () ->
{
......@@ -320,6 +322,7 @@ let (make_ec_exe : string -> vars * vars * (string -> unit) *
Event.data = ctx.Event.ctx_data;
Event.nb = Event.get_nb ();
Event.depth = ctx.Event.ctx_depth;
Event.port = Event.Exit;
Event.kind = Event.Node (fun () ->
{
Event.lang = "ec";
......@@ -505,6 +508,7 @@ let (make_ocaml : string -> vars * vars *
Event.data = ctx.Event.ctx_data;
Event.nb = Event.get_nb ();
Event.depth = ctx.Event.ctx_depth;
Event.port = Event.Exit;
Event.kind = Event.Node (fun () ->
{
Event.lang = "ocaml";
......
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