Abstract debugger (+ WPST debugging) (#261)

* Allow CI to be triggered manually

* Fix batteries version, add memtrace

* Add index to SpecExec branch case

* Tweak goto branching and reduction error handling

* Add fresh, assert and assume to WISL, tweak while

* Introduce abstract debugger

* Tweak confcont and formatting

* Tweak ConfCont, remove new_branches

* Simplify LAction branch case

* Ignore branch cases when not debugging

* Update some GIL compilations in sampleWorkspace

* Update debug extension for WPST debugging

* Bump Z3 timeout

* Fix docker build CI

* Simplify branch cases from spec proc calls

* Un-bump Z3 timeout

.github/workflows/ci.yml

@@ -6,6 +6,7 @@ on:
   pull_request:
     branches: [master]
   merge_group:
+  workflow_dispatch:
 
 env:
   NODE_VERSION: 18
@@ -239,6 +240,8 @@ jobs:
         uses: actions/checkout@v3
       - name: set up docker buildx
         uses: docker/setup-buildx-action@v2
+        with:
+          driver: docker
       - name: Restore Cache
         id: restore-cache
         uses: actions/cache@v3
@@ -251,7 +254,6 @@ jobs:
         uses: docker/build-push-action@v4
         with:
           context: .
-          engine: docker
           load: true
           tags: ${{ env.DOCKER_TEST_TAG }}
       - name: test

.gitignore

@@ -94,3 +94,6 @@ javert-test262
 # Built docs
 _docs/odoc
 _docs/sphinx
+
+# Memtraces
+*.ctf

GillianCore/GIL_Syntax/BranchCase.ml

@@ -1,8 +1,8 @@
 type t =
   | GuardedGoto of bool
   | LCmd of int
-  | SpecExec of Flag.t
-  | LAction of Yojson.Safe.t list
+  | SpecExec of Flag.t * int
+  | LAction of int
   | LActionFail of int
 [@@deriving show, yojson]
 

GillianCore/GIL_Syntax/Gil_syntax.mli

@@ -999,8 +999,8 @@ module BranchCase : sig
   type t =
     | GuardedGoto of bool  (** Effectively if/else; either true or false case *)
     | LCmd of int  (** Logical command *)
-    | SpecExec of Flag.t  (** Spec execution *)
-    | LAction of Yojson.Safe.t list  (** Logical action *)
+    | SpecExec of Flag.t * int  (** Spec execution *)
+    | LAction of int  (** Logical action *)
     | LActionFail of int  (** {i Failed} logical action*)
   [@@deriving yojson, show]
 

GillianCore/command_line/command_line.ml

@@ -35,10 +35,16 @@ struct
   module Verification = Verifier.Make (SState) (SPState) (PC) (External)
   module Lifter = Lifter (Verification)
   module Abductor = Abductor.Make (SPState) (PC) (External)
-  module Debugger = Debugger.Make (ID) (PC) (Verification) (Lifter)
-  module Debug_adapter = Debug_adapter.Make (Debugger)
+
+  module Symb_debugger =
+    Debugger.Symbolic_debugger.Make (ID) (PC) (Verification) (Lifter)
+
+  module Verif_debugger =
+    Debugger.Verification_debugger.Make (ID) (PC) (Verification) (Lifter)
 
   let main () =
+    Memtrace.trace_if_requested ();
+
     let doc = "An analysis toolchain" in
 
     let man =
@@ -58,7 +64,12 @@ struct
                   (Gil_parsing));
         (module Verification_console.Make (ID) (PC) (Verification) (Gil_parsing));
         (module Act_console.Make (ID) (PC) (Abductor) (Gil_parsing));
-        (module Debug_verification_console.Make (PC) (Debug_adapter));
+        (module Debug_verification_console.Make
+                  (PC)
+                  (Debug_adapter.Make (Verif_debugger)));
+        (module Debug_wpst_console.Make
+                  (PC)
+                  (Debug_adapter.Make (Symb_debugger)));
         (module Bulk_console.Make (PC) (Runners));
       ]
     in

GillianCore/command_line/debug_verification_console.ml

@@ -21,6 +21,7 @@ module Make (PC : ParserAndCompiler.S) (Debug_adapter : Debug_adapter.S) :
     Cmd.info "debugverify" ~doc ~man
 
   let start_debug_adapter manual () =
+    Config.current_exec_mode := Utils.Exec_mode.Verification;
     Config.manual_proof := manual;
     Lwt_main.run (Debug_adapter.start Lwt_io.stdin Lwt_io.stdout)
 

GillianCore/command_line/debug_wpst_console.ml

@@ -0,0 +1,28 @@
+open Cmdliner
+
+module Make (PC : ParserAndCompiler.S) (Debug_adapter : Debug_adapter.S) :
+  Console.S = struct
+  module Common_args = Common_args.Make (PC)
+
+  let debug_wpst_info =
+    let doc =
+      "Starts Gillian in debugging mode for whole-program symbolic testing"
+    in
+    let man =
+      [
+        `S Manpage.s_description;
+        `P
+          "Starts Gillian in debugging mode for whole-program symbolic \
+           testing, which communicates via the Debug Adapter Protocol";
+      ]
+    in
+    Cmd.info "debugwpst" ~doc ~man
+
+  let start_debug_adapter () =
+    Config.current_exec_mode := Utils.Exec_mode.Symbolic;
+    Lwt_main.run (Debug_adapter.start Lwt_io.stdin Lwt_io.stdout)
+
+  let debug_wpst_t = Common_args.use Term.(const start_debug_adapter)
+  let debug_wpst_cmd = Cmd.v debug_wpst_info debug_wpst_t
+  let cmds = [ debug_wpst_cmd ]
+end

GillianCore/command_line/dune

@@ -11,7 +11,8 @@
   logging
   debugger_lifter
   incrementalAnalysis
-  debug_adapter)
+  debug_adapter
+  memtrace)
  (flags
   :standard
   -open

GillianCore/debugging/adapter/inspect.ml

@@ -73,8 +73,8 @@ module Make (Debugger : Debugger.S) = struct
     DL.set_rpc_command_handler rpc ~name:"Unification"
       (module Unification_command)
       (fun { id } ->
-        let unify_id, unify_map = dbg |> Debugger.Inspect.get_unification id in
-        let result = Unification_command.Result.make ~unify_id ~unify_map in
+        let unify_map = dbg |> Debugger.Inspect.get_unify_map id in
+        let result = Unification_command.Result.make ~unify_id:id ~unify_map in
         Lwt.return result);
     Lwt.return ()
 end