From 1a153291f645c667cb3189a1f1352817bf316944 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Fri, 26 Aug 2016 15:14:02 +0200
Subject: [PATCH] Add the option --no-when-not because ec does not know "when
not".
---
_oasis | 2 +-
src/l2lNoWhenNot.ml | 257 +++++++++++++++++++++++++++++++++++++++++++
src/l2lNoWhenNot.mli | 20 ++++
src/l2lWhenOnId.ml | 7 +-
src/lv6Compile.ml | 7 +-
src/lv6MainArgs.ml | 15 ++-
src/lv6MainArgs.mli | 1 +
src/lv6version.ml | 4 +-
8 files changed, 303 insertions(+), 10 deletions(-)
create mode 100644 src/l2lNoWhenNot.ml
create mode 100644 src/l2lNoWhenNot.mli
diff --git a/_oasis b/_oasis
index 51dd635d..b8954e1e 100644
--- a/_oasis
+++ b/_oasis
@@ -1,6 +1,6 @@
OASISFormat: 0.4
Name: lustre-v6
-Version: 1.655
+Version: 1.656
Synopsis: The Lustre V6 Verimag compiler
Description: This package contains:
(1) lus2lic: the (current) name of the compiler (and interpreter via -exec).
diff --git a/src/l2lNoWhenNot.ml b/src/l2lNoWhenNot.ml
new file mode 100644
index 00000000..8f3d79fb
--- /dev/null
+++ b/src/l2lNoWhenNot.ml
@@ -0,0 +1,257 @@
+(** Time-stamp: <modified the 26/08/2016 (at 15:04) by Erwan Jahier> *)
+
+open Lxm
+open Lic
+open AstPredef
+
+let dbg = (Lv6Verbose.get_flag "nwn")
+
+
+(********************************************************************************)
+(** The functions below accumulate
+ (1) the new assertions
+ (2) the new equations
+ (3) the fresh variables
+ (4) the table mapping boolean clock var to its (created) negation
+**)
+
+type clock_tbl = (Lv6Id.t, Lic.var_info) Hashtbl.t (* use Map.t ? *)
+type acc =
+ Lic.var_info list (* new local vars *)
+ * Lic.eq_info srcflagged list (* equations *)
+ * Lic.val_exp srcflagged list (* assertions *)
+ * clock_tbl
+
+let new_var cv type_eff clock_eff clk_tbl =
+ try Hashtbl.find clk_tbl cv, true
+ with Not_found ->
+ Lv6Verbose.exe
+ ~flag:dbg
+ (fun() -> Printf.printf
+ "L2lNoWhenNot: '%s' not found; create a var\n" cv);
+ let id = Lv6Id.of_string (FreshName.local_var cv) in
+ let var = {
+ var_name_eff = id;
+ var_nature_eff = AstCore.VarLocal;
+ var_number_eff = -1;
+ var_type_eff = type_eff;
+ var_clock_eff = id,clock_eff;
+ }
+ in
+ Hashtbl.add clk_tbl cv var;
+ var,false
+
+(********************************************************************************)
+(* The one that performs the real work, namely:
+
+- if it hasn't been created yet
+ - invent a fresh var name NV,
+ - generate the equation defining NV (NV= not v);)
+*)
+let (gen_ident : Lxm.t -> Lv6Id.t -> type_ -> Lic.clock -> acc ->
+ var_info * acc ) =
+ fun lxm cv ct clk (vl,eql,al,tbl) ->
+ let nv, already_done = new_var cv ct clk tbl in
+ if already_done then
+ nv, (vl,eql,al,tbl)
+ else
+ let ve = {
+ ve_typ = [ct];
+ ve_clk = [clk];
+ ve_core = CallByPosLic(Lxm.flagit (Lic.VAR_REF cv) lxm,[])
+ }
+ in
+ let not_ve = {
+ ve_typ = [Bool_type_eff];
+ ve_clk = [clk];
+ ve_core =
+ CallByPosLic({it=Lic.PREDEF_CALL({it=(("Lustre","not"),[]);src=lxm});src=lxm},
+ [ve])
+ }
+ in
+ let new_eq = (* NV= not v *) {src=lxm;it=[LeftVarLic (nv, lxm)], not_ve} in
+ nv, (nv::vl,new_eq::eql,al,tbl)
+
+(********************************************************************************)
+let rec update_clock : Lxm.t -> acc -> clock -> clock * acc =
+ fun lxm acc clk ->
+ match clk with
+ | BaseLic | ClockVar _ -> clk, acc
+ | On((cc,cv,ct),sclk) ->
+ let sclk, acc = update_clock lxm acc sclk in
+ if cc <> ("Lustre","false") then
+ On((cc,cv,ct),sclk), acc
+ else
+ let nv, acc =
+ let (_,_,_,clk_tbl) = acc in
+ try Hashtbl.find clk_tbl cv, acc
+ with Not_found -> gen_ident lxm cv ct sclk acc
+ in
+ On((("Lustre","true"),nv.var_name_eff, Bool_type_eff), sclk), acc
+
+let update_var_info : Lxm.t -> acc -> var_info -> var_info * acc =
+ fun lxm acc vi ->
+ let (id, clk) = vi.var_clock_eff in
+ let clk, acc = update_clock lxm acc clk in
+ { vi with var_clock_eff = id, clk }, acc
+
+let update_var_info_list : Lxm.t -> var_info list * acc -> var_info ->
+ var_info list * acc =
+ fun lxm (res,acc) vi ->
+ let vi, acc = update_var_info lxm acc vi in
+ vi::res, acc
+
+ let rec update_left : acc -> left -> left * acc =
+ fun acc l ->
+ match l with
+ | LeftVarLic(vi,lxm) ->
+ let vi, acc = update_var_info lxm acc vi in
+ LeftVarLic(vi,lxm), acc
+ | LeftFieldLic(l,id,t) ->
+ let l, acc = update_left acc l in
+ LeftFieldLic(l,id,t),acc
+ | LeftArrayLic(l,i,t) ->
+ let l, acc = update_left acc l in
+ LeftArrayLic(l,i,t), acc
+ | LeftSliceLic(l,si,t) ->
+ let l, acc = update_left acc l in
+ LeftSliceLic(l,si,t), acc
+
+ let rec update_left_list : left list * acc -> left -> left list * acc =
+ fun (ll,acc) l ->
+ let l, acc = update_left acc l in
+ l::ll, acc
+
+
+(********************************************************************************)
+(* All the remaining are admnistrative functions *)
+
+let rec (do_eq : LicPrg.t -> Lic.eq_info srcflagged -> acc -> acc) =
+ fun licprg { src = lxm_eq ; it = (left_list, ve) } acc ->
+ let ve, (nv,neqs,nass,tbl) = do_val_exp licprg ve acc in
+ let left_list,acc = List.fold_left update_left_list ([],acc) left_list in
+ let left_list = List.rev left_list in
+ nv, { src = lxm_eq ; it = (left_list, ve) }::neqs, nass,tbl
+
+and (do_val_exp: LicPrg.t -> val_exp -> acc -> val_exp * acc) =
+ fun licprg ve acc ->
+ let ve_core, acc =
+ match ve.ve_core with
+ | Merge(ce,cl) -> (
+ let cl,acc =
+ List.fold_left
+ (fun (ncl,acc) (c, ve) ->
+ let ve, acc = do_val_exp licprg ve acc in
+ ((c, ve)::ncl), acc)
+ ([],acc)
+ cl
+ in
+ Merge(ce,cl),acc
+ )
+ | CallByNameLic(op, fl) -> (
+ let fl,acc = List.fold_left
+ (fun (nfl,acc) (id,ve) ->
+ let nf, acc = do_val_exp licprg ve acc in
+ ((id,nf)::nfl), acc
+ )
+ ([],acc)
+ fl
+ in
+ CallByNameLic(op, fl), acc
+ )
+ | CallByPosLic (op, vel) -> (
+ let vel, acc = List.fold_left
+ (fun (vel,acc) ve ->
+ let ve, acc = do_val_exp licprg ve acc in
+ (ve::vel), acc
+ )
+ ([],acc)
+ (List.rev vel)
+ in
+ match op.it with
+ | WHEN (On((("Lustre","false"),cv,Bool_type_eff),clk)) ->
+ let clk, acc = update_clock op.src acc clk in
+ let nv, acc =
+ let (_,_,_,clk_tbl) = acc in
+ try Hashtbl.find clk_tbl cv, acc
+ with Not_found -> gen_ident op.src cv Bool_type_eff clk acc
+ in
+ let true_cc = "Lustre","true" in
+ let new_op = WHEN (On((true_cc, nv.var_name_eff, Bool_type_eff),clk)) in
+ let op = Lxm.flagit new_op op.src in
+ CallByPosLic(op, vel), acc
+ | WHEN (On((cc,cv,Bool_type_eff),clk)) ->
+ let clk, acc = update_clock op.src acc clk in
+ let new_op = WHEN (On((cc, cv, Bool_type_eff),clk)) in
+ let op = Lxm.flagit new_op op.src in
+ CallByPosLic(op, vel), acc
+ | _ ->
+ CallByPosLic(op, vel), acc
+ )
+ in
+ { ve with ve_core = ve_core },acc
+
+and (do_val_exp_flag: LicPrg.t -> val_exp srcflagged -> acc ->
+ val_exp srcflagged * acc) =
+ fun licprg ve_f acc ->
+ let ve, acc = do_val_exp licprg ve_f.it acc in
+ { ve_f with it = ve }, acc
+
+and (do_node : LicPrg.t -> Lic.node_exp -> Lic.node_exp) =
+ fun licprg n ->
+ let tbl = Hashtbl.create 0 in
+ let aux licprg n acc =
+ match n.def_eff with
+ | ExternLic | MetaOpLic | AbstractLic _ -> n,acc
+ | BodyLic b ->
+ let acc = List.fold_left
+ (fun acc eq -> do_eq licprg eq acc)
+ acc
+ (List.rev b.eqs_eff)
+ in
+ let acc = List.fold_left
+ (fun acc ve ->
+ let ve,(nv,neq,nass,tbl) = do_val_exp_flag licprg ve acc in
+ (nv,neq,ve::nass,tbl)
+ )
+ acc
+ b.asserts_eff
+ in
+ let (nv,neqs,nass,tbl) = acc in
+ let nlocs = match n.loclist_eff with
+ | None -> nv (* SNO, but eats no bread *)
+ | Some v -> List.rev_append nv v
+ in
+ let uvi = update_var_info_list n.lxm in
+ let inlist_eff,acc = List.fold_left uvi ([],acc) n.inlist_eff in
+ let outlist_eff,acc = List.fold_left uvi ([],acc) n.outlist_eff in
+ let loclist_eff,acc = List.fold_left uvi ([],acc) nlocs in
+ { n with
+ def_eff = BodyLic { eqs_eff = neqs; asserts_eff = nass };
+ inlist_eff = List.rev inlist_eff;
+ outlist_eff = List.rev outlist_eff;
+ loclist_eff = Some (List.rev loclist_eff)
+ },acc
+ in
+ let n,(_,_,_,tbl) = aux licprg n ([],[],[],tbl) in
+ let n,acc = aux licprg n ([],[],[],tbl) in
+ (* do it twice to make sure they are all substituted *)
+ n
+
+(* exported *)
+let rec (doit : LicPrg.t -> LicPrg.t) =
+ fun inprg ->
+ let outprg = LicPrg.empty in
+ (** types and constants do not change *)
+ let outprg = LicPrg.fold_types LicPrg.add_type inprg outprg in
+ let outprg = LicPrg.fold_consts LicPrg.add_const inprg outprg in
+ (** transform nodes *)
+ let rec (doit_node : Lic.node_key -> Lic.node_exp -> LicPrg.t -> LicPrg.t) =
+ fun nk ne outprg ->
+ Lv6Verbose.exe ~flag:dbg (fun() -> Printf.printf "#DBG: L2lNoWhenNot '%s'\n"
+ (Lic.string_of_node_key nk));
+ let ne = do_node inprg ne in
+ LicPrg.add_node nk ne outprg
+ in
+ let outprg = LicPrg.fold_nodes doit_node inprg outprg in
+ outprg
diff --git a/src/l2lNoWhenNot.mli b/src/l2lNoWhenNot.mli
new file mode 100644
index 00000000..d421bc9e
--- /dev/null
+++ b/src/l2lNoWhenNot.mli
@@ -0,0 +1,20 @@
+(** Time-stamp: <modified the 26/08/2016 (at 10:49) by Erwan Jahier> *)
+
+(** Transforms equations of the form
+
+ y = x when not some_bool_clock;
+
+ into
+
+ not_some_bool_clock : bool;
+ [...]
+
+ y = x when not_some_bool_clock;
+
+It is useful for generating ec code, that does not understand "when not"
+statements (sigh).
+
+*)
+
+val doit : LicPrg.t -> LicPrg.t
+
diff --git a/src/l2lWhenOnId.ml b/src/l2lWhenOnId.ml
index f9916076..ee77956b 100644
--- a/src/l2lWhenOnId.ml
+++ b/src/l2lWhenOnId.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 25/08/2016 (at 17:20) by Erwan Jahier> *)
+(** Time-stamp: <modified the 26/08/2016 (at 10:53) by Erwan Jahier> *)
open Lxm
open Lic
@@ -9,12 +9,13 @@ let dbg = (Lv6Verbose.get_flag "woi")
(********************************************************************************)
(** The functions below accumulate
- (1) the assertions
+ (1) the new assertions
(2) the new equations
(3) the fresh variables
+ (4) the table mapping enumerated clocks to new boolean clock
*)
-type clock_tbl = ((Lv6Id.long * Lv6Id.t), Lic.var_info) Hashtbl.t (* Map.t ? *)
+type clock_tbl = ((Lv6Id.long * Lv6Id.t), Lic.var_info) Hashtbl.t (* use Map.t ? *)
type acc =
Lic.var_info list (* new local vars *)
* Lic.eq_info srcflagged list (* equations *)
diff --git a/src/lv6Compile.ml b/src/lv6Compile.ml
index 489443b9..778b52af 100644
--- a/src/lv6Compile.ml
+++ b/src/lv6Compile.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 25/08/2016 (at 16:50) by Erwan Jahier> *)
+(* Time-stamp: <modified the 26/08/2016 (at 15:07) by Erwan Jahier> *)
open Lxm
open Lv6errors
@@ -129,6 +129,11 @@ let (doit : Lv6MainArgs.t -> AstV6.pack_or_model list -> Lv6Id.idref option -> L
else
zelic
in
+ let zelic =
+ if not Lv6MainArgs.global_opt.Lv6MainArgs.no_when_not then zelic else (
+ profile_info "Replace 'when not' statements by new variables...\n";
+ L2lNoWhenNot.doit zelic)
+ in
(* Array and struct expansion: to do after polymorphism elimination
and after node expansion *)
let zelic = if not opt.Lv6MainArgs.expand_arrays then zelic else (
diff --git a/src/lv6MainArgs.ml b/src/lv6MainArgs.ml
index b2b9e29d..04d9d58d 100644
--- a/src/lv6MainArgs.ml
+++ b/src/lv6MainArgs.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 26/08/2016 (at 10:18) by Erwan Jahier> *)
+(* Time-stamp: <modified the 26/08/2016 (at 15:04) by Erwan Jahier> *)
(*
Le manager d'argument adapté de celui de lutin, plus joli
N.B. solution un peu batarde : les options sont stockées, comme avant, dans Global,
@@ -56,6 +56,7 @@ type global_opt = {
mutable expand_enums : enum_mode;
mutable one_op_per_equation : bool;
mutable when_on_ident : bool;
+ mutable no_when_not : bool;
mutable no_prefix : bool;
mutable nonreg_test : bool;
mutable current_file : string;
@@ -75,6 +76,7 @@ let (global_opt:global_opt) =
ec = false;
one_op_per_equation = true;
when_on_ident = false;
+ no_when_not = false;
no_prefix = false;
nonreg_test = false;
line_num = 1;
@@ -240,6 +242,8 @@ let set_v4_options opt =
let set_ec_options opt =
set_v4_options opt;
global_opt.ec <- true;
+ global_opt.no_when_not <- true;
+ global_opt.no_when_not <- true;
global_opt.no_prefix <- true;
opt.expand_nodes <- true;
opt.optim_ite <- false ; (* because merge won't work *)
@@ -300,9 +304,14 @@ let mkoptab (opt:t) : unit = (
mkopt opt ~doc_level:Advanced
["--when-on-ident"]
(Arg.Unit (fun _ -> global_opt.when_on_ident <- true))
- ["Invent ident name so that when only operates on idents (to be able ";
+ ["Invent ident names so that when only operates on idents (to be able ";
"to translate enums into ec/v4)"]
;
+ mkopt opt ~doc_level:Advanced
+ ["--no-when-not"]
+ (Arg.Unit (fun _ -> global_opt.no_when_not <- true))
+ ["Remove 'when not' statements (for ec) "]
+ ;
mkopt opt ~doc_level:Advanced
["-ei"; "--expand-iterators"]
(Arg.Unit (fun _ -> opt.inline_iterator <- true))
@@ -370,7 +379,7 @@ let mkoptab (opt:t) : unit = (
mkopt opt
["-ec"; "--expanded-code"]
(Arg.Unit (fun _ -> set_ec_options opt))
- ["Generate ec programs (actually just an alias for '-en -lv4 --no-prefix')"]
+ ["Generate ec programs (actually just an alias for '-en -lv4 --no-prefix --no-whe-not')"]
;
mkopt opt ~doc_level:Advanced
["-np"; "--no-prefix"]
diff --git a/src/lv6MainArgs.mli b/src/lv6MainArgs.mli
index 731698f7..76534f6c 100644
--- a/src/lv6MainArgs.mli
+++ b/src/lv6MainArgs.mli
@@ -58,6 +58,7 @@ type global_opt = {
mutable expand_enums : enum_mode;
mutable one_op_per_equation : bool;
mutable when_on_ident : bool;
+ mutable no_when_not : bool;
mutable no_prefix : bool;
mutable nonreg_test : bool;
mutable current_file : string;
diff --git a/src/lv6version.ml b/src/lv6version.ml
index 771f2999..6499d5ab 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 = "655"
-let sha_1 = "c62a8e7015fddbd0c797f63bff56dd0170876a4b"
+let commit = "656"
+let sha_1 = "ec68a79c765f907feb08a0a74eff5262bc4cd18c"
let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
let maintainer = "jahier@imag.fr"
--
GitLab