Add a return exp form to Sail, supported in type checker and in interpreter.

TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem

2 files changed, 76 insertions, 23 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 92fa4ec0..a2b496e0 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -250,6 +250,7 @@ type action =
  | Footprint of id * value
  | Nondet of list (exp tannot) * tag
  | Call_extern of string * value
+ | Return of value
  | Exit of (exp tannot)
  (* For the error case of a failed assert, carries up an optional error message*)
  | Fail of value 
@@ -853,6 +854,15 @@ let rec clear_stack_state stack =
     | Thunk_frame e t_level env lmem s -> Thunk_frame e t_level env lmem (clear_stack_state s)
 end
 
+let remove_top_stack_frame stack =
+  match stack with
+  | Top -> Nothing
+  | Hole_frame _ _ _ _ _ Top -> Nothing
+  | Thunk_frame _ _ _ _ Top -> Nothing
+  | Hole_frame _ _ _ _ _ stack -> Just stack
+  | Thunk_frame _ _ _ _ stack -> Just stack
+end
+
 (*functions for converting in progress evaluation back into expression for building current continuation*)
 let rec combine_typs ts =
   match ts with
@@ -1300,12 +1310,16 @@ and vec_concat_match_plev t_level pat r_vals dir l last_pat t =
           | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp nc;_;_]) ->
             if last_pat
             then 
-              (true,false,(add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length r_vals)) dir r_vals)) eenv),r_vals,[])
+              (true,false,
+               (add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length r_vals)) dir r_vals)) eenv),
+               r_vals,[])
             else (false,false,eenv,[],[]) (*TODO use some constraint bounds here*)
           | _ -> 
             if last_pat
             then 
-              (true,false,(add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length r_vals)) dir r_vals)) eenv),r_vals,[])
+              (true,false,
+               (add_to_env (id,(V_vector (if is_inc(dir) then 0 else (List.length r_vals)) dir r_vals)) eenv),
+               r_vals,[])
             else (false,false,eenv,[],[]) end)
       | P_wild -> (match t with
           | T_app "vector" (T_args [T_arg_nexp _;T_arg_nexp (Ne_const i);_;_]) ->
@@ -1550,32 +1564,36 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                                     (to_exp mode env (taint (V_lit diff) (r1 union r2)))
                                   | _ -> Assert_extra.failwith "For loop from and by values not range" end in
                                 let  e = 
-                                  (E_aux (E_block 
-                                            [(E_aux 
-                                                (E_let 
-                                                   (LB_aux (LB_val_implicit (P_aux (P_id id) (fl,val_annot ftyp)) from_e)
-                                                      (Unknown,val_annot ftyp))
-                                                   exp) (l,annot));
-                                             (E_aux (E_for id augment_e to_e by_e order exp) (l,annot))])
-                                            (l,annot)) in
+                                  (E_aux
+                                     (E_block 
+                                        [(E_aux 
+                                            (E_let 
+                                               (LB_aux (LB_val_implicit (P_aux (P_id id) (fl,val_annot ftyp)) from_e)
+                                                  (Unknown,val_annot ftyp))
+                                               exp) (l,annot));
+                                         (E_aux (E_for id augment_e to_e by_e order exp) (l,annot))])
+                                     (l,annot)) in
                                 if mode.eager_eval
                                 then interp_main mode t_level env lm e 
                                 else debug_out Nothing Nothing e t_level lm env
                             | V_unknown -> 
                               let e = 
-                                (E_aux (E_let 
-                                          (LB_aux 
-                                             (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
-                                             (fl, val_annot (val_typ from_val)))
-                                          exp) (l,annot)) in
+                                (E_aux
+                                   (E_let 
+                                      (LB_aux 
+                                         (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
+                                         (fl, val_annot (val_typ from_val)))
+                                      exp) (l,annot)) in
                               interp_main mode t_level env lm e
                             | _ -> (Error l "internal error: by must be a number",lm,le) end)
                         (fun a -> update_stack a 
                           (add_to_top_frame (fun b env -> (E_aux (E_for id from_e to_e b order exp) (l,annot), env))))
                     | V_unknown -> 
                       let e =
-                        (E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
-                                              (fl, val_annot (val_typ from_val))) exp) (l,annot)) in
+                        (E_aux
+                           (E_let (LB_aux
+                                     (LB_val_implicit (P_aux (P_id id) (fl, val_annot (val_typ from_val))) from_e)
+                                     (fl, val_annot (val_typ from_val))) exp) (l,annot)) in
                       interp_main mode t_level env lm e
                     | _ -> (Error l "internal error: to must be a number",lm,env) end)
                 (fun a -> update_stack a 
@@ -1583,11 +1601,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                     (E_aux (E_for id from_e t by order exp) (l,annot), env))))
             | V_unknown ->
               let e =
-                (E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_id id) (Unknown, val_annot (val_typ from_val))) from_e)
-                                      (Unknown, val_annot (val_typ from_val))) exp) (l,annot)) in
+                (E_aux
+                   (E_let (LB_aux (LB_val_implicit (P_aux (P_id id) (Unknown, val_annot (val_typ from_val))) from_e)
+                             (Unknown, val_annot (val_typ from_val))) exp) (l,annot)) in
               interp_main mode t_level env lm e
             | _ -> (Error l "internal error: from must be a number",lm,le) end)
