From 159bab2a5578c38c09b6b2bd8bd3c32e5f44fbd6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?L=C3=A9onard=20G=C3=A9rard?= Date: Tue, 8 Mar 2011 13:41:28 +0100 Subject: [PATCH] async constants. --- compiler/global/global_compare.ml | 5 ++- compiler/global/global_mapfold.ml | 3 ++ compiler/global/global_printer.ml | 1 + compiler/global/modules.ml | 2 +- compiler/global/static.ml | 2 ++ compiler/global/types.ml | 1 + compiler/heptagon/analysis/typing.ml | 3 ++ compiler/heptagon/parsing/hept_parser.mly | 15 +++++---- compiler/heptagon/parsing/hept_parsetree.ml | 1 + .../parsing/hept_parsetree_mapfold.ml | 3 ++ compiler/heptagon/parsing/hept_scoping.ml | 1 + compiler/minils/main/mls2seq.ml | 12 +++++-- compiler/minils/transformations/tomato.ml | 4 +++ compiler/obc/_tags | 2 +- compiler/obc/java/java.ml | 4 +-- compiler/obc/java/obc2java.ml | 13 ++++++-- compiler/obc/obc.ml | 16 +++++++++ compiler/obc/obc_mapfold.ml | 3 ++ compiler/obc/obc_printer.ml | 2 ++ lib/java/jeptagon/Pervasives.java | 33 +++++++++++++++++-- test/async/lent.ept | 12 +++++++ test/async/rapide_lent.ept | 24 ++++++++++++++ test/async/rapide_lent_a.ept | 24 ++++++++++++++ test/async/tt.ept | 12 +++++++ test/async/ttt.ept | 18 ++++++++++ tools/debugger_script | 2 -- 26 files changed, 198 insertions(+), 20 deletions(-) create mode 100644 test/async/lent.ept create mode 100644 test/async/rapide_lent.ept create mode 100644 test/async/rapide_lent_a.ept create mode 100644 test/async/tt.ept create mode 100644 test/async/ttt.ept diff --git a/compiler/global/global_compare.ml b/compiler/global/global_compare.ml index d216388..3f3279f 100644 --- a/compiler/global/global_compare.ml +++ b/compiler/global/global_compare.ml @@ -83,7 +83,10 @@ let rec static_exp_compare se1 se2 = | Sfield _, (Svar _ | Sint _ | Sfloat _ | Sbool _ | Sconstructor _) -> -1 | Sfield _, _ -> 1 - | Stuple _, (Srecord _ | Sop _ | Sarray _ | Sarray_power _) -> 1 + | Sasync _, (Svar _ | Sint _ | Sfloat _ | Sbool _ | Sconstructor _ | Sfield _) -> -1 + | Sasync _, _ -> 1 + + | Stuple _, (Srecord _ | Sop _ | Sarray _ | Sarray_power _ ) -> 1 | Stuple _, _ -> -1 | Sarray_power _, (Srecord _ | Sop _ | Sarray _) -> -1 diff --git a/compiler/global/global_mapfold.ml b/compiler/global/global_mapfold.ml index c3e9cff..0feecef 100644 --- a/compiler/global/global_mapfold.ml +++ b/compiler/global/global_mapfold.ml @@ -49,6 +49,9 @@ and static_exp_desc funs acc sd = match sd with (f, se), acc in let f_se_l, acc = mapfold aux acc f_se_l in Srecord f_se_l, acc + | Sasync se -> + let se, acc = static_exp_it funs acc se in + Sasync se, acc and ty_it funs acc t = try funs.ty funs acc t with Fallback -> ty funs acc t diff --git a/compiler/global/global_printer.ml b/compiler/global/global_printer.ml index 674a9d0..0c6181a 100644 --- a/compiler/global/global_printer.ml +++ b/compiler/global/global_printer.ml @@ -62,6 +62,7 @@ let rec print_static_exp ff se = match se.se_desc with | Srecord f_se_list -> print_record (print_couple print_qualname print_static_exp """ = """) ff f_se_list + | Sasync se -> fprintf ff "@[<2>async %a@]" print_static_exp se and print_static_exp_tuple ff l = fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "("","")") l diff --git a/compiler/global/modules.ml b/compiler/global/modules.ml index 807f3e1..0e67698 100644 --- a/compiler/global/modules.ml +++ b/compiler/global/modules.ml @@ -165,7 +165,7 @@ let add_const f v = let replace_value f v = g_env.values <- QualEnv.add f v g_env.values -(** { 3 Find functions look in the global environnement, nothing more } *) +(** { 3 Find functions look in the global environement, nothing more } *) let find_value x = QualEnv.find x g_env.values let find_type x = QualEnv.find x g_env.types diff --git a/compiler/global/static.ml b/compiler/global/static.ml index 23ce68c..c4f6bb9 100644 --- a/compiler/global/static.ml +++ b/compiler/global/static.ml @@ -74,6 +74,8 @@ let eval_core eval apply_op env se = match se.se_desc with | Srecord f_se_list -> { se with se_desc = Srecord (List.map (fun (f,se) -> f, eval env se) f_se_list) } + | Sasync se' -> + { se with se_desc = Sasync (eval env se') } (** [simplify env e] returns e simplified with the variables values taken from [env] or from the global env with [find_const]. diff --git a/compiler/global/types.ml b/compiler/global/types.ml index d9105ab..cf8b819 100644 --- a/compiler/global/types.ml +++ b/compiler/global/types.ml @@ -27,6 +27,7 @@ and static_exp_desc = | Sarray of static_exp list (** [ e1, e2, e3 ] *) | Srecord of (field_name * static_exp) list (** { f1 = e1; f2 = e2; ... } *) | Sop of fun_name * static_exp list (** defined ops for now in pervasives *) + | Sasync of static_exp and ty = | Tprod of ty list (** Product type used for tuples *) diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 9edef47..4e45722 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -449,6 +449,9 @@ and typing_static_exp const_env se = List.map (typing_static_field const_env fields (Tid q)) f_se_list in Srecord f_se_list, Tid q + | Sasync se -> + let typed_se, ty = typing_static_exp const_env se in + Sasync typed_se, Tasync ((),ty) in { se with se_ty = ty; se_desc = desc }, ty diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index fbd6e8d..8ddcd4f 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -427,6 +427,7 @@ simple_exp: _simple_exp: | IDENT { Evar $1 } | const { Econst $1 } + | ASYNC c=const { Econst (mk_static_exp (Sasync c) (Loc($startpos,$endpos))) } | LBRACE field_exp_list RBRACE { Estruct $2 } | LBRACKET array_exp_list RBRACKET { mk_call Earray $2 } | LPAREN tuple_exp RPAREN { mk_call Etuple $2 } @@ -555,14 +556,14 @@ qualname: ; -const: c=_const { mk_static_exp c (Loc($startpos,$endpos)) } +const: + | c=_const { mk_static_exp c (Loc($startpos,$endpos)) } _const: - | INT { Sint $1 } - | FLOAT { Sfloat $1 } - | BOOL { Sbool $1 } - | constructor { Sconstructor $1 } - | q=qualified (ident) - { Svar q } + | INT { Sint $1 } + | FLOAT { Sfloat $1 } + | BOOL { Sbool $1 } + | constructor { Sconstructor $1 } + | q=qualified(ident) { Svar q } ; tuple_exp: diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 5a43790..f4240b6 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -49,6 +49,7 @@ and static_exp_desc = | Sarray of static_exp list (** [ e1, e2, e3 ] *) | Srecord of (field_name * static_exp) list (** { f1 = e1; f2 = e2; ... } *) | Sop of fun_name * static_exp list (** defined ops for now in pervasives *) + | Sasync of static_exp type iterator_type = | Imap diff --git a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml index 7a8c3d0..566688b 100644 --- a/compiler/heptagon/parsing/hept_parsetree_mapfold.ml +++ b/compiler/heptagon/parsing/hept_parsetree_mapfold.ml @@ -104,6 +104,9 @@ and static_exp_desc funs acc sd = match sd with (f, se), acc in let f_se_l, acc = mapfold aux acc f_se_l in Srecord f_se_l, acc + | Sasync se -> + let se, acc = static_exp_it funs acc se in + Sasync se, acc and exp_it funs acc e = funs.exp funs acc e diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index 695d3ad..3fe1171 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -201,6 +201,7 @@ and translate_static_exp_desc ed = let qualf (f, se) = (qualify_field f, t se) in Types.Srecord (List.map qualf se_f_list) | Sop (fn, se_list) -> Types.Sop (qualify_value fn, List.map t se_list) + | Sasync se -> Types.Sasync (t se) let expect_static_exp e = match e.e_desc with | Econst se -> translate_static_exp se diff --git a/compiler/minils/main/mls2seq.ml b/compiler/minils/main/mls2seq.ml index 8246590..962e1f6 100644 --- a/compiler/minils/main/mls2seq.ml +++ b/compiler/minils/main/mls2seq.ml @@ -18,6 +18,7 @@ open Misc with or without static parameters *) type target = | Obc of (Obc.program -> unit) + | Obc_scalar of (Obc.program -> unit) | Obc_no_params of (Obc.program -> unit) | Minils of (Minils.program -> unit) | Minils_no_params of (Minils.program -> unit) @@ -39,7 +40,7 @@ let write_obc_file p = comment "Generation of Obc code" let targets = [ (*"c", Obc_no_params Cmain.program;*) - "java", Obc Java_main.program; + "java", Obc_scalar Java_main.program; "obc", Obc write_obc_file; "obc_np", Obc_no_params write_obc_file; "epo", Minils write_object_file ] @@ -65,10 +66,17 @@ let generate_target p s = let p_list = Callgraph.program p in let o_list = List.map Mls2obc.program p_list in print_unfolded p_list; - comment "Translation to Obc"; + comment "Obc Callgraph"; if !verbose then List.iter (Obc_printer.print stdout) o_list; List.iter convert_fun o_list + | Obc_scalar convert_fun -> + let o = Mls2obc.program p in + comment "Obc Scalarize"; + let o_s = Scalarize.program o in + convert_fun o; + if !verbose then Obc_printer.print stdout o_s + (** Translation into dataflow and sequential languages, defaults to obc. *) let program p = diff --git a/compiler/minils/transformations/tomato.ml b/compiler/minils/transformations/tomato.ml index 9352d46..fbef80b 100644 --- a/compiler/minils/transformations/tomato.ml +++ b/compiler/minils/transformations/tomato.ml @@ -67,6 +67,10 @@ module PatEnv = type penv_t = (int * exp * ident list) P.t + + (* An environment used for automata minimization: holds both a pattern environment mapping patterns to equivalence + classes, and a [(pat * int list) Env.t] that maps variable [x] to a [(pat, pth)] tuple where [pat] is the pattern + holding [x] at path [pth] *) type t = penv_t * (pat * int list) Env.t let empty = (P.empty, Env.empty) diff --git a/compiler/obc/_tags b/compiler/obc/_tags index c1549be..387e977 100644 --- a/compiler/obc/_tags +++ b/compiler/obc/_tags @@ -1 +1 @@ - or :include \ No newline at end of file + or or :include diff --git a/compiler/obc/java/java.ml b/compiler/obc/java/java.ml index 734c7de..4a415b8 100644 --- a/compiler/obc/java/java.ml +++ b/compiler/obc/java/java.ml @@ -111,8 +111,8 @@ let default_value ty = match ty with | Tarray _ -> Enew_array (ty,[]) -let java_pervasives = Names.modul_of_string "jeptagon.Pervasives" -let java_pervasives_class = Names.qualname_of_string "jeptagon.Pervasives" +let java_pervasive_class c = Names.qualname_of_string ("jeptagon.Pervasives."^c) +let the_java_pervasives = Names.qualname_of_string "jeptagon.Pervasives" let java_callable = Names.qualname_of_string "java.util.concurrent.Callable" diff --git a/compiler/obc/java/obc2java.ml b/compiler/obc/java/obc2java.ml index aac12f4..99f5361 100644 --- a/compiler/obc/java/obc2java.ml +++ b/compiler/obc/java/obc2java.ml @@ -15,6 +15,9 @@ Obc.Oobj and Oarray are simply Pvar and Parray_elem Obc.Types_alias are dereferenced since no simple type alias is possible in Java *) +(** Requires scalar Obc : [p = e] when [e] is an array is understand as a copy of the reference, + not a copy of the array. *) + open Format open Misc open Names @@ -97,6 +100,9 @@ let rec static_exp param_env se = match se.Types.se_desc with | Types.Sarray se_l -> Enew_array (ty param_env se.Types.se_ty, List.map (static_exp param_env) se_l) | Types.Srecord _ -> eprintf "ojSrecord@."; assert false; (* TODO java *) | Types.Sop (f, se_l) -> Efun (qualname_to_class_name f, List.map (static_exp param_env) se_l) + | Types.Sasync se -> + let t_c = Tgeneric (java_pervasive_class "StaticFuture", [boxed_ty param_env se.Types.se_ty]) in + Enew (t_c, [static_exp param_env se]) and boxed_ty param_env t = match t with | Types.Tprod ty_l -> tuple_ty param_env ty_l @@ -110,7 +116,7 @@ and boxed_ty param_env t = match t with and tuple_ty param_env ty_l = let ln = ty_l |> List.length |> Pervasives.string_of_int in - Tgeneric ({ qual = java_pervasives; name = "Tuple"^ln }, List.map (boxed_ty param_env) ty_l) + Tgeneric (java_pervasive_class ("Tuple"^ln), List.map (boxed_ty param_env) ty_l) and ty param_env t :Java.ty = match t with | Types.Tprod ty_l -> tuple_ty param_env ty_l @@ -197,6 +203,9 @@ let rec act_list param_env act_l acts = | Obc.Afor (v, se, se', b) -> let afor = Afor (var_dec param_env v, static_exp param_env se, static_exp param_env se', block param_env b) in afor::acts + | Obc.Ablock b -> + let ablock = Ablock (block param_env b) in + ablock::acts in List.fold_right _act act_l acts @@ -304,7 +313,7 @@ let create_async_classe async base_classe = let act_result = let exp_call = let args = var_inst::exps_step in - let executor = Eval (Pfield (Pclass java_pervasives_class, "executor_cached")) in + let executor = Eval (Pfield (Pclass the_java_pervasives, "executor_cached")) in Emethod_call (executor, "submit", [Enew (Tclass callable_classe_name, args)] ) in Aassgn (Pthis id_result, exp_call) in diff --git a/compiler/obc/obc.ml b/compiler/obc/obc.ml index aa8ab0f..bd67ce5 100644 --- a/compiler/obc/obc.ml +++ b/compiler/obc/obc.ml @@ -8,6 +8,21 @@ (**************************************************************************) (* Object code internal representation *) +(** { 3 Semantics } + Any variable is a reference to a constant memory. + Thus [p = e] is not the change of the reference, + but a recursive copy of what is referenced (deep copy). + As an example, [x = 3] but also [x = \[3; 4; 5\]] + and [t1 = t2] with the content of the array [t2] copied into the array [t1]. + Obc is also "SSA" in the sens that a variable is assigned a value only once per call of [step] etc. + Thus arguments are passed as constant references to a constant memory. + + One exception to the SSA rule is through the [mutable] variables. + Theses variables can be assigned multiple times. + Thus a [mutable] argument is passed as a reference to a constant memory. +*) + + open Misc open Names open Idents @@ -69,6 +84,7 @@ type act = | Aasync_call of async_t * pattern list * obj_ref * method_name * exp list | Acase of exp * (constructor_name * block) list | Afor of var_dec * static_exp * static_exp * block + | Ablock of block and block = { b_locals : var_dec list; diff --git a/compiler/obc/obc_mapfold.ml b/compiler/obc/obc_mapfold.ml index 9d131a6..27707d9 100644 --- a/compiler/obc/obc_mapfold.ml +++ b/compiler/obc/obc_mapfold.ml @@ -115,6 +115,9 @@ and act funs acc a = match a with let idx2, acc = static_exp_it funs.global_funs acc idx2 in let b, acc = block_it funs acc b in Afor(x, idx1, idx2, b), acc + | Ablock b -> + let b, acc = block_it funs acc b in + Ablock b, acc and block_it funs acc b = funs.block funs acc b and block funs acc b = diff --git a/compiler/obc/obc_printer.ml b/compiler/obc/obc_printer.ml index 4dbe75f..9efc2fe 100644 --- a/compiler/obc/obc_printer.ml +++ b/compiler/obc/obc_printer.ml @@ -108,6 +108,8 @@ let rec print_act ff a = print_obj_call o print_method_name meth print_exps es + | Ablock b -> + fprintf ff "do@\n %a@\ndone" print_block b and print_var_dec_list ff var_dec_list = match var_dec_list with | [] -> () diff --git a/lib/java/jeptagon/Pervasives.java b/lib/java/jeptagon/Pervasives.java index 2c1b6bb..607c052 100644 --- a/lib/java/jeptagon/Pervasives.java +++ b/lib/java/jeptagon/Pervasives.java @@ -1,17 +1,46 @@ package jeptagon; +import java.util.concurrent.Executors; +import java.util.concurrent.ExecutorService; +import java.util.concurrent.Future; +import java.util.concurrent.TimeUnit; + public class Pervasives { - public static final java.util.concurrent.ExecutorService executor_cached = java.util.concurrent.Executors.newCachedThreadPool(); + public static final ExecutorService executor_cached = Executors.newCachedThreadPool(); + public static class StaticFuture implements Future { + V v; + + public StaticFuture(V v) { this.v = v; } + + public boolean cancel(boolean mayInterruptIfRunning) { return false; } + + public boolean isCancelled() { return false; } + + public boolean isDone() { return true; } + + public V get() { return v; } + + public V get(long timeout, TimeUnit unit) { return v; } + } - public static class Tuple1 { + public static class Tuple1 { public final T c0; public Tuple1(T v) { c0 = v; } } + public static class Tuple22 { + public final Object c0; + public final Object c1; + public Tuple22(Object v0, Object v1) { + c0 = v0; + c1 = v1; + } + } + public static class Tuple2 { public final T0 c0; public final T1 c1; diff --git a/test/async/lent.ept b/test/async/lent.ept new file mode 100644 index 0000000..3b87307 --- /dev/null +++ b/test/async/lent.ept @@ -0,0 +1,12 @@ + +node g () returns (y : int) +let + y = 3 +tel + +node f (x : int; c : bool) returns (z : int) +let + z = merge c (true -> (0 fby (g(z when true(c))))) (false -> 0) +tel + + diff --git a/test/async/rapide_lent.ept b/test/async/rapide_lent.ept new file mode 100644 index 0000000..ac0aa53 --- /dev/null +++ b/test/async/rapide_lent.ept @@ -0,0 +1,24 @@ + + +node lent(coeff:int) returns (y:int) +let + y = do_stuff(coeff); +tel + + +node rapide<>() returns (z:int) +var y,cpt : int; big_step : bool; +let + big_step = cpt = 0; + cpt = size fby (if big_step then size else cpt - 1); + y = merge big_step + (true -> 0 -> (pre (lent(size)))) + (false -> 0 fby y when false(big_step)); + z = do_stuff(1) - y; +tel + + +node main() returns(r: int) +let + r = rapide<<1000>>(); +tel diff --git a/test/async/rapide_lent_a.ept b/test/async/rapide_lent_a.ept new file mode 100644 index 0000000..1c53a99 --- /dev/null +++ b/test/async/rapide_lent_a.ept @@ -0,0 +1,24 @@ + + +node lent(coeff:int) returns (y:int) +let + y = do_stuff(coeff); +tel + + +node rapide<>() returns (z:int) +var y : int; cpt : int; big_step : bool; +let + big_step = cpt = 0; + cpt = size fby (if big_step then size else cpt - 1); + y = merge big_step + (true -> 0 -> !(pre (async lent(size)))) + (false -> 0 fby y when false(big_step)); + z = do_stuff(1) - y; +tel + + +node main() returns(r: int) +let + r = rapide<<1000>>(); +tel diff --git a/test/async/tt.ept b/test/async/tt.ept new file mode 100644 index 0000000..e77a98c --- /dev/null +++ b/test/async/tt.ept @@ -0,0 +1,12 @@ +node counter(res: bool; tick: bool) returns (o: int) +let + o = if res then 0 else if tick then 1 -> pre o + 1 else 0 -> pre o; +tel + +node counter2() returns (b: bool) +var t : async int; +let + t = async 0 fby async counter(false,true); + b = counter(false,true) -1 = !t; +tel + diff --git a/test/async/ttt.ept b/test/async/ttt.ept new file mode 100644 index 0000000..95c4ae6 --- /dev/null +++ b/test/async/ttt.ept @@ -0,0 +1,18 @@ +node counter(res: bool; tick: bool) returns (o: int) +let + o = if res then 0 else if tick then 1 -> pre o + 1 else 0 -> pre o; +tel + +node counter3() returns (t: async bool) +var last async t: int; cpt: int; +let + cpt = counter(false,true); + automaton + state I do + t = async counter(false,true))); + until true continue III + state III do + until cpt/3 = 0 continue I + end; + b = 0 fby cpt - 1 = 0 -> !t ; +tel \ No newline at end of file diff --git a/tools/debugger_script b/tools/debugger_script index d6911ff..1caea16 100644 --- a/tools/debugger_script +++ b/tools/debugger_script @@ -1,5 +1,3 @@ -load_printer "/sw/lib/ocaml/menhirLib/menhirLib.cmo" -load_printer "/sw/lib/ocaml/str.cma" load_printer "_build/global/names.d.cmo" load_printer "_build/global/location.d.cmo" load_printer "_build/utilities/misc.d.cmo"