Skip to content

GitLab

L
lutin
Commit 43c4caa9 authored by erwan's avatar erwan
Browse files
Options

New: RdbgPlugin.t and Event.t now have now some save_state/restore_state functions. 

Rationale: a step to make time traveling work correctly.
parent dd9c4a6a
Hide whitespace changes
Inline Side-by-side
Showing with 107 additions and 61 deletions
examples/crazy-rabbit/rabbit.ml
View file @ 43c4caa9
......@@ -37,7 +37,8 @@ let _ =
let init _ = ()
let kill _ = ()
let reset _ = ()
let ss _i = ()
let rs _i = ()
type var_type = string
let (inputs :(string * Data.t) list) = [
......@@ -159,6 +160,8 @@ let plugin = {
inputs = inputs;
outputs= outputs;
reset= reset;
save_state = ss;
restore_state = rs;
kill= kill;
init_inputs=mems_i;
init_outputs=mems_o;
......
ltop/src/lustreRun.ml
View file @ 43c4caa9
(* Time-stamp: <modified the 04/04/2019 (at 16:45) by Erwan Jahier> *)
(* Time-stamp: <modified the 05/04/2019 (at 13:45) by Erwan Jahier> *)
open RdbgPlugin
type vars = (string * Data.t) list
......@@ -41,6 +41,9 @@ let (step_channel : in_channel -> out_channel -> vars -> vars ->
in
res
let nohope str _i =
Printf.eprintf "save/restore state impossible from %s \n" str;
flush stderr
(* wrap it with type transformation *)
let get_io_from_lustre a b =
let il, ol = Util.get_io_from_lustre a b in
......@@ -99,7 +102,7 @@ let (make_ec : string -> RdbgPlugin.t) =
let step_dbg sl ctx cont =
let enb = ctx.Event.nb in
let ctx = Event.incr_event_nb ctx in
{
{ ctx with
Event.nb = enb;
Event.step = ctx.Event.step;
Event.depth = ctx.Event.depth;
......@@ -122,6 +125,8 @@ let (make_ec : string -> RdbgPlugin.t) =
outputs= ec_out;
reset= (fun () -> RifIO.write ec_oc "#reset\n"; flush ec_oc);
kill= kill;
save_state = nohope "ec";
restore_state = nohope "ec";
init_inputs= [];
init_outputs= [];
step = step;
......@@ -222,7 +227,7 @@ let (make_socket_do : string -> int -> in_channel * RdbgPlugin.t) =
let step_dbg sl ctx cont =
let enb = ctx.Event.nb in
let ctx = Event.incr_event_nb ctx in
{
{ ctx with
Event.step = ctx.Event.step;
Event.data = ctx.Event.data;
Event.depth = ctx.Event.depth;
......@@ -247,6 +252,8 @@ let (make_socket_do : string -> int -> in_channel * RdbgPlugin.t) =
kill= kill;
init_inputs= [];
init_outputs= [];
save_state = nohope "socket";
restore_state = nohope "socket";
step = step;
step_dbg = step_dbg
}
......@@ -330,7 +337,7 @@ let (make_ec_exe : string -> RdbgPlugin.t) =
let step_dbg sl ctx cont =
let enb = ctx.Event.nb in
let ctx = Event.incr_event_nb ctx in
{
{ ctx with
Event.step = ctx.Event.step;
Event.data = ctx.Event.data;
Event.nb = enb;
......@@ -353,6 +360,8 @@ let (make_ec_exe : string -> RdbgPlugin.t) =
outputs= ec_out;
reset= (fun () -> RifIO.write ec_oc "#reset\n"; flush ec_oc);
kill= kill;
save_state = nohope "stdin/stdout";
restore_state = nohope "stdin/stdout";
init_inputs= [];
init_outputs= [];
step = step;
......
ltop/src/runDirect.ml
View file @ 43c4caa9
......@@ -72,17 +72,19 @@ let (check_compat : vars -> vars -> vars -> vars -> vars -> vars ->
type ctx = Event.t
type e = Event.t
let rec (list_split8: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h) list ->
'a list * 'b list * 'c list * 'd list * 'e list * 'f list * 'g list * 'h list) =
let rec (list_split: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i* 'j) list ->
'a list * 'b list * 'c list * 'd list * 'e list * 'f list
* 'g list * 'h list * 'i list* 'j list) =
function
| [] -> ([], [], [], [], [], [], [], [])
| (x,y,z,t,u,v,w,a)::l ->
let (rx, ry, rz, rt, ru, rv, rw, ra) = list_split8 l in
(x::rx, y::ry, z::rz, t::rt, u::ru, v::rv, w::rw, a::ra)
| [] -> ([], [], [], [], [], [], [], [], [], [])
| (x,y,z,t,u,v,w,a,b,c)::l ->
let (rx, ry, rz, rt, ru, rv, rw, ra, rb, rc) = list_split l in
(x::rx, y::ry, z::rz, t::rt, u::ru, v::rv, w::rw, a::ra, b::rb, c::rc)
open RdbgPlugin
let (make_rp_list : reactive_program list ->
vars list * vars list * (unit -> unit) list * (string -> unit) list *
(int -> unit) list * (int -> unit) list *
(Data.subst list -> Data.subst list) list *
(Data.subst list -> ctx -> (Data.subst list -> ctx -> Event.t) ->
Event.t) list * Data.subst list list * Data.subst list list) =
......@@ -101,8 +103,10 @@ let (make_rp_list : reactive_program list ->
| Ocaml(cmxs) -> OcamlRun.make_ocaml cmxs
| Lutin(args) -> LutinRun.make args
in
let ins, outs, reset, kill, step, step_dbg, initin, initout =
plugin.inputs,plugin.outputs,plugin.reset,plugin.kill,plugin.step,plugin.step_dbg,
let ins, outs, reset, kill, save_state, restore_state, step, step_dbg,
initin, initout =
plugin.inputs,plugin.outputs,plugin.reset,plugin.kill,plugin.save_state,
plugin.restore_state,plugin.step,plugin.step_dbg,
plugin.init_inputs,plugin.init_outputs
in
let step = if args.debug_ltop then
......@@ -119,9 +123,10 @@ let (make_rp_list : reactive_program list ->
else
step
in
ins, outs, reset, kill, step, step_dbg, initin, initout
ins, outs, reset, kill, save_state, restore_state, step, step_dbg,
initin, initout
in
list_split8 (List.map aux rpl)
list_split (List.map aux rpl)
type cov_opt =
......@@ -158,35 +163,50 @@ let (start : unit -> Event.t) =
fun () ->
(* 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_reset_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
let sut_in_l, sut_out_l, sut_reset_l,sut_kill_l, sut_ss_l,
sut_rs_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_reset () = List.iter (fun f-> f ()) sut_reset_l in
let sut_save_state i = List.iter (fun f-> f i) sut_ss_l in
let sut_restore_state i = List.iter (fun f-> f i) sut_rs_l in
let sut_kill msg = List.iter (fun f -> f msg) sut_kill_l in
let sut_init_in = List.flatten sut_init_in_l in
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_reset_l, oracle_kill_l, oracle_step_sl_l,
let oracle_in_l, oracle_out_l, oracle_reset_l, oracle_kill_l, oracle_ss_l,
oracle_rs_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
let oracle_reset () = List.iter (fun f-> f ()) oracle_reset_l in
let oracle_save_state i = List.iter (fun f-> f i) oracle_ss_l in
let oracle_restore_state i = List.iter (fun f-> f i) oracle_rs_l in
(* Get env info (var names, step func, etc.)*)
let env_in_l, env_out_l, env_reset_l,env_kill_l, env_step_sl_l, env_step_dbg_sl_l,
let env_in_l, env_out_l, env_reset_l,env_kill_l, env_save_state_l,
env_restore_state_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_reset () = List.iter (fun f-> f ()) env_reset_l in
let env_kill msg = List.iter (fun f -> f msg) env_kill_l in
let _env_init_in = Util.rm_dup (List.flatten env_init_in_l) in
let _env_init_out = Util.rm_dup (List.flatten env_init_out_l) in
let env_save_state i = List.iter (fun f-> f i) sut_ss_l in
let env_restore_state i = List.iter (fun f-> f i) sut_rs_l in
let reset () =
if args.verbose > 0 then (
Printf.eprintf "rdbgRun.start: resetting all RPs\n"; flush stderr);
sut_reset (); env_reset (); oracle_reset ()
in
let save_state i =
sut_save_state i; env_save_state i; oracle_save_state i
in
let restore_state i =
sut_restore_state i; env_restore_state i; oracle_restore_state i
in
let vars_to_string l =
String.concat "\n" (List.map (fun (vn,vt) ->
......@@ -464,7 +484,7 @@ let (start : unit -> Event.t) =
Event.terminate = term;
}
in
{
{ ctx with
Event.nb = enb;
Event.step = i;
Event.kind = Event.Ltop;
......@@ -521,6 +541,8 @@ let (start : unit -> Event.t) =
Event.data = [];
Event.terminate = (fun () -> killem_all cov_init);
Event.reset = (fun () -> reset ());
Event.save_state = (fun i -> save_state i);
Event.restore_state = (fun i -> restore_state i);
Event.lang = "";
Event.next = (fun () -> assert false);
Event.kind = Event.Ltop;
......
lutin/src/formula_to_bdd.ml
View file @ 43c4caa9
......@@ -241,8 +241,8 @@ let (clear_all : unit -> unit) =
fun _ ->
Hashtbl.clear bdd_tbl ;
Hashtbl.clear bdd_tbl_global ;
clear_global_linear_constraint_index ()
clear_global_linear_constraint_index ();
bdd_manager := init_manager ()
(****************************************************************************)
(****************************************************************************)
......
lutin/src/lutExe.ml
View file @ 43c4caa9
......@@ -772,6 +772,7 @@ let string_of_branch_ldbg b = (
" data.pres: "^(Value.OfIdent.to_short_string b.br_data_ldbg.pres)
)
(* misc. utils *)
let put_in_seq te1 te2 = (
if(te1 = TE_eps) then te2
......@@ -1539,7 +1540,7 @@ let rec (genpath_ldbg :
if (is_sat) then
let enb = ctx.Event.nb in
let ctx = event_incr ctx it.arg_opt in
{
{ ctx with
Event.kind = Event.MicroStep "sat ";
Event.nb = enb;
Event.lang = "lutin";
......@@ -1579,7 +1580,7 @@ let rec (genpath_ldbg :
let enb = ctx.Event.nb in
let ctx = event_incr ctx it.arg_opt in
let usat_event =
{
{ ctx with
Event.nb = enb;
Event.kind = Event.MicroStep "usat";
Event.lang = "lutin";
......@@ -1606,7 +1607,7 @@ let rec (genpath_ldbg :
in
let enb = ctx.Event.nb in
let ctx = event_incr ctx it.arg_opt in
{
{ ctx with
Event.nb = enb;
Event.kind = Event.MicroStep "try ";
Event.lang = "lutin";
......@@ -2094,7 +2095,7 @@ let rec (genpath_ldbg :
let enb,d = ctx.Event.nb, ctx.Event.depth in
let ctx = event_incr ctx it.arg_opt in
let event =
{
{ ctx with
Event.step = ctx.Event.step;
Event.nb = enb;
Event.depth = ctx.Event.depth;
......@@ -2343,9 +2344,9 @@ and (to_reactive_prg_ldbg :
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 si_atoms = List.map to_src_info zeguard.g_src in
let cstr = Exp.to_expr zeguard.g_form in
......@@ -2358,7 +2359,7 @@ and (to_reactive_prg_ldbg :
in
let ctx2 = event_incr ctx2 it.arg_opt in
let event =
{
{ ctx with
Event.step = ctx.Event.step;
Event.nb = ctx2.Event.nb-1;
Event.depth = ctx.Event.depth;
......@@ -2391,7 +2392,7 @@ and (to_reactive_prg_ldbg :
let enb = ctx.Event.nb in
let ctx = event_incr ctx it.arg_opt in
let ctx = Event.incr_event_depth ctx in (* inner events are one step deapper *)
{
{ ctx with
Event.step = ctx.Event.step;
Event.nb = enb ;
Event.depth = d;
......@@ -2573,7 +2574,7 @@ let (step_ldbg: ctx -> string -> t -> control_state -> data_state ->
in
let si_atoms = List.map to_src_info zeguard.g_src in
let cstr = Exp.to_expr zeguard.g_form in
{
{ ctx with
Event.step = ctx.Event.step;
Event.nb = ctx2.Event.nb-1;
Event.depth = ctx.Event.depth;
......
lutin/src/lutinRun.ml
View file @ 43c4caa9
(* Time-stamp: <modified the 29/03/2019 (at 08:36) by Erwan Jahier> *)
(* Time-stamp: <modified the 10/04/2019 (at 10:10) by Erwan Jahier> *)
(**********************************************************************************)
type vars = (string * Data.t) list
......@@ -23,6 +23,7 @@ open RdbgPlugin
type ctx = Event.t
type e = Event.t
let make argv =
let opt = MainArg.parse argv in
let prog = MainArg.infile opt
......@@ -33,18 +34,20 @@ let make argv =
let lut_in = List.map var_to_var_pair (LutExe.in_var_list lut_mach) in
let lut_out = List.map var_to_var_pair (LutExe.out_var_list lut_mach) in
let lut_memories =
(* if LtopArg.args.LtopArg.delay_env_outputs then *)
(* LutExe.get_init_pres lut_mach *)
(* else *)
(* if LtopArg.args.LtopArg.delay_env_outputs then *)
(* LutExe.get_init_pres lut_mach *)
(* else *)
Value.OfIdent.empty
in
let ctrl_state = ref (LutExe.get_init_state lut_mach) in
let data_state = ref
{ LutExe.ins = Value.OfIdent.empty;
LutExe.outs = lut_memories;
LutExe.mems = LutExe.get_init_pres lut_mach
}
{ LutExe.ins = Value.OfIdent.empty;
LutExe.outs = lut_memories;
LutExe.mems = LutExe.get_init_pres lut_mach
}
in
let ss_table = Hashtbl.create 10 in
let lut_step sl =
let _ = data_state := { !data_state with LutExe.ins = to_vals sl } in
let new_cs, new_ds = LutExe.step lut_mach !ctrl_state !data_state in
......@@ -63,27 +66,15 @@ let make argv =
cont (to_subst_list lut_out new_ds.LutExe.outs) ctx
in
data_state := { !data_state with LutExe.ins = to_vals sl };
(* { (* XXX l'enlever quand j'aurais trouvé le bon endroit dans lutExe ?? *) *)
(* 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 () -> *)
LutExe.step_ldbg ctx node lut_mach !ctrl_state !data_state cont_lut_step
(* Event.terminate = ctx.Event.ctx_terminate; *)
(* } *)
in
let mems_in =
List.fold_left
(fun acc (vn,_vt) ->
try
let v = Value.OfIdent.get lut_memories vn in
(vn, Value.to_data_val v)::acc
with Not_found -> acc
try
let v = Value.OfIdent.get lut_memories vn in
(vn, Value.to_data_val v)::acc
with Not_found -> acc
)
[]
lut_in
......@@ -91,10 +82,10 @@ let make argv =
let mems_out =
List.fold_left
(fun acc (vn,_vt) ->
try
let v = Value.OfIdent.get lut_memories vn in
(vn, Value.to_data_val v)::acc
with Not_found -> acc
try
let v = Value.OfIdent.get lut_memories vn in
(vn, Value.to_data_val v)::acc
with Not_found -> acc
)
[]
lut_out
......@@ -119,6 +110,26 @@ let make argv =
}
));
kill=(fun _ -> ());
save_state = (fun i ->
let prgs = Random.get_state () in
if Verbose.level() > 0 then (
Printf.eprintf "Save state %i from Lutin (%i)\n" i
(Random.State.bits (Random.State.copy prgs));
flush stderr);
Hashtbl.replace ss_table i (!ctrl_state, !data_state, prgs)
);
restore_state = (fun i ->
match Hashtbl.find_opt ss_table i with
| Some (cs, ds, prgs) ->
if Verbose.level() > 0 then (
Printf.eprintf "Restore state %i from Lutin (%i)\n" i
(Random.State.bits (Random.State.copy prgs));
flush stderr
);
ctrl_state := cs; data_state := ds;
Random.set_state prgs;
| None -> Printf.eprintf "Cannot restore state %i from Lutin\n" i; flush stderr
);
init_inputs=mems_in;
init_outputs=mems_out;
step=lut_step;
......@@ -126,5 +137,5 @@ let make argv =
}
Markdown is supported
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