Skip to content
This repository has been archived by the owner on Feb 1, 2020. It is now read-only.

K Debugger

Jump to bottom
Manasvi Saxena edited this page Feb 17, 2016 · 20 revisions

Current Status

K currently has a textual debugger which works with all backends that implement the K Rewriter Interface.

Using the Debugger

The debugger is intended to be used as a tool for analyzing your program's behavior.

The debugger works with krun. To use it call KRun with the --debugger flag.

Example:

krun --debugger filename

Will start debug mode, with the initial configuration loaded.

Supported Functionality

Type help at the prompt to get a list of commands. (Note: The debugger supports autocomplete)

Step

Take one or more steps, i.e., continue the execution for a pre specified number of steps.

Example

step 10

Continues the execution for 10 steps.

You can also just type step, which corresponds to step 1.

Back Step

To step back in the execution, use back-step or simply b.

Resume

To Continue the execution from the current state, use resume or r.

Peek

To view the current confiugation, use peek or p.

Show

To match a pattern on the current configuration, use the show <pattern> command. If the match is successful, the set of substitutions is displayed.

Watches

A watch in the K debugger is a pattern that is matched on the current configuration every time an action is performed. In order to specify a watch, use watch [pattern]. If the pattern argument is not specified, the debugger displays a list of all active watches.

Remwatch

In order to remove a watch, use the xwatch <Watch-Id> or remwatch <Watch-Id> command.

Setting Checkpoint Intervals

In order to change the interval at which the debugger records checkpoint-configurations, use the ch <interval> command, where interval is the desired checkpoint interval. For programs with large configurations, changing the checkpoint interval can have a significant impact on performance.

Roadmap used in the development of the KORE based debugger

The debugger is expected to be more than a concrete configuration stepper, and will eventually be an interactive program verifier. (Prof. Rosu's slides describing the debugger's intended functionality)

Design Overview

The design of the debugger infrastructure is based on the concept of having well defined, relatively stable, and exhaustively documented interfaces for the debugger and the rewriter. The new debugger design expects any classes implementing the debugger interface to interact with other parts of framework using only the well defined rewriter/parser/KORE APIs. The new KORE based debugger now has a well documented interface, and a class that implements the interface, strictly conforming to the standards described in the above mentioned slides.

Rewrite Engine API

This is the API by which the K framework tools make use of the rewrite engine provided by a backend. We want this API to be minimal and efficient. For example, an interface providing only a one-step rewrite relation is minimal but not efficient. K now has a relatively stable and efficient rewriter interface.

Debugger API

This is the API by which various debugger instances can access the state of the debugger. The API also allows other tools to communicate with the debugger. The KORE based debugger now has a stable API.

Intended Functionality

(Most of the content has been taken from Prof. Rosu's slides)

  • The debugger interface will allow for viewing of relevant parts of the configuration only. Sometimes, when configurations are very long, it's not feasible to view and find faults in the configuration. Hence, the debugger will allow for only parts of the configuration to be view (perhaps only the top cell initially). The user can then view the remaining parts of the configuration by clicking/selecting (depending on the interface) the part of the configuration required. (Also, it can be the case that the configuration's expansion/contraction will be managed by the fronted/observer, while the debugger will only manage the main rewriting functionality).

  • The debugger will work with symbolic configurations as well. The system will thus be interacting with Z3. The backend will be expanded to include functionality to allow symbolic execution for the debugger's interface. (Or the debugger's interface can have the functionality). Proving Reachability tasks will also be supported.

  • Equality of Configurations and tools built around it.

  • Rule Applied and Substitutions on a state with one/multiple steps to be supported. This functionality will also be supported in the current version, with the concrete execution stepper.

  • Taking multiple steps, and a different branch of the execution tree will be supported. For example, in the graphical executor, a double array can be used to indicate multiple steps. Options can include clicking (in the graphical frontend) the double array to view previous states, rules e.t.c.

  • KORE date strucutures will be used to store backend specific data as "blackboxes", for efficiency purposes.

  • Incrementally transforming the backend data (blackbox) into KAST, node by node. In a given configuration, instead of Converting the entire configuration, the conversion should be done one element at a time, depending on the user input. Currently, the entire configuration is processed at the same time, but we ultimately want only relevant parts to be processed.

Feedback/comments welcome.

Clone this wiki locally