Skip to content
GitLab
Menu
Projects
Groups
Snippets
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
verimag
synchrone
lustre-v6
Commits
d4748be6
Commit
d4748be6
authored
Jun 19, 2020
by
erwan
Browse files
Fix: current on node calls that had more than one output were not handled properly.
such as in the equation o1,o2 = current (n(x,y,z));
parent
50f8d179
Pipeline
#71200
failed with stages
in 1 minute and 30 seconds
Changes
7
Pipelines
3
Hide whitespace changes
Inline
Side-by-side
Makefile.dev
View file @
d4748be6
#######################################################################################
# debug with ocamldebug
debug
:
cd
bin
;
dune build main.bc
# generates build/default/bin/main.bc
#######################################################################################
...
...
bin/dune
View file @
d4748be6
(executable
(name main)
(modes byte exe)
(libraries lutils extlib lustre-v6)
)
...
...
lib/evalClock.ml
View file @
d4748be6
(* Time-stamp: <modified the
2
9/0
8
/20
19
(at 1
5:31
) by Erwan Jahier> *)
(* Time-stamp: <modified the
1
9/0
6
/20
20
(at 1
4:43
) by Erwan Jahier> *)
open
LicEvalConst
...
...
@@ -297,24 +297,24 @@ let rec (f : IdSolver.t -> subst -> Lic.val_exp -> Lxm.t list -> Lic.clock list
assert
(
ve
.
ve_clk
<>
[]
);
ve
,
inf_clks
,
s
and
(
f_aux
:
IdSolver
.
t
->
subst
->
Lic
.
val_exp
->
Lic
.
val_exp
*
Lic
.
id_clock
list
*
subst
)
=
and
(
f_aux
:
IdSolver
.
t
->
subst
->
Lic
.
val_exp
->
Lic
.
val_exp
*
Lic
.
id_clock
list
*
subst
)
=
fun
id_solver
s
ve
->
let
ve
,
cel
,
s
,
lxm
=
match
ve
.
ve_core
with
|
CallByPosLic
({
it
=
posop
;
src
=
lxm
}
,
args
)
->
(
let
args
,
cel
,
s
=
eval_by_pos_clock
id_solver
posop
lxm
args
s
in
(* current of a constant: we can ignore the current *)
if
(
match
posop
with
CURRENT
_
->
true
|
_
->
false
)
&&
(
List
.
length
args
=
1
)
&&
Lic
.
val_exp_is_constant
(
List
.
hd
args
)
then
(* current of a constant: we can ignore the current *)
let
ve
,
cel
,
s
=
f_aux
id_solver
s
(
List
.
hd
args
)
in
ve
,
cel
,
s
,
lxm
else
let
ve
=
match
posop
,
args
with
|
CURRENT
None
,
{
ve_clk
=
(
On
((
cc
,
cv
,
ct
)
,
cv_clk
))
::
_
;
_
}
::_
->
|
CURRENT
None
,
{
ve_clk
=
(
On
((
cc
,
cv
,
ct
)
,
cv_clk
))
::
clks
;
_
}
::_
->
(* We attach the clock constructor to CURRENT and the
clock var to the list of args. Indeed, the user does not need
to specify the clock when it uses current ; hence we add this
...
...
@@ -325,10 +325,14 @@ and (f_aux : IdSolver.t -> subst -> Lic.val_exp ->
let
cv_val_exp
=
{
ve_core
=
cv_val_exp
;
ve_typ
=
[
ct
]
;
ve_clk
=
[
cv_clk
];
ve_src
=
lxm
}
in
let
posop
,
args
=
CURRENT
(
Some
cc
)
,
cv_val_exp
::
args
in
List
.
iter
(* all clks should be the same *)
(
fun
clk
->
assert
(
clk
=
On
((
cc
,
cv
,
ct
)
,
cv_clk
)))
clks
;
let
ve
=
{
ve
with
ve_core
=
CallByPosLic
({
it
=
posop
;
src
=
lxm
}
,
args
)
;
ve_clk
=
[
cv_clk
]
}
in
ve_clk
=
cv_clk
::
(
List
.
map
(
fun
_
->
cv_clk
)
clks
)
}
in
ve
|
_
->
{
ve
with
ve_core
=
CallByPosLic
({
it
=
posop
;
src
=
lxm
}
,
args
)}
in
...
...
lib/l2lSplit.ml
View file @
d4748be6
...
...
@@ -66,69 +66,69 @@ let to_be_broken = function
let
(
break_it_do
:
val_exp
->
val_exp
list
)
=
fun
ve
->
let
nvel
=
match
ve
.
ve_core
with
|
CallByPosLic
({
it
=
Lic
.
PREDEF_CALL
({
it
=
((
"Lustre"
,
"if"
)
,
[]
)
;
_
});
src
=
lxm
}
,
[
c
;
ve1
;
ve2
])
->
let
vel1
=
get_vel_from_tuple
ve1
and
vel2
=
get_vel_from_tuple
ve2
in
assert
(
List
.
length
vel1
=
List
.
length
vel2
);
List
.
map2
(
fun
ve1
ve2
->
{
ve_core
=
CallByPosLic
({
it
=
Lic
.
PREDEF_CALL
(
{
it
=
((
"Lustre"
,
"if"
)
,
[]
);
src
=
lxm
});
src
=
lxm
}
,
[
c
;
ve1
;
ve2
]);
ve_typ
=
ve1
.
ve_typ
;
ve_clk
=
ve1
.
ve_clk
;
ve_src
=
lxm
}
)
vel1
vel2
|
CallByPosLic
({
it
=
WHEN
clk
;
src
=
lxm
}
,
vel
)
->
(
let
vel
=
List
.
flatten
(
List
.
map
get_vel_from_tuple
vel
)
in
List
.
map
(
fun
ve
->
{
ve
with
ve_core
=
CallByPosLic
({
it
=
WHEN
clk
;
src
=
lxm
}
,
[
ve
])})
vel
)
|
CallByPosLic
({
it
=
Lic
.
TUPLE
;
src
=_
lxm
}
,
vel
)
->
(
remove_tuple
vel
)
|
CallByPosLic
({
it
=
op
;
src
=
lxm
}
,
[
ve
])
->
let
vel
=
get_vel_from_tuple
ve
in
List
.
map
(
fun
ve
->
{
ve
with
ve_core
=
CallByPosLic
({
it
=
op
;
src
=
lxm
}
,
[
ve
])})
vel
|
CallByPosLic
({
it
=
CURRENT
c
;
src
=
lxm
}
,
[
clk
;
ve
])
->
let
vel
=
get_vel_from_tuple
ve
in
List
.
map
(
fun
ve
->
{
ve
with
ve_core
=
CallByPosLic
({
it
=
CURRENT
c
;
src
=
lxm
}
,
[
clk
;
ve
])})
vel
|
CallByPosLic
({
it
=
op
;
src
=
lxm
}
,
[
ve1
;
ve2
])
->
let
vel1
=
get_vel_from_tuple
ve1
and
vel2
=
get_vel_from_tuple
ve2
in
assert
(
List
.
length
vel1
=
List
.
length
vel2
);
List
.
map2
(
fun
ve1
ve2
->
{
ve_core
=
CallByPosLic
({
it
=
op
;
src
=
lxm
}
,
[
ve1
;
ve2
]);
ve_typ
=
ve1
.
ve_typ
;
ve_clk
=
ve1
.
ve_clk
;
ve_src
=
lxm
}
)
vel1
vel2
|
_
->
[
ve
]
(* assert false (* ougth to be dead code (guarded by to_be_broken...) *) *)
in
let
tl
=
ve
.
ve_typ
and
cl
=
ve
.
ve_clk
in
assert
(
List
.
length
ve
.
ve_typ
=
List
.
length
nvel
);
let
nvel
=
List
.
map2
(
fun
nve
t
->
{
nve
with
ve_typ
=
[
t
];
ve_clk
=
cl
}
)
nvel
ve
.
ve_typ
in
assert
(
ve
.
ve_typ
=
tl
);
nvel
let
nvel
=
match
ve
.
ve_core
with
|
CallByPosLic
({
it
=
Lic
.
PREDEF_CALL
({
it
=
((
"Lustre"
,
"if"
)
,
[]
)
;
_
});
src
=
lxm
}
,
[
c
;
ve1
;
ve2
])
->
let
vel1
=
get_vel_from_tuple
ve1
and
vel2
=
get_vel_from_tuple
ve2
in
assert
(
List
.
length
vel1
=
List
.
length
vel2
);
List
.
map2
(
fun
ve1
ve2
->
{
ve_core
=
CallByPosLic
({
it
=
Lic
.
PREDEF_CALL
(
{
it
=
((
"Lustre"
,
"if"
)
,
[]
);
src
=
lxm
});
src
=
lxm
}
,
[
c
;
ve1
;
ve2
]);
ve_typ
=
ve1
.
ve_typ
;
ve_clk
=
ve1
.
ve_clk
;
ve_src
=
lxm
}
)
vel1
vel2
|
CallByPosLic
({
it
=
WHEN
clk
;
src
=
lxm
}
,
vel
)
->
(
let
vel
=
List
.
flatten
(
List
.
map
get_vel_from_tuple
vel
)
in
List
.
map
(
fun
ve
->
{
ve
with
ve_core
=
CallByPosLic
({
it
=
WHEN
clk
;
src
=
lxm
}
,
[
ve
])})
vel
)
|
CallByPosLic
({
it
=
Lic
.
TUPLE
;
src
=_
lxm
}
,
vel
)
->
(
remove_tuple
vel
)
|
CallByPosLic
({
it
=
op
;
src
=
lxm
}
,
[
ve
])
->
let
vel
=
get_vel_from_tuple
ve
in
List
.
map
(
fun
ve
->
{
ve
with
ve_core
=
CallByPosLic
({
it
=
op
;
src
=
lxm
}
,
[
ve
])})
vel
|
CallByPosLic
({
it
=
CURRENT
c
;
src
=
lxm
}
,
[
clk
;
ve
])
->
let
vel
=
get_vel_from_tuple
ve
in
List
.
map
(
fun
ve
->
{
ve
with
ve_core
=
CallByPosLic
({
it
=
CURRENT
c
;
src
=
lxm
}
,
[
clk
;
ve
])})
vel
|
CallByPosLic
({
it
=
op
;
src
=
lxm
}
,
[
ve1
;
ve2
])
->
let
vel1
=
get_vel_from_tuple
ve1
and
vel2
=
get_vel_from_tuple
ve2
in
assert
(
List
.
length
vel1
=
List
.
length
vel2
);
List
.
map2
(
fun
ve1
ve2
->
{
ve_core
=
CallByPosLic
({
it
=
op
;
src
=
lxm
}
,
[
ve1
;
ve2
]);
ve_typ
=
ve1
.
ve_typ
;
ve_clk
=
ve1
.
ve_clk
;
ve_src
=
lxm
}
)
vel1
vel2
|
_
->
[
ve
]
(* assert false (* ougth to be dead code (guarded by to_be_broken...) *) *)
in
let
tl
=
ve
.
ve_typ
and
cl
=
ve
.
ve_clk
in
assert
(
List
.
length
ve
.
ve_typ
=
List
.
length
nvel
);
let
nvel
=
List
.
map2
(
fun
nve
t
->
{
nve
with
ve_typ
=
[
t
];
ve_clk
=
cl
}
)
nvel
ve
.
ve_typ
in
assert
(
ve
.
ve_typ
=
tl
);
nvel
let
rec
(
break_it
:
val_exp
->
val_exp
list
)
=
fun
ve
->
...
...
lib/socPredef.ml
View file @
d4748be6
(* Time-stamp: <modified the
2
9/0
8
/20
19
(at 1
6:45
) by Erwan Jahier> *)
(* Time-stamp: <modified the
1
9/0
6
/20
20
(at 1
4:56
) by Erwan Jahier> *)
(** Synchronous Object Code for Predefined operators. *)
...
...
@@ -556,7 +556,8 @@ let (soc_interface_of_pos_op:
let
concrete_type
=
try
List
.
nth
types
1
with
_
->
assert
false
in
let
soc
=
of_soc_key
lxm
((
"Lustre::current"
)
,
types
@
[
concrete_type
]
,
Curr
(
cc
))
in
instanciate_soc
soc
concrete_type
|
Lic
.
CURRENT
(
_
)
,
_
,
_
->
assert
false
(* sno *)
|
Lic
.
CURRENT
_
,
_
,
_
->
assert
false
(* sno *)
|
Lic
.
ARROW
,
_
,
_
->
let
concrete_type
=
List
.
nth
types
0
in
let
soc
=
of_soc_key
lxm
((
"Lustre::arrow"
)
,
types
@
[
concrete_type
]
,
...
...
lv6-ref-man/Makefile
View file @
d4748be6
...
...
@@ -89,8 +89,6 @@ $(MAIN).pdf : $(PARSER) $(SRCS) $(LUS2TEX) $(SUMMARY) $(FIGS) $(OBJPDF)/version
(
cd
objpdf
;
pdflatex ../
$(MAIN)
.tex
)
mv
objpdf/
$(MAIN)
.pdf .
scp
:
$(MAIN).pdf
scp
$(MAIN)
.pdf jahier@pressembois.imag.fr:/import/www/DIST-TOOLS/SYNCHRONE/lustre-v6/doc
#------------------------------
# Special : fig 2 latex 2 pdf
...
...
test/lus2lic.sum
View file @
d4748be6
==> lus2lic0.sum <==
Test run by jahier on Fri Jun 1
2
1
1:28:54
Test run by jahier on Fri Jun 1
9
1
5:04:42
Native configuration is x86_64-pc-linux-gnu
=== lus2lic0 tests ===
...
...
@@ -66,7 +66,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 Fri Jun 1
2
1
1:28:55
Test run by jahier on Fri Jun 1
9
1
5:04:43
Native configuration is x86_64-pc-linux-gnu
=== lus2lic1 tests ===
...
...
@@ -413,7 +413,7 @@ PASS: ./lus2lic {-2c multipar.lus -n multipar}
PASS: sh multipar.sh
==> lus2lic2.sum <==
Test run by jahier on Fri Jun 1
2
1
1:29:19
Test run by jahier on Fri Jun 1
9
1
5:05:07
Native configuration is x86_64-pc-linux-gnu
=== lus2lic2 tests ===
...
...
@@ -753,7 +753,7 @@ PASS: sh zzz2.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c zzz2.lus {}
==> lus2lic3.sum <==
Test run by jahier on Fri Jun 1
2
1
1:29:4
8
Test run by jahier on Fri Jun 1
9
1
5:05:3
8
Native configuration is x86_64-pc-linux-gnu
=== lus2lic3 tests ===
...
...
@@ -1267,7 +1267,7 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {}
==> lus2lic4.sum <==
Test run by jahier on Fri Jun 1
2
1
1:30:31
Test run by jahier on Fri Jun 1
9
1
5:06:23
Native configuration is x86_64-pc-linux-gnu
=== lus2lic4 tests ===
...
...
@@ -1759,7 +1759,7 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
# of expected failures 54
==> lus2lic1.sum <==
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus
4631
7 {}
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus
3413
7 {}
=== lus2lic1 Summary ===
...
...
@@ -1789,12 +1789,12 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus 46317
# Total number of failures: 10
lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 1 seconds
lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 24 seconds
lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in
29
seconds
lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 4
3
seconds
lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 2
3
seconds
lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in
31
seconds
lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 4
5
seconds
lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 2
2
seconds
* Ref time:
7
1.69
user 16.
57
system
1:59.66
elapsed 73%CPU (0avgtext+0avgdata 42
22
0maxresident)k
16
inputs+1
47896
outputs (0major+84
62673
minor)pagefaults 0swaps
7
4.43
user 16.
16
system
2:02.49
elapsed 73%CPU (0avgtext+0avgdata 42
08
0maxresident)k
0
inputs+1
51648
outputs (0major+84
08595
minor)pagefaults 0swaps
* Quick time (-j 4):
91.89
user 1
8.09
system
0:57.95
elapsed 1
89
%CPU (0avgtext+0avgdata 42
124
maxresident)k
8
0inputs+1
39528
outputs (0major+8
011124
minor)pagefaults 0swaps
86.00
user 1
6.60
system
1:10.17
elapsed 1
46
%CPU (0avgtext+0avgdata 42
096
maxresident)k
0inputs+1
46640
outputs (0major+8
181699
minor)pagefaults 0swaps
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment