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 Saxena edited this page Jan 6, 2015 · 20 revisions

Current Status

Currently K has a textual debugger, which has the following functionality:

  • Stepping - Step by step execution is supported. The initial and subsequent configurations are displayed. User can specify the number of steps that should be taken.

  • Subsequent States - All possible states that can be reached from a particular state. Another state can be selected from these states for further execution. Thus, any branch of the execution tree can be explored.

Future Direction

The debugger is expected to be more than a concrete configuration stepper, and will eventually be an interactive program verifier.

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.

Clone this wiki locally