taint tracking through most of interpreter

Need to add cases for tracking a taint past a conditional check where possible; and then to actually generate them from reading registers.

1 files changed, 159 insertions, 98 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 9cf0e41d..201bd0cc 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -346,6 +346,13 @@ let list_nth l n = List_extra.nth l (natFromInteger n)
 val list_length : forall 'a . list 'a -> integer
 let list_length l = integerFromNat (List.length l)
 
+val taint: value -> list reg_form -> value
+let taint value regs = 
+  match value with 
+  | V_track value rs -> V_track value (regs ++ rs)
+  | _ -> V_track value regs
+end
+
 val access_vector : value -> integer -> value
 let rec access_vector v n =
   match v with
@@ -502,9 +509,9 @@ let rec fupdate_vector_slice vec replace start 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_track v r, V_track vr rr) -> (V_track (fupdate_vector_slice v vr start stop) (r++rr))
-  | (V_track v r, replace) -> V_track (fupdate_vector_slice v replace start stop) r
-  | (vec, V_track vr rr) -> V_track (fupdate_vector_slice vec vr start stop) rr
+  | (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
   end
 
 val in_ctors : list (id * typ) -> id -> maybe typ
@@ -745,7 +752,7 @@ let rec find_function (Defs defs) id =
 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 v = 
+  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
@@ -787,7 +794,7 @@ let rec match_pattern (P_aux p _) value_whole =
      then foldr2
           (fun pat value (matched_p,used_unknown,bounds) ->
             if matched_p then
-              let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint value) in
+              let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat value) in
               (matched_p, (used_unknown || used_unknown'), (union_env new_bounds bounds))
             else (false,false,eenv)) (true,false,eenv) pats vals
      else (false,false,eenv)
@@ -796,7 +803,7 @@ let rec match_pattern (P_aux p _) value_whole =
      then foldr2
           (fun pat value (matched_p,used_unknown,bounds) ->
             if matched_p then
-              let (matched_p,used_unknown',new_bounds) = match_pattern pat (V_track value r) in
+              let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint value r) in
               (matched_p, (used_unknown || used_unknown'), (union_env new_bounds bounds))
             else (false,false,eenv)) (true,false,eenv) pats vals
      else (false,false,eenv)
@@ -833,7 +840,7 @@ let rec match_pattern (P_aux p _) value_whole =
      then foldr2
        (fun pat value (matched_p,used_unknown,bounds) -> 
 	 if matched_p then
-	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint value) in
+	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat value) in
 	   (matched_p, (used_unknown||used_unknown'), (union_env new_bounds bounds))
 	 else (false,false,eenv))
        (true,false,eenv) (if inc then pats else List.reverse pats) vals
@@ -847,7 +854,7 @@ let rec match_pattern (P_aux p _) value_whole =
 		then let (matched_p,used_unknown',new_bounds) = 
 		       match_pattern pat (match List.lookup i vals with
 			 | Nothing -> d
-			 | Just v  -> (taint v) end) in
+			 | Just v  -> (taint_pat v) end) in
 		     ((if inc then i+1 else i-1),matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
                 else (i,false,false,eenv)) (n,true,false,eenv) pats in
 	  (matched_p,used_unknown,bounds)
@@ -861,7 +868,7 @@ let rec match_pattern (P_aux p _) value_whole =
      let v_len = if inc then list_length vals + n else n - list_length vals in
      List.foldr
        (fun (i,pat) (matched_p,used_unknown,bounds) -> if matched_p && i < v_len then
-	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint (list_nth vals (if inc then i+n else i-n))) in
+	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat (list_nth vals (if inc then i+n else i-n))) in
 	   (matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
          else (false,false,eenv))
        (true,false,eenv) ipats
@@ -869,7 +876,7 @@ let rec match_pattern (P_aux p _) value_whole =
      List.foldr
        (fun (i,pat) (matched_p,used_unknown,bounds) -> if matched_p && i < m then
 	   let (matched_p,used_unknown',new_bounds) = 
-             match_pattern pat (match List.lookup i vals with | Nothing -> d | Just v -> (taint v) end) in
+             match_pattern pat (match List.lookup i vals with | Nothing -> d | Just v -> (taint_pat v) end) in
 	   (matched_p,used_unknown||used_unknown',(union_env new_bounds bounds))
 	 else (false,false,eenv))
        (true,false,eenv) ipats
@@ -894,7 +901,7 @@ let rec match_pattern (P_aux p _) value_whole =
      if ((List.length pats)= (List.length vals))
      then foldr2 
        (fun pat v (matched_p,used_unknown,bounds) -> if matched_p then
-	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint v) in
+	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat v) in
 	   (matched_p,used_unknown ||used_unknown', (union_env bounds new_bounds))
 	 else (false,false,eenv))
        (true,false,eenv) pats vals
@@ -908,7 +915,7 @@ let rec match_pattern (P_aux p _) value_whole =
      if ((List.length pats)= (List.length vals))
      then foldr2 
        (fun pat v (matched_p,used_unknown,bounds) -> if matched_p then
-	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint v) in
+	   let (matched_p,used_unknown',new_bounds) = match_pattern pat (taint_pat v) in
 	   (matched_p,used_unknown|| used_unknown', (union_env bounds new_bounds))
 	 else (false,false,eenv))
        (true,false,eenv) pats vals
@@ -1064,12 +1071,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	    (*Cast is changing vector start position, potentially*)
 	    | (_,V_vector start inc items) -> update_vector_start start (fun i -> (V_vector i inc items))
 	    | (_,V_track (V_vector start inc items) regs) -> 
-	      update_vector_start start (fun i -> (V_track (V_vector i inc items) regs))
+	      update_vector_start start (fun i -> (taint (V_vector i inc items) regs))
 	    (*TODO trim items below if i > (or < for dec) start *)
 	    | (_,V_vector_sparse start inc len items def) -> 
 	      update_vector_start start (fun i -> (V_vector_sparse i inc len items def)) 
 	    | (_,V_track (V_vector_sparse start inc len items def) regs) ->
-	      update_vector_start start (fun i -> (V_track (V_vector_sparse i inc len items def) regs))
+	      update_vector_start start (fun i -> (taint (V_vector_sparse i inc len items def) regs))
 	    | _ -> (Value v,lm,le) end))
 	(fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_cast ctyp e) (l,annot), env))))
     | E_id id -> 
