Merge branch 'master' of bitbucket.org:Peter_Sewell/l2

4 files changed, 172 insertions, 84 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index fef8c170..3e125b99 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -396,7 +396,7 @@ end
 val access_vector : value -> integer -> value
 let rec access_vector v n =
   match v with
-  | V_unknown -> V_unknown (*Likely shoud be unreachable*)
+  | V_unknown -> V_unknown 
   | V_vector m inc vs -> 
     if inc then
     list_nth vs (n - m)
@@ -572,7 +572,7 @@ let rec update_vector_slice vector value start stop mem =
   | (V_track v1 r1, v) -> (update_vector_slice v1 value start stop mem) 
 end
 
-let rec update_vector_start new_start v = match v with
+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 _) ->
@@ -580,9 +580,10 @@ let rec update_vector_start new_start v = match v with
   | 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_unknown
+  | V_unknown -> 
+    V_vector new_start true (List.replicate (natFromInteger expected_size) V_unknown)
   | V_lit (L_aux L_undef _) -> v
-  | V_track v r -> taint (update_vector_start new_start v) r
+  | V_track v r -> taint (update_vector_start new_start expected_size v) r
 end
 
 val in_ctors : list (id * typ) -> id -> maybe typ
@@ -752,8 +753,9 @@ let rec to_exp mode env v : (exp tannot * lenv) =
   | V_vector_sparse n m inc vals d ->
     let ((es : (list (exp tannot))),env') = mapf (List.map (fun (i,v) -> v) vals) env in
     let ((d : (exp tannot)),env')  = to_exp mode env' d in
-    (E_aux (E_vector_indexed ((if inc then List.reverse else (fun i -> i)) (List.map (fun ((i,v), e) -> (i, e)) (List.zip vals es)))
-	                     (Def_val_aux (Def_val_dec d) (Interp_ast.Unknown, Nothing))) annot, env')
+    (E_aux (E_vector_indexed 
+	      ((if inc then List.reverse else (fun i -> i)) (List.map (fun ((i,v), e) -> (i, e)) (List.zip vals es)))
+	      (Def_val_aux (Def_val_dec d) (Interp_ast.Unknown, Nothing))) annot, env')
   | V_record t ivals -> 
     let (es,env') = mapf (List.map (fun (i,v) -> v) ivals) env in
     (E_aux (E_record(FES_aux (FES_Fexps
@@ -771,7 +773,9 @@ let rec to_exp mode env v : (exp tannot * lenv) =
       if mode.track_values 
       then begin let (fid,env') = fresh_var env in
                  let env' = add_to_env (fid,vals) env' in
-                 (E_aux (E_app id [(E_aux (E_id fid) (Interp_ast.Unknown, (val_annot (val_typ vals))))]) (mk_annot true), env')
+                 (E_aux 
+		    (E_app id [(E_aux (E_id fid) (Interp_ast.Unknown, (val_annot (val_typ vals))))])
+		    (mk_annot true), env')
       end 
       else let (e,env') = (to_exp mode env vals) in (E_aux (E_app id [e]) (mk_annot true), env') 
     | _ -> 
@@ -1125,9 +1129,9 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	      | Typ_app (Id_aux (Id "vector") _) [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i) _)) _;_;_;_] ->
 		match v with 
 		  | V_vector start inc vs ->
-		    if start = i then (Value v,lm,le) else (Value (update_vector_start i v),lm,le)
+		    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 v),lm,le)
+		    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 
@@ -1459,7 +1463,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 				| (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,_) -> (Value V_unknown,lm,le)
+				| (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)
 			(fun a -> 
@@ -1485,7 +1494,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 		       let (ie1,env) = to_exp mode env i1v_whole in
 		       (E_aux (E_vector_subrange vec ie1 i2) (l,annot), env))))
 	 end) 
-        (fun a -> update_stack a (add_to_top_frame (fun i1 env -> (E_aux (E_vector_subrange vec i1 i2) (l,annot), env))))
+        (fun a -> 
+	  update_stack a (add_to_top_frame (fun i1 env -> (E_aux (E_vector_subrange vec i1 i2) (l,annot), env))))
     | E_vector_update vec i exp ->
       resolve_outcome 
 	(interp_main mode t_level l_env l_mem i)
@@ -1547,11 +1557,14 @@ 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_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_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)
@@ -1577,7 +1590,9 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                                       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)
-        (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))))
+        (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)
@@ -1664,8 +1679,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     | E_vector_indexed iexps (Def_val_aux default dannot) ->
       let (indexes,exps) = List.unzip iexps in
       let (is_inc,base,len) = (match typ with
-        | T_app "vector" (T_args [T_arg_nexp base;T_arg_nexp len; T_arg_order (Ord_aux Ord_inc _); _]) -> (true,base,len)
-        | T_app "vector" (T_args [T_arg_nexp base;T_arg_nexp len; T_arg_order (Ord_aux _ _); _]) -> (false,base,len) end) in
+        | T_app "vector" (T_args [T_arg_nexp base;T_arg_nexp len; T_arg_order (Ord_aux Ord_inc _); _]) -> 
+	  (true,base,len)
+        | T_app "vector" (T_args [T_arg_nexp base;T_arg_nexp len; T_arg_order (Ord_aux _ _); _]) -> 
+	  (false,base,len) end) in
       (match default with
 	| Def_val_empty ->
 	  exp_list mode t_level 
@@ -1686,11 +1703,15 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			    (Def_val_aux (Def_val_dec ev) dannot))
 		     (l,annot)))
 		(fun vs -> (V_vector_sparse b len is_inc (map2 (fun i v -> (i,v)) indexes vs) v)) l_env l_mem [] exps)
