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

6 files changed, 125 insertions, 41 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 8265fd5e..a2d59943 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -44,7 +44,7 @@ let extern_value mode for_mem v = match v with
     if for_mem 
     then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, Nothing)
     else (Bitvector (from_bits bits) inc fst, Nothing)
-  | Interp.V_track (Interp.V_vector fst inc bits) regs ->
+  | Interp.V_track (Interp.V_vector fst inc bits) regs -> 
     if for_mem
     then (Bytevector (List.reverse (to_bytes (from_bits bits))) inc fst, 
           if (mode.Interp.track_values) 
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 8d13bcb0..990382ff 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -80,32 +80,45 @@ let bitwise_not_bit v =
     | L_one  -> (V_lit (L_aux L_zero loc)) end in
   match v with
   | V_lit lit -> lit_not lit
+  | V_unknown -> V_unknown
   | V_track (V_lit lit) r -> V_track (lit_not lit) r 
 end;; 
 
 let bitwise_binop_bit op (V_tuple [x; y]) = match (x,y) with
   | (V_track x rx,V_track y ry) ->
-    V_track (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) (rx ++ ry)
+    taint (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) (rx ++ ry)
   | (V_track x rx,y) ->
-    V_track (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) rx
+    taint (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) rx
   | (x,V_track y ry) ->
-    V_track (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) ry
+    taint (bool_to_bit (op (bit_to_bool x) (bit_to_bool y))) ry
+  | (V_unknown,_) -> V_unknown
+  | (_,V_unknown) -> V_unknown
   | _ -> bool_to_bit (op (bit_to_bool x) (bit_to_bool y))
 end ;;
 
-let bitwise_binop op (V_tuple [v1;v2]) =
+let rec bitwise_binop op (V_tuple [v1;v2]) =
   match (v1,v2) with
   | (V_vector idx inc v, V_vector idx' inc' v') ->
   (* typechecker ensures inc = inc', idx = idx' and length v = length v' *)
   let apply (x, y) = bool_to_bit(op (bit_to_bool x) (bit_to_bool y)) in
   V_vector idx inc (List.map apply (List.zip v v'))
+  | (V_track v1 r1, V_track v2 r2) ->
+    taint (bitwise_binop op (V_tuple [v1;v2])) (r1 ++ r2)
+  | (V_track v1 r1,v2) ->
+    taint (bitwise_binop op (V_tuple [v1;v2])) r1
+  | (v1,V_track v2 r2) ->
+    taint (bitwise_binop op (V_tuple [v1;v2])) r2
+  | (V_unknown,_) -> V_unknown
+  | (_,V_unknown) -> V_unknown
 end ;;
 
 (* BitSeq expects LSB first.
  * By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
  * hence MSB first.
  * http://en.wikipedia.org/wiki/Bit_numbering *)
-let to_num signed (V_vector idx inc l) =
+let rec to_num signed v = 
+  match v with
+  | (V_vector idx inc l) ->
   (* Word library in Lem expects bitseq with LSB first *)
 (*TODO: Kathy think more
   We thought a reverse was needed due to above comments only in inc case.
@@ -115,7 +128,10 @@ let to_num signed (V_vector idx inc l) =
   let l = (*if inc then reverse l else l*) reverse l in
   (* Make sure the last bit is a zero to force unsigned numbers *)
   let l = if signed then l else l ++ [V_lit (L_aux L_zero Unknown)] in
-  V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown);;
+  V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown)
+  | V_unknown -> V_unknown
+  | V_track v r -> taint (to_num signed v) r
+end ;;
 
 (*TODO As with above, consider the reverse here in both cases, where we're again always interpreting with the MSB on the left *)
 let to_vec_inc (V_tuple([V_lit(L_aux (L_num len) _); (V_lit(L_aux (L_num n) ln))])) =
@@ -145,31 +161,73 @@ let neg (V_tuple [V_lit (L_aux arg la)]) = V_lit (L_aux (match arg with
 
 let neq = compose neg eq ;;
 
-let arith_op op (V_tuple args) = match args with
+let rec arith_op op (V_tuple args) = match args with
+  | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (op x y)) lx)
+  | [V_track v1 r1;V_track v2 r2] -> taint (arith_op op (V_tuple [v1;v2])) (r1++r2)
+  | [V_track v1 r1;v2] -> taint (arith_op op (V_tuple [v1;v2])) r1
+  | [v1;V_track v2 r2] -> taint (arith_op op (V_tuple [v1;v2])) r2
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
-  | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> V_lit(L_aux (L_num (op x y)) lx)
   end ;;
-let arith_op_vec op (V_tuple args) = match args with
+let rec arith_op_vec op (V_tuple args) = match args with
   | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
     let (l1',l2') = (to_num false l1,to_num false l2) in
     let n = arith_op op (V_tuple [l1';l2']) in
     to_vec ord (List.length cs) n
+  | [V_track v1 r1;V_track v2 r2] ->
+    taint (arith_op_vec op (V_tuple [v1;v2])) (r1++r2)
+  | [V_track v1 r1;v2] ->
+    taint (arith_op_vec op (V_tuple [v1;v2])) r1
+  | [v1;V_track v2 r2] ->
+    taint (arith_op_vec op (V_tuple [v1;v2])) r2
+  | [V_unknown;_] -> V_unknown
+  | [_;V_unknown] -> V_unknown
 end ;;
-let arith_op_range_vec op (V_tuple args) = match args with
+let rec arith_op_range_vec op (V_tuple args) = match args with
+  | [V_track v1 r1;V_track v2 r2] ->
+    taint (arith_op_range_vec op (V_tuple [v1;v2])) (r1++r2)
+  | [V_track v1 r1; v2] ->
+    taint (arith_op_range_vec op (V_tuple [v1;v2])) r1
+  | [v1;V_track v2 r2] -> 
+    taint (arith_op_range_vec op (V_tuple [v1;v2])) r2
+  | [V_unknown;_] -> V_unknown
+  | [_;V_unknown] -> V_unknown
   | [n; (V_vector _ ord cs as l2)] ->
     arith_op_vec op (V_tuple [(to_vec ord (List.length cs) n);l2])
 end ;;
-let arith_op_vec_range op (V_tuple args) = match args with
+let rec arith_op_vec_range op (V_tuple args) = match args with
+  | [V_track v1 r1;V_track v2 r2] ->
+    taint (arith_op_vec_range op (V_tuple [v1;v2])) (r1++r2)
+  | [V_track v1 r1; v2] ->
+    taint (arith_op_vec_range op (V_tuple [v1;v2])) r1
+  | [v1;V_track v2 r2] -> 
+    taint (arith_op_vec_range op (V_tuple [v1;v2])) r2
+  | [V_unknown;_] -> V_unknown
+  | [_;V_unknown] -> V_unknown
   | [(V_vector _ ord cs as l1);n] ->
-  arith_op_vec op (V_tuple [l1;(to_vec ord (List.length cs) n)])
+    arith_op_vec op (V_tuple [l1;(to_vec ord (List.length cs) n)])
 end ;;
-
-let arith_op_range_vec_range op (V_tuple args) = match args with
+let rec arith_op_range_vec_range op (V_tuple args) = match args with
+  | [V_track v1 r1;V_track v2 r2] ->
+    taint (arith_op_range_vec_range op (V_tuple [v1;v2])) (r1++r2)
+  | [V_track v1 r1; v2] ->
+    taint (arith_op_range_vec_range op (V_tuple [v1;v2])) r1
+  | [v1;V_track v2 r2] -> 
+    taint (arith_op_range_vec_range op (V_tuple [v1;v2])) r2
+  | [V_unknown;_] -> V_unknown
+  | [_;V_unknown] -> V_unknown
   | [n;(V_vector _ ord _ as l2)] ->
     arith_op op (V_tuple [n;(to_num ord l2)])
 end ;;
-let arith_op_vec_range_range op (V_tuple args) = match args with
+let rec arith_op_vec_range_range op (V_tuple args) = match args with
+  | [V_track v1 r1;V_track v2 r2] ->
+    taint (arith_op_vec_range_range op (V_tuple [v1;v2])) (r1++r2)
+  | [V_track v1 r1; v2] ->
+    taint (arith_op_vec_range_range op (V_tuple [v1;v2])) r1
+  | [v1;V_track v2 r2] -> 
+    taint (arith_op_vec_range_range op (V_tuple [v1;v2])) r2
+  | [V_unknown;_] -> V_unknown
+  | [_;V_unknown] -> V_unknown
   | [(V_vector _ ord _ as l1);n] ->
     arith_op op (V_tuple [(to_num ord l1);n])
 end ;;
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index 9591b918..5d461b52 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -59,9 +59,12 @@ let val_to_string v = match v with
 
 let reg_name_to_string = function
   | Reg0 s -> s
-  | Reg_slice(s,(first,second)) -> s (*contemplate putting slice here*)
+  | Reg_slice(s,(first,second)) -> 
+    s ^ "[" ^ string_of_big_int first ^ (if (eq_big_int first second) then "" else ".." ^ (string_of_big_int second)) ^ "]"
   | Reg_field(s,f,_) -> s ^ "." ^ f
-  | Reg_f_slice(s,f,_,(first,second)) -> s ^ "." ^ f
+  | Reg_f_slice(s,f,_,(first,second)) -> s ^ "." ^ f ^ "]" ^ string_of_big_int first ^ (if (eq_big_int first second) then "" else ".." ^ (string_of_big_int second)) ^ "]"
+
+let dependencies_to_string dependencies = String.concat ", " (List.map reg_name_to_string dependencies)
 
 let rec val_to_string_internal = function
  | Interp.V_boxref(n, t) -> sprintf "boxref %d" n
@@ -305,6 +308,7 @@ let run
   ?(reg=Reg.empty)
   ?(mem=Mem.empty)
   ?(eager_eval=true)
+  ?(track_dependencies= ref false)
   ?mode
   (name, spec) =
   let get_loc (E_aux(_, (l, _))) = loc_to_string l in
@@ -314,7 +318,8 @@ let run
   let usage = "Usage:
     step    go to next action [default]
     next    go to next break point
-    run     complete current execution,
+    run     complete current execution
+    track   begin/end tracking register dependencies
     bt      print call stack
     cont    print continuation of the top stack frame
     reg     print content of environment
@@ -341,6 +346,9 @@ let run
         (* print not-compacted continuation *)
         print_exp (top_frame_exp stack);
         interact mode env stack
+    | "track" | "t" ->
+      track_dependencies := not(!track_dependencies);
+      interact mode env stack
     | "show_casts" ->
         Pretty_interp.ignore_casts := false;
         interact mode env stack
@@ -357,10 +365,10 @@ let run
   let rec loop mode env = function
   | Done ->
     debugf "%s: %s\n" (grey name) (blue "done");
-    (true, mode, env)
+    (true, mode, !track_dependencies, env)
   | Error0 s -> 
     debugf "%s: %s: %s\n" (grey name) (red "error") s;
-    (false, mode, env) 
+    (false, mode, !track_dependencies, env) 
   | action ->
     let step ?(force=false) stack =
       let top_exp = top_frame_exp stack in
@@ -386,13 +394,25 @@ let run
 	| Read_mem0(kind, location, length, dependencies, next_thunk) ->
 	  (match return with
 	    | Some(value) -> 
-	      (*TODO: show length, conditionally show dependencies *)
 	      show "read_mem" (val_to_string location) right (val_to_string value);
+              (match dependencies with
+              | None -> ()
+              | Some(deps) ->
+                show "read_mem address depended on" (dependencies_to_string deps) "" "");
 	      let next = next_thunk value in
 	      (step next, env', next)
 	    | None -> assert false)
 	| Write_mem0(kind,location, length, dependencies, value, val_dependencies, next_thunk) ->
 	  show "write_mem" (val_to_string location) left (val_to_string value);
+          (match (dependencies,val_dependencies) with
+          | (None,None) -> ();
+          | (Some(deps),None) ->
+            show "write_mem address depended on" (dependencies_to_string deps) "" "";
+          | (None,Some(deps)) ->
+            show "write_mem value depended on" (dependencies_to_string deps) "" "";
+          | (Some(deps),Some(vdeps)) ->
+            show "write_mem address depended on" (dependencies_to_string deps) "" "";
+            show "write_mem value depended on" (dependencies_to_string vdeps) "" "";);
 	  let next = next_thunk true in
 	  (step next,env',next)
 	| Barrier0(bkind,next) ->
@@ -406,21 +426,21 @@ let run
 	  let choose_order = List.sort (fun (_,i1) (_,i2) -> compare i1 i2) 
 	    (List.combine nondets (List.map (fun _ -> Random.bits ()) nondets)) in
 	  show "nondeterministic evaluation begun" "" "" "";
-	  let (_,_,env') = List.fold_right (fun (next,_) (_,_,env') -> 
-	    loop mode env' (interp0 (make_mode (mode=Run) false) next)) choose_order (false,mode,env'); in
+	  let (_,_,_,env') = List.fold_right (fun (next,_) (_,_,_,env') -> 
+	    loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies) next)) choose_order (false,mode,!track_dependencies,env'); in
 	  show "nondeterministic evaluation ended" "" "" "";
 	  (step next,env',next)
 (*      | Exit e ->
 	show "exiting current evaluation" "" "" "";
 	step (),env', (set_in_context s e)*)
       in
-      loop mode' env' (interp0 (make_mode (mode' = Run) false) next) in
+      loop mode' env' (interp0 (make_mode (mode' = Run) !track_dependencies) next) in
   let mode = match mode with
   | None -> if eager_eval then Run else Step
   | Some m -> m in
   let context = build_context spec in
   let initial_state = initial_instruction_state context main_func parameters in
-  let imode = make_mode eager_eval false in
+  let imode = make_mode eager_eval !track_dependencies in
   let top_exp = top_frame_exp initial_state in
   debugf "%s: %s %s\n" (grey name) (blue "evaluate") (Pretty_interp.pp_exp top_exp);
   try
@@ -429,5 +449,5 @@ let run
   with e ->
     let trace = Printexc.get_backtrace () in
     debugf "%s: %s %s\n%s\n" (grey name) (red "interpretor error") (Printexc.to_string e) trace;
-    false, mode, (reg, mem)
+    (false, mode, !track_dependencies, (reg, mem))
 ;;
diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml
index 015aaf0c..3d140828 100644
--- a/src/myocamlbuild.ml
+++ b/src/myocamlbuild.ml
@@ -36,6 +36,7 @@ let lem_opts = [A "-lib"; P "../lem_interp";
                 A "-wl_pat_exh";  P "ign"; 
                 A "-wl_pat_fail"; P "ign";
                 A "-wl_unused_vars";   P "ign";
+(*                A "-suppress_renaming";*)
 ] ;;
 
 dispatch begin function
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
 ;;