Assorted bug fixes that gets one mips instruction running (then fails for expected reasons) :)

4 files changed, 120 insertions, 8 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index f4c19362..1e30a0dc 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -2186,7 +2186,59 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
     | LEXP_id id -> 
       let name = get_id id in
       match tag with
-	| Tag_empty ->
+      | Tag_intro ->
+        match detaint (in_lenv l_env id) with
+	    | V_unknown ->
+	      if is_top_level then
+		if name = "0" then
+		  ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
+		else 
+		  let (LMem owner c m s) = l_mem in
+		  let l_mem = (LMem owner (c+1) m s) in
+		  ((Value (V_lit (L_aux L_unit l)), 
+		    update_mem mode.track_lmem l_mem c value,
+		    (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
+	      else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing)
+            | v -> 
+	      if is_top_level 
+	      then 
+		if name = "0" then
+		  ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
+		else
+		  ((Error l ("Writes must be to reg values given " ^ (string_of_value v)),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_set ->        
+	  match detaint (in_lenv l_env id) with
+	    | ((V_boxref n t) as v) -> 
+	      if is_top_level 
+	      then ((Value (V_lit (L_aux L_unit l)), 
+		     update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing)
+	      else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
+	    | V_unknown ->
+	      if is_top_level then
+		if name = "0" then
+		  ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
+		else 
+		  let (LMem owner c m s) = l_mem in
+		  let l_mem = (LMem owner (c+1) m s) in
+		  ((Value (V_lit (L_aux L_unit l)), 
+		    update_mem mode.track_lmem l_mem c value,
+		    (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
+	      else ((Error l ("Unknown local id " ^ (get_id id)),l_mem,l_env),Nothing)
+            | v -> 
+	      if is_top_level 
+	      then 
+		if name = "0" then
+		  ((Value (V_lit (L_aux L_unit l)), update_mem true l_mem 0 value, l_env), Nothing)
+		else
+		  ((Error l ("Writes must be to reg values given " ^ (string_of_value v)),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_empty ->        
 	  match detaint (in_lenv l_env id) with
 	    | ((V_boxref n t) as v) -> 
 	      if is_top_level 
@@ -2406,6 +2458,42 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
     | LEXP_cast typc id -> 
       let name = get_id id in
       match tag with
+      | Tag_intro ->
+	  match detaint (in_lenv l_env id) with
+	    | V_unknown -> 	  
+	      if is_top_level 
+              then begin
+		let (LMem owner c m s) = l_mem in
+		let l_mem = (LMem owner (c+1) m s) in
+		((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value, 
+		  (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
+              end
+              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)))
+          end
+       | Tag_set ->
+	  match detaint (in_lenv l_env id) with
+	    | ((V_boxref n t) as v) -> 
+	      if is_top_level 
+	      then ((Value (V_lit (L_aux L_unit l)), 
+		     update_mem mode.track_lmem l_mem n (recenter_val t value), l_env),Nothing)
+	      else ((Value v, 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
+		let (LMem owner c m s) = l_mem in
+		let l_mem = (LMem owner (c+1) m s) in
+		((Value (V_lit (L_aux L_unit l)), update_mem mode.track_lmem l_mem c value, 
+		  (add_to_env (id,(V_boxref c typ)) l_env)),Nothing)
+              end
+              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)))
+          end 
 	| Tag_empty ->
 	  match detaint (in_lenv l_env id) with
 	    | ((V_boxref n t) as v) -> 
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem
index c1267fc6..e49c38e2 100644
--- a/src/lem_interp/interp_lib.lem
+++ b/src/lem_interp/interp_lib.lem
@@ -235,7 +235,7 @@ let to_vec_inc (V_tuple[v1;v2]) =
 
 let to_vec_dec (V_tuple([v1;v2])) =
   let tv_fun v1 v2 =
-    match (v1,v2) with 
+    match (v1,v2) with
       | (V_lit(L_aux (L_num len) _), (V_lit(L_aux (L_num n) ln))) ->
 	let len = if len < 0 then 0 else natFromInteger len in
 	let l = boolListFrombitSeq len (bitSeqFromInteger Nothing n) in
@@ -705,8 +705,8 @@ let library_functions direction = [
   ("EXTZ", extz direction);
   ("to_vec_inc", to_vec_inc);
   ("to_vec_inc_undef", to_vec_inc_undef);
-  ("to_vec_dec", to_vec_dec_undef);
-  ("to_vec_dec_undef", to_vec_dec);
+  ("to_vec_dec", to_vec_dec);
+  ("to_vec_dec_undef", to_vec_dec_undef);
   ("bitwise_not", bitwise_not);
   ("bitwise_not_bit", bitwise_not_bit);
   ("bitwise_and", bitwise_binop (&&) "&");
diff --git a/src/lem_interp/run_interp_model.ml b/src/lem_interp/run_interp_model.ml
index d5ec53f7..8ec1b4df 100644
--- a/src/lem_interp/run_interp_model.ml
+++ b/src/lem_interp/run_interp_model.ml
@@ -222,7 +222,7 @@ let run
           mode in
       let (return,env') = perform_action env action in
       let (mode', env', next) =
-        match action with    
+        (match action with    
         | Read_reg0(reg,next_thunk) ->
           (match return with
            | Some(value) -> 
@@ -269,6 +269,9 @@ let run
         | Internal((Some fn),None,next) ->
           show "breakpoint" fn "" "";
           (step ~force:true next, env',next)
+        | Internal(None,Some vdisp,next) ->
+          show "breakpoint" (vdisp ()) "" "";
+          (step ~force:true next,env', next)
         | Internal((Some fn),(Some vdisp),next) ->
           show "breakpoint" (fn ^ " " ^ (vdisp ())) "" "";
           (step ~force:true next, env', next)
@@ -281,10 +284,29 @@ let run
               choose_order (false,mode,!track_dependencies,env'); in
           show "nondeterministic evaluation ended" "" "" "";
           (step next,env',next)
+        | Analysis_non_det (possible_istates, i_state) ->
+          let choose_order = List.sort (fun (_,i1) (_,i2) -> Pervasives.compare i1 i2) 
+              (List.combine possible_istates (List.map (fun _ -> Random.bits ()) possible_istates)) in
+          if possible_istates = []
+          then (step i_state,env',i_state)
+          else begin
+            show "undefined triggered a non_det" "" "" "";
+            let (_,_,_,env') = List.fold_right (fun (next,_) (_,_,_,env') -> 
+              loop mode env' (interp0 (make_mode (mode=Run) !track_dependencies !default_endian) next))
+              choose_order (false,mode,!track_dependencies,env'); in
+            (step i_state,env',i_state) end
         | Escape(Some e,_) ->
           show "exiting current evaluation" "" "" "";
           step e,env', e
-        | _ -> assert false        
+        | Escape _ -> assert false
+        | Error0 _ -> assert false
+        | Done ->
+          show "done evalution" "" "" "";
+          assert false
+        | Footprint0 _ -> assert false
+        | Write_ea0 _ -> assert false
+        | Write_memv0 _ -> assert false)
+        (*| _ -> assert false*)
       in
       loop mode' env' (Interp_inter_imp.interp0 (make_mode (mode' = Run) !track_dependencies !default_endian) next) in
   let mode = match mode with
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 27d6a1bb..9e47ba88 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -3003,7 +3003,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
         [TA_nexp b2;TA_nexp r2;] -> 
         let cs = [Eq(co,b2,n_zero);LtEq(co,Guarantee,mk_sub (mk_2n(r1)) n_one,r2)] in
         (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "unsigned",l)),[e]),
-                            (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e)))))
+                            (l,
+                             cons_tag_annot_efr t2 (External (Some "unsigned")) cs (get_cummulative_effects (get_eannot e)))))
       | [TA_nexp b1;TA_nexp r1;TA_ord {order = Ovar o};TA_typ {t=Tid "bit"}],_ -> 
         eq_error l "Cannot convert a vector to a range without an order"
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
@@ -3015,7 +3016,8 @@ let rec type_coerce_internal co d_env enforce is_explicit widen bounds t1 cs1 e
         [TA_nexp b2] -> 
         let cs = [GtEq(co,Guarantee,b2,n_zero);LtEq(co,Guarantee,b2,mk_sub (mk_2n(r1)) n_one)] in
         (t2,cs,pure_e,E_aux(E_app((Id_aux(Id "unsigned",l)),[e]),
-                            (l, constrained_annot_efr t2 cs (get_cummulative_effects (get_eannot e)))))
+                            (l,
+                             cons_tag_annot_efr t2 (External (Some "unsigned")) cs (get_cummulative_effects (get_eannot e)))))
       | [TA_nexp b1;TA_nexp r1;TA_ord o;TA_typ t],_ -> 
         eq_error l "Cannot convert non-bit vector into an range"
       | _,_ -> raise (Reporting_basic.err_unreachable l "vector or range is not properly kinded"))