diff options
Diffstat (limited to 'src/test')
| -rw-r--r-- | src/test/power.sail | 31 | ||||
| -rw-r--r-- | src/test/run_power.ml | 40 | ||||
| -rw-r--r-- | src/test/run_tests.ml | 2 |
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 |
