Skip to content

GitLab

Commit e8f21702 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Add support to compile Lustre V6 programs.

parent 545e775f
Hide whitespace changes
Inline Side-by-side
Makefile
View file @ e8f21702
......@@ -16,17 +16,19 @@ clean:
VERSION:=$(shell E=`git log --oneline | wc -l` ; echo "$$E-165" | bc )
VERSION:=$(shell E=`git log --oneline | wc -l` ; echo "$$E-166" | bc )
VERSION:="1.$(VERSION)"
gen_version:
rm -f source/version.ml
echo "let str=\"$(VERSION)\"" > source/version.ml
rm VERSION
date +VERSION_DATE=%d-%m-%y > VERSION
echo "VERSION=$(VERSION)" >> VERSION
echo "export VERSION" >> VERSION
echo "export VERSION_DATE" >> VERSION
rm version.tex
date +VERSION_DATE=%d-%m-%y > version.tex
echo "\\newcommand{\\version}{$(VERSION)}" > version.tex
echo "\\newcommand{\\versiondate}{`date +%d-%m-%y`}" >> version.tex
# \newcommand{\version}{unstable.3}
# \newcommand{\versiondate}{01-02-07}
......
RELEASE-NOTES
View file @ e8f21702
V1.47 (25/03/2010)
V1.49 (8/04/2010)
* Lurette now accepts oracle that have more than one output. Only the
first one should be a boolean, and is the one taken into account in
order to decide if the test fails or not. All the outputs of the
oracle are printed in the rif file after the #ORACLE_OUTPUT pragma.
That can be very convenient to track why the oracle failed.
* Add support to compile Lustre V6 programs.
V1.48 (25/03/2010)
* Lurette now accepts oracles that have more than one output. Only
the first one should be a boolean, and is the one taken into
account in order to decide if the test fails or not. All the
outputs of the oracle are printed in the rif file after the
#ORACLE_OUTPUT pragma. That can be very convenient to track why
the oracle failed.
V1.47 (19/03/2010)
......
VERSION
View file @ e8f21702
VERSION_DATE=25-03-10
VERSION=48
VERSION_DATE=08-04-10
VERSION=1.49
export VERSION
export VERSION_DATE
doc/lurette-man/Makefile
View file @ e8f21702
......@@ -30,7 +30,7 @@ v :
xpdf $(MAIN).pdf
cp : $(MAIN).pdf
cp -f $(MAIN).pdf /usr/local/www/SYNCHRONE/lurette/doc/
cp -f $(MAIN).pdf /usr/local/www/DIST-TOOLS/SYNCHRONE/lurette/doc/
cp -f $(MAIN).pdf /usr/local/tools/lustre-misc/lurette/doc
......
doc/lurette-man/lurette-man.tex
View file @ e8f21702
......@@ -502,7 +502,7 @@ ambiguity: the scade compiler should be used.
However, for {\tt .lus} files, lurette needs to know whether to use
the Verimag or the Scade compiler. Furthermore, for {\tt .c} files,
the Verimag V4, the Verimag V6, or the Scade compiler. Furthermore, for {\tt .c} files,
lurette needs to know whether they follow the Verimag and the Scade
conventions.
......@@ -512,12 +512,13 @@ Users can specify the compiler mode using the
Figure~\ref{main-window-part}). They can choose between:
\begin{itemize}
\item {\tt verimag}
\item {\tt lv4}
\item {\tt lv6}
\item {\tt scade}
\item {\tt stdin/stdout}
\end{itemize}
The first two items correspond to the verimag and the scade
The first 3 items correspond to the verimag and the scade
conventions that we have been just talking about.
%
The third item correspond to an (experimental) completely different
......@@ -855,6 +856,8 @@ lurette\version/<arch>/set\_env\_var} file.
\item \envvar{LUS2EC}{lus2ec}{to override the lustre to ec verimag compiler}
\item \envvar{LUS2LIC}{lus2lic}{to override the lustre V6 verimag compiler}
\item \envvar{EC2C}{ec2c}{to override the ec to C verimag compiler}
\item \envvar{SCADE2LUSTRE}{scade2lustre}{to override the scade to lustre compiler}
......
examples/xlurette/tram/Makefile
View file @ e8f21702
......@@ -5,7 +5,7 @@ CC=g++
test1:
rm -f test1.rif0 .lurette_rc && \
$(LURETTETOP) --sut tramway.lus \
$(LURETTETOP) --sut tramway.lus --sut-compiler lv4 --oracle-compiler lv4 \
-msn controller -go -l 100 --draw-all-formula -td 10 \
--draw-inside 1 --compute-poly-volume \
--do-not-show-step -o test1.rif0 \
......@@ -21,7 +21,7 @@ test1:
test2 :
rm -f test2.rif0 && \
$(LURETTETOP) -l 100 -go -seed 1 \
$(LURETTETOP) -l 100 -go -seed 1 --sut-compiler lv4 --oracle-compiler lv4 \
--do-not-show-step -ns2c \
-sut tramway.lus --main-sut-node controller \
-oracle tramway.lus --main-oracle-node oracle \
......
install/configure.in
View file @ e8f21702
......@@ -161,9 +161,11 @@ AC_SUBST(MORE_LIB)
#-----------------------------------------------------------------------------#
# Lustre tools
LUS2LIC=lus2lic
LUS2EC=lus2ec
EC2C=ec2c
AC_SUBST(LUS2LIC)
AC_SUBST(LUS2EC)
AC_SUBST(EC2C)
......
install/set_env_var.in
View file @ e8f21702
......@@ -34,6 +34,11 @@ if test -z "$DOT" ; then
export DOT
fi
if test -z "$LUS2LIC" ; then
LUS2LIC=@LUS2LIC@
export LUS2LIC
fi
if test -z "$LUS2EC" ; then
LUS2EC=@LUS2EC@
export LUS2EC
......
source/Makefile
View file @ e8f21702
......@@ -686,11 +686,13 @@ check:
allw:libnc lucky ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc4c libluc4c_nc.a draw-all luc4ocaml-all
all: libnc lucky ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc4c libluc4c draw-all luc4ocaml-all
allnc: libncnc lucky ltop show stubs gnuplot-rif gnuplot-socket gen_luc luc2c luc4c libluc4c draw-all luc4ocaml-all
static: libnc lucky_static ltop_static show_static stubs_static gen_luc_static
OTAGS=/local/jahier/otags-3.09.3.2/otags
tags: $(REALLY_ALL_SOURCES)
otags -v ../source/*.ml && cp TAGS $(LURETTE_PATH)/source
$(OTAGS) -v $(REALLY_ALL_SOURCES) $(shell ocamlc -where)/*.mli
# ne marche que si on lance cette commande A LA MAIN (!!!) depuis une fenetre DOS
strtopwin:
......
source/Makefile.release
View file @ e8f21702
......@@ -3,7 +3,8 @@
ifeq ($(HOST_TYPE),win32)
VERSION = $(shell cat ../source/version.ml | sed 's/=/ /' | sed 's/\"//g' | awk '{printf "%s\n", $$3}')
else
VERSION = $(shell git log --oneline -1 | awk '{printf "%s\n", $$3}' )
SVERSION = $(shell E=`git log --oneline | wc -l` ; echo "$$E-166" | bc )
VERSION ="1.$(SVERSION)"
endif
#VERSION=1.43
......@@ -97,6 +98,7 @@ lurette-rel: strip
$(LURETTE_PATH)/$(HOST_TYPE)/bin/getsaonodes \
$(LURETTE_PATH)/$(HOST_TYPE)/bin/lusinfo$(EXE) \
$(LURETTE_PATH)/$(HOST_TYPE)/bin/lus2ec* \
$(LURETTE_PATH)/$(HOST_TYPE)/bin/luc2lic \
$(LURETTE_PATH)/$(HOST_TYPE)/bin/ec2c$(EXE) \
$(LURETTE_PATH)/$(HOST_TYPE)/bin/pollux$(EXE) \
$(LURETTE_PATH)/$(HOST_TYPE)/bin/lurettetop_exe$(EXE) \
......@@ -367,6 +369,12 @@ test-rel:
cd /tmp/$(ALL_RELEASE_NAME)/examples/ && \
make test
# Update the web site woth the new tgz
www:
cd ~/tools/html/ ; make go
cp ../RELEASE-NOTES $(SYNCHRONE_DIR)/lurette/
#################################################################################################"
......
source/gen_fake_lucky.ml
View file @ e8f21702
......@@ -396,7 +396,7 @@ let rec (main : unit -> unit) =
let (tdl, vi, vo) =
let comp = Gen_stubs_common.string_to_compiler compiler in
match comp with
Verimag -> Parse_poc.get_vn_and_ct_list header_file
| VerimagV4 | VerimagV6 -> Parse_poc.get_vn_and_ct_list header_file
| Scade -> Parse_c_scade.get_vn_and_ct_list header_file mod_name comp
| ScadeGUI -> Parse_c_scade.get_vn_and_ct_list header_file mod_name comp
| Sildex -> Parse_sildex.get_vn_and_ct_list header_file
......@@ -409,3 +409,4 @@ let rec (main : unit -> unit) =
main ();;
source/gen_fake_lutin.ml
View file @ e8f21702
......@@ -158,7 +158,7 @@ let rec (main : unit -> unit) =
in
let (vi, vo) =
match Gen_stubs_common.string_to_compiler compiler with
Verimag ->
| VerimagV4 | VerimagV6 ->
let (vi0, vo0) =
Parse_poc.get_vn_and_ct_list header_file
in
......@@ -168,6 +168,7 @@ let rec (main : unit -> unit) =
let vo = Gen_stubs_common.replace_ct_by_their_alias vo0 alias in
(vi, vo)
| VerimagV6 -> assert false
| Scade -> Parse_c_scade.get_vn_and_ct_list header_file mod_name
in
generate_lutin compiler (mod_name ^ "_env") (List.rev vo) (List.rev vi) dir
......
source/gen_stubs.ml
View file @ e8f21702
......@@ -46,10 +46,11 @@ open Gen_stubs_common
*)
let (gen_a_fake_oracle : string -> string -> string -> compiler -> string -> bool) =
fun user_dir tmp_dir sut_node compiler sut_h ->
try
(* try *)
let (tdl, sut_h, sut_vi, sut_vo) =
match compiler with
Verimag ->
| VerimagV6
| VerimagV4 ->
let (tdl, vi, vo) = Parse_poc.get_vn_and_ct_list sut_h in
(tdl, sut_h, vi, vo)
| Scade ->
......@@ -87,8 +88,9 @@ let (gen_a_fake_oracle : string -> string -> string -> compiler -> string -> boo
put "\n";
close_out oc;
true
with _ ->
false
(* with e -> *)
(* output_string stderr (Printexc.to_string e); *)
(* false *)
......@@ -146,7 +148,7 @@ let compile_lustre_program_if_needed
then
(Filename.chop_extension lustre_prog0) ^ ".saofdm"
else
exit 2
exit 100
)
else
lustre_prog0
......@@ -187,7 +189,7 @@ let compile_lustre_program_if_needed
((Filename.chop_extension lustre_prog) ^ ".lus")
lustre_node tmp_dir)
else
exit 2
exit 101
)
else if
(Filename.check_suffix lustre_prog ".lus")
......@@ -205,16 +207,26 @@ let compile_lustre_program_if_needed
(* if no .h or .c exists, or if they are too old, we (re)generate them. *)
(
match compiler with
Verimag ->
| VerimagV6 ->
output_string stderr (
"No " ^ lustre_node ^ ".c or no " ^ lustre_node ^
".h exist(s), so I try to compile " ^ lustre_prog ^
" with node " ^ lustre_node ^
" with the lus2ec and ec2c...\n");
" with lus2lic -ec and ec2c...\n");
if Util2.lv62ec lustre_prog lustre_node user_dir then
Util2.ec2c lustre_node tmp_dir
else
exit 102
| VerimagV4 ->
output_string stderr (
"No " ^ lustre_node ^ ".c or no " ^ lustre_node ^
".h exist(s), so I try to compile " ^ lustre_prog ^
" with node " ^ lustre_node ^
" with lus2ec and ec2c...\n");
if Util2.lus2ec lustre_prog lustre_node user_dir then
Util2.ec2c lustre_node tmp_dir
else
exit 2
exit 103
| ScadeGUI ->
output_string stderr (
......@@ -240,7 +252,7 @@ let compile_lustre_program_if_needed
output_string stderr (
"Lurette do not know how to compile Sildex code " ^
"yet. \nPlease provide the C files (for the sut and the oracle).\n");
exit 2
exit 104
)
else
......@@ -269,14 +281,15 @@ let (gen_stubs_file : string -> string -> compiler -> string -> compiler ->
string -> string -> bool -> bool) =
fun tmp_dir sut sut_compiler oracle oracle_compiler sut_h oracle_h
oracle_is_present ->
try
(* try *)
let sut_m = (Filename.basename sut) in
let oracle_m = (Filename.basename oracle) in
(* Get var names and types of the sut *)
let (sut_tdl, sut_vi, sut_vo) =
match sut_compiler with
Verimag ->
| VerimagV6
| VerimagV4 ->
let (x1, x2, x3) = Parse_poc.get_vn_and_ct_list sut_h in
(x1, x2, x3)
| Scade ->
......@@ -297,7 +310,8 @@ let (gen_stubs_file : string -> string -> compiler -> string -> compiler ->
([],[],[])
else
match oracle_compiler with
Verimag ->
| VerimagV6
| VerimagV4 ->
let (x1, x2, x3) = Parse_poc.get_vn_and_ct_list oracle_h in
(x1, x2, x3)
| Scade ->
......@@ -317,7 +331,8 @@ let (gen_stubs_file : string -> string -> compiler -> string -> compiler ->
(* Generate stubs files "lurette__sut.c.new" and "lurette__oracle.c.new" *)
(
match sut_compiler with
Verimag ->
| VerimagV6
| VerimagV4 ->
Gen_stubs_poc.go sut_m "lurette__sut" sut_tdl sut_vi sut_vo
| ScadeGUI ->
Gen_stubs_scade.go sut_m "lurette__sut" sut_tdl sut_vi sut_vo sut_h
......@@ -329,7 +344,8 @@ let (gen_stubs_file : string -> string -> compiler -> string -> compiler ->
(
match oracle_compiler with
Verimag ->
| VerimagV6
| VerimagV4 ->
(Gen_stubs_poc.go
oracle_m "lurette__oracle" oracle_tdl oracle_vi_ord_decl
oracle_vo)
......@@ -358,8 +374,10 @@ let (gen_stubs_file : string -> string -> compiler -> string -> compiler ->
(Filename.concat tmp_dir "lurette__oracle.c.new")
(Filename.concat tmp_dir "lurette__oracle.c");
true
with _ ->
false
(* with e -> *)
(* output_string stdout (Printexc.to_string e); *)
(* flush stdout; *)
(* false *)
(****************************************************************************)
......@@ -512,6 +530,6 @@ let (main : unit -> 'a) =
)
;;
if (main ()) then () else exit 2 ;;
if (main ()) then () else exit 105 ;;
source/gen_stubs_common.ml
View file @ e8f21702
......@@ -62,26 +62,31 @@ let print_typedef (name, t) =
(************************************************************************)
(* compiler used to compile sut and oracles *)
type compiler = Verimag | Scade | ScadeGUI | Sildex
type compiler = VerimagV4 | VerimagV6 | Scade | ScadeGUI | Sildex
let (string_to_compiler:string -> compiler) =
fun s ->
match s with
"verimag" -> Verimag
| "Verimag" -> Verimag
| "verimag" -> VerimagV4
| "verimag" -> VerimagV4
| "lv4" -> VerimagV4
| "lv4" -> VerimagV4
| "lv6" -> VerimagV6
| "lv6" -> VerimagV6
| "scade-gui" -> ScadeGUI
| "scade" -> Scade
| "Scade" -> Scade
| "sildex" -> Sildex
| "Sildex" -> Sildex
| other ->
print_string ("The compiler " ^ other ^ " is not supported sorry.\n");
print_string ("The compiler '" ^ other ^ "' is not supported sorry.\n");
exit 2
let (compiler_to_string : compiler -> string) =
fun c ->
match c with
Verimag -> "verimag"
| VerimagV4 -> "lv4"
| VerimagV6 -> "lv6"
| Scade -> "scade"
| ScadeGUI -> "scade-gui"
| Sildex -> "sildex"
......
source/gen_stubs_common.mli
View file @ e8f21702
......@@ -27,7 +27,7 @@ type alias = c_type * c_type
type typedef = string * c_type
(* compiler used to compiler sut and oracles *)
type compiler = Verimag | Scade | ScadeGUI | Sildex
type compiler = VerimagV4 | VerimagV6 | Scade | ScadeGUI | Sildex
val string_to_compiler : string -> compiler
val compiler_to_string : compiler -> string
......
source/lurettetop.ml
View file @ e8f21702
......@@ -52,7 +52,7 @@ let lurette_bin = (Filename.concat lurette_path "bin")
(* compiler used to compiler sut and oracles *)
type compiler = Verimag | Scade | ScadeGUI | Sildex | Stdin
type compiler = VerimagV4 | VerimagV6 | Scade | ScadeGUI | Sildex | Stdin
type step_mode = | Inside | Edges | Vertices
let string_to_step_mode = function
......@@ -138,8 +138,8 @@ let (flag : flagT) = {
oracle = None ;
oracle_node = "" ;
env = "";
sut_compiler = Verimag;
oracle_compiler = Verimag;
sut_compiler = VerimagV6;
oracle_compiler = VerimagV6;
make_opt = "nc" ;
step_nb = 10;
draw_nb = 1 ;
......@@ -213,7 +213,8 @@ let (my_create_process : string -> string list -> in_channel -> out_channel ->
)
else
(
output_string oc ("*** Error: " ^ prog ^ " exited ABnormally!\n");
output_string oc ("*** Error: " ^ prog ^ " exited ABnormally (return code=" ^
(string_of_int i)^").\n");
flush oc;
false
)
......@@ -241,8 +242,12 @@ let (my_create_process : string -> string list -> in_channel -> out_channel ->
let (string_to_compiler:string -> compiler option) =
fun s ->
match s with
"verimag" -> Some Verimag
| "Verimag" -> Some Verimag
| "verimag" -> Some VerimagV4
| "Verimag" -> Some VerimagV4
| "lv4" -> Some VerimagV4
| "lv4" -> Some VerimagV4
| "lv6" -> Some VerimagV6
| "lv6" -> Some VerimagV6
| "scade-gui" -> Some ScadeGUI
| "scade_gui" -> Some ScadeGUI
| "scade" -> Some Scade
......@@ -257,7 +262,8 @@ let (string_to_compiler:string -> compiler option) =
let (compiler_to_string : compiler -> string) =
fun c ->
match c with
Verimag -> "verimag"
| VerimagV4 -> "lv4"
| VerimagV6 -> "lv6"
| Scade -> "scade"
| ScadeGUI -> "scade-gui"
| Sildex -> "sildex"
......@@ -266,7 +272,8 @@ let (compiler_to_string : compiler -> string) =
let (compiler_to_extension : compiler -> string) =
fun c ->
match c with
Verimag -> ".lus"
| VerimagV4
| VerimagV6 -> ".lus"
| Scade -> ".saofdm"
| ScadeGUI -> assert false (* we should not need to compile any thing in that mode *)
| Sildex -> assert false (* XXX what is the extension of sildex files? *)
......@@ -407,7 +414,7 @@ let rec speclist =
flush !ocr;
exit 2
),
"<string> (\"verimag\" or \"scade\")\t Compiler used for the sut.";
"<string> (lv4, lv6, scade)\t Compiler used for the sut.";
"--oracle-compiler", Arg.String
(fun s ->
......@@ -418,7 +425,7 @@ let rec speclist =
flush !ocr;
exit 2
),
"<string> (\"verimag\" or \"scade\")\t Compiler used for the oracle.";
"<string> (lv4, lv6, or scade)\t Compiler used for the oracle.";
"--test-length", Arg.Int (fun i -> flag.step_nb <- i),
......@@ -769,15 +776,21 @@ let (build : string -> bool) =
let make_opt =
match (flag.sut_compiler, flag.oracle_compiler) with
| Scade, _ -> "scade"
| Verimag, Verimag -> "nc"
| Sildex, Verimag -> "sildex_sut"
| Verimag, Sildex -> "sildex_oracle"
| VerimagV4, VerimagV6 -> "nc"
| VerimagV6, VerimagV4 -> "nc"
| VerimagV6, VerimagV6 -> "nc"
| VerimagV4, VerimagV4 -> "nc"
| Sildex, VerimagV4 -> "sildex_sut"
| VerimagV4, Sildex -> "sildex_oracle"
| Sildex, Sildex -> "sildex_both"
| ScadeGUI, _ -> "lurette"
| _, ScadeGUI -> assert false
| _, Scade -> "scade"
| Stdin, _ -> assert false
| _, Stdin -> assert false
| sc,oc ->
assert false
in
if
(oracle2 <> "") && not (Sys.file_exists oracle2)
......@@ -1550,7 +1563,8 @@ set_oracle_cmd <shell command>
set_sut_compiler <string>
to set the compiler used for the sut. Its current value is " ^
(match flag.sut_compiler with
| Verimag -> "\"verimag\""
| VerimagV4 -> "\"lv4\""
| VerimagV6 -> "\"lv6\""
| Scade -> "\"scade\""
| ScadeGUI -> "\"scade-gui\""
| Sildex -> "\"sildex\""
......@@ -1560,7 +1574,8 @@ set_sut_compiler <string>
set_oracle_compiler <string>
to set the compiler used for the oracle. Its current value is " ^
(match flag.oracle_compiler with
Verimag -> "\"verimag\""
| VerimagV4 -> "\"lv4\""
| VerimagV6 -> "\"lv6\""
| Scade -> "\"scade\""
| ScadeGUI -> "\"scade-gui\""
| Sildex -> "\"sildex\""
......@@ -2612,8 +2627,8 @@ let (read_commands : string -> (unit -> string) -> bool) =
)
with
e ->
output_string !ocr ("Warning: syntax error in luretteto command ("
^ (Printexc.to_string e) ^ ") ("^str^") \n") ;
output_string !ocr ("Bad lurette command: "
^ (Printexc.to_string e) ^ " ("^str^") \n") ;
output_string !ocr cmd_usage ;
flush !ocr;
true
......@@ -2740,7 +2755,8 @@ let main_read_arg () =
let source_dir = (Filename.concat lurette_path "source") in
match flag.sut_compiler with
Verimag -> true
| VerimagV4 -> true
| VerimagV6 -> true
| ScadeGUI -> true
| Sildex -> true
| Stdin -> true
......
source/util.ml
View file @ e8f21702
......@@ -634,14 +634,22 @@ let (my_create_process : ?std_out:(Unix.file_descr) -> ?wait:(bool) -> string
)
else
(
output_string stderr ("*** Error: " ^ prog ^ " exited abnormally.\n");
output_string stderr ("*** Error: " ^ prog ^ " exited abnormally (return code=" ^
(string_of_int i)^").\n");
flush stderr;
false
)
| _ ->
output_string stderr ("*** Error: " ^ prog ^ " exited ABnormally!\n");
| Unix.WSIGNALED i->
output_string stderr ("*** Error: " ^ prog ^ " process was killed by signal " ^
(string_of_int i)^"\n");
flush stderr;
true
| Unix.WSTOPPED i ->
output_string stderr ("*** Error: " ^ prog ^ " process was stopped by signal " ^
(string_of_int i)^"\n");
flush stderr;
true
)
with
......
source/util2.ml
View file @ e8f21702
......@@ -239,6 +239,22 @@ let (ec2c: string -> string -> bool) =
flush stdout;
false
(** [lv62ec prog] generates ec .code from lustre V6 programs *)
let (lv62ec: string -> string -> string -> bool) =
fun lustre_prog lustre_node dir ->
try
let lus2lic = Unix.getenv "LUS2LIC" in
Util.my_create_process ~std_out:Unix.stderr ~wait:true lus2lic
[
lustre_prog; "--node" ; lustre_node; "-ec";
"-o"; (Filename.concat dir (lustre_node ^ ".ec"))
]
with e ->
print_string ("LUS2LIC:" ^ (Printexc.to_string e));
flush stdout;
false
let (sim2chro: string -> bool) =
fun file ->
......
source/version.ml
View file @ e8f21702
let str="48"
let str="1.49"
xlurette/xlurette.glade
View file @ e8f21702
......@@ -373,7 +373,8 @@
<case_sensitive>False</case_sensitive>
<use_arrows>True</use_arrows>
<use_arrows_always>False</use_arrows_always>
<items>verimag