Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
L
lutin
Project overview
Project overview
Details
Activity
Releases
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Issues
1
Issues
1
List
Boards
Labels
Service Desk
Milestones
Merge Requests
0
Merge Requests
0
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Operations
Operations
Incidents
Environments
Packages & Registries
Packages & Registries
Container Registry
Analytics
Analytics
CI / CD
Repository
Value Stream
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
verimag
synchrone
lutin
Commits
6e017db3
Commit
6e017db3
authored
Sep 05, 2014
by
Erwan Jahier
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Update the lus2lic plugin + more Makefile fixes.
parent
33119124
Changes
52
Hide whitespace changes
Inline
Side-by-side
Showing
52 changed files
with
803 additions
and
567 deletions
+803
-567
Makefile.version
Makefile.version
+2
-2
examples/lutin/lurette-socket/Makefile
examples/lutin/lurette-socket/Makefile
+3
-0
install/configure
install/configure
+2
-1
install/configure.in
install/configure.in
+2
-1
source/Gnuplot-rif/Makefile
source/Gnuplot-rif/Makefile
+2
-2
source/Lurettetop/ltopArg.ml
source/Lurettetop/ltopArg.ml
+2
-2
source/Lurettetop/runDirect.ml
source/Lurettetop/runDirect.ml
+1
-1
source/Lutin/Makefile.lutin
source/Lutin/Makefile.lutin
+1
-1
source/Makefile.release
source/Makefile.release
+7
-11
source/common/command_line.ml
source/common/command_line.ml
+2
-10
source/common/lurette_ocaml.ml
source/common/lurette_ocaml.ml
+1
-1
source/common/lustreRun.ml
source/common/lustreRun.ml
+2
-2
source/common/myArg.ml
source/common/myArg.ml
+4
-4
source/common/myGenlex.ml
source/common/myGenlex.ml
+1
-16
source/common/util.ml
source/common/util.ml
+31
-0
source/lus2lic/actionsDeps.ml
source/lus2lic/actionsDeps.ml
+4
-4
source/lus2lic/actionsDeps.mli
source/lus2lic/actionsDeps.mli
+2
-2
source/lus2lic/ast2lic.ml
source/lus2lic/ast2lic.ml
+31
-22
source/lus2lic/astCore.ml
source/lus2lic/astCore.ml
+2
-1
source/lus2lic/astTabSymbol.ml
source/lus2lic/astTabSymbol.ml
+2
-3
source/lus2lic/compile.ml
source/lus2lic/compile.ml
+3
-3
source/lus2lic/evalClock.ml
source/lus2lic/evalClock.ml
+91
-27
source/lus2lic/evalClock.mli
source/lus2lic/evalClock.mli
+6
-5
source/lus2lic/evalType.ml
source/lus2lic/evalType.ml
+8
-2
source/lus2lic/l2lCheckLoops.ml
source/lus2lic/l2lCheckLoops.ml
+2
-2
source/lus2lic/l2lExpandArrays.ml
source/lus2lic/l2lExpandArrays.ml
+41
-35
source/lus2lic/l2lExpandArrays.mli
source/lus2lic/l2lExpandArrays.mli
+7
-2
source/lus2lic/l2lExpandMetaOp.ml
source/lus2lic/l2lExpandMetaOp.ml
+75
-27
source/lus2lic/l2lExpandNodes.ml
source/lus2lic/l2lExpandNodes.ml
+2
-2
source/lus2lic/l2lSplit.ml
source/lus2lic/l2lSplit.ml
+26
-14
source/lus2lic/l2lSplit.mli
source/lus2lic/l2lSplit.mli
+2
-2
source/lus2lic/lic.ml
source/lus2lic/lic.ml
+73
-58
source/lus2lic/lic2soc.ml
source/lus2lic/lic2soc.ml
+75
-22
source/lus2lic/licDump.ml
source/lus2lic/licDump.ml
+4
-2
source/lus2lic/licEvalClock.ml
source/lus2lic/licEvalClock.ml
+2
-1
source/lus2lic/licPrg.ml
source/lus2lic/licPrg.ml
+35
-28
source/lus2lic/licTab.ml
source/lus2lic/licTab.ml
+33
-30
source/lus2lic/lus2licRun.ml
source/lus2lic/lus2licRun.ml
+1
-5
source/lus2lic/lv6MainArgs.ml
source/lus2lic/lv6MainArgs.ml
+10
-1
source/lus2lic/lv6MainArgs.mli
source/lus2lic/lv6MainArgs.mli
+1
-0
source/lus2lic/lv6util.ml
source/lus2lic/lv6util.ml
+2
-0
source/lus2lic/lv6version.ml
source/lus2lic/lv6version.ml
+2
-2
source/lus2lic/soc.ml
source/lus2lic/soc.ml
+3
-4
source/lus2lic/socExec.ml
source/lus2lic/socExec.ml
+96
-106
source/lus2lic/socExecEvalPredef.ml
source/lus2lic/socExecEvalPredef.ml
+3
-17
source/lus2lic/socExecValue.ml
source/lus2lic/socExecValue.ml
+12
-6
source/lus2lic/socPredef.ml
source/lus2lic/socPredef.ml
+44
-45
source/lus2lic/socUtils.ml
source/lus2lic/socUtils.ml
+3
-1
source/lus2lic/unifyClock.ml
source/lus2lic/unifyClock.ml
+28
-25
source/lus2lic/unifyClock.mli
source/lus2lic/unifyClock.mli
+3
-3
source/lus2lic/unifyType.ml
source/lus2lic/unifyType.ml
+5
-3
source/misc/Makefile.check_rif
source/misc/Makefile.check_rif
+1
-1
No files found.
Makefile.version
View file @
6e017db3
# well, finally, set it manually...
VERSION
:=
1.5
4
VERSION
:=
1.5
5
#
# When incrementing that version number, please don't forget to
# fill-in the RELEASE-NOTES file (using the git history).
...
...
@@ -34,4 +34,4 @@ gen_version:
echo
"
\\\n
ewcommand{
\\\v
ersiondate}{
`
date
+%d-%m-%y
`
}"
>>
doc/version.tex
;
\
[
-d
doc/lutin-man/objs
]
||
mkdir
doc/lutin-man/objs
;
\
cp
doc/version.tex doc/lutin-man/objs/
;
\
cp
doc/version.tex doc/lutin-man/
\ No newline at end of file
cp
doc/version.tex doc/lutin-man/
examples/lutin/lurette-socket/Makefile
View file @
6e017db3
...
...
@@ -30,6 +30,9 @@ test: simple_sut$(EXE)
PORT
=
2015
PORT2
=
2016
# an alternative using the call-via-socket script (provided in the bin dir of the distrib)
# the following 3 rules needs to be launched in parallel
lu
:
../../../bin/lurettetop
-go
--output
test.rif0
-l
9
\
-rp
"sut:socket:127.0.0.1:
$(PORT)
:"
\
...
...
install/configure
View file @
6e017db3
...
...
@@ -1864,7 +1864,7 @@ ac_compiler_gnu=$ac_cv_c_compiler_gnu
unset
LANG
unset
LC_ALL LC_CTYPE LC_COLLATE LC_MESSAGES LC_MONETARY LC_NUMERIC LC_TIME
#
unset LC_ALL LC_CTYPE LC_COLLATE LC_MESSAGES LC_MONETARY LC_NUMERIC LC_TIME
...
...
@@ -1873,6 +1873,7 @@ unset LC_ALL LC_CTYPE LC_COLLATE LC_MESSAGES LC_MONETARY LC_NUMERIC LC_TIME
# Determine the system type
case
`
./config.guess
`
in
x86_64-
*
-linux-
*
)
HOST_TYPE
=
linux
;;
i
*
86-pc-linux-
*
)
HOST_TYPE
=
linux
;;
sparc-sun-solaris2.
*
)
HOST_TYPE
=
sparc-sun
;;
i
*
86-
*
-cygwin
)
HOST_TYPE
=
win32
;;
...
...
install/configure.in
View file @
6e017db3
...
...
@@ -5,7 +5,7 @@
AC_INIT(Makefile.lurette.in)
unset LANG
unset LC_ALL LC_CTYPE LC_COLLATE LC_MESSAGES LC_MONETARY LC_NUMERIC LC_TIME
#
unset LC_ALL LC_CTYPE LC_COLLATE LC_MESSAGES LC_MONETARY LC_NUMERIC LC_TIME
...
...
@@ -14,6 +14,7 @@ unset LC_ALL LC_CTYPE LC_COLLATE LC_MESSAGES LC_MONETARY LC_NUMERIC LC_TIME
# Determine the system type
case `./config.guess` in
x86_64-*-linux-*) HOST_TYPE=linux ;;
i*86-pc-linux-*) HOST_TYPE=linux ;;
sparc-sun-solaris2.*) HOST_TYPE=sparc-sun ;;
i*86-*-cygwin) HOST_TYPE=win32 ;;
...
...
source/Gnuplot-rif/Makefile
View file @
6e017db3
...
...
@@ -6,10 +6,10 @@ OCAMLNCFLAGS = -inline 10
USE_CAMLP4
=
yes
LIBS
=
str unix
LIBS
=
str unix
nums
SOURCES
=
$(OBJDIR)
/myGenlex.ml
$(OBJDIR)
/gnuplotRif.ml
$(OBJDIR)
/gnuplotRifMain.ml
SOURCES
=
$(OBJDIR)
/
version.ml
$(OBJDIR)
/util.ml
$(OBJDIR)
/
myGenlex.ml
$(OBJDIR)
/gnuplotRif.ml
$(OBJDIR)
/gnuplotRifMain.ml
ln
:
$(OBJDIR) $(SOURCES)
...
...
source/Lurettetop/ltopArg.ml
View file @
6e017db3
...
...
@@ -402,8 +402,8 @@ let (parse_rp_string : string -> unit) =
"lutin:toto.luc:-main toto:"
*)
|
[
"v6"
;
prog
;
node
]
->
let
args
=
(
"lus2lic"
::
prog
::
"-node"
::
node
::
[]
)
in
|
"v6"
::
prog
::
node
::
opts
->
let
args
=
(
"lus2lic"
::
prog
::
"-node"
::
node
::
opts
)
in
LustreV6
(
Array
.
of_list
args
)
|
[
"ec_exe"
;
prog
]
->
LustreEcExe
(
prog
)
|
[
"ec"
;
prog
]
->
LustreEc
(
prog
)
...
...
source/Lurettetop/runDirect.ml
View file @
6e017db3
...
...
@@ -498,7 +498,7 @@ let (start : unit -> Event.t) =
|
Failure
str
->
print_string
(
"Failure occured in lurette: "
^
str
);
flush
stdout
;
raise
(
Event
.
End
2
)
raise
(
Event
.
End
2
)
|
Event
.
End
i
->
raise
(
Event
.
End
(
10
*
i
))
|
e
->
print_string
(
Printexc
.
to_string
e
);
...
...
source/Lutin/Makefile.lutin
View file @
6e017db3
...
...
@@ -9,7 +9,7 @@ include $(LURETTE_PATH)/source/Makefile.ln
######################################################################
ifneq
($(HOSTTYPE),Darwin-x86_64)
STATIC
=
yes
#
STATIC=yes
endif
OCAMLFLAGS
+=
-I
$(OBJDIR)
-I
$(OCAMLLIB)
-I
$(PREFIX)
/
$(HOSTTYPE)
/lib
...
...
source/Makefile.release
View file @
6e017db3
...
...
@@ -84,6 +84,7 @@ $(LURETTE_RELEASE_NAME).tgz: strip
mkdir
/tmp/
$(LURETTE_RELEASE_NAME)
/examples
mkdir
/tmp/
$(LURETTE_RELEASE_NAME)
/examples/lucky
mkdir
/tmp/
$(LURETTE_RELEASE_NAME)
/examples/lutin
mkdir
/tmp/
$(LURETTE_RELEASE_NAME)
/examples/lutin/lurette-socket
mkdir
/tmp/
$(LURETTE_RELEASE_NAME)
/examples/lutin/xlurette
mkdir
/tmp/
$(LURETTE_RELEASE_NAME)
/examples/lutin/external_code
mkdir
/tmp/
$(LURETTE_RELEASE_NAME)
/examples/xlurette
...
...
@@ -464,16 +465,11 @@ xxx:
# Faire un make all-rel avant ...
verimag
:
cp
$(SYNCHRONE_DIR)
/lurette/
$(ALL_RELEASE_NAME)
.tgz /usr/local/tools/lu
stre-misc
&&
\
cd
/usr/local/tools/lu
stre-misc
&&
\
cp
$(SYNCHRONE_DIR)
/lurette/
$(ALL_RELEASE_NAME)
.tgz /usr/local/tools/lu
rette
&&
\
cd
/usr/local/tools/lu
rette
&&
\
tar
xvfz
$(ALL_RELEASE_NAME)
.tgz
&&
\
rm
-rf
lurette_old
&&
\
mv
-f
/usr/local/tools/lustre-misc/lurette /usr/local/tools/lustre-misc/lurette_old
&&
\
mv
/usr/local/tools/lustre-misc/
$(ALL_RELEASE_NAME)
/usr/local/tools/lustre-misc/lurette
&&
\
cd
/usr/local/tools/lustre-misc/lurette
&&
\
rm
$(ALL_RELEASE_NAME)
.tgz
&&
\
cd
/usr/local/tools/lurette/
$(ALL_RELEASE_NAME)
&&
\
./RUN_ME
cd
/usr/local/tools/lustre-misc/lurette/examples/
&&
\
make
test
&&
\
mkdir
-p
$(
shell
ocamlc
-where
)
/../lucky
&&
\
cp
-rf
/usr/local/tools/lustre-misc/lurette/lib
$(
shell
ocamlc
-where
)
/../lucky
cd
/usr/local/tools/lurette/
$(ALL_RELEASE_NAME)
/examples/
&&
\
make
test
source/common/command_line.ml
View file @
6e017db3
...
...
@@ -174,13 +174,5 @@ let usage =
let
cmd_line_string_to_int
str
errmsg
=
try
(
int_of_string
str
)
with
Failure
(
"int_of_string"
)
->
print_string
usage
;
print_string
errmsg
;
flush
stdout
;
failwith
"
\n
*** Error when calling lurette.
\n
"
Util
.
my_int_of_string
str
(* Avoid crashing if int are too big *)
source/common/lurette_ocaml.ml
View file @
6e017db3
...
...
@@ -669,7 +669,7 @@ and
"
\n
One more loop ? [type 's' to stop, `CR' to continue, or an integer to change the number of steps to skip.]
\n
"
;
let
str
=
read_line
()
in
try
let
i
=
int_of_string
str
in
let
i
=
Util
.
my_
int_of_string
str
in
options
.
step_by_step
<-
Some
i
;
str
with
_
->
...
...
source/common/lustreRun.ml
View file @
6e017db3
(* Time-stamp: <modified the
26/03/2014 (at 17:46
) by Erwan Jahier> *)
(* Time-stamp: <modified the
02/09/2014 (at 14:53
) by Erwan Jahier> *)
open
RdbgPlugin
type
vars
=
(
string
*
Data
.
t
)
list
...
...
@@ -454,7 +454,7 @@ let (make_luciole : string -> vars -> vars ->
exit
2
)
|
"int"
->
(
try
Data
.
I
(
int_of_string
str
)
try
Data
.
I
(
Util
.
my_
int_of_string
str
)
with
e
->
output_msg2
(
"read_luciole_outputs:Can not convert the value of "
^
name
^
" into an int:'"
^
str
^
"'
\n
"
^
...
...
source/common/myArg.ml
View file @
6e017db3
...
...
@@ -165,14 +165,14 @@ let parse_argv ?(current=current) argv speclist anonfun errmsg =
incr
current
;
|
Int
f
when
!
current
+
1
<
l
->
let
arg
=
argv
.
(
!
current
+
1
)
in
begin
try
f
(
int_of_string
arg
)
with
Failure
"int_of_string"
->
raise
(
Stop
(
Wrong
(
s
,
arg
,
"an integer"
)))
begin
try
f
(
Util
.
my_
int_of_string
arg
)
with
Failure
"int_of_string"
->
raise
(
Stop
(
Wrong
(
s
,
arg
,
"an integer"
)))
end
;
incr
current
;
|
Set_int
r
when
!
current
+
1
<
l
->
let
arg
=
argv
.
(
!
current
+
1
)
in
begin
try
r
:=
(
int_of_string
arg
)
begin
try
r
:=
(
Util
.
my_
int_of_string
arg
)
with
Failure
"int_of_string"
->
raise
(
Stop
(
Wrong
(
s
,
arg
,
"an integer"
)))
end
;
...
...
source/common/myGenlex.ml
View file @
6e017db3
...
...
@@ -53,22 +53,7 @@ let get_string () =
(* The lexer *)
(* Avoid crashing if int are too big *)
let
my_int_of_string
str
=
try
int_of_string
str
with
_
->
let
i64
=
Int64
.
of_string
str
in
let
i
=
if
i64
>
(
Int64
.
of_int
max_int
)
then
max_int
/
4
else
if
i64
<
(
Int64
.
of_int
min_int
)
then
min_int
/
4
else
Int64
.
to_int
i64
(* deadcode IMHO *)
in
Printf
.
eprintf
"Warning: The integer %s is too big: truncate it to %i
\n
"
str
i
;
flush
stderr
;
i
let
my_int_of_string
=
Util
.
my_int_of_string
let
make_lexer
keywords
=
let
kwd_table
=
Hashtbl
.
create
17
in
...
...
source/common/util.ml
View file @
6e017db3
...
...
@@ -1046,3 +1046,34 @@ let int_of_num n =
(* Cloned from the OCaml stdlib Arg module: I want it on stdout! (scrogneugneu) *)
let
usage_out
speclist
errmsg
=
Printf
.
printf
"%s"
(
Arg
.
usage_string
speclist
errmsg
)
(* The behavior of ocaml wrt non representable int is arguably wrong.
It would make more sense to reason modulo 2^(max_int-1) instead of
raising a fatal error! Here I try to mimick the expected behavior
as much as possible.
*)
let
big_max_int
=
Big_int
.
big_int_of_nativeint
Nativeint
.
max_int
(* let big_min_int = Big_int.big_int_of_nativeint Nativeint.min_int *)
let
my_int_of_string
str
=
try
int_of_string
str
with
_
->
let
big_i
=
Big_int
.
big_int_of_string
str
in
try
let
big_i
=
Big_int
.
mod_big_int
big_i
big_max_int
in
Nativeint
.
to_int
(
Big_int
.
nativeint_of_big_int
big_i
)
with
_
->
assert
false
(* Should not occur !!!!
The following ran for hours...
let x = ref Big_int.zero_big_int;;
while true do
let i1 = (my_int_of_string (Big_int.string_of_big_int (!x))) in
let i2 = (my_int_of_string (Big_int.string_of_big_int (Big_int.minus_big_int !x))) in
if i1 = 0 then (print_string "coucou\n"; flush stdout);
x := Big_int.succ_big_int !x;
x := Big_int.mult_big_int (Big_int.big_int_of_int ((Random.int 1001) - 500 )) !x ;
done
*)
source/lus2lic/actionsDeps.ml
View file @
6e017db3
(** Time-stamp: <modified the
20/05/2014 (at 16:08
) by Erwan Jahier> *)
(** Time-stamp: <modified the
13/08/2014 (at 17:01
) by Erwan Jahier> *)
let
dbg
=
(
Verbose
.
get_flag
"deps"
)
...
...
@@ -130,6 +130,7 @@ let rec (get_parents : Soc.var_expr -> Soc.var_expr list) =
fun
var
->
(* if var = t.[2].field, then it returns (also) t.[2] and t *)
match
var
with
|
Soc
.
Slice
(
ve
,_,_,_,_,_
)
|
Soc
.
Field
(
ve
,_,_
)
|
Soc
.
Index
(
ve
,_,_
)
->
ve
::
(
get_parents
ve
)
|
Soc
.
Var
(
_
,
vt
)
...
...
@@ -173,7 +174,6 @@ let (get_var2actions_tbl : action list -> var2actions_tbl) =
[actions_of_vars input_vars al] trouve toutes les actions de [al] qui
ont besoin d'être effectuées avant de pouvoir se servir de [input_vars]
comme entrée d'une autre action.
TODO: gérer les dépendances entre des filtres plus complexes,
comme par ex., l'utilisation d'un champ d'une structure nécessite
...
...
@@ -187,7 +187,7 @@ let rec (actions_of_vars: Soc.var_expr list -> var2actions_tbl -> action list) =
try
Actions
.
elements
(
var2actions
var
tbl
)
with
Not_found
->
[]
in
let
vars
=
List
.
flatten
(
List
.
map
get_parents
vars
)
in
let
vars
=
List
.
flatten
(
List
.
map
get_parents
vars
)
in
let
vars
=
List
.
fold_left
(
fun
acc
x
->
if
List
.
mem
x
acc
then
acc
else
x
::
acc
)
[]
vars
in
List
.
flatten
(
List
.
map
find_deps
vars
)
...
...
@@ -284,7 +284,7 @@ let rec (visit : t -> color_table -> action -> color_table) =
|
Grey
->
raise
(
DependencyCycle
(
n
,
grey_actions
color_t
))
|
Black
->
color_t
with
(* The node [nt] is white *)
(* The node [nt] is white *)
Not_found
->
visit
succ_t
color_t
nt
)
(
MapAction
.
find
n
succ_t
)
...
...
source/lus2lic/actionsDeps.mli
View file @
6e017db3
(** Time-stamp: <modified the
11/12/2013 (at 17
:49) by Erwan Jahier> *)
(** Time-stamp: <modified the
09/07/2014 (at 15
:49) by Erwan Jahier> *)
(** Compute dependencies between actions *)
...
...
@@ -37,7 +37,7 @@ val string_of_action_simple: action -> string
Construit des dépendances entre les actions en reliant les entrées et
les sorties de ces actions.
Lic2soc.lic_to_soc_type is passed in
n argument to break a mutuel
dep loop
Lic2soc.lic_to_soc_type is passed in
argument to break a
dep loop
*)
val
build_data_deps_from_actions
:
(
Lic
.
type_
->
Data
.
t
)
->
t
->
action
list
->
t
...
...
source/lus2lic/ast2lic.ml
View file @
6e017db3
(* Time-stamp: <modified the 0
5/06/2013 (at 14:41
) by Erwan Jahier> *)
(* Time-stamp: <modified the 0
1/09/2014 (at 11:22
) by Erwan Jahier> *)
open
Lxm
...
...
@@ -30,7 +30,7 @@ let rec (of_type: IdSolver.t -> AstCore.type_exp -> Lic.type_) =
let
sz
=
EvalConst
.
eval_array_size
env
szexp
in
Array_type_eff
(
elt_teff
,
sz
)
with
EvalConst
.
EvalArray_error
msg
->
let
lxm
=
lxm_of_val_exp
szexp
in
let
lxm
=
AstCore
.
lxm_of_val_exp
szexp
in
raise
(
Compile_error
(
lxm
,
"can't eval type: "
^
msg
))
...
...
@@ -95,11 +95,11 @@ and (type_check_equation: IdSolver.t -> Lxm.t -> Lic.left list ->
(* Checks that the left part has the same clock as the right one. *)
and
(
clock_check_equation
:
IdSolver
.
t
->
Lxm
.
t
->
UnifyClock
.
subst
->
Lic
.
left
list
->
Lic
.
val_exp
->
unit
)
=
fun
id_solver
lxm
s
lpl_eff
ve_eff
->
let
clk_list
=
List
.
map
Lic
.
clock
_of_left
lpl_eff
in
let
_
,
right_part_clks
,
s
=
EvalClock
.
f
lxm
id_solver
s
ve_eff
clk_list
in
EvalClock
.
check_res
lxm
s
lpl_eff
right_part_clks
Lic
.
left
list
->
Lic
.
id_clock
list
->
Lic
.
val_exp
->
Lic
.
val_exp
)
=
fun
id_solver
lxm
s
lpl_eff
right_part_clks
ve_eff
->
let
lxms
=
List
.
map
Lic
.
lxm
_of_left
lpl_eff
in
EvalClock
.
check_res
lxms
s
lpl_eff
right_part_clks
;
ve_eff
(******************************************************************************)
(*
...
...
@@ -166,6 +166,8 @@ let get_abstract_static_params
*)
[]
)
(* exported *)
let
rec
of_node
...
...
@@ -287,15 +289,19 @@ and check_static_arg
(******************************************************************************)
(* exported *)
and
(
of_eq
:
IdSolver
.
t
->
AstCore
.
eq_info
srcflagged
->
Lic
.
eq_info
srcflagged
)
=
fun
id_solver
eq_info
->
let
(
lpl
,
ve
)
=
eq_info
.
it
in
let
lpl_eff
=
List
.
map
(
translate_left_part
id_solver
)
lpl
and
clk_subst
,
ve_eff
=
translate_val_exp_check
id_solver
UnifyClock
.
empty_subst
ve
let
lpl_eff
=
List
.
map
(
translate_left_part
id_solver
)
lpl
in
let
exp_clks
=
List
.
map
Lic
.
clock_of_left
lpl_eff
in
let
cs
=
UnifyClock
.
empty_subst
in
let
ve_eff
,
right_part_clks
,
cs
=
translate_val_exp_check
id_solver
exp_clks
cs
ve
in
let
ve_eff
=
type_check_equation
id_solver
eq_info
.
src
lpl_eff
ve_eff
;
clock_check_equation
id_solver
eq_info
.
src
cs
lpl_eff
right_part_clks
ve_eff
in
type_check_equation
id_solver
eq_info
.
src
lpl_eff
ve_eff
;
clock_check_equation
id_solver
eq_info
.
src
clk_subst
lpl_eff
ve_eff
;
flagit
(
lpl_eff
,
ve_eff
)
eq_info
.
src
...
...
@@ -345,14 +351,15 @@ and (translate_left_part : IdSolver.t -> AstCore.left_part -> Lic.left) =
(* Translate and performs the checks *)
and
(
translate_val_exp_check
:
IdSolver
.
t
->
UnifyClock
.
subst
->
AstCore
.
val_exp
->
UnifyClock
.
subst
*
Lic
.
val_exp
)
=
fun
id_solver
s
ve
->
and
(
translate_val_exp_check
:
IdSolver
.
t
->
Lic
.
clock
list
->
UnifyClock
.
subst
->
AstCore
.
val_exp
->
Lic
.
val_exp
*
Lic
.
id_clock
list
*
UnifyClock
.
subst
)
=
fun
id_solver
exp_clks
s
ve
->
let
s
,
vef
=
translate_val_exp
id_solver
s
ve
in
let
lxm
=
AstCore
.
lxm_of_val_exp
ve
in
(* let vef, tl = EvalType.f id_solver vef in *)
let
vef
,
_
,
s
=
EvalClock
.
f
lxm
id_solver
s
vef
[]
in
s
,
vef
let
lxms
=
List
.
map
(
fun
_
->
lxm
)
exp_clks
in
(* let vef, tl = EvalType.f id_solver vef in *)
EvalClock
.
f
id_solver
s
vef
lxms
exp_clks
and
(
translate_val_exp
:
IdSolver
.
t
->
UnifyClock
.
subst
->
AstCore
.
val_exp
->
UnifyClock
.
subst
*
Lic
.
val_exp
)
=
...
...
@@ -434,6 +441,7 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp
in
CallByPosLic
(
flagit
by_pos_op_eff
lxm
,
[
array_val_exp
])
in
let
s
,
vef_core
=
match
by_pos_op
with
|
WITH_n
(
_
,_,_
)
->
assert
false
(* handled at the top of the function *)
...
...
@@ -470,7 +478,7 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp
in
s
,
const
.
ve_core
)
|
CURRENT_n
->
s
,
mk_by_pos_op
Lic
.
CURRENT
|
CURRENT_n
->
s
,
mk_by_pos_op
(
Lic
.
CURRENT
None
)
|
PRE_n
->
s
,
mk_by_pos_op
Lic
.
PRE
|
ARROW_n
->
s
,
mk_by_pos_op
Lic
.
ARROW
...
...
@@ -483,7 +491,7 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp
s
,
CallByPosLic
(
flagit
Lic
.
ARROW
lxm
,
[
e1
;
ve_pre
])
|
_
->
assert
false
)
(* | FBY_n -> s, mk_by_pos_op Lic.FBY *)
(* | FBY_n -> s, mk_by_pos_op Lic.FBY *)
|
CONCAT_n
->
s
,
mk_by_pos_op
Lic
.
CONCAT
|
TUPLE_n
->
s
,
mk_by_pos_op
Lic
.
TUPLE
|
ARRAY_n
->
s
,
CallByPosLic
(
flagit
Lic
.
ARRAY
lxm
,
vel_eff
)
...
...
@@ -519,7 +527,6 @@ and (translate_val_exp : IdSolver.t -> UnifyClock.subst -> AstCore.val_exp
in
let
vef
=
{
ve_core
=
vef_core
;
ve_typ
=
[]
;
ve_clk
=
[]
}
in
let
vef
,
tl
=
EvalType
.
f
id_solver
vef
in
(* let vef, _, s = EvalClock.f lxm id_solver s vef [] in *)
s
,
vef
)
...
...
@@ -595,7 +602,9 @@ and (translate_slice_info : IdSolver.t -> AstCore.slice_info ->
let
(
of_assertion
:
IdSolver
.
t
->
AstCore
.
val_exp
Lxm
.
srcflagged
->
Lic
.
val_exp
Lxm
.
srcflagged
)
=
fun
id_solver
vef
->
let
s
,
val_exp_eff
=
translate_val_exp_check
id_solver
UnifyClock
.
empty_subst
vef
.
it
in
let
s
=
UnifyClock
.
empty_subst
in
let
exp_clks
=
[
BaseLic
]
in
(* assertions are on the base clock *)
let
val_exp_eff
,
_
,
s
=
translate_val_exp_check
id_solver
exp_clks
s
vef
.
it
in
(* Check that the assert is a bool. *)
let
val_exp_eff
,
evaled_exp
=
EvalType
.
f
id_solver
val_exp_eff
in
List
.
iter
...
...
@@ -612,7 +621,7 @@ let (of_assertion : IdSolver.t -> AstCore.val_exp Lxm.srcflagged ->
(* Clock check the assertion*)
let
_
,
clock_eff_list
,
_s
=
EvalClock
.
f
vef
.
src
id_solver
s
val_exp_eff
[
BaseLic
]
EvalClock
.
f
id_solver
s
val_exp_eff
[
vef
.
src
]
[
BaseLic
]
in
match
clock_eff_list
with
|
[
id
,
BaseLic
]
...
...
source/lus2lic/astCore.ml
View file @
6e017db3
(* Time-stamp: <modified the
04/04/2013 (at 15:10
) by Erwan Jahier> *)
(* Time-stamp: <modified the
26/08/2014 (at 16:06
) by Erwan Jahier> *)
(** (Raw) Abstract syntax tree of source Lustre Core programs. *)
...
...
@@ -214,3 +214,4 @@ let lxm_of_val_exp = function
|
CallByName
(
op
,_
)
->
op
.
src
|
Merge_n
(
ve
,_
)
->
ve
.
src
|
Merge_bool_n
(
id
,_,_
)
->
id
.
src
source/lus2lic/astTabSymbol.ml
View file @
6e017db3
(* Time-stamp: <modified the
11/04/2013 (at 15:2
8) by Erwan Jahier> *)
(* Time-stamp: <modified the
09/07/2014 (at 17:1
8) by Erwan Jahier> *)
(**
Sous-module pour AstTab
...
...
@@ -58,8 +58,7 @@ let find_node (this: t) (id: Ident.t) lxm =
if
Lxm
.
line
lxm
=
0
&&
Lxm
.
cend
lxm
=
0
then
(* A hack to print a nicer error msg when the node asked in the
command-line is not found in the input files*)
raise
(
Global_error
(
"Can not find node "
^
(
Ident
.
to_string
id
)
^
" in "
^
(
Lxm
.
file
lxm
)))
raise
(
Global_error
(
"Can not find node "
^
(
Ident
.
to_string
id
)))
else
let
all_nodes
=
Hashtbl
.
fold
(
fun
n
_
acc
->
(
Ident
.
to_string
n
)
::
acc
)
this
.
st_nodes
[]
...
...
source/lus2lic/compile.ml
View file @
6e017db3
(* Time-stamp: <modified the
12/06/2014 (at 09:42
) by Erwan Jahier> *)
(* Time-stamp: <modified the
04/09/2014 (at 10:41
) by Erwan Jahier> *)
open
Lxm
open
Lv6errors
...
...
@@ -13,7 +13,7 @@ let info msg =
let
(
doit
:
Lv6MainArgs
.
t
->
AstV6
.
pack_or_model
list
->
Ident
.
idref
option
->
LicPrg
.
t
)
=
fun
opt
srclist
main_node
->
let
t0
=
Sys
.
time
()
in
(* let t0 = Sys.time() in *)
info
"Start compiling to lic...
\n
"
;
let
syntax_tab
=
AstTab
.
create
srclist
in
(* Pour chaque package, on a un solveur de rfrences
...
...
@@ -58,7 +58,7 @@ let (doit : Lv6MainArgs.t -> AstV6.pack_or_model list -> Ident.idref option -> L
then
(
(* Split des equations (1 eq = 1 op) *)
info
"One op per equations...
\n
"
;
L2lSplit
.
doit
zelic
)
L2lSplit
.
doit
opt
zelic
)
else
zelic
in
...
...
source/lus2lic/evalClock.ml
View file @
6e017db3
(* Time-stamp: <modified the
25/09/2013 (at 10:58
) by Erwan Jahier> *)
(* Time-stamp: <modified the
01/09/2014 (at 14:29
) by Erwan Jahier> *)
open
AstPredef
...
...
@@ -70,7 +70,7 @@ open UnifyClock
- "cil_arg" the list of clocks of arguments (via a rec call to f)
In order to check that this call is correct, we check that both
terms
are unifiable
.
terms
match
.
It also modifies the substitution s (acculumated all along the
clock checking of the node) such that:
...
...
@@ -79,12 +79,20 @@ open UnifyClock
*)
let
(
check_args
:
Lxm
.
t
->
subst
->
Lic
.
id_clock
list
->
Lic
.
id_clock
list
->
subst
)
=
fun
lxm
s
cil_par
cil_arg
->
let
rec
fold_left3
f
accu
l1
l2
l3
=
match
(
l1
,
l2
,
l3
)
with
([]
,
[]
,
[]
)
->
accu
|
(
a1
::
l1
,
a2
::
l2
,
a3
::
l3
)
->
fold_left3
f
(
f
accu
a1
a2
a3
)
l1
l2
l3
|
(
_
,
_
,
_
)
->
invalid_arg
"fold_left3 (evalClock)"
let
(
check_args
:
Lxm
.
t
list
->
subst
->
Lic
.
id_clock
list
->
Lic
.
id_clock
list
->
subst
)
=
fun
lxms
s
cil_par
cil_arg
->
assert
(
List
.
length
cil_par
=
List
.
length
cil_arg
);
let
idl_par
,
cil_par
=
List
.
split
cil_par
and
idl_arg
,
cil_arg
=
List
.
split
cil_arg
in
let
ns
=
List
.
fold_left2
(
UnifyClock
.
f
lxm
)
s
cil_arg
cil_par
in
let
ns
=
assert
(
List
.
length
cil_arg
=
List
.
length
cil_par
);
fold_left3
UnifyClock
.
f
s
lxms
cil_arg
cil_par
in
(* should UnifyClock.f modify the *)
(
fst
s
,
snd
ns
)
(* ns *)
...
...
@@ -107,7 +115,7 @@ let (check_args : Lxm.t -> subst -> Lic.id_clock list -> Lic.id_clock list -> su
- "left" the list of Lic.left
- "rigth" the list of result clock. (via "get_clock_profile" again)
and we just need to check that both side
are unifiable
.
and we just need to check that both side
match
.
*)
let
rec
(
var_info_eff_of_left_eff
:
Lic
.
left
->
Lic
.
var_info
)
=
...
...
@@ -135,15 +143,16 @@ let rec (var_info_eff_of_left_eff: Lic.left -> Lic.var_info) =
let
var_info_eff_to_clock_eff
v
=
v
.
var_clock_eff
(* exported *)
let
(
check_res
:
Lxm
.
t
->
subst
->
Lic
.
left
list
->
Lic
.
id_clock
list
->
unit
)
=
fun
lxm
(
s1
,
s2
)
left
rigth
->
let
(
check_res
:
Lxm
.
t
list
->
subst
->
Lic
.
left
list
->
Lic
.
id_clock
list
->
unit
)
=
fun
lxm
s
(
s1
,
s2
)
left
rigth
->
let
left_vi
=
List
.
map
var_info_eff_of_left_eff
left
in
let
left_ci
=
List
.
map
var_info_eff_to_clock_eff
left_vi
in
if
(
List
.
length
left_ci
<>
List
.
length
rigth
)
then
assert
false
;
let
idl_rigth
,
rigth
=
List
.
split
rigth
and
idl_left
,
left_ci
=
List
.
split
left_ci
in
let
s
=
(
List
.
combine
idl_rigth
idl_left
)
@
s1
,
s2
in
ignore
(
List
.
fold_left2
(
UnifyClock
.
f
lxm
)
s
left_ci
rigth
)
assert
(
List
.
length
left_ci
=
List
.
length
rigth
);
ignore
(
fold_left3
UnifyClock
.
f
s
lxms
left_ci
rigth
)
(******************************************************************************)
...
...
@@ -165,11 +174,11 @@ let rec (is_a_sub_clock :
|
On
(
_
,_
)
,
BaseLic
->
None
|
sc
,
On
(
_
,
c_clk
)
->
(
try
Some
(
UnifyClock
.
f
lxm
s
sc
c
)
try
Some
(
UnifyClock
.
f
s
lxm
sc
c
)
with
Compile_error
_
->
aux
sc
c_clk
)
|
_
,_
->
try
Some
(
UnifyClock
.
f
lxm
s
sc
c
)
try
Some
(
UnifyClock
.
f
s
lxm
sc
c
)
with
Compile_error
_
->
None
in
aux
sc
c
...
...
@@ -183,25 +192,50 @@ let (get_clock_profile : Lic.node_exp -> clock_profile) =
let
ci2str
=
LicDump
.
string_of_clock2
let
list_fill
x
n
=
let
rec
aux
x
n
acc
=
if
n
<=
0
then
acc
else
aux
x
(
n
-
1
)
(
x
::
acc
)
in
aux
x
n
[]
let
rec
(
get_lxm_list
:
Lic
.
val_exp
list
->
int
->
Lxm
.
t
list
)
=
fun
args
n
->
if
n
<>
List
.
length
args
then
(* occur if args is a tuple (only ?).
get the list from the tuple in that case *)
(
match
args
with
|
[{
ve_core
=
CallByPosLic
({
it
=
Lic
.
TUPLE
}
,
args
)}]
->
get_lxm_list
args
n
|
_
->
(* occurs ? *)
let
lxm
=
lxm_of_val_exp
(
List
.
hd
args
)
in