From cc61f795555c6e80f2d82f9b6655a5a3115d50f2 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Sat, 23 Jul 2016 13:16:09 +0100 Subject: Add effect annotation for return, and actually keep a return after type check. --- language/l2.lem | 1 + language/l2.ml | 1 + language/l2.ott | 2 +- src/type_check.ml | 4 +++- src/type_internal.ml | 12 ++++++++---- 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 -- cgit v1.2.3