@@ -1309,13 +1316,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                     | V_vector _ _ _ -> (Value (access_vector vvec n),lm,le)
 		    | V_track ((V_vector _ _ _) as vvec) r ->
 		      (match iv_whole with
-			| V_track _ ir -> (Value (V_track (access_vector vvec n) (r++ir)),lm,le)
-			| _ -> (Value (V_track (access_vector vvec n) r),lm,le) end)
+			| 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 (V_track (access_vector vvec n) (r++ir)),lm,le)
-			| _ -> (Value (V_track (access_vector vvec n) r),lm,le) end)
+			| 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)
                     | _ -> (Error l "Vector access of non-vector",lm,le)end)
                 (fun a ->		  
@@ -1364,13 +1371,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			    | (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 (V_track (slice_vector vvec n1 n2) tr), lm,le)
+				| (V_vector _ _ _,tr) -> (Value (taint (slice_vector vvec n1 n2) tr), lm,le)
 				| (V_track ((V_vector _ _ _) as vvec) r,_) -> 
-				  (Value (V_track (slice_vector vvec n1 n2) (r++tracking)), lm,le)
+				  (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 (V_track (slice_vector vvec n1 n2) tr),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 (V_track (slice_vector vvec n1 n2) (r++tracking)), lm,le)
+				  (Value (taint (slice_vector vvec n1 n2) (r++tracking)), lm,le)
 				| (V_unknown,_) -> (Value V_unknown,lm,le)
 				| _ -> (Error l "Vector slice of non-vector",lm,le) end)
 			 end)
@@ -1408,10 +1415,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                       match (vec,tracking) with
                         | (V_vector _ _ _,[]) -> (Value (fupdate_vec vec n1 vup), lm,le)
 			| (V_track ((V_vector _ _ _) as vvec) r, tracking) ->
