crucible-debug: An interactive debugger for Crucible programs

[ bsd3, language, library, program ] [ Propose Tags ] [ Report a vulnerability ]

An interactive debugger for Crucible programs.

[Skip to Readme]

Modules

[Index] [Quick Jump]

Lang
- Crucible
  - Lang.Crucible.Debug
    - Lang.Crucible.Debug.Inputs
    - Lang.Crucible.Debug.Outputs
  - Lang.Crucible.Pretty

Downloads

crucible-debug-0.1.0.tar.gz [browse] (Cabal source package)
Package description (as included in the package)

Maintainer's Corner

Package maintainers

ryanglscott, galoisinc, mccleeary, sauclovian_g

For package maintainers and hackage trustees

edit package information

Candidates

No Candidates

Versions [RSS]	0.1.0
Change log	CHANGELOG.md
Dependencies	base (>=4.13 && <4.20), containers, crucible, crucible-debug, crucible-syntax, directory, filepath, isocline, lens, megaparsec, mtl, parameterized-utils, prettyprinter, ring-buffer, text, vector, what4 [details]
License	BSD-3-Clause
Author	Galois Inc.
Maintainer	langston@galois.com
Category	Language
Uploaded	by sauclovian_g at 2025-03-21T23:50:22Z
Distributions
Reverse Dependencies	1 direct, 2 indirect [details]
Executables	crucible-debug
Downloads	5 total (5 in the last 30 days)
Rating	(no votes yet) [estimated by Bayesian average]
Your Rating	λ λ λ
Status	Docs available [build log] Last success reported on 2025-03-22 [all 1 reports]

Readme for crucible-debug-0.1.0

[back to package description]

crucible-debug

crucible-debug is a library for interactive debugging of Crucible programs. It is structured as an ExecutionFeature, meaning that it can be used in situ inside of any program that uses Crucible.

Users interact with the debugger via a simple command language. This language features a number of familiar commands such as setting and removing breakpoints (break/delete), printing stack traces (backtrace), stepping through symbolic execution (step), and loading debugger commands from files (source). It additionally provides more Crucible-specific commands such as inspecting program CFGs (cfg) and printing the current path condition (path-condition). All available commands can be listed using the interactive documentation system (help).

In addition to the library, this package provides an executable. The executable begins the debugger inside of a "minimal" Crucible program that immediately returns the unit value (). This is not very interesting on its own, but the load command can load Crucible S-expression programs, and the call command can call functions from loaded programs.

The command language can be extended by downstream packages. Such extensions can be used to add commands that are specific to a particular Crucible syntax extension (i.e., source language). For example, the crucible-llvm-debug package provides the memory command to print the current LLVM memory.

This tool shares some functionality with the surveyor project. The principal architectural distinction is that crucible-debug is designed to be embedded into larger tools like Crux and SAW, while surveyor is a standalone application.

The test suite is described in its Haddocks.

Acknowledgements

This material is based upon work supported by the Defense Advanced Research Projects Agency under Contract No. W31P4Q-22-C-0017 and W31P4Q-23-C-0020

Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Defense Advanced Research Projects Agency or the U.S. Government.

Distribution Statement A. Approved for public release: distribution is unlimited.