Real asynchronous resets.

This commit is contained in:
Léonard Gérard 2011-05-23 09:24:57 +02:00
parent 96272339e4
commit 2a2b363bf7
21 changed files with 138 additions and 99 deletions

View file

@ -51,9 +51,12 @@ let rec fresh_ct ty = match ty with
(** returns the canonic (short) representant of a [ck]
and update it to this value. *)
let rec ck_repr ck = match ck with
| Cbase | Con _ | Cvar { contents = Cindex _ } -> ck
| Cbase | Con _
| Cvar { contents = Cindex _ } -> ck
| Cvar (({ contents = Clink ck } as link)) ->
let ck = ck_repr ck in (link.contents <- Clink ck; ck)
let ck = ck_repr ck in
link.contents <- Clink ck;
ck
(** verifies that index is fresh in ck. *)
@ -65,32 +68,31 @@ let rec occur_check index ck =
| Con (ck, _, _) -> occur_check index ck
| _ -> raise Unify
(** unify ck *)
let rec unify_ck ck1 ck2 =
and unify_ck ck1 ck2 =
let ck1 = ck_repr ck1 in
let ck2 = ck_repr ck2 in
if ck1 == ck2
then ()
if ck1 == ck2 then ()
else
(match (ck1, ck2) with
| (Cbase, Cbase) -> ()
| (Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 }) when
n1 = n2 -> ()
| (Cvar (({ contents = Cindex n1 } as v)), _) ->
(occur_check n1 ck2; v.contents <- Clink ck2)
| (_, Cvar (({ contents = Cindex n2 } as v))) ->
(occur_check n2 ck1; v.contents <- Clink ck1)
| (Con (ck1, c1, n1), Con (ck2, c2, n2)) when (c1 = c2) & (n1 = n2) ->
unify_ck ck1 ck2
| _ -> raise Unify)
match (ck1, ck2) with
| Cbase, Cbase -> ()
| Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 } when n1 = n2 -> ()
| Con (ck1, c1, n1), Con (ck2, c2, n2) when (c1 = c2) & (n1 = n2) ->
unify_ck ck1 ck2
| Cvar ({ contents = Cindex n } as v), ck
| ck, Cvar ({ contents = Cindex n } as v) ->
occur_check n ck;
v.contents <- Clink ck
| _ -> raise Unify
(** unify ct *)
let rec unify t1 t2 =
if t1 == t2 then () else
match (t1, t2) with
| (Ck (Cbase | Cvar { contents = Cindex _; }), Cprod [])
| (Cprod [], Ck (Cbase | Cvar { contents = Cindex _; })) ->
()
| (Cprod [], Ck (Cbase | Cvar { contents = Cindex _; })) -> ()
| (Ck ck1, Ck ck2) -> unify_ck ck1 ck2
| (Cprod t1_list, Cprod t2_list) -> unify_list t1_list t2_list
| _ -> raise Unify
@ -99,6 +101,7 @@ and unify_list t1_list t2_list =
try List.iter2 unify t1_list t2_list
with _ -> raise Unify
let rec skeleton ck = function
| Tprod ty_list ->
(match ty_list with
@ -118,29 +121,14 @@ let prod ck_l = match ck_l with
| _ -> Cprod (List.map (fun ck -> Ck ck) ck_l)
let rec root_ck_of ck = match ck_repr ck with
| Cbase | Cvar _ -> ck
| Cbase
| Cvar { contents = Cindex _ } -> ck
| Con(ck,_,_) -> root_ck_of ck
| Cvar { contents = Clink _ } -> Misc.internal_error "Clocks, wrong repr"
let rec last_clock ct = match ct with
| Ck ck -> ck
| Cprod l -> last_clock (Misc.last_element l)
(*
let rec tuple ck = function
| Tprod ty_list ->
(match ty_list with
| [] -> Ck ck
| _ -> Cprod (List.map (tuple ck) ty_list))
| Tarray (t, _) -> tuple ck t
| Tid _ | Tinvalid -> Ck ck
*)
(*
let max ck_1 ck_2 = match ck_repr ck_1, ck_reprck_2 with
|
let rec optim_base_ck base_ck ct = match ct with
| Ck ck ->
| Cprod c_l ->
*)

View file

@ -93,8 +93,8 @@ let _load_module modul =
let modname = match modul with
| Names.Pervasives -> "Pervasives"
| Names.Module n -> n
| Names.LocalModule -> Misc.internal_error "modules" 0
| Names.QualModule _ -> Misc.unsupported "modules" 0
| Names.LocalModule -> Misc.internal_error "modules"
| Names.QualModule _ -> Misc.unsupported "modules"
in
let name = String.uncapitalize modname in
try

View file

@ -68,7 +68,7 @@ let rec modul_of_string_list = function
let qualname_of_string s =
let q_l_n = Misc.split_string s "." in
match List.rev q_l_n with
| [] -> Misc.internal_error "Names" 0
| [] -> Misc.internal_error "Names"
| n::q_l -> { qual = modul_of_string_list q_l; name = n }
let modul_of_string s =

View file

@ -116,7 +116,7 @@ let rec ck_to_sck ck =
match ck with
| Clocks.Cbase -> Cbase
| Clocks.Con (ck,c,x) -> Con(ck_to_sck ck, c, Idents.source_name x)
| _ -> Misc.internal_error "Signature couldn't translate ck" 1
| _ -> Misc.internal_error "Signature couldn't translate ck"
let names_of_arg_list l = List.map (fun ad -> ad.a_name) l

View file

@ -58,7 +58,7 @@ let message exn =
(** When not [partial],
@raise Partial_evaluation when the application of the operator can't be evaluated (only Unknown_op).
@raise Partial_evaluation when the application of the operator can't be evaluated.
Otherwise keep as it is unknown operators. *)
let apply_op partial loc op se_list =
match se_list with
@ -87,7 +87,8 @@ let apply_op partial loc op se_list =
(** When not [partial],
@raise Partial_evaluation when a static var cannot be evaluated, a local static parameter for example.
@raise Partial_evaluation when a static var cannot be evaluated,
a local static parameter for example.
Otherwise evaluate in a best effort manner. *)
let rec eval_core partial env se = match se.se_desc with
| Sint _ | Sfloat _ | Sbool _ | Sstring _ | Sconstructor _ | Sfield _ -> se
@ -143,7 +144,7 @@ let eval env se =
@raise [Errors.Error] if it cannot be computed.*)
let int_of_static_exp env se = match (eval env se).se_desc with
| Sint i -> i
| _ -> Misc.internal_error "static int_of_static_exp" 1
| _ -> Misc.internal_error "static int_of_static_exp"
(** [is_true env constr] returns whether the constraint is satisfied
in the environment (or None if this can be decided)

View file

@ -264,7 +264,7 @@ and translate_eq ((d_list, eq_list) as context) eq = match eq.eq_desc with
mk_equation ~loc:eq.eq_loc (Eblock { b with b_local = v @ b.b_local; b_equs = eqs})
in
d_list, eq :: eq_list
| _ -> Misc.internal_error "normalize" 0
| _ -> Misc.internal_error "normalize"
and translate_eq_list d_list eq_list =
List.fold_left

View file

@ -76,7 +76,7 @@ let rec translate_op = function
| Heptagon.Eselect_trunc -> Eselect_trunc
| Heptagon.Econcat -> Econcat
| Heptagon.Earray -> Earray
| Heptagon.Etuple -> Misc.internal_error "hept2mls Etuple" 1
| Heptagon.Etuple -> Misc.internal_error "hept2mls Etuple"
| Heptagon.Earrow -> assert false
let translate_app app =

View file

@ -57,7 +57,7 @@ let rec pattern_of_idx_list p l =
let rec aux p l = match p.pat_ty, l with
| _, [] -> p
| Tarray (ty',_), idx :: l -> aux (mk_pattern ty' (Larray (p, idx))) l
| _ -> internal_error "mls2obc" 1
| _ -> internal_error "mls2obc"
in
aux p l
@ -68,7 +68,7 @@ let rec pattern_of_trunc_idx_list p l =
let rec aux p l = match p.pat_ty, l with
| _, [] -> p
| Tarray (ty', se), idx :: l -> aux (mk_pattern ty' (Larray (p, mk_between idx se))) l
| _ -> internal_error "mls2obc" 1
| _ -> internal_error "mls2obc"
in
aux p l
@ -78,7 +78,7 @@ let array_elt_of_exp idx e =
mk_exp ty (Econst c)
| _, Tarray (ty,_) ->
mk_pattern_exp ty (Larray(pattern_of_exp e, idx))
| _ -> internal_error "mls2obc" 2
| _ -> internal_error "mls2obc"
(** Creates the expression that checks that the indices
in idx_list are in the bounds. If idx_list=[e1;..;ep]
@ -98,7 +98,7 @@ let rec bound_check_expr idx_list bounds =
let e = mk_comp idx n in
mk_exp_bool (Eop (op_from_string "&",
[e; bound_check_expr idx_list bounds]))
| (_, _) -> internal_error "mls2obc" 3
| (_, _) -> internal_error "mls2obc"
let mk_plus_one e = match e.e_desc with
| Econst idx ->
@ -144,7 +144,7 @@ let update_record dest src f v =
in
let fields = match dest.pat_ty with
| Tid n -> Modules.find_struct n
| _ -> Misc.internal_error "mls2obc field of nonstruct" 1
| _ -> Misc.internal_error "mls2obc field of nonstruct"
in
List.map assgn_act fields
@ -219,7 +219,7 @@ let rec translate map e =
|Minils.Eselect_trunc|Minils.Eselect_slice
|Minils.Earray_fill|Minils.Efield_update
|Minils.Eifthenelse)}, _, _) ->
internal_error "mls2obc" 5
internal_error "mls2obc"
in
mk_exp e.Minils.e_ty desc
@ -274,7 +274,7 @@ and translate_act map pat
let x = var_from_name map x in
let t = match x.pat_ty with
| Tarray (t,_) -> t
| _ -> Misc.internal_error "mls2obc select slice type" 5
| _ -> Misc.internal_error "mls2obc select slice type"
in
let b = mk_block [Aassgn (mk_pattern t (Larray (x, mk_evar_int cpt)), e) ] in
[ Afor (cptd, mk_exp_const_int 0, mk_exp_static_int n, b) ]
@ -287,7 +287,7 @@ and translate_act map pat
let x = var_from_name map x in
let t = match x.pat_ty with
| Tarray (t,_) -> t
| _ -> Misc.internal_error "mls2obc select slice type" 5
| _ -> Misc.internal_error "mls2obc select slice type"
in
let idx = mk_exp_int (Eop (op_from_string "+",
[mk_evar_int cpt; mk_exp_int (Econst idx1) ])) in
@ -490,7 +490,7 @@ and translate_iterator map call_context it name_list
| Tarray (t,_) -> t
| _ ->
Format.eprintf "%a" Global_printer.print_type ty;
internal_error "mls2obc" 6
internal_error "mls2obc"
in
let array_of_output name_list ty_list =
List.map2 (fun l ty -> mk_pattern ty (Larray (l, mk_evar_int x))) name_list ty_list

