Transition debugger to SEDAP

.github/workflows/ci.yml

@@ -29,7 +29,7 @@ jobs:
       - uses: actions/setup-python@v4
         with:
           python-version: "3.10"
-      - uses: ocaml/setup-ocaml@v2
+      - uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: "ocaml-variants.5.2.0+options"
       - name: Installing Python prerequisites
@@ -91,7 +91,7 @@ jobs:
         uses: cda-tum/setup-z3@v1
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-      - uses: ocaml/setup-ocaml@v2
+      - uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: "ocaml-variants.5.2.0+options"
       - name: Checkout project
@@ -129,7 +129,7 @@ jobs:
         uses: cda-tum/setup-z3@v1
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-      - uses: ocaml/setup-ocaml@v2
+      - uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: "ocaml-variants.5.2.0+options"
       - name: Checkout project
@@ -167,11 +167,14 @@ jobs:
         uses: cda-tum/setup-z3@v1
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-      - uses: ocaml/setup-ocaml@v2
+      - uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: "ocaml-variants.5.2.0+options"
       - name: install CBMC
-        run: sudo apt install cbmc -y
+        run: |
+          curl -L -o cbmc.deb https://github.com/diffblue/cbmc/releases/download/cbmc-5.14.3/cbmc-5.14.3-Linux.deb
+          sudo dpkg -i cbmc.deb
+          rm cbmc.deb
       - name: Checkout project
         uses: actions/checkout@v3
         with:
@@ -205,7 +208,7 @@ jobs:
         uses: cda-tum/setup-z3@v1
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-      - uses: ocaml/setup-ocaml@v2
+      - uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: "ocaml-variants.5.2.0+options"
       - name: Checkout project
@@ -239,7 +242,7 @@ jobs:
         uses: cda-tum/setup-z3@v1
         env:
           GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-      - uses: ocaml/setup-ocaml@v2
+      - uses: ocaml/setup-ocaml@v3
         with:
           ocaml-compiler: "ocaml-variants.5.2.0+options"
       - name: checkout project
@@ -274,7 +277,7 @@ jobs:
   #       uses: cda-tum/setup-z3@v1
   #       env:
   #         GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-  #     - uses: ocaml/setup-ocaml@v2
+  #     - uses: ocaml/setup-ocaml@v3
   #       with:
   #         ocaml-compiler: "ocaml-variants.5.2.0+options"
   #     - name: Checkout project

.vscodeignore

@@ -0,0 +1,3 @@
+_dist
+_docs
+_opam

Gillian-C2/lib/lifter/c2_lifter.ml

@@ -57,7 +57,7 @@ struct
     id : id;
     all_ids : id list;
     display : string;
-    matches : matching list;
+    matches : Match_map.matching list;
     errors : string list;
     submap : id submap;
     prev : (id * Branch_case.t option) option;
@@ -99,7 +99,7 @@ struct
           (** All the paths that haven't been explored yet; a stack means depth-first exploration. *)
       ends : partial_end Ext_list.t;
           (** All the end points; there may be multiple if the cmd branches. *)
-      matches : matching Ext_list.t;
+      matches : Match_map.matching Ext_list.t;
           (** Unifications contained in this command *)
       errors : string Ext_list.t;  (** Errors occurring during this command *)
       mutable canonical_data : canonical_cmd_data option;
@@ -115,7 +115,7 @@ struct
       id : id;
       all_ids : id list;
       display : string;
-      matches : Exec_map.matching list;
+      matches : Match_map.matching list;
       errors : string list;
       next_kind : (Branch_case.t, branch_data) next_kind;
       callers : id list;
@@ -553,6 +553,31 @@ struct
   }
   [@@deriving to_yojson]
 
+  let package_case case =
+    let json = Branch_case.to_yojson case in
+    let display = Branch_case.display case in
+    (json, display)
+
+  let package_data { id; all_ids; display; matches; errors; submap; _ } =
+    Packaged.{ id; all_ids; display; matches; errors; submap }
+
+  let package_node { data : cmd_data; next } =
+    let data = package_data data in
+    let next =
+      match next with
+      | None -> None
+      | Some (Single (next, _)) -> Some (Single (next, ""))
+      | Some (Branch nexts) ->
+          let nexts =
+            nexts
+            |> List.map (fun (case, (next, _)) ->
+                   let case, bdata = package_case case in
+                   (case, (next, bdata)))
+          in
+          Some (Branch nexts)
+    in
+    { data; next }
+
   module Insert_new_cmd = struct
     let failwith ~state ~finished_partial msg =
       DL.failwith
