From b29c70ff1e4da8a055fb8d172cbb1e2dddd50d36 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Wed, 21 Jan 2015 17:35:20 +0100
Subject: [PATCH] Check node declaration wrt safety and memory.
More precisely, a node that has memory ougth to be declared using
"node", and using "function" otherwise.
Moreover, a node that performs side-effects (i.e., if it calls an
extern node that performs side effects) ougth to be declared as
"unsafe".
Safe/unsafe mismatches raise an error.
Memory mismatches raise an error in one way (a "function" that uses
memory), and a warning in the other way (a "node" that uses no
memory).
Also fix some errors done when transmitting the unsafe flag (well, it's
the first time I use it!).
---
src/ast2lic.ml | 8 +-
src/astCore.ml | 6 +-
src/astInstanciateModel.ml | 6 +-
src/astV6Dump.ml | 7 +-
src/compile.ml | 4 +-
src/l2lCheckLoops.ml | 3 +-
src/l2lCheckMemSafe.ml | 145 +++++++++++++++++++++++++++++++++++++
src/l2lCheckMemSafe.mli | 23 ++++++
src/l2lOptimIte.ml | 37 +---------
src/licDump.ml | 4 +-
src/licEvalType.ml | 79 ++++++++++----------
src/licEvalType.mli | 8 +-
src/licTab.ml | 6 +-
src/lv6parser.mly | 32 +++++++-
src/lv6version.ml | 4 +-
test/lus2lic.sum | 28 +++----
test/lus2lic.time | 18 ++---
17 files changed, 296 insertions(+), 122 deletions(-)
create mode 100644 src/l2lCheckMemSafe.ml
create mode 100644 src/l2lCheckMemSafe.mli
diff --git a/src/ast2lic.ml b/src/ast2lic.ml
index ce93fa39..b78efbbc 100644
--- a/src/ast2lic.ml
+++ b/src/ast2lic.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 01/09/2014 (at 11:22) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/01/2015 (at 17:00) by Erwan Jahier> *)
open Lxm
@@ -124,7 +124,7 @@ let do_abstract_static_param x =
match x.it with
| StaticParamType id -> ASP_type id
| StaticParamConst (id,_) -> ASP_const id
- | StaticParamNode (id,_,_,_) -> ASP_node id
+ | StaticParamNode (id,_,_,_,_) -> ASP_node id
let get_abstract_static_params
@@ -279,7 +279,7 @@ and check_static_arg
NodeStaticArgLic (id, neff.node_key_eff)
(* node exp vs node *)
| (StaticArgNode (Predef_n (op)), ASP_node id) ->
- let opeff = LicEvalType.make_node_exp_eff node_id_solver None op.it sa.src in
+ let opeff = LicEvalType.make_node_exp_eff node_id_solver None true op.it sa.src in
NodeStaticArgLic (id, opeff.node_key_eff)
| (_, ASP_type _) -> nature_error "type"
| (_, ASP_const _) -> nature_error "constant"
@@ -584,7 +584,7 @@ and node_of_static_arg id_solver node_or_node_ident lxm =
| StaticArgNode(CALL_n ne) -> of_node id_solver ne
| StaticArgNode(Predef_n (op)) ->
- LicEvalType.make_node_exp_eff id_solver None op.it lxm
+ LicEvalType.make_node_exp_eff id_solver None true op.it lxm
| StaticArgNode(_) -> assert false
diff --git a/src/astCore.ml b/src/astCore.ml
index 91cea96c..059f6332 100644
--- a/src/astCore.ml
+++ b/src/astCore.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 19/01/2015 (at 16:26) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/01/2015 (at 16:59) by Erwan Jahier> *)
(** (Raw) Abstract syntax tree of source Lustre Core programs. *)
@@ -38,7 +38,7 @@ and static_param =
| StaticParamType of Ident.t
| StaticParamConst of Ident.t * type_exp
| StaticParamNode of
- (Ident.t * var_info srcflagged list * var_info srcflagged list * has_mem_flag)
+ (Ident.t * var_info srcflagged list * var_info srcflagged list * has_mem_flag * is_safe_flag)
and node_vars = {
inlist : Ident.t list;
@@ -70,6 +70,7 @@ and node_body = {
eqs : (eq_info srcflagged) list;
}
and has_mem_flag = bool
+and is_safe_flag = bool
and eq_info = (left_part list * val_exp)
@@ -149,6 +150,7 @@ and static_arg =
| StaticArgIdent of Ident.idref
| StaticArgConst of val_exp
| StaticArgType of type_exp
+
| StaticArgNode of by_pos_op
(* | StaticArgFunc of node_exp *)
diff --git a/src/astInstanciateModel.ml b/src/astInstanciateModel.ml
index 49db939b..185951d5 100644
--- a/src/astInstanciateModel.ml
+++ b/src/astInstanciateModel.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 11/04/2013 (at 15:47) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/01/2015 (at 16:47) by Erwan Jahier> *)
open Lxm
open AstV6
@@ -79,7 +79,7 @@ let (check_arg :
put_in_tab "const" ctab s y ;
((ConstItem s)::defs, x::prov)
)
- | StaticParamNode (s, inl, outl, has_memory) -> (
+ | StaticParamNode (s, inl, outl, has_memory, is_safe) -> (
let arg = find_arg s in
let by_pos_op = match (arg.it) with
| StaticArgIdent idr -> CALL_n(Lxm.flagit ((idr,[])) arg.src)
@@ -94,7 +94,7 @@ let (check_arg :
loc_consts = [];
def = Alias (flagit by_pos_op arg.src);
has_mem = has_memory;
- is_safe = true;
+ is_safe = is_safe;
}
in
let x = Lxm.flagit (NodeInfo ni) param.src in
diff --git a/src/astV6Dump.ml b/src/astV6Dump.ml
index 3bc44e80..d22c30d2 100644
--- a/src/astV6Dump.ml
+++ b/src/astV6Dump.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 24/04/2013 (at 17:25) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/01/2015 (at 16:56) by Erwan Jahier> *)
open Lxm
@@ -197,8 +197,9 @@ and dump_static_param
| StaticParamType id -> fprintf os "type %s" (Ident.to_string id)
| StaticParamConst (id, exp) -> fprintf os "const %s : %a"
(Ident.to_string id) dump_type_exp exp
- | StaticParamNode (id, ins, outs, has_mem) -> (
- fprintf os "%s %s(@,%a@,)returns(@,%a@,)"
+ | StaticParamNode (id, ins, outs, has_mem,is_safe) -> (
+ fprintf os "%s%s %s(@,%a@,)returns(@,%a@,)"
+ (if is_safe then "" else "unsafe ")
(if has_mem then "node" else "function")
(Ident.to_string id)
dump_line_var_decl_list ins dump_line_var_decl_list outs
diff --git a/src/compile.ml b/src/compile.ml
index 832d9dda..26a9a222 100644
--- a/src/compile.ml
+++ b/src/compile.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 16/01/2015 (at 08:58) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/01/2015 (at 15:15) by Erwan Jahier> *)
open Lxm
open Lv6errors
@@ -41,6 +41,8 @@ let (doit : Lv6MainArgs.t -> AstV6.pack_or_model list -> Ident.idref option -> L
in
info "Converting to lic_prg...\n";
let zelic = LicTab.to_lic_prg lic_tab in
+ info "Check safety and memory declarations...\n";
+ L2lCheckMemSafe.doit zelic;
let zelic =
if not opt.Lv6MainArgs.optim_ite then zelic else (
info "Optimizing if/then/else...\n";
diff --git a/src/l2lCheckLoops.ml b/src/l2lCheckLoops.ml
index 2e84fe83..9dbbfc1f 100644
--- a/src/l2lCheckLoops.ml
+++ b/src/l2lCheckLoops.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 13/08/2014 (at 16:24) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/01/2015 (at 14:37) by Erwan Jahier> *)
open Lxm
open Lv6errors
@@ -117,7 +117,6 @@ let (check_node : Lic.node_exp -> unit) =
let f id _ vi = visit deps vi id [] in
ignore (IdMap.fold f deps vi)
-exception Compile_error_gen of Lxm.t * string
(* exported *)
let (doit : LicPrg.t -> unit) =
diff --git a/src/l2lCheckMemSafe.ml b/src/l2lCheckMemSafe.ml
new file mode 100644
index 00000000..a4f85072
--- /dev/null
+++ b/src/l2lCheckMemSafe.ml
@@ -0,0 +1,145 @@
+(** Time-stamp: <modified the 21/01/2015 (at 17:35) by Erwan Jahier> *)
+
+open Lxm
+open Lic
+open AstPredef
+
+let dbg = (Verbose.get_flag "check-mem")
+
+
+(********************************************************************************)
+(* exported *)
+let (is_memoryless_val_exp : LicPrg.t -> Lic.val_exp -> bool) =
+ fun licprg ve ->
+ let rec (aux_val_exp : Lic.val_exp -> bool) =
+ fun ve -> aux_val_exp_core ve.ve_core
+ and aux_val_exp_core ve_core =
+ match ve_core with
+ | CallByPosLic(op, vel) -> (
+ (List.for_all aux_val_exp vel) && aux_pos_op op.it
+ )
+ | CallByNameLic(_,cl) -> (
+ let vel = (snd (List.split cl)) in
+ List.for_all aux_val_exp vel
+ )
+ | Merge(ve,cl) -> (
+ let vel = ve::(snd (List.split cl)) in
+ List.for_all aux_val_exp vel
+ )
+ and (aux_pos_op: Lic.by_pos_op -> bool) =
+ function
+ | CALL({it=nk}) | PREDEF_CALL({it=nk}) -> (
+ match LicPrg.find_node licprg nk with
+ | None -> true (* SNO *)
+ | Some node_exp -> not node_exp.has_mem_eff
+ )
+ | CURRENT _ | PRE | ARROW | FBY
+ -> false
+ | HAT (_) | ARRAY| ARRAY_SLICE(_) | ARRAY_ACCES(_) | STRUCT_ACCESS(_)
+ | WHEN _ | TUPLE | CONCAT | CONST _ | CONST_REF _ | VAR_REF _
+ -> true
+ in
+ aux_val_exp ve
+
+
+let (check_memory : LicPrg.t -> bool -> val_exp -> Lxm.t -> bool -> bool) =
+ fun licprg should_have_mem ve lxm warning ->
+ match should_have_mem, not (is_memoryless_val_exp licprg ve) with
+ | false, false
+ | true, true -> false (* disable the warning *)
+ | false, true ->
+ let msg = "Error: this call uses memory from a function." in
+ raise (Lv6errors.Compile_error(lxm,msg))
+ | true, false -> warning
+
+(********************************************************************************)
+(* exported *)
+let (is_safe_val_exp : LicPrg.t -> Lic.val_exp -> bool) =
+ fun licprg ve ->
+ let rec (aux_val_exp : Lic.val_exp -> bool) =
+ fun ve -> aux_val_exp_core ve.ve_core
+ and aux_val_exp_core ve_core =
+ match ve_core with
+ | CallByPosLic(op, vel) -> (
+ (List.for_all aux_val_exp vel) && aux_pos_op op.it
+ )
+ | CallByNameLic(_,cl) -> (
+ let vel = (snd (List.split cl)) in
+ List.for_all aux_val_exp vel
+ )
+ | Merge(ve,cl) -> (
+ let vel = ve::(snd (List.split cl)) in
+ List.for_all aux_val_exp vel
+ )
+ and (aux_pos_op: Lic.by_pos_op -> bool) =
+ function
+ | CALL({it=nk}) | PREDEF_CALL({it=nk}) -> (
+ match LicPrg.find_node licprg nk with
+ | None -> true (* SNO *)
+ | Some node_exp -> node_exp.is_safe_eff
+ )
+ | CURRENT _ | PRE | ARROW | FBY
+ | HAT (_) | ARRAY| ARRAY_SLICE(_) | ARRAY_ACCES(_) | STRUCT_ACCESS(_)
+ | WHEN _ | TUPLE | CONCAT | CONST _ | CONST_REF _ | VAR_REF _
+ -> true
+ in
+ aux_val_exp ve
+
+let (check_safety : LicPrg.t -> bool -> val_exp -> Lxm.t -> bool -> bool) =
+ fun licprg should_be_safe ve lxm warning ->
+ match should_be_safe, is_safe_val_exp licprg ve with
+ | false, false
+ | true, true -> false (* disable the warning *)
+ | true, false ->
+ let msg = "Error: calling an unsafe node from a safe one." in
+ raise (Lv6errors.Compile_error(lxm,msg))
+ | false, true -> warning
+
+
+(********************************************************************************)
+let (check_node : LicPrg.t -> Lic.node_exp -> unit) =
+ fun licprg node ->
+ match node.def_eff with
+ | ExternLic | MetaOpLic | AbstractLic _ -> ()
+ | BodyLic{ eqs_eff = eql ; asserts_eff = vel } ->
+ let warning = true in
+ let warning = List.fold_left
+ (fun warn eq -> check_memory licprg node.has_mem_eff (snd eq.it) eq.src warn)
+ warning eql
+ in
+ let warning = List.fold_left
+ (fun warn eq -> check_memory licprg node.has_mem_eff eq.it eq.src warn)
+ warning vel
+ in
+ if warning then (
+ let id = Lic.string_of_node_key node.node_key_eff in
+ let msg = Printf.sprintf
+ "%s is declared as a node, but it uses no memory (i.e., it is a function)."
+ id
+ in
+ Lv6errors.warning node.lxm msg;
+ );
+ let warning = true in
+ let warning = List.fold_left
+ (fun warn eq -> check_safety licprg node.is_safe_eff (snd eq.it) eq.src warn)
+ warning eql
+ in
+ let warning = List.fold_left
+ (fun warn eq -> check_safety licprg node.is_safe_eff eq.it eq.src warn)
+ warning vel
+ in
+ if warning then (
+ let id = Lic.string_of_node_key node.node_key_eff in
+ let msg = Printf.sprintf "%s is declared as unsafe, but is safe." id in
+ Lv6errors.warning node.lxm msg
+ )
+
+
+(* exported *)
+let (doit : LicPrg.t -> unit) =
+ fun inprg ->
+ let rec (do_node : Lic.node_key -> Lic.node_exp -> unit) =
+ fun _nk ne -> check_node inprg ne
+ in
+ LicPrg.iter_nodes do_node inprg
+
diff --git a/src/l2lCheckMemSafe.mli b/src/l2lCheckMemSafe.mli
new file mode 100644
index 00000000..6d00fdc6
--- /dev/null
+++ b/src/l2lCheckMemSafe.mli
@@ -0,0 +1,23 @@
+(** Time-stamp: <modified the 21/01/2015 (at 15:43) by Erwan Jahier> *)
+
+(** Check node declaration wrt safety and memory.
+
+ More precisely, a node that has memory ougth to be declared using
+ "node", and using "function" otherwise.
+
+ Moreover, a node that performs side-effects (i.e., if it calls an
+ extern node that performs side effects) ougth to be declared as
+ "unsafe".
+
+ Safe/unsafe mismatches raise an error.
+
+ Memory mismatches raise an error in one way (a "function" that
+ uses memory), and a warning in the other way (a "node" that uses
+ no memory).
+
+*)
+val doit : LicPrg.t -> unit
+
+
+val is_safe_val_exp : LicPrg.t -> Lic.val_exp -> bool
+val is_memoryless_val_exp : LicPrg.t -> Lic.val_exp -> bool
diff --git a/src/l2lOptimIte.ml b/src/l2lOptimIte.ml
index 00514a7b..bb4eb207 100644
--- a/src/l2lOptimIte.ml
+++ b/src/l2lOptimIte.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 21/01/2015 (at 11:47) by Erwan Jahier> *)
+(** Time-stamp: <modified the 21/01/2015 (at 15:44) by Erwan Jahier> *)
open Lxm
open Lic
@@ -23,39 +23,10 @@ type acc =
let new_var = LicName.new_var_info
(********************************************************************************)
-let (is_memory_less_and_safe_val_exp : LicPrg.t -> Lic.val_exp -> bool) =
+let (is_memory_less_and_safe_val_exp : LicPrg.t -> Lic.val_exp -> bool) =
fun licprg ve ->
- let rec (aux_val_exp : Lic.val_exp -> bool) =
- fun ve -> aux_val_exp_core ve.ve_core
- and aux_val_exp_core ve_core =
- match ve_core with
- | CallByPosLic(op, vel) -> (
- (List.for_all aux_val_exp vel) && aux_pos_op op.it
- )
- | CallByNameLic(_,cl) -> (
- let vel = (snd (List.split cl)) in
- List.for_all aux_val_exp vel
- )
- | Merge(ve,cl) -> (
- let vel = ve::(snd (List.split cl)) in
- List.for_all aux_val_exp vel
- )
- and (aux_pos_op: Lic.by_pos_op -> bool) =
- function
- | CALL({it=nk}) | PREDEF_CALL({it=nk}) -> (
- match LicPrg.find_node licprg nk with
- | None -> assert false (* SNO *)
- | Some node_exp -> node_exp.is_safe_eff && not node_exp.has_mem_eff
- )
- | CURRENT _ (* XXX not clear. false is the safe value anyway. *)
- | PRE | ARROW | FBY -> false
-
- | WHEN _
- | TUPLE
- | CONCAT | HAT (_) | ARRAY| ARRAY_SLICE(_) | ARRAY_ACCES(_) | STRUCT_ACCESS(_)
- | CONST _ | CONST_REF _ | VAR_REF _ -> true
- in
- aux_val_exp ve
+ L2lCheckMemSafe.is_safe_val_exp licprg ve &&
+ L2lCheckMemSafe.is_memoryless_val_exp licprg ve
let (clock_of_cond: val_exp -> bool -> acc -> clock * acc) =
fun ve b acc ->
diff --git a/src/licDump.ml b/src/licDump.ml
index 79cd7071..3f4ac8c2 100644
--- a/src/licDump.ml
+++ b/src/licDump.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 14/01/2015 (at 15:13) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/01/2015 (at 17:17) by Erwan Jahier> *)
open Lv6errors
open Printf
@@ -615,6 +615,8 @@ and (const_decl: Ident.long -> Lic.const -> string) =
and node_of_node_exp_eff (neff: Lic.node_exp): string =
wrap_long_profile (
(
+ if neff.is_safe_eff then "" else "unsafe "
+ )^(
if neff.def_eff = ExternLic && not (global_opt.lv4)
(* no extern kwd in v4... *)
then "extern " else ""
diff --git a/src/licEvalType.ml b/src/licEvalType.ml
index 143e5f91..3320c73f 100644
--- a/src/licEvalType.ml
+++ b/src/licEvalType.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 21/01/2015 (at 11:26) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/01/2015 (at 16:55) by Erwan Jahier> *)
open AstPredef
open Lxm
@@ -295,8 +295,8 @@ let op2profile
(* VERSION GÉNÉRALE, valable pour les MACROS, et qui necessite donc
un IdSolver.t
*)
-let make_node_exp_eff (id_solver: IdSolver.t) (has_mem: bool option) (op: op) (lxm: Lxm.t)
- : Lic.node_exp =
+let make_node_exp_eff (id_solver: IdSolver.t) (has_mem: bool option) (is_safe:bool)
+ (op: op) (lxm: Lxm.t) : Lic.node_exp =
let id = AstPredef.op_to_long op in
let (lti,lto) = op2profile (Some id_solver) op lxm in
let i = ref 0 in
@@ -325,7 +325,7 @@ let make_node_exp_eff (id_solver: IdSolver.t) (has_mem: bool option) (op: op) (l
loclist_eff = None;
def_eff = ExternLic;
has_mem_eff = (match has_mem with Some b -> b | None -> false);
- is_safe_eff = true;
+ is_safe_eff = is_safe;
lxm = lxm;
(* is_polym_eff = *)
(* List.exists (fun vi -> Lic.is_polymorphic vi.var_type_eff) inlist_eff || *)
@@ -338,44 +338,45 @@ let make_node_exp_eff (id_solver: IdSolver.t) (has_mem: bool option) (op: op) (l
(* VERSION SIMPLE, valable
UNIQUEMENT pour les NON MACROS
*)
-let make_simple_node_exp_eff (has_mem: bool option) (op: op) (lxm: Lxm.t) : Lic.node_exp =
- let id = AstPredef.op_to_long op in
- let (lti,lto) = op2profile None op lxm in
- let i = ref 0 in
+let make_simple_node_exp_eff (has_mem: bool option) (is_safe:bool)
+ (op: op) (lxm: Lxm.t) : Lic.node_exp =
+ let id = AstPredef.op_to_long op in
+ let (lti,lto) = op2profile None op lxm in
+ let i = ref 0 in
(* let is_polymorphic = ref false in *)
- let to_var_info_eff nature (vid, te) =
- let res =
+ let to_var_info_eff nature (vid, te) =
+ let res =
(* if Lic.is_polymorphic te then is_polymorphic := true ; *)
- {
- var_name_eff = vid;
- var_nature_eff = nature;
- var_number_eff = !i;
- var_type_eff = te;
- var_clock_eff = vid,BaseLic;
- }
- in
- incr i;
- res
- in
- let inlist_eff = List.map (to_var_info_eff AstCore.VarInput) lti in
- let outlist_eff = (i:=0;List.map (to_var_info_eff AstCore.VarOutput) lto) in
- let res =
{
- node_key_eff = id,[] ;
- inlist_eff = inlist_eff;
- outlist_eff = outlist_eff;
- loclist_eff = None;
- def_eff = ExternLic;
- has_mem_eff = (match has_mem with Some b -> b | None -> false );
- is_safe_eff = true;
- lxm = lxm;
- (* is_polym_eff = *)
-(* List.exists (fun vi -> Lic.is_polymorphic vi.var_type_eff) inlist_eff || *)
-(* List.exists (fun vi -> Lic.is_polymorphic vi.var_type_eff) outlist_eff *)
- (* !is_polymorphic *)
+ var_name_eff = vid;
+ var_nature_eff = nature;
+ var_number_eff = !i;
+ var_type_eff = te;
+ var_clock_eff = vid,BaseLic;
}
- in
- res
+ in
+ incr i;
+ res
+ in
+ let inlist_eff = List.map (to_var_info_eff AstCore.VarInput) lti in
+ let outlist_eff = (i:=0;List.map (to_var_info_eff AstCore.VarOutput) lto) in
+ let res =
+ {
+ node_key_eff = id,[] ;
+ inlist_eff = inlist_eff;
+ outlist_eff = outlist_eff;
+ loclist_eff = None;
+ def_eff = ExternLic;
+ has_mem_eff = (match has_mem with Some b -> b | None -> false );
+ is_safe_eff = is_safe;
+ lxm = lxm;
+ (* is_polym_eff = *)
+ (* List.exists (fun vi -> Lic.is_polymorphic vi.var_type_eff) inlist_eff || *)
+ (* List.exists (fun vi -> Lic.is_polymorphic vi.var_type_eff) outlist_eff *)
+ (* !is_polymorphic *)
+ }
+ in
+ res
(* exported *)
let f (id_solver: IdSolver.t) (op: op) (lxm: Lxm.t) : typer = fun ll ->
@@ -403,7 +404,7 @@ let f (id_solver: IdSolver.t) (op: op) (lxm: Lxm.t) : typer = fun ll ->
[Bool_type_eff]
| _ ->
(* general case *)
- let node_eff = make_node_exp_eff id_solver (Some false) op lxm in
+ let node_eff = make_node_exp_eff id_solver (Some false) true op lxm in
let lti = List.map (fun v -> v.var_type_eff) node_eff.inlist_eff
and lto = List.map (fun v -> v.var_type_eff) node_eff.outlist_eff in
let l = List.flatten ll in
diff --git a/src/licEvalType.mli b/src/licEvalType.mli
index a6645720..f0f5bb09 100644
--- a/src/licEvalType.mli
+++ b/src/licEvalType.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 02/04/2013 (at 09:49) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/01/2015 (at 16:55) by Erwan Jahier> *)
(** Performs static evaluations of predefined operators in type expressions *)
@@ -23,9 +23,9 @@ val f : IdSolver.t -> AstPredef.op -> Lxm.t -> typer
- une pour les macros, qui nécessite un IdSolver.t pour traiter les Lic.static_arg list
- l'autre pour les noeuds simple qui peut être utilisée statiquement
*)
-(* [make_node_exp_eff id_solver has_mem op size lxm] *)
+(* [make_node_exp_eff id_solver has_mem is_safe op size lxm] *)
val make_node_exp_eff :
- IdSolver.t -> bool option -> AstPredef.op -> Lxm.t -> Lic.node_exp
+ IdSolver.t -> bool option -> bool -> AstPredef.op -> Lxm.t -> Lic.node_exp
val make_simple_node_exp_eff :
- bool option -> AstPredef.op -> Lxm.t -> Lic.node_exp
+ bool option -> bool -> AstPredef.op -> Lxm.t -> Lic.node_exp
diff --git a/src/licTab.ml b/src/licTab.ml
index 8bfa5ec7..9043953b 100644
--- a/src/licTab.ml
+++ b/src/licTab.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 04/09/2014 (at 13:58) by Erwan Jahier> *)
+(* Time-stamp: <modified the 21/01/2015 (at 17:02) by Erwan Jahier> *)
open Lxm
@@ -59,7 +59,7 @@ let (create : AstTab.t -> t) =
List.iter
(fun op ->
let op_str = AstPredef.op2string op in
- let op_eff = LicEvalType.make_simple_node_exp_eff None op (Lxm.dummy op_str) in
+ let op_eff = LicEvalType.make_simple_node_exp_eff None true op (Lxm.dummy op_str) in
let op_key = AstPredef.op_to_long op, [] in
Hashtbl.add nodes_tbl op_key (Lic.Checked op_eff);
Hashtbl.add prov_nodes_tbl op_key (Lic.Checked op_eff)
@@ -1061,7 +1061,7 @@ and (node_check_interface_do: t -> Lic.node_key -> Lxm.t ->
in
let predef_op_eff =
LicEvalType.make_node_exp_eff node_id_solver
- (Some node_def.it.has_mem) predef_op lxm
+ (Some node_def.it.has_mem) true predef_op lxm
in
predef_op_eff
diff --git a/src/lv6parser.mly b/src/lv6parser.mly
index c0aaba1c..3a55004a 100644
--- a/src/lv6parser.mly
+++ b/src/lv6parser.mly
@@ -595,7 +595,8 @@ StaticParam:
Lxm.id $2,
invars,
outvars,
- true
+ true,
+ true
) in
Lxm.flagit xn $2
}
@@ -607,9 +608,36 @@ StaticParam:
Lxm.id $2,
invars,
outvars,
- false
+ false,
+ true
) in
Lxm.flagit xn $2
+ }
+ | TK_UNSAFE TK_NODE Ident Params TK_RETURNS Params
+ {
+ let invars = clocked_ids_to_var_infos VarInput $4 in
+ let outvars = clocked_ids_to_var_infos VarOutput $6 in
+ let xn = StaticParamNode (
+ Lxm.id $3,
+ invars,
+ outvars,
+ true,
+ false
+ ) in
+ Lxm.flagit xn $3
+ }
+ | TK_UNSAFE TK_FUNCTION Ident Params TK_RETURNS Params
+ {
+ let invars = clocked_ids_to_var_infos VarInput $4 in
+ let outvars = clocked_ids_to_var_infos VarOutput $6 in
+ let xn = StaticParamNode (
+ Lxm.id $3,
+ invars,
+ outvars,
+ false,
+ false
+ ) in
+ Lxm.flagit xn $3
}
;
/* Le "." à la fin des noeuds est une fioriture historique,
diff --git a/src/lv6version.ml b/src/lv6version.ml
index d888f2b4..a4dd7a4c 100644
--- a/src/lv6version.ml
+++ b/src/lv6version.ml
@@ -1,7 +1,7 @@
(** Automatically generated from Makefile *)
let tool = "lus2lic"
let branch = "master"
-let commit = "549"
-let sha_1 = "54138036f775e06382e1ebee19efdbdd44b4d082"
+let commit = "550"
+let sha_1 = "6af23f417545f673c2ae7b41a6770ab07f28db4f"
let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
let maintainer = "jahier@imag.fr"
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index a47bdd8d..50611e8c 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,5 +1,5 @@
==> lus2lic0.sum <==
-Test Run By jahier on Wed Jan 21 13:55:27
+Test Run By jahier on Wed Jan 21 17:29:48
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic0 tests ===
@@ -63,7 +63,7 @@ XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/lecte
XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/s.lus
==> lus2lic1.sum <==
-Test Run By jahier on Wed Jan 21 13:55:29
+Test Run By jahier on Wed Jan 21 17:29:46
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic1 tests ===
@@ -397,7 +397,7 @@ PASS: gcc -o multipar.exec multipar_multipar.c multipar_multipar_loop.c
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus {}
==> lus2lic2.sum <==
-Test Run By jahier on Wed Jan 21 13:55:31
+Test Run By jahier on Wed Jan 21 17:29:50
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic2 tests ===
@@ -727,7 +727,7 @@ PASS: gcc -o zzz2.exec zzz2_zzz2.c zzz2_zzz2_loop.c
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c zzz2.lus {}
==> lus2lic3.sum <==
-Test Run By jahier on Wed Jan 21 13:55:35
+Test Run By jahier on Wed Jan 21 17:29:54
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic3 tests ===
@@ -1230,7 +1230,7 @@ PASS: ./myec2c {-o multipar.c multipar.ec}
PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {}
==> lus2lic4.sum <==
-Test Run By jahier on Wed Jan 21 13:55:33
+Test Run By jahier on Wed Jan 21 17:29:52
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic4 tests ===
@@ -1726,14 +1726,14 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
# of unexpected failures 3
===============================
# Total number of failures: 14
-lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 4 seconds
-lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 55 seconds
-lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 70 seconds
-lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 53 seconds
-lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 78 seconds
+lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 6 seconds
+lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 54 seconds
+lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 83 seconds
+lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 50 seconds
+lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 86 seconds
* Ref time:
-0.07user 0.08system 3:42.41elapsed 0%CPU (0avgtext+0avgdata 3020maxresident)k
-0inputs+0outputs (0major+14898minor)pagefaults 0swaps
+0.04user 0.09system 4:35.95elapsed 0%CPU (0avgtext+0avgdata 3016maxresident)k
+0inputs+0outputs (0major+14919minor)pagefaults 0swaps
* Quick time (-j 4):
-0.04user 0.08system 1:25.07elapsed 0%CPU (0avgtext+0avgdata 3020maxresident)k
-0inputs+0outputs (0major+14926minor)pagefaults 0swaps
+0.06user 0.05system 1:33.07elapsed 0%CPU (0avgtext+0avgdata 3016maxresident)k
+0inputs+0outputs (0major+14922minor)pagefaults 0swaps
diff --git a/test/lus2lic.time b/test/lus2lic.time
index c32bccb5..9a919717 100644
--- a/test/lus2lic.time
+++ b/test/lus2lic.time
@@ -1,11 +1,11 @@
-lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 4 seconds
-lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 55 seconds
-lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 70 seconds
-lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 53 seconds
-lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 78 seconds
+lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 6 seconds
+lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 54 seconds
+lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 83 seconds
+lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 50 seconds
+lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 86 seconds
* Ref time:
-0.07user 0.08system 3:42.41elapsed 0%CPU (0avgtext+0avgdata 3020maxresident)k
-0inputs+0outputs (0major+14898minor)pagefaults 0swaps
+0.04user 0.09system 4:35.95elapsed 0%CPU (0avgtext+0avgdata 3016maxresident)k
+0inputs+0outputs (0major+14919minor)pagefaults 0swaps
* Quick time (-j 4):
-0.04user 0.08system 1:25.07elapsed 0%CPU (0avgtext+0avgdata 3020maxresident)k
-0inputs+0outputs (0major+14926minor)pagefaults 0swaps
+0.06user 0.05system 1:33.07elapsed 0%CPU (0avgtext+0avgdata 3016maxresident)k
+0inputs+0outputs (0major+14922minor)pagefaults 0swaps
--
GitLab