View file

@ -93,7 +93,7 @@ let typing_app h base pat op w_list = match op with
| a::a_l, v::v_l -> (match a.a_name with
| None -> build_env a_l v_l env
| Some n -> build_env a_l v_l ((n,v)::env))
| _ -> Misc.internal_error "Clocking, non matching signature" 2
| _ -> Misc.internal_error "Clocking, non matching signature"
in
let env_pat = build_env node.node_outputs pat_id_list [] in
let env_args = build_env node.node_inputs w_list [] in
@ -110,7 +110,7 @@ let typing_app h base pat op w_list = match op with
| Wvar id -> id
| _ -> error_message w.w_loc Edefclock)
with Not_found ->
Misc.internal_error "Clocking, non matching signature" 3
Misc.internal_error "Clocking, non matching signature"
in
Clocks.Con (sigck_to_ck sck, c, id)
in
@ -141,45 +141,48 @@ let typing_eq h { eq_lhs = pat; eq_rhs = e } =
List.iter (fun (_, e) -> expect_extvalue h ck e) l;
Ck ck, ck
| Eapp({a_op = op}, args, r) ->
(* base clock of the node *)
let ck_r = match r with
(* (* base clock of the node have to be a sub-clock of the reset clock *)
let base_ck = match r with
| None -> fresh_clock ()
| Some(reset) -> ck_of_name h reset in
let ct = typing_app h ck_r pat op args in
ct, ck_r
| Eiterator (it, {a_op = op}, _, pargs, args, r) ->
(* base clock of the node *)
let ck_r = match r with
| None -> fresh_clock()
| Some(reset) -> ck_of_name h reset
in
in *)
let base_ck = fresh_clock () in
let ct = typing_app h base_ck pat op args in
ct, base_ck
| Eiterator (it, {a_op = op}, _, pargs, args, r) ->
(* (* base clock of the node *)
let base_ck = match r with
| None -> fresh_clock ()
| Some(reset) -> ck_of_name h reset
in *)
let base_ck = fresh_clock() in
let ct = match it with
| Imap -> (* exactly as if clocking the node *)
typing_app h ck_r pat op args
typing_app h base_ck pat op args
| Imapi -> (* clocking the node with the extra [i] input on [ck_r] *)
let i (* stubs [i] as 0 *) =
mk_extvalue ~ty:Initial.tint ~clock:ck_r (Wconst (Initial.mk_static_int 0))
mk_extvalue ~ty:Initial.tint ~clock:base_ck (Wconst (Initial.mk_static_int 0))
in
typing_app h ck_r pat op (args@[i])
typing_app h base_ck pat op (args@[i])
| Ifold | Imapfold ->
(* clocking node with equality constaint on last input and last output *)
let ct = typing_app h ck_r pat op args in
let ct = typing_app h base_ck pat op args in
unify_ck (Clocks.last_clock ct) (Misc.last_element args).w_ck;
ct
| Ifoldi -> (* clocking the node with the extra [i] and last in/out constraints *)
let i (* stubs [i] as 0 *) =
mk_extvalue ~ty:Initial.tint ~clock:ck_r (Wconst (Initial.mk_static_int 0))
mk_extvalue ~ty:Initial.tint ~clock:base_ck (Wconst (Initial.mk_static_int 0))
in
let rec insert_i args = match args with
| [] -> [i]
| [l] -> i::[l]
| h::l -> h::(insert_i l)
in
let ct = typing_app h ck_r pat op (insert_i args) in
let ct = typing_app h base_ck pat op (insert_i args) in
unify_ck (Clocks.last_clock ct) (Misc.last_element args).w_ck;
ct
in
ct, ck_r
ct, base_ck
in
e.e_base_ck <- base;
(try unify ct e.e_ct
@ -230,7 +233,7 @@ let typing_node node =
let h = append_env h node.n_local in
typing_eqs h node.n_equs;
(* synchronize input and output on base : find the free vars and set them to base *)
Env.iter (fun _ ck -> unify_ck (root_ck_of ck) Cbase) h0;
Env.iter (fun _ ck -> unify_ck Cbase (root_ck_of ck)) h0;
(*update clock info in variables descriptions *)
let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in
let node = { node with n_input = List.map set_clock node.n_input;

View file

@ -12,7 +12,7 @@ open Minils
(* Any clock variable left after clocking is free and should be set to level_ck.
Since inputs and outputs are grounded to Cbase, this append when
no data dependance exists between an expression and the inputs/outputs.*)
no data dependence exists between an expression and the inputs/outputs.*)
(* We are confident that it is sufficient to unify level_ck with base_ck
for expressions having a base_ck == Cvar.
@ -21,7 +21,7 @@ open Minils
let exp _ acc e =
let _ = match ck_repr e.e_base_ck with
| Cvar ({contents = Cindex _}) -> unify_ck e.e_base_ck e.e_level_ck
| Cvar {contents = Cindex _} -> unify_ck e.e_base_ck e.e_level_ck
| _ -> ()
in
e,acc (* no recursion since in minils exps are not recursive *)

View file

@ -72,7 +72,7 @@ struct
| Con(_, _, n) -> add n acc
| Cbase | Cvar { contents = Cindex _ } -> acc
| Cvar { contents = Clink ck } -> vars_ck acc ck
let rec vars_ct acc = function
| Ck ck -> vars_ck acc ck
| Cprod c_l -> List.fold_left vars_ct acc c_l
@ -141,7 +141,8 @@ struct
let head ck =
let rec headrec ck l =
match ck with
| Cbase | Cvar { contents = Cindex _ } -> l
| Cbase
| Cvar { contents = Cindex _ } -> l
| Con(ck, _, n) -> headrec ck (n :: l)
| Cvar { contents = Clink ck } -> headrec ck l
in

View file

@ -140,7 +140,7 @@ struct
(match q.qual with
| LocalModule -> (* This var is a static parameter, it has to be instanciated *)
(try QualEnv.find q m
with Not_found -> Misc.internal_error "callgraph" 0)
with Not_found -> Misc.internal_error "callgraph")
| _ -> se)
| _ -> se in
se, m
@ -222,8 +222,8 @@ let load_object_file modul =
let modname = match modul with
| Names.Pervasives -> "Pervasives"
| Names.Module n -> n
| Names.LocalModule -> Misc.internal_error "modules" 0
| Names.QualModule _ -> Misc.unsupported "modules" 0
| Names.LocalModule -> Misc.internal_error "modules"
| Names.QualModule _ -> Misc.unsupported "modules"
in
let name = String.uncapitalize modname in
try
@ -318,7 +318,7 @@ let program p =
(* Find the nodes without static parameters *)
let main_nodes = List.filter (function Pnode n -> is_empty n.n_params | _ -> false) p.p_desc in
let main_nodes = List.map (function Pnode n -> n.n_name, []
| _ -> Misc.internal_error "callgraph" 0) main_nodes in
| _ -> Misc.internal_error "callgraph") main_nodes in
info.opened <- ModulEnv.add p.p_modname p ModulEnv.empty;
(* Creates the list of instances starting from these nodes *)
List.iter call_node main_nodes;