-			  (Value (V_track (fupdate_vec vec n1 vup) (r++tracking)),lm,le)
+			  (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 (V_track (fupdate_vec vec n1 vup) (r++tracking)),lm,le)
+			  (Value (taint (fupdate_vec vec n1 vup) (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 
@@ -1438,7 +1445,7 @@ 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 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
+		  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_lit (L_aux (L_num n2) ln2) ->
                       resolve_outcome 
@@ -1449,19 +1456,22 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                              (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 (V_track (fupdate_vector_slice vvec v_rep n1 n2) (r++tracking)),lm,le)
+				   (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)
                                  | _ -> (Error l "Vector update requires vector",lm,le) end)
                              (fun a -> update_stack a 
                                (add_to_top_frame 
 				  (fun v env -> 
                                     let (e_rep,env') = to_exp mode env v_rep in
-                                    (E_aux (E_vector_update_subrange v 
-					      (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
-					      (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)) 
-					      e_rep) (l,annot), env'))))))
+                                    let (ei1, env') = to_exp mode env' vi1_whole in
+                                    let (ei2, env') = to_exp mode env' vi2_whole in
+                                    (E_aux (E_vector_update_subrange v ei1 ei2 e_rep) (l,annot), env'))))))
                         (fun a -> update_stack a 
                           (add_to_top_frame 
 			     (fun e env -> 
@@ -1481,20 +1491,36 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     | E_vector_append e1 e2 ->
       resolve_outcome 
 	(interp_main mode t_level l_env l_mem e1)
-        (fun v1 lm le ->
+        (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 ->
               (resolve_outcome 
 		 (interp_main mode t_level l_env lm e2)
                  (fun v2 lm le ->
-                   match v2 with
-                     | V_vector _ _ vals2 -> (Value (V_vector m inc (vals1++vals2)),lm,l_env)
-		     | V_vector_sparse _ len _ vals2 d ->
+                   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 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_unknown -> (Value V_unknown,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_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 -> 
@@ -1504,15 +1530,29 @@ 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 e2)
                  (fun v2 lm le ->
-                   match v2 with
-                     | V_vector _ _ vals2 -> 
+                   match (v2,tracking) with
+                     | (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_sparse _ new_len _ vals2 _ ->
+                     | (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_unknown -> (Value V_unknown,lm,l_env)
+                     | (V_vector_sparse _ new_len _ vals2 _, 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) 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_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
@@ -1557,9 +1597,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
       (Action (Nondet exps) 
 	      (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)
     | E_app f args ->
-      (match (exp_list mode t_level (fun es -> E_aux (E_app f es) (l,annot)) 
-		               (fun vs -> match vs with | [] -> V_lit (L_aux L_unit l) | [v] -> v | vs -> V_tuple vs end) 
-			       l_env l_mem [] args) with
+      (match (exp_list mode t_level 
+                (fun es -> E_aux (E_app f es) (l,annot)) 
+		(fun vs -> match vs with | [] -> V_lit (L_aux L_unit l) | [v] -> v | vs -> V_tuple vs end) 
+		l_env l_mem [] args) with
       | (Value v,lm,le) -> 
         let name = get_id f in 
         (match tag with
@@ -1570,9 +1611,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 		| [] -> 
 		  (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
 		| [(env,used_unknown,exp)] -> 
-		  resolve_outcome (if mode.eager_eval 
-		    then (interp_main mode t_level env emem exp)
-		    else (debug_out exp t_level emem env))  
+		  resolve_outcome 
+                    (if mode.eager_eval 
+		     then (interp_main mode t_level env emem exp)
+		     else (debug_out 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_of_string "0") 
@@ -1582,7 +1624,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                   let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in
                   interp_main mode t_level l_env l_mem (E_aux (E_block lets) (l,annot))
                end)
-          | Nothing -> (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
+            | Nothing -> (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
 	| Tag_empty -> 
 	  (match find_function defs f with
 	  | Just(funcls) -> 
@@ -1590,14 +1632,15 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	    | [] -> 
               (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env)
 	    | [(env,used_unknown,exp)] -> 
-	      resolve_outcome (if mode.eager_eval 
-		               then (interp_main mode t_level env emem exp)
-		               else (debug_out 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_of_string "0") 
-						          (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
-							  t_level l_env l_mem stack)))
+	      resolve_outcome 
+                (if mode.eager_eval 
+		 then (interp_main mode t_level env emem exp)
+		 else (debug_out 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_of_string "0") 
+				   (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
+				   t_level l_env l_mem stack)))
              end)
           | Nothing -> (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
 	| Tag_spec ->  
@@ -1613,7 +1656,9 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                  else (debug_out 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_of_string "0") (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot))) t_level l_env l_mem stack)))
+		  (fun stack -> 
+                    (Hole_frame (id_of_string "0") 
+                                (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot))) t_level l_env l_mem stack)))
              end)
           | Nothing -> (Error l (String.stringAppend "Specified function must be defined before executing " name),lm,le) end)
         | Tag_ctor ->
@@ -1743,7 +1788,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 		  | _ -> update_stack a (add_to_top_frame 
 					   (fun e env -> 
                                              let (ev,env') = (to_exp mode env v) in
-                                             (E_aux (E_assign (lexp_builder e) ev) (l,annot),env'))) end))
+                                             let (lexp,env') = (lexp_builder e env') in
+                                             (E_aux (E_assign lexp ev) (l,annot),env'))) end))
 	 end))
       (fun a -> update_stack a (add_to_top_frame (fun v env -> (E_aux (E_assign lexp v) (l,annot), env))))
   end
@@ -1766,7 +1812,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     end
 
 (*TODO The rebuilder function should take an environment and thread through as in to_exp and add_to_top_frame *)
-and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) =
+and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) : ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv))) =
    let (Env defs lets regs ctors subregs aliases) = t_level in
   let (typ,tag,ncs,ef) = match annot with 
     | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
@@ -1779,7 +1825,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	    | (V_boxref n t) -> 
 	      if is_top_level 
 	      then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
-	      else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_id id) (l,annot)))
+	      else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
 	    | V_unknown ->
 	      if is_top_level then
 		let (LMem c m) = l_mem in
@@ -1787,21 +1833,22 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		((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)
             | 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 -> LEXP_aux(LEXP_id id) (l,annot)))
+	      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)))
 	     end 
         | Tag_global -> 	     
 	  (match in_env lets id with
 	    | 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 -> LEXP_aux(LEXP_id id) (l,annot)))
+	      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)
 	   end)
         | Tag_extern _ ->
 	  let regf = Reg id annot in
-	  let request = (Action (Write_reg regf Nothing 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) else (request,Just (fun e -> LEXP_aux (LEXP_id id) (l,annot)))
+	  let request = 
+            (Action (Write_reg regf Nothing 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) else (request,Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
 	| Tag_alias -> 
 	  let request = 
 	    (match in_env aliases id with
@@ -1813,7 +1860,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 			(match in_env indexes subreg with
 			  | Just ir -> 
 			    (Action (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing value) 
-			       (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+			            (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)
 			  | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
 		      | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " id), l_mem, l_env) end)
@@ -1823,7 +1870,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 			(match in_env indexes subreg with
 			  | Just ir -> 
 			    (Action (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing value) 
-			       (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+			            (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)
 			  | _ -> (Error l "Internal error, alias spec has unknown field", l_mem, l_env) end)
 		      | _ -> (Error l (String.stringAppend "Internal error: alias spec has unknown register type " id), l_mem, l_env) end)
@@ -1832,7 +1879,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		      (fun v le lm -> match v with 
 			| V_lit (L_aux (L_num i) _) -> 
 			  (Action (Write_reg (Reg reg annot') (Just (i,i)) value) 
-			     (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+			          (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) end)
 		      (fun a -> a)
 		  | AL_slice (RI_aux (RI_id reg) (_,annot')) start stop -> 
@@ -1878,11 +1925,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
           let request = (Action (Write_mem id v Nothing value) 
                                 (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env lm Top),lm,l_env) in
           if is_top_level then (request,Nothing) 
-	  else (request,Just (fun e -> 
-	                       (LEXP_aux (LEXP_memory id 
-                                            (fst (to_exps mode eenv (match v with | V_tuple vs -> vs | v -> [v]end)))) (l,annot))))
+	  else 
+            (request,
+             Just (fun e env->
+               let (parms,env) = (to_exps mode env (match v with | V_tuple vs -> vs | v -> [v] end)) in
+	       (LEXP_aux (LEXP_memory id parms) (l,annot), env)))
          end)
-      | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) -> (LEXP_aux (LEXP_memory id es) (l,annot))))
+      | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) env -> (LEXP_aux (LEXP_memory id es) (l,annot), env)))
       | e -> (e,Nothing) end
     | LEXP_cast typc id -> 
       match tag with
@@ -1891,7 +1940,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	    | V_boxref n t -> 
 	      if is_top_level 
 	      then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
-	      else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_cast typc id) (l,annot)))
+	      else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
 	    | V_unknown -> 	  
 	      if is_top_level 
               then begin
@@ -1902,27 +1951,32 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
               else ((Error l (String.stringAppend "Undefined 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 -> LEXP_aux(LEXP_cast typc id) (l,annot)))
+	      else ((Value v,l_mem,l_env),Just (fun e env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env)))
           end 
         | Tag_extern _ ->
 	  let regf = Reg id annot in
 	  let request = (Action (Write_reg regf Nothing 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) else (request,Just (fun e -> LEXP_aux (LEXP_cast typc id) (l,annot)))
+          if is_top_level then (request,Nothing) else (request,Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
         | _ -> ((Error l (String.stringAppend "Internal error: writing to id with tag other than extern or empty " (get_id id)),l_mem,l_env),Nothing)
       end 
     | LEXP_vector lexp exp -> 
       match (interp_main mode t_level l_env l_mem exp) with
-      | (Value i,lm,le) ->
+      | (Value i_whole,lm,le) ->
+        let i = match i_whole with | V_track v _ -> v | _ -> i_whole end in
         (match i with 
         | V_lit (L_aux (L_num n) ln) -> 
-          let next_builder le_builder = (fun e -> 
-	                                  LEXP_aux (LEXP_vector (le_builder e) (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)) in
+          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
+	      (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,lm,le),maybe_builder) ->
+          | ((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
             (match v with 
             | V_vector inc m vs -> 
-              let nth = access_vector v n in
               (match (nth,is_top_level,maybe_builder) with
 	      | (V_register regform,true,_) ->
 		((Action (Write_reg regform Nothing value)
@@ -1936,7 +1990,6 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
               | ((V_boxref n t),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
               | (v,false, Just lexp_builder) -> ((Value v,lm,le), Just (next_builder lexp_builder)) end)
 	    | V_vector_sparse n m inc vs d ->
-              let nth = access_vector v n in
               (match (nth,is_top_level,maybe_builder) with
 		| (V_register regform,true,_) ->
 		  ((Action (Write_reg regform Nothing value)
@@ -1961,21 +2014,25 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
            | _ -> ((Action a s,lm,le), Just (next_builder lexp_builder)) end)
          | e -> e end)
         | _ -> ((Error l "Vector access must be a number",lm,le),Nothing) end)
-      | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e -> (LEXP_aux (LEXP_vector lexp e) (l,annot))))
+      | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector lexp e) (l,annot), env)))
       | e -> (e,Nothing) end
     | LEXP_vector_range lexp exp1 exp2  ->
       match (interp_main mode t_level l_env l_mem exp1) with
-      | (Value i1, lm, le) ->
+      | (Value i1_whole, lm, le) ->
+        let i1 = match i1_whole with | V_track v _ -> v | _ -> i1_whole end in
         (match i1 with
         | V_lit (L_aux (L_num n1) ln1) ->
           (match (interp_main mode t_level l_env l_mem exp2) with
-          | (Value i2,lm,le) ->
+          | (Value i2_whole,lm,le) ->
+            let i2 = match i2_whole with | V_track v _ -> v | _ -> i2_whole end in
             (match i2 with
             | V_lit (L_aux (L_num n2) ln2) ->
               let next_builder le_builder = 
-		(fun e -> LEXP_aux (LEXP_vector_range (le_builder e) 
-				                      (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing))
-						      (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing))) (l,annot)) in
+		(fun e env -> 
+                  let (e1,env) = to_exp mode env i1_whole in
+                  let (e2,env) = to_exp mode env i2_whole 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,lm,le), Just lexp_builder) ->
                 (match (v,is_top_level) with
@@ -1993,36 +2050,40 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
               | e -> e end)
             | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing) end)
           | (Action a s,lm,le) ->
-            ((Action a s,lm, le), Just (fun e -> LEXP_aux (LEXP_vector_range lexp 
-							                     (E_aux (E_lit (L_aux (L_num  n1) ln1)) (ln1,Nothing))
-									     e) (l,annot)))
+            ((Action a s,lm, le), 
+             Just (fun e env -> 
+               let (e1,env) = to_exp mode env i1_whole 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)
       | (Action a s,lm,le) ->
-        ((Action a s, lm,le), Just (fun e -> LEXP_aux (LEXP_vector_range lexp e exp2) (l,annot)))
+        ((Action a s, lm,le), Just (fun e env -> (LEXP_aux (LEXP_vector_range lexp e exp2) (l,annot), env)))
       | e -> (e,Nothing) end
    | LEXP_field lexp id ->
      (match (create_write_message_or_update mode t_level value l_env l_mem false lexp) with
      | ((Value (V_record t fexps),lm,le),Just lexp_builder) ->
+       let next_builder = Just (fun e env -> let (lexp,env) = (lexp_builder e env) in 
+                                             (LEXP_aux (LEXP_field lexp id) (l,annot), env)) in
        match (in_env fexps id,is_top_level) with
        | (Just (V_boxref n t),true) -> ((Value (V_lit (L_aux L_unit l)), update_mem lm n value, l_env),Nothing)
-       | (Just (V_boxref n t),false) -> 
-	 ((Value (in_mem lm n),lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+       | (Just (V_boxref n t),false) -> ((Value (in_mem lm n),lm,l_env),next_builder)
        | (Just v, true) -> ((Error l "Mutating a field access requires a reg type",lm,le),Nothing)
-       | (Just v,false) -> ((Value v,lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+       | (Just v,false) -> ((Value v,lm,l_env),next_builder)
        | (Nothing,_) -> ((Error l "Field not found in specified record",lm,le),Nothing) end
      | ((Action a s,lm,le), Just lexp_builder) ->  
+       let next_builder = Just (fun e env -> let (lexp,env) = (lexp_builder e env) in 
+                                             (LEXP_aux (LEXP_field lexp id) (l,annot), env)) in
        match a with
-       | Read_reg _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
-       | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
-       | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot)))
+       | Read_reg _ _ -> ((Action a s,lm,le), next_builder)
+       | Read_mem _ _ _ -> ((Action a s,lm,le), next_builder)
+       | Call_extern _ _ -> ((Action a s,lm,le), next_builder)
        | Write_reg ((Reg _ (Just(T_id id',_,_,_))) as regf) Nothing value -> 
 	 match in_env subregs (Id_aux (Id id') Unknown) with
 	   | Just(indexes) ->
 	     match in_env indexes id with
 	       | Just ir -> 
 		 ((Action (Write_reg (SubReg id regf ir) Nothing value) s,lm,le), 
-		  (if is_top_level then Nothing else Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))))
+		  (if is_top_level then Nothing else next_builder))
 	       | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
 		 end 
             | Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing) end
@@ -2032,7 +2093,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	     match in_env indexes id with
 	       | Just ir -> 
 		 ((Action (Write_reg (SubReg id regf ir) Nothing value) s,lm,le), 
-		  (if is_top_level then Nothing else Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))))
+		  (if is_top_level then Nothing else next_builder))
 	       | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
 		 end 
             | Nothing -> ((Error l "Internal error, unrecognized write, no subreges",lm,le),Nothing) end