Abstract tainting to almost always use taint, detaint, retaint, and binary_taint functions instead of V_track directly.

Annoyingly, Lem won't let one section of code use these functions, complaining of too much polymorphism.

Also, might fix arithmetic

2 files changed, 620 insertions, 800 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 70987971..f2fbcec2 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -394,26 +394,50 @@ let list_length l = integerFromNat (List.length l)
 
 val taint: value -> list reg_form -> value
 let rec taint value regs = 
-  match value with 
-  | V_track value rs -> V_track value (regs ++ rs)
-  | V_tuple vals -> V_tuple (List.map (fun v -> taint v regs) vals)
-  | _ -> V_track value regs
+  match regs with
+    | [] -> value
+    | _ ->
+      match value with 
+	| V_track value rs -> V_track value (regs ++ rs)
+	| V_tuple vals -> V_tuple (List.map (fun v -> taint v regs) vals)
+	| _ -> V_track value regs
+end end
+
+val retaint: value -> value -> value
+let retaint orig updated =
+  match orig with 
+    | V_track _ rs -> taint updated rs
+    | _ -> updated
 end
 
+val detaint: value -> value 
+let detaint value = 
+  match value with
+    | V_track value _ -> value
+    | v -> v
+end
+
+let binary_taint thunk vall valr =
+ match (vall,valr) with
+   | (V_track vl rl,V_track vr rr) -> taint (thunk vl vr) (rl++rr)
+   | (V_track vl rl,vr) -> taint (thunk vl vr) rl
+   | (vl,V_track vr rr) -> taint (thunk vl vr) rr
+   | (vl,vr) -> thunk vl vr
+end 
+
 val access_vector : value -> integer -> value
-let rec access_vector v n =
-  match v with
-  | V_unknown -> V_unknown 
-  | V_vector m inc vs -> 
-    if inc then
-    list_nth vs (n - m)
-    else list_nth vs (m - n)
-  | V_vector_sparse _ _ _ vs d ->
-    match (List.lookup n vs) with
-      | Nothing -> d
-      | Just v  -> v end 
-  | V_track v r -> V_track (access_vector v n) r 
-  end
+let access_vector v n =
+  retaint v (match (detaint v) with
+    | V_unknown -> V_unknown 
+    | V_vector m inc vs -> 
+      if inc then
+	list_nth vs (n - m)
+      else list_nth vs (m - n)
+    | V_vector_sparse _ _ _ vs d ->
+      match (List.lookup n vs) with
+	| Nothing -> d
+	| Just v  -> v end 
+  end )
 
 val from_n_to_n :forall 'a. integer -> integer  -> list 'a -> list 'a
 let from_n_to_n from to_ ls =
@@ -440,24 +464,23 @@ let rec slice_sparse_list compare update_n vals n1 n2 =
   end
 
 val slice_vector : value -> integer -> integer -> value
-let rec slice_vector v n1 n2 =
-  match v with
-  | V_vector m inc vs ->
-    if inc 
-    then V_vector n1 inc (from_n_to_n (n1 - m) (n2 - m) vs)
-    else V_vector (n1 - n2 + 1) inc (from_n_to_n (m - n1) (m - n2) vs)
-  | V_vector_sparse m n inc vs d -> 
-    let (slice, still_sparse) = 
+let slice_vector v n1 n2 =
+  retaint v (match detaint v with
+    | V_vector m inc vs ->
       if inc 
-      then slice_sparse_list (>) (fun i -> i + 1) vs n1 n2
-      else slice_sparse_list (<) (fun i -> i - 1) vs n1 n2 in
-    if still_sparse && inc
-    then V_vector_sparse n1 (n2 - n1) inc slice d
-    else if inc then V_vector 0 inc (List.map snd slice)
-    else if still_sparse then V_vector_sparse (n1 - n2 +1) (n1 - n2) inc slice d
-    else V_vector (n1 - n2 +1) inc (List.map snd slice)
-  | V_track v r -> V_track (slice_vector v n1 n2) r
-  end
+      then V_vector n1 inc (from_n_to_n (n1 - m) (n2 - m) vs)
+      else V_vector (n1 - n2 + 1) inc (from_n_to_n (m - n1) (m - n2) vs)
+    | V_vector_sparse m n inc vs d -> 
+      let (slice, still_sparse) = 
+	if inc 
+	then slice_sparse_list (>) (fun i -> i + 1) vs n1 n2
+	else slice_sparse_list (<) (fun i -> i - 1) vs n1 n2 in
+      if still_sparse && inc
+      then V_vector_sparse n1 (n2 - n1) inc slice d
+      else if inc then V_vector 0 inc (List.map snd slice)
+      else if still_sparse then V_vector_sparse (n1 - n2 +1) (n1 - n2) inc slice d
+      else V_vector (n1 - n2 +1) inc (List.map snd slice)
+ end )
 
 val update_field_list : list (id * value) -> list (id * value) -> list (id * value)
 let rec update_field_list base updates =
@@ -469,14 +492,12 @@ let rec update_field_list base updates =
 end
 
 val fupdate_record : value -> value -> value
-let rec fupdate_record base updates = 
-  match (base,updates) with
-  | (V_record t bs,V_record _ us) -> V_record t (update_field_list bs us) 
-  | (V_track v1 r1,V_track v2 r2) -> V_track (fupdate_record v1 v2) (r1++r2)
-  | (V_track v1 r1,updates)       -> V_track (fupdate_record v1 updates) r1
-  | (base, V_track v2 r2)         -> V_track (fupdate_record base v2) r2
-end
-
+let fupdate_record base updates = 
+  let fupdate_record_helper base updates =
+      (match (base,updates) with
+	| (V_record t bs,V_record _ us) -> V_record t (update_field_list bs us) 
+       end) in
+  binary_taint fupdate_record_helper base updates
 
 val fupdate_sparse : (integer -> integer -> bool) -> list (integer*value) -> integer -> value -> list (integer*value)
 let rec fupdate_sparse compare vs n vexp =
@@ -489,17 +510,15 @@ let rec fupdate_sparse compare vs n vexp =
 end
 
 val fupdate_vec : value -> integer -> value -> value
-let rec fupdate_vec v n vexp =
-  match v with
-  | V_vector m inc vals -> 
-    V_vector m inc (List.update vals (natFromInteger (if inc then (n-m) else (m-n))) vexp)
-  | V_vector_sparse m o inc vals d ->
-    V_vector_sparse m o inc (fupdate_sparse (if inc then (>) else (<)) vals n vexp) d
-  | V_track v r -> (match vexp with
-    | V_track vexp rexp -> V_track (fupdate_vec v n vexp) (r++rexp)
-    | _ -> V_track (fupdate_vec v n vexp) r end)
-  end
-
+let fupdate_vec v n vexp =
+  let tainted = binary_taint (fun v _ -> v) v vexp in
+  retaint tainted
+    (match detaint v with
+      | V_vector m inc vals -> 
+	V_vector m inc (List.update vals (natFromInteger (if inc then (n-m) else (m-n))) vexp)
+      | V_vector_sparse m o inc vals d ->
+	V_vector_sparse m o inc (fupdate_sparse (if inc then (>) else (<)) vals n vexp) d
+     end)
 
 val replace_is : forall 'a. list 'a -> list 'a -> integer -> integer -> integer -> list 'a
 let rec replace_is ls vs base start stop =
@@ -525,34 +544,33 @@ let rec replace_sparse compare vals reps =
 end
 
 val fupdate_vector_slice : value -> value -> integer -> integer -> value
-let rec fupdate_vector_slice vec replace start stop =
-  match (vec,replace) with
-  | (V_vector m inc vals,V_vector _ inc' reps) ->
-    V_vector m inc 
-      (replace_is vals 
-	 (if inc=inc' then reps else (List.reverse reps))
-	 0 (if inc then (start-m) else (m-start)) (if inc then (stop-m) else (m-stop)))
-  | (V_vector m inc vals, V_unknown) ->
-    V_vector m inc
-      (replace_is vals 
-	 (List.replicate (natFromInteger(if inc then (stop-start) else (start-stop))) V_unknown)
-	 0 (if inc then (start-m) else (m-start)) (if inc then (stop-m) else (m-stop)))
-  | (V_vector_sparse m n inc vals d,V_vector _ _ reps) ->
-    let (_,repsi) = List.foldr (fun r (i,rs) -> ((if inc then i+1 else i-1), (i,r)::rs)) (start,[]) reps in
-    (V_vector_sparse m n inc (replace_sparse (if inc then (<) else (>)) vals repsi) d)
-  | (V_vector_sparse m n inc vals d, V_unknown) ->
-    let (_,repsi) = List.foldr (fun r (i,rs) -> ((if inc then i+1 else i-1), (i,r)::rs)) (start,[]) 
-      (List.replicate (natFromInteger (if inc then (stop-start) else (start-stop))) V_unknown) in
-    (V_vector_sparse m n inc (replace_sparse (if inc then (<) else (>)) vals repsi) d)
-  | (V_track v r, V_track vr rr) -> (taint (fupdate_vector_slice v vr start stop) (r++rr))
-  | (V_track v r, replace) -> taint (fupdate_vector_slice v replace start stop) r
-  | (vec, V_track vr rr) -> taint (fupdate_vector_slice vec vr start stop) rr
-  | (V_unknown,_) -> V_unknown
-  end
+let fupdate_vector_slice vec replace start stop =
+  let fupdate_vec_help vec replace = 
+    (match (vec,replace) with
+    | (V_vector m inc vals,V_vector _ inc' reps) ->
+      V_vector m inc 
+	(replace_is vals 
+	   (if inc=inc' then reps else (List.reverse reps))
+	   0 (if inc then (start-m) else (m-start)) (if inc then (stop-m) else (m-stop)))
+    | (V_vector m inc vals, V_unknown) ->
+      V_vector m inc
+	(replace_is vals 
+	   (List.replicate (natFromInteger(if inc then (stop-start) else (start-stop))) V_unknown)
+	   0 (if inc then (start-m) else (m-start)) (if inc then (stop-m) else (m-stop)))
+    | (V_vector_sparse m n inc vals d,V_vector _ _ reps) ->
+      let (_,repsi) = List.foldr (fun r (i,rs) -> ((if inc then i+1 else i-1), (i,r)::rs)) (start,[]) reps in
+      (V_vector_sparse m n inc (replace_sparse (if inc then (<) else (>)) vals repsi) d)
+    | (V_vector_sparse m n inc vals d, V_unknown) ->
+      let (_,repsi) = List.foldr (fun r (i,rs) -> ((if inc then i+1 else i-1), (i,r)::rs)) (start,[]) 
+	(List.replicate (natFromInteger (if inc then (stop-start) else (start-stop))) V_unknown) in
+      (V_vector_sparse m n inc (replace_sparse (if inc then (<) else (>)) vals repsi) d)
+    | (V_unknown,_) -> V_unknown
+     end) in
+  binary_taint fupdate_vec_help vec replace
 
 val update_vector_slice : value -> value -> integer -> integer -> lmem -> lmem
-let rec update_vector_slice vector value start stop mem = 
-  match (vector,value) with
+let update_vector_slice vector value start stop mem = 
+  match (detaint vector,value) with
   | ((V_boxref n t), v) ->
     update_mem mem n (fupdate_vector_slice (in_mem mem n) v start stop)    
   | ((V_vector m inc vs),(V_vector n inc2 vals)) ->
@@ -576,23 +594,23 @@ let rec update_vector_slice vector value start stop mem =
     List.foldr (fun vbox mem -> match vbox with
                                     | V_boxref n t -> update_mem mem n v end)
       mem vs'
-  | (V_track v1 r1, v) -> (update_vector_slice v1 value start stop mem) 
 end
 
-let rec update_vector_start new_start expected_size v = match v with
-  | V_lit (L_aux L_zero _) ->
-    V_vector new_start true (*TODO: Check for default endianness here*) [v]
-  | V_lit (L_aux L_one _) ->
-    V_vector new_start true [v]
-  | V_vector m inc vs -> V_vector new_start inc vs
+let update_vector_start new_start expected_size v = 
+  retaint v
+    (match detaint v with
+      | V_lit (L_aux L_zero _) ->
+	V_vector new_start true (*TODO: Check for default endianness here*) [v]
+      | V_lit (L_aux L_one _) ->
+	V_vector new_start true [v]
+      | V_vector m inc vs -> V_vector new_start inc vs
   (*Note, may need to shrink and check if still sparse *)
-  | V_vector_sparse m n inc vals d -> V_vector_sparse new_start n inc vals d 
-  | V_unknown -> 
-    V_vector new_start true (List.replicate (natFromInteger expected_size) V_unknown)
-  | V_lit (L_aux L_undef _) -> 
-    V_vector new_start true (List.replicate (natFromInteger expected_size) v)
-  | V_track v r -> taint (update_vector_start new_start expected_size v) r
-end
+      | V_vector_sparse m n inc vals d -> V_vector_sparse new_start n inc vals d 
+      | V_unknown -> 
+	V_vector new_start true (List.replicate (natFromInteger expected_size) V_unknown)
+      | V_lit (L_aux L_undef _) -> 
+	V_vector new_start true (List.replicate (natFromInteger expected_size) v)
+     end)
 
 val in_ctors : list (id * typ) -> id -> maybe typ
 let rec in_ctors ctors id =
@@ -650,6 +668,8 @@ end
 
 let id_of_string s = (Id_aux (Id s) Unknown)
 
+let redex_id = id_of_string "0"
+
 (*functions for converting in progress evaluation back into expression for building current continuation*)
 let rec combine_typs ts =
   match ts with
@@ -827,12 +847,8 @@ end
 (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *)
 val match_pattern : pat tannot -> value -> bool * bool * lenv
 let rec match_pattern (P_aux p _) value_whole =
-  let value = match value_whole with | V_track v _ -> v | _ -> value_whole end in
-  let taint_pat v = 
-    match (v,value_whole) with 
-    | (V_track v r,V_track _ wr) -> V_track v (r++wr)
-    | (v, V_track _ r) -> V_track v r
-    | _ -> v end in
+  let value = detaint value_whole in
+  let taint_pat v = binary_taint (fun v _ -> v) v value_whole in
   match p with 
   | P_lit(lit) -> 
     if is_lit_vector lit then
@@ -886,12 +902,10 @@ let rec match_pattern (P_aux p _) value_whole =
      else (false,false,eenv)
    | V_ctor (Id_aux cid _) t v ->
      if id = cid
-     then (match (pats,v) with
+     then (match (pats,detaint v) with
      | ([],(V_lit (L_aux L_unit _))) -> (true,true,eenv)
-     | ([],(V_track (V_lit (L_aux L_unit _)) _)) -> (true,true,eenv)
      | ([P_aux (P_lit (L_aux L_unit _)) _],(V_lit (L_aux L_unit _))) -> (true,true,eenv)
-     | ([P_aux (P_lit (L_aux L_unit _)) _],(V_track (V_lit (L_aux L_unit _)) _)) -> (true,true,eenv)
-     | ([p],v) -> match_pattern p v
+     | ([p],_) -> match_pattern p v
      | _ -> (false,false,eenv) end)
      else (false,false,eenv)
    | V_unknown -> (true,true,eenv)
@@ -1136,19 +1150,17 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	  let conditional_update_vstart () =
 	    match typ with
 	      | Typ_app (Id_aux (Id "vector") _) [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i) _)) _;_;_;_] ->
-		match v with 
+		match (detaint v) with 
 		  | V_vector start inc vs ->
 		    if start = i then (Value v,lm,le) else (Value (update_vector_start i 1 v),lm,le)
-		  | V_track (V_vector start inc vs) r ->
-		    if start = i then (Value v,lm,le) else (Value (update_vector_start i 1 v),lm,le)
 		  | _ -> (Value v,lm,le) end
 	      | _ -> (Value v,lm,le) end in
-          (match (tag,v) with 
+          (match (tag,detaint v) with 
 	    (*Cast is telling us to read a register*)
 	    | (Tag_extern _, V_register regform) ->
 	      (Action (Read_reg regform Nothing) 
-	         (Hole_frame (id_of_string "0")
-		    (E_aux (E_id (id_of_string "0")) (Unknown, (val_annot (reg_to_t regform)))) t_level le lm Top), lm,le)
+	         (Hole_frame redex_id
+		    (E_aux (E_id redex_id) (Unknown, (val_annot (reg_to_t regform)))) t_level le lm Top), lm,le)
 	    (*Cast is changing vector start position, potentially*)
 	    | (_,v) -> conditional_update_vstart () end))
 	(fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_cast ctyp e) (l,annot), env))))
