Add effect annotation for return, and actually keep a return after type check.

5 files changed, 14 insertions, 6 deletions

diff --git a/language/l2.lem b/language/l2.lem
index 94c93fe5..88953684 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -87,6 +87,7 @@ type base_effect_aux =  (* effect *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
  | BE_escape (* Tracking of expressions and functions that might call exit *)
  | BE_lset (* Local mutation happend; not user-writable *)
+ | BE_lret (* Local return happened; not user-writable *)
 
 
 type base_effect = 
diff --git a/language/l2.ml b/language/l2.ml
index 39f430db..1a35432b 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -85,6 +85,7 @@ base_effect_aux =  (* effect *)
  | BE_nondet (* nondeterminism from intra-instruction parallelism *)
  | BE_escape (* Tracking of expressions and functions that might call exit *)
  | BE_lset (* Local mutation happend; not user-writable *)
+ | BE_lret (* Local return happened; not user-writable *)
 
 
 type 
diff --git a/language/l2.ott b/language/l2.ott
index 96a30265..96483b90 100644
--- a/language/l2.ott
+++ b/language/l2.ott
@@ -197,7 +197,7 @@ base_effect :: 'BE_' ::=
   | nondet                              :: :: nondet {{ com nondeterminism from intra-instruction parallelism }}
   | escape                              :: :: escape {{ com Tracking of expressions and functions that might call exit }}
   | lset                                :: :: lset {{ com Local mutation happend; not user-writable }}
-
+  | lret                                :: :: lret {{ com Local return happened; not user-writable }}
 
 effect :: 'Effect_' ::=
   {{ com effect set, of kind Effects }}
diff --git a/src/type_check.ml b/src/type_check.ml
index 4c7fb8e0..3e6580dc 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1364,7 +1364,9 @@ let rec check_exp envs (imp_param:nexp option) (widen_num:bool) (widen_vec:bool)
       let efs = add_effect (BE_aux(BE_escape, l)) pure_e in
       (E_aux (E_exit e',(l,(simple_annot_efr expect_t efs))),expect_t,t_env,[],nob,efs)
     | E_return e ->
-      check_exp envs imp_param true true ret_t ret_t e
+      let (e', t'',_,cs,_,efr) = check_exp envs imp_param true true ret_t ret_t e in
+      let ers = add_effect (BE_aux (BE_lret,l)) pure_e in
+      (E_aux (E_return e', (l, (simple_annot_efr ret_t ers))), ret_t, t_env,cs,nob,union_effects efr ers)
     | E_sizeof nexp ->
       let n = anexp_to_nexp envs nexp in
       let n_subst = subst_n_with_env tp_env n in
diff --git a/src/type_internal.ml b/src/type_internal.ml
index c4bdc902..8047b61a 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -345,6 +345,7 @@ and ef_to_string (Ast.BE_aux(b,l)) =
       | Ast.BE_unspec-> "unspec"
       | Ast.BE_nondet-> "nondet"
       | Ast.BE_lset  -> "lset"
+      | Ast.BE_lret  -> "lret"
       | Ast.BE_escape -> "escape" 
 and efs_to_string es = 
   match es with
@@ -463,10 +464,10 @@ let union_effects e1 e2 =
     (*let _ = Printf.eprintf "union effects of length %s and %s\n" (e_to_string e1) (e_to_string e2) in*)
     {effect= Eset (effect_remove_dups (b1@b2))}  
 
-let remove_lsets ef = match ef.effect with
+let remove_local_effects ef = match ef.effect with
   | Evar _ | Euvar _ | Eset [] -> ef
   | Eset effects ->
-    {effect = Eset (List.filter (fun (BE_aux(be,l)) -> (match be with | BE_lset -> false | _ -> true))
+    {effect = Eset (List.filter (fun (BE_aux(be,l)) -> (match be with | BE_lset | BE_lret -> false | _ -> true))
                                 (effect_remove_dups effects)) }
 
 let rec lookup_record_typ (typ : string) (env : rec_env list) : rec_env option =
@@ -2935,6 +2936,9 @@ let compare_effect (BE_aux(e1,_)) (BE_aux(e2,_)) =
   | (BE_lset,BE_lset) -> 0
   | (BE_lset,_) -> -1
   | (_,BE_lset) -> 1
+  | (BE_lret,BE_lret) -> 0
+  | (BE_lret,_) -> -1
+  | (_, BE_lret) -> 1
   | (BE_escape,BE_escape) -> 0
 
 let effect_sort = List.sort compare_effect
@@ -2957,7 +2961,7 @@ let order_eq co o1 o2 =
 
 let rec remove_internal_effects = function
   | [] -> []
-  | (BE_aux(BE_lset,_))::effects -> remove_internal_effects effects
+  | (BE_aux((BE_lset | BE_lret),_))::effects -> remove_internal_effects effects
   | b::effects -> b::(remove_internal_effects effects)
 
 let has_effect searched_for eff =
@@ -4209,7 +4213,7 @@ let resolve_constraints cs =
 let check_tannot l annot imp_param constraints efs = 
   match annot with
   | Base((params,t),tag,cs,ef,_,bindings) ->
-    let efs = remove_lsets efs in
+    let efs = remove_local_effects efs in
     ignore(effects_eq (Specc l) efs ef);
     let s_env = (t_remove_unifications Envmap.empty t) in
     let params = Envmap.to_list s_env in