Skip to content

GitLab

L
lutin
Commit 8671d38c authored by erwan's avatar erwan
Browse files
Options

Upgrade: the rdbg package renamed Event into RdbgEvent

parent 7addffd8
Pipeline #39230 passed with stages
        in 4 minutes and 43 seconds
        Hide whitespace changes
        Inline Side-by-side
        Showing with 166 additions and 162 deletions
        bin/lurette-nocaml/dune
        View file @ 8671d38c
        (executable
        (name lurette)
        (modes (byte exe) (native exe))
        (libraries lustre-v6 lutin)
        ; (libraries camlidl lustre-v6 lutin sasa)
        ......@@ -12,5 +13,8 @@
        (install
        (section bin)
        (package lutin)
        (files (lurette.exe as lurette))
        (files
        (lurette.exe as lurette)
        (lurette.bc as lurette4dbg)
        )
        )
        bin/lurette-nocaml/lurette.ml
        View file @ 8671d38c
        (* Time-stamp: <modified the 06/02/2020 (at 17:25) by Erwan Jahier> *)
        (* Time-stamp: <modified the 16/03/2020 (at 11:43) by Erwan Jahier> *)
        (* Mimick the behavior of 'rdbg -lurette', but without the dependency
        on ocaml *)
        ......@@ -141,7 +141,7 @@ let _ =
        RdbgRun.clean_terminate();
        flush stderr;
        exit 2
        | Event.End(i) ->
        | RdbgEvent.End(i) ->
        RdbgRun.clean_terminate();
        exit i
        | pb ->
        ......
        lib/lutin/lutExe.ml
        View file @ 8671d38c
        ......@@ -89,7 +89,7 @@ let (_tbl_to_string: t -> string) =
        *)
        let (to_event_var:'a Var.t -> Event.var) =
        let (to_event_var:'a Var.t -> RdbgEvent.var) =
        fun v ->
        Var.name v, Type.to_data_t (Var.typ v)
        ......@@ -262,7 +262,7 @@ let make opt infile mnode = (
        let exped = Expand.make tlenv mainprg mnode in
        Verbose.put ~flag:dbg "LutExe.make: Expand.make %s OK\n" mnode;
        (* actual result .... *)
        (* Verbose.put ~flag:dbg "Event.set_seed %i\n"(MainArg.seed opt); *)
        (* Verbose.put ~flag:dbg "RdbgEvent.set_seed %i\n"(MainArg.seed opt); *)
        MainArg.set_seed opt (Some (MainArg.seed opt));
        if MainArg.run opt then
        of_expanded_code opt exped
        ......@@ -506,33 +506,33 @@ let min_max_src (bl1,el1,bc1,ec1,bchar1,echar1) (bl2,el2,bc2,ec2,bchar2,echar2)
        exception No_src_info
        let rec (to_src_info: CoIdent.src_stack -> Event.src_info_atom) =
        let rec (to_src_info: CoIdent.src_stack -> RdbgEvent.src_info_atom) =
        fun l ->
        match l with
        | [] -> raise No_src_info
        | (lxm, _,None)::tl ->
        {
        Event.file = lxm.Lexeme.file;
        Event.line = lxm.Lexeme.line, lxm.Lexeme.line;
        Event.char = lxm.Lexeme.cstart, lxm.Lexeme.cend;
        Event.stack = if tl=[] then None else Some (to_src_info tl);
        Event.str = lxm.Lexeme.str;
        RdbgEvent.file = lxm.Lexeme.file;
        RdbgEvent.line = lxm.Lexeme.line, lxm.Lexeme.line;
        RdbgEvent.char = lxm.Lexeme.cstart, lxm.Lexeme.cend;
        RdbgEvent.stack = if tl=[] then None else Some (to_src_info tl);
        RdbgEvent.str = lxm.Lexeme.str;
        }
        | (lxm,_,Some ve)::tl ->
        let line_b, line_e, col_b, col_e, char_b, char_e = cstr_src_info_of_val_exp ve in
        let file = lxm.Lexeme.file in
        let filecontent = Mypervasives.readfile file in
        {
        Event.str =
        RdbgEvent.str =
        (try String.sub filecontent char_b (char_e - char_b + 1)
        with _ ->
        try String.sub filecontent char_b (String.length filecontent - char_b)
        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 = col_b, col_e;
        Event.stack = if tl=[] then None else Some (to_src_info tl);
        RdbgEvent.file = file;
        RdbgEvent.line = line_b, line_e;
        RdbgEvent.char = col_b, col_e;
        RdbgEvent.stack = if tl=[] then None else Some (to_src_info tl);
        }
        ......@@ -705,8 +705,8 @@ let string_of_cont_mnemo = function
        | Crun (s) -> Printf.sprintf "!%s" s
        type e = Event.t
        type ctx = Event.t
        type e = RdbgEvent.t
        type ctx = RdbgEvent.t
        type continuation = {
        doit: behavior -> behavior;
        ......@@ -780,7 +780,7 @@ let put_in_para te1 te2 = (
        let (event_incr : ctx -> MainArg.t -> ctx) =
        fun ctx opt ->
        MainArg.event_incr opt;
        Event.incr_event_nb ctx
        RdbgEvent.incr_event_nb ctx
        let rec genpath (t : t) (data : store) (* data env = inputs + pres *)
        ......@@ -1540,31 +1540,31 @@ let rec (genpath_ldbg : t -> store -> t CoTraceExp.t -> ctx ->
        let try_cont ctx t () =
        let t, new_acc, is_sat = check_satisfiablity t new_acc in
        if (is_sat) then
        let enb = ctx.Event.nb in
        let enb = ctx.RdbgEvent.nb in
        let ctx = event_incr ctx t.arg_opt in
        { ctx with
        Event.kind = Event.MicroStep "sat ";
        Event.nb = enb;
        Event.lang = "lutin";
        Event.next = (fun () ->
        RdbgEvent.kind = RdbgEvent.MicroStep "sat ";
        RdbgEvent.nb = enb;
        RdbgEvent.lang = "lutin";
        RdbgEvent.next = (fun () ->
        (br_cont.doit_ldbg ctx t (Goto (new_acc, TE_eps))
        cont fail_cont excn_cont));
        Event.sinfo = Some (fun () -> {
        Event.expr = cstr;
        Event.more = None;
        Event.atoms = si_atoms;
        Event.in_subst = [];
        Event.out_subst = [];
        RdbgEvent.sinfo = Some (fun () -> {
        RdbgEvent.expr = cstr;
        RdbgEvent.more = None;
        RdbgEvent.atoms = si_atoms;
        RdbgEvent.in_subst = [];
        RdbgEvent.out_subst = [];
        });
        Event.depth = ctx.Event.depth;
        Event.step = ctx.Event.step;
        Event.name = ctx.Event.name;
        Event.inputs = ctx.Event.inputs;
        Event.outputs = ctx.Event.outputs;
        Event.locals = []; (* fixme *)
        Event.data = ctx.Event.data;
        Event.terminate = ctx.Event.terminate;
        Event.reset = ctx.Event.reset;
        RdbgEvent.depth = ctx.RdbgEvent.depth;
        RdbgEvent.step = ctx.RdbgEvent.step;
        RdbgEvent.name = ctx.RdbgEvent.name;
        RdbgEvent.inputs = ctx.RdbgEvent.inputs;
        RdbgEvent.outputs = ctx.RdbgEvent.outputs;
        RdbgEvent.locals = []; (* fixme *)
        RdbgEvent.data = ctx.RdbgEvent.data;
        RdbgEvent.terminate = ctx.RdbgEvent.terminate;
        RdbgEvent.reset = ctx.RdbgEvent.reset;
        }
        else (* the constraint is unsat *)
        let lazy_ci = fun () ->
        ......@@ -1579,41 +1579,41 @@ let rec (genpath_ldbg : t -> store -> t CoTraceExp.t -> ctx ->
        let expr_cc = Exp.to_expr cc.g_form in
        ExprUtil.get_info t.snt bdd bdd_acc (expr_cc, bdd_cc)
        in
        let enb = ctx.Event.nb in
        let enb = ctx.RdbgEvent.nb in
        let ctx = event_incr ctx t.arg_opt in
        let usat_event =
        { ctx with
        Event.nb = enb;
        Event.kind = Event.MicroStep "usat";
        Event.lang = "lutin";
        Event.next = (* backtrack *) (fun () -> fail_cont ctx t);
        Event.sinfo = Some (fun () -> {
        Event.expr = cstr;
        Event.more = Some lazy_ci;
        Event.atoms = si_atoms;
        Event.in_subst = [];
        Event.out_subst = [];
        RdbgEvent.nb = enb;
        RdbgEvent.kind = RdbgEvent.MicroStep "usat";
        RdbgEvent.lang = "lutin";
        RdbgEvent.next = (* backtrack *) (fun () -> fail_cont ctx t);
        RdbgEvent.sinfo = Some (fun () -> {
        RdbgEvent.expr = cstr;
        RdbgEvent.more = Some lazy_ci;
        RdbgEvent.atoms = si_atoms;
        RdbgEvent.in_subst = [];
        RdbgEvent.out_subst = [];
        });
        Event.locals = []; (* fixme *)
        RdbgEvent.locals = []; (* fixme *)
        }
        in
        usat_event
        in
        let enb = ctx.Event.nb in
        let enb = ctx.RdbgEvent.nb in
        let ctx = event_incr ctx t.arg_opt in
        { ctx with
        Event.nb = enb;
        Event.kind = Event.MicroStep "try ";
        Event.lang = "lutin";
        Event.sinfo = Some (fun () -> {
        Event.expr = cstr;
        Event.more = None;
        Event.atoms = si_atoms;
        Event.in_subst = [];
        Event.out_subst = [];
        RdbgEvent.nb = enb;
        RdbgEvent.kind = RdbgEvent.MicroStep "try ";
        RdbgEvent.lang = "lutin";
        RdbgEvent.sinfo = Some (fun () -> {
        RdbgEvent.expr = cstr;
        RdbgEvent.more = None;
        RdbgEvent.atoms = si_atoms;
        RdbgEvent.in_subst = [];
        RdbgEvent.out_subst = [];
        });
        Event.locals = []; (* fixme *)
        Event.next = try_cont ctx t;
        RdbgEvent.locals = []; (* fixme *)
        RdbgEvent.next = try_cont ctx t;
        }
        )
        (* Sequence *)
        ......@@ -2110,25 +2110,25 @@ let rec (genpath_ldbg : t -> store -> t CoTraceExp.t -> ctx ->
        cont2
        in
        (* exiting a run *)
        let enb,_d = ctx.Event.nb, ctx.Event.depth in
        let enb,_d = ctx.RdbgEvent.nb, ctx.RdbgEvent.depth in
        let ctx = event_incr ctx t.arg_opt in
        let event =
        { ctx with
        Event.step = ctx.Event.step;
        Event.nb = enb;
        Event.depth = ctx.Event.depth;
        Event.kind = Event.MicroStep "quit";
        Event.lang = "lutin";
        Event.name = rid;
        Event.inputs = ctx.Event.inputs;
        Event.outputs = ctx.Event.outputs;
        Event.locals = []; (* fixme *)
        Event.data = ctx.Event.data;
        Event.sinfo = ctx.Event.sinfo;
        Event.next =
        RdbgEvent.step = ctx.RdbgEvent.step;
        RdbgEvent.nb = enb;
        RdbgEvent.depth = ctx.RdbgEvent.depth;
        RdbgEvent.kind = RdbgEvent.MicroStep "quit";
        RdbgEvent.lang = "lutin";
        RdbgEvent.name = rid;
        RdbgEvent.inputs = ctx.RdbgEvent.inputs;
        RdbgEvent.outputs = ctx.RdbgEvent.outputs;
        RdbgEvent.locals = []; (* fixme *)
        RdbgEvent.data = ctx.RdbgEvent.data;
        RdbgEvent.sinfo = ctx.RdbgEvent.sinfo;
        RdbgEvent.next =
        (fun () -> step_ldbg ctx t react ins cont3 fail_cont excn_cont);
        Event.terminate = ctx.Event.terminate;
        Event.reset = ctx.Event.reset;
        RdbgEvent.terminate = ctx.RdbgEvent.terminate;
        RdbgEvent.reset = ctx.RdbgEvent.reset;
        }
        in
        event
        ......@@ -2330,14 +2330,14 @@ and (to_reactive_prg_ldbg :
        let predata = List.map (fun (n,v) -> "pre_"^n, Value.to_data_val v) predata in
        let ctx_save = ctx in
        let ctx = { ctx with
        Event.name = rid;
        Event.data = edata@predata;
        Event.inputs = List.map to_event_var (in_var_list run_t);
        Event.outputs = List.map to_event_var (out_var_list run_t);
        RdbgEvent.name = rid;
        RdbgEvent.data = edata@predata;
        RdbgEvent.inputs = List.map to_event_var (in_var_list run_t);
        RdbgEvent.outputs = List.map to_event_var (out_var_list run_t);
        }
        in
        let ctx = Event.incr_event_depth ctx in
        let d = ctx.Event.depth in
        let ctx = RdbgEvent.incr_event_depth ctx in
        let d = ctx.RdbgEvent.depth in
        let (cont2: ctx -> t -> behavior -> e) = fun ctx2 t b ->
        match b with
        | Raise x -> excn_cont ctx2 caller_t x
        ......@@ -2374,30 +2374,30 @@ and (to_reactive_prg_ldbg :
        let cstr = Exp.to_expr zeguard.g_form in
        let ctx2 = { ctx_save with
        (* once we exit, we return back to the previous ctx *)
        Event.nb = ctx2.Event.nb;
        Event.data = edata; (* used? *)
        Event.depth = ctx.Event.depth -1
        RdbgEvent.nb = ctx2.RdbgEvent.nb;
        RdbgEvent.data = edata; (* used? *)
        RdbgEvent.depth = ctx.RdbgEvent.depth -1
        }
        in
        let ctx2 = event_incr ctx2 t.arg_opt in
        let event =
        { ctx with
        Event.nb = ctx2.Event.nb-1;
        Event.kind = Event.Exit;
        Event.lang = "lutin";
        (* Event.port = Event.Exit (guard_to_string zeguard, cstr,lazy_si); *)
        Event.name = rid;
        Event.locals = []; (* fixme *)
        Event.data = edata;
        Event.sinfo = Some (fun () -> {
        Event.expr = cstr;
        (*Event.str = guard_to_string zeguard; *)
        Event.more = None;
        Event.atoms = si_atoms;
        Event.in_subst = [];
        Event.out_subst = [];
        RdbgEvent.nb = ctx2.RdbgEvent.nb-1;
        RdbgEvent.kind = RdbgEvent.Exit;
        RdbgEvent.lang = "lutin";
        (* RdbgEvent.port = RdbgEvent.Exit (guard_to_string zeguard, cstr,lazy_si); *)
        RdbgEvent.name = rid;
        RdbgEvent.locals = []; (* fixme *)
        RdbgEvent.data = edata;
        RdbgEvent.sinfo = Some (fun () -> {
        RdbgEvent.expr = cstr;
        (*RdbgEvent.str = guard_to_string zeguard; *)
        RdbgEvent.more = None;
        RdbgEvent.atoms = si_atoms;
        RdbgEvent.in_subst = [];
        RdbgEvent.out_subst = [];
        });
        Event.next =
        RdbgEvent.next =
        (fun () ->
        cont ctx2 caller_t
        (DoStep_ldbg (to_reactive_prg_ldbg rid run_t state'))
        ......@@ -2406,20 +2406,20 @@ and (to_reactive_prg_ldbg :
        in
        event
        in (* end of cont2 *)
        let enb = ctx.Event.nb in
        let enb = ctx.RdbgEvent.nb in
        let ctx = event_incr ctx run_t.arg_opt in
        let ctx = Event.incr_event_depth ctx in (* inner events are one step deapper *)
        let ctx = RdbgEvent.incr_event_depth ctx in (* inner events are one step deapper *)
        { ctx with
        Event.nb = enb ;
        Event.depth = d;
        Event.kind = Event.Call;
        Event.lang = "lutin";
        Event.name = rid;
        Event.locals = []; (* fixme *)
        Event.data = edata @ predata;
        Event.next = (fun () -> genpath_ldbg run_t data cstate ctx cont2
        RdbgEvent.nb = enb ;
        RdbgEvent.depth = d;
        RdbgEvent.kind = RdbgEvent.Call;
        RdbgEvent.lang = "lutin";
        RdbgEvent.name = rid;
        RdbgEvent.locals = []; (* fixme *)
        RdbgEvent.data = edata @ predata;
        RdbgEvent.next = (fun () -> genpath_ldbg run_t data cstate ctx cont2
        fail_cont excn_cont);
        Event.sinfo = None;
        RdbgEvent.sinfo = None;
        }
        ......@@ -2519,11 +2519,11 @@ let (step_rdbg: ctx -> string -> t -> control_state -> data_state ->
        in
        let ctx_save = ctx in
        let ctx = { ctx with
        Event.name = node;
        Event.depth = ctx.Event.depth+1;
        Event.data = datal;
        Event.inputs = List.map to_event_var (in_var_list t);
        Event.outputs = List.map to_event_var (out_var_list t);
        RdbgEvent.name = node;
        RdbgEvent.depth = ctx.RdbgEvent.depth+1;
        RdbgEvent.data = datal;
        RdbgEvent.inputs = List.map to_event_var (in_var_list t);
        RdbgEvent.outputs = List.map to_event_var (out_var_list t);
        }
        in
        let cont2 = fun ctx2 t bg ->
        ......@@ -2563,55 +2563,55 @@ let (step_rdbg: ctx -> string -> t -> control_state -> data_state ->
        let ctx2 = event_incr ctx2 t.arg_opt in
        let ctx2 = { ctx_save with
        (* once we exit, we return back to the previous ctx *)
        Event.nb = ctx2.Event.nb;
        Event.data = edata; (* used? *)
        Event.depth = ctx.Event.depth -1
        RdbgEvent.nb = ctx2.RdbgEvent.nb;
        RdbgEvent.data = edata; (* used? *)
        RdbgEvent.depth = ctx.RdbgEvent.depth -1
        }
        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;
        Event.kind = Event.Exit;
        Event.lang = "lutin";
        Event.name = node;
        Event.inputs = ctx.Event.inputs;
        Event.outputs = ctx.Event.outputs;
        Event.locals = []; (* fixme *)
        Event.data = edata;
        RdbgEvent.step = ctx.RdbgEvent.step;
        RdbgEvent.nb = ctx2.RdbgEvent.nb-1;
        RdbgEvent.depth = ctx.RdbgEvent.depth;
        RdbgEvent.kind = RdbgEvent.Exit;
        RdbgEvent.lang = "lutin";
        RdbgEvent.name = node;
        RdbgEvent.inputs = ctx.RdbgEvent.inputs;
        RdbgEvent.outputs = ctx.RdbgEvent.outputs;
        RdbgEvent.locals = []; (* fixme *)
        RdbgEvent.data = edata;
        Event.sinfo = Some (fun () -> {
        Event.expr = cstr;
        (* Event.str = guard_to_string zeguard; *)
        Event.more = None;
        Event.atoms = si_atoms;
        Event.in_subst = [];
        Event.out_subst = [];
        RdbgEvent.sinfo = Some (fun () -> {
        RdbgEvent.expr = cstr;
        (* RdbgEvent.str = guard_to_string zeguard; *)
        RdbgEvent.more = None;
        RdbgEvent.atoms = si_atoms;
        RdbgEvent.in_subst = [];
        RdbgEvent.out_subst = [];
        });
        (* Event.Exit (guard_to_string zeguard, cstr, lazy_si) *)
        Event.next = (fun () -> cont ctx2 t ctrl data);
        Event.terminate = ctx2.Event.terminate;
        Event.reset = ctx2.Event.reset;
        (* RdbgEvent.Exit (guard_to_string zeguard, cstr, lazy_si) *)
        RdbgEvent.next = (fun () -> cont ctx2 t ctrl data);
        RdbgEvent.terminate = ctx2.RdbgEvent.terminate;
        RdbgEvent.reset = ctx2.RdbgEvent.reset;
        }
        )
        )
        in
        let enb = ctx.Event.nb in
        let enb = ctx.RdbgEvent.nb in
        let ctx = event_incr ctx t.arg_opt in
        let d = ctx.Event.depth in
        let ctx = { ctx with depth = ctx.Event.depth+1 } in
        let d = ctx.RdbgEvent.depth in
        let ctx = { ctx with depth = ctx.RdbgEvent.depth+1 } in
        { ctx with
        Event.nb = enb;
        Event.depth = d;
        Event.kind = Event.Call;
        Event.lang = "lutin";
        Event.name = node;
        Event.next = (fun () ->
        RdbgEvent.nb = enb;
        RdbgEvent.depth = d;
        RdbgEvent.kind = RdbgEvent.Call;
        RdbgEvent.lang = "lutin";
        RdbgEvent.name = node;
        RdbgEvent.next = (fun () ->
        get_behavior_gen_ldbg t data.ins data.mems ctrl ctx cont2);
        Event.sinfo = None; (* XXX fixme ? *)
        RdbgEvent.sinfo = None; (* XXX fixme ? *)
        }
        ......
        lib/lutin/lutExe.mli
        View file @ 8671d38c
        ......@@ -87,10 +87,10 @@ val find_one_sol : t -> guard -> t * guard * (Var.env_out * Var.env_loc)
        val make_pre : Var.env_in -> Var.env_out -> Var.env_loc -> Var.env
        (*
        May raise Deadlock (or Event.Error ("deadlock",event))
        May raise Deadlock (or RdbgEvent.Error ("deadlock",event))
        *)
        type ctx = Event.t
        type e = Event.t
        type ctx = RdbgEvent.t
        type e = RdbgEvent.t
        val step: t -> control_state -> data_state -> t * control_state * data_state
        val step_rdbg: ctx -> string -> t -> control_state -> data_state ->
        (ctx -> t -> control_state -> data_state -> e) -> e
        ......
        lib/lutin/lutinRun.ml
        View file @ 8671d38c
        (* Time-stamp: <modified the 30/08/2019 (at 14:37) by Erwan Jahier> *)
        (* Time-stamp: <modified the 16/03/2020 (at 11:38) by Erwan Jahier> *)
        (**********************************************************************************)
        let (var_to_var_pair: Exp.var -> string * Data.t) =
        ......@@ -19,7 +19,7 @@ let (to_vals : Data.subst list -> Value.OfIdent.t) =
        Value.OfIdent.empty
        open RdbgPlugin
        type ctx = Event.t
        type ctx = RdbgEvent.t
        let compact str =
        let str = Str.global_replace (Str.regexp "\n") ";" str in
        ......@@ -62,7 +62,7 @@ let make argv =
        in
        let (lut_step_dbg:
        Data.subst list -> ctx ->
        (Data.subst list -> ctx -> Event.t) -> Event.t) =
        (Data.subst list -> ctx -> RdbgEvent.t) -> RdbgEvent.t) =
        fun sl ctx cont ->
        let cont_lut_step ctx =
        fun new_tables new_cs new_ds ->
        ......
        lib/lutin/reactive.ml
        View file @ 8671d38c
        ......@@ -5,8 +5,8 @@ type prg = DoStep of (Value.t list -> Value.t list * prg)
        let step p = match p with DoStep p -> p
        type ctx = Event.t
        type e = Event.t
        type ctx = RdbgEvent.t
        type e = RdbgEvent.t
        type 't prg_ldbg =
        DoStep_ldbg of (ctx -> 't -> Value.t list ->
        ......
        lib/lutin/reactive.mli
        View file @ 8671d38c
        ......@@ -4,8 +4,8 @@
        type prg = DoStep of (Value.t list -> Value.t list * prg)
        val step : prg -> Value.t list -> (Value.t list * prg)
        type ctx = Event.t
        type e = Event.t
        type ctx = RdbgEvent.t
        type e = RdbgEvent.t
        type 't prg_ldbg =
        ......
        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