RDBG - a Reactive programs DeBuGger

Table of Contents

Table of Contents

1 TL;DR

RDBG is a programable Reactive programs DeBuGger that shares the same infrastructure as lurette. With lurette one can test a reactive program (SUT) by

  • executing it into a simulated (reactive) environment
  • checking the execution is correct w.r.t. to some specification using test oracles (synchronous observers).

For instance, if one wants to test

  • a reactive program written in Lustre V6 (node main of file prog.lus),
  • whose environment model is defined by a Lutin program (node main of file progenv.lut),
  • whose correct behavior is defined by another Lustre V6 programs (node prop of file prog.lus),

one can invoke lurette as follows:

  lurette -sut "lv6 prog.lus -n main" \
          -env "lutin progenv.lut -n main" \
          -oracle "lv6 prog.lus -n prog_prop"

If lurette finds a problem, i.e., if an oracle is violated because of a bug in the SUT, its environment, or in the oracle, one can invoke rdbg in exactly the same manner:

  rdbg -sut "lv6 prog.lus -n main" \
       -env "lutin progenv.lut -n main" \
       -oracle "lv6 prog.lus -n prog_prop"

Note that you are not obliged to use any oracle. Actually, you are even note obliged to use any environment, but that you have to provide inputs manually (which can be cumbersome, but also useful in some cases).

  rdbg -sut "lv6 prog.lus -n main"

~The source code is available at https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/rdbg

2 Install

2.1 Via opam 2 (prefered method)

opam repo add verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
opam update -y
opam install -y rdbg

Once this is done, upgrading to the last version of the tools is as simple as:

opam update
opam upgrade

2.2 Via docker

2.3 From source

You will need:

  • make (gnu)
  • a set of tools installable via opam
    • dune
    • rdbg
    • lutin (not for compiling actually, but for using sasa with custom demons)

One can mimick the content of the build job in the project Gitlab CI script.

3 Basic usage

3.1 Tutorial (Level 0)

This tutorial is made for people that knows nothing about ocaml, and that are not willing to learn it to take advantage of the programming capability of rdbg.

Although rdbg is built on top of an ocaml toplevel REPL interpreter, it is possible to use it with knowing ocaml at all. Of course you loose the possibility of extending the set of available commands.

