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

K Debugger

Jump to bottom
Manasvi edited this page Mar 23, 2015 · 20 revisions

Current Status

K currently has a textual debugger which works with the Java backend. The debugger also works with the maude backend. However, currently development focuses on the Java backend.

Using the Debugger

The debugger is intended to be used as a tool for analyzing your program's behavior, and finding faults within the semantics.

Starting the debugger.

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 -s 10

Continues the execution for 10 steps.

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

Resume

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

show-graph

Allows for viewing the state of the current graph. The nodes are represented by their ids, and the transitions are represented as edges between those nodes. A sample invocation will result in something like:

Command > show-graph

The search graph is:

Vertices:

Node 0:
// Details of State
Node 2:
// Details of State
Node 3:
// Details of State
Edges:
 [Node 0 Rule at File: <Location of rule in file>, Node 2]
 [Node 2 Rule at File: <Location of rule in file>, Node 3]

show-state

View a node in the execution graph.

Sample invocation:

show-state -s <node_id>

show-transition

Explore a particular transition in the execution graph.

Sample invocation:

show-transtion -s <Node_id> <Node_id>

will result in something like:

Unparsed Node
=>
Unparsed Node

Rule at Source File: <Rule location in File>

Unparsed Rule

Both show-state and show-transition work best when used with show-graph. Both commands allow for greater analysis of a particular state or transition.

select

Select a state from all available states.

Sample invocation:

select -s <node_id>

Future Direction

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 debugger will consists of one main API, which will interact with the broader Rewrite Engine's API. Deciding the functionality of the APIs is high in priority.

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.

Debugger API

This is the API by which various debugger instances can access the state of the debugger.

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 date 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