From 52272a2fbe08006770c9b14d021734947bf1e40a Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Tue, 26 Aug 2008 10:26:10 +0200
Subject: [PATCH] Fix a bug occuring when instanciating models.
+ enhance error msg (which helped finding the bug, but that migth
also be useful for ed-users...).
---
src/compiledData.ml | 16 +++----
src/lazyCompiler.ml | 62 +++++++++++++++++++--------
src/licDump.ml | 6 ++-
src/licDump.mli | 3 +-
src/test/should_work/NONREG/model.lus | 28 ++++++++++++
src/test/test.res.exp | 21 +++++++++
6 files changed, 107 insertions(+), 29 deletions(-)
create mode 100644 src/test/should_work/NONREG/model.lus
diff --git a/src/compiledData.ml b/src/compiledData.ml
index 898cafa2..3485d894 100644
--- a/src/compiledData.ml
+++ b/src/compiledData.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 21/08/2008 (at 18:06) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/08/2008 (at 10:17) by Erwan Jahier> *)
(**
@@ -406,15 +406,15 @@ let (type_eff_are_compatible : type_eff -> type_eff -> bool) =
| External_type_eff _, _ -> true
| t1, t2 -> t1 = t2
+let rec (clock_eff_are_equals : clock_eff -> clock_eff -> bool) =
+ fun c1 c2 -> match c1, c2 with
+ | On(_,c1), On(_,c2) -> clock_eff_are_equals c1 c2
+ | c1, c2 -> c1 = c2
+
let (var_eff_are_compatible : var_info_eff -> var_info_eff -> bool) =
fun v1 v2 ->
- let type_is_ok =
- match v1.var_type_eff, v2.var_type_eff with
- | External_type_eff id1, External_type_eff id2 -> id1 = id2
- | External_type_eff _, _ -> true
- | t1, t2 -> t1 = t2
- in
- type_is_ok && v1.var_clock_eff = v2.var_clock_eff
+ (type_eff_are_compatible v1.var_type_eff v2.var_type_eff) &&
+ (clock_eff_are_equals v1.var_clock_eff v2.var_clock_eff)
(****************************************************************************)
(* Utilitaires liés aux node_key *)
diff --git a/src/lazyCompiler.ml b/src/lazyCompiler.ml
index 41a2fbad..1067ff86 100644
--- a/src/lazyCompiler.ml
+++ b/src/lazyCompiler.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 25/08/2008 (at 11:44) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/08/2008 (at 10:25) by Erwan Jahier> *)
open Lxm
@@ -486,28 +486,52 @@ and (node_check_interface_do: t -> CompiledData.node_key -> Lxm.t ->
(** [type_eff_are_compatible t1 t2] checks that t1 is compatible with t2, i.e.,
if t1 = t2 or t1 is abstract and and t2.
*)
- let type_is_comp v1 v2 = CompiledData.var_eff_are_compatible v1 v2 in
+ let msg_prefix =
+ ("provided node for " ^ (Ident.string_of_long (fst nk)) ^
+ " is not compatible with its implementation: ")
+ in
+ let str_of_var = LicDump.type_string_of_var_info_eff in
+ let type_is_not_comp v1 v2 = not (CompiledData.var_eff_are_compatible v1 v2) in
if
- prov_node_exp_eff.node_key_eff = body_node_exp_eff.node_key_eff &&
- (List.for_all2 type_is_comp
- prov_node_exp_eff.inlist_eff body_node_exp_eff.inlist_eff) &&
- (List.for_all2 type_is_comp
- prov_node_exp_eff.outlist_eff body_node_exp_eff.outlist_eff) &&
- prov_node_exp_eff.has_mem_eff = body_node_exp_eff.has_mem_eff &&
- prov_node_exp_eff.is_safe_eff = body_node_exp_eff.is_safe_eff &&
+ prov_node_exp_eff.node_key_eff <> body_node_exp_eff.node_key_eff
+ then
+ raise(Compile_error (node_def.src, msg_prefix ^ " ??? "))
+ else if
+ (List.exists2 type_is_not_comp
+ prov_node_exp_eff.inlist_eff body_node_exp_eff.inlist_eff)
+ then
+ let msg = msg_prefix ^ "bad input profile. \n*** " ^
+ (String.concat "*" (List.map str_of_var prov_node_exp_eff.inlist_eff)) ^
+ " <> " ^
+ (String.concat "*" (List.map str_of_var body_node_exp_eff.inlist_eff))
+ in
+ raise(Compile_error (node_def.src, msg))
+ else if
+ (List.exists2 type_is_not_comp
+ prov_node_exp_eff.outlist_eff body_node_exp_eff.outlist_eff)
+ then
+ let msg = msg_prefix ^ "bad output profile. \n*** " ^
+ (String.concat "*" (List.map str_of_var prov_node_exp_eff.outlist_eff)) ^
+ " <> " ^
+ (String.concat "*" (List.map str_of_var body_node_exp_eff.outlist_eff))
+ in
+ raise(Compile_error (node_def.src, msg))
+ else if
+ prov_node_exp_eff.has_mem_eff <> body_node_exp_eff.has_mem_eff
+ then
+ raise(Compile_error (node_def.src, msg_prefix ^ " node or function?"))
+ else if
+ prov_node_exp_eff.is_safe_eff <> body_node_exp_eff.is_safe_eff
+ then
+ raise(Compile_error (node_def.src, msg_prefix ^ "safe or unsafe?"))
+ else if
match prov_node_exp_eff.def_eff, body_node_exp_eff.def_eff with
- | (AbstractEff,_) -> true
- | (_,_) -> prov_node_exp_eff.def_eff = body_node_exp_eff.def_eff
+ | (AbstractEff,_) -> false
+ | (_,_) -> prov_node_exp_eff.def_eff <> body_node_exp_eff.def_eff
then
- prov_node_exp_eff
+ raise(Compile_error (node_def.src, msg_prefix ^ "abstract or not?"))
else
- raise(
- Compile_error (
- node_def.src,
- ("provided node \n\t" ^
- (LicDump.profile_of_node_exp_eff prov_node_exp_eff) ^
- "\n is not compatible with its implementation \n\t" ^
- (LicDump.profile_of_node_exp_eff body_node_exp_eff))))
+ prov_node_exp_eff
and (node_check_do: t -> CompiledData.node_key -> Lxm.t -> SymbolTab.t ->
diff --git a/src/licDump.ml b/src/licDump.ml
index f2a9efcf..ba3b3262 100644
--- a/src/licDump.ml
+++ b/src/licDump.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 25/08/2008 (at 10:13) by Erwan Jahier> *)
+(** Time-stamp: <modified the 25/08/2008 (at 18:16) by Erwan Jahier> *)
open CompiledData
open Printf
@@ -238,6 +238,10 @@ and (string_of_var_info_eff: var_info_eff -> string) =
fun x ->
(Ident.to_string x.var_name_eff) ^ ":"^(string_of_type_eff x.var_type_eff)
+and (type_string_of_var_info_eff: var_info_eff -> string) =
+ fun x -> (string_of_type_eff x.var_type_eff) ^
+ (string_of_clock2 x.var_clock_eff)
+
and string_of_decl var_info_eff =
(Ident.to_string var_info_eff.var_name_eff) ^ ":" ^
(string_of_type_eff var_info_eff.var_type_eff) ^
diff --git a/src/licDump.mli b/src/licDump.mli
index bb1e3833..e1a50f89 100644
--- a/src/licDump.mli
+++ b/src/licDump.mli
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 22/08/2008 (at 14:53) by Erwan Jahier> *)
+(** Time-stamp: <modified the 25/08/2008 (at 18:04) by Erwan Jahier> *)
open CompiledData
@@ -16,6 +16,7 @@ val const_decl: Ident.long -> const_eff -> string
val profile_of_node_exp_eff: node_exp_eff -> string
val string_of_var_info_eff: var_info_eff -> string
+val type_string_of_var_info_eff: var_info_eff -> string
val string_of_slice_info_eff : slice_info_eff -> string
diff --git a/src/test/should_work/NONREG/model.lus b/src/test/should_work/NONREG/model.lus
new file mode 100644
index 00000000..c1c4fcb0
--- /dev/null
+++ b/src/test/should_work/NONREG/model.lus
@@ -0,0 +1,28 @@
+
+model m
+needs
+ type elementType;
+ node _isEqualTo_(e1 : elementType; e2 : elementType) returns (x : bool);
+provides
+ node est_egal(e1 : elementType; e2 : elementType) returns (x : bool);
+body
+
+
+node est_egal = _isEqualTo_;
+
+end
+
+
+package u
+provides
+ node egal(i1:int; i2:int) returns (o:bool);
+body
+ node egal(i1:int; i2:int) returns (o:bool);
+ let
+ o = (i1 = i2);
+ tel
+
+end
+
+
+package p = m(int, u::egal);
\ No newline at end of file
diff --git a/src/test/test.res.exp b/src/test/test.res.exp
index 4e6244f8..3011281a 100644
--- a/src/test/test.res.exp
+++ b/src/test/test.res.exp
@@ -3439,6 +3439,27 @@ tel
-- end of node mm3::mm3
+----------------------------------------------------------------------
+====> ../lus2lic -vl 2 --compile-all-items should_work/NONREG/model.lus
+Opening file should_work/NONREG/model.lus
+node u::egal(i1:int; i2:int) returns (o:bool);
+let
+ o = (i1 = i2);
+tel
+-- end of node u::egal
+type _p::elementType = int;
+node p::_isEqualTo_(i1:int; i2:int) returns (o:bool);
+let
+ o = (u::egal(i1, i2));
+tel
+-- end of node p::_isEqualTo_
+node p::est_egal(i1:int; i2:int) returns (o:bool);
+let
+ o = (p::_isEqualTo_(i1, i2));
+tel
+-- end of node p::est_egal
+
+
----------------------------------------------------------------------
====> ../lus2lic -vl 2 --compile-all-items should_work/NONREG/mouse.lus
Opening file should_work/NONREG/mouse.lus
--
GitLab