From 78703f987512fbc90ccccea4b813f24fe0ccd49a Mon Sep 17 00:00:00 2001
From: Gabriel Kerneis
Date: Fri, 4 Apr 2014 11:14:25 +0100
Subject: Improve Power execution

- Move FDE loop to the OCaml side of the Power model (avoid leaking
  memory due to lack of TCO in interpreter)
- Display cycle count
- Check the value of CIA at the end of each cycle and stop if it is
  equal to the initial value of LR, returning the value in GPR3.
---
 src/lem_interp/run_interp.ml |  6 +++---
 src/test/power.sail          | 31 ++-----------------------------
 src/test/run_power.ml        | 40 +++++++++++++++++++++++++++++++++++++---
 src/test/run_tests.ml        |  2 +-
 4 files changed, 43 insertions(+), 36 deletions(-)

(limited to 'src')

diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 7100a197..556e61c6 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -208,14 +208,14 @@ let run
   ?(mem=Mem.empty)
   (name, test) =
   let rec loop env = function
-  | Value (v, _) -> eprintf "%s: returned %s\n" name (val_to_string v); true
+  | Value (v, _) -> eprintf "%s: returned %s\n" name (val_to_string v); true, env
   | Action (a, s) ->
       eprintf "%s: suspended on action %s\n" name (act_to_string a);
       (*eprintf "%s: suspended on action %s, with stack %s\n" name (act_to_string a) (stack_to_string s);*)
       let return, env' = perform_action env a in
       eprintf "%s: action returned %s\n" name (val_to_string return);
       loop env' (resume test s return)
-  | Error(l, e) -> eprintf "%s: %s: error: %s\n" name (loc_to_string l) e; false in
+  | Error(l, e) -> eprintf "%s: %s: error: %s\n" name (loc_to_string l) e; false, env in
   eprintf "%s: starting\n" name;
   try
     Printexc.record_backtrace true;
@@ -223,5 +223,5 @@ let run
   with e ->
     let trace = Printexc.get_backtrace () in
     eprintf "%s: interpretor error %s\n%s\n" name (Printexc.to_string e) trace;
-    false
+    false, (reg, mem)
 ;;
diff --git a/src/test/power.sail b/src/test/power.sail
index e75e24ef..9cf49dc3 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -186,37 +186,10 @@ end ast
 
 register ast instr (* monitor decoded instructions *)
 
-(* fetch-decode-execute loop *)
-function rec unit fde_loop () = {
+(* fetch-decode-execute cycle *)
+function unit cycle () = {
   NIA := CIA + 4;
   instr := decode(MEM(CIA, 4));
   execute(instr);
   CIA := NIA;
-  fde_loop ()
-}
-
-function unit init() = {
-  (* CIA is initialiazed externally, as well as MEM *)
-
-  (* initial stack-pointer. stack grows downwards, the first step is to
-  decrement it which should (hopefully) wrap around to the largest
-  possible 64-bit value *)
-  GPR1 := 0;
-  (* initial value of environment pointer - no clue what it is used for,
-     only saved in restore in our simple example. *)
-  GPR31 := 0;
-
-  (* unused in practice, but must be set for bclr computation *)
-  CTR := 0;
-  CR := 0;
-  (* return address -- I have no idea what to put there, let's make an
-  infinite loop! *)
-  LR := CIA;
-
-
-}
-
-function unit main () = {
-  init();
-  fde_loop();
 }
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index 91bb0448..8ad5187e 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -54,9 +54,23 @@ let load_section ic (offset,size,addr) =
   done
 ;;
 
+(* use zero as a sentinel --- it might prevent a minimal loop from
+ * working in principle, but won't happen in practice *)
+let lr_init_value = Big_int.zero_big_int
+
 let init_reg () =
+  let init name value size =
+    (* fix index - this is necessary for CR, indexed from 32 *)
+    let offset (V_vector(_, inc, v)) =
+      V_vector(Big_int.big_int_of_int (64 - size), inc, v) in
+    Id_aux(Id name, Unknown), offset (big_int_to_vec value size) in
   List.fold_left (fun r (k,v) -> Reg.add k v r) Reg.empty [
-    Id_aux(Id "CIA", Unknown), big_int_to_vec (hex_to_big_int !startaddr) 64 ;
+    init "CIA" (hex_to_big_int !startaddr) 64;
+    init "GPR1" Big_int.zero_big_int 64;
+    init "GPR31" Big_int.zero_big_int 64;
+    init "CTR" Big_int.zero_big_int 64;
+    init "CR" Big_int.zero_big_int 32;
+    init "LR" lr_init_value 64;
   ]
 ;;
 
@@ -75,6 +89,24 @@ let time_it action arg =
   finish_time -. start_time
 ;;
 
+let get_reg reg name =
+  let reg_content = Reg.find (Id_aux(Id name, Unknown)) reg in
+  let V_lit(L_aux(L_num n, Unknown)) = to_num true reg_content in
+  n
+;;
+
+let rec fde_loop count entry mem reg prog =
+  eprintf "\n**** cycle %d  ****\n" count;
+  match Run_interp.run ~entry ~mem ~reg prog with
+  | false, _ -> eprintf "FAILURE\n"; exit 1
+  | true, (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
+;;
+
 let run () =
   Arg.parse args (fun _ -> raise (Arg.Bad "anonymous parameter")) "" ;
   if !file = "" then begin
@@ -91,8 +123,10 @@ let run () =
   eprintf "done. (%f seconds)\n%!" t;
   close_in ic;
   let reg = init_reg () in
-  let r = Run_interp.run ~mem:!mem ~reg (!file, Power.defs) in
-  eprintf "%s\n" (if r then "SUCCESS" else "FAILURE")
+  (* entry point: unit -> unit cycle *)
+  let entry = E_aux(E_app(Id_aux((Id "cycle"),Unknown),
+    [E_aux(E_lit (L_aux(L_unit,Unknown)),(Unknown,None))]),(Unknown,None)) in
+  fde_loop 0 entry !mem reg (!file, Power.defs)
 ;;
 
 run () ;;
diff --git a/src/test/run_tests.ml b/src/test/run_tests.ml
index 570c49aa..a8323322 100644
--- a/src/test/run_tests.ml
+++ b/src/test/run_tests.ml
@@ -11,7 +11,7 @@ let tests = [
   (*"power", Power.defs;*)
 ] ;;
 
-let run_one ((name, _) as t) = (name, Run_interp.run t)
+let run_one ((name, _) as t) = (name, fst(Run_interp.run t))
 
 let run_all () =
   let results = List.map run_one tests in
-- 
cgit v1.2.3