Complete tainting phase 1

Now when mode.track_values is true, on every register read, the returned value is tainted with the register it came from. This tracking is followed through every operation the interperter touches (except library functions, to be completed next).
One a memory operation involving a tracked value, there is optionally list of registers that value arose from in the memory request (i.e. maybe (list reg_name)).

2 files changed, 54 insertions, 27 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 08aa04a7..14745763 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -5,7 +5,7 @@ open import Interp_interface
 open import Pervasives
 
 val intern_value : value -> Interp.value
-val extern_value : bool -> Interp.value -> value
+val extern_value : interp_mode -> bool -> Interp.value -> (value * maybe (list reg_name))
 val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name
 
 let build_context defs = Interp.to_top_env defs
@@ -28,20 +28,27 @@ let intern_value v = match v with
   | Unknown -> Interp.V_unknown
 end
 
-let extern_value for_mem v = match v with
-  | Interp.V_vector _ true bits ->
-    if for_mem 
-    then Bytevector (to_bytes (from_bits bits))
-    else Bitvector (from_bits bits)
-  | _ -> Unknown
-end
-
 let extern_reg r slice = match (r,slice) with
   | (Interp.Reg (Id_aux (Id x) _) _,Nothing) -> Reg x
   | (Interp.Reg (Id_aux (Id x) _) _,Just(i1,i2)) -> Reg_slice x (i1,i2)
   | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> Reg_field x y (i,i)
 end
 
+let extern_value mode for_mem v = match v with
+  | Interp.V_vector _ true bits ->
+    if for_mem 
+    then (Bytevector (to_bytes (from_bits bits)), Nothing)
+    else (Bitvector (from_bits bits), Nothing)
+  | Interp.V_track (Interp.V_vector _ true bits) regs ->
+    if for_mem
+    then (Bytevector (to_bytes (from_bits bits)), 
+          if (mode.Interp.track_values) 
+          then (Just (List.map (fun r -> extern_reg r Nothing) regs))
+          else Nothing)
+    else (Bitvector (from_bits bits), Nothing)
+  | _ -> (Unknown,Nothing)
+end
+
 let initial_instruction_state top_level main arg = 
   let (e_arg,env) = Interp.to_exp <| Interp.eager_eval = true; Interp.track_values = false |> Interp.eenv (intern_value arg) in
   Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [e_arg]) (Interp_ast.Unknown, Nothing)) top_level Interp.eenv Interp.emem
@@ -50,13 +57,14 @@ let initial_instruction_state top_level main arg =
 let external_functions = 
   Interp_lib.function_map
 
-type mem_function = (string * (maybe read_kind * maybe write_kind * Interp.value -> value))
+type mem_function = (string * 
+                     (maybe read_kind * maybe write_kind * (interp_mode -> Interp.value -> (value * (maybe (list reg_name))))))
 
 (*List of memory functions; needs to be expanded with all of the memory functions needed for PPCMem.
   Should probably be expanded into a parameter to mode as with above
 *)
 let memory_functions =
