Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CN debugger: allow debugging of CN via Gillian #128

Draft
wants to merge 21 commits into
base: main
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
21 commits
Select commit Hold shift + click to select a range
c4291af
debugger: a rudimentary debugger that handles `initialize`
samcowger Oct 18, 2024
3f78a83
ci: debugger configuration
samcowger Nov 4, 2024
d1b637e
debugger: make initialization a little less synchronous
samcowger Oct 18, 2024
04e833a
debugger: initialize simple state on `launch` command
samcowger Oct 30, 2024
cae9d2f
debugger: handle `debuggerState` commands
samcowger Oct 30, 2024
df378e2
debugger: organize command modules together
samcowger Oct 30, 2024
00c10a9
debugger: handle `stepSpecific` command, support `debugStateUpdate` e…
samcowger Oct 30, 2024
0cc8007
debugger: support `jump` command
samcowger Oct 30, 2024
82bec10
debugger: send `initialized` event
samcowger Oct 30, 2024
937374e
debugger: send `stopped` event
samcowger Oct 30, 2024
2cc2aaf
debugger: handle `threads` request
samcowger Oct 30, 2024
954e2cb
debugger: support `stackTrace` requests
samcowger Oct 30, 2024
d941328
debugger: merge `Order` and `FrameMap` modules
samcowger Oct 30, 2024
9d32bc7
debugger: handle `scopes` request
samcowger Nov 1, 2024
7dd4884
debugger: handle `variables` requests
samcowger Nov 1, 2024
5683c0a
server: implement lens creation
samcowger Nov 4, 2024
955a105
server: publish gillian-debugging lenses
samcowger Nov 4, 2024
c5366fe
client: declare and register debugging facilities
samcowger Nov 4, 2024
7538fa3
server: condition lens publication on configuration option
samcowger Nov 4, 2024
cbf1126
client: expose lens configuration option
samcowger Nov 4, 2024
e9ebbca
debugger: only use `state_report`s with locations
samcowger Nov 5, 2024
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 44 additions & 0 deletions .github/workflows/debugger-ci.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
name: CN Debugger CI

on:
push:
branches:
- main
pull_request:
branches:
- main

# Cancel in-progress job when a new push is performed
concurrency:
group: ci-${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true

jobs:
build:
strategy:
matrix:
ocaml-version: [5.1.1]
os: [ubuntu-22.04]

runs-on: ${{ matrix.os }}

steps:
- name: Check out repository
uses: actions/checkout@v4

- name: Set up OCaml
uses: ocaml/setup-ocaml@v3
with:
ocaml-compiler: ${{ matrix.ocaml-version }}

- name: Link lockfile
run: ln -s cn-dap.opam.locked-${{ matrix.ocaml-version }} cn-dap.opam.locked

- name: Install dependencies
run: opam install ./cn-dap.opam --deps-only --locked -y

- name: Build
run: eval $(opam env) && dune build

- name: Run tests
run: eval $(opam env) && dune test
2 changes: 1 addition & 1 deletion .github/workflows/ocaml-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ jobs:
ln -s cn-lsp.opam.locked-${{ matrix.ocaml-version }} cn-lsp.opam.locked

- name: Install dependencies
run: opam install . --deps-only --locked -y
run: opam install ./telemetry.opam ./cn-lsp.opam --deps-only --locked -y

- name: Build
run: eval $(opam env) && dune build
Expand Down
11 changes: 11 additions & 0 deletions cn-client/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -49,13 +49,24 @@
"default": null,
"description": "Location of the LSP server"
},
"CN.showGillianDebugLenses": {
"type": "boolean",
"default": false,
"description": "Show code lenses that activate Gillian debugging. Note that this functionality relies on the Gillian debugging extension (https://gillianplatform.github.io/sphinx/debugger.html) being installed, or run in a development host context."
},
"CN.telemetryDir": {
"type": "string",
"default": null,
"description": "Where to store telemetry. Changes take effect on server start/restart."
}
}
},
"debuggers": [
{
"type": "CN",
"label": "CN Debugger"
}
],
"grammars": [
{
"path": "./syntaxes/cn.tmLanguage.json",
Expand Down
30 changes: 30 additions & 0 deletions cn-client/src/extension.ts
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,13 @@ export async function activate(context: vsc.ExtensionContext): Promise<void> {
client.sendRequest(req, params);
});

context.subscriptions.push(
vsc.debug.registerDebugAdapterDescriptorFactory(
"CN",
new CNDebugAdaptorDescriptorFactory()
)
);

client.start();
console.log("started client");
}
Expand Down Expand Up @@ -186,3 +193,26 @@ async function setConfiguredServerContext(serverContext: ServerContext) {
vsc.ConfigurationTarget.Global
);
}

