From f8ce6918ad8267248a3eb2dfb34ab457ffbb96be Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Thu, 19 Jun 2014 14:35:21 +0200
Subject: [PATCH] Soc2c: fix the behavior of the arrow soc.
The arrow soc now has a memory used to hold if the first step has be triggered.
---
src/soc2c.ml | 6 +++---
src/socExec.ml | 8 ++++----
src/socExecEvalPredef.ml | 8 +++++---
src/socExecValue.ml | 5 ++---
src/socPredef.ml | 8 +++++---
src/socPredef2c.ml | 12 +++++++-----
test/lus2lic.sum | 4 ++--
test/lus2lic.time | 2 +-
8 files changed, 29 insertions(+), 24 deletions(-)
diff --git a/src/soc2c.ml b/src/soc2c.ml
index 781fc1da..e29dd574 100644
--- a/src/soc2c.ml
+++ b/src/soc2c.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 19/06/2014 (at 10:44) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/06/2014 (at 11:33) by Erwan Jahier> *)
(* let put (os: out_channel) (fmt:('a, unit, string, unit) format4) : 'a = *)
@@ -78,7 +78,7 @@ let rec (string_of_var_expr: Soc.t -> Soc.var_expr -> string) =
| Const("true", _) -> "_true"
| Const("false", _) -> "_false"
| Const(id, _) -> id2s id
- | Var ("mem_pre",_) -> (* Clutch! it's not an interface var... *) "ctx->mem_pre"
+ | Var ("_memory",_) -> (* Clutch! it's not an interface var... *) "ctx->_memory"
| Var (id,_) ->
if not (mem_interface soc id) then id2s id
else if is_memory_less soc then
@@ -260,7 +260,7 @@ let (typedef_of_soc : Soc.t -> string) =
(match soc.have_mem with
| None -> ""
| Some t ->
- Printf.sprintf " /*Memory cell*/\n %s ;\n" (id2s (type_to_string t "mem_pre"))
+ Printf.sprintf " /*Memory cell*/\n %s ;\n" (id2s (type_to_string t "_memory"))
)
in
let str = str ^ (if soc.instances <> [] then " /*INSTANCES*/\n" else "") in
diff --git a/src/socExec.ml b/src/socExec.ml
index 8e9ff5b0..d595cd8c 100644
--- a/src/socExec.ml
+++ b/src/socExec.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 17/06/2014 (at 10:42) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/06/2014 (at 14:32) by Erwan Jahier> *)
open Soc
open Data
@@ -65,7 +65,7 @@ let rec (soc_step : Soc.step_method -> Soc.tbl -> Soc.t -> SocExecValue.ctx
let inst_name =
match soc.instances with
| [] -> let (proc_name,_,_) = node_soc.key in proc_name
- | [inst] -> fst inst
+ | [inst] -> fst inst
| _ -> assert false
in
let path_saved = ctx.cpath in
@@ -78,7 +78,7 @@ let rec (soc_step : Soc.step_method -> Soc.tbl -> Soc.t -> SocExecValue.ctx
else
let first_step = Var ("$first_step",Bool) in
let v = get_value ctx first_step in
- if v = B true then
+ if v = U || v = B true then
(* We are on the first step of node_soc;
- we assign the output var to the default values *)
let ctx = { ctx with cpath=path_saved } in
@@ -88,6 +88,7 @@ let rec (soc_step : Soc.step_method -> Soc.tbl -> Soc.t -> SocExecValue.ctx
and the output will keep their previous value. *)
{ ctx with cpath=path_saved }
in
+ let ctx = { ctx with s = sadd ctx.s ("$first_step"::ctx.cpath) (B false) } in
ctx
)
| Iterator(iter, node_sk, n) ->
@@ -122,7 +123,6 @@ let rec (soc_step : Soc.step_method -> Soc.tbl -> Soc.t -> SocExecValue.ctx
rctx := assign_expr !rctx a_in a_out); (* a_out=a_n *)
!rctx;
in
- let ctx = { ctx with s = sadd ctx.s ("$first_step"::ctx.cpath) (B false) } in
ctx
and (do_gao : Lxm.t -> Soc.tbl -> SocExecValue.ctx -> gao -> SocExecValue.ctx) =
diff --git a/src/socExecEvalPredef.ml b/src/socExecEvalPredef.ml
index b38cb5db..38325b3c 100644
--- a/src/socExecEvalPredef.ml
+++ b/src/socExecEvalPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 26/03/2014 (at 09:45) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/06/2014 (at 14:16) by Erwan Jahier> *)
open SocExecValue
open Data
@@ -318,12 +318,14 @@ let lustre_current ctx =
let lustre_arrow ctx =
let (vn,vv) =
match ([get_val "x" ctx; get_val "y" ctx;
- get_val "$first_step" { ctx with cpath=List.tl ctx.cpath}])
+ get_val "_memory" { ctx with cpath=List.tl ctx.cpath}])
with
| [v1;v2; fs] -> "z"::ctx.cpath, if fs=B false then v2 else v1
| _ -> assert false
in
- { ctx with s = sadd ctx.s vn vv }
+ let ctx = { ctx with s = sadd ctx.s vn vv } in
+ let ctx = { ctx with s = sadd ctx.s ("_memory"::ctx.cpath) (B false) } in
+ ctx
let lustre_hat tl ctx =
let i = match tl with
diff --git a/src/socExecValue.ml b/src/socExecValue.ml
index 93fc94df..8be646fb 100644
--- a/src/socExecValue.ml
+++ b/src/socExecValue.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 16/06/2014 (at 17:53) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/06/2014 (at 14:31) by Erwan Jahier> *)
let dbg = (Verbose.get_flag "exec")
@@ -225,13 +225,12 @@ let (get_val : ident -> ctx -> Data.v) =
in
try find ctx.s (List.rev (id::ctx.cpath))
with Not_found ->
- if id = "$first_step" then Data.B true else (
Verbose.exe ~flag:dbg (fun () ->
let msg = "Warning " ^(path_to_string (id::ctx.cpath)) ^ " unbound in \n"
^ (string_of_substs ctx.s)
in
print_string msg; flush stdout);
- U)
+ U
let (get_enum : ident -> ctx -> ident) =
fun id ctx ->
diff --git a/src/socPredef.ml b/src/socPredef.ml
index b4f3a921..978c8728 100644
--- a/src/socPredef.ml
+++ b/src/socPredef.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 02/06/2014 (at 09:32) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/06/2014 (at 11:43) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
@@ -68,6 +68,8 @@ let first_step = Var("$first_step", Bool)
let (get_mem_name : Soc.key -> Data.t -> string) =
fun (k,tl,_) vt ->
+ "_memory"
+(*
match Str.split (Str.regexp "::") k with
| ["Lustre";op] -> (
match op.[0] with
@@ -75,7 +77,7 @@ let (get_mem_name : Soc.key -> Data.t -> string) =
| _ -> "mem_"^op
)
| _ -> "mem_"^k
-
+*)
let of_fby_soc_key : Soc.var_expr -> Soc.key -> Soc.t =
fun init sk ->
@@ -226,7 +228,7 @@ let of_soc_key : Soc.key -> Soc.t =
}
];
precedences = [];
- have_mem = None;
+ have_mem = Some Bool;
}
| "Lustre::if" -> {
key = sk;
diff --git a/src/socPredef2c.ml b/src/socPredef2c.ml
index 1218be25..bfceb71f 100644
--- a/src/socPredef2c.ml
+++ b/src/socPredef2c.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 18/06/2014 (at 18:24) by Erwan Jahier> *)
+(* Time-stamp: <modified the 19/06/2014 (at 11:34) by Erwan Jahier> *)
open Data
open Soc
@@ -28,10 +28,12 @@ let (lustre_impl : Soc.key -> string) =
let (lustre_arrow : Soc.key -> string) =
fun sk ->
- let ctx = get_ctx_name sk in
- let x,y,z = ctx^".x", ctx^".y", ctx^".z" in
- Printf.sprintf" %s = (first_step)? %s : %s;\n" z x y
-
+(* let ctx = get_ctx_name sk in *)
+(* let x,y,z = ctx^".x", ctx^".y", ctx^".z" in *)
+ let x,y,z = "ctx->x", "ctx->y", "ctx->z" in
+ (Printf.sprintf" %s = (ctx->_memory)? %s : %s;\n" z x y) ^
+ (" ctx->_memory = _false;\n")
+
let (lustre_merge : Soc.key -> string) =
fun sk ->
let ctx = get_ctx_name sk in
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index a1910c22..e102c3d0 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,4 +1,4 @@
-Test Run By jahier on Thu Jun 19 10:58:46 2014
+Test Run By jahier on Thu Jun 19 14:32:33 2014
Native configuration is i686-pc-linux-gnu
=== lus2lic tests ===
@@ -1483,5 +1483,5 @@ XPASS: Test bad programs (semantics): lus2lic {-o /tmp/bug.lic should_fail/seman
# of unexpected failures 149
# of unexpected successes 21
# of expected failures 37
-testcase ./lus2lic.tests/non-reg.exp completed in 143 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 130 seconds
testcase ./lus2lic.tests/progression.exp completed in 0 seconds
diff --git a/test/lus2lic.time b/test/lus2lic.time
index 7ffb5592..6879740d 100644
--- a/test/lus2lic.time
+++ b/test/lus2lic.time
@@ -1,2 +1,2 @@
-testcase ./lus2lic.tests/non-reg.exp completed in 143 seconds
+testcase ./lus2lic.tests/non-reg.exp completed in 130 seconds
testcase ./lus2lic.tests/progression.exp completed in 0 seconds
--
GitLab