-  [ ("MEM", (Just(Interp.Read_plain), Just(Interp.Write_plain), (fun v -> extern_value true v)));
+  [ ("MEM", (Just(Interp.Read_plain), Just(Interp.Write_plain), (fun mode v -> extern_value mode true v)));
   ]
 
 let rec interp_to_outcome mode thunk = 
@@ -65,16 +73,27 @@ let rec interp_to_outcome mode thunk =
   | Interp.Error l msg -> Error msg (*Todo, add the l information the string format*)
   | Interp.Action a next_state ->
     match a with
-    | Interp.Read_reg reg_form slice -> Read_reg (extern_reg reg_form slice) (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
-    | Interp.Write_reg reg_form slice value -> Write_reg (extern_reg reg_form slice) (extern_value false value) next_state
+    | Interp.Read_reg reg_form slice -> 
+      Read_reg (extern_reg reg_form slice) 
+               (fun v -> 
+                 let v = (intern_value v) in
+                 let v = if mode.Interp.track_values then (Interp.V_track v [reg_form]) else v in 
+                 Interp.add_answer_to_stack next_state v)
+    | Interp.Write_reg reg_form slice value -> 
+      let (v,_) = extern_value mode false value in Write_reg (extern_reg reg_form slice) v next_state
     | Interp.Read_mem (Id_aux (Id i) _) value slice ->
       match List.lookup i memory_functions with
-      | (Just (Just read_k,_,f)) -> Read_mem read_k (f value) (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
+      | (Just (Just read_k,_,f)) -> 
+        let (location, tracking) = (f mode value) in
+        Read_mem read_k location tracking (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
       | _ -> Error ("Memory " ^ i ^ " function with read kind not found")
       end
     | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val ->
       match List.lookup i memory_functions with
-      | (Just (_,Just write_k,f)) -> Write_mem write_k (f loc_val) (extern_value true write_val) (fun b -> next_state) 
+      | (Just (_,Just write_k,f)) -> 
+        let (location, tracking) = (f mode loc_val) in
+        let (value, val_tracking) = (extern_value mode true write_val) in
+        Write_mem write_k location tracking value val_tracking (fun b -> next_state) 
       | _ -> Error ("Memory " ^ i ^ " function with write kind not found")
       end 
     | Interp.Barrier (Id_aux (Id i) _) lval ->
@@ -86,7 +105,7 @@ let rec interp_to_outcome mode thunk =
       match List.lookup i external_functions with
       | Nothing -> Error ("External function not available " ^ i)
       | Just f  -> interp_to_outcome mode (fun _ -> Interp.resume mode next_state (Just (f value))) end
-    | Interp.Step l _ _ -> Internal next_state
+    | Interp.Step l _ _ -> Internal (fun _ -> "Function state to string not implemented yet") next_state 
     end 
   end 
 
@@ -100,11 +119,11 @@ let rec ie_loop mode i_state =
       (E_read_reg reg)::(ie_loop mode (i_state_fun Unknown))
     | Write_reg reg value i_state->
       (E_write_reg reg value)::(ie_loop mode i_state)
-    | Read_mem read_k loc i_state_fun ->
-      (E_read_mem read_k loc)::(ie_loop mode (i_state_fun Unknown))
-    | Write_mem write_k loc value i_state_fun ->
-      (E_write_mem write_k loc value)::(ie_loop mode (i_state_fun true))
-    | Internal next -> (ie_loop mode next)
+    | Read_mem read_k loc tracking i_state_fun ->
+      (E_read_mem read_k loc tracking)::(ie_loop mode (i_state_fun Unknown))
+    | Write_mem write_k loc l_track value v_track i_state_fun ->
+      (E_write_mem write_k loc l_track value v_track)::(ie_loop mode (i_state_fun true))
+    | Internal _ next -> (ie_loop mode next)
      end ;;
   
 let interp_exhaustive i_state = 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index f74a70db..a1ddef88 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -1,4 +1,5 @@
 import Interp
+open import Pervasives
 open import Num
 
 type read_kind = Interp.read_kind
@@ -24,19 +25,26 @@ type reg_name =
 | Reg_f_slice of string * string * slice * slice (* Same as above but only accessing second slice of the field *)
 
 type outcome =
-| Read_mem of read_kind * value * (value -> instruction_state)
-| Write_mem of write_kind * value * value * (bool -> instruction_state)
+(* Request to read memory, value is location to read followed by registers that location depended on when mode.track_values *)
+| Read_mem of read_kind * value * maybe (list reg_name) *  (value -> instruction_state)
+(* Request to write memory, first value and dependent registers is location, second is the value to write *)
+| Write_mem of write_kind * value * maybe (list reg_name) * value * maybe (list reg_name) * (bool -> instruction_state)
+(* Request a memory barrier *)
 | Barrier of barrier_kind * instruction_state
+(* Request to read register, will track dependency when mode.track_values *)
 | Read_reg of reg_name * (value -> instruction_state) 
+(* Request to write register *)
 | Write_reg of reg_name * value * instruction_state
+(* List of instruciton states to be run in parrallel, any order permitted *)
 | Nondet_choice of list instruction_state * instruction_state
-| Internal of instruction_state
+(* Stop for incremental stepping, function can be used to display function call data *)
+| Internal of (unit -> string) * instruction_state
 | Done
 | Error of string
 
 type event = 
-| E_read_mem of read_kind * value
-| E_write_mem of write_kind * value * value
+| E_read_mem of read_kind * value * maybe (list reg_name) 
+| E_write_mem of write_kind * value * maybe (list reg_name) * value * maybe (list reg_name)
 | E_barrier of barrier_kind
 | E_read_reg of reg_name
 | E_write_reg of reg_name * value
@@ -47,7 +55,7 @@ type event =
 val build_context : Interp_ast.defs Interp.tannot -> context
 val initial_instruction_state : context -> string -> value -> instruction_state
 
-type interp_mode = <| eager_eval : bool |>
+type interp_mode = Interp.interp_mode 
 val interp : interp_mode -> instruction_state -> outcome
 
 val interp_exhaustive : instruction_state -> list event