From 3b930777a1bae3c7c0b419ae261a49a3139e23f8 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Fri, 29 Mar 2013 17:02:44 +0100
Subject: [PATCH] The -exec mode now supports the boolred iterator.
---
src/lic2soc.ml | 103 ++++++++++++++++++++++++++-----------------
src/licMetaOp.ml | 4 +-
src/misc.ml | 3 +-
src/socExec.ml | 19 ++++++--
src/socExecValue.ml | 11 ++---
src/socExecValue.mli | 12 ++++-
src/socPredef.ml | 11 +----
src/socPredef.mli | 3 +-
src/socUtils.ml | 9 +++-
src/socUtils.mli | 5 ++-
test/lus2lic.sum | 2 +-
test/lus2lic.time | 4 +-
12 files changed, 114 insertions(+), 72 deletions(-)
diff --git a/src/lic2soc.ml b/src/lic2soc.ml
index 35b5ffbe..74f99c73 100644
--- a/src/lic2soc.ml
+++ b/src/lic2soc.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 29/03/2013 (at 11:12) by Erwan Jahier> *)
+(** Time-stamp: <modified the 29/03/2013 (at 16:36) by Erwan Jahier> *)
open Lxm
open Lic
@@ -713,45 +713,68 @@ let rec f: (LicPrg.t -> Lic.node_key -> Soc.key * Soc.tbl) =
in
let (soc_of_metaop: Lic.node_key -> Soc.tbl -> (ctx * Soc.t * Soc.tbl) option) =
fun nk soc_tbl ->
- let iter_node,c = match List.sort compare (snd nk) with
- | [ConstStaticArgLic(_,Int_const_eff(c)) ; NodeStaticArgLic(_,node_key)]
- | [ConstStaticArgLic(_,Int_const_eff(c)) ; TypeStaticArgLic(_);
- NodeStaticArgLic(_,node_key)] ->
- node_key,c
- | _ -> assert false
- in
- let nsk, soc_tbl = process_node iter_node soc_tbl in
- let nsoc = SocUtils.find lxm nsk soc_tbl in
- let nsoc_step = match nsoc.step with [s] -> s
- | _ -> assert false
- (* hmm. Iterating on a pre will not work. XXX fixme ! *)
- in
- let rec make_n_instance ctx acc n =
- if n=0 then ctx,acc else
- match make_instance lxm Lic.BaseLic ctx nsoc with
- | ctx,Some inst -> make_n_instance ctx (inst::acc) (n-1)
- | ctx,None -> ctx,[]
- in
- let c = int_of_string c in
- let ctx, instances = make_n_instance ctx [] c in
- let soc = {
- Soc.key = soc_key;
- Soc.profile = soc_profile_of_node node;
- Soc.instances = instances ;
- Soc.step = [
- {
- name = "step";
- lxm = nsoc_step.lxm;
- idx_ins = nsoc_step.idx_ins;
- idx_outs = nsoc_step.idx_outs;
- impl = Iterator(snd (fst nk), nsk, c);
- }
- ];
- Soc.have_mem = None;
- Soc.precedences = [];
- }
- in
- Some(ctx, soc, soc_tbl)
+ match List.sort compare (snd nk) with
+ | [ConstStaticArgLic(_,Int_const_eff(c)); NodeStaticArgLic(_,iter_node)]
+ | [ConstStaticArgLic(_,Int_const_eff(c)); TypeStaticArgLic(_);
+ NodeStaticArgLic(_,iter_node)] -> (
+ let nsk, soc_tbl = process_node iter_node soc_tbl in
+ let nsoc = SocUtils.find lxm nsk soc_tbl in
+ let nsoc_step = match nsoc.step with [s] -> s
+ | _ -> assert false (* hmm. Iterating on a pre will not work. XXX fixme ! *)
+ in
+ let rec make_n_instance ctx acc n =
+ if n=0 then ctx,acc else
+ match make_instance lxm Lic.BaseLic ctx nsoc with
+ | ctx,Some inst -> make_n_instance ctx (inst::acc) (n-1)
+ | ctx,None -> ctx,[]
+ in
+ let c = int_of_string c in
+ let ctx, instances = make_n_instance ctx [] c in
+ let soc = {
+ Soc.key = soc_key;
+ Soc.profile = soc_profile_of_node node;
+ Soc.instances = instances ;
+ Soc.step = [
+ {
+ name = "step";
+ lxm = nsoc_step.lxm;
+ idx_ins = nsoc_step.idx_ins;
+ idx_outs = nsoc_step.idx_outs;
+ impl = Iterator(snd (fst nk), nsk, c);
+ }
+ ];
+ Soc.have_mem = None;
+ Soc.precedences = [];
+ }
+ in
+ Some(ctx, soc, soc_tbl)
+ )
+ | _ ->
+ match (snd nk) with
+ [ConstStaticArgLic(_,Int_const_eff(i));
+ ConstStaticArgLic(_,Int_const_eff(j));
+ ConstStaticArgLic(_,Int_const_eff(k)) ] -> (
+ let i,j,k = int_of_string i, int_of_string j, int_of_string k in
+ let soc = {
+ Soc.key = soc_key;
+ Soc.profile = soc_profile_of_node node;
+ Soc.instances = [] ;
+ Soc.step = [
+ {
+ name = "step";
+ lxm = lxm;
+ idx_ins = [0];
+ idx_outs = [0];
+ impl = Boolred(i,j,k);
+ }
+ ];
+ Soc.have_mem = None;
+ Soc.precedences = [];
+ }
+ in
+ Some(ctx, soc, soc_tbl)
+ )
+ | _ -> assert false
in
let (soc_of_extern: Lic.node_exp -> Soc.tbl -> (ctx * Soc.t * Soc.tbl) option) =
fun node soc_tbl ->
diff --git a/src/licMetaOp.ml b/src/licMetaOp.ml
index 43ef3b2c..3f841649 100644
--- a/src/licMetaOp.ml
+++ b/src/licMetaOp.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 27/03/2013 (at 09:46) by Erwan Jahier> *)
+(* Time-stamp: <modified the 29/03/2013 (at 16:23) by Erwan Jahier> *)
(* *)
@@ -9,7 +9,7 @@ open Errors
let get_node_and_int_const (lxm: Lxm.t) (sargs: Lic.static_arg list)
: (Lic.node_key * int) =
match sargs with
- | [ NodeStaticArgLic (_,nk); ConstStaticArgLic carg ] -> (
+ | (NodeStaticArgLic (_,nk))::(ConstStaticArgLic carg)::_ -> (
let c = match carg with
| (_, Int_const_eff c) -> c
| (_, Abstract_const_eff(_,_,Int_const_eff c, true)) -> c
diff --git a/src/misc.ml b/src/misc.ml
index 90a245f4..d7ec3f99 100644
--- a/src/misc.ml
+++ b/src/misc.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 23/01/2013 (at 10:06) by Erwan Jahier> *)
+(* Time-stamp: <modified the 29/03/2013 (at 16:06) by Erwan Jahier> *)
open Lic
open Lxm
@@ -42,3 +42,4 @@ let rec (left_eff_to_filtered_left: Lic.left Lxm.srcflagged -> filtered_left) =
f
in
(v,lxm, List.rev f)
+
diff --git a/src/socExec.ml b/src/socExec.ml
index 408f1cbc..25454425 100644
--- a/src/socExec.ml
+++ b/src/socExec.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 29/03/2013 (at 15:45) by Erwan Jahier> *)
+(* Time-stamp: <modified the 29/03/2013 (at 16:57) by Erwan Jahier> *)
open Soc
open SocExecValue
@@ -34,9 +34,20 @@ let rec (soc_step : Soc.step_method -> Soc.tbl -> Soc.t -> SocExecValue.ctx
flush stdout; assert false
)
| Gaol(vl,gaol) -> List.fold_left (do_gao step.lxm soc_tbl) ctx gaol
- | Boolred(i,j,k) ->
- assert false
-
+ | Boolred(i,j,k) -> (
+ let inputs, outputs = soc.profile in
+ let b_array = (List.hd inputs) in
+ let cpt = ref 0 in
+ for i = 0 to k-1 do
+ let a_i = array_index i b_array in
+ let v = SocExecValue.get_value ctx a_i in
+ if v = B true then incr cpt;
+ done;
+ let res = B (!cpt >= i && !cpt <= j) in
+ let res_var = fst (List.hd outputs) in
+ let s = sadd ctx.s (res_var::ctx.cpath) res in
+ { ctx with s = s }
+ )
| Iterator(iter, node_sk, n) ->
let node_soc = SocUtils.find step.lxm node_sk soc_tbl in
let node_step = match node_soc.step with [step] -> step | _ -> assert false in
diff --git a/src/socExecValue.ml b/src/socExecValue.ml
index d33a2b41..c7ac57bc 100644
--- a/src/socExecValue.ml
+++ b/src/socExecValue.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 29/03/2013 (at 09:57) by Erwan Jahier> *)
+(* Time-stamp: <modified the 29/03/2013 (at 16:55) by Erwan Jahier> *)
open Soc
@@ -103,12 +103,7 @@ let rec (get_top_id : Soc.var_expr -> ident) =
-(* [sadd_partial ct ve path v] updates ct by associating ve::path to v in ct ;
-
- nb : It is a more general version of sadd that does not only work on
- var but on var_expr (which means that it can update an array element,
- or a struct field, whereas sadd only updates variable.
-*)
+(* exported *)
let (sadd_partial : substs -> var_expr -> path -> t -> substs) =
fun ct ve x v ->
let top_id = get_top_id ve in
@@ -135,7 +130,7 @@ let (sadd_partial : substs -> var_expr -> path -> t -> substs) =
(* fun ct (x,v) -> *)
(* (x,v)::(List.remove_assoc x ct) *)
-(* [sadd ct x v] updates updates ct by associating x to v in ct *)
+(* exported *)
let (sadd : substs -> path -> t -> substs) =
fun ct x v ->
let rec aux ct (x,v) =
diff --git a/src/socExecValue.mli b/src/socExecValue.mli
index 5f5da7ac..2c67252b 100644
--- a/src/socExecValue.mli
+++ b/src/socExecValue.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 22/03/2013 (at 08:35) by Erwan Jahier> *)
+(* Time-stamp: <modified the 29/03/2013 (at 16:55) by Erwan Jahier> *)
(** Manipulating data in the Soc interpreter *)
@@ -17,10 +17,18 @@ type substs
(* update the memory. The path correspond to a path in the call tree,
except the last ident that is the variable name we want to
associate a value to.
+
+ [sadd ct x v] updates updates ct by associating x to v in ct
*)
val sadd : substs -> path -> t -> substs
-(* ditto, but in the case of a partial assignment (e.g., a[i] = something). *)
+(* [sadd_partial ct ve path v] updates ct by associating ve::path to v in ct ;
+
+ nb : It is a more general version of sadd that does not only work on
+ var but on var_expr. This means that it can update an array element,
+ or a struct field, whereas sadd only updates variable.
+*)
+
val sadd_partial : substs -> Soc.var_expr -> path -> t -> substs
diff --git a/src/socPredef.ml b/src/socPredef.ml
index fac49b2f..a7cdd592 100644
--- a/src/socPredef.ml
+++ b/src/socPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 27/03/2013 (at 15:28) by Erwan Jahier> *)
+(* Time-stamp: <modified the 29/03/2013 (at 16:06) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
@@ -306,13 +306,6 @@ let make_slice_soc: Lic.slice_info -> Soc.var_type -> Soc.t =
(* init = None; *)
}
-let gen_index_list n =
- let rec aux acc i n =
- if i<0 then acc else aux (i::acc) (i-1) n
- in
- aux [] (n-1) n
-
-let _ = assert (gen_index_list 5 = [0;1;2;3;4])
let make_array_soc: int -> Soc.var_type -> Soc.t =
fun i t ->
@@ -333,7 +326,7 @@ let make_array_soc: int -> Soc.var_type -> Soc.t =
{
name = "step";
lxm = Lxm.dummy "predef array soc";
- idx_ins = gen_index_list i;
+ idx_ins = SocUtils.gen_index_list i;
idx_outs = [0];
impl = Predef;
};
diff --git a/src/socPredef.mli b/src/socPredef.mli
index e8e70962..398211cc 100644
--- a/src/socPredef.mli
+++ b/src/socPredef.mli
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 19/03/2013 (at 11:18) by Erwan Jahier> *)
+(* Time-stamp: <modified the 29/03/2013 (at 16:06) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
@@ -14,3 +14,4 @@ val soc_interface_of_pos_op:
Lxm.t -> Lic.by_pos_op -> Soc.var_type list -> Soc.t
val get_mem_name : Soc.key -> Soc.var_type -> string
+
diff --git a/src/socUtils.ml b/src/socUtils.ml
index 4d079aca..ecd20726 100644
--- a/src/socUtils.ml
+++ b/src/socUtils.ml
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 27/03/2013 (at 15:26) by Erwan Jahier> *)
+(** Time-stamp: <modified the 29/03/2013 (at 16:05) by Erwan Jahier> *)
open Soc
@@ -377,4 +377,11 @@ let (find_no_exc : Soc.key -> Soc.tbl -> Soc.t) =
+let gen_index_list n =
+ let rec aux acc i n =
+ if i<0 then acc else aux (i::acc) (i-1) n
+ in
+ aux [] (n-1) n
+
+let _ = assert (gen_index_list 5 = [0;1;2;3;4])
diff --git a/src/socUtils.mli b/src/socUtils.mli
index 91ffcd11..74c139d7 100644
--- a/src/socUtils.mli
+++ b/src/socUtils.mli
@@ -1,4 +1,4 @@
-(** Time-stamp: <modified the 13/03/2013 (at 11:10) by Erwan Jahier> *)
+(** Time-stamp: <modified the 29/03/2013 (at 16:06) by Erwan Jahier> *)
(** Donne toute les méthodes d'un composant. *)
@@ -44,3 +44,6 @@ val find : Lxm.t -> Soc.key -> Soc.tbl -> Soc.t
(* Raise an internal error if not found *)
val find_no_exc : Soc.key -> Soc.tbl -> Soc.t
+
+(* gen_index_list 5 = [0;1;2;3;4] *)
+val gen_index_list : int -> int list
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index e8e78026..507cea7e 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,4 +1,4 @@
-Test Run By jahier on Fri Mar 29 11:35:44 2013
+Test Run By jahier on Fri Mar 29 16:59:38 2013
Native configuration is i686-pc-linux-gnu
=== lus2lic tests ===
diff --git a/test/lus2lic.time b/test/lus2lic.time
index 8eb98ea4..4095f965 100644
--- a/test/lus2lic.time
+++ b/test/lus2lic.time
@@ -1,2 +1,2 @@
-testcase ./lus2lic.tests/non-reg.exp completed in 26 seconds
-testcase ./lus2lic.tests/progression.exp completed in 0 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 25 seconds
+testcase ./lus2lic.tests/progression.exp completed in 1 seconds
--
GitLab