summaryrefslogtreecommitdiff
path: root/src/test
diff options
context:
space:
mode:
authorGabriel Kerneis2014-04-04 11:14:25 +0100
committerGabriel Kerneis2014-04-04 11:14:25 +0100
commit78703f987512fbc90ccccea4b813f24fe0ccd49a (patch)
treedbfbf4fb49793db6d495cb1098b7b25b113fb948 /src/test
parent6211671cf52fb51aafe46438ba408d3e3e009734 (diff)
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.
Diffstat (limited to 'src/test')
-rw-r--r--src/test/power.sail31
-rw-r--r--src/test/run_power.ml40
-rw-r--r--src/test/run_tests.ml2
3 files changed, 40 insertions, 33 deletions
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