-	    (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_vector_indexed iexps (Def_val_aux (Def_val_dec e) dannot)) (l,annot), env)))) end)	  
+	    (fun a -> 
+	      update_stack a 
+		(add_to_top_frame (fun e env -> 
+		  (E_aux (E_vector_indexed iexps (Def_val_aux (Def_val_dec e) dannot)) (l,annot), env)))) end)	  
     | E_block exps -> interp_block mode t_level l_env l_env l_mem l annot exps
     | E_nondet exps ->
       (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)
+	      (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)) 
@@ -1719,7 +1740,8 @@ 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) -> 
@@ -1737,7 +1759,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 				   (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)
+          | Nothing -> 
+	    (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
 	| Tag_spec ->  
           (match find_function defs f with
 	  | Just(funcls) -> 
@@ -1753,9 +1776,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                 (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)))
+                       (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)
+          | Nothing -> 
+	    (Error l (String.stringAppend "Specified function must be defined before executing " name),lm,le) end)
         | Tag_ctor ->
           (match in_ctors ctors f with
           | Just(_) -> (Value (V_ctor f typ v), lm, le)
@@ -1775,14 +1799,16 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                     (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level le lm Top), lm, le)
 	  else if has_wmem_effect effects
 	  then 
-	    (Action (Write_mem (id_of_string name_ext) v Nothing v) (*TODO This is wrong, need to split up value or unsplit generally*)
-	            (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)
+	    (*TODO This is wrong, need to split up value or unsplit generally*)
+	    (Action (Write_mem (id_of_string name_ext) v Nothing v) 
+	       (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)
           else 
             (Action (Call_extern name_ext v) 
 	            (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)
-        | _ -> (Error l (String.stringAppend "Tag other than empty, spec, ctor, or extern on function call " name),lm,le) end)
+        | _ ->
+	  (Error l (String.stringAppend "Tag not empty, spec, ctor, or extern on function call " name),lm,le) end)
       | out -> out end)
     | E_app_infix lft op r -> 
        let op = match op with
@@ -1812,7 +1838,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                             (fun a -> update_stack a 
 			      (fun stack -> 
 				(Hole_frame (Id_aux (Id "0") l)
-				   (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot))) t_level l_env l_mem stack)))
+				   (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
+				   t_level l_env l_mem stack)))
 				                end)end)
 		| Tag_empty -> 
 		  (match find_function defs op with
@@ -1828,7 +1855,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			    (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)) t_level l_env l_mem stack)))
+					       (E_aux (E_id (Id_aux (Id "0") l)) (l,annot))
+					       t_level l_env l_mem stack)))
 		       end)end)
                 | Tag_spec ->
                   (match find_function defs op with
@@ -1844,7 +1872,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			    (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,(intern_annot annot))) t_level l_env l_mem stack)))
+					       (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
+					       t_level l_env l_mem stack)))
 		       end)end)
                 | Tag_extern ext_name ->
                   let ext_name = match ext_name with Just s -> s | Nothing -> name end in
@@ -1857,7 +1886,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
         (fun a -> update_stack a (add_to_top_frame (fun lft env -> (E_aux (E_app_infix lft op r) (l,annot), env))))
   | E_exit exp ->
     (Action (Exit exp) 
-            (Thunk_frame (E_aux (E_lit (L_aux L_unit Unknown)) (l, intern_annot annot)) t_level l_env l_mem Top),l_mem, l_env)
+            (Thunk_frame (E_aux (E_lit (L_aux L_unit Unknown)) (l, intern_annot annot)) 
+	       t_level l_env l_mem Top),l_mem, l_env)
   | E_let (lbind : letbind tannot) exp -> 
     match (interp_letbind mode t_level l_env l_mem lbind) with
     | ((Value v,lm,le),_) ->