@@ -1179,9 +1191,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 		| Just(V_register regform) -> regform
 		| _ -> Reg id annot end end in
 	  (Action (Read_reg regf Nothing)
-	          (Hole_frame (Id_aux (Id "0") Unknown)
-		         (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level l_env l_mem Top),
-           l_mem,l_env)
+	          (Hole_frame redex_id
+		         (E_aux (E_id redex_id) (l,intern_annot annot)) t_level l_env l_mem Top),l_mem,l_env)
         | Tag_alias -> 
 	  match in_env aliases id with
 	    | Just aspec -> interp_alias_read mode t_level l_env l_mem aspec
@@ -1192,12 +1203,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
       resolve_outcome 
 	(interp_main mode t_level l_env l_mem cond)
 	(fun value_whole lm le -> 
-	  let value = match value_whole with | V_track v _ -> v | _ -> value_whole end in
+	  let value = detaint value_whole in
 	  match (value,mode.eager_eval) with
 	    (*TODO remove booleans here when fully removed elsewhere *)
-            | (V_lit(L_aux L_true _),true) -> interp_main mode t_level l_env lm thn
 	    | (V_lit(L_aux L_one _),true) -> interp_main mode t_level l_env lm thn
-	    | (V_lit(L_aux L_true _),false) -> debug_out Nothing Nothing thn t_level lm l_env 
 	    | (V_lit(L_aux L_one _),false) -> debug_out Nothing Nothing thn t_level lm l_env
 	    | (V_vector _ _ [(V_lit(L_aux L_one _))],true) -> interp_main mode t_level l_env lm thn
 	    | (V_vector _ _ [(V_lit(L_aux L_one _))],false) -> debug_out Nothing Nothing thn t_level lm l_env
@@ -1210,21 +1219,21 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
       resolve_outcome 
 	(interp_main mode t_level l_env l_mem from)
         (fun from_val_whole lm le ->
-	  let from_val = match from_val_whole with | V_track v _ -> v | v -> v end in
+	  let from_val = detaint from_val_whole in
           let (from_e,env) = to_exp mode le from_val_whole in
           match from_val with
             | V_lit(L_aux(L_num from_num) fl) -> 
               resolve_outcome 
 		(interp_main mode t_level env lm to_)
                 (fun to_val_whole lm le ->
-		  let to_val = match to_val_whole with | V_track v _ -> v | v -> v end in
+		  let to_val = detaint to_val_whole in
 		  let (to_e,env) = to_exp mode le to_val_whole in
                   match to_val with
                     | V_lit(L_aux (L_num to_num) tl) ->
                       resolve_outcome 
                         (interp_main mode t_level env lm by)
                         (fun by_val_whole lm le ->
-			  let by_val = match by_val_whole with V_track v _ -> v | v -> v end in
+			  let by_val = detaint by_val_whole in
 			  let (by_e,env) = to_exp mode le by_val_whole in
                           match by_val with 
                             | V_lit (L_aux (L_num by_num) bl) ->
@@ -1233,13 +1242,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                               else
 				let (ftyp,ttyp,btyp) = (val_typ from_val,val_typ to_val,val_typ by_val) in
 				let augment_annot = (fl, val_annot (combine_typs [ftyp;ttyp])) in
-				let diff = L_aux (L_num (if is_inc then from_num + by_num else from_num - by_num)) fl in
+				let diff = L_aux (L_num (if is_inc then from_num+by_num else from_num - by_num)) fl in
 				let (augment_e,env) = match (from_val_whole,by_val_whole) with
 				  | (V_lit _, V_lit _) -> ((E_aux (E_lit diff) augment_annot), env)
-				  | (V_track _ rs, V_lit _) -> to_exp mode env (V_track (V_lit diff) rs)
-				  | (V_lit _, V_track _ rs) -> to_exp mode env (V_track (V_lit diff) rs)
+				  | (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 (V_track (V_lit diff) (r1 ++ r2))) end in
+				    (to_exp mode env (taint (V_lit diff) (r1 ++ r2))) end in
 				let  e = 
 				  (E_aux (E_block 
 					    [(E_aux 
@@ -1335,11 +1344,9 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
         (fun hdv lm le -> 
 	  resolve_outcome
             (interp_main mode t_level l_env lm tl)
-            (fun tlv lm le -> match tlv with 
-              | V_list t -> (Value(V_list (hdv::t)),lm,le)
-	      | V_unknown -> (Value V_unknown,lm,le)
-	      | V_track (V_list t) r -> (Value (V_track (V_list (hdv::t)) r),lm,le)
-	      | V_track V_unknown r -> (Value (V_track V_unknown r),lm,le)
+            (fun tlv lm le -> match detaint tlv with 
+              | V_list t -> (Value (retaint tlv (V_list (hdv::t))),lm,le)
+	      | V_unknown -> (Value (retaint tlv V_unknown),lm,le)
               | _ -> (Error l "Internal error '::' of non-list value",lm,le) end)
             (fun a -> update_stack a 
               (add_to_top_frame 
@@ -1348,18 +1355,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     | E_field exp id -> 
       resolve_outcome 
 	(interp_main mode t_level l_env l_mem exp)
-        (fun value lm le -> 
-          match value with 
+        (fun value_whole lm le -> 
+          match detaint value_whole with 
             | V_record t fexps -> 
 	      (match in_env fexps id with
-                | Just v -> (Value v,lm,l_env)
-                | Nothing -> (Error l "Internal_error: Field not found in record",lm,le) end)
-            | V_track (V_record t fexps) r -> 
-	      (match in_env fexps id with
-                | Just v -> (Value (V_track v r),lm,l_env)
+                | Just v -> (Value (retaint value_whole v),lm,l_env)
                 | Nothing -> (Error l "Internal_error: Field not found in record",lm,le) end)
-	    | V_unknown -> (Value V_unknown,lm,l_env)
-	    | V_track V_unknown r -> (Value value,lm,l_env)
+	    | V_unknown -> (Value (retaint value_whole V_unknown),lm,l_env)
             | _ -> (Error l "Internal error, neither register nor record at field access",lm,le) end)
         (fun a -> 
 	  match (exp,a) with
@@ -1387,118 +1389,98 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     | E_vector_access vec i ->
       resolve_outcome 
 	(interp_main mode t_level l_env l_mem i)
-        (fun iv_whole lm le -> 
-	  let iv = match iv_whole with | V_track v _ -> v | _ -> iv_whole end in
-          match iv with
-	    | V_unknown -> (Value iv_whole,lm,le)
-            | V_lit (L_aux (L_num n) ln) -> 
+        (fun iv lm le -> 
+	  match detaint iv with
+	    | V_unknown -> (Value iv,lm,le)
+	    | V_lit (L_aux (L_num n) ln) ->
               resolve_outcome
 		(interp_main mode t_level l_env lm vec)
-                (fun vvec lm le ->
-                  match vvec with
-		    | V_vector _ _ _ -> (Value (access_vector vvec n),lm,le)
-		    | V_track ((V_vector _ _ _) as vvec) r ->
-		      (match iv_whole with
-			| V_track _ ir -> (Value (taint (access_vector vvec n) (r++ir)),lm,le)
-			| _ -> (Value (taint (access_vector vvec n) r),lm,le) end)
-		    | V_vector_sparse _ _ _ _ _ -> (Value (access_vector vvec n),lm,le)
-		    | V_track ((V_vector_sparse _ _ _ _ _) as vvec) r ->
-		      (match iv_whole with
-			| V_track _ ir -> (Value (taint (access_vector vvec n) (r++ir)),lm,le)
-			| _ -> (Value (taint (access_vector vvec n) r),lm,le) end)
-		    | V_unknown -> (Value V_unknown,lm,le)
-                    | V_track V_unknown r -> (Value (V_track V_unknown r),lm,le)
-                    | _ -> (Error l "Vector access reading of non-vector",lm,le)end)
-                (fun a ->
+		(fun vvec lm le ->
+		  let v_access vvec num = (match (vvec,num) with
+		    | (V_vector _ _ _,V_lit _) -> access_vector vvec n
+		    | (V_vector_sparse _ _ _ _ _,V_lit _) -> access_vector vvec n
+		    | (V_vector _ _ _,V_unknown) -> V_unknown
+		    | (V_vector_sparse _ _ _ _ _,V_unknown) -> V_unknown
+		    | (V_unknown,_) -> V_unknown 
+		    | _ -> Assert_extra.failwith 
+		      ("Vector access error: " ^ (string_of_value vvec) ^ "[" ^ (string_of_integer n) ^ "]") end) in
+		  (Value (binary_taint v_access vvec iv),lm,le))
+		(fun a ->
 		  match a with
-                    | Action (Read_reg reg Nothing) stack -> 
-		      match vec with
+		    | Action (Read_reg reg Nothing) stack -> 
+		      (match vec with
 			| (E_aux _ (l,Just(_,Tag_extern _,_,_))) -> Action (Read_reg reg (Just(n,n))) stack
 			| _ -> Action (Read_reg reg Nothing) 
-			              (add_to_top_frame 
-					 (fun v env -> 
-					   let (iv_e, env) = to_exp mode env iv_whole in
-					   (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end
-                    | Action (Read_reg reg (Just (o,p))) stack ->
-		      match vec with
+			  (add_to_top_frame 
+			     (fun v env -> 
+			       let (iv_e, env) = to_exp mode env iv in
+			       (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end)
+		    | Action (Read_reg reg (Just (o,p))) stack ->
+		      (match vec with
 			| (E_aux _ (l,Just(_,Tag_extern _,_,_))) -> Action (Read_reg reg (Just(n,n))) stack
 			| _ -> Action (Read_reg reg (Just (o,p))) 
-			              (add_to_top_frame 
-					 (fun v env -> 
-					   let (iv_e, env) = to_exp mode env iv_whole in
-					   (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end
-                    | _ -> 
-                      update_stack a 
+			  (add_to_top_frame 
+			     (fun v env -> 
+			       let (iv_e, env) = to_exp mode env iv in
+			       (E_aux (E_vector_access v iv_e) (l,annot),env)) stack) end)
+		    | _ -> 
+		      update_stack a 
 			(add_to_top_frame 
 			   (fun v env -> 
-			     let (iv_e, env) = to_exp mode env iv_whole in
+			     let (iv_e, env) = to_exp mode env iv in
 			     (E_aux (E_vector_access v iv_e) (l,annot), env))) end)
             | _ -> (Error l "Vector access not given a number for index",lm,l_env) end)
         (fun a -> update_stack a (add_to_top_frame (fun i env -> (E_aux (E_vector_access vec i) (l,annot), env))))
     | E_vector_subrange vec i1 i2 ->
       resolve_outcome 
 	(interp_main mode t_level l_env l_mem i1)
-        (fun i1v_whole lm le ->
-	  let iv1 = (match i1v_whole with | V_track iv1 _ -> iv1 | _ -> i1v_whole end) in
-	  match iv1 with
-	    | V_unknown -> (Value i1v_whole,lm,le)
-	    | _ -> 
+        (fun i1v lm le ->
+	  match detaint i1v with
+	    | V_unknown -> (Value i1v,lm,le)
+	    | V_lit (L_aux (L_num n1) nl1) -> 
               resolve_outcome 
 		(interp_main mode t_level l_env lm i2)
-		(fun i2v_whole lm le ->
-		  let iv2 = (match i2v_whole with | V_track iv2 _ -> iv2 | _ -> i2v_whole end) in
-		  match iv2 with
-		    | V_unknown -> (Value i2v_whole,lm,le)
+		(fun i2v lm le ->
+		  match detaint i2v with
+		    | V_unknown -> (Value i2v,lm,le)
 		    | _ ->
 		      resolve_outcome 
 			(interp_main mode t_level l_env lm vec)
 			(fun vvec lm le ->
-			  let tracking = (match (i1v_whole,i2v_whole) with 
-			    | (V_track _ r1,V_track _ r2) -> (r1++r2)
-			    | (V_track _ r, _) -> r
-			    | (_, V_track _ r) -> r
-			    | _ -> [] end) in
-			  match (iv1,iv2) with
-			    | (V_lit (L_aux (L_num n1) ln1),V_lit (L_aux (L_num n2) ln2)) ->
-			      (match (vvec,tracking) with
-				| (V_vector _ _ _,[]) -> (Value (slice_vector vvec n1 n2),lm,le)
-				| (V_vector _ _ _,tr) -> (Value (taint (slice_vector vvec n1 n2) tr), lm,le)
-				| (V_track ((V_vector _ _ _) as vvec) r,_) -> 
-				  (Value (taint (slice_vector vvec n1 n2) (r++tracking)), lm,le)
-				| (V_vector_sparse _ _ _ _ _,[]) -> (Value (slice_vector vvec n1 n2), lm,le)
-				| (V_vector_sparse _ _ _ _ _,tr) -> (Value (taint (slice_vector vvec n1 n2) tr),lm,le)
-				| (V_track ((V_vector_sparse _ _ _ _ _) as vvec) r,_) ->
-				  (Value (taint (slice_vector vvec n1 n2) (r++tracking)), lm,le)
-				| (V_track V_unknown r, tr) -> (Value (V_track V_unknown (r++tr)),lm,le)
-				| (V_unknown,_) -> 
+			  let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) i1v i2v in
+			  let take_slice vtup vvec =
+			    (match vtup with
+			      | V_tuple [V_lit (L_aux (L_num n1) ln1);V_lit (L_aux (L_num n2) ln2)] ->
+				(match vvec with
+				| V_vector _ _ _ -> slice_vector vvec n1 n2
+				| V_vector_sparse _ _ _ _ _ -> slice_vector vvec n1 n2
+				| V_unknown -> 
 				  let inc = n1 < n2 in
-				  (Value
-				    (V_vector n1 inc 
-				      (List.replicate (natFromInteger ((if inc then n1-n2 else n2-n1)+1)) V_unknown)),
-				   lm,le)
-				| _ -> (Error l "Vector slice of non-vector",lm,le) end)
-			 end)
+				  V_vector n1 inc 
+				    (List.replicate (natFromInteger ((if inc then n1-n2 else n2-n1)+1)) V_unknown)
+				| _ -> Assert_extra.failwith "Vector slice of non-vector" end) end) in
+			  (Value (binary_taint take_slice slice vvec), lm,le))
 			(fun a -> 
-			  let rebuild v env = let (ie1,env) = to_exp mode env i1v_whole in
-					      let (ie2,env) = to_exp mode env i2v_whole in
+			  let rebuild v env = let (ie1,env) = to_exp mode env i1v in
+					      let (ie2,env) = to_exp mode env i2v in
 					      (E_aux (E_vector_subrange v ie1 ie2) (l,annot), env) in
 			  match a with 
 			    | Action (Read_reg reg Nothing) stack ->
 			      match vec with
 				| (E_aux _ (l,Just(_,Tag_extern _,_,_))) -> 
-				  Action (Read_reg reg (Just((get_num iv1),(get_num iv2)))) stack
+				  Action (Read_reg reg (Just((get_num i1v),(get_num i2v)))) stack
 				| _ -> Action (Read_reg reg Nothing) (add_to_top_frame rebuild stack) end
 		            | Action (Read_reg reg (Just (o,p))) stack ->
 			      match vec with
 				| (E_aux _ (l,Just(_,Tag_extern _,_,_))) -> 
-				  Action (Read_reg reg (Just((get_num iv1),(get_num iv2)))) stack
+				  Action (Read_reg reg (Just((get_num i1v),(get_num i2v)))) stack
 				| _ -> Action (Read_reg reg (Just (o,p))) (add_to_top_frame rebuild stack) end
                             | _ -> update_stack a (add_to_top_frame rebuild) end)
 		 end)
                 (fun a -> update_stack a 
 		  (add_to_top_frame 
 		     (fun i2 env -> 
-		       let (ie1,env) = to_exp mode env i1v_whole in
+		       let (ie1,env) = to_exp mode env i1v in
 		       (E_aux (E_vector_subrange vec ie1 i2) (l,annot), env))))
 	 end) 
         (fun a -> 
@@ -1506,55 +1488,47 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     | E_vector_update vec i exp ->
       resolve_outcome 
 	(interp_main mode t_level l_env l_mem i)
-        (fun vi_whole lm le ->
-	  let (vi,tracking) = match vi_whole with V_track v r -> (v,r) | _ -> (vi_whole,[]) end in
-          match vi with
+        (fun vi lm le ->
+          (match (detaint vi) with
             | V_lit (L_aux (L_num n1) ln1) ->
-              resolve_outcome 
-		(interp_main mode t_level le lm exp)
-                (fun vup lm le ->
-                  resolve_outcome 
-		    (interp_main mode t_level le lm vec)
-                    (fun vec lm le ->
-                      match (vec,tracking) with
-                        | (V_vector _ _ _,[]) -> (Value (fupdate_vec vec n1 vup), lm,le)
-			| (V_track ((V_vector _ _ _) as vvec) r, tracking) ->
-			  (Value (taint (fupdate_vec vec n1 vup) (r++tracking)),lm,le)
-			| (V_vector_sparse _ _ _ _ _,[]) -> (Value (fupdate_vec vec n1 vup),lm,le)
-			| (V_track ((V_vector_sparse _ _ _ _ _) as vvec) r, tracking) ->
-			  (Value (taint (fupdate_vec vec n1 vup) (r++tracking)),lm,le)
-			| (V_track V_unknown r,_) ->
-			  (Value (taint V_unknown (r++tracking)),lm,le)
-			| (V_unknown,_) -> (Value V_unknown, lm, le)
-                        | _ -> (Error l "Update of vector given non-vector",lm,le) end)
-                    (fun a -> update_stack a 
-		      (add_to_top_frame 
-			 (fun v env ->
-                           let (eup,env') = (to_exp mode env vup) in 
-			   let (ei, env') = (to_exp mode env' vi_whole) in
-                           (E_aux (E_vector_update v ei eup) (l,annot), env')))))
-                (fun a -> update_stack a 
-		  (add_to_top_frame 
-		     (fun e env -> 
-		       let (ei, env) = to_exp mode env vi_whole in
-		       (E_aux (E_vector_update vec ei e) (l,annot), env))))
-	    | V_unknown -> (Value vi_whole,lm,l_env)
-            | _ -> (Error l "Update of vector requires number for access",lm,le) end)
+              (resolve_outcome 
+		 (interp_main mode t_level le lm exp)
+                 (fun vup lm le ->
+                   resolve_outcome 
+		     (interp_main mode t_level le lm vec)
+                     (fun vec lm le ->
+		       let fvup vi vec = (match vec with
+			 | V_vector _ _ _ -> fupdate_vec vec n1 vup
+			 | V_vector_sparse _ _ _ _ _ -> fupdate_vec vec n1 vup
+			 | V_unknown -> V_unknown
+                         | _ -> Assert_extra.failwith "Update of vector given non-vector" end) in
+		       (Value (binary_taint fvup vi vec),lm,le))
+                     (fun a -> update_stack a 
+		       (add_to_top_frame 
+			  (fun v env ->
+                            let (eup,env') = (to_exp mode env vup) in 
+			    let (ei, env') = (to_exp mode env' vi) in
+                            (E_aux (E_vector_update v ei eup) (l,annot), env')))))
+                 (fun a -> update_stack a 
+		   (add_to_top_frame 
+		      (fun e env -> 
+			let (ei, env) = to_exp mode env vi in
+			(E_aux (E_vector_update vec ei e) (l,annot), env)))))
+	    | V_unknown -> (Value vi,lm,l_env)
+            | _ -> Assert_extra.failwith "Update of vector requires number for access" end))
         (fun a -> update_stack a (add_to_top_frame (fun i env -> (E_aux (E_vector_update vec i exp) (l,annot), env))))
     | E_vector_update_subrange vec i1 i2 exp ->
       resolve_outcome 
 	(interp_main mode t_level l_env l_mem i1)
-        (fun vi1_whole lm le ->
-	  let (vi1,v1_t) = match vi1_whole with | V_track v r -> (v,r) | _ -> (vi1_whole,[]) end in
-          match vi1 with
-	    | V_unknown -> (Value vi1_whole,lm,le)
+        (fun vi1 lm le ->
+	  match detaint vi1 with
+	    | V_unknown -> (Value vi1,lm,le)
             | V_lit (L_aux (L_num n1) ln1) ->
               resolve_outcome 
                 (interp_main mode t_level l_env lm i2) 
-                (fun vi2_whole lm le ->
-		  let (vi2,tracking) = match vi2_whole with | V_track v r -> (v,(r++v1_t)) | _ -> (vi2_whole,v1_t) end in
-                  match vi2 with
-		    | V_unknown -> (Value vi2_whole,lm,le)
+                (fun vi2 lm le ->
+		  match detaint vi2 with
+		    | V_unknown -> (Value vi2,lm,le)
                     | V_lit (L_aux (L_num n2) ln2) ->
                       resolve_outcome 
 			(interp_main mode t_level l_env lm exp)
@@ -1562,27 +1536,19 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                           (resolve_outcome 
                              (interp_main mode t_level l_env lm vec)
                              (fun vvec lm le ->
-                               match (vvec,tracking) with
-                                 | (V_vector _ _ _,[]) -> (Value (fupdate_vector_slice vvec v_rep n1 n2),lm,le)
-                                 | (V_vector _ _ _,tr) -> 
-				   (Value (taint (fupdate_vector_slice vvec v_rep n1 n2) tr),lm,le)
-				 | (V_track ((V_vector _ _ _) as vvec) r,t) -> 
-				   (Value (taint (fupdate_vector_slice vvec v_rep n1 n2) (r++tracking)),lm,le)
-				 | (V_vector_sparse _ _ _ _ _,[]) -> 
-				   (Value (fupdate_vector_slice vvec v_rep n1 n2),lm,le)
-                                 | (V_vector_sparse _ _ _ _ _,tr) -> 
-				   (Value (taint (fupdate_vector_slice vvec v_rep n1 n2) tr),lm,le)
-                                 | (V_track ((V_vector_sparse _ _ _ _ _) as vvec) rs,tr) ->
-                                   (Value (taint (fupdate_vector_slice vvec v_rep n1 n2) (rs++tr)),lm,le)
-				 | (V_unknown,_) -> (Value V_unknown,lm,le)
-				 | (V_track V_unknown r,_) -> (Value (taint V_unknown (r++tracking)),lm,le)
-                                 | _ -> (Error l "Vector update requires vector",lm,le) end)
+			       let slice = binary_taint (fun v1 v2 -> V_tuple[v1;v2]) vi1 vi2 in
+			       let fup_v_slice v1 vvec = (match vvec with
+                                 | V_vector _ _ _ -> fupdate_vector_slice vvec v_rep n1 n2
+				 | V_vector_sparse _ _ _ _ _ -> fupdate_vector_slice vvec v_rep n1 n2
+				 | V_unknown -> V_unknown
+				 | _ -> Assert_extra.failwith "Vector update requires vector" end) in
+			       (Value (binary_taint fup_v_slice slice vvec),lm,le))
                              (fun a -> update_stack a 
                                (add_to_top_frame 
 				  (fun v env -> 
                                     let (e_rep,env') = to_exp mode env v_rep in
-                                    let (ei1, env') = to_exp mode env' vi1_whole in
-                                    let (ei2, env') = to_exp mode env' vi2_whole in
+                                    let (ei1, env') = to_exp mode env' vi1 in
+                                    let (ei2, env') = to_exp mode env' vi2 in
                                     (E_aux (E_vector_update_subrange v ei1 ei2 e_rep) (l,annot), env'))))))
                         (fun a -> update_stack a 
                           (add_to_top_frame 
@@ -1590,89 +1556,48 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                                let (ei1,env') = to_exp mode env vi1 in
                                let (ei2,env') = to_exp mode env' vi2 in
                                (E_aux (E_vector_update_subrange vec ei1 ei2 e) (l,annot),env'))))
-                    | _ -> (Error l "vector update requires number",lm,le) end)
+                    | _ -> Assert_extra.failwith "vector update requires number" end)
                 (fun a -> 
 		  update_stack a (add_to_top_frame 
                                     (fun i2 env -> 
                                       let (ei1, env') = to_exp mode env vi1 in
                                       (E_aux (E_vector_update_subrange vec ei1 i2 exp) (l,annot), env'))))
-            | _ -> (Error l "vector update requires number",lm,le) end)
+            | _ -> Assert_extra.failwith "vector update requires number" end)
         (fun a -> 
 	  update_stack a 
 	    (add_to_top_frame (fun i1 env -> (E_aux (E_vector_update_subrange vec i1 i2 exp) (l,annot), env))))
     | E_vector_append e1 e2 ->
       resolve_outcome 
 	(interp_main mode t_level l_env l_mem e1)
-        (fun v1_whole lm le ->
-          let (v1,tracking) = match v1_whole with | V_track v r -> (v,r) | _ -> (v1_whole,[]) end in
-          match v1 with
-            | V_vector m inc vals1 ->
+        (fun v1 lm le ->
+         match detaint v1 with
+	    | V_unknown -> (Value v1,lm,l_env)
+            | _ ->
               (resolve_outcome 
 		 (interp_main mode t_level l_env lm e2)
                  (fun v2 lm le ->
-                   match (v2,tracking) with
-                     | (V_vector _ _ vals2,[]) -> (Value (V_vector m inc (vals1++vals2)),lm,l_env)
-                     | (V_vector _ _ vals2,tr) -> (Value (V_track (V_vector m inc (vals1++vals2)) tr),lm,l_env)
-                     | (V_track (V_vector _ _ vals2) r,tr) ->
-                       (Value (V_track (V_vector m inc (vals1++vals2)) (r++tr)), lm,l_env)
-		     | (V_vector_sparse _ len _ vals2 d,[]) ->
+		   let append v1 v2 = (match (v1,v2) with
+                     | (V_vector m inc vals1, V_vector _ _ vals2) -> V_vector m inc (vals1++vals2)
+		     | (V_vector m inc vals1, V_vector_sparse _ len _ vals2 d) ->
 		       let original_len = integerFromNat (List.length vals1) in
 		       let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (m,[]) vals1 in
 		       let sparse_update = List.map (fun (i,v) -> (i+m+original_len,v)) vals2 in
-		       (Value (V_vector_sparse m (len+original_len) inc (sparse_vals ++ sparse_update) d), lm,l_env)
-                     | (V_vector_sparse _ len _ vals2 d,tr) ->
-		       let original_len = integerFromNat (List.length vals1) in
-		       let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (m,[]) vals1 in
-		       let sparse_update = List.map (fun (i,v) -> (i+m+original_len,v)) vals2 in
-		       (Value 
-                          (V_track (V_vector_sparse m (len+original_len) inc (sparse_vals ++ sparse_update) d) tr), lm,l_env)
-                     | (V_track (V_vector_sparse _ len _ vals2 d) reg, tr) ->
-		       let original_len = integerFromNat (List.length vals1) in
-		       let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (m,[]) vals1 in
-		       let sparse_update = List.map (fun (i,v) -> (i+m+original_len,v)) vals2 in
-		       (Value 
-                          (V_track (V_vector_sparse m (len+original_len) inc (sparse_vals ++ sparse_update) d) (reg++tr)), lm,l_env)
-		     | (V_track V_unknown r,_) -> (Value (taint V_unknown (r++tracking)),lm,l_env)
-		     | (V_unknown,_) -> (Value V_unknown,lm,l_env)
-                     | _ -> (Error l "vector concat requires vector",lm,le) end)
-                 (fun a -> update_stack a (add_to_top_frame 
-                                             (fun e env -> 
-                                               let (e1,env') = to_exp mode env v1 in
-                                               (E_aux (E_vector_append e1 e) (l,annot),env')))))
-	    | V_vector_sparse m len inc vals1 d ->
-	      (resolve_outcome 
-		 (interp_main mode t_level l_env lm e2)
-                 (fun v2 lm le ->
-                   match (v2,tracking) with
-                     | (V_vector _ _ vals2,[]) -> 
+		       V_vector_sparse m (len+original_len) inc (sparse_vals ++ sparse_update) d
+		     | (V_vector_sparse m len inc vals1 d, V_vector _ _ vals2) ->
 		       let new_len = integerFromNat (List.length vals2) in
 		       let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (len,[]) vals2 in
-		       (Value (V_vector_sparse m (len+new_len) inc (vals1++sparse_vals) d), lm,l_env)
-                     | (V_vector _ _ vals2,tr) -> 
-		       let new_len = integerFromNat (List.length vals2) in
-		       let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (len,[]) vals2 in
-		       (Value (V_track (V_vector_sparse m (len+new_len) inc (vals1++sparse_vals) d) tr), lm,l_env)
-                     | (V_track (V_vector _ _ vals2) rs,tr) ->
-                       let new_len = integerFromNat (List.length vals2) in
-		       let (_,sparse_vals) = List.foldr (fun v (i,vals) -> (i+1,(i,v)::vals)) (len,[]) vals2 in
-		       (Value (V_track (V_vector_sparse m (len+new_len) inc (vals1++sparse_vals) d) (rs++tr)), lm,l_env)
-		     | (V_vector_sparse _ new_len _ vals2 _,[]) ->
-		       let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in
-		       (Value (V_vector_sparse m (len+new_len) inc (vals1 ++ sparse_update) d), lm,l_env)
-                     | (V_vector_sparse _ new_len _ vals2 _, tr) ->
+		       V_vector_sparse m (len+new_len) inc (vals1++sparse_vals) d
+		     | (V_vector_sparse m len inc vals1 d, V_vector_sparse _ new_len _ vals2 _) ->
 		       let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in
-		       (Value (V_track (V_vector_sparse m (len+new_len) inc (vals1 ++ sparse_update) d) tr), lm,l_env)
-                     | (V_track (V_vector_sparse _ new_len _ vals2 _) rs, tr) ->
-                       let sparse_update = List.map (fun (i,v) -> (i+len,v)) vals2 in
-		       (Value (V_track (V_vector_sparse m (len+new_len) inc (vals1 ++ sparse_update) d) (rs++tr)), lm,l_env)
-		     | (V_track V_unknown r,_) -> (Value (taint V_unknown (r++tracking)),lm,l_env)
-                     | (V_unknown,_) -> (Value V_unknown,lm,l_env)
-                     | _ -> (Error l "vector concat requires vector",lm,le) end)
+		       V_vector_sparse m (len+new_len) inc (vals1 ++ sparse_update) d
+		     | (V_unknown,_) -> V_unknown (*update to get length from type*)
+		     | (_,V_unknown) -> V_unknown (*see above*)
+                     | _ -> Assert_extra.failwith "vector concat requires vector" end) in
+		   (Value (binary_taint append v1 v2),lm,le))
                  (fun a -> update_stack a (add_to_top_frame 
-                                             (fun e env -> let (e1,env') = to_exp mode env v1 in
-                                                           (E_aux (E_vector_append e1 e) (l,annot),env')))))
-	    | V_unknown -> (Value v1,lm,l_env)
-            | _ -> (Error l "vector concat requires vector",lm,le) end)
+                                             (fun e env -> 
+                                               let (e1,env') = to_exp mode env v1 in
+                                               (E_aux (E_vector_append e1 e) (l,annot),env'))))) end)
         (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_vector_append e e2) (l,annot),env))))
     | E_tuple(exps) -> 
       exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps
@@ -1833,10 +1758,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
               match tag with
                 | Tag_global ->
 		  (match find_function defs op with
-		    | Nothing -> (Error l (String.stringAppend "Internal error, no function def for " name),lm,le)
+		    | Nothing -> (Error l ("Internal error, no function def for " ^ name),lm,le)
                     | Just (funcls) ->
 		      (match find_funcl funcls (V_tuple [lv;rv]) with 
-			| [] -> (Error l (String.stringAppend "No matching pattern for function " name),lm,l_env)
+			| [] -> (Error l ("No matching pattern for function " ^ name),lm,l_env)
 			| [(env,used_unknown,exp)] ->
 			  resolve_outcome 
 			    (if mode.eager_eval
@@ -1851,10 +1776,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 				                end)end)
 		| Tag_empty -> 
 		  (match find_function defs op with
-		    | Nothing -> (Error l (String.stringAppend "Internal error, no function def for " name),lm,le)
+		    | Nothing -> (Error l ("Internal error, no function def for " ^ name),lm,le)
                     | Just (funcls) ->
 		      (match find_funcl funcls (V_tuple [lv;rv]) with 
-			| [] -> (Error l (String.stringAppend "No matching pattern for function " name),lm,l_env)
+			| [] -> (Error l ("No matching pattern for function " ^ name),lm,l_env)
 			| [(env,used_unknown,exp)] ->
 			  resolve_outcome 
 			    (if mode.eager_eval
@@ -1862,16 +1787,15 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			     else (debug_out (Just name) (Just (V_tuple [lv;rv])) exp t_level emem env)) 
 			    (fun ret lm le -> (Value ret,l_mem,l_env))
                             (fun a -> update_stack a 
-			      (fun stack -> (Hole_frame (Id_aux (Id "0") l)
-					       (E_aux (E_id (Id_aux (Id "0") l)) (l,annot))
+			      (fun stack -> (Hole_frame redex_id (E_aux (E_id redex_id) (l,annot))
 					       t_level l_env l_mem stack)))
 		       end)end)
                 | Tag_spec ->
                   (match find_function defs op with
-		    | Nothing -> (Error l (String.stringAppend "No function definition found for " name),lm,le)
+		    | Nothing -> (Error l ("No function definition found for " ^ name),lm,le)
                     | Just (funcls) ->
 		      (match find_funcl funcls (V_tuple [lv;rv]) with 
-			| [] -> (Error l (String.stringAppend "No matching pattern for function " name),lm,l_env)
+			| [] -> (Error l ("No matching pattern for function " ^ name),lm,l_env)
 			| [(env,used_unknown,exp)] ->
 			  resolve_outcome 
 			    (if mode.eager_eval 
@@ -1886,8 +1810,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                 | Tag_extern ext_name ->
                   let ext_name = match ext_name with Just s -> s | Nothing -> name end in
         (Action (Call_extern ext_name (V_tuple [lv;rv])) 
-	   (Hole_frame (Id_aux (Id "0") l) 
-	      (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level le lm Top),lm,le) end)
+	   (Hole_frame redex_id 
+	      (E_aux (E_id redex_id) (l,intern_annot annot)) t_level le lm Top),lm,le) end)
             (fun a -> update_stack a 
               (add_to_top_frame 
                  (fun r env -> let (el,env') = to_exp mode env lv in (E_aux (E_app_infix el op r) (l,annot), env')))))
@@ -1930,8 +1854,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 (*TODO shrink location information on recursive calls *)
  and interp_block mode t_level init_env local_env local_mem l tannot exps =
    match exps with
-    | [ ] -> (Value (V_lit (L_aux (L_unit) Unknown)), local_mem, init_env)
-    | [ exp ] -> 
+    | [] -> (Value (V_lit (L_aux (L_unit) Unknown)), local_mem, init_env)
+    | [exp] -> 
       if mode.eager_eval
       then interp_main mode t_level local_env local_mem exp
       else debug_out Nothing Nothing exp t_level local_mem local_env
@@ -1954,7 +1878,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
     | LEXP_id id -> 
       match tag with
 	| Tag_empty ->
-	  match in_lenv l_env id with
+	  match detaint (in_lenv l_env id) with
 	    | ((V_boxref n t) as v) -> 
 	      if is_top_level 
 	      then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
@@ -1965,7 +1889,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		let l_mem = (LMem (c+1) m) in
 		((Value (V_lit (L_aux L_unit l)), 
 		  update_mem l_mem c value, (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
-	      else ((Error l (String.stringAppend "Unknown local id " (get_id id)),l_mem,l_env),Nothing)
+	      else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing)
             | v -> 
 	      if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing)
 	      else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
@@ -1975,7 +1899,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	    | Just v -> 
 	      if is_top_level then ((Error l "Writes must be to reg or registers",l_mem,l_env),Nothing)
 	      else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_id id) (l,annot), env)))
-	    | Nothing -> ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),Nothing)
+	    | Nothing -> ((Error l ("Undefined id " ^ (get_id id)),l_mem,l_env),Nothing)
 	   end)
         | Tag_extern _ ->
 	  let regf = 
@@ -1985,7 +1909,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
           let start_pos = reg_start_pos regf in
 	  let reg_size = reg_size regf in
 	  let request = 
-            (Action (Write_reg regf Nothing (update_vector_start start_pos reg_size value)) 
+            (Action (Write_reg regf Nothing (update_vector_start start_pos reg_size value))
 	       (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
 	     l_mem,l_env) in
           if is_top_level then (request,Nothing) 
@@ -2031,11 +1955,11 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		  | AL_slice (RI_aux (RI_id reg) (_,annot')) start stop -> 
 		    resolve_outcome (interp_main mode t_level l_env l_mem start)
 		      (fun v lm le -> 
-			match v with 
+			match detaint v with 
 			  | V_lit (L_aux (L_num start) _) ->
 			    (resolve_outcome (interp_main mode t_level l_env lm stop)
 			       (fun v le lm ->
-				 (match v with
+				 (match detaint v with
 				   | V_lit (L_aux (L_num stop) _) ->
 				     (Action (Write_reg (Reg reg annot') (Just (start,stop)) 
 						(update_vector_start start ((abs (start - stop)) +1) value)) 
@@ -2087,7 +2011,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
     | LEXP_cast typc id -> 
       match tag with
 	| Tag_empty ->
-	  match in_lenv l_env id with
+	  match detaint (in_lenv l_env id) with
 	    | ((V_boxref n t) as v) -> 
 	      if is_top_level 
 	      then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
@@ -2123,20 +2047,19 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
       end 
     | LEXP_vector lexp exp -> 
       match (interp_main mode t_level l_env l_mem exp) with
-      | (Value i_whole,lm,le) ->
-        let i = match i_whole with | V_track v _ -> v | _ -> i_whole end in
-        (match i with 
-	| V_unknown -> ((Value i_whole,lm,le),Nothing)
+      | (Value i,lm,le) ->
+        (match detaint i with 
+	| V_unknown -> ((Value i,lm,le),Nothing)
         | V_lit (L_aux (L_num n) ln) -> 
           let next_builder le_builder = 
             (fun e env -> 
               let (lexp,env) = le_builder e env in
-              let (ie,env) = to_exp mode env i_whole in
+              let (ie,env) = to_exp mode env i in
 	      (LEXP_aux (LEXP_vector lexp ie) (l,annot), env)) in
           (match (create_write_message_or_update mode t_level value l_env lm false lexp) with
           | ((Value v_whole,lm,le),maybe_builder) ->
-            let v = (match v_whole with | V_track v _ -> v | _ -> v_whole end) in
-            let nth _ = (match access_vector v n with | V_track v _ -> v | v -> v end) in
+            let v = detaint v_whole in
+            let nth _ = detaint (access_vector v n) in
             (match v with 
 	      | V_unknown -> ((Value v_whole,lm,le),Nothing)
 	      | V_boxref i _ -> 
@@ -2181,12 +2104,6 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		    ((Action (Write_reg regform Nothing (update_vector_start start_pos reg_size value)) 
 		      (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
 		      l_mem,l_env),Nothing)
-		| (V_track (V_register regform) _,true,_) ->
-		    let start_pos = reg_start_pos regform in 
-		    let reg_size = reg_size regform in
-		    ((Action (Write_reg regform Nothing (update_vector_start start_pos reg_size value)) 
-		      (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
-		      l_mem,l_env),Nothing)
 		| (V_register regform,false,Just lexp_builder) ->
 		    let start_pos = reg_start_pos regform in
 		    let reg_size = reg_size regform in
@@ -2194,13 +2111,6 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		      (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
 		      l_mem,l_env),
                      Just (next_builder lexp_builder))				
-		| (V_track (V_register regform) _,false,Just lexp_builder) ->
-		    let start_pos = reg_start_pos regform in
-		    let reg_size = reg_size regform in
-		    ((Action (Write_reg regform Nothing (update_vector_start start_pos reg_size value)) 
-		      (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),
-		      l_mem,l_env),
-                   Just (next_builder lexp_builder))
 		| (V_boxref n t,true,_) -> 
 		  ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
 		| (v,true,_) -> 
@@ -2235,27 +2145,24 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
       | e -> (e,Nothing) end
     | LEXP_vector_range lexp exp1 exp2  ->
       match (interp_main mode t_level l_env l_mem exp1) with
-      | (Value i1_whole, lm, le) ->
-        let i1 = match i1_whole with | V_track v _ -> v | _ -> i1_whole end in
-        (match i1 with
-	| V_unknown -> ((Value i1_whole,lm,le),Nothing)
+      | (Value i1, lm, le) ->
+        (match detaint i1 with
+	| V_unknown -> ((Value i1,lm,le),Nothing)
         | V_lit (L_aux (L_num n1) ln1) ->
           (match (interp_main mode t_level l_env l_mem exp2) with
-          | (Value i2_whole,lm,le) ->
-            let i2 = match i2_whole with | V_track v _ -> v | _ -> i2_whole end in
-            (match i2 with
-	    | V_unknown -> ((Value i2_whole,lm,le),Nothing)
+          | (Value i2,lm,le) ->
+            (match detaint i2 with
+	    | V_unknown -> ((Value i2,lm,le),Nothing)
             | V_lit (L_aux (L_num n2) ln2) ->
               let next_builder le_builder = 
 		(fun e env -> 
-                  let (e1,env) = to_exp mode env i1_whole in
-                  let (e2,env) = to_exp mode env i2_whole in
+                  let (e1,env) = to_exp mode env i1 in
+                  let (e2,env) = to_exp mode env i2 in
                   let (lexp,env) = le_builder e env in
                   (LEXP_aux (LEXP_vector_range lexp e1 e2) (l,annot), env)) in
               (match (create_write_message_or_update mode t_level value l_env lm false lexp) with
-              | ((Value v_whole,lm,le), Just lexp_builder) ->
-		let v = match v_whole with | V_track v _ -> v | _ -> v_whole end in
-                (match (v,is_top_level) with
+              | ((Value v,lm,le), Just lexp_builder) ->
+		(match (detaint v,is_top_level) with
                 | (V_vector m inc vs,true) -> 
                   ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice v value n1 n2 lm, l_env), Nothing)
 		| (V_boxref _ _, true) -> 
@@ -2285,7 +2192,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
           | (Action a s,lm,le) ->
             ((Action a s,lm, le), 
              Just (fun e env -> 
-               let (e1,env) = to_exp mode env i1_whole in
+               let (e1,env) = to_exp mode env i1 in
                (LEXP_aux (LEXP_vector_range lexp e1 e) (l,annot), env)))
           | e -> (e,Nothing) end)
         | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing) end)
@@ -2361,9 +2268,7 @@ end
 
 and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
   let (Env defs instrs lets regs ctors subregs aliases) = t_level in 
-  let stack = Hole_frame (Id_aux (Id "0") Unknown)
-		          (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
-			  t_level l_env l_mem Top in
+  let stack = Hole_frame redex_id (E_aux (E_id redex_id) (l,(intern_annot annot))) t_level l_env l_mem Top in
   let get_reg_typ_name typ =
     match typ with
       | T_id i -> i
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 174837f3..890372f2 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -94,42 +94,37 @@ let rec sparse_walker update ni processed_length length ls df =
     else df::(sparse_walker update (update ni) (processed_length + 1) length ((i,v)::ls) df)
 end
 
-let rec fill_in_sparse v = match v with
-  | V_vector_sparse first length inc ls df -> 
-    V_vector first inc (sparse_walker (if inc then (fun (x: integer) -> x + onei) else (fun (x: integer) -> x - onei)) first zeroi length ls df)
-  | V_unknown -> V_unknown
-  | V_track v r -> taint (fill_in_sparse v) r
-end    
-
-let is_one v = match v with 
-  | V_lit (L_aux (L_num n) lb) -> V_lit (L_aux (if n=1 then L_one else L_zero) lb)
-  | V_track (V_lit (L_aux (L_num n) lb)) r -> V_track (V_lit (L_aux (if n=1 then L_one else L_zero) lb)) r
-  | V_lit (L_aux b lb) -> V_lit (L_aux (if b = L_one then L_one else L_zero) lb)
-  | V_track (V_lit (L_aux b lb)) r -> V_track (V_lit (L_aux (if b = L_one then L_one else L_zero) lb)) r
-  | V_track V_unkown _ -> v
-  | V_unknown -> v
+let fill_in_sparse v = 
+  retaint v (match detaint v with
+    | V_vector_sparse first length inc ls df -> 
+      V_vector first inc 
+	(sparse_walker 
+	   (if inc then (fun (x: integer) -> x + onei) else (fun (x: integer) -> x - onei)) first zeroi length ls df)
+    | V_unknown -> V_unknown
+    end)
+
+let is_one v = 
+  retaint v
+    match detaint v with 
+      | V_lit (L_aux (L_num n) lb) -> V_lit (L_aux (if n=1 then L_one else L_zero) lb)
+      | V_lit (L_aux b lb) -> V_lit (L_aux (if b = L_one then L_one else L_zero) lb)
+      | V_unknown -> v
 end ;;
 
-let rec lt_range (V_tuple[v1;v2]) = match (v1,v2) with 
+let lt_range (V_tuple[v1;v2]) = 
+  let lr_helper v1 v2 = match (v1,v2) with
   | (V_lit (L_aux (L_num l1) lr),V_lit (L_aux (L_num l2) ll)) ->
     if l1 < l2
     then V_lit (L_aux L_one Unknown)
     else V_lit (L_aux L_zero Unknown)
-  | (V_track v1 r1, V_track v2 r2) -> 
-    taint (lt_range (V_tuple [v1;v2])) (r1++r2)
-  | (V_track v1 r1, v2) ->
-    taint (lt_range (V_tuple [v1;v2])) r1
-  | (v1,V_track v2 r2) ->
-    taint (lt_range (V_tuple [v1;v2])) r2
   | (V_unknown,_) -> V_unknown
   | (_,V_unknown) -> V_unknown
-end ;;
+  end in
+  binary_taint lr_helper v1 v2
 
-let bit_to_bool b = match b with
+let bit_to_bool b = match detaint b with
   | V_lit (L_aux L_zero _) -> false
-  | V_track (V_lit (L_aux L_zero _)) _ -> false
   | V_lit (L_aux L_one _) -> true
-  | V_track (V_lit (L_aux L_one _)) _ -> true
   end ;;
 let bool_to_bit b = match b with
     false -> V_lit (L_aux L_zero Unknown)
@@ -140,61 +135,38 @@ let bitwise_not_bit v =
   let lit_not (L_aux l loc) = match l with
     | L_zero -> (V_lit (L_aux L_one loc))
     | L_one  -> (V_lit (L_aux L_zero loc)) end in
-  match v with
+  retaint v (match detaint v with
   | V_lit lit -> lit_not lit
-  | V_track (V_lit lit) r -> V_track (lit_not lit) r 
-  | V_unknown -> v
-  | V_track V_unknown r -> v
-end;; 
+  | V_unknown -> V_unknown end)
 
 let rec bitwise_not v =
-  match v with
+  retaint v (match detaint v with
   | V_vector idx inc v ->
     V_vector idx inc (List.map bitwise_not_bit v)
-  | V_unknown -> v
-  | V_track bv r -> taint (bitwise_not bv) r
-end ;;
+  | V_unknown -> V_unknown end)
 
-let rec bitwise_binop_bit op op_s (V_tuple [x; y]) = match (x,y) with
-  | (V_track x rx,V_track y ry) ->
-    taint ((bitwise_binop_bit op op_s) (V_tuple[x; y])) (rx ++ ry)
-  | (V_track x rx,y) ->
-    taint ((bitwise_binop_bit op op_s) (V_tuple[x;y])) rx
-  | (x,V_track y ry) ->
-    taint ((bitwise_binop_bit op op_s) (V_tuple[x;y])) ry
+let rec bitwise_binop_bit op op_s (V_tuple [x; y]) = 
+  let b_b_b_help x y = match (x,y) with
   | (V_vector _ _ [b],y) -> bitwise_binop_bit op op_s (V_tuple [b; y])
   | (_,V_vector _ _ [b]) -> bitwise_binop_bit op op_s (V_tuple [x; b])
   | (V_unknown,_) -> V_unknown
   | (_,V_unknown) -> V_unknown
   | (V_lit (L_aux L_undef li), v) -> 
-    (match op_s with 
-      | "|" -> y
-      | "&" -> x
-      | "^" -> y
-     end )
+    (match op_s with | "|" -> y | "&" -> x | "^" -> y end )
   | (v,V_lit (L_aux L_undef li)) ->
-    (match op_s with
-      | "|" -> x
-      | "&" -> y
-      | "^" -> y
-     end)
-  | _ -> bool_to_bit (op (bit_to_bool x) (bit_to_bool y))
-end ;;
+    (match op_s with | "|" -> x | "&" -> y | "^" -> y end)
+  | _ -> bool_to_bit (op (bit_to_bool x) (bit_to_bool y)) end in
+  binary_taint b_b_b_help x y
 
 let rec bitwise_binop op op_s (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' *)
-    V_vector idx inc (List.map (fun (x,y) -> (bitwise_binop_bit op op_s (V_tuple[x; y]))) (List.zip v v'))
-  | (V_track v1 r1, V_track v2 r2) ->
-    taint (bitwise_binop op op_s (V_tuple [v1;v2])) (r1 ++ r2)
-  | (V_track v1 r1,v2) ->
-    taint (bitwise_binop op op_s (V_tuple [v1;v2])) r1
-  | (v1,V_track v2 r2) ->
-    taint (bitwise_binop op op_s (V_tuple [v1;v2])) r2
-  | (V_unknown,_) -> V_unknown
-  | (_,V_unknown) -> V_unknown
-end ;;
+  let b_b_help 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' *)
+	V_vector idx inc (List.map (fun (x,y) -> (bitwise_binop_bit op op_s (V_tuple[x; y]))) (List.zip v v'))
+      | (V_unknown,_) -> V_unknown
+      | (_,V_unknown) -> V_unknown end in
+  binary_taint b_b_help v1 v2
 
 type signed = Unsigned | Signed
 
@@ -202,127 +174,122 @@ type signed = Unsigned | Signed
  * By convention, MSB is on the left, so increasing = Big-Endian (MSB0),
  * hence MSB first.
  * http://en.wikipedia.org/wiki/Bit_numbering *)
-let rec to_num signed v = 
-  match v with
-  | (V_vector idx inc l) ->
-    if has_unknown v 
-    then V_unknown
-    else 
-  (* Word library in Lem expects bitseq with LSB first *)
-      let l = reverse l in
-  (* Make sure the last bit is a zero to force unsigned numbers *)
-      let l = (match signed with | Signed -> l | Unsigned -> l ++ [V_lit (L_aux L_zero Unknown)] end) in
-      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 ;;
+let to_num signed v = 
+  retaint v   
+    (match detaint v with
+      | (V_vector idx inc l) ->
+	if has_unknown v 
+	then V_unknown
+	else 
+      (* Word library in Lem expects bitseq with LSB first *)
+	  let l = reverse l in
+      (* Make sure the last bit is a zero to force unsigned numbers *)
+	  let l = (match signed with | Signed -> l | Unsigned -> l ++ [V_lit (L_aux L_zero Unknown)] end) in
+	  V_lit(L_aux (L_num(integerFromBitSeq (Maybe_extra.fromJust (bitSeqFromBoolList (map bit_to_bool l))))) Unknown)
+      | V_unknown -> V_unknown
+     end)
+
+let to_vec_inc (V_tuple[v1;v2]) = 
+  let tv_help v1 v2 = 
+    match (v1,v2) with
+      | (V_lit(L_aux (L_num len) _), (V_lit(L_aux (L_num n) ln))) ->
+	let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
+	V_vector 0 true (map bool_to_bit (reverse l)) 
+      | ((V_lit(L_aux (L_num n) ln)),V_unknown) -> 
+	V_vector 0 true (List.replicate (natFromInteger n) V_unknown)
+      | (_,V_unknown) -> V_unknown
+      | (V_unknown,_) -> V_unknown
+      | _ -> Assert_extra.failwith ("to_vec_inc parameters were " ^ (string_of_value (V_tuple[v1;v2])))
+  end in
+  binary_taint tv_help v1 v2
+
+let to_vec_dec (V_tuple([v1;v2])) =
+  let tv_fun v1 v2 =
+    match (v1,v2) with 
+      | (V_lit(L_aux (L_num len) _), (V_lit(L_aux (L_num n) ln))) ->
+	let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
+	V_vector (len - 1) false (map bool_to_bit (reverse l)) 
+      | ((V_lit(L_aux (L_num n) ln)),V_unknown) -> 
+	V_vector (n-1) false (List.replicate (natFromInteger n) V_unknown)
+      | (_,V_unknown) -> V_unknown
+      | (V_unknown,_) -> V_unknown
+      | _ -> Assert_extra.failwith ("to_vec_dec parameters were " ^ (string_of_value (V_tuple[v1;v2])))
+   end in
+  binary_taint tv_fun v1 v2
 
-let rec to_vec_inc (V_tuple[v1;v2]) = match (v1,v2) with
-  | (V_lit(L_aux (L_num len) _), (V_lit(L_aux (L_num n) ln))) ->
-    let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
-    V_vector 0 true (map bool_to_bit (reverse l)) 
-  | (V_track v1 r1,V_track v2 r2) -> taint (to_vec_inc (V_tuple[v1;v2])) (r1++r2)
-  | (V_track v1 r1,v2) -> taint (to_vec_inc (V_tuple[v1;v2])) r1
-  | (v1,V_track v2 r2) -> taint (to_vec_inc (V_tuple[v1;v2])) r2
-  | ((V_lit(L_aux (L_num n) ln)),V_unknown) -> 
-    V_vector 0 true (List.replicate (natFromInteger n) V_unknown)
-  | (_,V_unknown) -> V_unknown
-  | (V_unknown,_) -> V_unknown
-  | _ -> Assert_extra.failwith ("to_vec_inc parameters were " ^ (string_of_value (V_tuple[v1;v2])))
-end
-;;
-let rec to_vec_dec (V_tuple([v1;v2])) = match (v1,v2) with 
-  | (V_lit(L_aux (L_num len) _), (V_lit(L_aux (L_num n) ln))) ->
-    let l = boolListFrombitSeq (natFromInteger len) (bitSeqFromInteger Nothing n) in
-    V_vector (len - 1) false (map bool_to_bit (reverse l)) 
-  | (V_track v1 r1,V_track v2 r2) -> taint (to_vec_dec (V_tuple[v1;v2])) (r1++r2)
-  | (V_track v1 r1,v2) -> taint (to_vec_dec (V_tuple[v1;v2])) r1
-  | (v1,V_track v2 r2) -> taint (to_vec_dec (V_tuple[v1;v2])) r2
-  | ((V_lit(L_aux (L_num n) ln)),V_unknown) -> 
-    V_vector (n-1) false (List.replicate (natFromInteger n) V_unknown)
-  | (_,V_unknown) -> V_unknown
-  | (V_unknown,_) -> V_unknown
-  | _ -> Assert_extra.failwith ("to_vec_dec parameters were " ^ (string_of_value (V_tuple[v1;v2])))
-end
-;;
 let to_vec ord len n =
   if ord
   then to_vec_inc (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
   else to_vec_dec (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
 ;;
 
-let rec exts (V_tuple[v1;v]) = match v1 with
-  | V_lit(L_aux (L_num len) _) -> (match v with
-      | V_vector _ inc _  -> to_vec inc (natFromInteger len) (to_num Signed v)
-      | V_unknown -> V_unknown
-      | V_track v r2 -> taint (exts (V_tuple[v1;v])) r2 end)
-  | V_unknown -> v1
-  | V_track v1 r1 -> taint (exts (V_tuple[v1;v])) r1
-end
-;;
+let exts (V_tuple[v1;v]) = 
+  let exts_help v1 v = match (v1,v) with
+    | (V_lit(L_aux (L_num len) _), V_vector _ inc _)-> to_vec inc (natFromInteger len) (to_num Signed v)
+    | (V_lit(L_aux (L_num len) _), V_unknown) -> to_vec true (natFromInteger len) V_unknown
+    | (V_unknown,_) -> V_unknown
+  end in
+  binary_taint exts_help v1 v
+
+let eq (V_tuple [x; y]) = 
+  let combo = binary_taint (fun v _ -> v) x y in
+  retaint combo (V_lit (L_aux (if value_eq (detaint x) (detaint y) then L_one else L_zero) Unknown))
 
-let eq (V_tuple [x; y]) = V_lit (L_aux (if value_eq x y then L_one else L_zero) Unknown) ;;
 (* XXX interpret vectors as unsigned numbers for equality *)
 let eq_vec_range (V_tuple [v; r]) = eq (V_tuple [to_num Unsigned v; r]) ;;
 let eq_range_vec (V_tuple [r; v]) = eq (V_tuple [r; to_num Unsigned v]) ;;
 let eq_vec_vec (V_tuple [v;v2]) = eq (V_tuple [to_num Signed v; to_num Signed v2]);;
 
-let rec neg v = match v with
+let rec neg v = retaint v (match detaint v with
   | V_lit (L_aux arg la) -> 
     V_lit (L_aux (match arg with
       | L_one -> L_zero
       | L_zero -> L_one end) la) 
   | V_unknown -> V_unknown
-  | V_track v r -> taint (neg v) r
   | V_tuple [v] -> neg v
-end 
-;;
+end)
 
 let neq = compose neg eq ;;
 
 let neq_vec = compose neg eq_vec_vec
 
-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
-  end ;;
-let rec arith_op_vec op sign size (V_tuple args) = match args with
-  | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
-    let (l1',l2') = (to_num sign l1,to_num sign l2) in
-    let n = arith_op op (V_tuple [l1';l2']) in
-    to_vec ord ((List.length cs) * size) n
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec op sign size (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1;v2] ->
-    taint (arith_op_vec op sign size (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] ->
-    taint (arith_op_vec op sign size (V_tuple [v1;v2])) r2
-  | [V_unknown;_] -> V_unknown
-  | [_;V_unknown] -> V_unknown
-end ;;
-let rec arith_op_vec_vec_range op sign (V_tuple args) = match args with
-  | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
-    let (l1',l2') = (to_num sign l1,to_num sign l2) in
-    arith_op op (V_tuple [l1';l2'])
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec_vec_range op sign (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1;v2] ->
-    taint (arith_op_vec_vec_range op sign (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] ->
-    taint (arith_op_vec_vec_range op sign (V_tuple [v1;v2])) r2
-  | [V_unknown;_] -> V_unknown
-  | [_;V_unknown] -> V_unknown
-end ;;
-let rec arith_op_overflow_vec op sign size (V_tuple args) = match args with
-  | [(V_vector b ord cs1 as l1);(V_vector _ _ cs2 as l2)] ->
-    let act_size = (List.length cs1) * size in
-    let (is_l1_unknown,is_l2_unknown) = ((has_unknown l1), (has_unknown l2)) in
-    let (l1',l2') = (if is_l1_unknown then V_unknown else (to_num sign l1),
-                     if is_l2_unknown then V_unknown else (to_num sign l2)) in
+let arith_op op (V_tuple [vl;vr]) = 
+  let arith_op_help vl vr = 
+    match (vl,vr) 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_unknown,_) -> V_unknown
+      | (_,V_unknown) -> V_unknown
+  end in 
+  binary_taint arith_op_help vl vr
+let rec arith_op_vec op sign size (V_tuple [vl;vr]) =
+  let arith_op_help vl vr =
+    match (vl,vr) with
+      | ((V_vector b ord cs as l1),(V_vector _ _ _ as l2)) ->
+	let (l1',l2') = (to_num sign l1,to_num sign l2) in
+	let n = arith_op op (V_tuple [l1';l2']) in
+	to_vec ord ((List.length cs) * size) n
+      | (V_unknown,_) -> V_unknown
+      | (_,V_unknown) -> V_unknown
+  end in
+  binary_taint arith_op_help vl vr
+let rec arith_op_vec_vec_range op sign (V_tuple [vl;vr]) = 
+  let arith_op_help vl vr =
+    match (vl,vr) with
+      | (V_vector _ _ _,V_vector _ _ _ ) ->
+	let (l1,l2) = (to_num sign vl,to_num sign vr) in
+	arith_op op (V_tuple [l1;l2])
+      | (V_unknown,_) -> V_unknown
+      | (_,V_unknown) -> V_unknown
+   end in
+   binary_taint arith_op_help vl vr
+let rec arith_op_overflow_vec op sign size (V_tuple [vl;vr]) = 
+  let overflow_help vl vr =
+    match (vl,vr) with
+      | (V_vector b ord cs1,V_vector _ _ cs2) ->
+	let act_size = (List.length cs1) * size in
+	let (is_l1_unknown,is_l2_unknown) = ((has_unknown vl), (has_unknown vr)) in
+	let (l1',l2') = (if is_l1_unknown then V_unknown else (to_num sign vl),
+                         if is_l2_unknown then V_unknown else (to_num sign vr)) in
     let n = if is_l1_unknown || is_l2_unknown then V_unknown else arith_op op (V_tuple [l1';l2']) in
     let correct_size_num = to_vec ord act_size n in
     let overflow = if (is_l1_unknown || is_l2_unknown) then V_unknown 
@@ -331,261 +298,209 @@ let rec arith_op_overflow_vec op sign size (V_tuple args) = match args with
 	  if (n' <= (get_max_representable_in act_size)) &&
 	     (n' >= (get_min_representable_in act_size))
 	  then V_lit (L_aux L_zero ln)
-	  else V_lit (L_aux L_one ln)
-	| _ -> V_unknown end) in
+	  else V_lit (L_aux L_one ln) end) in
     let c_out = if (is_l1_unknown || is_l2_unknown) then V_unknown
-      else let detaint x = match x with | V_track v _ -> v | _ -> x end in
-      (carry_out (List.reverse (List.map detaint cs1)) (List.reverse (List.map detaint cs2)) (V_lit (L_aux L_zero Unknown))) in
+      else match to_vec ord (act_size + 1) n with
+	| V_vector _ _ (msb::vs) -> msb end in
     V_tuple [correct_size_num;overflow;c_out]
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_overflow_vec op sign size (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1;v2] ->
-    taint (arith_op_overflow_vec op sign size (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] ->
-    taint (arith_op_overflow_vec op sign size (V_tuple [v1;v2])) r2
-  | [V_unknown;_] -> V_tuple [V_unknown;V_unknown;V_unknown]
-  | [_;V_unknown] -> V_tuple [V_unknown;V_unknown;V_unknown]
-end ;;
-let rec arith_op_overflow_vec_bit op sign size (V_tuple args) = match args with
-  | [(V_vector b ord cs as l1);(V_lit (L_aux L_one li))] ->
-    let l1' = to_num sign l1 in
-    let n = arith_op op (V_tuple [l1';(V_lit (L_aux (L_num 1) li))]) in
-    let correct_size_num = to_vec ord ((List.length cs) * size) n in
-    let one_larger = to_num Signed (to_vec ord (((List.length cs) * size) +1) n) in
-    let overflow =  neq (V_tuple [correct_size_num;one_larger]) in
-    V_tuple [correct_size_num;overflow;V_lit (L_aux L_zero Unknown)]
-  | [(V_vector b ord cs as l1);(V_lit (L_aux L_zero li))] ->
-    let l1' = to_num sign l1 in
-    let n = arith_op op (V_tuple [l1';(V_lit (L_aux (L_num 0) li))]) in
-    let correct_size_num = to_vec ord ((List.length cs) * size) n in
-    let one_larger = to_num Signed (to_vec ord (((List.length cs) * size) +1) n) in
-    let overflow =  neq (V_tuple [correct_size_num;one_larger]) in
-    V_tuple [correct_size_num;overflow;V_lit (L_aux L_zero Unknown)]    
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_overflow_vec_bit op sign size (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1;v2] ->
-    taint (arith_op_overflow_vec_bit op sign size (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] ->
-    taint (arith_op_overflow_vec_bit op sign size (V_tuple [v1;v2])) r2
-  | [V_unknown;_] -> V_tuple [V_unknown;V_unknown;V_unknown]
-  | [_;V_unknown] -> V_tuple [V_unknown;V_unknown;V_unknown]
-end ;;
-
-
-let rec arith_op_range_vec op sign size (V_tuple args) = match args with
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_range_vec op sign size (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1; v2] ->
-    taint (arith_op_range_vec op sign size (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] -> 
-    taint (arith_op_range_vec op sign size (V_tuple [v1;v2])) r2
-  | [V_unknown;_] -> V_unknown
-  | [_;V_unknown] -> V_unknown
-  | [n; (V_vector _ ord cs as l2)] ->
-    arith_op_vec op sign size (V_tuple [(to_vec ord (List.length cs) n);l2])
-end ;;
-let rec arith_op_vec_range op sign size (V_tuple args) = match args with
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec_range op sign size (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1; v2] ->
-    taint (arith_op_vec_range op sign size (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] -> 
-    taint (arith_op_vec_range op sign size (V_tuple [v1;v2])) r2
-  | [V_unknown;_] -> V_unknown
-  | [_;V_unknown] -> V_unknown
-  | [(V_vector _ ord cs as l1);n] ->
-    arith_op_vec op sign size (V_tuple [l1;(to_vec ord (List.length cs) n)])
-end ;;
-let rec arith_op_range_vec_range op sign (V_tuple args) = match args with
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_range_vec_range op sign (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1; v2] ->
-    taint (arith_op_range_vec_range op sign (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] -> 
-    taint (arith_op_range_vec_range op sign (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 Unsigned l2)])
-end ;;
-let rec arith_op_vec_range_range op sign (V_tuple args) = match args with
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec_range_range op sign (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1; v2] ->
-    taint (arith_op_vec_range_range op sign (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] -> 
-    taint (arith_op_vec_range_range op sign (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 sign l1);n])
-end ;;
-let rec arith_op_vec_bit op sign size (V_tuple args) = match args with
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec_bit op sign size (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1; v2] ->
-    taint (arith_op_vec_bit op sign size (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] -> 
-    taint (arith_op_vec_bit op sign size (V_tuple [v1;v2])) r2
-  | [V_unknown;_] -> V_unknown
-  | [_;V_unknown] -> V_unknown
-  | [(V_vector _ ord cs as l1);V_lit (L_aux bit _)] ->
-    let l1' = to_num sign l1 in
-    let n = arith_op op (V_tuple 
-			   [l1';
-			    V_lit 
-			      (L_aux (L_num (match bit with | L_one -> 1 | L_zero -> 0 end)) Unknown)])
-    in
-    to_vec ord ((List.length cs) * size) n
-end 
-;;
-let rec arith_op_no0 op (V_tuple args) = match args with
-  | [V_lit(L_aux (L_num x) lx); V_lit(L_aux (L_num y) ly)] -> 
-    if y = 0 
-    then V_lit (L_aux L_undef ly)
-    else V_lit(L_aux (L_num (op x y)) lx)
-  | [V_track v1 r1;V_track v2 r2] -> taint (arith_op_no0 op (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1;v2] -> taint (arith_op_no0 op (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] -> taint (arith_op_no0 op (V_tuple [v1;v2])) r2
-  | [V_unknown;_] -> V_unknown
-  | [_;V_unknown] -> V_unknown
-  end ;;
-
-let rec arith_op_vec_no0 op op_s sign size (V_tuple args) = match args with
-  | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
-    let act_size = (List.length cs) * size in
-    let (is_l1_unknown,is_l2_unknown) = ((has_unknown l1), (has_unknown l2)) in
-    let (l1',l2') = (if is_l1_unknown then V_unknown else (to_num sign l1),
-                     if is_l2_unknown then V_unknown else (to_num sign l2)) in
-    let n = if is_l1_unknown || is_l2_unknown then V_unknown else arith_op op (V_tuple [l1';l2']) in
-    let representable = 
-      match n with 
-	| V_lit (L_aux (L_num n') ln) ->  
-	  let rep_size = (if op_s = "quot" then act_size/2 else act_size) in
-	  ((n' <= (get_max_representable_in act_size)) && (n' >= (get_min_representable_in act_size)))
-	| _ -> true end in
-    if representable then to_vec ord act_size n else to_vec ord act_size (V_lit (L_aux L_undef Unknown))
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec_no0 op op_s sign size (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1;v2] ->
-    taint (arith_op_vec_no0 op op_s sign size (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] ->
-    taint (arith_op_vec_no0 op op_s sign size (V_tuple [v1;v2])) r2
-  | [V_unknown;_] -> V_unknown
-  | [_;V_unknown] -> V_unknown
-end ;;
-let rec arith_op_overflow_vec_no0 op op_s sign size (V_tuple args) = match args with
-  | [(V_vector b ord cs as l1);(V_vector _ _ _ as l2)] ->
-    let act_size = (List.length cs) * size in
-    let (is_l1_unknown,is_l2_unknown) = ((has_unknown l1), (has_unknown l2)) in
-    let (l1',l2') = (if is_l1_unknown then V_unknown else (to_num sign l1),
-                     if is_l2_unknown then V_unknown else (to_num sign l2)) in
-    let n = if is_l1_unknown || is_l2_unknown then V_unknown else arith_op op (V_tuple [l1';l2']) in
-    let representable = 
-      match n with 
-	| V_lit (L_aux (L_num n') ln) ->  
-	  let rep_size = (if op_s = "quot" then act_size/2 else act_size) in
-	  ((n' <= (get_max_representable_in act_size)) && (n' >= (get_min_representable_in act_size)))
-	| _ -> true end in
-    let correct_size_num = if representable then to_vec ord act_size n else to_vec ord act_size (V_lit (L_aux L_undef Unknown)) in
-    let overflow = if (has_unknown l1 || has_unknown l2) then V_unknown else 
-	if representable then V_lit (L_aux L_zero Unknown) else V_lit (L_aux L_one Unknown) in
-    V_tuple [correct_size_num;overflow;V_lit (L_aux L_zero Unknown)]
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_overflow_vec_no0 op op_s sign size (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1;v2] ->
-    taint (arith_op_overflow_vec_no0 op op_s sign size (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] ->
-    taint (arith_op_overflow_vec_no0 op op_s sign size (V_tuple [v1;v2])) r2
-  | [V_unknown;_] -> V_tuple [V_unknown;V_unknown;V_unknown]
-  | [_;V_unknown] -> V_tuple [V_unknown;V_unknown;V_unknown]
-end ;;
-
-let rec arith_op_vec_range_no0 op op_s sign size (V_tuple args) = match args with
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (arith_op_vec_range_no0 op op_s sign size (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1; v2] ->
-    taint (arith_op_vec_range_no0 op op_s sign size (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] -> 
-    taint (arith_op_vec_range_no0 op op_s sign size (V_tuple [v1;v2])) r2
-  | [V_unknown;_] -> V_unknown
-  | [_;V_unknown] -> V_unknown
-  | [(V_vector _ ord cs as l1);n] ->
-    arith_op_vec_no0 op op_s sign size (V_tuple [l1;(to_vec ord (List.length cs) n)])
-end ;;
-
-let rec compare_op op (V_tuple args) = match args with
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (compare_op op (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1;v2] ->
-    taint (compare_op op (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] ->
-    taint (compare_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)] -> 
-    if (op x y)
-    then V_lit(L_aux L_one lx)
-    else V_lit(L_aux L_zero lx)
-end ;;
-let rec compare_op_vec op sign (V_tuple args) = match args with
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (compare_op_vec op sign (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1;v2] ->
-    taint (compare_op_vec op sign (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] ->
-    taint (compare_op_vec op sign (V_tuple [v1;v2])) r2
-  | [V_unknown;_] -> V_unknown
-  | [_;V_unknown] -> V_unknown
-  | [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] ->
-    let (l1',l2') = (to_num sign l1, to_num sign l2) in
-    compare_op op (V_tuple[l1';l2'])
-end ;;
-let rec compare_op_vec_unsigned op (V_tuple args) = match args with
-  | [V_track v1 r1;V_track v2 r2] ->
-    taint (compare_op_vec_unsigned op (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1;v2] ->
-    taint (compare_op_vec_unsigned op (V_tuple [v1;v2])) r1
-  | [v1;V_track v2 r2] ->
-    taint (compare_op_vec_unsigned op (V_tuple [v1;v2])) r2
-  | [V_unknown;_] -> V_unknown
-  | [_;V_unknown] -> V_unknown
-  | [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] ->
-    let (l1',l2') = (to_num Unsigned l1, to_num Unsigned l2) in
-    compare_op op (V_tuple[l1';l2'])
-end ;;
-
-
-
-let rec duplicate (V_tuple args) = match args with
-  | [V_track v1 r1;V_track v2 r2] -> taint (duplicate (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1; v2] -> taint (duplicate (V_tuple[v1;v2])) r1 
-  | [v1;V_track v2 r2] -> taint (duplicate (V_tuple[v1;v2])) r2 
-  | [V_unknown;_] -> V_unknown
-  | [_;V_unknown] -> V_unknown
-  | [(V_lit _ as v);(V_lit (L_aux (L_num n) _))] ->
-    (V_vector 0 true (List.replicate (natFromInteger n) v))
-end
-
-let rec vec_concat (V_tuple args) = match args with
-  | [V_vector n d l; V_vector n' d' l'] ->
+  | (V_unknown,_) -> V_tuple [V_unknown;V_unknown;V_unknown]
+  | (_,V_unknown) -> V_tuple [V_unknown;V_unknown;V_unknown]
+  end in
+  binary_taint overflow_help vl vr
+let rec arith_op_overflow_vec_bit op sign size (V_tuple [vl;vr]) =
+  let arith_help vl vr = 
+    match (vl,vr) with
+      | (V_vector b ord cs, V_lit (L_aux bit li)) ->
+	let act_size = (List.length cs) * size in
+	let l1' = to_num sign vl in
+	let n = 
+	  arith_op op (V_tuple [l1';(V_lit (L_aux (match bit with | L_one -> L_num 1 | L_zero -> L_num 0 end) li))]) in
+	let correct_size_num = to_vec ord act_size n in
+	let one_larger = to_vec ord (act_size +1) n in
+	let overflow = (match n with 
+	  | V_lit (L_aux (L_num n') ln) -> 
+	    if (n' <= (get_max_representable_in act_size)) &&
+	      (n' >= (get_min_representable_in act_size))
+	    then V_lit (L_aux L_zero ln)
+	    else V_lit (L_aux L_one ln) end) in
+	V_tuple [correct_size_num;overflow;(match one_larger with V_vector _ _ (c::rst) -> c end)]
+      | (V_unknown,_) -> V_tuple [V_unknown;V_unknown;V_unknown]
+      | (_,V_unknown) -> V_tuple [V_unknown;V_unknown;V_unknown]
+      end in
+   binary_taint arith_help vl vr
+
+let rec arith_op_range_vec op sign size (V_tuple [vl;vr]) = 
+  let arith_help vl vr = match (vl,vr) with
+    | (V_unknown,_) -> V_unknown
+    | (_,V_unknown) -> V_unknown
+    | (n, V_vector _ ord cs) ->
+      arith_op_vec op sign size (V_tuple [(to_vec ord (List.length cs) n);vr])
+  end in
+  binary_taint arith_help vl vr
+let rec arith_op_vec_range op sign size (V_tuple [vl;vr]) = 
+  let arith_help vl vr = match (vl,vr) with
+    | (V_unknown,_) -> V_unknown
+    | (_,V_unknown) -> V_unknown
+    | (V_vector _ ord cs,n) ->
+      arith_op_vec op sign size (V_tuple [vl;(to_vec ord (List.length cs) n)])
+  end in
+  binary_taint arith_help vl vr
+let rec arith_op_range_vec_range op sign (V_tuple [vl;vr]) =
+  let arith_help vl vr = match (vl,vr) with
+    | (V_unknown,_) -> V_unknown
+    | (_,V_unknown) -> V_unknown
+    | (n,V_vector _ ord _) ->
+      arith_op op (V_tuple [n;(to_num Unsigned vr)])
+  end in
+  binary_taint arith_help vl vr
+let arith_op_vec_range_range op sign (V_tuple [vl;vr]) = 
+  let arith_help vl vr = match (vl,vr) with
+    | (V_unknown,_) -> V_unknown
+    | (_,V_unknown) -> V_unknown
+    | (V_vector _ ord _ ,n) ->
+      arith_op op (V_tuple [(to_num sign vl);n])
+   end in
+   binary_taint arith_help vl vr
+let rec arith_op_vec_bit op sign size (V_tuple [vl;vr]) =
+  let arith_help vl vr =
+    match (vl,vr) with
+      | (V_unknown,_) -> V_unknown
+      | (_,V_unknown) -> V_unknown
+      | (V_vector _ ord cs,V_lit (L_aux bit _)) ->
+	let l1' = to_num sign vl in
+	let n = arith_op op (V_tuple 
+			       [l1';
+				V_lit 
+				  (L_aux (L_num (match bit with | L_one -> 1 | L_zero -> 0 end)) Unknown)])
+	in
+	to_vec ord ((List.length cs) * size) n
+      end in
+   binary_taint arith_help vl vr 
+
+let rec arith_op_no0 op (V_tuple [vl;vr]) = 
+  let arith_help vl vr =
+    match (vl,vr) with
+      | (V_lit(L_aux (L_num x) lx), V_lit(L_aux (L_num y) ly)) -> 
+	if y = 0 
+	then V_lit (L_aux L_undef ly)
+	else V_lit(L_aux (L_num (op x y)) lx)
+      | (V_unknown,_) -> V_unknown
+      | (_,V_unknown) -> V_unknown
+  end in 
+  binary_taint arith_help vl vr
+
+let rec arith_op_vec_no0 op op_s sign size (V_tuple [vl;vr]) = 
+  let arith_help vl vr = 
+    match (vl,vr) with
+      | (V_vector b ord cs, V_vector _ _ _) ->
+	let act_size = (List.length cs) * size in
+	let (is_l1_unknown,is_l2_unknown) = ((has_unknown vl), (has_unknown vr)) in
+	let (l1',l2') = (if is_l1_unknown then V_unknown else (to_num sign vl),
+                         if is_l2_unknown then V_unknown else (to_num sign vr)) in
+	let n = if is_l1_unknown || is_l2_unknown then V_unknown else arith_op op (V_tuple [l1';l2']) in
+	let representable = 
+	  match n with 
+	    | V_lit (L_aux (L_num n') ln) ->  
+	      let rep_size = (if op_s = "quot" then act_size/2 else act_size) in
+	      ((n' <= (get_max_representable_in act_size)) && (n' >= (get_min_representable_in act_size)))
+	    | _ -> true end in
+         if representable 
+	 then to_vec ord act_size n else to_vec ord act_size (V_lit (L_aux L_undef Unknown))
+      | (V_unknown,_) -> V_unknown
+      | (_,V_unknown) -> V_unknown
+   end in
+   binary_taint arith_help vl vr
+let rec arith_op_overflow_vec_no0 op op_s sign size (V_tuple [vl;vr]) =
+  let arith_help vl vr = 
+    match (vl,vr) with
+      | (V_vector b ord cs, V_vector _ _ _) ->
+	let act_size = (List.length cs) * size in
+	let (is_l1_unknown,is_l2_unknown) = ((has_unknown vl), (has_unknown vr)) in
+	let (l1',l2') = (if is_l1_unknown then V_unknown else (to_num sign vl),
+                         if is_l2_unknown then V_unknown else (to_num sign vr)) in
+	let n = if is_l1_unknown || is_l2_unknown then V_unknown else arith_op op (V_tuple [l1';l2']) in
+	let representable = 
+	  match n with 
+	    | V_lit (L_aux (L_num n') ln) ->  
+	      let rep_size = (if op_s = "quot" then act_size/2 else act_size) in
+	      ((n' <= (get_max_representable_in act_size)) && (n' >= (get_min_representable_in act_size)))
+	    | _ -> true end in
+        let correct_size_num = 
+	  if representable then to_vec ord act_size n else to_vec ord act_size (V_lit (L_aux L_undef Unknown)) in
+	let overflow = if is_l1_unknown || is_l2_unknown then V_unknown else 
+	    if representable then V_lit (L_aux L_zero Unknown) else V_lit (L_aux L_one Unknown) in
+	V_tuple [correct_size_num;overflow;V_lit (L_aux L_zero Unknown)]
+	| (V_unknown,_) -> V_tuple [V_unknown;V_unknown;V_unknown]
+	| (_,V_unknown) -> V_tuple [V_unknown;V_unknown;V_unknown]
+   end in
+  binary_taint arith_help vl vr
+
+let rec arith_op_vec_range_no0 op op_s sign size (V_tuple [vl;vr]) =
+  let arith_help vl vr =
+    match (vl,vr) with
+      | (V_unknown,_) -> V_unknown
+      | (_,V_unknown) -> V_unknown
+      | (V_vector _ ord cs,n) ->
+	arith_op_vec_no0 op op_s sign size (V_tuple [vl;(to_vec ord (List.length cs) n)])
+  end in
+  binary_taint arith_help vl vr
+
+let rec compare_op op (V_tuple [vl;vr]) =
+  let comp_help vl vr = match (vl,vr) with
+    | (V_unknown,_) -> V_unknown
+    | (_,V_unknown) -> V_unknown
+    | (V_lit(L_aux (L_num x) lx), V_lit(L_aux (L_num y) ly)) -> 
+      if (op x y)
+      then V_lit(L_aux L_one lx)
+      else V_lit(L_aux L_zero lx)
+   end in
+   binary_taint comp_help vl vr
+let rec compare_op_vec op sign (V_tuple [vl;vr]) = 
+  let comp_help vl vr = match (vl,vr) with
+    | (V_unknown,_) -> V_unknown
+    | (_,V_unknown) -> V_unknown
+    | (V_vector _ _ _,V_vector _ _ _) ->
+      let (l1',l2') = (to_num sign vl, to_num sign vr) in
+      compare_op op (V_tuple[l1';l2'])
+   end in
+   binary_taint comp_help vl vr
+let rec compare_op_vec_unsigned op (V_tuple [vl;vr]) = 
+  let comp_help vl vr = match (vl,vr) with
+    | (V_unknown,_) -> V_unknown
+    | (_,V_unknown) -> V_unknown
+    | (V_vector _ _ _,V_vector _ _ _) ->
+      let (l1',l2') = (to_num Unsigned vl, to_num Unsigned vr) in
+      compare_op op (V_tuple[l1';l2'])
+  end in
+  binary_taint comp_help vl vr
+
+let duplicate (V_tuple [vl;vr]) = 
+  let dup_help vl vr =
+    match (vl,vr) with
+      | ((V_lit _ as v),(V_lit (L_aux (L_num n) _))) ->
+	V_vector 0 true (List.replicate (natFromInteger n) v)
+      | (V_unknown,(V_lit (L_aux (L_num n) _))) ->
+	V_vector 0 true (List.replicate (natFromInteger n) V_unknown)
+      | (V_unknown,_) -> V_unknown
+    end in
+  binary_taint dup_help vl vr
+
+let rec vec_concat (V_tuple [vl;vr]) = 
+  let concat_help vl vr = 
+    match (vl,vr) with
+      | (V_vector n d l, V_vector n' d' l') ->
       (* XXX d = d' ? dropping n' ? *)
-      V_vector n d (l ++ l')
-  | [V_lit l; (V_vector n d l' as x)] -> vec_concat (V_tuple [litV_to_vec l d; x])
-  | [(V_vector n d l' as x); V_lit l] -> vec_concat (V_tuple [x; litV_to_vec l d]) 
-  | [V_track v1 r1;V_track v2 r2] -> taint (vec_concat (V_tuple [v1;v2])) (r1++r2)
-  | [V_track v1 r1; v2] -> taint (vec_concat (V_tuple[v1;v2])) r1 
-  | [v1; V_track v2 r2] -> taint (vec_concat (V_tuple[v1;v2])) r2 
-  | [V_unknown;_] -> V_unknown
-  | [_;V_unknown] -> V_unknown
-  
-  end ;;
-
-let rec v_length v = match v with
+	V_vector n d (l ++ l')
+      | (V_lit l, (V_vector n d l' as x)) -> vec_concat (V_tuple [litV_to_vec l d; x])
+      | ((V_vector n d l' as x), V_lit l) -> vec_concat (V_tuple [x; litV_to_vec l d]) 
+      | (V_unknown,_) -> V_unknown
+      | (_,V_unknown) -> V_unknown
+  end in
+  binary_taint concat_help vl vr
+
+let v_length v = retaint v (match detaint v with
   | V_vector n d l -> V_lit (L_aux (L_num (integerFromNat (List.length l))) Unknown)
-  | V_unknown -> V_unknown
-  | V_track v r -> taint (v_length v) r
-end ;;
+  | V_unknown -> V_unknown end)
 
 let function_map = [
   ("ignore", ignore_sail);