Begin doing better analysis on case splits over unknowns

5 files changed, 135 insertions, 76 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index a68e8ff9..d9b089e0 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -27,9 +27,10 @@ let ctor_annot typ = Just(typ,Tag_ctor,[],pure)
 
 let enum_annot typ max = Just(typ,Tag_enum max,[],pure)
 
-(* This is different from OCaml: it will drop elements from the longest list. *)
-let foldr2 f x l l' = List.foldr (Tuple.uncurry f) x (List.zip l l')
-let map2 f l l' = List.map (Tuple.uncurry f) (List.zip l l')
+let non_det_annot annot = match annot with
+  | Just(t,_,cs,ef) -> Just(t,Tag_unknown,cs,ef)
+  | _ -> Nothing
+end
 
 type i_direction = IInc | IDec
 let is_inc = function | IInc -> true | _ -> false end
@@ -104,37 +105,42 @@ let rec {ocaml} string_of_value v = match v with
 end
 let ~{ocaml} string_of_value _ = ""
 
-let rec {coq;ocaml} id_value_eq (i, v) (i', v') = i = i' && value_eq v v'
-and value_eq left right =
-  (* XXX it is not clear whether t = t' will work in all cases *)
+let rec {coq;ocaml} id_value_eq strict (i, v) (i', v') = i = i' && value_eq strict v v'
+and value_eq strict left right =
   match (left, right) with
   | (V_lit l, V_lit l') -> lit_eq l l'
   | (V_boxref n t, V_boxref m t') -> n = m && t = t'
-  | (V_tuple l, V_tuple l') -> listEqualBy value_eq l l'
-  | (V_list l, V_list l') -> listEqualBy value_eq l l'
-  | (V_vector n b l, V_vector m b' l') -> b = b' && listEqualBy value_eq l l'
+  | (V_tuple l, V_tuple l') -> listEqualBy (value_eq strict) l l'
+  | (V_list l, V_list l') -> listEqualBy (value_eq strict) l l'
+  | (V_vector n b l, V_vector m b' l') -> b = b' && listEqualBy (value_eq strict) l l'
   | (V_vector_sparse n o b l v, V_vector_sparse m p b' l' v') ->
-    n=m && o=p && b=b' && listEqualBy (fun (i,v) (i',v') -> i=i' && (value_eq v v')) l l' && value_eq v v'
+    n=m && o=p && b=b' && 
+    listEqualBy (fun (i,v) (i',v') -> i=i' && (value_eq strict v v')) l l' && value_eq strict v v'
   | (V_record t l, V_record t' l') ->
       t = t' &&
-      listEqualBy id_value_eq l l'
-  | (V_ctor i t ckind v, V_ctor i' t' ckind' v') -> t = t' && ckind=ckind' && id_value_eq (i, v) (i', v')
+      listEqualBy (id_value_eq strict) l l'
+  | (V_ctor i t ckind v, V_ctor i' t' ckind' v') -> t = t' && ckind=ckind' && id_value_eq strict (i, v) (i', v')
   | (V_ctor _ _ (C_Enum i) _,V_lit (L_aux (L_num j) _)) -> i = (natFromInteger j)
   | (V_lit (L_aux (L_num j) _), V_ctor _ _ (C_Enum i) _) -> i = (natFromInteger j)
-  | (V_unknown,_) -> true
-  | (_,V_unknown) -> true
-  | (V_track v _, v2) -> value_eq v v2
-  | (v,V_track v2 _)  -> value_eq v v2
+  | (V_unknown,V_unknown) -> true
+  | (V_unknown,_) -> if strict then false else true
+  | (_,V_unknown) -> if strict then false else true
+  | (V_track v1 ts1, V_track v2 ts2) -> 
+    if strict 
+    then value_eq strict v1 v2 && ts1 = ts2
+    else value_eq strict v1 v2
+  | (V_track v _, v2) -> if strict then false else value_eq strict v v2
+  | (v,V_track v2 _)  -> if strict then false else value_eq strict v v2
   | (_, _) -> false
   end
-let {isabelle;hol} id_value_eq = unsafe_structural_equality
-let {isabelle;hol} value_eq = unsafe_structural_equality
+let {isabelle;hol} id_value_eq _ x y = unsafe_structural_equality x y
+let {isabelle;hol} value_eq _ x y = unsafe_structural_equality x y
 
-let {coq;ocaml} value_ineq n1 n2 = not (value_eq n1 n2)
+let {coq;ocaml} value_ineq n1 n2 = not (value_eq false n1 n2)
 let {isabelle;hol} value_ineq = unsafe_structural_inequality
 
 instance (Eq value)
-  let (=)  = value_eq
+  let (=)  = value_eq false
   let (<>) = value_ineq
 end
 
@@ -221,8 +227,7 @@ type action =
  | Write_memv of id * value
  | Barrier of id * value
  | Footprint of id * value
- | Write_next_IA of value (* Perhaps not needed? *)
- | Nondet of list (exp tannot)
+ | Nondet of list (exp tannot) * tag
  | Call_extern of string * value
  | Exit of (exp tannot)
  (* For stepper, no action needed. String is function called, value is parameter where applicable *)
@@ -242,17 +247,17 @@ type outcome =
  | Action of action * stack
  | Error of l * string 
 
-type interp_mode = <| eager_eval : bool; track_values : bool; |>
+type interp_mode = <| eager_eval : bool; track_values : bool; track_lmem : bool|>
 
 (* Evaluates global let binds and prepares the context for individual expression evaluation in the current model *)
 val to_top_env : (i_direction -> outcome -> maybe value) -> defs tannot -> (maybe outcome * top_level)
 val get_default_direction : top_level -> i_direction
 
 (* interprets the exp sequentially in the presence of a set of top level definitions and returns a value, a memory request, or other external action *)
-val interp :interp_mode -> (i_direction -> outcome -> maybe value) -> defs tannot -> exp tannot -> outcome
+val interp :interp_mode -> (i_direction -> outcome -> maybe value) -> defs tannot -> exp tannot -> (outcome * lmem * lenv)
 
 (* Takes a paused partially evaluated expression, puts the value into the environment, and runs again *)
-val resume : interp_mode -> stack -> maybe value -> outcome
+val resume : interp_mode -> stack -> maybe value -> (outcome * lmem * lenv)
 
 (* Internal definitions to setup top_level *)
 val to_fdefs : defs tannot -> map string (list (funcl tannot))
@@ -463,6 +468,48 @@ let rec binary_taint thunk = fun vall valr ->
    | (vl,vr) -> thunk vl vr
 end 
 
+let rec merge_values v1 v2 = 
+  if value_eq true v1 v2 
+  then v1 
+  else match (v1,v2) with
+  | (V_lit l, V_lit l') -> if lit_eq l l' then v1 else V_unknown
+  | (V_boxref n t, V_boxref m t') -> 
+    if n = m then v1 else V_unknown (*Any change to locations in memory should be handled above this level*)
+  | (V_tuple l, V_tuple l') -> 
+    V_tuple (map2 merge_values l l') 
+  | (V_list l, V_list l') -> 
+    if (List.length l = List.length l') 
+    then V_list (map2 merge_values l l')
+    else V_unknown
+  | (V_vector n b l, V_vector m b' l') -> 
+    if b = b' && (List.length l = List.length l') 
+    then V_vector n b (map2 merge_values l l')
+    else V_unknown
+  | (V_vector_sparse n o b l v, V_vector_sparse m p b' l' v') ->
+    if (n=m && o=p && b=b' && listEqualBy (fun (i,_) (i',_) -> i=i') l l')
+    then V_vector_sparse n o b (map2 (fun (i,v1) (i',v2) -> (i, merge_values v1 v2)) l l') (merge_values v v')
+    else V_unknown
+  | (V_record t l, V_record t' l') ->
+    (*assumes canonical order for fields in a record*)
+    if t = t' && List.length l = length l' 
+    then V_record t (map2 (fun (i,v1) (_,v2) -> (i, merge_values v1 v2)) l l')
+    else V_unknown
+  | (V_ctor i t (C_Enum j) v, V_ctor i' t' (C_Enum j') v') -> 
+    if i = i' then v1 else V_unknown
+  | (V_ctor _ _ (C_Enum i) _,V_lit (L_aux (L_num j) _)) -> if i = (natFromInteger j) then v1 else V_unknown
+  | (V_lit (L_aux (L_num j) _), V_ctor _ _ (C_Enum i) _) -> if i = (natFromInteger j) then v2 else V_unknown
+  | (V_ctor i t ckind v, V_ctor i' t' _ v') ->
+    if t = t' && i = i' 
+    then (V_ctor i t ckind (merge_values v v'))
+    else V_unknown
+  | (V_unknown,V_unknown) -> V_unknown
+  | (V_track v1 ts1, V_track v2 ts2) -> 
+    taint (merge_values v1 v2) (ts1 union ts2)
+  | (V_track v1 ts, v2) -> taint (merge_values v1 v2) ts
+  | (v1,V_track v2 ts)  -> taint (merge_values v1 v2) ts
+  | (_, _) -> V_unknown
+end 
+
 let vector_length v = match (detaint v) with
   | V_vector n inc vals -> List.length vals
   | V_vector_sparse n m inc vals def -> m
@@ -1327,7 +1374,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	    | (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
-	    | (V_unknown,_) -> interp_main mode t_level l_env lm (E_aux (E_block [thn;els]) (l,annot))
+	    | (V_unknown,_) -> 
+	      interp_main mode t_level l_env lm (E_aux (E_nondet [thn;els]) (l,(non_det_annot annot)))
             | (_,true) -> interp_main mode t_level l_env lm els 
 	    | (_,false) -> debug_out Nothing Nothing els t_level lm l_env end)
         (fun a -> update_stack a (add_to_top_frame (fun c env -> (E_aux (E_if c thn els) (l,annot), env))))
@@ -1419,7 +1467,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 	      let (lets,taint_env) = 
 		List.foldr (fun (env,_,exp) (rst,taint_env) -> 
 		  let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
-	      interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot))
+	      interp_main mode t_level taint_env lm (E_aux (E_nondet lets) (l,(non_det_annot annot)))
 	 end)
         (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_case e pats) (l,annot), env))))
     | E_record(FES_aux (FES_Fexps fexps _) fes_annot) -> 
@@ -1795,7 +1843,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 		  (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) 
+      (Action (Nondet exps tag) 
 	      (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 ->
@@ -1826,7 +1874,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
 		  let (lets,taint_env) = 
 		    List.foldr (fun (env,_,exp) (rst,taint_env) -> 
 		      let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
-		  interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot))
+		  interp_main mode t_level taint_env lm (E_aux (E_nondet lets) (l,(non_det_annot annot)))
 	       end)
             | Nothing -> 
 	      (Error l (String.stringAppend "Internal error: function with tag global unfound " name),lm,le) end)
@@ -2558,7 +2606,7 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
 			        (l,(intern_annot annot))) t_level l_env l_mem Top), l_mem,l_env) end
 
 let rec eval_toplevel_let handle_action tlevel env mem lbind = 
-  match interp_letbind <|eager_eval=true; track_values=false;|> tlevel env mem lbind with
+  match interp_letbind <|eager_eval=true; track_values=false; track_lmem=false|> tlevel env mem lbind with
     | ((Value v, lm, (LEnv _ le)),_) -> Just le
     | ((Action a s,lm,le), Just le_builder) -> 
       (match handle_action (Action a s) with
@@ -2625,10 +2673,8 @@ let to_top_env external_functions defs =
 let interp mode external_functions defs exp =
   match (to_top_env external_functions defs) with
     | (Nothing,t_level) -> 
-      match interp_main mode t_level eenv emem exp with
-	| (o,_,_) -> o
-      end 
-    | (Just o,_) -> o (* Should do something different for action to allow global lets to call external functions *)
+      interp_main mode t_level eenv emem exp
+    | (Just o,_) -> (o,emem,eenv) 
   end
 
 let rec resume_with_env mode stack value =
@@ -2663,33 +2709,32 @@ let rec resume_with_env mode stack value =
 
 let rec resume mode stack value =
   match (stack,value) with
-  | (Top,_) -> Error Unknown "Top hit without expression to evaluate in resume"
+  | (Top,_) -> (Error Unknown "Top hit without expression to evaluate in resume",emem,eenv)
   | (Hole_frame id exp t_level env mem Top,Just value) -> 
-    match interp_main mode t_level (add_to_env (id,value) env) mem exp with | (o,_,_) -> o end 
+    interp_main mode t_level (add_to_env (id,value) env) mem exp
   | (Hole_frame id exp t_level env mem Top,Nothing) ->
-    Error Unknown "Top hole frame hit wihtout a value in resume"
+    (Error Unknown "Top hole frame hit wihtout a value in resume", mem, env)
   | (Hole_frame id exp t_level env mem stack,Just value) ->
     match resume mode stack (Just value) with
-    | Value v -> 
-      match interp_main mode t_level (add_to_env (id,v) env) mem exp with | (o,_,_) -> o end 
-    | Action action stack -> Action action (Hole_frame id exp t_level env mem stack)
-    | Error l s -> Error l s
+    | (Value v,_,_) -> 
+      interp_main mode t_level (add_to_env (id,v) env) mem exp  
+    | (Action action stack,lm,le) -> (Action action (Hole_frame id exp t_level env mem stack),lm,le)
+    | (Error l s,lm,le) -> (Error l s,lm,le)
     end  
   | (Hole_frame id exp t_level env mem stack, Nothing) ->
     match resume mode stack Nothing with
-      | Value v ->
-	match interp_main mode t_level (add_to_env (id,v) env) mem exp with | (o,_,_) -> o end
-      | Action action stack -> Action action (Hole_frame id exp t_level env mem stack)
-      | Error l s -> Error l s
+      | (Value v,_,_) ->
+	interp_main mode t_level (add_to_env (id,v) env) mem exp 
+      | (Action action stack,lm,le) -> (Action action (Hole_frame id exp t_level env mem stack),lm,le)
+      | (Error l s,lm,le) -> (Error l s,lm,le)
     end
   | (Thunk_frame exp t_level env mem Top,_) ->
-    match interp_main mode t_level env mem exp with | (o,_,_) -> o end
+    interp_main mode t_level env mem exp 
   | (Thunk_frame exp t_level env mem stack,value) ->
     match resume mode stack value with
-    | Value v -> 
-      match interp_main mode t_level env mem exp with | (o,_,_) -> o end 
-    | Action action stack -> Action action (Thunk_frame exp t_level env mem stack)
-    | Error l s -> Error l s
+    | (Value v,_,_) -> interp_main mode t_level env mem exp
+    | (Action action stack,lm,le) -> (Action action (Thunk_frame exp t_level env mem stack), lm, le)
+    | (Error l s,lm,le) -> (Error l s,lm,le)
     end  
   end
 
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index ba6e5107..ed576d2d 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -14,15 +14,15 @@ val extern_reg_value : reg_name -> Interp.value -> register_value
 val extern_mem_value : interp_mode -> Interp.value -> (memory_value * maybe (list reg_name))
 val extern_reg : Interp.reg_form -> maybe (nat * nat) -> reg_name
 
-let make_interp_mode eager_eval tracking_values = <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values|>;;
+let make_interp_mode eager_eval tracking_values = 
+  <| Interp.eager_eval = eager_eval; Interp.track_values = tracking_values; Interp.track_lmem = false|>;;
 
 let make_mode eager_eval tracking_values endian = 
   <|internal_mode = make_interp_mode eager_eval tracking_values;
     endian = endian|>;;
 let tracking_dependencies mode = mode.internal_mode.Interp.track_values
 let make_eager_mode mode = <| mode with internal_mode = <|mode.internal_mode with Interp.eager_eval = true |> |>;;
-let make_default_mode _ = <|internal_mode = <| Interp.eager_eval = false; Interp.track_values = false |>;
-                            endian = E_big_endian|>;;
+let make_default_mode _ = <|internal_mode = make_interp_mode false false; endian = E_big_endian|>;;
 
 let bitl_to_ibit = function 
   | Bitl_zero -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown)) 
@@ -292,41 +292,41 @@ let initial_instruction_state top_level main args =
 
 let rec interp_to_value_helper arg err_str instr direction thunk = 
   match thunk() with
-    | Interp.Value value -> (Just value,Nothing)
-    | Interp.Error l msg -> (Nothing, Just (Internal_error msg))
-    | Interp.Action (Interp.Call_extern i value) stack ->
+    | (Interp.Value value,_,_) -> (Just value,Nothing)
+    | (Interp.Error l msg,_,_) -> (Nothing, Just (Internal_error msg))
+    | (Interp.Action (Interp.Call_extern i value) stack,_,_) ->
       match List.lookup i (Interp_lib.library_functions direction) with
 	| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
 	| Just f  -> 
           interp_to_value_helper arg err_str instr direction 
 	    (fun _ -> Interp.resume (make_interp_mode true false) stack (Just (f value)))
       end 
-    | Interp.Action (Interp.Exit ((E_aux e _) as exp)) stack ->
+    | (Interp.Action (Interp.Exit ((E_aux e _) as exp)) stack,_,_) ->
       match e with
 	| E_id (Id_aux (Id "unsupported_instruction") _) -> (Nothing,Just (Unsupported_instruction_error instr))
 	| E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just (Not_an_instruction_error arg))
 	| E_lit (L_aux (L_string str) _) -> (Nothing, Just (Internal_error ("Exit called with message: " ^ str)))
 	| E_id (Id_aux (Id i) _) -> 
 	  (match (Interp.resume (make_interp_mode true false) (Interp.set_in_context stack exp) Nothing) with
-	    | Interp.Value (Interp.V_lit (L_aux (L_string str) _)) ->
+	    | (Interp.Value (Interp.V_lit (L_aux (L_string str) _)),_,_) ->
 	      (Nothing, Just (Internal_error ("Exit called when decoding "^err_str ^" with message: " ^ str)))
 	    | _ -> (Nothing, Just (Internal_error ("Exit called with unrecognized expression bound to an id " ^ i))) end)
 	| _ -> (Nothing, Just (Internal_error "Exit called with unrecognized expression"))
       end 
-    | Interp.Action (Interp.Read_reg r _) _ ->
+    | (Interp.Action (Interp.Read_reg r _) _,_,_) ->
       let rname = match r with 
 	| Interp.Reg (Id_aux (Id i) _) _ _ -> i
 	| Interp.SubReg (Id_aux (Id i) _) (Interp.Reg (Id_aux (Id i2) _) _ _) _ -> i2 ^ "." ^ i end in
       (Nothing, Just (Internal_error ("Register read of "^ rname^" request in a decode of " ^ err_str)))
-    | Interp.Action (Interp.Write_reg _ _ _) _ ->
+    | (Interp.Action (Interp.Write_reg _ _ _) _,_,_) ->
       (Nothing, Just (Internal_error "Register write request in a decode"))
-    | Interp.Action (Interp.Read_mem _ _ _) _ ->
+    | (Interp.Action (Interp.Read_mem _ _ _) _,_,_) ->
       (Nothing, Just (Internal_error "Read memory request in a decode"))
-    | Interp.Action (Interp.Write_mem _ _ _ _) _ ->
+    | (Interp.Action (Interp.Write_mem _ _ _ _) _,_,_) ->
       (Nothing, Just (Internal_error "Write memory request in a decode"))
-    | Interp.Action (Interp.Write_ea _ _) _ ->
+    | (Interp.Action (Interp.Write_ea _ _) _,_,_) ->
       (Nothing, Just (Internal_error "Write ea request in a decode"))
-    | Interp.Action (Interp.Write_memv _ _) _ ->
+    | (Interp.Action (Interp.Write_memv _ _) _,_,_) ->
       (Nothing, Just (Internal_error "Write memory value request in a decode"))
     | _ -> (Nothing, Just (Internal_error "Non expected action in a decode"))
 end
@@ -389,7 +389,7 @@ let decode_to_istate top_level value =
 		  (name, [(p_name,t, (extern_ifield_value name p_name value t))], effects)
 		| (Interp.V_tuple vals,parms) -> 
 		  (name, 
-		   (Interp.map2 (fun value (p_name,ie_typ) -> 
+		   (Interp_utilities.map2 (fun value (p_name,ie_typ) -> 
 		     let t = migrate_typ ie_typ in
 		     (p_name,t,(extern_ifield_value name p_name value t))) vals parms), effects)
           end end end in 
@@ -451,9 +451,9 @@ let rec interp_to_outcome mode context thunk =
   let (Context _ direction mem_reads mem_writes mem_write_eas mem_write_vals barriers spec_externs) = context in
   let internal_direction = if direction = D_increasing then Interp.IInc else Interp.IDec in
   match thunk () with
-  | Interp.Value _ -> Done
-  | Interp.Error l msg -> Error msg (*Todo, add the l information the string format*)
-  | Interp.Action a next_state ->
+  | (Interp.Value _,lm,le) -> Done
+  | (Interp.Error l msg,lm,le) -> Error msg 
+  | (Interp.Action a next_state,lm,le) ->
     match a with
     | Interp.Read_reg reg_form slice -> 
       Read_reg (extern_reg reg_form slice) 
@@ -526,9 +526,14 @@ let rec interp_to_outcome mode context thunk =
 	| _ -> Error ("Barrier " ^ i ^ " function not found") end
     | Interp.Footprint (Id_aux (Id i) _) lval ->
       Footprint (IState next_state context)
-    | Interp.Nondet exps -> 
-      let nondet_states = List.map (Interp.set_in_context next_state) exps in
-      Nondet_choice (List.map (fun i -> IState i context) nondet_states) (IState next_state context)
+    | Interp.Nondet exps tag ->
+      match tag with
+	| Tag_unknown ->
+	  let possible_states = List.map (Interp.set_in_context next_state) exps in
+	  Analysis_non_det (List.map (fun i -> IState i context) possible_states) (IState next_state context)
+	| _ -> 
+	  let nondet_states = List.map (Interp.set_in_context next_state) exps in
+	  Nondet_choice (List.map (fun i -> IState i context) nondet_states) (IState next_state context) end
     | Interp.Call_extern i value -> 
       match List.lookup i ((Interp_lib.library_functions internal_direction) ++ spec_externs) with
       | Nothing -> Error ("External function not available " ^ i)
@@ -598,9 +603,9 @@ let rec ie_loop mode register_values (IState interp_state context) =
   match interp mode (IState interp_state context) with
     | Done -> []
     | Error msg -> [E_error msg]
-    | Escape Nothing i_state -> E_escape :: (ie_loop mode register_values i_state)
+    | Escape Nothing i_state -> [E_escape]
     (*Do we want to record anything about the escape expression, which may be a function call*)
-    | Escape _ i_state -> E_escape :: (ie_loop mode register_values i_state) 
+    | Escape _ i_state -> [E_escape] 
     | Read_reg reg i_state_fun -> 
       let v =  match register_values with
 	| Nothing -> unknown_reg (reg_size reg)
@@ -624,6 +629,9 @@ let rec ie_loop mode register_values (IState interp_state context) =
     | Footprint i_state ->
       E_footprint::(ie_loop mode register_values i_state)
     | Internal _ _ next -> (ie_loop mode register_values next)
+    | Analysis_non_det possible_states i_state ->
+      (*TODO: need to merge the stores from the stacks/results somehow (so probably need to have a different loop)*)
+      (List.concat (List.map (ie_loop mode register_values) possible_states))++(ie_loop mode register_values i_state)
      end ;;
   
 let interp_exhaustive register_values i_state = 
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 3c79ed5e..305539f8 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -457,11 +457,14 @@ type outcome =
 | Write_reg of reg_name * register_value * instruction_state
 (* List of instruciton states to be run in parrallel, any order permitted *)
 | Nondet_choice of list instruction_state * instruction_state
-(* Stop for incremental stepping, function can be used to display function call data *)
-| Internal of maybe string * maybe (unit -> string) * instruction_state
 (* Escape the current instruction, for traps, some sys calls, interrupts, etc. Can optionally provide a handler 
    The non-optional instruction_state is what we would be doing if we're not escaping. This is for exhaustive interp*)
 | Escape of maybe instruction_state * instruction_state
+(* Stop for incremental stepping, function can be used to display function call data *)
+| Internal of maybe string * maybe (unit -> string) * instruction_state
+(* Analysis can lead to non_deterministic evaluation, represented with this outcome *)
+(*Note: this should not be externally visible *)
+| Analysis_non_det of list instruction_state * instruction_state
 | Done
 | Error of string
 
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index 875907fe..eb555c1c 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -271,7 +271,7 @@ let eq (V_tuple [x; y]) =
   retaint combo 
     (if has_unknown x || has_unknown y 
     then V_unknown
-    else (V_lit (L_aux (if value_eq (detaint x) (detaint y) then L_one else L_zero) Unknown)))
+    else (V_lit (L_aux (if ((detaint x) = (detaint 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]) ;;
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
index b808208b..6d7cb9cf 100644
--- a/src/lem_interp/interp_utilities.lem
+++ b/src/lem_interp/interp_utilities.lem
@@ -6,6 +6,9 @@ let rec power (a: integer) (b: integer) : integer =
  then 1
  else a * (power a (b-1))
 
+let foldr2 f x l l' = List.foldr (Tuple.uncurry f) x (List.zip l l')
+let map2 f l l' = List.map (Tuple.uncurry f) (List.zip l l')
+
 type tannot = maybe (t * tag * list nec * effect)
 
 let get_exp_l (E_aux e (l,annot)) = l