View file

@ -128,7 +128,7 @@ and boxed_ty param_env t = match t with
| Types.Tid t when t = Initial.pfloat -> Tclass (Names.local_qn "Float")
| Types.Tid t -> Tclass (qualname_to_class_name t)
| Types.Tarray (t,size) -> Tarray (ty param_env t, static_exp param_env size)
| Types.Tinvalid -> Misc.internal_error "obc2java invalid type" 1
| Types.Tinvalid -> Misc.internal_error "obc2java invalid type"
and tuple_ty param_env ty_l =
let ln = ty_l |> List.length |> Pervasives.string_of_int in
@ -142,7 +142,7 @@ and ty param_env t :Java.ty = match t with
| Types.Tid t when t = Initial.pfloat -> Tfloat
| Types.Tid t -> Tclass (qualname_to_class_name t)
| Types.Tarray (t,size) -> Tarray (ty param_env t, static_exp param_env size)
| Types.Tinvalid -> Misc.internal_error "obc2java invalid type" 1
| Types.Tinvalid -> Misc.internal_error "obc2java invalid type"
and var_dec param_env vd = { vd_type = ty param_env vd.v_type; vd_ident = vd.v_ident }

View file

@ -169,19 +169,19 @@ let fold_righti f l acc =
aux 0 l acc
exception Assert_false
let internal_error passe code =
let internal_error passe =
Format.eprintf "@.---------\n
Internal compiler error\n
Passe : %s, Code : %d\n
----------@." passe code;
Passe : %s\n
----------@." passe;
raise Assert_false
exception Unsupported
let unsupported passe code =
let unsupported passe =
Format.eprintf "@.---------\n
Unsupported feature, please report it\n
Passe : %s, Code : %d\n
----------@." passe code;
Passe : %s\n
----------@." passe;
raise Unsupported
(* Functions to decompose a list into a tuple *)

