Bugs 🐞🐛

Writing good computer programs is hard. Debugging them is, more often than not, harder. While bugs are inherent to software programming, certain classes of programming languages avoid many types of bugs by making such bugs impossible to exist. So while you can have memory leaks in a C program, Java’s garbage collector makes sure that you don’t have to manage memory, thus avoiding this whole class of bugs.

Scilla was designed to prevent entire classes of bugs such as memory leaks, memory access violations, and with a guarantee of termination (i.e., any Scilla code execution always terminates). This does not however mean that Scilla code cannot have bugs at all. Functional bugs (i.e., bugs in the business logic coded, for example) cannot be avoided. While we also have on-going efforts on tools for formal-verification of Scilla programs, a tool to aid debugging of Scilla programs is still a necessity.

Debuggers 🐞🔍

Debuggers, in contrast to what the name indicates, do not fix bugs. They are tools that programmers use to find the cause of bugs. Typically, debuggers enable executing a program (along with its inputs) step-by-step and viewing the values of program variables during this controlled execution.

The process for debugging Scilla programs, today, is not straight-forward. To find the code path that a particular execution follows, programmers must insert eventstatements (as a substitute for printf debugging). It is cumbersome most times to add extra code just for debugging and ensuring to delete them later. A debugger for Scilla can make life easier.

Instead of writing a debugger from scratch, we’ve decided to piggy-back on our ongoing Scilla Compiler (+VM) project and develop debugging tools in that framework.

The Scilla Compiler and VM

Sometime back, we wrote about a compiled execution framework for Scilla, which involves compiling Scilla down to LLVM-IR and executing the LLVM-IR by JIT compiling it to machine code in an LLVM based Virtual Machine (VM). The technically curious reader may also refer to our LLVM developer meeting 2020 poster and submission write-up. This framework is mostly feature complete, and we’re working on bringing it to production at the earliest.

An advantage that this framework provides (in addition to its main goal of lower latency execution) is the full power of the LLVM compiler infrastructure, which in our case, and for the purposes of this article, is developing a debugging tool for Scilla.

As the first step in adding debug information (debuginfo) support for our
compiler, we contributed debuginfo support to LLVM’s OCaml interface. This enabled us to annotate the LLVM-IR we generate for our Scilla contracts with source location information.

Demo Video

The video below shows a simple contract that makes a Scilla map access, and the execution of its transition IncrementNOpt line-by-line.

A GDB script is set up (for convenience) to set a breakpoint in IncrementNOpt and the debugging session is started. Once the breakpoint is hit, a line-by-line trace is performed. The executable file in this session is a user-friendly frontend for the VM that takes in a contract and its inputs (message and state JSONs) from the command line and produces an output JSON, just like the command line Scilla interpreter. The GDB session is in-fact a debugging session of this executable, that, during the run, enters into the JIT-compiled native code of the Scilla contract / transition.

We expect that this single step execution support (as the first phase in our debug tooling work) will help Scilla programmers make sense of complex control flows.

What Next?

Our implementation of debugging support today covers only line number information which enables step-by-step execution of Scilla code. There is no support yet for printing runtime values of Scilla variables. This is relatively a more complex task, but we do plan to have it for the production release of Scilla compiler and VM.

On a broader note, our Scilla development toolkit currently provides a static type checker (labeled as “Scilla Checker” in the chart below), and an interpreter. The following items are planned for future releases:

• A higher level language: Scilla is an intermediate level language. This means that it is designed to be easily used as input for optimizers, static checkers and verification tools. This can sometimes result in Scilla programs being verbose and hard to write manually. To address this problem, we plan to design and implement a higher-level language with an aim of being “easy to write code in”. A compiler to translate programs written in this new language to Scilla will be provided.
• Scilla compiler and VM: We’ve already spoken about this with many details and references above.
• Verification tools: Our ongoing project to transpile Scilla to TLA+ is a part of our overall effort in providing formal verification and proof support for Scilla contracts.
  

   │
      Higher│
      Level │Language
            │
       ┌────▼─────┐
       │ Compiler │
       │          │
       └────┬─────┘
            │
       ┌────▼─────┐
       │  Scilla  │
       │  Checker │
       │          │
  ┌────┴─────┬────┴────┐
  │          │         │
  │          │         │
  │          │         │

┌─────▼──────┐ │ ┌──────▼─────┐ ┌────────────┐
│ Scilla │ │ │ Scilla ◄─┤ GDB Based │
│Interpreter │ │ │ Compiler │ │ Debugger │
│ │ │ │ & VM ├─► │
└────────────┘ │ └────────────┘ └────────────┘
│
┌──────────▼─────────┐
│ Formal │
│ Verification │
│ Tools │
│ │
└────────────────────┘