Skip to content

Commit

Permalink
Fix some debug bugs, organise debugging examples (#279)
Browse files Browse the repository at this point in the history
* Clean up debugger workspace

* Fix ConfError report IDs

* Debug: Fix end-of-branch detection

* Reorganise WISL debug exampels

* Fix end-of-loop detection in WISL lifter
  • Loading branch information
NatKarmios authored Mar 20, 2024
1 parent 3efef67 commit adb44df
Show file tree
Hide file tree
Showing 60 changed files with 903 additions and 6,238 deletions.
31 changes: 6 additions & 25 deletions GillianCore/debugging/debugger/base_debugger.ml
Original file line number Diff line number Diff line change
Expand Up @@ -496,30 +496,11 @@ struct

(* A command step with no results *should* mean that we're returning.
If we're at the top of the callstack, this *should* mean that we're hitting the end of the program. *)
let is_eob ~content ~type_ ~id =
let is_root =
match
content |> Yojson.Safe.from_string |> ConfigReport.of_yojson
with
| Error _ ->
DL.log (fun m ->
m
"Handle_continue.is_eob: Not a ConfigReport (type %s); I'm \
not sure what to do here."
type_);
true
| Ok report -> (
match report.callstack with
| [] -> failwith "HORROR: Empty callstack!"
| [ _ ] -> true
| _ -> false)
in
if is_root then
L.Log_queryer.get_cmd_results id
|> List.for_all (fun (_, content) ->
let result = content |> of_yojson_string CmdResult.of_yojson in
result.errors <> [])
else false
let is_eob ~id =
L.Log_queryer.get_cmd_results id
|> List.for_all (fun (_, content) ->
let result = content |> of_yojson_string CmdResult.of_yojson in
result.errors <> [])

type continue_kind = ProcInit | EoB | Continue

Expand All @@ -529,7 +510,7 @@ struct
if type_ = Content_type.proc_init then (
DL.log (fun m -> m "Debugger.%s: Skipping proc_init..." log_context);
ProcInit)
else if is_eob ~content ~type_ ~id then (
else if is_eob ~id then (
DL.log (fun m ->
m
"Debugger.%s: No non-error results for %a; stepping again \
Expand Down
5 changes: 2 additions & 3 deletions GillianCore/engine/general_semantics/general/g_interpreter.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1739,7 +1739,6 @@ struct
| _, (_, LAction _) -> simplify state
| _ -> [ state ]
in
let prev_cmd_report_id = !report_id_ref in
List.concat_map
(fun state ->
try
Expand All @@ -1755,7 +1754,7 @@ struct
error_state;
errors;
branch_path = List_utils.cons_opt branch_case branch_path;
prev_cmd_report_id;
prev_cmd_report_id = !report_id_ref;
};
]
| State.Internal_State_Error (errs, error_state) ->
Expand All @@ -1768,7 +1767,7 @@ struct
error_state;
errors = List.map (fun x -> Exec_err.EState x) errs;
branch_path = List_utils.cons_opt branch_case branch_path;
prev_cmd_report_id;
prev_cmd_report_id = !report_id_ref;
};
])
states
Expand Down
64 changes: 0 additions & 64 deletions debugger-vscode-extension/sampleWorkspace/js/DLL.js

This file was deleted.

Loading

0 comments on commit adb44df

Please sign in to comment.