Skip to content

Commit 2a6cb19

Browse files
author
Mark R. Tuttle
committed
First complete draft of documentation.
1 parent e6905cb commit 2a6cb19

File tree

16 files changed

+368
-220
lines changed

16 files changed

+368
-220
lines changed

‎docs/book.toml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,4 +3,4 @@ authors = ["Mark R. Tuttle"]
33
language = "en"
44
multilingual = false
55
src = "src"
6-
title = "Proof debugger"
6+
title = "CBMC Proof Debugger"

‎docs/src/README.md‎

Lines changed: 34 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,41 @@
1-
# Proof debugger
1+
# CBMC Proof Debugger
22

3-
This is a proof debugger for
3+
The
4+
[CBMC Proof Debugger](https://github.com/model-checking/cbmc-proof-debugger)
5+
is a
46
[Visual Studio Code](https://code.visualstudio.com/)
5-
that makes it easy to debug proof counterexamples produced by
6-
[CBMC](https://github.com/diffblue/cbmc) and
7-
[Kani](https://github.com/model-checking/kani) on C and Rust code.
7+
debugger for
8+
[CBMC](https://github.com/diffblue/cbmc)
9+
error traces.
10+
11+
[CBMC](https://github.com/diffblue/cbmc)
12+
is a model checker for C. CBMC will explore all possible paths
13+
through your code on all possible inputs, and will check that all
14+
assertions in your code are true. CBMC can also check for the
15+
possibility of security issues (like buffer overflow) and for
16+
instances of undefined behavior (like signed integer overflow).
17+
If CBMC finds a code issue, it generates an error trace demonstrating how that
18+
issue could occur.
19+
If CBMC terminates without finding any issues, the result is
20+
assurance that your code behaves as expected.
21+
CBMC is a *bounded* model checker, however, so getting CBMC to terminate
22+
may require restricting inputs to some bounded size,
23+
and CBMC's assurance is restricted to these bounded inputs.
24+
25+
[CBMC Viewer](https://github.com/model-checking/cbmc-viewer)
26+
is a tool that scans the output of CBMC and produces a browsable summary
27+
of its findings, making it easy to root cause the issues CBMC finds using
28+
any web browser. Viewer also produces a summary of its findings in the
29+
form of a collection of json blobs.
30+
31+
The
32+
[CBMC Proof Debugger](https://github.com/model-checking/cbmc-proof-debugger)
33+
loads the json summaries produced by CBMC Viewer,
34+
and lets a developer explore the error traces produced by CBMC using
35+
the Visual Studio Code's debugger.
836

937
To get started, see our
10-
* [installation instructions](installation.md) and a
38+
* [installation instructions](user-guide/installation.md) and a
1139
* [simple demonstration](demo) of how to use the proof debugger.
1240

1341
References:

‎docs/src/SUMMARY.md‎

Lines changed: 6 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,12 @@
11
# Summary
22

3-
* [Getting started](README.md)
4-
* [Installation](installation.md)
5-
* [Simple demo](demo/README.md)
6-
* [HTTP demo](demo-on-http/README.md)
3+
* [CBMC Proof Debugger](README.md)
74
* [User guide](user-guide/README.md)
5+
* [Installation](user-guide/installation.md)
6+
* [Configuration](user-guide/configuration.md)
7+
* [Demonstration](demo/README.md)
88
* [Developer guide](developer-guide/README.md)
9+
* [Installation](developer-guide/installation.md)
910
* [Architecture](developer-guide/architecture.md)
11+
* [Implementation](developer-guide/implementation.md)
1012
* [Frequently asked questions](faq/README.md)

‎docs/src/demo/README.md‎

Lines changed: 86 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,90 @@
11
# Demonstration
22

3-
Follow the [installation instructions](../installation.md) to install the
4-
proof debugger if you have not already done so.
5-
These instructions will clone the source tree into the directory
6-
`proof-debugger` and install the debugger into Visual Studio Code.
3+
This is a simple demonstration of the CBMC Proof Debugger.
74

8-
Change to the directory `proof-debugger/demo`.
5+
* Follow the CBMC
6+
[installation](https://model-checking.github.io/cbmc-training/installation.html)
7+
instructions to install CBMC and CBMC-related tools.
8+
* Follow the debugger [installation](../user-guide/installation.md)
9+
instructions to add the debugger to Visual Studio Code.
10+
* Clone the debugger code repository and change to the demo directory
11+
```
12+
git clone https://github.com/model-checking/cbmc-proof-debugger
13+
cd cbmc-proof-debugger/demo
14+
```
15+
This directory contains a simple project consisting of a
16+
[Makefile](proof-debugger/demo/Makefile) and two source files
17+
[foo.c](demo/foo.c) and [main.c](demo/main.c).
18+
* Run CBMC on the source code
19+
```
20+
make
21+
```
22+
This will run `goto-cc` to compile the source code for CBMC,
23+
run `cbmc` to do bounded model checking on the source code with CBMC, and
24+
run `cbmc-viewer` to produce a browsable summary of the CBMC findings.
25+
* Just for fun, open the browsable summary in a web browser and look around.
26+
On MacOS, do
27+
```
28+
open report/html/index.html
29+
```
30+
The `report` directory produced by `cbmc-viewer`
31+
actually contains two subdirectories:
32+
* `html` contains the browsable summary.
33+
* `json` contains some JSON files that are summaries of artifacts produced
34+
by CBMC.
935

10-
This directory contains a simple project consisting of a
11-
[Makefile](proof-debugger/demo/Makefile) and two source files
12-
[foo.c](demo/foo.c) and [main.c](demo/main.c).
36+
Now let's run the debugger on the error traces produced by CBMC.
37+
In the `demo` project directory:
38+
* Open Visual Studio Code.
39+
```
40+
code .
41+
```
42+
43+
* Configure the debugger for this project using the
44+
[configuration](../user-guide/configuration.md) instructions.
45+
* Open the proof debugger console: At the bottom of the screen, click on
46+
the console name "Proof Debugger."
47+
(If you don't see any consoles at the bottom
48+
of the screen, click on "View -> Terminal" to make them visible.)
49+
* Load the error traces: On the right of the debugger console, click on
50+
"Load Traces," navigate to the folder `demo/report/json` in the dialog
51+
window, and click on "Open."
52+
* Select the trace you want to debug: Clicking on the failure description
53+
for the failure you want to debug. For example, under Line 3,
54+
click on "dereference failure: pointer NULL in *ptr."
55+
* Start the debugger: Click on the "debug and run" icon on the left,
56+
and select the "CBMC Proof Debugger" from the drop-down list of available
57+
debuggers at the top, and press the green "start" icon to the left of
58+
"CBMC Proof Debugger."
59+
60+
Now you can see the familiar debugger interface. In particular, you can see
61+
the debugger toolbar at the top of the screen.
62+
63+
<img src="debugger-toolbar.png" alt="Debugger toolbar"
64+
style="height: 40px; margin: auto; display: block;">
65+
66+
The icons left-to-right are:
67+
* Run forwards
68+
* Step over forwards
69+
* Step into function
70+
* Step out of function
71+
* Step over backwards
72+
* Run backwards
73+
* Restart the debugger
74+
* Halt the debugger
75+
76+
For more information, read about
77+
[debugging](https://code.visualstudio.com/docs/editor/debugging).
78+
79+
Now you can use the debugger interface to examine the program behavior
80+
determined by the error trace just as you would to examine the program
81+
behavior determined by a set of input values.
82+
83+
* You can run forward to run until the failure occurs, examine
84+
the program stack, and step forwards and backwards to examine the
85+
code leading up to the failure.
86+
* You can set a break point and run forwards or backwards to a break point.
87+
* You can examine data in any stack frame, any static variable, and any
88+
heap object by clicking in the data view on the left. In particular,
89+
for structured data like strings, arrays, and structs, you can click
90+
on a value to open it up and expose data components.

‎docs/src/demo/debugger-toolbar.png‎

9.4 KB
Loading

‎docs/src/developer-guide/README.md‎

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,6 @@
11
# Developer guide
22

3-
## Installation
4-
5-
* `npm upgrade` will upgrade dependencies to the lastest versions and
6-
update packages.json.
7-
* `make format` will run the typescript source code formatter
8-
[tsfmt](https://www.npmjs.com/package/typescript-formatter).
3+
This is the start of a developer guide for the CBMC Proof Debugger.
4+
* [Installation](installation.md)
5+
* [Architecture](architecture.md)
6+
* [Implementation](implementation.md)

‎docs/src/developer-guide/architecture.md‎

Lines changed: 48 additions & 135 deletions
Original file line numberDiff line numberDiff line change
@@ -1,59 +1,8 @@
11
# Architecture
22

3-
This document describes the overall architecture of the proof
4-
debugger. It describes the major components of the implementation and
5-
the organization of the source code. A lot of the presentation here
6-
comes from comments embedded in the source code. For more detail, see
7-
the source code itself.
3+
This is a description of the debugger architecture in Visual Studio Code.
84

9-
## Visual Studio Code
10-
11-
The [user documentation](https://code.visualstudio.com/docs)
12-
is the place to start if you are unfamiliar with Visual Studio Code. The
13-
[user guide](https://code.visualstudio.com/docs/editor/codebasics)
14-
introduces the basic concepts like
15-
[editing](https://code.visualstudio.com/docs/editor/codebasics)
16-
and
17-
[debugging](https://code.visualstudio.com/docs/editor/debugging).
18-
Most important are
19-
* The
20-
[debug actions](https://code.visualstudio.com/docs/editor/debugging#_debug-actions)
21-
that a software developer uses to interact with a debugger.
22-
* The [debug configuration](https://code.visualstudio.com/docs/editor/debugging#_launch-configurations)
23-
that a software developer uses to select a debugger.
24-
25-
26-
The [developer documentation](https://code.visualstudio.com/api) is the place
27-
for extension developers to start.
28-
Most important is
29-
* The
30-
[debugger extension](https://code.visualstudio.com/api/extension-guides/debugger-extension)
31-
overview gives a fairly complete example of how to write and package a debugger
32-
extension.
33-
The code repository used in that example was the starting point for this debugger.
34-
35-
36-
You should now be able to read the code implementing this debugger,
37-
but you will eventually want to skim
38-
* The
39-
[Extension Guides](https://code.visualstudio.com/api/extension-guides/overview)
40-
that describe the Visual Studio Code Extension APIs.
41-
This debugger uses
42-
* [Tree Views](https://code.visualstudio.com/api/extension-guides/tree-view)
43-
to display the code issues having traces available for debugging.
44-
* The [UX Guidelines](https://code.visualstudio.com/api/ux-guidelines/overview)
45-
that describe the Visual Studio Code user interface. This debugger uses
46-
47-
* [Views](https://code.visualstudio.com/api/ux-guidelines/views)
48-
as containers of the content that appears in sidebars and panels,
49-
* [Sidebars](https://code.visualstudio.com/api/ux-guidelines/sidebars)
50-
and
51-
[Panels](https://code.visualstudio.com/api/ux-guidelines/panel)
52-
to display views, and
53-
* [Notifications](https://code.visualstudio.com/api/ux-guidelines/notifications)
54-
to display progress and error messages.
55-
56-
## Architecture overview
5+
## Debugger overview
576

587
Visual Studio Code implements a generic user interface to debuggers.
598
A developer needs to learn only one user interface to use any debugger
@@ -99,85 +48,49 @@ for gdb:
9948
<img src="https://microsoft.github.io/debug-adapter-protocol/img/init-launch.png">
10049
</center>
10150

102-
## Implementation overview
103-
104-
### Values
105-
106-
A value can be a string, a number, a struct, or an array. A value can appear in a trace or be stored in memory.
107-
A value is represented in CBMC output as a string that must be parsed.
108-
* value.ts: Defines the Value class and subclasses for strings, number, structs, and arrays.
109-
* valueLexer.ts: A lexer for values in CBMC output.
110-
* valueParser.ts: A parser for values in CBMC output.
111-
112-
### Variables
113-
114-
A variable in a trace is a string like 'foo.bar[0]` consisting of a base name 'foo'
115-
followed by a list of selectors like field member selection '.bar' or array
116-
indexing '[0]'.
117-
We model memory as a single struct, so 'foo.bar[0]' is modeled as 'MEMORY.foo.bar[0]'.
118-
We think of '.foo.bar[0]' as a path through memory, where path elements
119-
denote field selection and array indexing.
120-
A variable is represented in CBMC output as a string that must be parsed.
121-
* variable.ts: Defines the Element class and subclasses for field selection and array indexing.
122-
* variableLexer.ts: A lexer for variables in CBMC output.
123-
* variableParser.ts: A parser for variables in CBMC output.
124-
125-
### Failures
126-
127-
A panel at the bottom of the screen displays the set of failures that can be debugged.
128-
The failures are organized into a tree and displayed as
129-
nested lists of files, functions within a file, lines within a
130-
function, and failures at a line.
131-
The debug extension describes this tree to Visual Studio Code using the Tree View API.
132-
The key to the Tree View is the TreeDataProvider interface that includes
133-
functions like getChildren(node) returning a node's children and getTreeItem(node)
134-
returning a node's contents.
135-
So the debug extension must load the failures available for debugging,
136-
organize them into a tree,
137-
and use the tree to implement the TreeDataProvider interface.
138-
* traceData.ts:
139-
The method create(result, property, loop) loads the summaries produced
140-
by cbmc-viewer and returns a mapping file_name -> function_name -> line_number -> failure.
141-
* traceTree.ts:
142-
The method create(mapping) transforms a failure mapping into a failure tree.
143-
* traceView.ts:
144-
The class TraceProvider implements the TreeDataProvider.
145-
146-
### Debug adapter
147-
148-
The debug adapter sits between Visual Studio Code and the debugger.
149-
The job of the debug adapter is to accept requests from Visual Studio
150-
Code like "set breakpoint" and "run" and to generate responses after
151-
driving the debugger and inspecting its state.
152-
153-
Visual Studio Code and the debug adapter communicate via requests and responses
154-
defined by the [Debug Adapter Protocol](https://microsoft.github.io/debug-adapter-protocol).
155-
Visual Studio Code sends the
156-
[SetBreakpointsRequest](https://microsoft.github.io/debug-adapter-protocol/specification#Requests_SetBreakpoints)
157-
to the debug adapter which sends a SetBreakpointsResponse back to Visual Studio Code.
158-
159-
The class ProofDebuggerSession implements the DebugSession interface. It maintains the state of the
160-
debug adapter for one debugging session, and it implements methods like setBreakPointsRequest that
161-
Visual Studio Code can use to send the SetBreakpointsRequest and receive the SetBreapointsRepsonse.
162-
163-
How the debug adapter and the debugger communicate is of no concern to Visual Studio Code. In our case,
164-
the debugger is really just a trace simulator. The debug adaptor uses methods in the simulator interface
165-
to move the simulator forwards and backwards in the trace, and to examine the current state of the trace.
166-
167-
* adapter.ts: Defines ProofDebuggerSession implementing the DebugSession interface.
168-
169-
### Debugger
170-
171-
* simulator.ts: Simulator is the debugger being managed by the debug adpater
172-
* simulatorState.ts: A state of a trace being simulated by the simulator
173-
* simulatorTrace.ts: A trace being simulated by the simulator (and methods to load the trace)
174-
175-
### Extension activation
176-
177-
* extension.ts: Methods to activate and deactive the debugger extension.
178-
179-
### Extension utilities
180-
181-
* constants.ts: Defines string constants used in the extension
182-
* exceptions.ts: Defines an exception raised by the extension
183-
* storage.ts: Defines methods to access the persistent storage available to the extension
51+
## Debugger documentation
52+
53+
The [user documentation](https://code.visualstudio.com/docs)
54+
is the place to start if you are unfamiliar with Visual Studio Code. The
55+
[user guide](https://code.visualstudio.com/docs/editor/codebasics)
56+
introduces the basic concepts like
57+
[editing](https://code.visualstudio.com/docs/editor/codebasics)
58+
and
59+
[debugging](https://code.visualstudio.com/docs/editor/debugging).
60+
Most important are
61+
* The
62+
[debug actions](https://code.visualstudio.com/docs/editor/debugging#_debug-actions)
63+
that a software developer uses to interact with a debugger.
64+
* The [debug configuration](https://code.visualstudio.com/docs/editor/debugging#_launch-configurations)
65+
that a software developer uses to select a debugger.
66+
67+
68+
The [developer documentation](https://code.visualstudio.com/api) is the place
69+
for extension developers to start.
70+
Most important is
71+
* The
72+
[debugger extension](https://code.visualstudio.com/api/extension-guides/debugger-extension)
73+
overview gives a fairly complete example of how to write and package a debugger
74+
extension.
75+
The code repository used in that example was the starting point for this debugger.
76+
77+
78+
You should now be able to read the code implementing this debugger,
79+
but you will eventually want to skim
80+
* The
81+
[Extension Guides](https://code.visualstudio.com/api/extension-guides/overview)
82+
that describe the Visual Studio Code Extension APIs.
83+
This debugger uses
84+
* [Tree Views](https://code.visualstudio.com/api/extension-guides/tree-view)
85+
to display the code issues having traces available for debugging.
86+
* The [UX Guidelines](https://code.visualstudio.com/api/ux-guidelines/overview)
87+
that describe the Visual Studio Code user interface. This debugger uses
88+
89+
* [Views](https://code.visualstudio.com/api/ux-guidelines/views)
90+
as containers of the content that appears in sidebars and panels,
91+
* [Sidebars](https://code.visualstudio.com/api/ux-guidelines/sidebars)
92+
and
93+
[Panels](https://code.visualstudio.com/api/ux-guidelines/panel)
94+
to display views, and
95+
* [Notifications](https://code.visualstudio.com/api/ux-guidelines/notifications)
96+
to display progress and error messages.

0 commit comments

Comments
 (0)