From 1026bf313da1e1f9f547e0245819f7c0b0952bce Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Wed, 5 Jun 2013 10:59:44 +0200
Subject: [PATCH] Fix the handling of fby in Soc.
Indeed, the initialisation of the fby was done when the soc was
created. Hence the first fby that was translated was giving its
initial value to all others forthcoming fby !!!
In order to fix that, I've modified the type of Soc.key so that the
initial value is part of its key.
Note that currently, it does not work if the initial value is an input.
---
src/data.ml | 5 +++-
src/lic2soc.ml | 24 ++++++++++++-------
src/soc.ml | 26 ++++++++++++--------
src/socExecEvalPredef.ml | 4 ++--
src/socExecValue.ml | 12 ++++++----
src/socPredef.ml | 40 +++++++++++++++++--------------
src/socUtils.ml | 51 ++++++++++++++++++++++------------------
test/lus2lic.sum | 12 +++++++---
test/lus2lic.time | 4 ++--
9 files changed, 106 insertions(+), 72 deletions(-)
diff --git a/src/data.ml b/src/data.ml
index aed5fd52..a9a22fe8 100644
--- a/src/data.ml
+++ b/src/data.ml
@@ -113,7 +113,10 @@ let rec (update_val : v -> v -> access list -> v) =
A a
)
| A a, (Idx i)::access ->
- let a = Array.copy a in
+ let a = Array.copy a
+ (* necessary for arrays of arrays. It would probably more
+ clever to only copy a_i though. *)
+ in
let a_i = update_val a.(i) v access in
a.(i) <- a_i;
A a
diff --git a/src/lic2soc.ml b/src/lic2soc.ml
index 206e0eae..28164589 100644
--- a/src/lic2soc.ml
+++ b/src/lic2soc.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 17/05/2013 (at 17:46) by Erwan Jahier> *)
+(** Time-stamp: <modified the 05/06/2013 (at 10:57) by Erwan Jahier> *)
open Lxm
open Lic
@@ -261,7 +261,9 @@ let soc_profile_of_node: Lic.node_exp -> Soc.var list * Soc.var list =
let (make_soc_key_of_node_exp : Lic.node_key -> Lic.slice_info option -> Data.t list -> Soc.key) =
fun nk si_opt vl ->
LicDump.string_of_node_key_rec false nk, vl,
- (match si_opt with None -> None | Some si -> Some(si.Lic.se_first,si.Lic.se_last,si.Lic.se_step))
+ (match si_opt with
+ | None -> Soc.Nomore
+ | Some si -> Soc.Slic(si.Lic.se_first,si.Lic.se_last,si.Lic.se_step))
let (soc_key_of_node_exp : Lic.node_exp -> Soc.key) =
fun n ->
@@ -398,7 +400,7 @@ let (make_instance :
| [] -> (
match soc.Soc.have_mem with
| None -> ctx, None
- | Some (_,_) -> (* pre/fby *)
+ | Some (_) -> (* pre/fby *)
let ctx, m = create_instance_from_soc ctx soc in
ctx, Some(m)
)
@@ -510,15 +512,19 @@ let rec (actions_of_expression_acc: Lxm.t -> Soc.tbl ->
(List.flatten (List.map (fun ve -> ve.ve_typ) val_exp_list))
in
let res_type = List.map lic_to_data_type expr.ve_typ in
-(* let res_type = get_exp_type lpl in *)
+ (* let res_type = get_exp_type lpl in *)
let full_profile = args_types @ res_type in
let si_opt = match by_pos_op_flg.it with
Lic.ARRAY_SLICE si -> Some si | _ -> None
in
let sk = make_soc_key_of_node_exp (("",id),[]) si_opt full_profile in
- let fby_init_opt =
+ let (sk_name, sk_prof,_) = sk in
+ let sk,fby_init_opt =
let init = val_exp_to_filter ctx.prg (List.hd val_exp_list) in
- if by_pos_op_flg.it = Lic.FBY then Some init else None
+ if by_pos_op_flg.it = Lic.FBY then
+ (sk_name, sk_prof, Soc.MemInit init), Some init
+ else
+ sk, None
in
try Soc.SocMap.find sk soc_tbl
with Not_found ->
@@ -542,7 +548,7 @@ let rec (actions_of_expression_acc: Lxm.t -> Soc.tbl ->
List.map lic_to_data_type
(List.flatten (List.map (fun (_,ve) -> ve.ve_typ) cl))
in
-(* let res_type = List.map lic_to_data_type expr.ve_typ in *)
+ (* let res_type = List.map lic_to_data_type expr.ve_typ in *)
let res_type = get_exp_type lpl in
let full_profile = args_types @ res_type in
let sk = make_soc_key_of_node_exp (("Lustre","merge"),[]) None full_profile in
@@ -566,7 +572,7 @@ let rec (actions_of_expression_acc: Lxm.t -> Soc.tbl ->
| [] -> assert false
| x::t -> if x = c1 then 0,1 else if x = c2 then 1,0 else aux t
in
- aux l
+ aux l
in
let long_of_const = function Enum_const_eff(l,_) -> l | _ -> assert false in
let compare_enum_case ({it=c1},_) ({it=c2},_) =
@@ -681,7 +687,7 @@ let rec f: (LicPrg.t -> Lic.node_key -> Soc.key * Soc.tbl) =
| Undef_soc (sk,lxm,pos_op, types, fby_init_opt) -> (
let soc = SocPredef.soc_interface_of_pos_op lxm pos_op types fby_init_opt in
- if sk<>soc.key then (
+ if ( sk)<>( soc.key) then (
print_string ("Soc key mismatch :\n\t" ^
(SocUtils.string_of_soc_key sk) ^ "\n<>\n\t" ^
(SocUtils.string_of_soc_key soc.key) ^ "\n");
diff --git a/src/soc.ml b/src/soc.ml
index 32f1ca4f..58f2e007 100644
--- a/src/soc.ml
+++ b/src/soc.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 17/05/2013 (at 17:41) by Erwan Jahier> *)
+(* Time-stamp: <modified the 04/06/2013 (at 17:43) by Erwan Jahier> *)
(** Synchronous Object Component *)
@@ -10,13 +10,6 @@ type ident = string
type var = ident * Data.t
-type key =
- ident *
- Data.t list * (* I/O type list *)
- (int * int * int) option (* to deal with slices (unused FTTB) *)
-
-type instance = ident * key
-
(* Variable denotation *)
type var_expr =
| Var of var
@@ -25,6 +18,19 @@ type var_expr =
| Index of var_expr * int * Data.t
| Slice of var_expr * int * int * int * int * Data.t (* first, last, step, width *)
+type key_opt =
+ | Nomore
+ | Slic of int * int * int (* for slices *)
+ | MemInit of var_expr (* for fby *)
+
+type key =
+ ident *
+ Data.t list * (* I/O type list *)
+ key_opt
+
+type instance = ident * key
+
+
let (data_type_of_var_expr : var_expr -> Data.t) =
function
| Var(_,vt)
@@ -81,8 +87,8 @@ type t = {
step : step_method list; (* the order in the list is a valid w.r.t.
the partial order defined in precedences *)
precedences : precedence list; (* partial order over step methods *)
- have_mem : (Data.t * var_expr option) option;
- (* Do this soc have a memory (pre, fby) + its type + default value *)
+ have_mem : Data.t option;
+ (* Do this soc have a memory (pre, fby) + its type *)
}
diff --git a/src/socExecEvalPredef.ml b/src/socExecEvalPredef.ml
index f27470b0..0e6c814a 100644
--- a/src/socExecEvalPredef.ml
+++ b/src/socExecEvalPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 28/05/2013 (at 15:03) by Erwan Jahier> *)
+(* Time-stamp: <modified the 04/06/2013 (at 17:50) by Erwan Jahier> *)
open SocExecValue
open Data
@@ -247,7 +247,7 @@ let lustre_slice tl si_opt ctx =
in
let (vn,vv) =
match ([get_val "x" ctx], si_opt) with
- | [A a],Some(b,e,step) ->
+ | [A a],Slic(b,e,step) ->
let a_res = Array.make size a.(0) in
let j=ref 0 in
for i = b to e do
diff --git a/src/socExecValue.ml b/src/socExecValue.ml
index b49c2bb3..090bda85 100644
--- a/src/socExecValue.ml
+++ b/src/socExecValue.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 04/06/2013 (at 08:55) by Erwan Jahier> *)
+(* Time-stamp: <modified the 05/06/2013 (at 09:59) by Erwan Jahier> *)
let dbg = (Verbose.get_flag "exec")
@@ -349,16 +349,18 @@ let rec (create_ctx : Soc.tbl -> Soc.t -> ctx) =
let rec (init_soc: Soc.t -> ident list -> substs -> substs) =
fun soc cpath mem ->
let mem =
- match soc.have_mem with
- | Some(vt, Some(dft_value)) ->
+ match soc.have_mem, soc.key with
+ | Some(vt), (_,_,MemInit dft_value) -> (
let name = (SocPredef.get_mem_name soc.key vt)::cpath in
let value = get_value empty_ctx dft_value in
sadd mem name value
- | Some(vt, None) ->
+ )
+ | Some(vt), _ -> (
let name = (SocPredef.get_mem_name soc.key vt)::cpath in
let value = U in
sadd mem name value
- | None -> mem
+ )
+ | None,_ -> mem
in
List.fold_left (init_instances cpath) mem soc.instances
diff --git a/src/socPredef.ml b/src/socPredef.ml
index 1db21156..03f988b7 100644
--- a/src/socPredef.ml
+++ b/src/socPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 03/06/2013 (at 10:51) by Erwan Jahier> *)
+(* Time-stamp: <modified the 04/06/2013 (at 17:48) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
@@ -64,7 +64,8 @@ let make_soc key profile steps = {
}
-let first_instant = Var("first_instant", Bool)
+let first_step = Var("$first_step", Bool)
+
let (get_mem_name : Soc.key -> Data.t -> string) =
fun (k,tl,_) vt ->
match Str.split (Str.regexp "::") k with
@@ -82,19 +83,24 @@ let of_fby_soc_key : Soc.var_expr -> Soc.key -> Soc.t =
let t = List.hd tl in
let pre_mem:var = (get_mem_name sk t, t) in
let prof = soc_profile_of_types tl in
- let v2,vout = match prof with ([_;v2],[vout]) -> v2,vout | _ -> assert false in
+ let v1,v2,vout = match prof with ([v1;v2],[vout]) -> v1,v2,vout | _ -> assert false in
{
key = sk;
profile = prof;
instances = [];
- have_mem = Some (t, Some(init)); (* so that pre_mem exist *)
- step = [
+ have_mem = Some t; (* so that pre_mem exist *)
+ step = [
+(* faire qque chose de init maintenant !!! *)
{
name = "get";
lxm = Lxm.dummy "predef soc";
idx_ins = [];
idx_outs = [0];
impl = Gaol([pre_mem],[Call([Var(vout)], Assign, [Var(pre_mem)])]);
+(* impl = Gaol([pre_mem],[ *)
+(* Case("$first_step", (["t", [Call([Var(vout)], Assign, [Var(v1)])]; *)
+(* "f", [Call([Var(vout)], Assign, [Var(pre_mem)])]])) *)
+(* ]); *)
};
{
name = "set";
@@ -151,7 +157,7 @@ let of_soc_key : Soc.key -> Soc.t =
key = sk;
profile = (sp tl);
instances = [];
- have_mem = Some (t, None); (* so that pre_mem exist *)
+ have_mem = Some (t); (* so that pre_mem exist *)
step = [
{
name = "get";
@@ -181,7 +187,7 @@ let of_soc_key : Soc.key -> Soc.t =
key = sk;
profile = (sp tl);
instances = [];
- have_mem = Some (t, None); (* so that pre_mem exist *)
+ have_mem = Some (t); (* so that pre_mem exist *)
step = [
{
name = "get";
@@ -341,7 +347,7 @@ let make_array_slice_soc : Lic.slice_info -> int -> Data.t -> Soc.t =
let array_type_out = Array(t,size) in
let key_prof = [array_type_in; array_type_out] in
{
- key = ("Lustre::array_slice", key_prof, Some(si.Lic.se_first,si.Lic.se_last,si.Lic.se_step));
+ key = ("Lustre::array_slice", key_prof, Slic(si.Lic.se_first,si.Lic.se_last,si.Lic.se_step));
profile = (["x", array_type_in], ["z", array_type_out]);
instances = [];
step = [
@@ -399,7 +405,7 @@ let make_array_soc: int -> Data.t -> Soc.t =
let array_type = Array(t,i) in
let key_prof = (List.map snd iprof) @ [array_type] in
{
- key = ("Lustre::array", key_prof, None);
+ key = ("Lustre::array", key_prof, Nomore);
profile = (iprof, ["z", array_type]);
instances = [];
step = [
@@ -421,7 +427,7 @@ let make_array_concat_soc: int -> int -> Data.t -> Soc.t =
let iprof = (["x", Array(t,s1); "y", Array(t,s2)], ["z", Array(t,s1+s2)])in
let key_prof = [Array(t,s1); Array(t,s2); Array(t,s1+s2)] in
{
- key = ("Lustre::concat", key_prof, None);
+ key = ("Lustre::concat", key_prof, Nomore);
profile = iprof;
instances = [];
step = [
@@ -445,7 +451,7 @@ let make_hat_soc: int -> Data.t -> Soc.t =
| t -> Data.Array(t,i)
in
{
- key = ("Lustre::hat", [t;array_type], None);
+ key = ("Lustre::hat", [t;array_type], Nomore);
profile = ([("x", t)], ["z", array_type]);
instances = [];
step = [
@@ -483,30 +489,30 @@ let (soc_interface_of_pos_op:
match (op, types,fby_init_opt) with
| Lic.PREDEF_CALL ({Lxm.it=("Lustre","if"),[]}),_ ,_ ->
let concrete_type = List.nth types 1 in
- let soc = of_soc_key ("Lustre::if", types@[concrete_type], None) in
+ let soc = of_soc_key ("Lustre::if", types@[concrete_type], Nomore) in
instanciate_soc soc concrete_type
| Lic.PREDEF_CALL {Lxm.it=(op,sargs)}, _, _ ->
assert (sargs=[]);
let soc_name = Ident.string_of_long op in
let out_type = output_type_of_op soc_name types in
- let soc = of_soc_key (soc_name, types@[out_type], None) in
+ let soc = of_soc_key (soc_name, types@[out_type], Nomore) in
soc
| Lic.FBY, _, Some init ->
let concrete_type = List.nth types 0 in
- let soc = of_fby_soc_key init (("Lustre::fby"), types@[concrete_type], None) in
+ let soc = of_fby_soc_key init (("Lustre::fby"), types@[concrete_type], MemInit init) in
instanciate_soc soc concrete_type
| Lic.FBY, _, None -> assert false (* should ot occur *)
| Lic.PRE, _, _ ->
let concrete_type = List.nth types 0 in
- let soc = of_soc_key (("Lustre::pre"), types@[concrete_type], None) in
+ let soc = of_soc_key (("Lustre::pre"), types@[concrete_type], Nomore) in
instanciate_soc soc concrete_type
| Lic.CURRENT, _, _ ->
let concrete_type = List.nth types 0 in
- let soc = of_soc_key (("Lustre::current"), types@[concrete_type], None) in
+ let soc = of_soc_key (("Lustre::current"), types@[concrete_type], Nomore) in
instanciate_soc soc concrete_type
| Lic.ARROW, _, _ ->
let concrete_type = List.nth types 0 in
- let soc = of_soc_key (("Lustre::arrow"), types@[concrete_type], None) in
+ let soc = of_soc_key (("Lustre::arrow"), types@[concrete_type], Nomore) in
let soc = instanciate_soc soc concrete_type in
soc
| Lic.HAT i,_, _ ->
diff --git a/src/socUtils.ml b/src/socUtils.ml
index 5e9e3f97..e68c457b 100644
--- a/src/socUtils.ml
+++ b/src/socUtils.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 04/06/2013 (at 15:45) by Erwan Jahier> *)
+(** Time-stamp: <modified the 04/06/2013 (at 17:47) by Erwan Jahier> *)
open Soc
@@ -41,20 +41,6 @@ and string_of_type_ref: (Data.t -> string) = fun v ->
call_fun_ff (string_of_type_ref_ff v)
-(* Clé de composant *)
-let string_of_soc_key_ff: (Soc.key -> Format.formatter -> unit) =
- fun (id, types, si_opt) ff ->
- (match types with
- | [] -> fprintf ff "%s" id
- | _ -> fprintf ff "%s:%s" id
- (String.concat " -> " (List.map string_of_type_ref types)));
- (match si_opt with
- | None -> ()
- | Some(f,l,step) -> fprintf ff "[%d .. %d step %d]" f l step)
-
-let string_of_soc_key: (Soc.key -> string) = fun v ->
- call_fun_ff (string_of_soc_key_ff v)
-
(* Variable *)
let string_of_var_ff: (Soc.var -> Format.formatter -> unit) = fun (id, type_) ff ->
@@ -71,14 +57,6 @@ let string_of_instance_ff: (instance -> Format.formatter -> unit) =
let string_of_instance: (instance -> string) = fun (name,sk) -> name
-(* Opération *)
-let string_of_operation_ff: (atomic_operation -> Format.formatter -> unit) = fun v ff -> match v with
- | Assign -> () (* On suppose qu'il est déjà affiché dans string_of_gao *)
- | Method((n, sk),sname) -> fprintf ff "%s.%s" n sname
- | Procedure(proc) -> fprintf ff "%s" (string_of_soc_key proc)
-
-let string_of_operation: (atomic_operation -> string) = fun v ->
- call_fun_ff (string_of_operation_ff v)
(* Filtre d'accès *)
@@ -93,6 +71,33 @@ let rec string_of_filter_ff: (Soc.var_expr -> Format.formatter -> unit) =
let string_of_filter: (Soc.var_expr -> string) = fun v ->
call_fun_ff (string_of_filter_ff v)
+
+(* Clé de composant *)
+let string_of_soc_key_ff: (Soc.key -> Format.formatter -> unit) =
+ fun (id, types, si_opt) ff ->
+ (match types with
+ | [] -> fprintf ff "%s" id
+ | _ -> fprintf ff "%s:%s" id
+ (String.concat " -> " (List.map string_of_type_ref types)));
+ (match si_opt with
+ | Nomore -> ()
+ | Slic(f,l,step) -> fprintf ff "[%d .. %d step %d]" f l step
+ | MemInit ve -> string_of_filter_ff ve ff
+ )
+
+
+let string_of_soc_key: (Soc.key -> string) = fun v ->
+ call_fun_ff (string_of_soc_key_ff v)
+
+(* Opération *)
+let string_of_operation_ff: (atomic_operation -> Format.formatter -> unit) = fun v ff -> match v with
+ | Assign -> () (* On suppose qu'il est déjà affiché dans string_of_gao *)
+ | Method((n, sk),sname) -> fprintf ff "%s.%s" n sname
+ | Procedure(proc) -> fprintf ff "%s" (string_of_soc_key proc)
+
+let string_of_operation: (atomic_operation -> string) = fun v ->
+ call_fun_ff (string_of_operation_ff v)
+
(* Code *)
let rec string_of_gao_ff: (gao -> Format.formatter -> unit) = fun v ff -> match v with
| Case (ck, cases) ->
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index ad5e3c73..f40e614d 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,4 +1,4 @@
-Test Run By jahier on Tue Jun 4 15:46:03 2013
+Test Run By jahier on Wed Jun 5 10:17:20 2013
Native configuration is i686-pc-linux-gnu
=== lus2lic tests ===
@@ -231,6 +231,10 @@ PASS: ./lus2lic {-o /tmp/bascule.lic should_work/bascule.lus}
PASS: ./lus2lic {-ec -o /tmp/bascule.ec should_work/bascule.lus}
PASS: ./myec2c {-o /tmp/bascule.c /tmp/bascule.ec}
PASS: ../utils/test_lus2lic_no_node should_work/bascule.lus
+PASS: ./lus2lic {-o /tmp/double_delay.lic should_work/double_delay.lus}
+PASS: ./lus2lic {-ec -o /tmp/double_delay.ec should_work/double_delay.lus}
+PASS: ./myec2c {-o /tmp/double_delay.c /tmp/double_delay.ec}
+FAIL: Try to compare lus2lic -exec and ecexe: ../utils/test_lus2lic_no_node should_work/double_delay.lus
PASS: ./lus2lic {-o /tmp/struct_with.lic should_work/struct_with.lus}
PASS: ./lus2lic {-ec -o /tmp/struct_with.ec should_work/struct_with.lus}
PASS: ./myec2c {-o /tmp/struct_with.c /tmp/struct_with.ec}
@@ -1020,7 +1024,9 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman
=== lus2lic Summary ===
-# of expected passes 874
-# of unexpected failures 76
+# of expected passes 877
+# of unexpected failures 77
# of unexpected successes 21
# of expected failures 37
+testcase ./lus2lic.tests/non-reg.exp completed in 310 seconds
+testcase ./lus2lic.tests/progression.exp completed in 1 seconds
diff --git a/test/lus2lic.time b/test/lus2lic.time
index 61853046..4ea77774 100644
--- a/test/lus2lic.time
+++ b/test/lus2lic.time
@@ -1,2 +1,2 @@
-testcase ./lus2lic.tests/non-reg.exp completed in 229 seconds
-testcase ./lus2lic.tests/progression.exp completed in 0 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 310 seconds
+testcase ./lus2lic.tests/progression.exp completed in 1 seconds
--
GitLab