hacks on taint tracking

3 files changed, 21 insertions, 4 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index a2f224af..96ce8893 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1288,7 +1288,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 			| 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)
+                    | 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 ->		  
                   match a with
                     | Action (Read_reg reg Nothing) stack -> 
@@ -1342,6 +1343,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 				| (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,_) -> (Value V_unknown,lm,le)
 				| _ -> (Error l "Vector slice of non-vector",lm,le) end)
 			 end)
@@ -1966,7 +1968,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
 		| (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))
 		| (v,false, Just lexp_builder) -> ((Value v,lm,le), Just (next_builder lexp_builder)) end)
-            | _ -> ((Error l "Vector access of non-vector",lm,l_env),Nothing) end)
+            | _ -> ((Error l "Vector access to write of non-vector",lm,l_env),Nothing) end)
          | ((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)) value) s, lm,le), Nothing)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 773de556..98b1e447 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -342,7 +342,7 @@ let rec ie_loop mode i_state =
      end ;;
   
 let interp_exhaustive i_state = 
-  let mode = make_mode true false in
+  let mode = make_mode true true in
   ie_loop mode i_state
 
 let rec rr_ie_loop mode i_state = 
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 804a50bd..b4a79e8c 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -58,6 +58,9 @@ 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)
@@ -72,6 +75,9 @@ let bitwise_not v =
   | V_track (V_vector idx inc v) r ->
     let apply x = bool_to_bit(not (bit_to_bool x)) in
     V_track (V_vector idx inc (List.map apply v)) r
+(* PS HACKING TO MAKE BUILD *)
+  | V_track V_unknown r -> v
+(* END HACK *)
 end ;;
 
 let bitwise_not_bit v = 
@@ -149,6 +155,9 @@ let to_vec ord len n =
 let exts (V_tuple[V_lit(L_aux (L_num len) _);v]) = match v with
   | V_vector _ inc _  -> to_vec inc (natFromInteger len) (to_num true v)
   | V_unknown -> V_unknown
+(* PS HACK TO MAKE BUILD *)
+  | V_track v r -> v
+(* END HACK*)
 end
 ;;
 
@@ -253,13 +262,19 @@ end ;;
 let rec duplicate (V_tuple args) = match args with
   | [V_unknown;_] -> V_unknown
   | [_;V_unknown] -> V_unknown
+  (* HERE PS HACKING TO MAKE BUILD*)
+  | [V_track v1 r1;V_track v2 r2] -> V_track v1 r1 (* PLACEHOLDER *)
+  | [V_track v1 r1; v2] -> V_track v1 r1 (* PLACEHOLDER *)
+  | [v1;V_track v2 r2] -> v1 (* PLACEHOLDER *)
+  (* END OF HACK *)
+
   | [(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'] ->
-      (* XXX d = d' ? droping n' ? *)
+      (* XXX d = d' ? dropping n' ? *)
       V_vector n d (l ++ l')
   | [V_lit l; x] -> vec_concat (V_tuple [litV_to_vec l true; x]) (*TODO, get the correct order*)
   | [x; V_lit l] -> vec_concat (V_tuple [x; litV_to_vec l true]) (*TODO, get the correct order*)