Finishing up some of the support for Exit

2 files changed, 14 insertions, 10 deletions

diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index f297b5bb..54cd60e2 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -245,7 +245,7 @@ let rec perform_action ((reg, mem) as env) = function
      perform_action env (Write_mem (id, n, slice, V_vector(zero_big_int, true, [value])))
  (* extern functions *)
  | Call_extern (name, arg) -> eval_external name arg, env
- | Debug _ | Nondet _ -> unit_lit, env
+ | Debug _ | Nondet _ | Exit _ -> unit_lit, env
  | _ -> assert false
 ;;
 
@@ -338,32 +338,32 @@ let run
       let show act lhs arrow rhs = debugf "%s: %s: %s %s %s\n"
         (grey loc) (green act) lhs (blue arrow) rhs in
       let left = "<-" and right = "->" in
-      let mode',env' = begin match a with
+      let (mode',env',s) = begin match a with
       | Read_reg (reg, sub) ->
           show "read_reg" (reg_to_string reg ^ sub_to_string sub) right (val_to_string return);
-          step (),env'
+          step (),env',s
       | Write_reg (reg, sub, value) ->
           assert (return = unit_lit);
           show "write_reg" (reg_to_string reg ^ sub_to_string sub) left (val_to_string value);
-          step (),env'
+          step (),env',s
       | Read_mem (id, args, sub) ->
           show "read_mem" (id_to_string id ^ val_to_string args ^ sub_to_string sub) right (val_to_string return);
-          step (),env'
+          step (),env',s
       | Write_mem (id, args, sub, value) ->
           assert (return = unit_lit);
           show "write_mem" (id_to_string id ^ val_to_string args ^ sub_to_string sub) left (val_to_string value);
-          step (),env'
+          step (),env',s
       (* distinguish single argument for pretty-printing *)
       | Call_extern (f, (V_tuple _ as args)) ->
           show "call_lib" (f ^ val_to_string args) right (val_to_string return);
-          step (),env'
+          step (),env',s
       | Call_extern (f, arg) ->
           show "call_lib" (sprintf "%s(%s)" f (val_to_string arg)) right (val_to_string return);
-          step (),env'
+          step (),env',s
       | Debug _ ->
           assert (return = unit_lit);
           show "breakpoint" "" "" "";
-          step ~force:true (),env'
+          step ~force:true (),env',s
       | Nondet exps ->
 	let stacks = List.sort (fun (_,i1) (_,i2) -> compare i1 i2)
 	                       (List.combine (List.map (set_in_context s) exps)
@@ -371,7 +371,10 @@ let run
 	show "nondeterministic evaluation begun" "" "" "";
 	let (_,_,env') = List.fold_right (fun (stack,_) (_,_,env') -> loop mode env' (resume {eager_eval = (mode = Run)} stack None)) stacks (false,mode,env'); in
 	show "nondeterministic evaluation ended" "" "" "";
-	step (),env'
+	step (),env',s
+      | Exit e ->
+	show "exiting current evaluation" "" "" "";
+	step (),env', (set_in_context s e)
       | Barrier (_, _) | Write_next_IA _  ->
           failwith "unexpected action"
       end in
diff --git a/src/type_check.ml b/src/type_check.ml
index 902785df..e952a457 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1430,6 +1430,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,tannot))),
       Env(d_env,(if is_rec then t_env else Envmap.insert t_env (id,tannot)))
 
+(*TODO Only works for inc vectors, need to add support for dec*)
 let check_alias_spec envs alias (AL_aux(al,(l,annot))) e_typ =
   let (Env(d_env,t_env)) = envs in
   let check_reg (Id_aux(_,l) as id) : (string * typ * typ) =