Let's illustrate the use of rdbg on a Lustre program. Let's download of such example from the Lustre examples github repository (https://github.com/jahierwan/lustre-examples/blob/master/verimag-v6/).

wget https://raw.githubusercontent.com/jahierwan/lustre-examples/master/core/examples/stopwatch.lus

If you have installed the Synchrone Reactive Tool Box, you should be able to simulate this program.

lv6 stopwatch.lus -n stopwatch -exec

As this program requires 3 Boolean inputs, you are prompted to enter a sequence of Boolean values. Try to enter the following input (that will perform 4 steps):

t f f
t t f
t f f
t f f

As manually entering inputs is boring, we can ask to a Lutin program (env.lut) to generate random ones.

echo "node env(time:int) returns(time_unit:bool;b1:bool;b2:bool) = loop true" > env.lut

You can simulate this Lutin program as follows:

lutin env.lut -n env

Now we can invoke rdbg using those 2 programs plugged onto each other:

rdbg -sut "lv6 stopwatch.lus -n stopwatch -exec" -env "lutin env.lut -n env"

rdbg asks to enter one of the 3 following choices:

[] create a fresh session
[q] quit

The first possibility in the list is the one that is chosen by default if you directly press [Return]. Hence press [Return] to create a fresh session (This will create a rdbg-session.ml file, but let's forget about that for now)

  1   1   call env            ()
(rdbg)

The first integer is the event number, and the second is the step number. Then comes the kind of event (call or exit), the name of the current node, and the variables instanciation.

Here at the first event, we should be able to see the value of the node env input (time:int). But this input comes from the SUT output, and is this not available at the first step. Let's move one step forward to see such a value.

(rdbg) s
120   2   call env            (0)
(rdbg)

Now you can see the value (0) of the =time input of node env at the beginning of the second step. Notice also that the step counter has been incremented by 1, while the event counter has been incremented by 119!

You can list the available commands with 'l'. You may try each of those commands to see what happens.

(rdbg) l
(rdbg) help "n"

(rdbg) n
(rdbg) n
(rdbg) ni 10
(rdbg) b
(rdbg) s
(rdbg) si 5
(rdbg)

3.2 Redo the last command

If you type [Enter] without any key, the last command will be used.

3.3 Leave the debugger, and come back

To leave rdbg, simply type 'q'.

To launch again previous sessions, you don't need to provide any arguments; just launch rdbg. By default the first created session will be used. If you have created several different sessions, you can chose it from a list (session numbers are created in increasing order):

$ rdbg 
Enter one of the following key (the first is the default one):
  [] #use "rdbg-session.ml"
  [1] #use "rdbg-session1.ml"
  [2] #use "rdbg-session2.ml"
  [c] create a fresh session
  [q] quit

[/1/2/c/q/s]:

If you don't want to reuse a previous session, enter the c key. In this case of course, you should have provided some -sut arguments.

If you type [Enter] without any key, the firstly created session will be used. If you want to launch an older session, type the corresponding integer.

3.4 Multi-line mode

If you type (at least) a space (i.e., an empty string) before your command at the rdbg prompt, you will enter a multi-line mode. In this mode, the [Enter] key won't send the command to the rdbg engine. It will do it only once you enter the ";;" string. This is handy to type programs on several lines, which is out of the scope of this tutorial. We mention this here because if by mistake you enter a space, you will be stuck in this multi-line mode.

3.5 Using emacs

In order to let rdbg opens emacs buffer and highlights active expressions, one can call rdbg with the --emacs options (you need to install the emacs highligth package available in melpa). In order to turn on or off the emacs mode from rdbg, one can do:

 emacs := true;;
 emacs := false;;

3.6 The list of commands

The list of commands can be obtained with the 'l' key:

(rdbg) l
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)
  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
  q: quit rdbg
(rdbg)

3.7 The rdbg CLI

 rdbg --help
rdbg is a Reactive programs debugger. 
rdbg is extensible: debugging commands or functions can be programmed
rdbg is meant to be easily pluggable. Currently, existing plugins are: 
    lutin, lustre-v6, sasa

Examples of usage:
  rdbg -sut "lv6 file.lus -n node" -env "lutin f.lut -n main"
  rdbg -sut "ecexe-rif f.ec node" -env "lutin f.lut -n main"
  lv6 -2c -cc f.lus -n n ;rdbg -sut "./n.exec" -env "lutin f.lut -n main"

Hint: preprend rdbg by 'ledit' (or 'ledit -h rdbg-history -x').

More information: http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/rdbg/

usage: rdbg [<options>] 
where <options> are:

-sut, --sut <string>
      Add a sut 
-sut-nd, --sut-nd <string>
      Add a sut, but don't debug it
-env, --env <string>
      Add an env
-env-nd, --env-nd <string>
      Add an env, but don't debug it
-oracle, --oracle <string>
      Add an oracle
-oracle-nd, --oracle-nd <string>
      Add an oracle, but don't debug it
-lurette, --lurette
      Use the lurette mode (i.e., runs everything without debugging)
-l, --test-length, --step-number <int>
      in lurette mode only: Set test length (step number)
-o, -output, --output, -rif, --rif <string>
      Set the output file name (currently,  "www.rif")
-e, -emacs, --emacs
      Use emacs to open appropriate buffers while debugging
-h, -help, --help
      Display this help message
-m, -more, --more
      Display more options
 rdbg --more
-g, --gnuplot
      in lurette mode only:  Launch gnuplot to visualize the generated rif file
-s, --sim2chro
      in lurette mode only:  Launch sim2chro to visualize the generated rif file
-orf, --overwrite-rif-file
      Overwrite "www.rif" if it exists without trying to invent a new name
-dsoe, --dont-stop-on-oracle-error
      Do not stop if one oracle is violated
-cv, --cov-file <string>
      file name coverage info will be put into
-rcv, --reset-cov-file
      Reset coverage file data
-no-log, --no-log
      Do no generate a rdbg.log file and output everything on stdout
-v, -verbose, --verbose
      Echo the commands sent to rdbg-top
--debug
      set on a verbose mode to (try to) understand what's going on
--ocaml-version
      Print the current ocaml version it was compiled with and exit
-version, --version
      Print the current version and exit

4 Advanced usage

4.1 Introduction

This tutorial is made for people that knows a little bit of ocaml, and that are willing to take advantage of the programming capability of rdbg.

rdbg-top is an ocaml toplevel REPL (Read-Eval-Print-Loop) with some modules pre-loaded (cf the rdbg.log to see the messages generated by rdbg-top during this loading).

rdbg is a wrapper around rdbg-top, which basically performs 3 things:

  1. It discharges users from writing () and ;; before rdbg commands. This wrapping can be:
    • turned on/off by the #auto_on / #auto_off directives;
    • locally inhibited for lines beginning with the ' ' character.
  2. It generates a rdbg-session-<i>.ml file that is loaded by rdbg-top. Each time rdbg is invoked with some arguments, an new rdbg-session-<i>.ml can be created. When rdbg is invoked (with or without argument), the user is prompted with the possibility to use previously generated sessions (cf Basic usage Section).
  3. It generates a default my-rdbg-tuning.ml file, if none exists in the current directory. my-rdbg-tuning.ml is meant to contains user commands that persist across sessions. This file is loaded by from rdbg-session-<i>.ml at the very end of it.

my-rdbg-tuning.ml actually contains all the code that implements the Basic (Level 0) commands, taking advantage of Ocaml modules described in Sections 5, 6, and 7. We explain how below.

4.2 The rdbg kernel

All rdbg commands are built on top of 2 functions only:

run : unit -> Event.t
next :  Event.t -> Event.t

run (Section 5) returns the first event (Section 6). next allows one to access to the next event. Launch rdbg-top, and try to enter the following Ocaml sentences:

let e = run();;
let e = next e;;
let e = next e;;
let e = next e;;
let e = next e;;

e is of type Event.t, which is an ocaml structure. You can access to the various fields of that structure as follows:

e.nb;;
e.data;;

If you are an ocaml programmer, you probably understand all the things that you could program using those 2 functions. Anyway, you just can use the ones that are provided in the RdbgStdLib module, which Interface documentation can be found in Section 7. You may also want to look at how they are implemented. Most of most are fairly simple.

4.3 Sugaring rdbg-top

Writing let e = next e;; to move one event forward is tedious. A sensible trick is to store the current event in a reference, and to define shortcuts that, by a side-effect, updates the current event.

let e = ref (run());;
let n () = e:=next !e;;

Now, to move one event forward from rdbg-top, you can type n();;. From rdbg, since it automatically adds () and ;;, you can actually just type n. The generated my-rdbg-tuning.ml file contains such kind of short-cuts for most useful functions defined in 7.

4.4 More details on How rdbg interacts with the ocaml REPL

An OCaml sentence is any string you type at the ocaml REPL prompt until you type ;; and then the [Return] key. An rdbg sentence is any string you type at the rdbg prompt until you press the [Return] key.

rdbg sends everything you type to an ocaml toplevel REPL, trying to guess when to add boring () and ;; and the end of your rdbg sentence (). Hence, when you type at the rdbg prompt:

  • help "apropos"[Return] it sends to the ocaml REPL the string help "apropos";;, which calls the help (pre-loaded) function with the ="apropos"= string argument.
  • n[Return] it sends n();; to the ocaml REPL (which will do something iff the function n is defined and takes () (unit) as argument).

If you want to be sure that rdbg does not add anything to the sentences you type, just add a leading blank:

  • ​ let my_n () = n ();; sends let my_n () = n ();;

but if you type

  • ​ n[Return] it sends n and nothing happen as ocaml waits for ;;; so if then you type
  • ;;[Return] it sends ;;, which returns the type of n, but without actually calling n as no () has been provided.

In different words n[Return] has the same effect as ​ n();;[Return]

4.5 Multi-line mode

If you want to write a function on several lines, begin your sentence by a space (i.e., an empty string) at the rdbg prompt. To end your sentence and send it to rdbg-top, enter the ";;" string.

5 RdbgMain

This Section might be useful for Level 1 users (those who want to write debugging commands in ocaml). The functions and the documentation it contains can be obtained at the (rdbg prompt using the apropos (a) and the help (h) functions.

(rdbg) help "apropos" 
(rdbg) help "help"

This is the rdbg-top Main module.

6 Event

This Section might be useful for Level 1 users (those who want to write debugging commands in ocaml). The functions and the documentation it contains can be obtained at the (rdbg prompt using the apropos (a) and the help (h) functions.

(rdbg) help "apropos" 
(rdbg) help "help"

This module only defines the Event.t type.

6.3 Expr

7 RdbgStdLib

This Section might be useful for Level 1 users (those who want to write debugging commands in ocaml). The functions and the documentation it contains can be obtained at the (rdbg prompt using the apropos (a) and the help (h) functions. Try the following (without leading space!):

(rdbg) help "apropos" 
(rdbg) help "help" 
help "back"

This library is built on top of the Event module and the run function of the RdbgMain module.

run : unit -> Event.t

If you want to see how they are implemented:

The following ones are specific to Lutin programs:

https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/rdbg/blob/master/lib/lutinRdbg.mli

8 FAQ

8.1 Is there a FAQ?

yes

Author: Erwan Jahier

Created: 2019-11-13 mer. 14:04

Emacs 25.2.2 (Org mode 8.2.10)

Validate