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
db127044
Commit
db127044
authored
Mar 15, 2021
by
erwan
Browse files
Update: refuse programs that iterates over array of structures using polymorphic nodes.
parent
a5758195
Pipeline
#62322
passed with stages
in 5 minutes and 8 seconds
Changes
2
Pipelines
2
Hide whitespace changes
Inline
Side-by-side
lib/soc2c.ml
View file @
db127044
(* Time-stamp: <modified the 1
3
/03/202
0
(at
11:44
) by Erwan Jahier> *)
(* Time-stamp: <modified the 1
5
/03/202
1
(at
23:07
) by Erwan Jahier> *)
(* let put (os: out_channel) (fmt:('a, unit, string, unit) format4) : 'a = *)
...
...
@@ -107,59 +107,76 @@ let (gao2c : Soc.tbl -> 'a soc_pp -> Soc.gao -> unit) =
let
(
step2c
:
Soc
.
tbl
->
'
a
soc_pp
->
Soc
.
step_method
->
unit
)
=
fun
stbl
sp
sm
->
if
inlined_soc
sp
.
soc
.
key
then
()
(* don't generate code if inlined *)
else
(* let sname = Soc2cDep.step_name sp.soc.key sm.name in *)
let
sname
=
Soc2cDep
.
step_name
sp
.
soc
.
key
sm
.
name
in
if
sm
.
impl
<>
Extern
then
(
let
decl
,
def
,
ctype
=
Soc2cDep
.
get_step_prototype
sm
sp
.
soc
in
sp
.
hput
(
Printf
.
sprintf
"%s
\n
"
decl
);
sp
.
cput
(
Printf
.
sprintf
"%s"
def
);
(
match
sm
.
impl
with
|
Extern
->
()
|
Predef
->
(
match
sp
.
soc
.
key
with
|
(
"Lustre::eq"
,
(
Array
_
)
::_,_
)
->
let
str
=
Printf
.
sprintf
" *out = memcmp((const void *) i1, (const void *) i2, %s)==0;
\n
"
ctype
in
sp
.
cput
str
|
(
"Lustre::eq"
,
(
Struct
_
)
::_,_
)
->
let
str
=
Printf
.
sprintf
" *out = memcmp((const void *) &i1, (const void *) &i2, %s)==0;
\n
"
ctype
in
sp
.
cput
str
|
(
"Lustre::neq"
,
(
Array
_
)
::_,_
)
->
let
str
=
Printf
.
sprintf
" *out = !memcmp((const void *) i1, (const void *) i2, %s)==0;
\n
"
ctype
in
sp
.
cput
str
|
(
"Lustre::neq"
,
(
Struct
_
)
::_,_
)
->
let
str
=
Printf
.
sprintf
" *out = !memcmp((const void *) &i1, (const void *) &i2, %s)==0;
\n
"
ctype
in
sp
.
cput
str
|
n
->
sp
.
cput
(
Soc2cDep
.
get_predef_op
n
)
)
|
Gaol
(
vl
,
gaol
)
->
(
if
Lv6MainArgs
.
global_opt
.
Lv6MainArgs
.
gen_wcet
then
List
.
iter
(
fun
v
->
sp
.
cput
(
Soc2cUtil
.
string_of_flow_decl_w7annot
gaol
v
))
vl
else
List
.
iter
(
fun
v
->
sp
.
cput
(
Soc2cUtil
.
string_of_flow_decl
v
))
vl
;
sp
.
cput
"
\n
"
;
List
.
iter
(
gao2c
stbl
sp
)
gaol
)
|
Iterator
(
it
,
it_soc_key
,
s
)
->
let
it_soc
=
SocUtils
.
find
sm
.
lxm
it_soc_key
stbl
in
sp
.
cput
(
Soc2cDep
.
get_iterator
sp
.
soc
it
it_soc
s
)
|
Boolred
(
i
,
j
,
k
)
->
sp
.
cput
(
Soc2cDep
.
get_boolred
sp
.
soc
i
j
k
)
|
Condact
(
k
,
el
)
->
sp
.
cput
(
Soc2cDep
.
get_condact
sp
.
soc
(
SocUtils
.
find
sm
.
lxm
k
stbl
)
el
)
);
sp
.
cput
(
sprintf
"
\n
} // End of %s
\n\n
"
sname
)
)
if
inlined_soc
sp
.
soc
.
key
then
()
(* don't generate code if inlined *)
else
(* let sname = Soc2cDep.step_name sp.soc.key sm.name in *)
let
sname
=
Soc2cDep
.
step_name
sp
.
soc
.
key
sm
.
name
in
if
sm
.
impl
<>
Extern
then
(
let
decl
,
def
,
ctype
=
Soc2cDep
.
get_step_prototype
sm
sp
.
soc
in
sp
.
hput
(
Printf
.
sprintf
"%s
\n
"
decl
);
sp
.
cput
(
Printf
.
sprintf
"%s"
def
);
(
match
sm
.
impl
with
|
Extern
->
()
|
Predef
->
(
match
sp
.
soc
.
key
with
|
(
"Lustre::eq"
,
(
Array
_
)
::_,_
)
->
let
str
=
Printf
.
sprintf
" *out = memcmp((const void *) i1, (const void *) i2, %s)==0;
\n
"
ctype
in
sp
.
cput
str
|
(
"Lustre::eq"
,
(
Struct
_
)
::_,_
)
->
let
str
=
Printf
.
sprintf
" *out = memcmp((const void *) &i1, (const void *) &i2, %s)==0;
\n
"
ctype
in
sp
.
cput
str
|
(
"Lustre::neq"
,
(
Array
_
)
::_,_
)
->
let
str
=
Printf
.
sprintf
" *out = !memcmp((const void *) i1, (const void *) i2, %s)==0;
\n
"
ctype
in
sp
.
cput
str
|
(
"Lustre::neq"
,
(
Struct
_
)
::_,_
)
->
let
str
=
Printf
.
sprintf
" *out = !memcmp((const void *) &i1, (const void *) &i2, %s)==0;
\n
"
ctype
in
sp
.
cput
str
|
n
->
sp
.
cput
(
Soc2cDep
.
get_predef_op
n
)
)
|
Gaol
(
vl
,
gaol
)
->
(
if
Lv6MainArgs
.
global_opt
.
Lv6MainArgs
.
gen_wcet
then
List
.
iter
(
fun
v
->
sp
.
cput
(
Soc2cUtil
.
string_of_flow_decl_w7annot
gaol
v
))
vl
else
List
.
iter
(
fun
v
->
sp
.
cput
(
Soc2cUtil
.
string_of_flow_decl
v
))
vl
;
sp
.
cput
"
\n
"
;
List
.
iter
(
gao2c
stbl
sp
)
gaol
)
|
Iterator
(
it
,
it_soc_key
,
s
)
->
(
(* iterating on Lustre::eq or neq currently does not work
Refuse such programs explicitly *)
match
sp
.
soc
.
key
with
|
_
,
(
Array
(
Array
_
,_
))
::_,
_
|
_
,
(
Array
(
Struct
_
,_
))
::_,
_
->
(
match
it_soc_key
with
|
_
,
(
Alpha
_
::_
)
,_
->
let
msg
=
Printf
.
sprintf
"%s
\n
Iterating on polymorphic nodes over arrays of structures %s"
(
Lxm
.
details
sm
.
lxm
)
"is currently unsupported"
in
failwith
msg
|
_
->
()
)
|
_
,_,_
->
()
);
let
it_soc
=
SocUtils
.
find
sm
.
lxm
it_soc_key
stbl
in
sp
.
cput
(
Soc2cDep
.
get_iterator
sp
.
soc
it
it_soc
s
)
|
Boolred
(
i
,
j
,
k
)
->
sp
.
cput
(
Soc2cDep
.
get_boolred
sp
.
soc
i
j
k
)
|
Condact
(
k
,
el
)
->
sp
.
cput
(
Soc2cDep
.
get_condact
sp
.
soc
(
SocUtils
.
find
sm
.
lxm
k
stbl
)
el
)
);
sp
.
cput
(
sprintf
"
\n
} // End of %s
\n\n
"
sname
)
)
let
(
gen_instance_init_call
:
'
a
soc_pp
->
Soc
.
key
*
int
->
unit
)
=
fun
sp
(
key
,
i
)
->
let
ctx_name
=
get_ctx_name
key
in
...
...
test/lus2lic.sum
View file @
db127044
==> lus2lic0.sum <==
Test run by jahier on
Thu
Mar 1
1 17:05:4
3
Test run by jahier on
Mon
Mar 1
5 23:09:3
3
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
Thu
Mar 1
1 17:05:43
Test run by jahier on
Mon
Mar 1
5 23:09:34
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
Thu
Mar 1
1 17:06:11
Test run by jahier on
Mon
Mar 1
5 23:10:02
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
Thu
Mar 1
1 17:06:47
Test run by jahier on
Mon
Mar 1
5 23:10:38
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
Thu
Mar 1
1 17:07:30
Test run by jahier on
Mon
Mar 1
5 23:11: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 3
6527
{}
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus 3
4133
{}
=== lus2lic1 Summary ===
...
...
@@ -1787,14 +1787,14 @@ PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus 36527
# of unexpected failures 6
===============================
# Total number of failures: 10
lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in
0
seconds
lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 2
7
seconds
lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in
1
seconds
lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 2
8
seconds
lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 36 seconds
lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 4
3
seconds
lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 2
5
seconds
lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 4
5
seconds
lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 2
6
seconds
* Ref time:
8
0.22
user 1
7.98
system 2:1
2.40
elapsed 7
4
%CPU (0avgtext+0avgdata 423
80
maxresident)k
0inputs+15
1696
outputs (0major+84
122
42minor)pagefaults 0swaps
8
5.81
user 1
8.64
system 2:1
6.24
elapsed 7
6
%CPU (0avgtext+0avgdata 423
76
maxresident)k
0inputs+15
0784
outputs (0major+84
08
42
5
minor)pagefaults 0swaps
* Quick time (-j 4):
96
.1
7
user 1
9.5
5system 1:2
6
.5
4
elapsed 1
33
%CPU (0avgtext+0avgdata 42
36
8maxresident)k
6
672
inputs+14
9632
outputs (
12
major+831
7848
minor)pagefaults 0swaps
83
.1
6
user 1
6.2
5system 1:2
2
.5
7
elapsed 1
20
%CPU (0avgtext+0avgdata 42
42
8maxresident)k
6
000
inputs+14
8480
outputs (
8
major+831
0354
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