-        (fun a -> update_stack a (add_to_top_frame (fun f env -> (E_aux (E_for id f to_ by order exp) (l,annot), env))))
+          (fun a -> update_stack a
+              (add_to_top_frame (fun f env -> (E_aux (E_for id f to_ by order exp) (l,annot), env))))
     | E_case exp pats ->
       resolve_outcome 
         (interp_main mode t_level l_env l_mem exp)
@@ -1974,7 +1994,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                             (Def_val_aux (Def_val_dec ev) dannot))
                      (l,annot), env''))
                 (fun vs -> 
-                  (V_vector_sparse b len dir (map2 (fun i v -> ((natFromInteger i),v)) indexes vs) v)) l_env l_mem [] exps)
+                   (V_vector_sparse b len dir
+                      (map2 (fun i v -> ((natFromInteger i),v)) indexes vs) v)) l_env l_mem [] exps)
             (fun a -> 
               update_stack a 
                 (add_to_top_frame (fun e env -> 
@@ -2015,7 +2036,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
                     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
                   let (branches,maybe_id) = fix_up_nondet typ lets (l,annot) in
-                  interp_main mode t_level taint_env lm (E_aux (E_nondet branches) (l,(non_det_annot annot maybe_id)))
+                  let exp = E_aux (E_nondet branches) (l,(non_det_annot annot maybe_id)) in
+                  interp_main mode t_level taint_env lm exp
                end)
             | Nothing -> 
               (Error l ("Internal error: function with tag global unfound " ^ name),lm,le) end)
@@ -2169,6 +2191,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
         (fun a -> update_stack a (add_to_top_frame (fun lft env -> (E_aux (E_app_infix lft op r) (l,annot), env))))
   | E_exit exp ->
     (Action (Exit exp) (mk_thunk l annot t_level l_env l_mem),l_mem, l_env)
+  | E_return exp ->
+    resolve_outcome
+      (interp_main mode t_level l_env l_mem exp)
+      (fun v lm le ->
+         (Action (Return v) (mk_thunk l annot t_level l_env l_mem), l_mem, l_env))
+      (fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_return e) (l,annot), env)))) 
   | E_assert cond msg ->
     resolve_outcome 
       (interp_main mode t_level l_env l_mem msg)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index a2988ee5..04af1f94 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -331,8 +331,28 @@ let rec interp_to_value_helper arg ivh_mode err_str instr direction registers ev
                | Ivh_decode -> (Ivh_error (Not_an_instruction_error arg), events_out)
                | Ivh_illegal -> (Ivh_error (Not_an_instruction_error arg), events_out)
                | Ivh_unsupported -> (Ivh_error (Unsupported_instruction_error instr), events_out)
-               | Ivh_translate -> Assert_extra.failwith "Reached unreachable pattern" end) end) end)
+               | Ivh_translate -> Assert_extra.failwith "Reached unreachable pattern" end)
+            | _ -> (Ivh_error (Internal_error ("Value not an option for " ^ errk_str)), events_out) end) end)
     | (Interp.Error l msg,_,_) -> (Ivh_error (Internal_error msg), events_out)
+    | (Interp.Action (Interp.Return value) stack,_,_) ->
+      (match Interp.remove_top_stack_frame stack with
+       | Nothing ->
+         if exn_seen
+         then (Ivh_value_after_exn value, events_out)
+         else (match ivh_mode with
+             | Ivh_translate -> (Ivh_value value, events_out)
+             | _ ->
+                          (match value with
+            | Interp.V_ctor (Id_aux (Id "Some") _) _ _ vinstr -> (Ivh_value vinstr,events_out)
+            | Interp.V_ctor (Id_aux (Id "None") _) _ _ _ ->
+              (match ivh_mode with
+               | Ivh_decode -> (Ivh_error (Not_an_instruction_error arg), events_out)
+               | Ivh_illegal -> (Ivh_error (Not_an_instruction_error arg), events_out)
+               | Ivh_unsupported -> (Ivh_error (Unsupported_instruction_error instr), events_out)
+               | Ivh_translate -> Assert_extra.failwith "Reached unreachable pattern" end)
+            | _ -> (Ivh_error (Internal_error ("Value not an option for " ^ errk_str)), events_out)end) end)
+       | Just stack -> interp_to_value_helper arg ivh_mode err_str instr direction registers events exn_seen
+                                              (fun _ -> Interp.resume mode stack (Just value)) end)
     | (Interp.Action (Interp.Call_extern i value) stack,_,_) ->
       match List.lookup i (Interp_lib.library_functions direction) with
         | Nothing -> (Ivh_error (Internal_error ("External function not available " ^ i)), events_out)
@@ -642,6 +662,11 @@ let rec interp_to_outcome mode context thunk =
                       (Just (fun _ -> (Interp.string_of_value value) ^ "=>" ^ (Interp.string_of_value new_v)))
                       (IState (Interp.add_answer_to_stack next_state new_v) context), lm)
             end)
+         | Interp.Return value ->
+           (match Interp.remove_top_stack_frame next_state with
+            | Nothing -> (Done, lm)
+            | Just stack ->
+              interp_to_outcome mode context (fun _ -> Interp.resume mode.internal_mode stack (Just value)) end)
          | Interp.Step l Nothing Nothing -> (Internal Nothing Nothing (IState next_state context), lm)
          | Interp.Step l (Just name) Nothing -> (Internal (Just name) Nothing (IState next_state context), lm)
          | Interp.Step l (Just name) (Just value) ->