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

A first second towards a Morphine lutin/lustre debugger for lurette/lutin/lustre.

I can now trace Lutin step.
parent 2de4e3ac
......@@ -113,7 +113,7 @@ if test -z "$AWK_DOS" ; then
fi
if test -z "$GCC" ; then
GCC=gcc@EXE@ -mno-cygwin
GCC=gcc@EXE@ @NOCYGWIN@
export GCC
fi
if test -z "$GCC_DOS" ; then
......
type ctx = (* herited debug info *)
{
ctx_step :int;
ctx_data: Data.subst list;
ctx_terminate: unit -> unit;
}
type t = {
step : int;
kind : string; (* XXX Mettre un type somme bien propre à terme *)
data: Data.subst list;
next: unit -> t;
terminate: unit -> unit;
......
......@@ -19,6 +19,8 @@ let run = RunDirect.start
let next = Event.next
let data = Event.data
let terminate = Event.terminate
let off () = fun () -> LtopArg.args.LtopArg.ldbg <- false
let on () = fun () -> LtopArg.args.LtopArg.ldbg <- true
let rec (goto : Event.t -> int -> Event.t) =
fun e i ->
......
......@@ -174,6 +174,7 @@ type t = {
mutable socket_port : int option;
mutable socket_err_port : int option;
mutable debug_ltop : bool;
mutable ldbg : bool;
mutable cov_file : string;
mutable reset_cov_file : bool;
......@@ -249,6 +250,7 @@ let (args : t) = {
socket_port = None;
socket_err_port = None;
debug_ltop = false;
ldbg = false;
cov_file = "lurette.cov";
reset_cov_file = false;
......@@ -293,6 +295,8 @@ let (to_string : t -> (string * string * string) list) =
bool_opt args.stop_on_oracle_error "stop_on_oracle_error true" "--stop-on-oracle-error";
bool_opt args.debug_ltop "set_dbg_on" "--dbg";
bool_opt args.ldbg "set_ldbg_on" "--ldbg";
"set_verbose", "--verbose", soi args.verbose ;
"set_precision", "--precision" , soi args.precision;
......@@ -597,7 +601,8 @@ let rec speclist =
"<int>\t\tSeed the random engine is initialised with." ;
"-seed", Arg.Int (fun i -> args.seed <- Some i), " <int>\n";
"--dbg", Arg.Unit (fun () -> args.debug_ltop <- true), " debug mode\n";
"--dbg", Arg.Unit (fun () -> args.debug_ltop <- true), " debug mode (to debug lurettetop)\n";
"-ldbg", Arg.Unit (fun () -> args.ldbg <- true), " use the lurette debugger \n";
(* This option is not meant to be available to end-users... *)
(* "--make-opt", Arg.String (fun s -> args.make_opt <- s), *)
......
......@@ -217,7 +217,7 @@ let main_loop_start () =
output_string args.ocr (" This is Lurette Version "^(Version.str)^" ("^Version.sha^") \n");
flush args.ocr;
if not (args.go) then (main_loop 1; Unix.chdir args.sut_dir)
else
else if args.ldbg then () else
(if args.direct_mode || Build.f args then (
Unix.chdir args.sut_dir;
let res = Run.f () in
......
......@@ -64,11 +64,12 @@ let (check_compat : vars -> vars -> vars -> vars -> vars -> vars -> int * (vars
let (make_rp_list : reactive_program list ->
vars list * vars list * (string -> unit) list *
(Data.subst list -> Data.subst list) list *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) list *
Data.subst list list * Data.subst list list) =
fun rpl ->
let add_init init (a,b,c,d) = (a,b,c,d,init,init) in
let add_init init (a,b,c,d,e) = (a,b,c,d,e,init,init) in
let aux rp =
let ins, outs, kill, step, initin, initout =
let ins, outs, kill, step, step_dbg, initin, initout =
match rp with
| LustreV6(prog,node) -> add_init [] (LustreRun.make_v6 prog node)
| LustreV4(prog,node) -> add_init [] (LustreRun.make_v4 prog node)
......@@ -93,9 +94,9 @@ let (make_rp_list : reactive_program list ->
else
step
in
ins, outs, kill, step, initin, initout
ins, outs, kill, step, step_dbg, initin, initout
in
Util.list_split6 (List.map aux rpl)
Util.list_split7 (List.map aux rpl)
type cov_opt =
......@@ -107,22 +108,13 @@ exception SutStop of cov_opt
let gnuplot_time = ref 0.0
type ctx = (* herited debug info *)
{
ctx_step :int;
ctx_data: Data.subst list;
ctx_terminate: unit -> unit;
}
let (start : unit -> Event.t) =
fun () ->
gnuplot_time := 0.0;
(* Get sut info (var names, step func, etc.) *)
let _ = if args.debug_ltop then LustreRun.debug := args.debug_ltop in
let sut_in_l, sut_out_l, sut_kill_l, sut_step_sl_l, sut_init_in_l, sut_init_out_l =
make_rp_list args.suts
let sut_in_l, sut_out_l, sut_kill_l, sut_step_sl_l, sut_step_dbg_sl_l,
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
......@@ -130,17 +122,32 @@ let (start : unit -> Event.t) =
let sut_init_out = List.flatten sut_init_out_l in
(* Get oracle info (var names, step func, etc.)*)
let oracle_in_l, oracle_out_l, oracle_kill_l, oracle_step_sl_l, _, _ =
let oracle_in_l, oracle_out_l, oracle_kill_l, oracle_step_sl_l, oracle_step_dbg_sl_l, _, _ =
make_rp_list args.oracles
in
let oracle_kill msg = List.iter (fun f -> f msg) oracle_kill_l in
(* Get env info (var names, step func, etc.)*)
let env_in_l, env_out_l, env_kill_l, env_step_sl_l, env_init_in_l, env_init_out_l =
make_rp_list args.envs
let env_in_l, env_out_l, env_kill_l, env_step_sl_l, env_step_dbg_sl_l,
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_sl sl = List.flatten (List.map (fun f -> f sl) env_step_sl_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
......@@ -274,20 +281,36 @@ let (start : unit -> Event.t) =
if i > args.step_nb then (killem_all cov; raise (Event.End 0) )
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
let env_out_vals = env_step_sl env_in_vals in
(* { *)
(* step = i; *)
(* data = []; *)
(* next = (fun () -> *)
loop2 cov env_in_vals pre_env_out_vals i luciole_outs env_out_vals
(* ); *)
(* terminate = (fun () -> killem_all cov) *)
(* } *)
if args.ldbg then (* XXX l'idéal serait de faire ce test à
l'interieur de la boucle en passant la
fonction qui va bien selon le
mode. Apres tout, c'est l'un des
avantages du CPS... *)
let edata = env_in_vals@pre_env_out_vals in
let ctx =
{
Event.ctx_step = i;
Event.ctx_data = edata;
Event.ctx_terminate = (fun () -> killem_all cov)
}
in
let cont = loop2 cov env_in_vals pre_env_out_vals i luciole_outs in
env_step_dbg_sl 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_out_vals = env_step_sl env_in_vals in
loop2 cov env_in_vals pre_env_out_vals i luciole_outs env_out_vals
(*
{
step = i;
data = [];
next = (fun () -> loop2 cov env_in_vals pre_env_out_vals i luciole_outs env_out_vals );
terminate = (fun () -> killem_all cov)
}
*)
and
loop2 cov env_in_vals pre_env_out_vals i luciole_outs env_out_vals =
let env_out_vals = luciole_outs @ env_out_vals in
......@@ -339,6 +362,7 @@ let (start : unit -> Event.t) =
{
Event.step = i;
Event.data = edata;
Event.kind = "ltop_step";
Event.next =
(fun () ->
loop (check_oracles oracle_in_vals i oracle_out_l oracle_out_vals_l cov)
......
......@@ -41,7 +41,8 @@ let (step_channel : in_channel -> out_channel -> vars -> vars ->
(* XXX Doable with DynLink? Or via Ezdl? *)
let (make_ec : string -> vars * vars * (string -> unit) *
(Data.subst list -> Data.subst list)) =
(Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) ) =
fun ec_file ->
let ec_in, ec_out = Util.get_io_from_lustre ec_file None in
......@@ -86,7 +87,16 @@ let (make_ec : string -> vars * vars * (string -> unit) *
with e -> (Printf.printf "Killing of ecexe process failed: %s\n" (Printexc.to_string e) ))
in
let step = step_channel ec_ic ec_oc ec_in ec_out in
ec_in, ec_out, kill, step
let step_dbg sl ctx cont =
{
Event.step = ctx.Event.ctx_step;
Event.data = ctx.Event.ctx_data;
Event.kind = "lustre_step";
Event.next = (fun () -> cont (step sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
}
in
ec_in, ec_out, kill, step, step_dbg
(* Via une edition de liens dynamique *)
......@@ -106,7 +116,8 @@ let (make_ec_dynlink: string -> string -> string -> vars * vars * (string -> uni
(**********************************************************************************)
let (make_v6 : string -> string -> vars * vars * (string -> unit) *
(Data.subst list -> Data.subst list)) =
(Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) ) =
fun lus_file node ->
let dir = Filename.dirname lus_file in
if Util2.lv62ec lus_file node dir then
......@@ -116,7 +127,8 @@ let (make_v6 : string -> string -> vars * vars * (string -> unit) *
(**********************************************************************************)
let (make_v4 : string -> string -> vars * vars * (string -> unit) *
(Data.subst list -> Data.subst list)) =
(Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) ) =
fun lus_file node ->
let dir = Filename.dirname lus_file in
if Util2.lv42ec lus_file node dir then
......@@ -144,7 +156,8 @@ let rec connect_loop sock addr k =
let (make_socket_do : string -> int -> in_channel *
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list)) =
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) ) =
fun sock_adr port ->
let _ =
if !debug then (
......@@ -185,32 +198,46 @@ let (make_socket_do : string -> int -> in_channel *
Rif_base.read_interface label sock_in (if !debug then Some stderr else None)
in
let step = step_channel sock_in sock_out vars_in vars_out in
let step_dbg sl ctx cont =
{
Event.step = ctx.Event.ctx_step;
Event.data = ctx.Event.ctx_data;
Event.kind = "socket_step";
Event.next = (fun () -> cont (step sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
}
in
if !debug then (
Printf.fprintf stderr "\nInterface declarations on %s:%i, ok.\n" sock_adr port;
flush stderr);
sock_in, vars_in, vars_out, kill, step
flush stderr
);
sock_in, vars_in, vars_out, kill, step, step_dbg
(* exported *)
let (make_socket : string -> int ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list)) =
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)) =
fun sock_adr port ->
let _, vars_in, vars_out, kill, step = make_socket_do sock_adr port in
vars_in, vars_out, kill, step
let _, vars_in, vars_out, kill, step,step_dbg = make_socket_do sock_adr port in
vars_in, vars_out, kill, step, step_dbg
(* exported *)
let (make_socket_init : string -> int ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list)
* Data.subst list * Data.subst list) =
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) *
Data.subst list * Data.subst list) =
fun sock_adr port ->
let sock_in, vars_in, vars_out, kill, step = make_socket_do sock_adr port in
let sock_in, vars_in, vars_out, kill, step, step_dbg = make_socket_do sock_adr port in
let out_init = Rif_base.read sock_in None vars_out in
let in_init = Rif_base.read sock_in None vars_in in
vars_in, vars_out, kill, step, in_init, out_init
vars_in, vars_out, kill, step, step_dbg, in_init, out_init
(**********************************************************************************)
let (make_ec_exe : string -> vars * vars * (string -> unit) *
(Data.subst list -> Data.subst list)) =
(Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
) =
fun ec_file ->
let exe = (Filename.chop_extension ec_file) ^ (Util.exe()) in
let _ = if not (Sys.file_exists exe) then (
......@@ -263,7 +290,16 @@ let (make_ec_exe : string -> vars * vars * (string -> unit) *
with e -> (Printf.printf "Killing of %s process failed: %s\n" exe (Printexc.to_string e) ))
in
let step = step_channel ec_ic ec_oc ec_in ec_out in
ec_in, ec_out, kill, step
let step_dbg sl ctx cont =
{
Event.step = ctx.Event.ctx_step;
Event.data = ctx.Event.ctx_data;
Event.kind = "ec_step";
Event.next = (fun () -> cont (step sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
}
in
ec_in, ec_out, kill, step, step_dbg
(**********************************************************************************)
......@@ -401,7 +437,7 @@ let (make_luciole : string -> vars -> vars ->
let (make_dro : string -> vars * vars *
(string -> unit) * (Data.subst list -> Data.subst list)) =
fun dro ->
assert false
assert false
(* finish me *)
(**********************************************************************************)
......@@ -414,8 +450,9 @@ let (make_dro : string -> vars * vars *
let (make_ocaml : string -> vars * vars *
(string -> unit) * (Data.subst list -> Data.subst list)
* Data.subst list * Data.subst list) =
(string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) *
Data.subst list * Data.subst list) =
fun cmxs ->
let _ =
try Dynlink.loadfile cmxs
......@@ -426,11 +463,21 @@ let (make_ocaml : string -> vars * vars *
exit 2
in
let imems, omems = OcamlRM.get_mems cmxs in
let step_dbg sl ctx cont =
{
Event.step = ctx.Event.ctx_step;
Event.data = ctx.Event.ctx_data;
Event.kind = "ocaml_step";
Event.next = (fun () -> cont (OcamlRM.get_step cmxs sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
}
in
let res = (
OcamlRM.get_inputs cmxs,
OcamlRM.get_outputs cmxs,
OcamlRM.get_kill cmxs,
OcamlRM.get_step cmxs,
step_dbg,
imems,
omems
)
......
......@@ -23,23 +23,27 @@ type vars = (string * string) list
Raises Failure of string if something bas happens.
*)
val make_ec : string ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list)
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
(* [make_ec_exe ec_file.ec] supposes that ec_file.ec has already been compiled
into an executable that is named ec_file.
*)
val make_ec_exe : string ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list)
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
(** [make_v6 file node] handles Verimag/Lustre v6 programs
Raises Failure of string if something bas happens.
*)
val make_v6 : string -> string ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list)
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
val make_v4 : string -> string -> vars * vars * (string -> unit) *
(Data.subst list -> Data.subst list)
(Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
(** [make_socket sock_addr port]
......@@ -52,10 +56,12 @@ val make_v4 : string -> string -> vars * vars * (string -> unit) *
to stop if it receives "#quit".
*)
val make_socket : string -> int ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list)
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
val make_socket_init : string -> int ->
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list)
vars * vars * (string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
* Data.subst list * Data.subst list
(** [make_luciole dro_file inputs outputs]
......@@ -67,7 +73,8 @@ val make_luciole : string -> vars -> vars ->
(string -> unit) * (Data.subst list -> Data.subst list)
val make_ocaml : string -> vars * vars *
(string -> unit) * (Data.subst list -> Data.subst list)
(string -> unit) * (Data.subst list -> Data.subst list) *
(Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
* Data.subst list * Data.subst list
(**/**)
......
......@@ -8,11 +8,15 @@ let (to_subst_list : (string * string) list -> Value.OfIdent.t -> Data.subst lis
fun var_decl vals ->
List.map (fun (n,_) -> n, Value.to_data_val (Value.OfIdent.get vals n)) var_decl
let (to_vals : Data.subst list -> Value.OfIdent.t) =
List.fold_left
(fun acc (n,v) -> Value.OfIdent.add acc (n, Value.from_data_val v))
(* ditto, but without taking care of variable order *)
let (from_vals : Value.OfIdent.t -> Data.subst list) = fun vals ->
Value.OfIdent.fold (fun id v acc -> (id,Value.to_data_val v)::acc) vals []
let (to_vals : Data.subst list -> Value.OfIdent.t) =
List.fold_left
(fun acc (n,v) -> Value.OfIdent.add acc (n, Value.from_data_val v))
Value.OfIdent.empty
let make_lut argv =
let opt = MainArg.parse argv in
......@@ -43,6 +47,22 @@ let make_lut argv =
data_state := new_ds;
to_subst_list lut_out new_ds.LutExe.outs
in
let (lut_step_dbg:
Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t) =
fun sl ctx cont ->
{
Event.step = ctx.Event.ctx_step;
Event.kind = "lutin_step prog='" ^ (String.concat "," prog) ^
"' node ='" ^ node ^ "' \n dump expr =" ^
(LutExe.string_of_control_state !ctrl_state) ^ " \n stack : "
(* ^ *)
(* (CoIdent.string_of_src_stack ()) *)
;
Event.data = ctx.Event.ctx_data;
Event.next = (fun () -> cont (lut_step sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
}
in
let mems_in =
List.fold_left
(fun acc (vn,_vt) ->
......@@ -65,4 +85,4 @@ let make_lut argv =
[]
lut_out
in
lut_in, lut_out, (fun _ -> ()), lut_step, mems_in, mems_out
lut_in, lut_out, (fun _ -> ()), lut_step, lut_step_dbg, mems_in, mems_out
......@@ -9,5 +9,5 @@ type vars = (string * string) list
val make_lut: string array ->
vars * vars * (string -> unit)
* (Data.subst list -> Data.subst list)
(* * (Data.subst list -> Event.ctx -> (Data.subst list -> Event.t) -> Event.t *)
* (Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
* Data.subst list * Data.subst list
......@@ -310,6 +310,14 @@ let rec (list_split6: ('a * 'b * 'c * 'd * 'e * 'f) list ->
| (x,y,z,t,u,v)::l ->
let (rx, ry, rz, rt, ru, rv) = list_split6 l in (x::rx, y::ry, z::rz, t::rt, u::ru,v::rv)
let rec (list_split7: ('a * 'b * 'c * 'd * 'e * 'f * 'g) list ->
'a list * 'b list * 'c list * 'd list * 'e list * 'f list * 'g list) =
function
| [] -> ([], [], [], [], [], [], [])
| (x,y,z,t,u,v,w)::l ->
let (rx, ry, rz, rt, ru, rv, rw) =
list_split7 l in (x::rx, y::ry, z::rz, t::rt, u::ru, v::rv, w::rw)
(** checks that a list does not contain any duplicate *)
......
......@@ -104,7 +104,7 @@ let rif_all = rif_in @ rif_out
(**************************************************************************)
(* Oracle launching *)
let oracle_in, oracle_out, kill_oracle, step_oracle =
let oracle_in, oracle_out, kill_oracle, step_oracle, step_oracle_dbg =
LustreRun.make_ec arg.ec
(**************************************************************************)
......
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