View file

@ -98,7 +98,7 @@ val (|>) : 'a -> ('a -> 'b) -> 'b
val file_extension : string -> string
(** Internal error : Is used when an assertion wrong *)
val internal_error : string -> int -> 'a
val internal_error : string -> 'a
(** Unsupported : Is used when something should work but is not currently supported *)
val unsupported : string -> int -> 'a
val unsupported : string -> 'a

View file

@ -17,7 +17,7 @@ coption=
CAMLC=ocamlc
JAVAC=javac
LUSTREC=lustre
CC="gcc -std=c99"
CC="gcc -std=c99 -I../../../lib/c"
# par defaut : pas de test de generation de code

View file

@ -51,5 +51,5 @@ tel
node itmapi(a:int^n) returns (o:int^n)
let
o = mapi <<n>> m(<a>)(a);
tel
o = mapi <<n>> m<(a)>(a);
tel

16
test/good/t.ept Normal file
View file

@ -0,0 +1,16 @@
node count() returns (o : int)
let
o = 0 fby 1;
tel
node main() returns (c : int)
let
automaton
state One
do c = count ()
until count() = 5 then Two
state Two
do c = count ()
until count() = 3 then One
end
tel

15
test/good/tt.ept Normal file
View file

@ -0,0 +1,15 @@
node g() returns (o :int)
let
o = 0 fby 1
tel
node f (i:int) returns (o1,o2,o3:int)
let
reset
o1 = o2 + g();
every true;
o2 = if true then g() else 0;
o3 = o2 + 4;
tel