@@ -587,11 +612,19 @@ struct
                     pp_id caller_id
             in
             match new_next with
-            | Ok next -> ({ node with next }, Ok ())
+            | Ok next ->
+                let node = { node with next } in
+                (node, Ok node)
             | Error e -> (node, Error e))
       in
       match result with
-      | Some r -> r
+      | Some r ->
+          let++ new_node = r in
+          let () =
+            Effect.perform
+              (Node_updated (caller_id, Some (package_node new_node)))
+          in
+          ()
       | None ->
           Fmt.error "update_caller_branches - caller %a not found" pp_id
             caller_id
@@ -661,43 +694,58 @@ struct
       { data; next }
 
     let insert_as_next ~state ~prev_id ?case new_id =
-      map_node_extra_exn state.map prev_id (fun prev ->
-          let new_next =
-            let** next =
-              match prev.next with
-              | Some next -> Ok next
-              | None -> Error "trying to insert next of final cmd!"
+      let++ new_prev =
+        map_node_extra_exn state.map prev_id (fun prev ->
+            let new_next =
+              let** next =
+                match prev.next with
+                | Some next -> Ok next
+                | None -> Error "trying to insert next of final cmd!"
+              in
+              match (next, case) with
+              | Single _, Some _ ->
+                  Error "trying to insert to non-branch cmd with branch"
+              | Branch _, None ->
+                  Error "trying to insert to branch cmd with no branch"
+              | Single (Some _, _), _ -> Error "duplicate insertion"
+              | Single (None, bdata), None ->
+                  Ok (Some (Single (Some new_id, bdata)))
+              | Branch nexts, Some case -> (
+                  match List.assoc_opt case nexts with
+                  | None -> Error "case not found"
+                  | Some (Some _, _) -> Error "duplicate insertion"
+                  | Some (None, bdata) ->
+                      let nexts =
+                        List_utils.assoc_replace case (Some new_id, bdata) nexts
+                      in
+                      Ok (Some (Branch nexts)))
             in
-            match (next, case) with
-            | Single _, Some _ ->
-                Error "trying to insert to non-branch cmd with branch"
-            | Branch _, None ->
-                Error "trying to insert to branch cmd with no branch"
-            | Single (Some _, _), _ -> Error "duplicate insertion"
-            | Single (None, bdata), None ->
-                Ok (Some (Single (Some new_id, bdata)))
-            | Branch nexts, Some case -> (
-                match List.assoc_opt case nexts with
-                | None -> Error "case not found"
-                | Some (Some _, _) -> Error "duplicate insertion"
-                | Some (None, bdata) ->
-                    let nexts =
-                      List_utils.assoc_replace case (Some new_id, bdata) nexts
-                    in
-                    Ok (Some (Branch nexts)))
-          in
-          match new_next with
-          | Ok next -> ({ prev with next }, Ok ())
-          | Error e ->
-              (prev, Fmt.error "insert_as_next (%a) - %s" pp_id prev_id e))
+            match new_next with
+            | Ok next ->
+                let prev = { prev with next } in
+                (prev, Ok prev)
+            | Error e ->
+                (prev, Fmt.error "insert_as_next (%a) - %s" pp_id prev_id e))
+      in
+      let () =
+        Effect.perform (Node_updated (prev_id, Some (package_node new_prev)))
+      in
+      ()
 
     let insert_as_submap ~state ~parent_id new_id =
