Commit 3721d420 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Apply the change of data structure done in Data and Event Modules of rdbg

(cf 55d3d77c470f416befd16a1b7d47f751eb2171fc)

remove ldbg tests (ldbg is dead, vive rdbg!)
parent a122bf02
......@@ -44,7 +44,6 @@ test-lutin:
cd lutin/lustre && make test ;
cd lutin/C && make test;
cd lutin/crazy-rabbit && make test;
cd lutin/ldbg && make test;
echo "All lutin tests ran correctly."
# problem ~
......
......@@ -40,18 +40,18 @@ let kill _ = ()
type var_type = string
let (inputs :(string * string) list) = [
"x", "real";
"y", "real";
"p1x", "real";
"p1y", "real";
"p2x", "real";
"p2y", "real";
"p3x", "real";
"p3y", "real";
"p4x", "real";
"p4y", "real";
"freeze", "bool"
let (inputs :(string * Data.t) list) = [
"x", Data.Real;
"y", Data.Real;
"p1x", Data.Real;
"p1y", Data.Real;
"p2x", Data.Real;
"p2y", Data.Real;
"p3x", Data.Real;
"p3y", Data.Real;
"p4x", Data.Real;
"p4y", Data.Real;
"freeze", Data.Bool
]
let mems_i = []
......@@ -61,10 +61,10 @@ let mems_o = [
"y_min", Data.F 0.0; "y_max", Data.F 100.0
]
let (outputs :(string * string) list) =
let (outputs :(string * Data.t) list) =
[
"x_min", "real"; "x_max", "real";
"y_min", "real"; "y_max", "real"
"x_min", Data.Real; "x_max", Data.Real;
"y_min", Data.Real; "y_max", Data.Real
]
let cross_product(ux,uy,vx,vy) = (ux*.vy-.uy*.vx);;
......
......@@ -128,7 +128,7 @@ utest5:test5.rif
utest: utest1 utest2 utest4 utest5
test: test1 test2 test4 test5
test: test1 test2 test4
%.ec: %.lus
../../../bin/lus2lic$(EXE) -ec $^ -n $* -o $@
......
......@@ -26,9 +26,8 @@ let set_sim2chro b = LtopArg.args.LtopArg.display_sim2chro <- b
let run () =
Event.event_nb :=0;
RunDirect.start ()
let next = Event.next
let data = Event.data
let terminate = Event.terminate
let next e = e.next()
let terminate e = e.terminate
let off () = LtopArg.args.LtopArg.ldbg <- false
let on () = LtopArg.args.LtopArg.ldbg <- true
......
......@@ -2,7 +2,7 @@ open Ldbg
open Event
(*
(******************************************************************)
(* print_event stuff *)
let show_trace = ref true
......@@ -398,3 +398,4 @@ let (explain_failure : Event.t -> unit) =
| _ -> print_string "Current Event is not a fail\n"
*)
(*
(** Compute the next event, call the hooks functions on it, and return that event *)
val next : Event.t -> Event.t
......@@ -111,3 +111,4 @@ val goto : Event.t -> int -> Event.t
(** Try to hint why the current constraint failed (at fail events only) *)
val explain_failure : Event.t -> unit
*)
(* Time-stamp: <modified the 21/11/2013 (at 11:19) by Erwan Jahier> *)
(* Time-stamp: <modified the 20/02/2014 (at 10:25) by Erwan Jahier> *)
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
*)
type vars = (string * string) list
type vars = (string * Data.t) list
open Lv6MainArgs
open Soc
......@@ -11,8 +11,7 @@ open SocExecValue
let make argv =
let opt = Lv6MainArgs.parse argv in
let node = opt.main_node in
if (opt.infiles = []) then (
Lv6MainArgs.usage stderr opt;
exit 1
......@@ -29,8 +28,7 @@ let make argv =
let nsl = Compile.get_source_list opt opt.infiles in
let lic_prg = Compile.doit opt nsl main_node in
let first_file = List.hd opt.infiles in
let nk = (Lic.node_key_of_idref (Ident.to_idref opt.main_node)) in
let nk = (Lic.node_key_of_idref (Ident.to_idref opt.main_node)) in
let sk, soc_tbl =
if LicPrg.node_exists lic_prg nk then (
Lic2soc.f lic_prg nk
......@@ -42,12 +40,10 @@ let make argv =
)
in
let soc = try Soc.SocMap.find sk soc_tbl with Not_found -> assert false in
let vntl_of_profile = List.map (fun (x,t) -> x,SocUtils.string_of_type_ref t) in
let soc_inputs = (SocExec.expand_profile true (fst soc.profile)) in
let soc_outputs = (SocExec.expand_profile true (snd soc.profile)) in
let (vntl_i:Data.vntl) = vntl_of_profile soc_inputs in
let (vntl_o:Data.vntl) = vntl_of_profile soc_outputs in
let oc = stdout in
let (vntl_i:Data.vntl) = soc_inputs in
let (vntl_o:Data.vntl) = soc_outputs in
(* Lv6util.dump_entete oc; *)
(* RifIO.write_interface oc vntl_i vntl_o None None; *)
(* RifIO.flush oc; *)
......
type vars = (string * string) list
type vars = (string * Data.t) list
val make: string array ->
vars * vars * (string -> unit)
......
open LtopArg
open Event
let (f : unit -> int) =
fun () ->
try
if args.direct_mode then
try
let rec loop_cont e =
loop_cont (Event.next e)
loop_cont (e.next())
in
loop_cont (RunDirect.start ())
with Event.End i -> i
......
......@@ -2,7 +2,7 @@
open LutExe
open LtopArg
type vars = (string * string) list
type vars = (string * Data.t) list
(* returns a \ b *)
......@@ -33,7 +33,9 @@ let (check_compat : vars -> vars -> vars -> vars -> vars -> vars -> int * (vars
let luciole_in = list_minus (env_out@sut_out) luciole_out in
(* let luciole_in = [] in *)
let vars_to_string vars = String.concat "," (List.map (fun (n,t) -> n^":"^t) vars) in
let vars_to_string vars =
String.concat "," (List.map (fun (n,t) -> n^":"^(Data.type_to_string t)) vars)
in
if missing_sut_in <> [] then (
let missing_str = vars_to_string missing_sut_in in
Printf.printf "Some variables are missing in input of the SUT: %s\n" missing_str
......@@ -59,7 +61,7 @@ let (check_compat : vars -> vars -> vars -> vars -> vars -> vars -> int * (vars
) else (
Printf.eprintf "RP Variables are compatible.\n";
flush stderr;
0, if args.luciole_mode then Some(luciole_in, ["Step","bool"]) else None
0, if args.luciole_mode then Some(luciole_in, ["Step",Data.Bool]) else None
)
)
......@@ -95,7 +97,7 @@ let (make_rp_list : reactive_program list ->
(reactive_program_to_string rp) (sl2str sli) (sl2str slo);
flush stderr;
slo)
else
else
step
in
ins, outs, kill, step, step_dbg, initin, initout
......@@ -157,7 +159,9 @@ let (start : unit -> Event.t) =
let _env_init_out = Util.rm_dup (List.flatten env_init_out_l) in
let vars_to_string l =
String.concat "\n" (List.map (fun (vn,vt) -> Printf.sprintf "\t%s:%s" vn vt) l)
String.concat "\n" (List.map (fun (vn,vt) ->
let vt = Data.type_to_string vt in
Printf.sprintf "\t%s:%s" vn vt) l)
in
let flat_sut_in = Util.rm_dup (List.flatten sut_in_l)
and flat_sut_out = Util.rm_dup (List.flatten sut_out_l)
......@@ -200,7 +204,7 @@ let (start : unit -> Event.t) =
if List.flatten oracle_out_l = [] then NO else
let oracle_out = List.flatten (List.map List.tl oracle_out_l) in
if List.length oracle_out < 1 then OO else
let is_bool (_,t) = (t = "bool") in
let is_bool (_,t) = (t = Data.Bool) in
let names = List.filter is_bool oracle_out in
let names = fst (List.split names) in
OC (Coverage.init names args.cov_file args.reset_cov_file)
......@@ -422,7 +426,11 @@ let (start : unit -> Event.t) =
Event.kind = Event.Ltop;
Event.depth = 1;
Event.data = edata;
Event.other = "";
Event.name = "rdbg";
Event.lang = "";
Event.inputs=[];
Event.outputs=[];
Event.sinfo=None;
Event.next =
(fun () ->
loop (check_oracles oracle_in_vals i oracle_out_l oracle_out_vals_l cov)
......
This diff is collapsed.
......@@ -652,9 +652,9 @@ endif
old: lucky luc2luciole luc4c liblucky_nc.a libluc4c_nc.a
compile_all: gen_version $(OBJDIR) gnuplot-rif gnuplot-socket call-via-socket draw-all $(LUCKY_DEF) lutin check-rif ltop lut4ocaml-clean lut4ocaml-all ldbg
compile_all: gen_version $(OBJDIR) gnuplot-rif gnuplot-socket call-via-socket draw-all $(LUCKY_DEF) lutin check-rif ltop lut4ocaml-clean lut4ocaml-all
rest: ltop lut4ocaml-clean lut4ocaml-all ldbg
rest: lut4ocaml-clean lut4ocaml-all
allnc: clean lucky ltop show stubs gnuplot-rif gnuplot-socket call-via-socket gen_luc luc2luciole luc4c libluc4c_nc.a draw-all lut4ocaml-all check-rif
static: lucky_static ltop_static show_static stubs_static gen_luc_static
......
type vars = (string * string) list
type vars = (string * Data.t) list
let debug = ref false
let debug_msg msg = if !debug then (output_string stderr ("*** dbg: "^msg) ; flush stderr)
......@@ -39,6 +39,14 @@ let (step_channel : in_channel -> out_channel -> vars -> vars ->
in
res
(* wrap it with type transformation *)
let get_io_from_lustre a b =
let il, ol = Util.get_io_from_lustre a b in
let il = List.map (fun (id,t) -> id, Data.type_of_string t) il in
let ol = List.map (fun (id,t) -> id, Data.type_of_string t) ol in
il, ol
(* XXX Doable with DynLink? Or via Ezdl? *)
let (make_ec : string -> vars * vars * (string -> unit) *
......@@ -46,7 +54,7 @@ let (make_ec : string -> vars * vars * (string -> unit) *
(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
let ec_in, ec_out = get_io_from_lustre ec_file None in
let (ec_stdin_in, ec_stdin_out) = Unix.pipe () in
let (ec_stdout_in, ec_stdout_out) = Unix.pipe () in
......@@ -93,16 +101,12 @@ 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.kind = Event.Node
{
Event.lang = "lustre";
Event.port = Event.Exit("",Expr.True (* XXX *),fun () -> []);
Event.name=ec_file;
Event.inputs = [] ;
Event.outputs = [];
};
Event.other = "";
Event.kind = Event.Exit;
Event.lang = "lustre";
Event.name=ec_file;
Event.inputs = [] ;
Event.outputs = [];
Event.sinfo = None;
Event.data = ctx.Event.ctx_data;
Event.next = (fun () -> cont (step sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
......@@ -115,7 +119,7 @@ let (make_ec : string -> vars * vars * (string -> unit) *
let (make_ec_dynlink: string -> string -> string -> vars * vars * (string -> unit) *
(Data.subst list -> Data.subst list)) =
fun node ec_file dl_file ->
let ec_in, ec_out = Util.get_io_from_lustre ec_file None in
let ec_in, ec_out = get_io_from_lustre ec_file None in
let dl = Ezdl.dlopen dl_file in
let new_ctx_cfunc = Ezdl.dlsym dl (node^ "_new_ctx") in
let step_cfunc = Ezdl.dlsym dl (node^ "_step") in
......@@ -215,16 +219,12 @@ let (make_socket_do : string -> int -> in_channel *
Event.data = ctx.Event.ctx_data;
Event.depth = ctx.Event.ctx_depth;
Event.nb = Event.get_nb ();
Event.kind = Event.Node
{
Event.lang = "socket";
Event.name=sock_adr ^ ":" ^ (string_of_int port);
Event.port = Event.Exit("",Expr.True,fun () -> []);
Event.inputs = [] ;
Event.outputs = [];
};
Event.other = "";
Event.kind = Event.Exit;
Event.lang = "socket";
Event.name=sock_adr ^ ":" ^ (string_of_int port);
Event.inputs = [] ;
Event.outputs = [];
Event.sinfo = None;
Event.next = (fun () -> cont (step sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
}
......@@ -271,7 +271,7 @@ let (make_ec_exe : string -> vars * vars * (string -> unit) *
flush stdout
)
in
let ec_in, ec_out = Util.get_io_from_lustre ec_file None in
let ec_in, ec_out = get_io_from_lustre ec_file None in
let (ec_stdin_in, ec_stdin_out) = Unix.pipe () in
let (ec_stdout_in, ec_stdout_out) = Unix.pipe () in
......@@ -318,16 +318,12 @@ 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.kind = Event.Node (
{
Event.lang = "ec";
Event.name=ec_file;
Event.port = Event.Exit("",Expr.True,fun() -> []);
Event.inputs = [] ;
Event.outputs = [];
});
Event.other = "";
Event.kind = Event.Exit;
Event.lang = "ec";
Event.name = ec_file;
Event.inputs = [] ;
Event.outputs = [];
Event.sinfo = None;
Event.next = (fun () -> cont (step sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
}
......@@ -339,10 +335,12 @@ let (make_ec_exe : string -> vars * vars * (string -> unit) *
let (make_luciole : string -> vars -> vars ->
(string -> unit) * (Data.subst list -> Data.subst list)) =
fun dro_file luciole_inputs luciole_outputs ->
if luciole_outputs <> ["Step","bool"] || luciole_outputs <> [] then (
if luciole_outputs <> ["Step",Data.Bool] || luciole_outputs <> [] then (
Printf.eprintf "Inputs are missing. Try to generate them with luciole\n";
Printf.eprintf "Luciole: generate lurette_luciole.c\n"
);
let luciole_outputs = List.map (fun (id,t) -> id, Data.type_to_string t) luciole_outputs in
let luciole_inputs = List.map (fun (id,t) -> id, Data.type_to_string t) luciole_inputs in
Luciole.gen_stubs true "lurette" luciole_outputs luciole_inputs;
Printf.eprintf "Luciole: generate lurette.dro from lurette_luciole.c\n";
flush stderr;
......
......@@ -12,7 +12,7 @@
*)
(* var name and var type list *)
type vars = (string * string) list
type vars = (string * Data.t) list
(** [make_ec ec_file.ec] handles ec programs (expanded code coming from
......
(* Time-stamp: <modified the 09/12/2013 (at 11:31) by Erwan Jahier> *)
(* Time-stamp: <modified the 20/02/2014 (at 10:26) by Erwan Jahier> *)
(**********************************************************************************)
type vars = (string * string) list
type vars = (string * Data.t) list
let (var_to_string_pair: Exp.var -> string * string) =
fun v -> Var.name v, Type.to_string2 (Var.typ v)
let (var_to_var_pair: Exp.var -> string * Data.t) =
fun v -> Var.name v, Type.to_data_t (Var.typ v)
let (to_subst_list : (string * string) list -> Value.OfIdent.t -> Data.subst list) =
let (to_subst_list : (string * Data.t) list -> Value.OfIdent.t -> Data.subst list) =
fun var_decl vals ->
try List.map (fun (n,_) -> n, Value.to_data_val (Value.OfIdent.get vals n)) var_decl
with Not_found -> assert false
......@@ -21,13 +21,12 @@ let (to_vals : Data.subst list -> Value.OfIdent.t) =
let make_lut argv =
let opt = MainArg.parse argv in
let libs = MainArg.libs opt
and prog = MainArg.infile opt
let prog = MainArg.infile opt
and node = MainArg.main_node opt
in
let lut_mach = LutExe.make opt prog node in
let lut_in = List.map var_to_string_pair (LutExe.in_var_list lut_mach) in
let lut_out = List.map var_to_string_pair (LutExe.out_var_list lut_mach) in
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 *)
......@@ -95,3 +94,36 @@ let make_lut argv =
lut_out
in
lut_in, lut_out, (fun _ -> ()), lut_step, lut_step_dbg, mems_in, mems_out
type lut_evt =
| Ltop | Call | Exit
| Try (* Try a constraint to compute the current step *)
| Sat (* the tryied constraint is Satisfiable *)
| Nsat (* the tryied constraint is Not satisfiable *)
(* | Deadlock *)
(*
(Ltop (Call (Try.Nsat*.Sat))* Exit)* )*
*)
let (to_lut_evt: Event.kind -> lut_evt) = function
| Event.Ltop -> Ltop
| Event.Call -> Call
| Event.Exit -> Exit
(* | Event.Abort -> Deadlock *)
| Event.MicroStep "try " -> Try
| Event.MicroStep "sat " -> Sat
| Event.MicroStep "usat" -> Nsat
| Event.MicroStep _ -> assert false
let (from_lut_evt: lut_evt -> Event.kind) = function
| Ltop -> Event.Ltop
| Call -> Event.Call
| Exit -> Event.Exit
| Try -> Event.MicroStep "try "
| Sat -> Event.MicroStep "sat "
| Nsat -> Event.MicroStep "usat"
(* | Deadlock -> Event.Abort *)
(* Time-stamp: <modified the 22/01/2014 (at 09:51) by Erwan Jahier> *)
(* Time-stamp: <modified the 19/02/2014 (at 17:56) by Erwan Jahier> *)
type vars = (string * string) list
type vars = (string * Data.t) list
val make_lut: string array ->
vars * vars * (string -> unit)
......@@ -8,3 +8,14 @@ val make_lut: string array ->
* (Data.subst list -> Event.ctx -> (Data.subst list -> Event.ctx -> Event.t) -> Event.t)
* Data.subst list * Data.subst list
type lut_evt =
| Ltop | Call | Exit
| Try (* Try a constraint to compute the current step *)
| Sat (* the tryied constraint is Satisfiable *)
| Nsat (* the tryied constraint is Not satisfiable *)
(* | Deadlock *)
val to_lut_evt: Event.kind -> lut_evt
val from_lut_evt: lut_evt -> Event.kind
(* Time-stamp: <modified the 19/02/2014 (at 15:35) by Erwan Jahier> *)
(* class type ocaml_reactive_machine = *)
(* object *)
(* method step : Data.subst list -> Data.subst list *)
(* method kill : string -> unit *)
(* end;; *)
type vars = (string * string) list
type vars = (Data.ident * Data.t) list
let (make_ocaml : string -> 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 cmxs ->
let _ =
let (make_ocaml : string -> 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 cmxs ->
let _ =
try Dynlink.loadfile cmxs
with Dynlink.Error msg ->
Printf.eprintf "\n*** Error in Lurette when dyn-linking against %s:\n\t%s.\n"
with Dynlink.Error msg ->
Printf.eprintf "\n*** error in rdbg (Dynlink.loadfile %s).\n*** %s.\n"
cmxs (Dynlink.error_message msg);
flush stderr;
exit 2
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.nb = Event.get_nb ();
Event.depth = ctx.Event.ctx_depth;
Event.kind = Event.Node (
let inputs = OcamlRM.get_inputs cmxs in
let inputs = List.map (fun (n,t) -> n, t) inputs in
let outputs = OcamlRM.get_outputs cmxs in
let outputs = List.map (fun (n,t) -> n, t) outputs in
let step_dbg =
try OcamlRM.get_step_dbg cmxs
with _ ->
let step_dbg sl ctx cont =
{
Event.step = ctx.Event.ctx_step;
Event.data = ctx.Event.ctx_data;
Event.nb = Event.get_nb ();
Event.depth = ctx.Event.ctx_depth;
Event.kind = Event.Exit;
Event.name = cmxs;
Event.lang = "ocaml";
Event.name=cmxs;
Event.port = Event.Exit("",Expr.True,fun() -> []);
Event.inputs = [] ;
Event.outputs = [];
});
Event.other = "";
Event.next = (fun () -> cont (OcamlRM.get_step cmxs sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
}
Event.inputs = inputs;
Event.outputs = outputs;
Event.sinfo = None;
Event.next = (fun () -> cont (OcamlRM.get_step cmxs sl) ctx);
Event.terminate = ctx.Event.ctx_terminate;
}
in
step_dbg
in
let res = (
OcamlRM.get_inputs cmxs,
OcamlRM.get_outputs cmxs,
inputs, outputs,
OcamlRM.get_kill cmxs,
OcamlRM.get_step cmxs,
step_dbg,
......@@ -51,8 +55,8 @@ let (make_ocaml : string -> vars * vars *
omems
)
in
Printf.eprintf "Lurette: %s file loaded.\n" cmxs;
res
Printf.eprintf "rdbg: %s file loaded.\n" cmxs;
res
(* cf
http://blog.rastageeks.org/ocaml/article/dynlink-as-dlopen
http://okmij.org/ftp/ML/first-class-modules/
......
type vars = (string * string) list
type vars = (Data.ident * Data.t) 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