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

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

Add hooks support for Ldbg_utils.next.

Add a simple Ldbg_utils.profiler.

Add a reset_rp command.

Also, do not call clear_step all the time but only before the step
(which change some non-reg test).

Add a -check option to Lutin and performs all the checks but do not
run.
parent 3ae18d8a
let within(min,v,max:int) : bool =
min < v and v < max
node main () returns ( x : int) =
exist px: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 {
| 100: within(px,x, ppx)
| 100: within(ppx,x, px)
| 1: within(0,x,10)
}
......@@ -6,8 +6,8 @@
0.00 0.00 0.34 0.03 #outs f
#oracle_outs t 0.00 0.34 0.03
#step 1
0.00 0.00 0.12 -0.09 #outs t
#oracle_outs t 0.00 0.12 -0.09
0.00 0.00 -0.37 0.41 #outs t
#oracle_outs t 0.00 -0.37 0.41
#step 2
0.00 0.00 0.11 -0.41 #outs t
#oracle_outs t 0.00 0.11 -0.41
0.00 0.00 -0.38 0.08 #outs t
#oracle_outs t 0.00 -0.38 0.08
This diff is collapsed.
......@@ -21,7 +21,7 @@ OCAMLLDFLAGS= -cclib -lstdc++ -cclib -I/usr/lib/w32api \
endif
CC= $(GPP) $(DWIN32)
CC= $(GCC) $(DWIN32)
LIBS = unix dynlink str nums polka bdd
CLIBS = camlidl $(CLIBS_WIN32) bdd_stubs
......
......@@ -130,17 +130,8 @@ add_rp "^rp_help^"
env: "^ (String.concat "," (List.map reactive_program_to_string args.envs)) ^ "
oracle: "^ (String.concat "," (List.map reactive_program_to_string args.oracles)) ^ "
reset_rp sut
Reset the sut field. Its current value is: "
^ (String.concat "," (List.map reactive_program_to_string args.suts)) ^ "
reset_rp env
Reset the env field. Its current value is: "
^ (String.concat "," (List.map reactive_program_to_string args.envs)) ^ "
reset_rp oracle
Reset the oracle field. Its current value is: "
^ (String.concat "," (List.map reactive_program_to_string args.oracles)) ^ "
reset_rp
Reset the sut, env, and oracle fields
stl <integer>, set_test_length <integer>
Set the test length. Its current value is \"" ^
......@@ -421,6 +412,8 @@ let rec (parse_tok : tok -> t) =
(try parse_rp_string str; Nop
with Failure(msg) -> Error (msg)
)
| [< 'Genlex.Ident(_, "reset_rp") >] ->
args.oracles <- []; args.envs <- [] ; args.suts <- []; Nop
| [< 'Genlex.Ident(_, "set_root_node") ; node = parse_node >] -> RootNode(node)
......
......@@ -17,11 +17,11 @@ type src_info = {
type node_info = {
lang:string;
name: string;
src : src_info list;
lang : string;
name : string;
src : src_info list;
cstr : string; (* XXX poor name! *)
inputs : string list;
inputs : string list;
outputs : string list;
}
......@@ -32,12 +32,12 @@ type kind =
type t = {
nb:int;
step : int;
step : int;
depth : int;
kind : kind;
data: Data.subst list;
kind : kind;
data : Data.subst list;
other : string;
next: unit -> t;
next : unit -> t;
terminate: unit -> unit;
}
(* ou bien un MapString ?
......
......@@ -17,7 +17,7 @@ let info() = ltop "i"
let i = info
let stl i = ltop ("stl " ^ (string_of_int i))
let add_rp str = ltop ("add_rp \"" ^ str ^ "\"")
let set_rp str = ltop ("set_rp \"" ^ str ^ "\"")
let reset_rp () = ltop ("reset_rp")
(* XXX finish me! *)
let set_gnuplot b = LtopArg.args.LtopArg.display_gnuplot <- b
......@@ -133,7 +133,7 @@ let a = apropos
let _ =
output_string stdout (" This is ldbg Version "^(Version.str)^" ("^Version.sha^") \n");
output_string stdout "type
Ldbg.man ();;
man ();;
for a small on-line manual\n";
flush stdout
......
......@@ -7,9 +7,11 @@ val run : unit -> Event.t
val off : unit -> unit
(** add a Reactive program *)
val add_rp : string -> unit
val set_rp : string -> unit
(** reset a Reactive programs *)
val reset_rp : unit -> unit
(** Display info about the test parameters *)
val info : unit -> unit
......
......@@ -56,12 +56,24 @@ let print_event (e:t) =
if !show_src then print_src e;
flush stdout
(******************************************************************)
(* hooks (functions that are called after each next) *)
let (hooks: (string * (Event.t -> unit)) list ref) =
ref ["print_event",(fun e -> if !show_trace then print_event e)]
let add_hooks h = hooks := (h::!hooks)
let (del_hooks : string -> unit) =
fun str ->
hooks := List.remove_assoc str !hooks
(******************************************************************)
(* Moving forward *)
let next e =
let ne = Event.next e in
if !show_trace then print_event ne;
List.iter (fun (_,f) -> f ne) !hooks;
ne
let rec (nexti : Event.t -> int -> Event.t) =
......@@ -92,6 +104,9 @@ let rec (goto_s : Event.t -> int -> Event.t) =
fun e i ->
if e.step < i then goto_s (next e) i else e
let rec loopforever e = loopforever (e.next ());;
(******************************************************************)
(* Breakpoints stuff *)
......@@ -127,24 +142,33 @@ let (break_matches : Event.t -> string -> bool) =
"file"
"file::line"
*)
let si_match_file str si =
(si.file = str || Filename.basename si.file = str)
in
let si_match_line ln {line=(d,f)} =
let i = try int_of_string ln with _ -> -1 in
(d <= i && i <= f)
in
match e.kind, Str.split (Str.regexp "::") b with
| (Ltop|Noinfo),_ -> false
| Node _, [] -> false
| Node n, str::[] -> (n()).name = str
| Node n, str::ln::[] ->
let line = try int_of_string ln with _ -> -1 in
| Node n, str::tail ->
let ni = n() in
if Sys.file_exists str then
List.exists
(fun si ->
Filename.basename si.file = str &&
(fst si.line <= line && line <= snd si.line))
(n()).src
match tail with
| [ln] ->
List.exists
(fun si -> si_match_file str si && si_match_line ln si) ni.src
| [] -> List.exists (si_match_file str) ni.src
| _ -> false
else
(n()).name = str &&
(List.exists
(fun si -> (fst si.line <= line && line <= snd si.line))
(n()).src)
| _,_ -> false
(* str in a node *)
ni.name = str &&
(match tail with
| [] -> true
| [ln] -> List.exists (si_match_line ln) ni.src
| _ -> false
)
let (goto : Event.t -> string -> Event.t) =
fun e b ->
......@@ -185,3 +209,49 @@ let (vb:string -> Event.t -> bool) =
match List.assoc n e.data with
| Data.B b -> b
| _ -> failwith (n^" is not a bool")
(******************************************************************)
(* a very simple Profiler *)
let prof_tbl = Hashtbl.create 50
let incr_prof si =
try
let cpt = Hashtbl.find prof_tbl si in
Hashtbl.replace prof_tbl si (cpt+1)
with
Not_found -> Hashtbl.add prof_tbl si 1
let (prof_add: Event.t -> unit) =
fun e ->
match e.kind with
| Node n -> List.iter incr_prof (n()).src
| _ -> ()
let (profiler : bool -> unit) =
fun on ->
if on then add_hooks ("profile",prof_add)
else del_hooks "profile"
let (reset_profiler : unit -> unit) =
fun () ->
Hashtbl.clear prof_tbl
let (dump_profile_info : unit -> string) =
fun () ->
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
)
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") ^
(String.concat "" str_l) ^
("|-------+-------+------+------------------------------------------+------------+ \n")
(** Returns the next event *)
(** Compute the next event, call the hooks functions on it, and return that event *)
val next : Event.t -> Event.t
val hooks: (string * (Event.t -> unit)) list ref
(** Add a function that is called after each next call *)
val add_hooks : (string * (Event.t -> unit)) -> unit
(** Remove a hook *)
val del_hooks : string -> unit
(** Returns the ith next event *)
val nexti : Event.t -> int -> Event.t
......@@ -12,6 +21,9 @@ val goto_i : Event.t -> int -> Event.t
(** go to step number i *)
val goto_s : Event.t -> int -> Event.t
(** loop forever *)
val loopforever : Event.t -> Event.t
(** control the printing of skipped events *)
val show_trace : bool ref
......@@ -61,3 +73,12 @@ val continue : Event.t -> Event.t
(** Goto to a specific explicit breakpoint (cf 'break' for breakpoints syntax) *)
val goto : Event.t -> string -> Event.t
(** set on/off the profiler *)
val profiler : bool -> unit
(** Reset profiling info *)
val reset_profiler : unit -> unit
(** Dump profiling info *)
val dump_profile_info : unit -> string
......@@ -260,7 +260,11 @@ 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 .... *)
of_expanded_code opt exped
if MainArg.run opt then
of_expanded_code opt exped
else
exit 0
) with
Sys_error(s) -> (
prerr_string (s^"\n") ; exit 1
......@@ -410,10 +414,10 @@ let find_some_sols
= match g.g_sol with
| Some s -> s
| None ->
(* Formula_to_bdd.clear_step (); *)
(* !Solver.clear_snt (); *)
let zesol = (
(* clean everything in case ? *)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
(* HERE : don't know exactly why but it seems to be
necessary to call Solver.is_satisfiable first
......@@ -452,6 +456,7 @@ let find_some_sols
zesol
)
let find_one_sol it g =
let thick = match MainArg.step_mode it.arg_opt with
| Lucky.StepInside -> (1,0,Thickness.AtMost 0)
......@@ -513,7 +518,10 @@ let rec (to_src_info: CoIdent.src_stack -> Event.src_info) =
let file = lxm.Lexeme.file in
let filecontent = Util.readfile file in
{
Event.str = String.sub filecontent char_b (char_e - char_b + 1);
Event.str =
(try String.sub filecontent char_b (char_e - char_b + 1)
with _ ->
Printf.sprintf "%s: fail to get chars %i-%i" file char_b char_e);
Event.file = file;
Event.line = line_b, line_e;
Event.char = char_b, char_e;
......@@ -544,8 +552,8 @@ let add_to_guard it data (e:CoAlgExp.t) (acc:guard) (si:CoTraceExp.src_info) = (
g_src = if snd si = [] then acc.g_src else (snd si)::acc.g_src
}
in
if (check_satisfiablity it res) then res
else raise Deadlock
if (check_satisfiablity it res) then res
else raise Deadlock
)
(** Tries to compute a value in a context *)
......@@ -1366,9 +1374,9 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
let id2trace s =
(Hashtbl.find (Expand.trace_tab xenv) s).Expand.ti_def_exp
in
(*-------------------------------------------*
* Fonction récursive :
* --------------------------------------------*)
(*-------------------------------------------*
* Fonction récursive :
* --------------------------------------------*)
let rec (rec_genpath_ldbg : branch_ldbg -> (behavior -> Event.t) -> Event.t) =
fun br cont -> (
let data = br.br_data_ldbg in
......@@ -1385,9 +1393,9 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
Printf.fprintf stderr "--------\n";
);
match br.br_ctrl_ldbg with
(** Aliased trace *)
(** Aliased trace *)
| TE_ref s -> (rec_genpath_ldbg ({br with br_ctrl_ldbg = id2trace s}) cont)
(** Leaves: apply cont *)
(** Leaves: apply cont *)
| TE_raise s -> br_cont.doit_ldbg (Raise s) cont
| TE_eps -> br_cont.doit_ldbg Vanish cont
(** No eps: forbids e to vanish (but not to raise !) *)
......@@ -1407,11 +1415,52 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
br_cont
cont2
)
(** Constraint: ~same but solve the conjunction first *)
(** 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
(* n.b. raise Deadlock if impossible *)
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 edata =
List.map (fun (n,v) -> n, Value.to_data_val v) edata
in
let predata = (Value.OfIdent.content data.pres) in
let predata =
List.map (fun (n,v) -> "pre_" ^ n, Value.to_data_val v) predata
in
let enb = Event.get_nb () in
let event =
{
Event.step = ctx.Event.ctx_step;
Event.nb = enb;
Event.depth = ctx.Event.ctx_depth;
Event.kind = (* compute it if necessary only *)
Event.Node (* CstrUnsat ? *)
(fun () -> {
Event.lang = "lutin";
Event.name = "XXX get it from ctx !";
Event.src =
List.map to_src_info (
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.data = edata @ predata;
Event.next =
(* n.b. raise Deadlock if impossible *)
(fun () ->
Event.event_nb := enb ;
raise Deadlock);
Event.terminate = ctx.Event.ctx_terminate;
}
in
event
*)
)
(** Sequence *)
| TE_fby (te1, te2) -> (
......@@ -1432,18 +1481,18 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
br_cont
cont2
)
(** Priority:
Deadlock is catched HERE
*)
(** Priority:
Deadlock is catched HERE
*)
| TE_prio [] -> raise Deadlock
| 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
rec_genpath_ldbg ({br with br_ctrl_ldbg=(TE_prio tel)}) cont
)
)
(** Try similar to a recurse priority *)
(** 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
......@@ -1594,7 +1643,7 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
br_cont
cont2
)
(** Catch *)
(** Catch *)
| TE_catch (i,e,eco) -> (
let cont2 catch_cont =
rec_genpath_ldbg ({br with br_ctrl_ldbg=e ; br_cont_ldbg=catch_cont}) cont
......@@ -1759,9 +1808,9 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
) in
let new_pres = List.fold_left addp data.pres vars in
let new_data = {data with pres=new_pres} in
(* get the corresponding expanded code *)
(* get the corresponding expanded code *)
let (zecode : Expand.t) = Expand.get_run_expanded_code it.expanded_code rid in
(* build a slave LutExe *)
(* build a slave LutExe *)
let zeexe = of_expanded_code it.arg_opt zecode in
let inits = get_init_internal_state zeexe in
let (cont2: Reactive.prg_ldbg -> Event.t) =
......@@ -1776,7 +1825,7 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
}
in
cont2 (Reactive.DoStep_ldbg(to_reactive_prg_ldbg ctx rid zeexe inits))
(* builds the corresponding abstract reactive prg *)
(* builds the corresponding abstract reactive prg *)
)
| TE_dyn_erun (rid, react, vars, args, e) -> assert false
| TE_dyn_erun_ldbg (rid, react, vars, args, e) -> (
......@@ -1870,7 +1919,7 @@ let rec (genpath_ldbg : t -> store -> CoTraceExp.t -> Event.ctx -> (behavior ->
) in
let new_pres = List.fold_left addp data.pres vars in
let new_data = {data with pres=new_pres} in
(* get the corresponding expanded code *)
(* get the corresponding expanded code *)
let (zecode : Expand.t) = Expand.get_run_expanded_code it.expanded_code rid in
(* build a slave LutExe *)
let zeexe = of_expanded_code it.arg_opt zecode in
......@@ -2017,7 +2066,7 @@ and (to_reactive_prg_ldbg : Event.ctx -> string -> t -> internal_state -> Value.
let pres' = make_pre it ins outs locs in
let state' = (ctrl', pres') in
let outvals = List.map (fun x -> Value.OfIdent.get outs (Var.name x)) (out_var_list it) in
let edata = (* XXX quoi mettre ??? *)
let edata =
List.map
(fun x -> Var.name x,
Value.to_data_val (Value.OfIdent.get outs (Var.name x)))
......@@ -2025,17 +2074,17 @@ and (to_reactive_prg_ldbg : Event.ctx -> string -> t -> internal_state -> Value.
in
let edata = edata @
List.map
(fun x -> Var.name x,
Value.to_data_val (Value.OfIdent.get ins (Var.name x)))
(in_var_list it)
(fun x -> Var.name x,
Value.to_data_val (Value.OfIdent.get ins (Var.name x)))
(in_var_list it)
in
let edata = edata @
List.map
(fun x -> Var.name x,
Value.to_data_val (Value.OfIdent.get locs (Var.name x)))
(loc_var_list it)
(fun x -> Var.name x,
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;
}
in
......@@ -2066,9 +2115,9 @@ and (to_reactive_prg_ldbg : Event.ctx -> string -> t -> internal_state -> Value.
}
in
event
(* if LtopArg.args.LtopArg.ldbg then event else Event.next event *)
(* if LtopArg.args.LtopArg.ldbg then event else Event.next event *)
in
genpath_ldbg it data cstate ctx cont2
......@@ -2121,6 +2170,13 @@ type data_state = {
(* version step unique *)
let (step: t -> control_state -> data_state -> control_state * data_state) =
fun prog ctrl data ->
let _ =
(* clean tabulated results to avoid memory leaks.
Cleanning at every step may be overkill though...
*)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
in
let bg = get_behavior_gen prog data.ins data.mems ctrl in
match bg () with
| NoMoreBehavior -> failwith "NoMoreBehavior"
......@@ -2149,6 +2205,13 @@ let (step: t -> control_state -> data_state -> control_state * data_state) =
let (step_ldbg: Event.ctx -> string -> t -> control_state -> data_state ->
(control_state -> data_state -> Event.t) -> Event.t) =
fun ctx node prog ctrl data cont ->
let _ =
(* clean tabulated results to avoid memory leaks.
Cleanning at every step may be overkill though...
*)
Formula_to_bdd.clear_step ();
!Solver.clear_snt ();
in
let ctx = { ctx with Event.ctx_depth = 2 } in
let cont2 = fun bg ->
match bg with
......
......@@ -87,7 +87,7 @@ val make_pre : t -> Var.env_in -> Var.env_out -> Var.env_loc -> Var.env
(*
May raise Deadlock
*)
val step: t -> control_state -> data_state -> control_state * data_state
val step: t -> control_state -> data_state -> control_state * data_state
val step_ldbg: Event.ctx -> string -> t -> control_state -> data_state ->
(control_state -> data_state -> Event.t) -> Event.t
......
......@@ -43,7 +43,7 @@ type t = {
mutable _riffile : string option;
mutable _only_outputs: bool;
mutable _call_gnuplot: bool;
mutable _run:bool;
}
let (make_opt : unit -> t) =
......@@ -76,6 +76,7 @@ let (make_opt : unit -> t) =
_riffile = None;
_only_outputs = false;
_call_gnuplot = false;
_run=true;
}
......@@ -121,7 +122,7 @@ let step_mode opt = opt._step_mode
let set_step_mode opt sm = opt._step_mode <- sm