Support breakpoints when debugging (#310)

* Fix workspace folder in VSCode JSON files

* Support breakpoints in WISL lifter

* Fix error at end-of-branch in GIL lifter

* Support breakpoints in GIL lifter

* Support breakpoints in Kani lifter

.vscode/launch.json

@@ -6,11 +6,11 @@
 			"type": "extensionHost",
 			"request": "launch",
 			"args": [
-				"--extensionDevelopmentPath=${workspaceFolder}/debugger-vscode-extension",
+				"--extensionDevelopmentPath=${workspaceFolder}/debug-ui",
 				"${workspaceFolder}/debug-ui/examples"
 			],
 			"outFiles": [
-				"${workspaceFolder}/debugger-vscode-extension/out/**/*.js"
+				"${workspaceFolder}/debug-ui/out/**/*.js"
 			]
 		},
 	]

GillianCore/debugging/debugger/base_debugger.ml

@@ -314,15 +314,16 @@ struct
 
     let process_files = Process_files.f
 
-    let has_hit_breakpoint dbg =
-      match dbg.frames with
-      | [] -> false
-      | frame :: _ ->
-          if Hashtbl.mem dbg.breakpoints frame.source_path then
-            let breakpoints = Hashtbl.find dbg.breakpoints frame.source_path in
-            (* Currently only one breakpoint per line is supported *)
-            Breakpoints.mem frame.start_line breakpoints
-          else false
+    (* Currently only one breakpoint per line is supported *)
+    let is_breakpoint ~file ~lines proc =
+      match Hashtbl.find_opt proc.breakpoints file with
+      | None -> false
+      | Some breakpoints ->
+          let rec aux = function
+            | [] -> false
+            | line :: ls -> Breakpoints.mem line breakpoints || aux ls
+          in
+          aux lines
 
     let rec call_stack_to_frames call_stack next_proc_body_idx prog =
       match call_stack with
@@ -613,8 +614,9 @@ struct
         exec_data
 
       let with_lifter_effects f proc_state state =
-        let open Effect.Deep in
+        let open Lift in
         let open Lifter in
+        let open Effect.Deep in
         try_with f ()
           {
             effc =
@@ -626,7 +628,11 @@ struct
                         let step_result =
                           handle_step_effect id case path proc_state state
                         in
-                        Effect.Deep.continue k step_result)
+                        continue k step_result)
+                | IsBreakpoint (file, lines) ->
+                    Some
+                      (fun (k : (a, _) continuation) ->
+                        is_breakpoint ~file ~lines proc_state |> continue k)
                 | _ ->
                     let s = Printexc.to_string (Effect.Unhandled eff) in
                     Fmt.failwith "HORROR: effect leak!\n%s" s);

GillianCore/debugging/lifter/gil_lifter.ml

@@ -1,6 +1,7 @@
 module L = Logging
 module DL = Debugger_log
 open Lifter_intf
+open Syntaxes.Option
 include Gil_lifter_intf
 
 type id = L.Report_id.t [@@deriving yojson]
@@ -27,6 +28,7 @@ functor
       submap : id submap;
       branch_path : branch_path;
       parent : (id * branch_case option) option;
+      loc : (string * int) option;
     }
     [@@deriving to_yojson]
 
@@ -73,8 +75,16 @@ functor
         }
         () =
       let display = Fmt.to_to_string Cmd.pp_indexed cmd_report.cmd in
+      let loc =
+        let annot = cmd_report.annot in
+        let+ loc =
+          Annot.get_origin_loc annot
+          |> Option.map Debugger_utils.location_to_display_location
+        in
+        (loc.loc_source, loc.loc_start.pos_line)
+      in
       let data =
-        { id; display; matches; errors; submap; branch_path; parent }
+        { id; display; matches; errors; submap; branch_path; parent; loc }
       in
       let next =
         match next_kind with
@@ -244,24 +254,22 @@ functor
       Option.get case
 
     let find_next state id case =
-      let next =
-        match (get_exn state.map id).next with
-        | None -> failwith "HORROR - tried to step from FinalCmd!"
-        | Some next -> next
-      in
-      match (next, case) with
-      | Single _, Some _ ->
+      let node = get_exn state.map id in
+      match (node.next, case) with
+      | (None | Some (Single _)), Some _ ->
           failwith "HORROR - tried to step case for non-branch cmd"
-      | Single (None, _), None -> Either.Right None
-      | Single (Some next, _), None -> Either.Left (get_exn state.map next)
-      | Branch nexts, None ->
+      | Some (Single (None, _)), None -> Either.Right None
+      | Some (Single (Some next, _)), None ->
+          Either.Left (get_exn state.map next)
+      | Some (Branch nexts), None ->
           let case = select_case nexts in
           Either.Right (Some case)
-      | Branch nexts, Some case -> (
+      | Some (Branch nexts), Some case -> (
           match List.assoc_opt case nexts with
           | None -> failwith "case not found"
           | Some (None, _) -> Either.Right (Some case)
           | Some (Some next, _) -> Either.Left (get_exn state.map next))
+      | None, None -> Either.Left node
 
     let request_next state id case =
       let path = path_of_id id state in
@@ -305,15 +313,23 @@ functor
       in
       (stop_id, Debugger_utils.Step)
 
+    let is_breakpoint node =
+      match node.data.loc with
+      | None -> false
+      | Some (file, line) -> Effect.perform (IsBreakpoint (file, [ line ]))
+
     let continue state id =
       let open Utils.Syntaxes.Option in
-      let rec aux stack ends =
+      let rec aux ?(first = false) stack ends =
         match stack with
         | [] -> List.rev ends
         | (id, case) :: rest -> (
-            match step state id case with
-            | Either.Left nexts -> aux (nexts @ rest) ends
-            | Either.Right end_id -> aux rest (end_id :: ends))
+            let node = get_exn state.map id in
+            if (not first) && is_breakpoint node then aux rest (id :: ends)
+            else
+              match step state id case with
+              | Either.Left nexts -> aux (nexts @ rest) ends
+              | Either.Right end_id -> aux rest (end_id :: ends))
       in
       let end_ =
         let end_, stack =
@@ -327,15 +343,25 @@ functor
               (None, stack)
         in
         let- () = end_ in
-        let ends = aux stack [] in
+        let ends = aux ~first:true stack [] in
         List.hd ends
       in
       (end_, Debugger_utils.Step)
 
     let step_out = continue
 
     (* TODO: breakpoints *)
-    let continue_back t _ = (Option.get t.map.root, Debugger_utils.Step)
+    let continue_back t id =
+      let rec aux id = function
+        | None -> (id, Debugger_utils.Step)
+        | Some (id, _) ->
+            let node = get_exn t.map id in
+            if is_breakpoint node then (id, Breakpoint)
+            else aux id node.data.parent
+      in
+      let node = get_exn t.map id in
+      aux id node.data.parent
+    (* (Option.get t.map.root, Debugger_utils.Step) *)
 
     let init_manual proc_name all_procs =
       let map = Exec_map.make () in

GillianCore/debugging/lifter/lifter_intf.ml

@@ -24,6 +24,8 @@ module Types = struct
     | Stop of Logging.Report_id.t option
     | ExecNext of (Logging.Report_id.t option * Branch_case.t option)
   [@@deriving yojson]
+
+  type _ Effect.t += IsBreakpoint : (string * int list) -> bool Effect.t
 end
 
 include Types