From 91c8ff746f968c2204016d135cb769082a9f01e6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 16 Nov 2016 12:37:18 -0800 Subject: [PATCH] feat(cli_debugger): add commands for traversing stack frames --- library/init/meta/vm.lean | 36 ++++----- src/library/tactic/vm_monitor.cpp | 122 ++++++++++++++++++++---------- src/library/vm/vm.cpp | 3 + src/library/vm/vm.h | 5 ++ tmp/cli_debugger.lean | 104 ++++++++++++++++++++----- 5 files changed, 194 insertions(+), 76 deletions(-) diff --git a/library/init/meta/vm.lean b/library/init/meta/vm.lean index bb1f41c4f6..8cc5760bed 100644 --- a/library/init/meta/vm.lean +++ b/library/init/meta/vm.lean @@ -58,23 +58,25 @@ meta instance : monad vm_core := @[reducible] meta def vm (A : Type) : Type := optionT.{1 1} vm_core A namespace vm -meta constant get_env : vm environment -meta constant get_decl : name → vm vm_decl -meta constant get_options : vm options -meta constant stack_size : vm nat -meta constant stack_obj : nat → vm vm_obj -meta constant stack_obj_info : nat → vm (name × option expr) -meta constant format_stack_obj : nat → vm format -meta constant call_stack_size : vm nat -meta constant call_stack_fn : nat → vm name -meta constant curr_fn : vm name -meta constant bp : vm nat -meta constant pc : vm nat -meta constant obj_to_string : vm_obj → vm string -meta constant put_str : string → vm unit -meta constant get_line : vm string -meta constant eof : vm bool -meta constant get_attribute : name → vm (list name) +meta constant get_env : vm environment +meta constant get_decl : name → vm vm_decl +meta constant get_options : vm options +meta constant stack_size : vm nat +meta constant stack_obj : nat → vm vm_obj +meta constant stack_obj_info : nat → vm (name × option expr) +meta constant pp_stack_obj : nat → vm format +meta constant pp_expr : expr → vm format +meta constant call_stack_size : vm nat +meta constant call_stack_fn : nat → vm name +meta constant call_stack_var_range : nat → vm (nat × nat) +meta constant curr_fn : vm name +meta constant bp : vm nat +meta constant pc : vm nat +meta constant obj_to_string : vm_obj → vm string +meta constant put_str : string → vm unit +meta constant get_line : vm string +meta constant eof : vm bool +meta constant get_attribute : name → vm (list name) meta def trace {A : Type} [has_to_format A] (a : A) : vm unit := do fmt ← return $ to_fmt a, diff --git a/src/library/tactic/vm_monitor.cpp b/src/library/tactic/vm_monitor.cpp index 133ba8c61c..fdbe97f51d 100644 --- a/src/library/tactic/vm_monitor.cpp +++ b/src/library/tactic/vm_monitor.cpp @@ -302,7 +302,7 @@ static format default_format(vm_state const & vm, unsigned idx) { return format(out.str()); } -vm_obj vm_format_stack_obj(vm_obj const & i, vm_obj const & /*s*/) { +vm_obj vm_pp_stack_obj(vm_obj const & i, vm_obj const & /*s*/) { auto const & vm = get_vm_state_being_debugged(); unsigned idx = force_to_unsigned(i, std::numeric_limits::max()); if (idx >= vm.stack_size()) return mk_vm_failure(); @@ -339,6 +339,30 @@ vm_obj vm_call_stack_fn(vm_obj const & i, vm_obj const & /*s*/) { return mk_vm_success(to_obj(vm.call_stack_fn(idx))); } +vm_obj vm_call_stack_var_range(vm_obj const & i, vm_obj const & /*s*/) { + auto const & vm = get_vm_state_being_debugged(); + unsigned idx = force_to_unsigned(i, std::numeric_limits::max()); + unsigned csz = vm.call_stack_size(); + if (idx >= csz) { + return mk_vm_failure(); + } else { + lean_assert(csz > 0); + unsigned start, end; + if (idx == csz - 1) { + start = vm.bp(); + end = vm.stack_size(); + } else if (idx == csz - 2) { + start = vm.call_stack_bp(csz - 1); + end = vm.bp(); + } else { + lean_assert(idx < csz - 2); + start = vm.call_stack_bp(idx + 1); + end = vm.call_stack_bp(idx + 2); + } + return mk_vm_success(mk_vm_pair(mk_vm_nat(start), mk_vm_nat(end))); + } +} + vm_obj vm_bp(vm_obj const & /*s*/) { return mk_vm_success(mk_vm_nat(get_vm_state_being_debugged().bp())); } @@ -396,47 +420,63 @@ vm_obj vm_get_attribute(vm_obj const & vm_n, vm_obj const &) { } } +vm_obj vm_pp_expr(vm_obj const & e, vm_obj const &) { + auto const & vm = get_vm_state_being_debugged(); + formatter_factory const & fmtf = get_global_ios().get_formatter_factory(); + type_context ctx(vm.env()); + formatter fmt = fmtf(vm.env(), vm.get_options(), ctx); + try { + return mk_vm_success(to_obj(fmt(to_expr(e)))); + } catch (exception &) { + std::ostringstream out; + out << to_expr(e); + return mk_vm_success(to_obj(format(out.str()))); + } +} + void initialize_vm_monitor() { - DECLARE_VM_BUILTIN(name({"vm_monitor", "register"}), _vm_monitor_register); - DECLARE_VM_BUILTIN(name({"vm_core", "map"}), vm_core_map); - DECLARE_VM_BUILTIN(name({"vm_core", "ret"}), vm_core_ret); - DECLARE_VM_BUILTIN(name({"vm_core", "bind"}), vm_core_bind); - DECLARE_VM_BUILTIN(name({"vm_obj", "kind"}), _vm_obj_kind); - DECLARE_VM_BUILTIN(name({"vm_obj", "cidx"}), vm_obj_cidx); - DECLARE_VM_BUILTIN(name({"vm_obj", "fn_idx"}), vm_obj_fn_idx); - DECLARE_VM_BUILTIN(name({"vm_obj", "fields"}), vm_obj_fields); - DECLARE_VM_BUILTIN(name({"vm_obj", "to_nat"}), vm_obj_to_nat); - DECLARE_VM_BUILTIN(name({"vm_obj", "to_name"}), vm_obj_to_name); - DECLARE_VM_BUILTIN(name({"vm_obj", "to_level"}), vm_obj_to_level); - DECLARE_VM_BUILTIN(name({"vm_obj", "to_expr"}), vm_obj_to_expr); - DECLARE_VM_BUILTIN(name({"vm_obj", "to_declaration"}), vm_obj_to_declaration); - DECLARE_VM_BUILTIN(name({"vm_obj", "to_environment"}), vm_obj_to_environment); - DECLARE_VM_BUILTIN(name({"vm_obj", "to_tactic_state"}), vm_obj_to_tactic_state); - DECLARE_VM_BUILTIN(name({"vm_obj", "to_format"}), vm_obj_to_format); - DECLARE_VM_BUILTIN(name({"vm_decl", "kind"}), _vm_decl_kind); - DECLARE_VM_BUILTIN(name({"vm_decl", "to_name"}), vm_decl_to_name); - DECLARE_VM_BUILTIN(name({"vm_decl", "idx"}), vm_decl_idx); - DECLARE_VM_BUILTIN(name({"vm_decl", "arity"}), vm_decl_arity); - DECLARE_VM_BUILTIN(name({"vm_decl", "pos"}), vm_decl_pos); - DECLARE_VM_BUILTIN(name({"vm_decl", "olean"}), vm_decl_olean); - DECLARE_VM_BUILTIN(name({"vm_decl", "args_info"}), vm_decl_args_info); - DECLARE_VM_BUILTIN(name({"vm", "get_env"}), vm_get_env); - DECLARE_VM_BUILTIN(name({"vm", "get_decl"}), vm_get_decl); - DECLARE_VM_BUILTIN(name({"vm", "stack_size"}), vm_stack_size); - DECLARE_VM_BUILTIN(name({"vm", "stack_obj"}), vm_stack_obj); - DECLARE_VM_BUILTIN(name({"vm", "stack_obj_info"}), vm_stack_obj_info); - DECLARE_VM_BUILTIN(name({"vm", "call_stack_size"}), vm_call_stack_size); - DECLARE_VM_BUILTIN(name({"vm", "call_stack_fn"}), vm_call_stack_fn); - DECLARE_VM_BUILTIN(name({"vm", "bp"}), vm_bp); - DECLARE_VM_BUILTIN(name({"vm", "pc"}), vm_pc); - DECLARE_VM_BUILTIN(name({"vm", "curr_fn"}), vm_curr_fn); - DECLARE_VM_BUILTIN(name({"vm", "get_options"}), vm_get_options); - DECLARE_VM_BUILTIN(name({"vm", "obj_to_string"}), vm_obj_to_string); - DECLARE_VM_BUILTIN(name({"vm", "format_stack_obj"}), vm_format_stack_obj); - DECLARE_VM_BUILTIN(name({"vm", "put_str"}), vm_put_str); - DECLARE_VM_BUILTIN(name({"vm", "get_line"}), vm_get_line); - DECLARE_VM_BUILTIN(name({"vm", "eof"}), vm_eof); - DECLARE_VM_BUILTIN(name({"vm", "get_attribute"}), vm_get_attribute); + DECLARE_VM_BUILTIN(name({"vm_monitor", "register"}), _vm_monitor_register); + DECLARE_VM_BUILTIN(name({"vm_core", "map"}), vm_core_map); + DECLARE_VM_BUILTIN(name({"vm_core", "ret"}), vm_core_ret); + DECLARE_VM_BUILTIN(name({"vm_core", "bind"}), vm_core_bind); + DECLARE_VM_BUILTIN(name({"vm_obj", "kind"}), _vm_obj_kind); + DECLARE_VM_BUILTIN(name({"vm_obj", "cidx"}), vm_obj_cidx); + DECLARE_VM_BUILTIN(name({"vm_obj", "fn_idx"}), vm_obj_fn_idx); + DECLARE_VM_BUILTIN(name({"vm_obj", "fields"}), vm_obj_fields); + DECLARE_VM_BUILTIN(name({"vm_obj", "to_nat"}), vm_obj_to_nat); + DECLARE_VM_BUILTIN(name({"vm_obj", "to_name"}), vm_obj_to_name); + DECLARE_VM_BUILTIN(name({"vm_obj", "to_level"}), vm_obj_to_level); + DECLARE_VM_BUILTIN(name({"vm_obj", "to_expr"}), vm_obj_to_expr); + DECLARE_VM_BUILTIN(name({"vm_obj", "to_declaration"}), vm_obj_to_declaration); + DECLARE_VM_BUILTIN(name({"vm_obj", "to_environment"}), vm_obj_to_environment); + DECLARE_VM_BUILTIN(name({"vm_obj", "to_tactic_state"}), vm_obj_to_tactic_state); + DECLARE_VM_BUILTIN(name({"vm_obj", "to_format"}), vm_obj_to_format); + DECLARE_VM_BUILTIN(name({"vm_decl", "kind"}), _vm_decl_kind); + DECLARE_VM_BUILTIN(name({"vm_decl", "to_name"}), vm_decl_to_name); + DECLARE_VM_BUILTIN(name({"vm_decl", "idx"}), vm_decl_idx); + DECLARE_VM_BUILTIN(name({"vm_decl", "arity"}), vm_decl_arity); + DECLARE_VM_BUILTIN(name({"vm_decl", "pos"}), vm_decl_pos); + DECLARE_VM_BUILTIN(name({"vm_decl", "olean"}), vm_decl_olean); + DECLARE_VM_BUILTIN(name({"vm_decl", "args_info"}), vm_decl_args_info); + DECLARE_VM_BUILTIN(name({"vm", "get_env"}), vm_get_env); + DECLARE_VM_BUILTIN(name({"vm", "get_decl"}), vm_get_decl); + DECLARE_VM_BUILTIN(name({"vm", "stack_size"}), vm_stack_size); + DECLARE_VM_BUILTIN(name({"vm", "stack_obj"}), vm_stack_obj); + DECLARE_VM_BUILTIN(name({"vm", "stack_obj_info"}), vm_stack_obj_info); + DECLARE_VM_BUILTIN(name({"vm", "call_stack_size"}), vm_call_stack_size); + DECLARE_VM_BUILTIN(name({"vm", "call_stack_fn"}), vm_call_stack_fn); + DECLARE_VM_BUILTIN(name({"vm", "call_stack_var_range"}), vm_call_stack_var_range); + DECLARE_VM_BUILTIN(name({"vm", "bp"}), vm_bp); + DECLARE_VM_BUILTIN(name({"vm", "pc"}), vm_pc); + DECLARE_VM_BUILTIN(name({"vm", "curr_fn"}), vm_curr_fn); + DECLARE_VM_BUILTIN(name({"vm", "get_options"}), vm_get_options); + DECLARE_VM_BUILTIN(name({"vm", "obj_to_string"}), vm_obj_to_string); + DECLARE_VM_BUILTIN(name({"vm", "pp_stack_obj"}), vm_pp_stack_obj); + DECLARE_VM_BUILTIN(name({"vm", "pp_expr"}), vm_pp_expr); + DECLARE_VM_BUILTIN(name({"vm", "put_str"}), vm_put_str); + DECLARE_VM_BUILTIN(name({"vm", "get_line"}), vm_get_line); + DECLARE_VM_BUILTIN(name({"vm", "eof"}), vm_eof); + DECLARE_VM_BUILTIN(name({"vm", "get_attribute"}), vm_get_attribute); } void finalize_vm_monitor() { diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index a823357bf6..ba8f56fc75 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -2655,6 +2655,9 @@ void initialize_vm() { #endif g_debugger = new name{"debugger"}; register_bool_option(*g_debugger, false, "(debugger) debug code using VM monitors"); + /* TODO(Leo): move to .lean after we add primitives for creating new options on .lean files */ + register_bool_option(name({"debugger", "autorun"}), false, + "(debugger) skip debugger startup messages and initial prompt"); } void finalize_vm() { diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index 18d3e4567b..04216e60cf 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -624,6 +624,11 @@ public: return m_decl_map.find(m_call_stack[idx].m_curr_fn_idx)->get_name(); } + unsigned call_stack_bp(unsigned idx) const { + lean_assert(idx < m_call_stack.size()); + return m_call_stack[idx].m_bp; + } + unsigned bp() const { return m_bp; } unsigned pc() const { return m_pc; } diff --git a/tmp/cli_debugger.lean b/tmp/cli_debugger.lean index f655e22878..27249bab43 100644 --- a/tmp/cli_debugger.lean +++ b/tmp/cli_debugger.lean @@ -49,7 +49,7 @@ do { return n } <|> -return "" +return "[current file]" meta def pos_info (fn : name) : vm string := do { @@ -61,11 +61,14 @@ do { <|> return "" +meta def display_fn (header : string) (fn : name) (frame : nat) : vm unit := +do pos ← pos_info fn, + vm.put_str ("[" ++ frame^.to_string ++ "] " ++ header ++ " " ++ fn^.to_string ++ " at " ++ pos ++ "\n") + meta def display_curr_fn (header : string) : vm unit := do fn ← vm.curr_fn, - pos ← pos_info fn, sz ← vm.call_stack_size, - vm.put_str ("[" ++ sz^.to_string ++ "] " ++ header ++ " " ++ fn^.to_string ++ " at " ++ pos ++ "\n") + display_fn header fn (sz-1) meta def display_help : vm unit := do @@ -73,6 +76,10 @@ do vm.put_str "help - display this message\n", vm.put_str "run - continue execution\n", vm.put_str "step - execute until another function in on the top of the stack\n", + vm.put_str "stack trace\n", + vm.put_str " up - move up in the stack trace\n", + vm.put_str " down - move down in the stack trace\n", + vm.put_str " vars - display variables in the current stack frame\n", vm.put_str "breakpoints\n", vm.put_str " break fn - add breakpoint for fn\n", vm.put_str " rbreak fn - remove breakpoint\n", @@ -118,8 +125,58 @@ meta def show_breakpoints : list name → vm unit vm.put_str "\n", show_breakpoints fns -meta def cmd_loop : state → list string → vm state -| s default_cmd := do +meta def show_frame (frame : nat) : vm unit := +do sz ← vm.call_stack_size, + fn ← if frame >= sz then vm.curr_fn else vm.call_stack_fn frame, + display_fn "frame" fn frame + +meta def up (frame : nat) : vm nat := +if frame = 0 then return 0 +else show_frame (frame - 1) >> return (frame - 1) + +meta def down (frame : nat) : vm nat := +do sz ← vm.call_stack_size, + if frame >= sz - 1 then return frame + else show_frame (frame + 1) >> return (frame + 1) + +meta def type_to_string : option expr → nat → vm string +| none i := do + o ← vm.stack_obj i, + match o^.kind with + | vm_obj_kind.simple := return "[tagged value]" + | vm_obj_kind.constructor := return "[constructor]" + | vm_obj_kind.closure := return "[closure]" + | vm_obj_kind.mpz := return "[big num]" + | vm_obj_kind.name := return "name" + | vm_obj_kind.level := return "level" + | vm_obj_kind.expr := return "expr" + | vm_obj_kind.declaration := return "declaration" + | vm_obj_kind.environment := return "environment" + | vm_obj_kind.tactic_state := return "tactic_state" + | vm_obj_kind.format := return "format" + | vm_obj_kind.options := return "options" + | vm_obj_kind.other := return "[other]" + end +| (some type) i := do + fmt ← vm.pp_expr type, + opts ← vm.get_options, + return (fmt^.to_string opts) + +meta def show_vars_core : nat → nat → nat → vm unit +| c i e := + if i = e then return () + else do + (n, type) ← vm.stack_obj_info i, + type_str ← type_to_string type i, + vm.put_str $ "#" ++ c^.to_string ++ " " ++ n^.to_string ++ " : " ++ type_str ++ "\n", + show_vars_core (c+1) (i+1) e + +meta def show_vars (frame : nat) : vm unit := +do (s, e) ← vm.call_stack_var_range frame, + show_vars_core 0 s e + +meta def cmd_loop_core : state → nat → list string → vm state +| s frame default_cmd := do is_eof ← vm.eof, if is_eof then do vm.put_str "stopping debugger... 'end of file' has been found\n", @@ -130,21 +187,28 @@ meta def cmd_loop : state → list string → vm state tks ← return $ split l, tks ← return $ if tks = [] then default_cmd else tks, match tks with - | [] := cmd_loop s default_cmd + | [] := cmd_loop_core s frame default_cmd | (cmd::args) := - if cmd = "help" then display_help >> cmd_loop s default_cmd + if cmd = "help" then display_help >> cmd_loop_core s frame default_cmd else if cmd = "exit" then return {s with md := mode.done } else if cmd = "run" ∨ cmd = "r" then return {s with md := mode.run } else if cmd = "step" ∨ cmd = "s" then return {s with md := mode.step } - else if cmd = "break" ∨ cmd = "b" then do new_s ← add_breakpoint s args, cmd_loop new_s default_cmd - else if cmd = "rbreak" then do new_s ← remove_breakpoint s args, cmd_loop new_s default_cmd + else if cmd = "break" ∨ cmd = "b" then do new_s ← add_breakpoint s args, cmd_loop_core new_s frame default_cmd + else if cmd = "rbreak" then do new_s ← remove_breakpoint s args, cmd_loop_core new_s frame default_cmd else if cmd = "bs" then do vm.put_str "breakpoints\n", show_breakpoints s^.fn_bps, - cmd_loop s default_cmd - else do vm.put_str "unknown command, type 'help' for help\n", cmd_loop s default_cmd + cmd_loop_core s frame default_cmd + else if cmd = "up" ∨ cmd = "u" then do frame ← up frame, cmd_loop_core s frame ["u"] + else if cmd = "down" ∨ cmd = "d" then do frame ← down frame, cmd_loop_core s frame ["d"] + else if cmd = "vars" ∨ cmd = "v" then do show_vars frame, cmd_loop_core s frame ["vars"] + else do vm.put_str "unknown command, type 'help' for help\n", cmd_loop_core s frame default_cmd end +meta def cmd_loop (s : state) (default_cmd : list string) : vm state := +do csz ← vm.call_stack_size, + cmd_loop_core s (csz - 1) default_cmd + def prune_active_bps_core (csz : nat) : list (nat × name) → list (nat × name) | [] := [] | ((csz', n)::ls) := if csz < csz' then prune_active_bps_core ls else ((csz',n)::ls) @@ -163,10 +227,13 @@ do opts ← vm.get_options, else do bps ← vm.get_attribute `breakpoint, new_s ← return {s with fn_bps := bps}, - vm.put_str "Lean debugger\n", - display_curr_fn "debugging", - vm.put_str "type 'help' for help\n", - cmd_loop new_s [] + if opts^.get_bool `debugger.autorun ff then + return {new_s with md := mode.run} + else do + vm.put_str "Lean debugger\n", + display_curr_fn "debugging", + vm.put_str "type 'help' for help\n", + cmd_loop new_s [] meta def step_transition (s : state) : vm state := do @@ -219,12 +286,13 @@ run_command vm_monitor.register `debugger.monitor run_command attribute.register `debugger.attr set_option debugger true +set_option debugger.autorun true -def g (a : nat) := a + 1 +def g (c : nat) := c + 1 -def h (a : nat) := g a + 1 +def h (a : nat) (b : nat) := g b + a -def s (a : nat) := h a + h a +def s (a : nat) := h 2 a + h 3 a local attribute [breakpoint] h