Use set instead of list for tainted values

2 files changed, 16 insertions, 14 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index d0899674..ef5743bf 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -56,7 +56,7 @@ type value =
  | V_unknown (* Distinct from undefined, used by memory system *)
  | V_register of reg_form (* Value to store register access, when not actively reading or writing *)
  | V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *)
- | V_track of value * (list reg_form) (* Used when memory system wants to track what register(s) a value came from *)
+ | V_track of value * (set reg_form) (* Used when memory system wants to track what register(s) a value came from *)
 
 let rec {ocaml} string_of_reg_form r = match r with
   | Reg id _ _ -> get_id id
@@ -431,16 +431,15 @@ let list_nth l n = List_extra.nth l n
 val list_length : forall 'a . list 'a -> integer
 let list_length l = integerFromNat (List.length l)
 
-val taint: value -> list reg_form -> value
+val taint: value -> set reg_form -> value
 let rec taint value regs = 
-  match regs with
-    | [] -> value
-    | _ ->
-      match value with 
-	| V_track value rs -> taint value (regs ++ rs)
-	| V_tuple vals -> V_tuple (List.map (fun v -> taint v regs) vals)
-	| _ -> V_track value regs
-end end
+  if Set.null regs
+  then value
+  else match value with 
+    | V_track value rs -> taint value (regs union rs)
+    | V_tuple vals -> V_tuple (List.map (fun v -> taint v regs) vals)
+    | _ -> V_track value regs
+end
 
 val retaint: value -> value -> value
 let retaint orig updated =
@@ -459,7 +458,7 @@ end
 (* the inner lambda is to make Isabelle happier about overlapping patterns *)
 let rec binary_taint thunk = fun vall valr ->
  match (vall,valr) with
-   | (V_track vl rl,V_track vr rr) -> taint (binary_taint thunk vl vr) (rl++rr)
+   | (V_track vl rl,V_track vr rr) -> taint (binary_taint thunk vl vr) (rl union rr)
    | (V_track vl rl,vr) -> taint (binary_taint thunk vl vr) rl
    | (vl,V_track vr rr) -> taint (binary_taint thunk vl vr) rr
    | (vl,vr) -> thunk vl vr
@@ -1367,7 +1366,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 				  | (V_track _ rs, V_lit _) -> to_exp mode env (taint (V_lit diff) rs)
 				  | (V_lit _, V_track _ rs) -> to_exp mode env (taint (V_lit diff) rs)
 				  | (V_track _ r1, V_track _ r2) -> 
-				    (to_exp mode env (taint (V_lit diff) (r1 ++ r2))) end in
+				    (to_exp mode env (taint (V_lit diff) (r1 union r2))) end in
 				let  e = 
 				  (E_aux (E_block 
 					    [(E_aux 
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index ba762162..ccf21c4e 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -1,6 +1,7 @@
 import Interp
 import Interp_lib
 import Instruction_extractor
+import Set_extra
 open import Interp_ast
 open import Interp_interface
 open import Pervasives
@@ -191,7 +192,9 @@ let rec extern_mem_value mode v = match v with
   | Interp.V_track v regs -> 
     let (external_v,_) = extern_mem_value mode v in
     (external_v,
-     if mode.internal_mode.Interp.track_values then (Just (List.map (fun r -> extern_reg r Nothing) regs)) else Nothing)
+     if mode.internal_mode.Interp.track_values 
+     then (Just (List.map (fun r -> extern_reg r Nothing) (Set_extra.toList regs)))
+     else Nothing)
   | Interp.V_vector fst inc bits -> 
     let bytes = to_bytes (bitls_from_ibits bits) in 
     if mode.endian = E_big_endian 
@@ -437,7 +440,7 @@ let rec interp_to_outcome mode context thunk =
       Read_reg (extern_reg reg_form slice) 
                (fun v -> 
                  let v = (intern_reg_value v) in
-                 let v = if mode.internal_mode.Interp.track_values then (Interp.V_track v [reg_form]) else v in 
+                 let v = if mode.internal_mode.Interp.track_values then (Interp.V_track v (Set.fromList [reg_form])) else v in 
                  IState (Interp.add_answer_to_stack next_state v) context)
     | Interp.Write_reg reg_form slice value ->
       let reg_name = extern_reg reg_form slice in