@@ -1903,7 +1933,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			if mode.eager_eval
 			then interp_block mode t_level init_env le lm l tannot exps
 			else debug_out Nothing Nothing (E_aux (E_block exps) (l,tannot)) t_level lm le)
-                      (fun a -> update_stack a (add_to_top_frame (fun e env-> (E_aux (E_block(e::exps)) (l,tannot), env))))
+                      (fun a -> update_stack a 
+			(add_to_top_frame (fun e env-> (E_aux (E_block(e::exps)) (l,tannot), env))))
     end
 
 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))) =
@@ -1924,7 +1955,8 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	      if is_top_level then
 		let (LMem c m) = l_mem in
 		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)
+		((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)
@@ -1943,10 +1975,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	      | Just(V_register regform) -> regform
 	      | _ -> Assert_extra.failwith "Register not known in regenv" end in
           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 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)))
+            (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) 
+	  else (request,Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
 	| Tag_alias -> 
 	  let request = 
 	    (match in_env aliases id with
@@ -1957,30 +1992,33 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		      | Just indexes -> 
 			(match in_env indexes subreg with
 			  | Just ir -> 
-			    (Action (Write_reg (SubReg subreg (Reg reg annot') ir) 
-				               Nothing (update_vector_start (get_first_index_range ir) value)) 
-			            (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+			    (Action 
+			       (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing 
+				  (update_vector_start (get_first_index_range ir) (get_index_range_size ir) 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)
 			  | _ -> (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)
+		      | _ -> 
+			(Error l ("Internal error: alias spec has unknown register type " ^ id), l_mem, l_env) end)
 		  | AL_subreg (RI_aux (RI_id reg) (li, ((Just((T_abbrev (T_id id) _),_,_,_)) as annot'))) subreg ->
 		    (match in_env subregs (Id_aux (Id id) Unknown) with
 		      | Just indexes -> 
 			(match in_env indexes subreg with
 			  | Just ir -> 
-			    (Action (Write_reg (SubReg subreg (Reg reg annot') ir)
-				               Nothing (update_vector_start (get_first_index_range ir) value))
-			            (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l, intern_annot annot))
+			    (Action 
+			       (Write_reg (SubReg subreg (Reg reg annot') ir) Nothing 
+				  (update_vector_start (get_first_index_range ir) (get_index_range_size ir) 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)
 			  | _ -> (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)
+		      | _ -> (Error l ("Internal error: alias spec has unknown register type "^id), l_mem, l_env) end)
 		  | AL_bit (RI_aux (RI_id reg) (_,annot')) e ->
 		    resolve_outcome (interp_main mode t_level l_env l_mem e) 
 		      (fun v le lm -> match v with 
 			| V_lit (L_aux (L_num i) _) -> 
-			  (Action (Write_reg (Reg reg annot') (Just (i,i)) (update_vector_start i value)) 
+			  (Action (Write_reg (Reg reg annot') (Just (i,i)) (update_vector_start i 1 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) end)
+				     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 -> 
 		    resolve_outcome (interp_main mode t_level l_env l_mem start)
@@ -1991,7 +2029,8 @@ 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 stop) _) ->
-				     (Action (Write_reg (Reg reg annot') (Just (start,stop)) (update_vector_start start value)) 
+				     (Action (Write_reg (Reg reg annot') (Just (start,stop)) 
+						(update_vector_start start ((abs (start - stop)) +1) 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) end))
@@ -2011,9 +2050,11 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 						              (fst (to_exp <| mode with track_values =false|> eenv 
                                                                            (slice_vector value (r1+1) r2)))) annot2)
 				              t_level l_env l_mem Top), l_mem,l_env) end) end)
-	    | _ -> (Error l (String.stringAppend "Internal error: alias not found for id " (get_id id)),l_mem,l_env) end) in
+	    | _ -> (Error l ("Internal error: alias not found for id " ^(get_id id)),l_mem,l_env) end) in
 	  (request,Nothing)
-        | _ -> ((Error l (String.stringAppend "Internal error: writing to id with tag other than extern, empty, or alias " (get_id id)),l_mem,l_env),Nothing)
+        | _ -> 
+	  ((Error l ("Internal error: writing to id with tag other than extern, empty, or alias " ^ (get_id id)),
+	    l_mem,l_env),Nothing)
       end 
     | LEXP_memory id exps -> 
       match (exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (Unknown,Nothing)) 
@@ -2023,7 +2064,8 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
         (match tag with
         | Tag_extern ->
           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
+                           (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,
@@ -2031,7 +2073,8 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
                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) _) env -> (LEXP_aux (LEXP_memory id es) (l,annot), env)))
+      | (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
@@ -2046,9 +2089,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
               then begin
 		let (LMem c m) = l_mem in
 		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)
+		((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)
               end
-              else ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),Nothing)
+              else ((Error l ("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 env -> (LEXP_aux(LEXP_cast typc id) (l,annot), env)))
@@ -2059,11 +2103,15 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	      | Just(V_register regform) -> regform
 	      | _ -> Assert_extra.failwith "Register not known in regenv" end in
           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 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_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)
+            (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)
+	  else (request,Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
+        | _ -> 
+	  ((Error l ("Internal error: writing to id not 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
@@ -2099,15 +2147,20 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		(match (nth(),is_top_level,maybe_builder) with
 		  | (V_register regform,true,_) ->
 		    let start_pos = reg_start_pos regform in
-		    ((Action (Write_reg regform Nothing (update_vector_start start_pos 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),
+		    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
-		    ((Action (Write_reg regform Nothing (update_vector_start start_pos 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),
+		    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_boxref n t,true,_) -> 
+		    ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
 		  | (V_unknown,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), lm, l_env),Nothing)
 		  | (v,true,_) -> ((Error l "Vector does not contain reg or register values",lm,l_env),Nothing)
 		  | ((V_boxref n t),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
@@ -2116,17 +2169,24 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
               (match (nth(),is_top_level,maybe_builder) with
 		| (V_register regform,true,_) ->
 		    let start_pos = reg_start_pos regform in 
-		    ((Action (Write_reg regform Nothing (update_vector_start start_pos 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)
+		    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
-		    ((Action (Write_reg regform Nothing (update_vector_start start_pos 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),
+		    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_boxref n t,true,_) -> 
+		  ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing)
 		| (v,true,_) -> 
-		  ((Error l ("Vector does not contain reg or register values " ^ (string_of_value v)),lm,l_env),Nothing)
-		| ((V_boxref n t),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder))
+		  ((Error l ("Vector does not contain reg or register values " ^ (string_of_value v)),lm,l_env),
+		   Nothing)
+		| ((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 -> 
 	      ((Error l ("Vector access to write of non-vector" ^ (string_of_value v)),lm,l_env),Nothing)
@@ -2134,9 +2194,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
          | ((Action a s,lm,le),Just lexp_builder) ->
            (match (a,is_top_level) with
            | ((Write_reg regf Nothing value),true) -> 
-	     ((Action (Write_reg regf (Just (n,n)) (update_vector_start n value)) s, lm,le), Nothing)
+	     ((Action (Write_reg regf (Just (n,n)) (update_vector_start n 1 value)) s, lm,le), Nothing)
            | ((Write_reg regf Nothing value),false) -> 
-	     ((Action (Write_reg regf (Just (n,n)) (update_vector_start n value)) s,lm,le), Just  (next_builder lexp_builder))
+	     ((Action (Write_reg regf (Just (n,n)) (update_vector_start n 1 value)) s,lm,le),
+	      Just  (next_builder lexp_builder))
            | ((Write_mem id a Nothing value),true) -> ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Nothing)
            | ((Write_mem id a Nothing value),false) -> 
 	     ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder))
@@ -2178,7 +2239,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
                 | _ -> ((Error l "Vector required",lm,le),Nothing) end)
               | ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder) ->
                 ((Action 
-		    (Write_reg regf (Just (n1,n2)) (update_vector_start n1 value)) s,lm,le),
+		    (Write_reg regf (Just (n1,n2)) (update_vector_start n1 ((abs (n1-n2)) +1) value)) s,lm,le),
 		 Just (next_builder lexp_builder))
               | ((Action (Write_mem id a Nothing value) s,lm,le), Just lexp_builder) ->
                 ((Action (Write_mem id a (Just (n1,n2)) value) s,lm,le), Just (next_builder lexp_builder))
@@ -2219,7 +2280,9 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	   | Just(indexes) ->
 	     match in_env indexes id with
 	       | Just ir -> 
-		 ((Action (Write_reg (SubReg id regf ir) Nothing (update_vector_start (get_first_index_range ir) value)) s,lm,le), 
+		 ((Action (Write_reg (SubReg id regf ir) Nothing 
+			     (update_vector_start (get_first_index_range ir) (get_index_range_size ir) value)) s,
+		   lm,le), 
 		  (if is_top_level then Nothing else next_builder))
 	       | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
 		 end 
@@ -2229,7 +2292,9 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 	   | Just(indexes) ->
 	     match in_env indexes id with
 	       | Just ir -> 
-		 ((Action (Write_reg (SubReg id regf ir) Nothing (update_vector_start (get_first_index_range ir) value)) s,lm,le), 
+		 ((Action (Write_reg (SubReg id regf ir) Nothing 
+			     (update_vector_start (get_first_index_range ir) (get_index_range_size ir) value)) s,
+		   lm,le), 
 		  (if is_top_level then Nothing else next_builder))
 	       | _ -> ((Error l "Internal error, unrecognized write, no field",lm,le),Nothing)
 		 end 
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 22250e46..bdd5fcca 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -15,6 +15,15 @@ let zeroi = integerFromNat 0
 let onei = integerFromNat 1
 let twoi = integerFromNat 2
 
+let is_unknown v = match v with
+  | V_unknown -> true
+  | _ -> false
+end 
+
+let has_unknown v = match v with
+  | V_vector _ _ vs -> List.any is_unknown vs
+end
+
 let rec sparse_walker update ni processed_length length ls df =
   if processed_length = length 
   then []
@@ -60,9 +69,6 @@ let bit_to_bool b = match b with
   | 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
-(* PS HACK TO MAKE BUILD *)
-  | _ -> false  (* ARGH - SHOULDN'T HAVE TO CHOOSE *)
-(* END HACK *)
   end ;;
 let bool_to_bit b = match b with
     false -> V_lit (L_aux L_zero Unknown)
@@ -124,11 +130,14 @@ type signed = Unsigned | Signed
 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
+      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)
+      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 ;;
@@ -140,7 +149,8 @@ let rec to_vec_inc (V_tuple[v1;v2]) = match (v1,v2) with
   | (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_unknown,_) -> V_unknown
+  | ((V_lit(L_aux (L_num n) ln)),V_unknown) -> 
+    V_vector 0 true (List.replicate (natFromInteger n) V_unknown)
   | (_,V_unknown) -> V_unknown
   | _ -> Assert_extra.failwith ("to_vec_inc parameters were " ^ (string_of_value (V_tuple[v1;v2])))
 end
@@ -152,7 +162,8 @@ let rec to_vec_dec (V_tuple([v1;v2])) = match (v1,v2) with
   | (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_unknown,_) -> V_unknown
+  | ((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
 end
 ;;
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index 7aa211e7..1bfa698b 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -95,5 +95,11 @@ let rec get_first_index_range (BF_aux i _) = match i with
   | BF_single i -> i
   | BF_range i j -> i
   | BF_concat s _ -> get_first_index_range s
+end 
+
+let rec get_index_range_size (BF_aux i _) = match i with
+  | BF_single _ -> 1
+  | BF_range i j -> (abs (i-j)) + 1
+  | BF_concat i j -> (get_index_range_size i) + (get_index_range_size j)
 end
 
diff --git a/src/lem_interp/printing_functions.ml b/src/lem_interp/printing_functions.ml
index 22aea37e..dd94be6e 100644
--- a/src/lem_interp/printing_functions.ml
+++ b/src/lem_interp/printing_functions.ml
@@ -58,6 +58,10 @@ let bit_lifted_to_string = function
   | Bitl_undef -> "u"
   | Bitl_unknown -> "?"
 
+let bit_to_string = function
+  | Bitc_zero -> "0"
+  | Bitc_one -> "1"
+
 let reg_value_to_string v = 
   let l = List.length v.rv_bits in
   let start = string_of_int v.rv_start in
@@ -67,6 +71,8 @@ let reg_value_to_string v =
   else (string_of_int l) ^ "_" ^ start ^ "'b" ^ 
     collapse_leading (List.fold_right (^) (List.map bit_lifted_to_string v.rv_bits) "")
 
+let ifield_to_string v =
+  "0b"^ collapse_leading (List.fold_right (^) (List.map bit_to_string v) "")
 
 let register_value_to_string rv = 
   reg_value_to_string rv  
@@ -292,10 +298,10 @@ let instr_parm_to_string (name, typ, value) =
   name ^"="^
   match typ with
     | Other -> "Unrepresentable external value"
-    | _ -> let intern_v = (Interp_inter_imp.intern_reg_value value) in
+    | _ -> let intern_v = (Interp_inter_imp.intern_ifield_value value) in
 	      match Interp_lib.to_num Interp_lib.Unsigned intern_v with
 		| V_lit (L_aux(L_num n, _)) -> string_of_big_int n
-		| _ -> reg_value_to_string value
+		| _ -> ifield_to_string value
 
 let rec instr_parms_to_string ps = 
   match ps with