View file

@ -10,12 +10,12 @@ tel
fun convol_1_h <<n,m,k,kl,kt,kr,kb :int>> (t:int^n^m; line : int^m; i :int) returns (r :int^m)
let
r = mapi<<m>> (kernel_1<<n,m,k,kl,kt,kr,kb>>)(<t,i>) (line)
r = mapi<<m>> (kernel_1<<n,m,k,kl,kt,kr,kb>>)<(t,i)> (line)
tel
fun convol_1 <<n,m,k,kl,kt,kr,kb :int>> (t:int^n^m) returns (r :int^n^m)
let
r = mapi<<n>> ( convol_1_h<<n,m,k,kl,kt,kr,kb>> ) (<t>) (t)
r = mapi<<n>> ( convol_1_h<<n,m,k,kl,kt,kr,kb>> ) <(t)> (t)
tel
@ -37,11 +37,11 @@ tel
fun convol_2_h<<n,m,ktt,klt,kt,ktr,kll,kl,k,kr,krr,kbl,kb,krb,kbb :int>> (t:int^n^m; line : int^m; i :int) returns (r :int^m)
let
r = mapi<<m>> (kernel_2<<n,m,ktt,klt,kt,ktr,kll,kl,k,kr,krr,kbl,kb,krb,kbb>>) (<t,i>) (line)
r = mapi<<m>> (kernel_2<<n,m,ktt,klt,kt,ktr,kll,kl,k,kr,krr,kbl,kb,krb,kbb>>) <(t,i)> (line)
tel
fun convol_2<<n,m,ktt,klt,kt,ktr,kll,kl,k,kr,krr,kbl,kb,krb,kbb :int>>(t:int^n^m) returns (r :int^n^m)
let
r = mapi<<n>> (convol_2_h<<n,m,ktt,klt,kt,ktr,kll,kl,k,kr,krr,kbl,kb,krb,kbb>>) (<t>) (t)
r = mapi<<n>> (convol_2_h<<n,m,ktt,klt,kt,ktr,kll,kl,k,kr,krr,kbl,kb,krb,kbb>>) <(t)> (t)
tel

15
test/tt.ept Normal file
View file

@ -0,0 +1,15 @@
node m(x:int) returns (y:int)
let
y = 0 fby x
tel
node f(x,y:int;c1,c2:bool) returns (o1,o2:int)
var r:bool;
let
r = true;
reset
o1 = m(x when c1);
o2 = y
every (true when c2)
tel