Allow command line interface to exhaustively evaluate the next step, printing the events.

Note: this commit switches back to a standard lem build located in ~/bitbucket/lem/lem

3 files changed, 53 insertions, 3 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index a2d59943..9c706828 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -150,5 +150,25 @@ let rec ie_loop mode i_state =
      end ;;
   
 let interp_exhaustive i_state = 
-  let mode = <| Interp.eager_eval = true; Interp.track_values = false |>in
+  let mode = make_mode true false in
   ie_loop mode i_state
+
+let rec rr_ie_loop mode i_state = 
+  match (interp mode i_state) with
+    | Done -> ([],Done)
+    | Error msg -> ([E_error msg], Error msg)
+    | Read_reg reg i_state_fun -> ([], Read_reg reg i_state_fun)
+    | Write_reg reg value i_state->
+      let (events,outcome) = (rr_ie_loop mode i_state) in
+      (((E_write_reg reg value)::events), outcome)
+    | Read_mem read_k loc length tracking i_state_fun ->
+      let (events,outcome) = (rr_ie_loop mode (i_state_fun Unknown)) in 
+      (((E_read_mem read_k loc length tracking)::events),outcome)
+    | Write_mem write_k loc length l_track value v_track i_state_fun ->
+      let (events,outcome) = (rr_ie_loop mode (i_state_fun true)) in
+      (((E_write_mem write_k loc length l_track value v_track)::events),outcome)
+    | Internal _ next -> (rr_ie_loop mode next)
+     end ;;
+
+let rr_interp_exhaustive mode i_state events = 
+  let (events',outcome) = rr_ie_loop mode i_state in ((events ++ events'),outcome)
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 5d461b52..17ef81a9 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -246,6 +246,30 @@ let increment bytes =
 ;;
 let unit_lit = (L_aux(L_unit,Interp_ast.Unknown))
 
+let rec format_events = function
+  | [] -> 
+    "     Done\n"
+  | [E_error s] -> 
+    "     Failed with message : " ^ s ^ "\n"
+  | (E_error s)::events ->
+    "     Failed with message : " ^ s ^ " but continued on erroneously\n"
+  | (E_read_mem(read_kind, location, length, dep))::events ->
+    "     Read_mem at " ^ (val_to_string location) ^ " for " ^ (string_of_big_int length) ^ " bytes \n" ^
+    (format_events events)
+  | (E_write_mem(write_kind,location, length, dep, value, vdep))::events ->
+    "     Write_mem at " ^ (val_to_string location) ^ " writing " ^ (val_to_string value) ^ " across " ^ (string_of_big_int length) ^ " bytes\n" ^
+    (format_events events)
+  | ((E_barrier b_kind)::events) ->
+    "     Memory_barrier occurred\n" ^ 
+    (format_events events)
+  | (E_read_reg reg_name)::events ->
+    "     Read_reg of " ^ (reg_name_to_string reg_name) ^ "\n" ^
+    (format_events events)
+  | (E_write_reg(reg_name, value))::events ->
+    "     Write_reg of " ^ (reg_name_to_string reg_name) ^ " writing " ^ (val_to_string value) ^ "\n" ^
+    (format_events events)
+;;
+
 let rec perform_action ((reg, mem) as env) = function
  (* registers *)
  | Read_reg0((Reg0 id), _) -> (Some(Reg.find id reg), env)
@@ -324,6 +348,7 @@ let run
     cont    print continuation of the top stack frame
     reg     print content of environment
     mem     print content of memory
+    exh     run interpreter exhaustively with unknown and print events 
     quit    exit interpreter" in
   let rec interact mode ((reg, mem) as env) stack =
     flush_all();
@@ -333,7 +358,7 @@ let run
     | "s" | "step" -> Step
     | "n" | "next" -> Next
     | "r" | "run" -> Run
-    | "e" | "reg" | "registers" ->
+    | "rg" | "reg" | "registers" ->
         Reg.iter (fun k v -> debugf "%s\n" (Reg.to_string k v)) reg;
         interact mode env stack
     | "m" | "mem" | "memory" ->
@@ -342,6 +367,11 @@ let run
     | "bt" | "backtrace" | "stack" ->
         List.iter print_exp (compact_stack stack);
         interact mode env stack
+    | "e" | "exh" | "exhaust" ->
+      debugf "interpreting exhaustively from current state\n";
+      let events = interp_exhaustive stack in
+      debugf "%s" (format_events events);
+      interact mode env stack
     | "c" | "cont" | "continuation" ->
         (* print not-compacted continuation *)
         print_exp (top_frame_exp stack);
diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml
index 3d140828..5ba172cb 100644
--- a/src/myocamlbuild.ml
+++ b/src/myocamlbuild.ml
@@ -16,7 +16,7 @@ let split ch s =
   go s
 
 (* paths relative to _build *)
-let lem_dir = "../../../../bitbucket-lem-for-sail/lem" ;;
+let lem_dir = "../../../lem" ;;
 let lem_libdir = lem_dir / "ocaml-lib/_build" ;;
 let lem_lib = lem_libdir / "extract" ;;
 let lem = lem_dir / "lem" ;;