-      map_node_extra_exn state.map parent_id (fun parent ->
-          match parent.data.submap with
-          | Proc _ | Submap _ -> (parent, Error "duplicate submaps!")
-          | NoSubmap ->
-              let data = { parent.data with submap = Submap new_id } in
-              ({ parent with data }, Ok ()))
+      let++ parent =
+        map_node_extra_exn state.map parent_id (fun parent ->
+            match parent.data.submap with
+            | Proc _ | Submap _ -> (parent, Error "duplicate submaps!")
+            | NoSubmap ->
+                let data = { parent.data with submap = Submap new_id } in
+                let parent = { parent with data } in
+                (parent, Ok parent))
+      in
+      let () =
+        Effect.perform (Node_updated (parent_id, Some (package_node parent)))
+      in
+      ()
 
     let insert_to_empty_map ~state ~prev ~stack_direction new_cmd =
       let- () =
@@ -753,6 +801,9 @@ struct
         let new_cmd = make_new_cmd ~func_return_label finished_partial in
         let** new_cmd = insert_cmd ~state ~prev ~stack_direction new_cmd in
         let () = insert state.map ~id ~all_ids new_cmd in
+        let () =
+          Effect.perform (Node_updated (id, Some (package_node new_cmd)))
+        in
         Ok new_cmd
       in
       Result_utils.or_else (failwith ~state ~finished_partial) r
@@ -821,36 +872,6 @@ struct
     init_or_handle ~state ~prev_id ?gil_case exec_data
 
   let dump = to_yojson
-  let get_gil_map _ = failwith "get_gil_map: not implemented!"
-
-  let package_case case =
-    let json = Branch_case.to_yojson case in
-    let display = Branch_case.display case in
-    (json, display)
-
-  let package_data { id; all_ids; display; matches; errors; submap; _ } =
-    Packaged.{ id; all_ids; display; matches; errors; submap }
-
-  let package_node { data : cmd_data; next } =
-    let data = package_data data in
-    let next =
-      match next with
-      | None -> None
-      | Some (Single (next, _)) -> Some (Single (next, ""))
-      | Some (Branch nexts) ->
-          let nexts =
-            nexts
-            |> List.map (fun (case, (next, _)) ->
-                   let case, bdata = package_case case in
-                   (case, (next, bdata)))
-          in
-          Some (Branch nexts)
-    in
-    { data; next }
-
-  let package = Packaged.package Fun.id package_node
-  let get_lifted_map_exn { map; _ } = package map
-  let get_lifted_map state = Some (get_lifted_map_exn state)
   let get_matches_at_id id { map; _ } = (get_exn map id).data.matches
   let path_of_id id { gil_state; _ } = Gil_lifter.path_of_id id gil_state
 

Gillian.code-workspace

@@ -0,0 +1,49 @@
+{
+	"folders": [
+		{
+			"name": "Gillian Core",
+			"path": "GillianCore"
+		},
+		{
+			"name": "WISL",
+			"path": "wisl"
+		},
+		{
+			"name": "Gillian-C",
+			"path": "Gillian-C"
+		},
+		{
+			"name": "Gillian-JS",
+			"path": "Gillian-JS"
+		},
+		{
+			"name": "Gillian-C2",
+			"path": "Gillian-C2"
+		},
+		{
+			"name": "Gillian (root)",
+			"path": "."
+		}
+	],
+	"settings": {
+		"files.associations": {
+			"stdlib.h": "c",
+			"stdio.h": "c",
+			"slist.h": "c",
+			"algorithm": "c",
+			"__bit_reference": "cpp",
+			"__string": "cpp",
+			"cstring": "cpp",
+			"tuple": "c",
+			"string.h": "c",
+			"random": "c",
+			"ranges": "c",
+			"base.h": "c"
+		},
+		"ocaml.sandbox": {
+			"kind": "opam",
+			"switch": "${workspaceFolder:Gillian (root)}"
+		},
+		"typescript.tsc.autoDetect": "off"
+	}
+}

GillianCore/debugging/adapter/breakpoints.ml

@@ -1,4 +1,4 @@
-open Debug_protocol_ext
+open Protocol
 
 (**/**)
 
@@ -7,7 +7,7 @@ module DL = Debugger_log
 (**/**)
 
 module Make (Debugger : Debugger.S) = struct
-  let run dbg rpc =
+  let run { dbg; rpc; _ } =
     Lwt.pause ();%lwt
     DL.set_rpc_command_handler rpc ~name:"Set breakpoints"
       (module Set_breakpoints_command)