(* Some useful short-cuts for rdbg interactive sessions *) (* you need to install the emacs highligth package available in melpa *) let hl hook (file, line, charb, chare) = let cmd = Printf.sprintf "emacsclient -e '(save-selected-window (find-file-other-window \"%s\") %s (goto-char (point-min)) (forward-line %i) (forward-char %i) (set-mark-command nil) (forward-char %i) (hlt-highlight-region) )' " file hook (line-1) charb (max 1 (chare-charb)) in ignore(Sys.command cmd) let hl_atoms = function | []-> () | x::t -> hl "(hlt-unhighlight-region)" x; List.iter (hl "") t (*| x::t -> hl "(hlt-unhighlight-all-prop t)" x; List.iter (hl "") t *) let _ = let cmd = "emacsclient -e ' (hlt-choose-default-face \"org-checkbox\") '" in ignore(Sys.command cmd) let emacs = ref false let emacs_udate e = if !emacs then try match e.sinfo with | None -> () | Some si -> let si_list = List.map (fun si -> (si.file, fst si.line, fst si.char, snd si.char)) (si()).atoms in hl_atoms si_list with Match_failure _ -> () (**********************************************************************) (* implement an undo command *) let redos = ref [1];; let store i = redos := i::!redos;; (**********************************************************************) (**********************************************************************) (* print_event tuning *) (* split the vars into returns (the enab vars, the activated vars, the other vars) nb: in the "Enab" prefix is removed from enab vars names; ie we leave only the pid and the action name *) type s = (string * string * Data.v) let split_data (l:Data.subst list) : s list * s list * s list = let l = List.map (fun (x,v) -> Str.split (Str.regexp "_") x, v) l in let rec sortv (enab, other) (x,v) = match x with | "Enab"::pid::tail -> (pid, String.concat "_" tail,v)::enab, other | pid::tail -> enab, (pid,(String.concat "_" tail),v)::other | [] -> assert false in let enab, other = List.fold_left sortv ([],[]) l in let acti_names = List.map (fun (pid, n, v) -> pid, n) enab in let act, vars = List.partition (fun (pid,n, _) -> List.mem (pid,n) acti_names) other in enab, act, vars let only_true l = List.filter (fun (_,_, v) -> v = B true) l (* Only print the active process values *) let print_sasa_event e = if e.kind <> Ltop then print_event e else let enab, act, vars = split_data e.data in let enab = only_true enab in let act = only_true act in let act_pid = List.map (fun (pid,_,_) -> pid) act in let vars = List.filter (fun (pid, _,_) -> List.mem pid act_pid) vars in let _to_string (pid, n, _) = Printf.sprintf "%s_%s" pid n in let to_string_var (pid, n, v) = Printf.sprintf "%s_%s=%s" pid n (Data.val_to_string string_of_float v) in let vars = List.rev vars in Printf.printf "[%i%s] %s\n%!" e.step (if e.step <> e.nb then (":" ^ (string_of_int e.nb)) else "") (String.concat " " (List.map to_string_var vars)) let _ = del_hook "print_event"; add_hook "print_event" print_sasa_event (**********************************************************************) let _ = time_travel true;; let e = ref (RdbgStdLib.run());; let s () = e:=step !e; emacs_udate !e; store !e.nb;; let si i = e:=stepi !e i; emacs_udate !e; store !e.nb;; let n () = e:=next !e; emacs_udate !e; store !e.nb;; let ni i = e:= nexti !e i;emacs_udate !e; store !e.nb;; let g i = e:= goto !e i;emacs_udate !e; store !e.nb;; let b () = e:= back !e ;emacs_udate !e; store !e.nb;; let bi i = e:= backi !e i;emacs_udate !e; store !e.nb;; let r () = !e.Event.reset(); e:=RdbgStdLib.run();emacs_udate !e; redos := [1];; let c () = e:= continue !e;emacs_udate !e; store !e.nb;; let cb () = e:= rev !e;emacs_udate !e; store !e.nb;; let undo () = match !redos with | _::i::t -> redos := i::t; e:=goto !e i;emacs_udate !e | _ -> e:=goto !e 1; emacs_udate !e let u = undo (**********************************************************************) open Callgraph;; let cgf () = gen_call_graph_full !e;; let cg () = (gen_call_graph !e);; let dcg ()= ignore(display_call_graph ());; let bt () = print_src !e;; let finish () = loopforever !e;; let where () = print_call_stack !e;; (**********************************************************************) (* breakpoints *) let blist () = !breakpoints;; (**********************************************************************) (* Goto to the next event which name contains a string (useful for navigating inside lustre or lutin programs) *) let nm str = e:= next_match !e str ;; let pm str = e:=previous_match !e str ;; (**********************************************************************) (* Online Level 0 doc *) let l () = print_string " Here is the list of rdbg Level 0 commands: - forward moves: n: move forward of one event ni i: move forward of i events s: move forward of one step si i: move forward of n steps nm <string>: move forward until a function which name matches a <string> - backward moves: b: move backward of one event bi i: move backward of i events pm <string>: move backward until a function which name matches a <string> g i: go to event number i - Call graphs (requires GraphViz dot, and works from Lustre node only) cg: generate the call graph (one level) cgf: generate the full call graph (i.e., node are clickable) dcg: display the generated call graph - Breakpoints: break <brpt>: add a breakpoint where <brpt> is a string of the form: \"node\" \"node@line\" \"file\" \"file@line\" c: continue forward until the next breakpoint cb: ditto backwards blist: list of the current breakpoints delete: empty the list of the current breakpoints - misc: where: print the call stack with source information - main: l: print this list of L0 commands i: print information relative to the current session parameters r: restart u: undo the last move q: quit rdbg ";; (**********************************************************************) (**********************************************************************) #mod_use "../../lib/algo/algo.ml";; #mod_use "../../lib/sasacore/register.ml";; #mod_use "../../lib/sasacore/topology.ml";; #use "../rdbg-utils/dot.ml";; let p = Topology.read dotfile;; (* shortcuts for dot viewer *) let dot () = dot p dotfile !e;; let ne () = neato p dotfile !e;; let tw () = twopi p dotfile !e;; let ci () = circo p dotfile !e;; let fd () = fdp p dotfile !e;; let sf () = sfdp p dotfile !e;; let pa () = patchwork p dotfile !e;; let os () = osage p dotfile !e;; (* To be able to choose the different default dot viewer on a per directory basis. To change the graph printer: dot_view := ci;; *) let dot_view : (unit -> unit) ref = ref ( (* choosing a reasonable default viewer *) if String.length dotfile > 4 && String.sub dotfile 0 4 = "ring" then ci else if Algo.is_directed () then dot else ne) let d = !dot_view (* Move forward until convergence, i.e., when no data changes *) let rec go () = let data = !e.data in s(); if data = !e.data then !dot_view () else go () ;; let sd () = s();!dot_view();; let nd () = n();!dot_view();; let bd () = b();!dot_view();; (**********************************************************************) (** Computing rounds *) (* a process can be removed from the mask if one action of p is triggered or if no action of p is enabled *) let get_removable pl = let pl = List.filter (fun p -> (List.exists (fun (_,_,acti) -> acti) p.actions) || (List.for_all (fun (_,enab,_) -> (not enab)) p.actions) ) pl in List.map (fun p -> p.name) pl let verbose = ref false let last_round = ref 0 let mask = ref [] (* nodes we look the activation at *) let (round : Event.t -> bool) = fun e -> e.kind = Ltop && let (pl : process list) = get_processes e in let rm_me = get_removable pl in if !verbose then ( Printf.printf "Mask : %s\n" (String.concat "," !mask); Printf.printf "To remove from mask: %s\n" (String.concat "," rm_me); flush stdout; ); mask := List.filter (fun pid -> not (List.mem pid rm_me)) !mask; let res = !mask = [] || (* when round is called twice, it should have the same result *) !last_round = e.nb in if !mask = [] then ( last_round := e.nb; mask := ( let p_with_enable_action = List.filter (fun p -> List.exists (fun (_,enab,acti) -> enab && not(acti)) p.actions) pl in let pidl = List.map (fun p -> p.name) p_with_enable_action in let pidl = List.rev pidl in if !verbose then ( Printf.printf "Next mask : %s\n" (String.concat "," pidl); flush stdout ); pidl ) ); res (* go to next and previous rounds *) let next_round e = next_cond e round;; let nr () = e:=next_round !e; !dot_view ();; let pr () = e:=goto_last_ckpt !e.nb; !dot_view ();; (* shortcuts to the default and sasa event printers *) let pe () = print_event !e;; let spe () = print_sasa_event !e;; (**********************************************************************) (* Goto to the next Lustre oracle violation *) let goto_next_false_oracle e = next_cond e (fun e -> e.kind = Exit && e.lang = "lustre" && List.mem ("ok", Bool) e.outputs && not (vb "ok" e)) let viol () = e:=goto_next_false_oracle !e (**********************************************************************) (* Perform the checkpointing at rounds! *) let _ = check_ref := round;; (**********************************************************************) let l () = l(); print_string " - sasa commands + Display network with GraphViz tools d: display the current network with dot ne: display the current network with neato tw: display the current network with twopi ci: display the current network with circo fd: display the current network with fdp sf: display the current network with sfdp pa: display the current network with patchwork os: display the current network with osage + Moving commands sd: go to the next step and display the network with one of the GraphViz tools (*) nd: go to the next event and display the network bd: go to the previous event and display the network nd: go to the next round and display the network pr: go to the previous round and display the network (*) In order to change the current graph drawing engine, you can use the dot_view command as follows: dot_view := ci " (**********************************************************************) (* ok, let's start the debugging session! *) let pdf_viewer = if Sys.command "which zathura" = 0 then "zathura" else if Sys.command "which xpdf" = 0 then "xpdf" else if Sys.command "which acroread" = 0 then "acroread" else if Sys.command "which evince" = 0 then "evince" else failwith "No pdf viewer is found" let _ = !dot_view (); let cmd = Printf.sprintf "%s sasa-%s.pdf&" pdf_viewer dotfile in Printf.printf "%s\n!" cmd; Unix.sleep 1; ignore(Sys.command cmd); round !e let _ = print_string " --> type 'man' for online help " ;;