class CNDebugAdaptorDescriptorFactory
implements vsc.DebugAdapterDescriptorFactory
{
createDebugAdapterDescriptor(
_session: vsc.DebugSession,
executable: vsc.DebugAdapterExecutable | undefined
): vsc.ProviderResult<vsc.DebugAdapterDescriptor> {
let langCmd: string = "cn-debug";

const config = vsc.workspace.getConfiguration("gillianDebugger");
console.log("Configuring debugger...", { config });

let args = [
"--log",
"/Users/sam/projects/verse/verse-toolchain/cn-dap/debugger/log.txt",
];

executable = new vsc.DebugAdapterExecutable(langCmd, args);

return executable;
}
}
54 changes: 54 additions & 0 deletions cn-dap.opam
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
# This file is generated by dune, edit dune-project instead
opam-version: "2.0"
synopsis: "CN Debug Adapter"
description: "A debug adapter protocol implementation for CN state dumps"
maintainer: ["Sam Cowger"]
authors: ["Sam Cowger"]
depends: [
"dune" {>= "3.16"}
"ocaml" {>= "4.14.1" & < "6.0.0"}
"base" {>= "v0.16.3" & < "v0.18"}
"cerberus" {= "b9daa22"}
"cerberus-lib" {= "b9daa22"}
"cn" {= "b9daa22"}
"dap" {>= "1.0.6" & < "2.0.0"}
"gillian" {= "c6802c5"}
"logs" {>= "0.7.0" & < "1.0.0"}
"odoc" {with-doc}
]
build: [
["dune" "subst"] {dev}
[
"dune"
"build"
"-p"
name
"-j"
jobs
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
]
]
pin-depends: [
[
"cerberus.b9daa22"
"git+https://github.com/rems-project/cerberus.git#b9daa22"
]
[
"cerberus-lib.b9daa22"
"git+https://github.com/rems-project/cerberus.git#b9daa22"
]
[
"cn.b9daa22"
"git+https://github.com/rems-project/cerberus.git#b9daa22"
]
[
"gillian.c6802c5"
"git+https://github.com/GillianPlatform/Gillian.git#c6802c5"
]
[
"simple_smt.~dev"
"git+https://github.com/NatKarmios/simple-smt-ocaml#b88c4b0685f6ec989e8b4c911e296c4087768db8"
]
]
130 changes: 130 additions & 0 deletions cn-dap.opam.locked-5.1.1
Original file line number Diff line number Diff line change
@@ -0,0 +1,130 @@
opam-version: "2.0"
name: "cn-dap"
version: "dev"
synopsis: "CN Debug Adapter"
description: "A debug adapter protocol implementation for CN state dumps"
maintainer: "Sam Cowger"
authors: "Sam Cowger"
depends: [
"alcotest" {= "1.0.1"}
"angstrom" {= "0.16.0"}
"angstrom-lwt-unix" {= "0.16.0"}
"astring" {= "0.8.5"}
"base" {= "v0.17.1"}
"base-bigarray" {= "base"}
"base-bytes" {= "base"}
"base-domains" {= "base"}
"base-nnp" {= "base"}
"base-threads" {= "base"}
"base-unix" {= "base"}
"bigstringaf" {= "0.10.0"}
"cerberus" {= "b9daa22"}
"cerberus-lib" {= "b9daa22"}
"cmdliner" {= "1.3.0"}
"cn" {= "b9daa22"}
"conf-findutils" {= "1"}
"conf-gmp" {= "4"}
"conf-pkg-config" {= "3"}
"conf-sqlite3" {= "1"}
"cppo" {= "1.6.9"}
"csexp" {= "1.5.2"}
"dap" {= "1.0.6"}
"dune" {= "3.16.0"}
"dune-configurator" {= "3.16.0"}
"fmt" {= "0.9.0"}
"gillian" {= "c6802c5"}
"jane-street-headers" {= "v0.17.0"}
"jst-config" {= "v0.17.0"}
"lem" {= "2022-12-10"}
"logs" {= "0.7.0"}
"lwt" {= "5.7.0"}
"lwt_ppx" {= "2.1.0"}
"lwt_react" {= "1.2.0"}
"memtrace" {= "0.2.3"}
"menhir" {= "20231231"}
"menhirCST" {= "20231231"}
"menhirLib" {= "20231231"}
"menhirSdk" {= "20231231"}
"monomorphic" {= "2.1.0"}
"num" {= "1.5-1"}
"ocaml" {= "5.1.1"}
"ocaml-base-compiler" {= "5.1.1"}
"ocaml-compiler-libs" {= "v0.12.4"}
"ocaml-config" {= "3"}
"ocaml-options-vanilla" {= "1"}
"ocaml-syntax-shims" {= "1.0.0"}
"ocaml_intrinsics_kernel" {= "v0.17.0"}
"ocamlbuild" {= "0.15.0"}
"ocamlfind" {= "1.9.6"}
"ocamlgraph" {= "2.1.0"}
"ocplib-endian" {= "1.2"}
"parsexp" {= "v0.17.0"}
"pprint" {= "20230830"}
"ppx_assert" {= "v0.17.0"}
"ppx_base" {= "v0.17.0"}
"ppx_cold" {= "v0.17.0"}
"ppx_compare" {= "v0.17.0"}
"ppx_derivers" {= "1.2.1"}
"ppx_deriving" {= "6.0.2"}
"ppx_deriving_yojson" {= "3.8.0"}
"ppx_enumerate" {= "v0.17.0"}
"ppx_expect" {= "v0.17.0"}
"ppx_globalize" {= "v0.17.0"}
"ppx_hash" {= "v0.17.0"}
"ppx_here" {= "v0.17.0"}
"ppx_inline_test" {= "v0.17.0"}
"ppx_optcomp" {= "v0.17.0"}
"ppx_sexp_conv" {= "v0.17.0"}
"ppxlib" {= "0.32.1"}
"ppxlib_jane" {= "v0.17.0"}
"re" {= "1.11.0"}
"react" {= "1.2.2"}
"result" {= "1.5"}
"seq" {= "base"}
"sexplib" {= "v0.17.0"}
"sexplib0" {= "v0.17.0"}
"sha" {= "1.15.4"}
"simple_smt" {= "~dev"}
"sqlite3" {= "5.0.2"}
"stdio" {= "v0.17.0"}
"stdlib-shims" {= "0.3.0"}
"time_now" {= "v0.17.0"}
"topkg" {= "1.0.7"}
"uuidm" {= "0.9.8"}
"visitors" {= "20210608"}
"yojson" {= "2.2.2"}
"zarith" {= "1.14"}
]
build: [
["dune" "subst"] {dev}
[
"dune"
"build"
"-p"
name
"-j"
jobs
"@install"
"@runtest" {with-test}
"@doc" {with-doc}
]
]
pin-depends: [
[
"cerberus.b9daa22"
"git+https://github.com/rems-project/cerberus.git#b9daa22"
]
[
"cerberus-lib.b9daa22"
"git+https://github.com/rems-project/cerberus.git#b9daa22"
]
["cn.b9daa22" "git+https://github.com/rems-project/cerberus.git#b9daa22"]
[
"gillian.c6802c5"
"git+https://github.com/GillianPlatform/Gillian.git#c6802c5"
]
[
"simple_smt.~dev"
"git+https://github.com/NatKarmios/simple-smt-ocaml#b88c4b0685f6ec989e8b4c911e296c4087768db8"
]
]
22 changes: 22 additions & 0 deletions cn-dap.opam.template
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
pin-depends: [
[
"cerberus.b9daa22"
"git+https://github.com/rems-project/cerberus.git#b9daa22"
]
[
"cerberus-lib.b9daa22"
"git+https://github.com/rems-project/cerberus.git#b9daa22"
]
[
"cn.b9daa22"
"git+https://github.com/rems-project/cerberus.git#b9daa22"
]
[
"gillian.c6802c5"
"git+https://github.com/GillianPlatform/Gillian.git#c6802c5"
]
[
"simple_smt.~dev"
"git+https://github.com/NatKarmios/simple-smt-ocaml#b88c4b0685f6ec989e8b4c911e296c4087768db8"
]
]
5 changes: 5 additions & 0 deletions cn-dap/bin/dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,5 @@
(executable
(public_name cn-debug)
(name main)
(package cn-dap)
(libraries cndap logs))
31 changes: 31 additions & 0 deletions cn-dap/bin/main.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
open Cndap

let log_setup (log_path : string option) : unit =
let log_file = Option.value log_path ~default:"/tmp/cn-debug-log.txt" in
let log_channel = Out_channel.open_text log_file in
let formatter = Format.formatter_of_out_channel log_channel in
let reporter = Logs.format_reporter ~app:formatter ~dst:formatter () in
let () = Logs.set_level (Some Logs.Debug) in
let () = Logs.set_reporter reporter in
()
;;

type options = { log_path : string option }

let parse_arguments () : options =
let log_file_ref : string option ref = ref None in
let populate r s = r := Some s in
let usage = String.concat " " [ "Usage: cn-debug"; "--log <log-file>" ] in
let arglist = [ "--log", Arg.String (populate log_file_ref), "Path to log file" ] in
let handle_positional _ = () in
let () = Arg.parse arglist handle_positional usage in
{ log_path = !log_file_ref }
;;

let main () : unit =
let options = parse_arguments () in
log_setup options.log_path;
Adapter.run_stdio ()
;;

let () = main ()
Loading
Loading