Make exhaust run from the first breakpoint in the interactive interpreter

(I still think this is a silly place to run exhaust from, but it no longer finds errors or crashes)

3 files changed, 15 insertions, 3 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 94c3e283..6edebc49 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1338,12 +1338,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
         (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 V_unknown,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_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)
@@ -1994,6 +1995,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
       | (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 V_unknown,lm,le),Nothing)
         | V_lit (L_aux (L_num n) ln) -> 
           let next_builder le_builder = 
             (fun e env -> 
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index bc9610de..afa58f6d 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -31,6 +31,7 @@ let intern_value v = match v with
     (to_bits (List.reverse
 		(List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys))))
   | Unknown -> Interp.V_unknown
+  | _ -> Interp.V_unknown
 end
 
 let extern_reg r slice = match (r,slice) with
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index c04ff73d..c0237cbc 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -146,8 +146,10 @@ let to_vec ord len n =
   else to_vec_dec (V_tuple ([V_lit(L_aux (L_num (integerFromNat len)) Interp_ast.Unknown); n]))
 ;;
 
-let exts len ((V_vector _ inc _) as v) =
-  to_vec inc len (to_num true v)
+let exts len v = match v with
+  | V_vector _ inc _  -> to_vec inc len (to_num true v)
+  | V_unknown -> V_unknown
+end
 ;;
 
 let eq (V_tuple [x; y]) = V_lit (L_aux (if value_eq x y then L_one else L_zero) Unknown) ;;
@@ -233,18 +235,24 @@ let rec arith_op_vec_range_range op (V_tuple args) = match args with
 end ;;
 
 let compare_op op (V_tuple args) = match args 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 ;;
 let compare_op_vec op (V_tuple args) = match args with
+  | [V_unknown;_] -> V_unknown
+  | [_;V_unknown] -> V_unknown
   | [((V_vector _ _ _) as l1);((V_vector _ _ _) as l2)] ->
     let (l1',l2') = (to_num true l1, to_num true l2) in
     compare_op op (V_tuple[l1';l2'])
 end ;;
 
 let rec duplicate (V_tuple args) = match args with
+  | [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
@@ -267,6 +275,7 @@ let function_map = [
   ("add_range_vec_range", arith_op_range_vec_range (+));
   ("minus", arith_op (-));
   ("minus_vec", arith_op_vec (-) 1);
+  ("minus_vec_range", arith_op_vec_range (-) 1);
   ("multiply", arith_op ( * ));
   ("multiply_vec", arith_op_vec ( * ) 2);
   ("mod", arith_op (mod));