From ec68a79c765f907feb08a0a74eff5262bc4cd18c Mon Sep 17 00:00:00 2001 From: Erwan Jahier <jahier@imag.fr> Date: Fri, 26 Aug 2016 10:36:44 +0200 Subject: [PATCH] --when-on-ident: Make sure we don't create the same var twice and replace enumerated clock in the var_info even if it does not appear in a val_exp. nb : luciole-rif is now in the rdbg repo. --- _oasis | 2 +- src/l2lSplit.ml | 5 +- src/l2lWhenOnId.ml | 217 ++++++++++++++++++++++++---------------- src/lic.ml | 4 +- src/licDump.ml | 14 +-- src/licTab.ml | 2 +- src/lv6Compile.ml | 22 ++-- src/lv6MainArgs.ml | 7 +- src/lv6version.ml | 4 +- src/socPredef2cStack.ml | 3 +- utils/luciole-rif | 30 ------ 11 files changed, 163 insertions(+), 147 deletions(-) delete mode 100755 utils/luciole-rif diff --git a/_oasis b/_oasis index ec90b2c5..51dd635d 100644 --- a/_oasis +++ b/_oasis @@ -1,6 +1,6 @@ OASISFormat: 0.4 Name: lustre-v6 -Version: 1.654 +Version: 1.655 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/l2lSplit.ml b/src/l2lSplit.ml index d9e1f00c..fed08a5b 100644 --- a/src/l2lSplit.ml +++ b/src/l2lSplit.ml @@ -195,7 +195,8 @@ and (split_val_exp : bool -> bool -> Lic.val_exp -> Lic.val_exp * split_acc) = let clk_l = ve.ve_clk in let typ_l = ve.ve_typ in assert (List.length typ_l = List.length clk_l); - let nv_l = List.map2 new_var typ_l clk_l in + let nv_l = List.map2 new_var typ_l clk_l + in let lxm = lxm_of_val_exp ve in let vi2val_exp nv = let _,clk = nv.var_clock_eff in @@ -215,7 +216,7 @@ and (split_val_exp : bool -> bool -> Lic.val_exp -> Lic.val_exp * split_acc) = let lpl = List.map (fun nv -> LeftVarLic(nv, lxm)) nv_l in let eq = Lxm.flagit (lpl, rhs) lxm in nve, (eql@[eq], vl@nv_l) - ) + ) | CallByPosLic({it=Lic.VAR_REF _}, _) -> ve, ([],[]) | CallByPosLic({it=Lic.CONST_REF _}, _) -> ve, ([],[]) | CallByPosLic({src=lxm;it=Lic.CONST _}, _) diff --git a/src/l2lWhenOnId.ml b/src/l2lWhenOnId.ml index 4b6aa85c..f9916076 100644 --- a/src/l2lWhenOnId.ml +++ b/src/l2lWhenOnId.ml @@ -1,4 +1,4 @@ -(** Time-stamp: <modified the 07/06/2016 (at 13:30) by Erwan Jahier> *) +(** Time-stamp: <modified the 25/08/2016 (at 17:20) by Erwan Jahier> *) open Lxm open Lic @@ -6,6 +6,7 @@ open AstPredef let dbg = (Lv6Verbose.get_flag "woi") + (********************************************************************************) (** The functions below accumulate (1) the assertions @@ -20,37 +21,15 @@ type acc = * Lic.val_exp srcflagged list (* assertions *) * clock_tbl - -let rec update_clock : clock_tbl -> clock -> clock = - fun clk_tbl clk -> - match clk with - | BaseLic | ClockVar _ -> clk - | On((cc,cv,ct),sclk) -> - let sclk = update_clock clk_tbl sclk in - try - let nv = Hashtbl.find clk_tbl (cc,cv) in - On((("Lustre","true"),nv.var_name_eff, Bool_type_eff), sclk) - with Not_found -> - On((cc,cv,ct),sclk) - - let update_var_info : clock_tbl -> var_info -> var_info = - fun tbl vi -> - let (id, clk) = vi.var_clock_eff in - { vi with var_clock_eff = id, update_clock tbl clk } - - let rec update_left : clock_tbl -> left -> left = - fun tbl l -> - match l with - | LeftVarLic(vi,lxm) -> LeftVarLic(update_var_info tbl vi,lxm) - | LeftFieldLic(l,id,t) -> LeftFieldLic(update_left tbl l,id,t) - | LeftArrayLic(l,i,t) -> LeftArrayLic(update_left tbl l,i,t) - | LeftSliceLic(l,si,t) -> LeftSliceLic(update_left tbl l,si,t) - - - let new_var (cc,cv) type_eff clock_eff clk_tbl = - try Hashtbl.find clk_tbl (cc,cv) - with Not_found -> +let new_var (cc,cv) type_eff clock_eff clk_tbl = + try Hashtbl.find clk_tbl (cc,cv), true + with Not_found -> let str = (snd cc) ^ "_" ^ cv in + let str2 = (snd cc) ^ "(" ^ cv ^")" in + Lv6Verbose.exe + ~flag:dbg + (fun() -> Printf.printf + "L2lWhenOnId: '%s' not found; create a var\n" str2); let id = Lv6Id.of_string (FreshName.local_var str) in let var = { @@ -62,56 +41,109 @@ let rec update_clock : clock_tbl -> clock -> clock = } in Hashtbl.add clk_tbl (cc,cv) var; - var - - + var,false (********************************************************************************) -(* The one that perform the real work, namely: +(* The one that performs the real work, namely: -- invent a fresh var name NV -- replace 'when Idle(st)' by 'when NV' -- generate the equation defining NV (NV=(Idle=st);) +- if it hasn't been created yet + - invent a fresh var name NV, + - generate the equation defining NV (NV=(Idle=st);) *) - let (gen_ident : Lxm.t -> Lv6Id.long -> Lv6Id.t -> type_ -> Lic.clock -> acc -> - Lic.by_pos_op srcflagged * acc ) = - fun lxm cc cv ct clk (vl,eql,al,tbl) -> (* On(Idle, st, enum_t) *) - - let nv = new_var (cc,cv) Bool_type_eff clk tbl in + var_info * acc ) = + fun lxm cc cv ct clk (vl,eql,al,tbl) -> (* On(Idle, st, enum_t) *) + let nv, already_done = new_var (cc,cv) Bool_type_eff clk tbl in + let ve1 = { + ve_typ = [ct]; + ve_clk = [clk]; + ve_core = CallByPosLic(Lxm.flagit (Lic.CONST_REF cc) lxm,[]) + } + in + let ve2 = { + ve_typ = [ct]; + ve_clk = [clk]; + ve_core = CallByPosLic(Lxm.flagit (Lic.VAR_REF cv) lxm,[]) + } + in + let ve = (* Idle=st *){ + ve_typ = [Bool_type_eff]; + ve_clk = [clk]; + ve_core = + CallByPosLic({it=Lic.PREDEF_CALL({it=(("Lustre","eq"),[]);src=lxm});src=lxm}, + [ve1;ve2]) + } + in + if already_done then + nv, (vl,eql,al,tbl) + else + let new_eq = (* NV=(Idle=st) *) {src=lxm;it=[LeftVarLic (nv, lxm)], 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 + let (_,_,_,clk_tbl) = acc in + try + let nv = Hashtbl.find clk_tbl (cc,cv) in + On((("Lustre","true"),nv.var_name_eff, Bool_type_eff), sclk), acc + with Not_found -> + if cc = ("Lustre","true") || cc = ("Lustre","false") then + On((cc,cv,ct),sclk), acc + else + let nv, acc = gen_ident lxm cc cv ct sclk acc in + On((("Lustre","true"),nv.var_name_eff, Bool_type_eff), sclk), acc - let ve1 = { - ve_typ = [ct]; - ve_clk = [clk]; - ve_core = CallByPosLic(Lxm.flagit (Lic.CONST_REF cc) lxm,[]) - } - in - let ve2 = { - ve_typ = [ct]; - ve_clk = [clk]; - ve_core = CallByPosLic(Lxm.flagit (Lic.VAR_REF cv) lxm,[]) - } - in - let ve = (* Idle=st *){ - ve_typ = [Bool_type_eff]; - ve_clk = [clk]; - ve_core = - CallByPosLic({it=Lic.PREDEF_CALL({it=(("Lustre","eq"),[]);src=lxm});src=lxm}, - [ve1;ve2]) - } - in - let new_eq = (* NV=(Idle=st) *) {src=lxm;it=[LeftVarLic (nv, lxm)], ve} in - let true_cc = "Lustre","true" in - let op = WHEN (On((true_cc, nv.var_name_eff, Bool_type_eff),clk)) in - Lxm.flagit op lxm, (nv::vl,new_eq::eql,al,tbl) +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 + Lv6Verbose.exe + ~flag:dbg + (fun() -> Printf.printf + "#DBG: L2lWhenOnId; update_var_info %s\n" id); + { 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 = List.map (update_left tbl) left_list 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) = @@ -150,12 +182,20 @@ and (do_val_exp: LicPrg.t -> val_exp -> acc -> val_exp * acc) = (List.rev vel) in match op.it with - | WHEN (On((_,_,Bool_type_eff),_)) -> (* nothing to do in this case *) + | WHEN (On((cc,cv,Bool_type_eff),clk)) -> (* nothing to do in this case *) + 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 + | WHEN (On((cc,cv,ct),clk)) -> + let clk, acc = update_clock op.src acc clk in + let nv, acc = gen_ident op.src cc cv ct 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,ct),clk)) -> - let op, acc = gen_ident op.src cc cv ct clk acc in + | _ -> CallByPosLic(op, vel), acc - | _ -> CallByPosLic(op, vel), acc ) in { ve with ve_core = ve_core },acc @@ -169,14 +209,14 @@ and (do_val_exp_flag: LicPrg.t -> val_exp srcflagged -> 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 = + let aux licprg n acc = match n.def_eff with - | ExternLic | MetaOpLic | AbstractLic _ -> n + | ExternLic | MetaOpLic | AbstractLic _ -> n,acc | BodyLic b -> let acc = List.fold_left - (fun acc eq -> do_eq licprg eq acc) - ([],[],[],tbl) - (List.rev b.eqs_eff) + (fun acc eq -> do_eq licprg eq acc) + acc + (List.rev b.eqs_eff) in let acc = List.fold_left (fun acc ve -> @@ -191,19 +231,20 @@ and (do_node : LicPrg.t -> Lic.node_exp -> Lic.node_exp) = | None -> nv (* SNO, but eats no bread *) | Some v -> List.rev_append nv v in - let update_var_info = update_var_info tbl 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.map update_var_info n.inlist_eff; - outlist_eff = List.map update_var_info n.outlist_eff; - loclist_eff = Some (List.map update_var_info nlocs); - } + 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 = aux licprg n in - let n = aux licprg n in (* do it twice to make sure they are all substituted *) + 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 *) diff --git a/src/lic.ml b/src/lic.ml index 5e77e45c..db8d35d0 100644 --- a/src/lic.ml +++ b/src/lic.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 31/05/2016 (at 17:17) by Erwan Jahier> *) +(* Time-stamp: <modified the 07/07/2016 (at 10:23) by Erwan Jahier> *) (** Define the Data Structure representing Compiled programs. By compiled we mean that constant are propagated, packages are @@ -215,8 +215,6 @@ and by_pos_op = ----------------------------------------------------------------------*) and const = (* type predef *) - - Bool_const_eff of bool | Int_const_eff of string | Real_const_eff of string diff --git a/src/licDump.ml b/src/licDump.ml index 7357c06d..df271a00 100644 --- a/src/licDump.ml +++ b/src/licDump.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 31/05/2016 (at 15:18) by Erwan Jahier> *) +(* Time-stamp: <modified the 26/08/2016 (at 10:32) by Erwan Jahier> *) open Lv6errors open Printf @@ -573,14 +573,14 @@ and string_of_val_exp_eff_core ve_core = | Merge (ve, [({it=Bool_const_eff false}, cf); ({it=Bool_const_eff true}, ct)]) -> if global_opt.lv4 then ( "if " ^ (string_of_val_exp_eff ve) ^ " then current (" ^ - (string_of_val_exp_eff ct) ^ ") else current (" ^ - (string_of_val_exp_eff cf) ^")" - ) else ( + (string_of_val_exp_eff ct) ^ ") else current (" ^ + (string_of_val_exp_eff cf) ^")" + ) else ( if global_opt.kcg then ( "merge ( " ^ (string_of_val_exp_eff ve) ^ ";" ^ - (string_of_val_exp_eff ct) ^ "when " ^(string_of_val_exp_eff ve) ^ ";" ^ - (string_of_val_exp_eff cf) ^ "when not " ^ (string_of_val_exp_eff ve) ^ ")" - ) else ( + (string_of_val_exp_eff ct) ^ "when " ^(string_of_val_exp_eff ve) ^ ";" ^ + (string_of_val_exp_eff cf) ^ "when not " ^ (string_of_val_exp_eff ve) ^ ")" + ) else ( "merge " ^ (string_of_val_exp_eff ve) ^ " (true -> " ^ (string_of_val_exp_eff ct) ^ ") (false -> "^ (string_of_val_exp_eff cf) ^")" ) diff --git a/src/licTab.ml b/src/licTab.ml index d2a22a01..8dd05e7f 100644 --- a/src/licTab.ml +++ b/src/licTab.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 27/05/2016 (at 16:02) by Erwan Jahier> *) +(* Time-stamp: <modified the 24/08/2016 (at 14:49) by Erwan Jahier> *) open Lxm diff --git a/src/lv6Compile.ml b/src/lv6Compile.ml index 4ff2a93f..489443b9 100644 --- a/src/lv6Compile.ml +++ b/src/lv6Compile.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 01/06/2016 (at 17:34) by Erwan Jahier> *) +(* Time-stamp: <modified the 25/08/2016 (at 16:50) by Erwan Jahier> *) open Lxm open Lv6errors @@ -51,11 +51,6 @@ let (doit : Lv6MainArgs.t -> AstV6.pack_or_model list -> Lv6Id.idref option -> L profile_info "Optimizing if/then/else...\n"; L2lOptimIte.doit zelic) in - let zelic = (* should be done after, as optim_ite introduces some 'when' *) - if not Lv6MainArgs.global_opt.Lv6MainArgs.when_on_ident then zelic else ( - profile_info "Creating ident on when statements if necessary...\n"; - L2lWhenOnId.doit zelic) - in let zelic = (* élimination polymorphisme surcharge *) profile_info "Removing polymorphism...\n"; @@ -68,7 +63,8 @@ let (doit : Lv6MainArgs.t -> AstV6.pack_or_model list -> Lv6Id.idref option -> L ) in let zelic = - if Lv6MainArgs.global_opt.Lv6MainArgs.kcg && not opt.Lv6MainArgs.inline_iterator then + if Lv6MainArgs.global_opt.Lv6MainArgs.kcg && not opt.Lv6MainArgs.inline_iterator + then L2lExpandMetaOp.doit_boolred zelic else zelic @@ -85,6 +81,12 @@ let (doit : Lv6MainArgs.t -> AstV6.pack_or_model list -> Lv6Id.idref option -> L else zelic in + let zelic = + (* should be done after L2lOptimIte, as it introduces some 'when' *) + if not Lv6MainArgs.global_opt.Lv6MainArgs.when_on_ident then zelic else ( + profile_info "Creating ident on when statements if necessary...\n"; + L2lWhenOnId.doit zelic) + in let zelic = if opt.Lv6MainArgs.expand_node_call <> [] || opt.Lv6MainArgs.expand_nodes then ( let mn:Lv6Id.idref = @@ -96,7 +98,9 @@ let (doit : Lv6MainArgs.t -> AstV6.pack_or_model list -> Lv6Id.idref option -> L ) | Some mn -> mn in - let ids_to_expand = (List.map Lv6Id.idref_of_string opt.Lv6MainArgs.expand_node_call) in + let ids_to_expand = + List.map Lv6Id.idref_of_string opt.Lv6MainArgs.expand_node_call + in let long_match_idref (p,n) idref = (* if no pack is specified, we match them all *) (Lv6Id.name_of_idref idref = n) @@ -145,7 +149,7 @@ let (doit : Lv6MainArgs.t -> AstV6.pack_or_model list -> Lv6Id.idref option -> L L2lCheckLoops.doit zelic ); profile_info "Check unique outputs...\n"; - L2lCheckOutputs.doit zelic; + L2lCheckOutputs.doit zelic; profile_info "Lic Compilation done!\n"; zelic ) diff --git a/src/lv6MainArgs.ml b/src/lv6MainArgs.ml index 94e9755a..b2b9e29d 100644 --- a/src/lv6MainArgs.ml +++ b/src/lv6MainArgs.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 03/06/2016 (at 11:08) by Erwan Jahier> *) +(* Time-stamp: <modified the 26/08/2016 (at 10:18) 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, @@ -318,10 +318,11 @@ let mkoptab (opt:t) : unit = ( (Arg.Unit (fun _ -> global_opt.expand_enums <- AsInt)) [" Translate enums using integers (to be kind with data plotters)"] ; - mkopt opt ~doc_level:Advanced + mkopt opt ~doc_level:Dev ["-eeb"; "--expand-enums-as-bool"] (Arg.Unit (fun _ -> global_opt.expand_enums <- AsBool)) - [" Translate enums using boolean arrays (to be kind with model-checkers)"] + [" Translate enums using boolean arrays (to be kind with model-checkers)"; + "ZZZ: buggy for arrays and using bools is not necessary for lesar."] ; mkopt opt ~doc_level:Advanced ["-esa"; "--expand-structs-and-arrays"] diff --git a/src/lv6version.ml b/src/lv6version.ml index 7b1fb29e..771f2999 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 = "654" -let sha_1 = "579d15a3cca62430283d44d291684fca4d112454" +let commit = "655" +let sha_1 = "c62a8e7015fddbd0c797f63bff56dd0170876a4b" let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")") let maintainer = "jahier@imag.fr" diff --git a/src/socPredef2cStack.ml b/src/socPredef2cStack.ml index ff99b6b5..4968389a 100644 --- a/src/socPredef2cStack.ml +++ b/src/socPredef2cStack.ml @@ -1,4 +1,4 @@ -(* Time-stamp: <modified the 10/04/2015 (at 17:06) by Erwan Jahier> *) +(* Time-stamp: <modified the 26/08/2016 (at 10:34) by Erwan Jahier> *) open Data open Soc @@ -355,6 +355,7 @@ let (get_iterator : Soc.t -> string -> Soc.t -> int -> string) = else buff := !buff^(Soc2cStack.gen_assign telt a_out a_in_bis) ) + | _,_ -> assert false (* SNO *) ); !buff diff --git a/utils/luciole-rif b/utils/luciole-rif deleted file mode 100755 index 0b79427d..00000000 --- a/utils/luciole-rif +++ /dev/null @@ -1,30 +0,0 @@ -#!/bin/sh -# set -x #echo on - -TOOL=luciole-rif - - -if [ "$#" -eq 0 ]; then - echo "usage: $TOOL [any sys call that reads/writes in RIF] -examples: - $TOOL lutin -rif env.lut -n main - $TOOL lus2lic -rif controller.lus -n main - " - exit 01 -fi - -case $1 in - *lutin|*lus2lic) - eval "rdbg-batch -lurette -l 1000 --sut-stdio \"$@ -rif\"" - ;; - *) - eval "rdbg-batch -lurette -l 1000 --sut-stdio \"$@\"" - ;; -esac -rm rdbg_luciole.c -rm rdbg_luciole.dro - -echo "@0: bye" -# pbs: -# - killing luciole does not kill the process -# -- GitLab