From 2105d7ad181a16dfabadbd4d943e4892d8eaa22f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= Date: Thu, 8 Sep 2011 10:45:19 +0200 Subject: [PATCH] Fix for linear types and automata --- compiler/heptagon/analysis/linear_typing.ml | 26 ++++++++++++++++++--- test/bad/bad_param_ident.ept | 4 ++++ test/bad/linear_autom.ept | 19 +++++++++++++++ test/bad/linear_init.ept | 11 +++++++++ test/good/linear_automata.ept | 8 +++---- 5 files changed, 60 insertions(+), 8 deletions(-) create mode 100644 test/bad/bad_param_ident.ept create mode 100644 test/bad/linear_autom.ept create mode 100644 test/bad/linear_init.ept diff --git a/compiler/heptagon/analysis/linear_typing.ml b/compiler/heptagon/analysis/linear_typing.ml index 41dfc59..06e0f32 100644 --- a/compiler/heptagon/analysis/linear_typing.ml +++ b/compiler/heptagon/analysis/linear_typing.ml @@ -321,6 +321,7 @@ let build env vds = let build_ids env vds = List.fold_left (fun env vd -> IdentSet.add vd.v_ident env) env vds +(* Linear inputs are considered initialised *) let build_location env vds = let add_one env vd = match vd.v_linearity with @@ -329,6 +330,15 @@ let build_location env vds = in List.fold_left add_one env vds +(* Linear variables with last: last x is initialised and x is used *) +let build_last_location (used_vars, init_vars) vds = + let add_one (used_vars, init_vars) vd = + match vd.v_last, vd.v_linearity with + | Last _, Lat r -> IdentSet.add vd.v_ident used_vars, LocationSet.add r init_vars + | _ -> used_vars, init_vars + in + List.fold_left add_one (used_vars, init_vars) vds + (** [extract_lin_exp args_lin e_list] returns the linearities and expressions from e_list that are not yet set to Lat r.*) let rec extract_lin_exp args_lin e_list = @@ -392,7 +402,7 @@ let rec typing_exp env e = let l, env = match e.e_desc with | Econst _ -> lin_skeleton Ltop e.e_ty, env | Evar x -> lin_of_ident x env, env - | Elast _ -> Ltop, env + | Elast x -> lin_of_ident x env, env | Epre (_, e) -> let lin = (not_linear_for_exp e) in let env = safe_expect env lin e in @@ -680,7 +690,8 @@ and typing_eq env eq = match eq.eq_desc with | Eautomaton(state_handlers) -> let typing_state (u, i) h = - let _, u1, i1 = typing_state_handler env h in + let (top_env, top_u, _) = env in + let _, u1, i1 = typing_state_handler (top_env, top_u, i) h in IdentSet.union u u1, LocationSet.union i i1 in let env, u, i = env in @@ -688,7 +699,8 @@ and typing_eq env eq = env, u, i | Eswitch(e, switch_handlers) -> let typing_switch (u, i) h = - let _, u1, i1 = typing_switch_handler env h in + let (top_env, top_u, _) = env in + let _, u1, i1 = typing_switch_handler (top_env, top_u, i) h in IdentSet.union u u1, LocationSet.union i i1 in let env, u, i = safe_expect env Ltop e in @@ -702,6 +714,13 @@ and typing_eq env eq = let env, u, i = safe_expect env Ltop e in let _, u, i = typing_block (env, u, i) b in env, u, i + (*TODO: faire la meme chose si on a un tuple *) + (* for init<> y = v fby x, we expect a linear type for x *) + | Eeq(Evarpat y, { e_desc = Efby(e_1, e_2) }) -> + let lin = lin_of_ident y env in + let _, env = check_init env eq.eq_loc eq.eq_inits lin in + safe_expect env Ltop e_1; + safe_expect env lin e_2 | Eeq(pat, e) -> let lin_pat = typing_pat env pat in let lin_pat, env = check_init env eq.eq_loc eq.eq_inits lin_pat in @@ -721,6 +740,7 @@ and typing_escape env esc = and typing_block (env,u,i) block = let env = build env block.b_local in + let u, i = build_last_location (u, i) block.b_local in List.fold_left typing_eq (env, u, i) block.b_equs and typing_switch_handler (env, u, i) sh = diff --git a/test/bad/bad_param_ident.ept b/test/bad/bad_param_ident.ept new file mode 100644 index 0000000..9ec5f40 --- /dev/null +++ b/test/bad/bad_param_ident.ept @@ -0,0 +1,4 @@ +node f<>(n: int) returns (o:int) +let + o = n +tel \ No newline at end of file diff --git a/test/bad/linear_autom.ept b/test/bad/linear_autom.ept new file mode 100644 index 0000000..ea70ab1 --- /dev/null +++ b/test/bad/linear_autom.ept @@ -0,0 +1,19 @@ +const n:int = 100 + +node autom_init() returns (u:int) +var o, a:int^n at r; +let + automaton + state S1 + do + init<> o = 3^n + until true then S2 + + state S2 + do + init<> o = 4^n + until false then S1 + end; + a = [ o with [0] = 0]; + u = a[0] +tel \ No newline at end of file diff --git a/test/bad/linear_init.ept b/test/bad/linear_init.ept new file mode 100644 index 0000000..4e79fdd --- /dev/null +++ b/test/bad/linear_init.ept @@ -0,0 +1,11 @@ +const n:int = 100 + +node bad_mem() + returns (v : float) +var t2,t,t_next:float^n at r; +let + t_next = [t with [0] = 0.0]; + t2 = [ t_next with [1] = 1.0 ]; + init<> t = (0.0^n) fby t_next; + v = t2[0]; +tel \ No newline at end of file diff --git a/test/good/linear_automata.ept b/test/good/linear_automata.ept index b9f2960..57dd8de 100644 --- a/test/good/linear_automata.ept +++ b/test/good/linear_automata.ept @@ -27,9 +27,8 @@ let tel node autom_last() returns (u:int) -var a:int^n at r; last o : int^n at r; +var last o : int^n at r = 0^n; let - init<> a = 1^n; automaton state S1 do @@ -37,9 +36,8 @@ let state S2 do - o = g(a) + o = g(last o) until false then S1 end; - u = a[0] + u = o[0] tel -