Improve interaction after chat with Peter

- remember mode (run, step or next) between instructions
- display continuation by default in step mode
- start in step mode by default
- incompatible change: the shorthand for stack is now bt (=backtrace),
  since s becomes the shorthand for step
- incompatible change: pressing enter now repeats the current mode,
  instead of "step"

3 files changed, 28 insertions, 14 deletions

diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index d7f42c3d..dfee73b0 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -263,6 +263,7 @@ let run
   ?(reg=Reg.empty)
   ?(mem=Mem.empty)
   ?(eager_eval=true)
+  ?mode
   (name, test) =
   let get_loc (E_aux(_, (l, _))) = loc_to_string l in
   let print_exp  e =
@@ -309,12 +310,19 @@ let run
     end
   in
   let rec loop mode env = function
-  | Value (v, _) -> debugf "%s: return %s\n" name (val_to_string v); true, env
+  | Value (v, _) ->
+      debugf "%s: return %s\n" name (val_to_string v);
+      true, mode, env
   | Action (a, s) ->
       let top_exp = top_frame_exp s in
-      let loc = get_loc top_exp in
+      let loc = get_loc (compact_exp top_exp) in
       let return, env' = perform_action env a in
-      let step () = if mode = Step then interact mode env s else mode in
+      let step ?(force=false) () =
+        if mode = Step || force then begin
+          debugf "%s\n" (Pretty_interp.pp_exp top_exp);
+          interact mode env s
+       end else
+         mode in
       let mode' = begin match a with
       | Read_reg (reg, sub) ->
           debugf "%s: read_reg: %s%s -> %s\n"
@@ -345,20 +353,24 @@ let run
           step ()
       | Debug _ ->
           assert (return = unit_lit);
-          print_exp top_exp;
-          interact mode env' s
+          debugf "%s: breakpoint:\n" loc;
+          step ~force:true ()
       | Barrier (_, _) | Write_next_IA _ | Nondet _ ->
           failwith "unexpected action"
       end in
       loop mode' env' (resume {eager_eval = (mode' = Run)} s (Some return))
-  | Error(l, e) -> debugf "%s: error: %s\n" (loc_to_string l) e; false, env in
+  | Error(l, e) ->
+      debugf "%s: error: %s\n" (loc_to_string l) e;
+      false, mode, env in
   debugf "%s: evaluate %s\n" name (Pretty_interp.pp_exp entry);
+  let mode = match mode with
+  | None -> if eager_eval then Run else Step
+  | Some m -> m in
   try
     Printexc.record_backtrace true;
-    let mode = if eager_eval then Run else Step in
     loop mode (reg, mem) (interp {eager_eval} test entry)
   with e ->
     let trace = Printexc.get_backtrace () in
     debugf "%s: interpretor error %s\n%s\n" name (Printexc.to_string e) trace;
-    false, (reg, mem)
+    false, mode, (reg, mem)
 ;;
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index c47b60d3..ca4dbc97 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -103,16 +103,16 @@ let get_reg reg name =
   |  _ -> assert false
 ;;
 
-let rec fde_loop count entry mem reg prog =
+let rec fde_loop count entry mem reg ?mode prog =
   debugf "\n**** instruction %d  ****\n" count;
-  match Run_interp.run ~entry ~mem ~reg ~eager_eval:!eager_eval prog with
-  | false, _ -> eprintf "FAILURE\n"; exit 1
-  | true, (reg, mem) ->
+  match Run_interp.run ~entry ~mem ~reg ~eager_eval:!eager_eval ?mode prog with
+  | false, _, _ -> eprintf "FAILURE\n"; exit 1
+  | true, mode, (reg, mem) ->
       if Big_int.eq_big_int (get_reg reg "CIA") lr_init_value then
         eprintf "\nSUCCESS: returned with value %s\n"
           (Big_int.string_of_big_int (get_reg reg "GPR3"))
       else
-        fde_loop (count+1) entry mem reg prog
+        fde_loop (count+1) entry mem reg ~mode:mode prog
 ;;
 
 let run () =
diff --git a/src/test/run_tests.ml b/src/test/run_tests.ml
index a8323322..770ed426 100644
--- a/src/test/run_tests.ml
+++ b/src/test/run_tests.ml
@@ -11,7 +11,9 @@ let tests = [
   (*"power", Power.defs;*)
 ] ;;
 
-let run_one ((name, _) as t) = (name, fst(Run_interp.run t))
+let fst3 (x,_,_) = x
+
+let run_one ((name, _) as t) = (name, fst3(Run_interp.run t))
 
 let run_all () =
   let results = List.map run_one tests in