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
d82601e2
Commit
d82601e2
authored
Jul 05, 2021
by
erwan
Browse files
New: add a -dro option
parent
3300825b
Pipeline
#70567
passed with stages
in 4 minutes and 24 seconds
Changes
5
Pipelines
2
Hide whitespace changes
Inline
Side-by-side
lib/lv6MainArgs.ml
View file @
d82601e2
(* Time-stamp: <modified the 0
7
/0
5
/2021 (at 10:
11
) by Erwan Jahier> *)
(* Time-stamp: <modified the 0
2
/0
7
/2021 (at 10:
48
) by Erwan Jahier> *)
(*
Le manager d'argument adapt de celui de lutin, plus joli
N.B. solution un peu batarde : les options sont stockes, comme avant, dans Global,
...
...
@@ -66,6 +66,7 @@ type global_opt = {
mutable
soc2c_one_file
:
bool
;
mutable
soc2c_inline_loops
:
bool
;
mutable
soc2c_global_ctx
:
bool
;
mutable
soc2c_dro
:
bool
;
mutable
gen_wcet
:
bool
;
mutable
io_transmit_mode
:
io_transmit_mode
;
mutable
schedul_mode
:
schedul_mode
;
...
...
@@ -90,6 +91,7 @@ let (global_opt:global_opt) =
soc2c_one_file
=
true
;
soc2c_inline_loops
=
false
;
soc2c_global_ctx
=
false
;
soc2c_dro
=
false
;
gen_wcet
=
false
;
io_transmit_mode
=
Stack
;
schedul_mode
=
Simple
;
...
...
@@ -426,6 +428,12 @@ let mkoptab (opt:t) : unit = (
(
Arg
.
Unit
(
fun
()
->
global_opt
.
soc2c_global_ctx
<-
true
;
set_c_options
opt
))
[
"Node context allocated as global variable (no
\"
new_ctx
\"
method)"
]
;
mkopt
opt
~
doc_level
:
Advanced
[
"-dro"
;
"--2c-dro"
]
(
Arg
.
Unit
(
fun
()
->
global_opt
.
soc2c_dro
<-
true
;
set_c_options
opt
;
global_opt
.
io_transmit_mode
<-
Heap
))
[
"Generate a .dro file (for luciole)"
]
;
mkopt
opt
~
doc_level
:
Advanced
[
"-lic"
;
"--gen-lic"
]
(
Arg
.
Unit
(
fun
()
->
opt
.
gen_lic
<-
true
))
...
...
lib/lv6MainArgs.mli
View file @
d82601e2
(* Time-stamp: <modified the 2
9
/0
8
/201
9
(at 1
4:37
) by Erwan Jahier> *)
(* Time-stamp: <modified the
0
2/0
7
/20
2
1 (at 1
0:11
) by Erwan Jahier> *)
type
enum_mode
=
AsInt
(* translate enums into int (for rif-friendlyness *)
...
...
@@ -71,6 +71,7 @@ type global_opt = {
mutable
soc2c_one_file
:
bool
;
mutable
soc2c_inline_loops
:
bool
;
mutable
soc2c_global_ctx
:
bool
;
mutable
soc2c_dro
:
bool
;
mutable
gen_wcet
:
bool
;
mutable
io_transmit_mode
:
io_transmit_mode
;
mutable
schedul_mode
:
schedul_mode
;
...
...
lib/soc2c.ml
View file @
d82601e2
(* Time-stamp: <modified the
1
5/0
3
/2021 (at
23:0
7) by Erwan Jahier> *)
(* Time-stamp: <modified the
0
5/0
7
/2021 (at
09:1
7) by Erwan Jahier> *)
(* let put (os: out_channel) (fmt:('a, unit, string, unit) format4) : 'a = *)
...
...
@@ -191,7 +191,21 @@ let (gen_instance_init_call : 'a soc_pp -> Soc.key * int -> unit) =
)
module
KeySet
=
Set
.
Make
(
struct
type
t
=
Soc
.
key
let
compare
=
compare
end
)
(****************************************************************************)
let
(
type_to_format_string
:
Data
.
t
->
string
)
=
function
|
String
->
"%s"
|
Bool
->
"%d"
|
Int
->
"%d"
|
Real
->
"%f"
|
Extern
_s
->
"%s"
|
Enum
(
_s
,
_sl
)
->
"%d"
|
Struct
(
_sid
,_
)
->
"%s"
|
Array
(
_ty
,
_sz
)
->
"%s"
|
Alpha
_nb
->
assert
false
|
Alias
_
->
assert
false
let
(
get_used_soc
:
Soc
.
t
->
KeySet
.
t
)
=
fun
soc
->
(* dig into the soc for the list of socs it uses *)
let
rec
get_soc_of_gao
acc
=
function
...
...
@@ -225,7 +239,7 @@ let (soc2c : int -> out_channel -> out_channel -> Soc.tbl -> Soc.key ->
if
pass
=
1
then
(
(* Only for ctx of memoryless nodes + main node *)
if
SocUtils
.
ctx_is_global
soc
then
Printf
.
kprintf
(
fun
t
->
output_string
cfile
t
)
"%s %s;
\n
"
ctx_name_type
ctx_name
;
Printf
.
kprintf
(
fun
t
->
output_string
cfile
t
)
"
static
%s %s;
\n
"
ctx_name_type
ctx_name
;
cfiles_acc
)
else
(
let
base
=
string_of_soc_key
soc
.
key
in
...
...
@@ -313,7 +327,6 @@ let (soc2c : int -> out_channel -> out_channel -> Soc.tbl -> Soc.key ->
);
cfmt
"// Step function(s) for %s
\n
"
ctx_name
;
List
.
iter
(
step2c
stbl
sp
)
soc
.
step
;
()
;
if
not
(
one_file
()
||
msoc_key
=
soc
.
key
)
then
(
hfmt
"#endif /* _%s_H_FILE */"
base
;
close_out
hfile
;
...
...
@@ -325,20 +338,6 @@ let (soc2c : int -> out_channel -> out_channel -> Soc.tbl -> Soc.key ->
cfiles_acc
)
(****************************************************************************)
let
(
type_to_format_string
:
Data
.
t
->
string
)
=
function
|
String
->
"%s"
|
Bool
->
"%d"
|
Int
->
"%d"
|
Real
->
"%f"
|
Extern
_s
->
"%s"
|
Enum
(
_s
,
_sl
)
->
"%d"
|
Struct
(
_sid
,_
)
->
"%s"
|
Array
(
_ty
,
_sz
)
->
"%s"
|
Alpha
_nb
->
assert
false
|
Alias
_
->
assert
false
(****************************************************************************)
...
...
@@ -969,7 +968,10 @@ let (f : Lv6MainArgs.t -> Soc.key -> Soc.tbl -> LicPrg.t -> unit) =
let
loopfile
=
base
^
"_loop.c"
in
let
occ
=
open_out
cfile
in
let
och
=
open_out
hfile
in
let
ocl
=
open_out
loopfile
in
let
ocl
=
if
Lv6MainArgs
.
global_opt
.
Lv6MainArgs
.
soc2c_dro
then
stdout
else
open_out
loopfile
in
let
types_h_oc
=
open_out
"lustre_types.h"
in
let
consts_h_oc
=
open_out
"lustre_consts.h"
in
let
consts_c_oc
=
open_out
"lustre_consts.c"
in
...
...
@@ -1012,9 +1014,11 @@ typedef float _float;
try
let
putc
s
=
output_string
occ
s
in
let
cfmt
fmt
=
Printf
.
kprintf
(
fun
t
->
output_string
occ
t
)
fmt
in
let
puth
s
=
output_string
och
s
in
Lv6util
.
entete
occ
"/*"
"*/"
;
Lv6util
.
entete
och
"/*"
"*/"
;
if
Lv6MainArgs
.
global_opt
.
Lv6MainArgs
.
soc2c_dro
then
()
else
if
Lv6MainArgs
.
global_opt
.
Lv6MainArgs
.
gen_wcet
then
(
gen_loop_file4ogensim
main_soc
base
ocl
stbl
;
gen_main_wcet_file
main_soc
base
stbl
...
...
@@ -1039,15 +1043,102 @@ typedef float _float;
putc
(
Soc2cExtern
.
const_declaration
licprg
);
let
cfiles_acc
=
if
io_transmit_mode
()
=
Lv6MainArgs
.
Heap
then
(
puth
"/////////////////////////////////////////////////
\n
"
;
puth
"//// Static allocation of memoryless soc ctx
\n
"
;
if
socs
=
[]
then
[]
else
(
putc
"/////////////////////////////////////////////////
\n
"
;
putc
"//// Static allocation of memoryless soc ctx
\n
"
;
let
cfiles_acc
=
List
.
fold_left
(
soc2c
1
och
occ
stbl
msoc
)
cfiles_acc
socs
in
put
h
"/////////////////////////////////////////////////
\n
"
;
put
c
"/////////////////////////////////////////////////
\n
"
;
cfiles_acc
);
)
else
cfiles_acc
in
putc
"//// Defining step functions
\n
"
;
let
cfiles_acc
=
List
.
fold_left
(
soc2c
2
och
occ
stbl
msoc
)
cfiles_acc
socs
in
let
inputs
,
outputs
=
main_soc
.
profile
in
let
inputs_exp
=
SocVar
.
expand_profile
true
true
inputs
in
let
outputs_exp
=
SocVar
.
expand_profile
true
true
outputs
in
let
inputs_exp2
=
SocVar
.
expand_profile
true
false
inputs
in
let
outputs_exp2
=
SocVar
.
expand_profile
true
false
outputs
in
let
name
=
get_base_name
main_soc
.
key
in
if
Lv6MainArgs
.
global_opt
.
Lv6MainArgs
.
soc2c_dro
then
(
cfmt
"///////// dro stuff
/* droconf.h begins */
/*
Struct necessary for building a DRO archive
(Dynamically linkable Reactive Object)
Such an archive can be loaded by simec/luciole
*/
#define DROVERSION
\"
1.1
\"
#define xstr(s) str(s) /* converts macro to string */
#define str(s) #s
/* should be of type type dro_desc_t */
#define DRO_DESC_NAME dro_desc
struct dro_var_t {
const char* ident;
const char* type;
void* valptr;
};
struct dro_desc_t {
const char* version;
const char* name;
int nbins;
struct dro_var_t* intab;
int nbouts;
struct dro_var_t* outab;
int ( *step )();
void ( *reset )();
void ( *init )();
};
/* droconf.h ends */
"
;
cfmt
"static %s_ctx_type %s_ctx;
\n
"
name
name
;
cfmt
"//dro requires : int ( *step )();
static int ze_step(){
%s_step(& %s_ctx);
return 0;
}
//dro requires : void ( *reset )();
static void ze_reset(){
%s
}
#define DRO_REAL(X) ((sizeof(_real)==4)?
\"
float
\"
: (sizeof(_real)==8)?
\"
double
\"
:
\"
unknown
\"
)
#define DRO_INT(X)
\"
int
\"
#define DRO_BOOL(X)
\"
bool
\"
#define DRO_EXTERN(X)
\"
X
\"
struct dro_var_t dro_intab[] = {
"
name
name
(
if
SocUtils
.
is_memory_less
main_soc
then
""
else
Printf
.
sprintf
"%s_ctx_reset(& %s_ctx);"
name
name
);
let
line2str
(
id
,
t
)
(
id2
,
_t
)
=
let
t
=
(
type_to_string_rif
t
)
in
let
cap_t
=
String
.
uppercase_ascii
t
in
Printf
.
sprintf
" {
\"
%s
\"
, DRO_%s(%s), (void*)&%s_ctx.%s}"
id2
cap_t
t
name
id
in
putc
(
String
.
concat
",
\n
"
(
List
.
map2
line2str
inputs_exp
inputs_exp2
));
cfmt
"
\n
};
/* dro: output pointers table */
struct dro_var_t dro_outab[] = {
"
;
putc
(
String
.
concat
",
\n
"
(
List
.
map2
line2str
outputs_exp
outputs_exp2
));
cfmt
"
\n
};
/* dro: dynamic linking infos table */
struct dro_desc_t DRO_DESC_NAME = {
DROVERSION, /* expected dro version */
\"
%s
\"
, /* appli name */
%d, dro_intab, /* nb inputs + table */
%d, dro_outab, /* nb outputs + table */
ze_step, /* step proc */
ze_reset, /* reset proc */
ze_reset /* init proc = reset proc */
};
"
name
(
List
.
length
inputs_exp
)
(
List
.
length
outputs_exp
);
);
(* end dro stuff *)
puth
"/////////////////////////////////////////////////
\n
"
;
if
assign_ext_types_list
<>
[]
then
(
...
...
@@ -1065,7 +1156,8 @@ typedef float _float;
flush
ocl
;
close_out
ocl
;
flush
consts_h_oc
;
close_out
consts_h_oc
;
flush
consts_c_oc
;
close_out
consts_c_oc
;
Printf
.
eprintf
"W: %s has been generated.
\n
"
loopfile
;
if
not
Lv6MainArgs
.
global_opt
.
Lv6MainArgs
.
soc2c_dro
then
Printf
.
eprintf
"W: %s has been generated.
\n
"
loopfile
;
Printf
.
eprintf
"W: %s has been generated.
\n
"
hfile
;
Printf
.
eprintf
"W: %s has been generated.
\n
"
cfile
;
flush
stderr
;
...
...
@@ -1078,7 +1170,7 @@ typedef float _float;
in
let
cflags
=
try
Sys
.
getenv
"CFLAGS"
with
Not_found
->
""
in
let
ocsh
=
open_out
(
node
^
".sh"
)
in
let
main_file
,
ogensim_main_file
,
gcc
=
let
main_file
,
ogensim_main_file
,
gcc
=
if
Lv6MainArgs
.
global_opt
.
Lv6MainArgs
.
gen_wcet
then
base
^
"_main.c"
,
base
^
"_loop.c"
,
"$gcc --specs=linux.specs -g"
else
...
...
@@ -1088,6 +1180,10 @@ typedef float _float;
let
cfiles_acc
=
if
needs_cfile
then
ext_cfile
::
cfiles_acc
else
cfiles_acc
in
let
cfiles
=
String
.
concat
" "
cfiles_acc
in
let
gcc
,
gcc_ogensim
=
if
Lv6MainArgs
.
global_opt
.
Lv6MainArgs
.
soc2c_dro
then
(
Printf
.
sprintf
"%s -shared -o %s.dro
\\\n\t
%s %s"
gcc
node
cfiles
cflags
,
"dead string"
)
else
Printf
.
sprintf
"%s -o %s
\\\n\t
%s %s %s"
gcc
execfile
cfiles
cflags
main_file
,
Printf
.
sprintf
"%s -o %s
\\\n\t
%s %s %s"
...
...
test/should_work/dadic_x5_c.lus
View file @
d82601e2
-- nonreg: dadic.lus
package
Toto2
uses
D
adic
;
package
dadic_x5_c
uses
d
adic
;
provides
node
x5
(
x
:
bool
)
returns
(
y
:
bool
);
node
dadic_x5_c
(
x
:
bool
)
returns
(
y
:
bool
);
body
node
x5
=
Mult
<<
5
>>
;
node
dadic_x5_c
=
Mult
<<
5
>>
;
end
utils/test_lus2lic_no_node
View file @
d82601e2
...
...
@@ -39,7 +39,7 @@ if
then
echo
"lus2lic -ec done"
else
echo
"
E
rror"
echo
"
lus2lic
$lustre_file
-n
$node
-ec -o
$ec
: returned an e
rror"
exit
2
fi
...
...
@@ -59,16 +59,16 @@ export PATH=/usr/local/tools/lustre/v4/bin/:$PATH
if
# -rp "sut:v4:$lv4:$lv4_node" \
PRECISION
=
4
lurette
-l
10
\
-sut
"ecexe-rif
$ec
$lv4_node
-rif"
\
-env
"lutin
$env
-n
$env_node
-p
$PRECISION
"
\
-oracle
"./lus2lic
$_oracle
-n
$oracle
$OPT
"
PRECISION
=
4
lurette
-l
10
\
-sut
"ecexe-rif
$ec
$lv4_node
-rif"
\
-env
"lutin
$env
-n
$env_node
-p
$PRECISION
"
\
-oracle
"./lus2lic
$_oracle
-n
$oracle
$OPT
"
# lurettetop_exe -p $PRECISION -rp "sut:ec:$ec:$lv4_node" -rp "env:lutin:$env:-p:$PRECISION" -rp "oracle:v6:$_oracle:$oracle:$OPT" -go -l 10 -ns2c --stop-on-oracle-error;
then
echo
"lurettetop ok"
echo
"lurettetop ok"
else
echo
"error"
echo
"
lurette returned an
error"
exit
2
fi
exit
0
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