Add ability to track register dependencies in interactive stepper; thus testing register tracking/tainting

2 files changed, 19 insertions, 14 deletions

diff --git a/src/test/power.sail b/src/test/power.sail
index ade9bf7c..fd2a87fc 100644
--- a/src/test/power.sail
+++ b/src/test/power.sail
@@ -9,6 +9,8 @@ function bit carry_out ( x ) = bitzero
 function nat length ( x ) = 64
 (* XXX Storage control *)
 function forall Type 'a . 'a real_addr ( x ) = x
+(* XXX For stvxl and lvxl - what does that do? *)
+function forall Type 'a . unit mark_as_not_likely_to_be_needed_again_anytime_soon ( x ) = ()
 
 (* XXX *)
 val extern forall Nat 'k, Nat 'r,
@@ -297,10 +299,14 @@ val extern forall Nat 'n, Nat 'm. bit['n] -> bit['m] effect pure EXTZ
 val forall Nat 'n, Nat 'm, 'm <= 'n. (bit['n], [|'m|]) -> bit['m] effect pure Chop
 function forall Nat 'm. (bit['m]) Chop(x, y) = x[0..y]
 
-val forall Nat 'n, Nat 'm, 'n <= 0, 0 <= 'm.
-  (nat, [|'n|], [|'m|]) -> [|'n:'m|] effect { wreg } Clamp
+val forall Nat 'n, Nat 'm, Nat 'p, Nat 'q, Nat 'k, 'n <= 0, 0 <= 'm,
+  'n + 2** 'p = 0, 'm = 2** 'q, 'k = 'p + 'q.
+  (nat, [|'n|], [|'m|]) -> bit['k] effect { wreg } Clamp
 
-function forall Nat 'n, Nat 'm, 'n <= 0, 0 <= 'm. ([|'n:'m|])
+(*
+(*TODO: This is not the right type, Clamp needs the implicit additional parameter *)
+function forall Nat 'n, Nat 'm, Nat 'p, Nat 'q, Nat 'k, 'n <= 0, 0 <= 'm,
+  'n + 2** 'p = 0, 'm = 2** 'q, 'k = 'p + 'q. (bit['k])
 Clamp((nat) x, ([|'n|]) y, ([|'m|]) z) = {
   ([|'n:'m|]) result := 0;
   if (x<y) then {
@@ -312,8 +318,8 @@ Clamp((nat) x, ([|'n|]) y, ([|'m|]) z) = {
   } else {
     result := x;
   };
-  result;
-}
+  (bit['k]) result;
+}*)
 
 (* XXX *)
 val extern bit[32] -> bit[32] effect pure RoundToSPIntCeil
@@ -340,6 +346,7 @@ val extern forall Nat 'n. ( bit[64] , [|'n|] ) -> (bit[8 * 'n]) effect { rmem }
 val extern unit -> unit effect pure trap
 
 register (bool) mode64bit
+register (bool) bigendianmode
 
 scattered function unit execute
 scattered typedef ast = const union
@@ -445,8 +452,6 @@ end execute
 end ast
 
 
-(*register ast instr (* monitor decoded instructions *)*)
-
 (* fetch-decode-execute *)
 function unit fde () = {
   NIA := CIA + 4;
diff --git a/src/test/run_power.ml b/src/test/run_power.ml
index 3c58ebfa..9afd692b 100644
--- a/src/test/run_power.ml
+++ b/src/test/run_power.ml
@@ -112,16 +112,16 @@ let eq_zero = function
   | Bitvector(bools,_,_) -> List.for_all (not) bools
 ;;
 
-let rec fde_loop count main_func parameters mem reg ?mode prog =
+let rec fde_loop count main_func parameters mem reg ?mode track_dependencies prog =
   debugf "\n**** instruction %d  ****\n" count;
-  match Run_interp_model.run ~main_func ~parameters ~mem ~reg ~eager_eval:!eager_eval ?mode prog with
-  | false, _, _ -> eprintf "FAILURE\n"; exit 1
-  | true, mode, (reg, mem) ->
+  match Run_interp_model.run ~main_func ~parameters ~mem ~reg ~eager_eval:!eager_eval ~track_dependencies:(ref track_dependencies) ?mode prog with
+  | false, _,_, _ -> eprintf "FAILURE\n"; exit 1
+  | true, mode, track_dependencies, (reg, mem) ->
       if eq_zero (get_reg reg "CIA") then
         eprintf "\nSUCCESS: returned with value %s\n"
           (Run_interp_model.val_to_string (get_reg reg "GPR3"))
       else
-        fde_loop (count+1) main_func parameters mem reg ~mode:mode prog
+        fde_loop (count+1) main_func parameters mem reg ~mode:mode track_dependencies prog
 ;;
 
 let run () =
@@ -143,9 +143,9 @@ let run () =
   let reg = init_reg () in
   (* entry point: unit -> unit fde *)
   let funk_name = "fde" in
-  let args = [] in
+  let parms = [] in
   let name = Filename.basename !file in
-  let t =time_it (fun () -> fde_loop 0 funk_name args !mem reg (name, Power.defs)) () in
+  let t =time_it (fun () -> fde_loop 0 funk_name parms !mem reg false (name, Power.defs)) () in
   eprintf "Execution time: %f seconds\n" t
 ;;