Commit 533fac24 authored by Erwan Jahier's avatar Erwan Jahier

Enhance ocaml support in lurette (cf 74f93d6c)

The oracle is not necessary anymore to run a test.

Moreover, the sut no more needs to (and must not) be named 'sut.ml'
(resp.  'oracle.ml' for the oracle).

Moreover, rename the env var EXTRA_CFILES into EXTRA_SOURCE_FILES, so that users
use it for ocaml programs.
parent 3d7485e8
......@@ -35,10 +35,10 @@ in your current directory. It might confuse Lurette.
or constants. For example, the scade compiler generates files such
as "foo_const.dc" or "foo_fctext.dc" that needs to be completed
and renamed "foo_const.c" resp "foo_fctext.c". One then need to
say Lurette to use it by filling the EXTRA_CFILES entry of the
say Lurette to use it by filling the EXTRA_SOURCE_FILES entry of the
"Extra Environment Variables" window. Note that this is not a
Lurette issue, but an issue with the code generator you use (the
EXTRA_CFILES entry filling excepted).
EXTRA_SOURCE_FILES entry filling excepted).
* It does not work.
......
......@@ -44,5 +44,7 @@ diff:
echo "il y a $(shell grep "+" diff.diff | wc -l) + et $(shell grep "-" diff.diff | wc -l) -"
# in order to tag a version, 'git tag 1.52'
# XXX automate that tag numbering and via a make rule
#tag:
# git tag ``xxx
......@@ -2,7 +2,7 @@ VERSION:=$(shell E=`git log --oneline | wc -l` ; echo "$$E-166" | bc )
VERSION:="1.$(VERSION)"
# well, finally, set it manually...
VERSION:=1.51
VERSION:=1.52
# the sha is still automatic tough!
SHA:=`git log -1 --pretty=format:"%h"`
......
V1.52 (18/08/2010)
* Add support for testing ocaml programs via lurette.
V1.51 (8/07/2010)
* New feature: when some SUT or environement inputs are missing, use
......
......@@ -11,16 +11,20 @@ $(objdir)/lurette-start.ps $(objdir)/lurette-try.ps \
$(objdir)/obj-code-gen.ps $(objdir)/components-diagram.ps \
$(objdir)/heater_sensors.ps
ALLTEX=sensors.tex wearing_sensors.tex heater_control.tex heater_control_env.tex
ALLTEX=sensors.tex wearing_sensors.tex heater_control.tex heater_control_env.tex touch.tex
all : $(objdir) pdf
make re
make re
re :
touch $(MAIN).tex; make pdf
.PHONY:touch.tex
touch.tex:
touch touch.tex
pdf:$(MAIN).pdf
re : touch.tex
make pdf
pdf:touch.tex $(MAIN).pdf
cp $(objdir)/$(MAIN).pdf .
bib :
......@@ -44,7 +48,7 @@ $(objdir):
$(MAIN).ps : $(objdir)/$(MAIN).dvi
cd $(objdir); dvips $(MAIN).dvi -o ../$(MAIN).ps ; cp $(MAIN).dvi ..
$(MAIN).pdf : $(objdir)/$(MAIN).tex $(FIGS)
$(MAIN).pdf : touch.tex $(objdir)/$(MAIN).tex $(FIGS)
cd $(objdir); pdflatex $(MAIN).tex -o ../$(MAIN).pdf
$(objdir)/$(MAIN).dvi : $(objdir)/$(MAIN).tex $(FIGS)
......
......@@ -212,7 +212,7 @@ for more information.
\newpage
\section{Lurette principles }
\section{The principles }
\label{lurette-func}
......@@ -412,6 +412,9 @@ elected at the previous step (instead of {\tt boot~i}).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newpage
\section{The tool}
\subsection{The XLurette Main window parameters}
\label{test-parameters}
......@@ -496,59 +499,36 @@ is selected in a directory that is not the same as the current one.
\subsubsection{The compiling modes}
\label{compiling-mode}
The SUT and the oracle can be either {\tt .saofdm}, {\tt .lus} or
{\tt .c} files. When the SUT is a {\tt .saofdm}, there is no
ambiguity: the scade compiler should be used.
However, for {\tt .lus} files, lurette needs to know whether to use
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.
Users can specify the compiler mode using the
combo boxes at the rigth-hand-side of the node names (cf,
Figure~\ref{main-window-part}). They can choose between:
The SUT and the oracle can be either {\tt .saofdm}, {\tt .lus}, {\tt
.c}, or {\tt .ml} files. When the SUT is a {\tt .saofdm}, there is
no ambiguity: the scade compiler should be used. However, for {\tt
.lus} files, lurette needs to know whether to use the Verimag V4,
the Verimag V6, or the Scade compiler (The same holds for C files).
Users can specify the compiler mode using the combo boxes at the
rigth-hand-side of the node names (cf,
Figure~\ref{main-window-part}). They can choose between:
\begin{itemize}
\item {\tt lv4}
\item {\tt lv6}
\item {\tt scade}
\item {\tt ocaml}
\item {\tt stdin/stdout}
\end{itemize}
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
execution mode. In this mode, users do not specify a SUT/oracle file
and node name, but a system call that launches a program that
reads/writes its input/output on the standard input/output
(stdin/stdout). The inputs must follow the RIF convention
(cf~Appendix\ref{rif}), and the outputs will.
%
For example, one can enter the string {\tt "ecexe heater\_control.ec"},
because the{\tt ecexe} ec files interpreter reads and writes data
on stdin/stdout following the RIF conventions.
\paragraph{Watch out:} in the {\tt verimag} and {\tt scade} modes,
the link between the SUT, the environment and the oracle is done via
{\bf variable names}, whereas in the {\tt stdin/stdout} mode, it is done
via the {\bf variable positions} of their declaration in the
interface.
More details on the different compiling modes can be found in
Sections~\ref{lustre-mode}, ~\ref{c-mode}, ~\ref{ocaml-mode},
and~\ref{stdin-mode}.
%
Note also that the test thickness parameters (cf
\ref{test-thickness}) are (currently) ignored in the {\tt
stdin/stdout} mode.
\subsubsection{The Extra Environment variables window}
\label{extra-var-window}
One can launch the ``Extra Environment Parameters'' window by
clicking on the button just below the oracle line. A snapshot of
......@@ -573,10 +553,10 @@ are used in the Makefile that builds the final test executable.
\begin{itemize}
\item {\tt EXTRA\_CFILES} lets one add C files. For example, the
\item {\tt EXTRA\_SOURCE\_FILES} lets one add C files. For example, the
scade compiler sometimes generates a file named {\tt
<sut>\_const.c} that contains the definitions of the some of the
SUT constants. C files appearing in {\tt EXTRA\_CFILES} are
SUT constants. C files appearing in {\tt EXTRA\_SOURCE\_FILES} are
compiled and linked with the SUT by lurette.
\item {\tt EXTRA\_LIBS} lets one add libraries ({\tt <file>.a}).
\item {\tt EXTRA\_LIBDIRS} lets one add paths to directories containing librairies.
......@@ -593,7 +573,7 @@ For all those environment variables, one can put several items
\subsection{The Test Parameters window}
\subsection{The XLurette Test parameters window}
The ``Test Parameters window'' lets one set additional parameters;
one can launch it by clicking on the
......@@ -742,46 +722,160 @@ It is the first part of the RIF (see~\ref{rif}) file name used to
test length.
%--------------------------------------------------------------------
%--------------------------------------------------------------------
\newpage
\section{Supported Architectures and languages}
\label{supported-arch}
\subsection{Testing Lustre or Scade Programs}
\label{lustre-mode}
Lurette has been tested with the following architectures:
In order to test lustre programs, one needs to specify which compiler
should be used (cf Section~\ref{compiling-mode}). For the time being,
3 lustre compilers are supported: the Verimag Lustre V4 compiler
(lv4); the the Verimag Lustre V6 compiler (lv6); the
Esterel-Technologies Lustre compiler (scade). In the scade mode, one
can also test Scade (.saofdm) programs.
Note that a different compiling mode might be used for the oracle;
but not all the combinations are supported. More precisely,
\begin{itemize}
\item Ultra-sparc machine running Solaris 2.8;
\item i686 running Linux;
\item i686 running WindowsNt and Cygwin.
\item lv4 and lv6 modes can be mixed arbitrarily
\item In the the scade mode for the SUT, the oracle can be lv4, lv6,
or scade
\item Otherwise, the SUT and the oracle compiling modes should be the same.
\end{itemize}
\subsection{Testing C Programs}
\label{c-mode}
The System Under Test can either be:
Since all lustre (and scade) compilers generates C code, any C code
that follows one of the lustre compilers convention can be used.
One's need to be very familiar with those conventions though.
\begin{itemize}
\item an academic Lustre program ({\tt .lus});
\item a Scade\footnote{only tested with the 4.2 version} program
({\tt .saofdm});
\item a C file, provided that it follows the Verimag~\cite{poc-man}
or the Scade code generators conventions.
\end{itemize}
\subsection{Testing OCaml Programs}
\label{ocaml-mode}
Is is also possible (since August 2010) to test ocaml programs using
Lurette. We suppose that readers are familiar with ocaml in this
section.
\paragraph{The SUT.}
If your SUT is in Ocaml, it must implement the following interface:
\begin{small}
\begin{example}
val init : unit -> unit
type var_type = string (* Should be "bool", "int", or "float" *)
val get_input_var_name_and_type : unit -> (string * var_type) list
val get_output_var_name_and_type : unit -> (string * var_type) list
val step : (string * Value.t) list -> (string, Value.t) Hashtbl.t
val step_try : (string * Value.t) list -> (string, Value.t) Hashtbl.t
\end{example}
\end{small}
Of course, the outputs of {\tt get\_input\_var\_name\_and\_type} and
{\tt get\_output\_var\_name\_and\_type} should be consistent with
{\tt step} and {\tt step\_try}, i.e. , the arity, and the variable
names and types should match.
{\tt step\_try} is supposed to save the current state of the SUT,
perform a {\tt step}, and restore the saved state. Hence {\tt step\_try}
is the same as {\tt step} for stateless programs.
\paragraph{The oracle.}
Similarly, oracles written in Ocaml must implement the following
interface:
\begin{small}
\begin{example}
val init : unit -> unit
type var_type = string
val get_input_var_name_and_type : unit -> (string * var_type) list
val get_output_var_name_and_type: unit -> (string * var_type) list
val step: (string * Value.t) list -> (string, Value.t) Hashtbl.t -> bool * Var.subst list
val step_try: (string * Value.t) list -> (string, Value.t) Hashtbl.t -> bool * Var.subst list
\end{example}
\end{small}
{\tt step} (and {\tt step\_try}) should return a pair made of the result
of the oracle (success or failure) and the list of oracle outputs.
Note that the oracle step takes as input the SUT inputs, and then the
SUT outputs. Hence you should make sure that the oracle inputs is
made of the SUT inputs and the SUT outputs. In other words, you
should satisfy the following assertion:
\begin{small}
\begin{example}
assert(
List.sort (compare)
(TheSut.get_input_var_name_and_type())@(TheSut.get_output_var_name_and_type())
=
List.sort (compare) (TheOracle.get_input_var_name_and_type ())
)
\end{example}
\end{small}
\paragraph{nb.}
Like in other modes, if our ocaml programs is splited into several
files, or if its uses libraries, one need to set appropriately the
parameters in the \emph{Extra Environment variables window} (cf
Section~\ref{extra-var-window}).
\subsection{Testing any Programs (using stdin/stdout and RIF conventions)}
\label{stdin-mode}
There exists a versatile (and rather experimental) mode, that is
language-agnostic. It can test any (executable) programs that reads
and writes its IO on its standard inputs and outputs using the RIF
conventions (cf Appendix~\ref{rif}). In this mode, lurette will
launch a system call using the string written in the SUT (and the
oracle) box. It can be a command with parameters.
Note that the SUT and the oracle can be in C (provided that they
follow the poc or the scade conventions), but the SUT environment
descriptions needs to be in Lutin, Lustre, or Lucky. Indeed, in
the Lurette testing process, the SUT and the oracle just need to be
compiled and executed, whereas the environment description needs to
be parsed and interpreted.
For example, one can write {\tt "ecexe heater\_control.ec"} in the
SUT box. Indeed, the {\tt ecexe} ec files interpreter (present in the
Lustre V4 distribution) reads and writes data on stdin/stdout
following the RIF conventions.
%
If you have a data file that follows the RIF convention, something
like {\tt "cat my\_data\_file.rif"} ougth to work also.
\paragraph{Watch out:} the {\tt stdin/stdout} mode,
the link between the SUT, the environment and the oracle is done by
{\bf variable positions}, whereas it is done by {\bf variable names}
in all the other modes.
Note also that the test thickness parameters (cf
\ref{test-thickness}) are (currently) ignored in this mode.
%--------------------------------------------------------------------
%--------------------------------------------------------------------
\newpage
\section{Installation and configuration issues}
\subsection{Installation and configuration issues}
\label{install}
\label{supported-arch}
Lurette has been tested with the following architectures:
\begin{itemize}
\item Solaris/Sparc.
\item Linux/PC.
\item Windows/PC.
\item Mac os/PC and powermac.
\end{itemize}
In order to use Lurette, you need
\begin{itemize}
......@@ -878,6 +972,7 @@ explicitely specify the full path of tools that are used by Lurette.
%--------------------------------------------------------------------
%--------------------------------------------------------------------
\newpage
\input{fault-tolerant-tut}
......
LUTINSRC=../../source/Lutin
SRCS=./src/commands.tex \
./src/language.tex \
./src/lutsyntax.tex \
./src/semantics.tex \
SRCS=./commands.tex \
./language.tex \
./lutsyntax.tex \
./semantics.tex \
./objs/lutyacc.tex \
./objs/version.tex \
./src/main.tex \
./main.tex \
all: lutin-man.pdf
......@@ -34,5 +34,5 @@ clean:
rm -f ./objs/*
re:
touch $(LUTINSRC)/lutParser.mly
touch src/*
touch *.tex
make
LTOP=../../../$(HOST_TYPE)/bin/lurettetop
LURETTETOP=$(LTOP) --precision 2 --sut sut.ml \
LURETTETOP=$(LTOP) --precision 2 --sut heat_ctrl.ml \
--sut-compiler ocaml \
--oracle-compiler ocaml --oracle oracle.ml \
--oracle-compiler ocaml --oracle not_a_sauna.ml \
--test-length 500 --thick-draw 1 \
--draw-inside 0 --draw-edges 0 --draw-vertices 0 --draw-all-vertices \
--step-mode Inside --local-var --no-sim2chro --seed 3 \
......@@ -27,7 +27,7 @@ utest:
clean:
rm -rf *.ec *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp
rm -rf *.ec *.cm* *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp
......
(* Time-stamp: <modified the 13/07/2010 (at 15:47) by Erwan Jahier> *)
(* Time-stamp: <modified the 18/08/2010 (at 11:02) by Erwan Jahier> *)
......@@ -6,14 +6,14 @@ let init _ = ()
let pre_res = ref false
type str_type = string
(* An str_type can be "bool", "int", or "float" *)
type var_type = string
(* An var_type can be "bool", "int", or "float" *)
let (get_input_var_name_and_type : unit -> (string * str_type) list) =
let (get_input_var_name_and_type : unit -> (string * var_type) list) =
fun () -> ["T", "float"; "T1", "float"; "T2", "float"; "T3", "float"]
let (get_output_var_name_and_type : unit -> (string * str_type) list) =
let (get_output_var_name_and_type : unit -> (string * var_type) list) =
fun () -> ["Heat_on", "bool"]
......@@ -34,22 +34,13 @@ let (step : (string * Value.t) list -> (string, Value.t) Hashtbl.t) =
Hashtbl.replace tbl "Heat_on" (B(res));
tbl
(* Trie save the current state of the SUT, perfoms a step, and restore the saved state
nb : i cannot call it try, it is an ocaml kwd ... *)
let (trie : (string * Value.t) list -> (string, Value.t) Hashtbl.t)=
let (step_try : (string * Value.t) list -> (string, Value.t) Hashtbl.t)=
fun l ->
step l
(** Where module Value is defined as follows:
(** Where module Value defines the following types:
type num = I of int | F of float
type t = B of bool | N of num
......
(* Time-stamp: <modified the 13/07/2010 (at 15:49) by Erwan Jahier> *)
(* Time-stamp: <modified the 18/08/2010 (at 11:02) by Erwan Jahier> *)
let init _ = ()
type str_type = string
(* An str_type can be "bool", "int", or "float" *)
type var_type = string
(* An var_type can be "bool", "int", or "float" *)
let (get_input_var_name_and_type : unit -> (string * str_type) list) =
let (get_input_var_name_and_type : unit -> (string * var_type) list) =
fun () -> ["T", "float"; "T1", "float"; "T2", "float"; "T3", "float";"Heat_on", "bool"]
let (get_output_var_name_and_type : unit -> (string * str_type) list) =
let (get_output_var_name_and_type : unit -> (string * var_type) list) =
fun () -> ["ok", "bool"]
......@@ -36,9 +36,6 @@ let (step : (string * Value.t) list -> (string, Value.t) Hashtbl.t -> bool* Va
in
ok, ["ok", (B(ok))]
(* Trie save the current state of the SUT, perfoms a step, and restore the saved state
nb : i cannot call it try, it is an ocaml kwd ... *)
let (trie : (string * Value.t) list -> (string, Value.t) Hashtbl.t -> bool* Var.subst list)=
let (step_try : (string * Value.t) list -> (string, Value.t) Hashtbl.t -> bool* Var.subst list)=
fun inputs outputs ->
step inputs outputs
......@@ -10,7 +10,7 @@
# SUT, SUT_DIR, ORACLE, ORACLE_DIR, LURETTE_TMP_DIR,
# USER_TESTING_DIR, are set up by by xlurette (via lurettetop)
#
# EXTRA_LIBS, EXTRA_LIBDIRS, EXTRA_INCLUDEDIRS, and EXTRA_CFILES
# EXTRA_LIBS, EXTRA_LIBDIRS, EXTRA_INCLUDEDIRS, and EXTRA_SOURCE_FILES
# are set up by xlurette or in the user env: can be used by
# lurette users to add their owns libs for their applications.
......@@ -51,7 +51,7 @@ ifeq ($(ORACLE), "")
PATH_ORACLE =
endif
SOURCES_C = $(EXTRA_CFILES) $(SUT_DIR)/$(SUT).c lurette__sut.c \
SOURCES_C = $(EXTRA_SOURCE_FILES) $(SUT_DIR)/$(SUT).c lurette__sut.c \
$(PATH_ORACLE) $(LURETTE_TMP_DIR)/lurette__oracle.c
......@@ -86,29 +86,38 @@ all: nc
# Ocaml
sut.ml:
cp $(USER_TESTING_DIR)/sut.ml .
$(SUT):$(USER_TESTING_DIR)/$(SUT)
ifdef SUT
cp $(USER_TESTING_DIR)/$(SUT) .
endif
sut.mli:
cp $(LURETTE_PATH)/lib/sut.mli .
oracle.ml:
cp $(USER_TESTING_DIR)/oracle.ml .
$(ORACLE):$(USER_TESTING_DIR)/$(ORACLE)
ifdef ORACLE
cp $(USER_TESTING_DIR)/$(ORACLE) $(LURETTE_TMP_DIR)
endif
sut.mli:
cp $(LURETTE_PATH)/lib/sut.mli .
oracle.mli:
cp $(LURETTE_PATH)/lib/oracle.mli .
SOURCES_ML = oracle.mli oracle.ml sut.mli sut.ml $(EXTRA_ML_FILES)
SOURCES_ML = $(EXTRA_SOURCE_FILES) $(SUT) $(ORACLE) sut.ml oracle.ml oracle.mli sut.mli
ocaml: sut.ml sut.mli oracle.ml oracle.mli
ocaml: sut.ml sut.mli oracle.ml oracle.mli $(SUT) $(ORACLE)
ocamlopt.opt \
-I $(LURETTE_PATH)/lib \
-ccopt -L $(LURETTE_PATH)/lib \
-I /home/jahier/lurette/i386-linux-gcc3/lib \
-ccopt -L/home/jahier/lurette/i386-linux-gcc3/lib \
$(EXTRA_INCLUDEDIRS) \
$(EXTRA_LIBSDIRS) \
$(EXTRA_LIBS) \
str.cmxa unix.cmxa nums.cmxa polka.cmxa bdd.cmxa \
$(SOURCES_ML) lurette_ml_exec.cmxa $(LURETTE_PATH)/lib/lurette_exec.ml \
-o lurette
-o lurette
##############################################################################
#
......@@ -192,7 +201,7 @@ $(NODE_OBJECTS)/memories.o: $(LURETTE_TMP_DIR)/memories.c
scade: $(NODE_OBJ)
$(CC) $(DEBUG) $(SCADE_LIB_DIRS) $(SCADE_INCLUDE_DIRS) $(NODE_OBJ) $(LDFLAGS) \
$(LIB_GC) $(LIB_OS) $(EXTRA_CFILES) -llurette_nc -llucky_nc $(LIBS) -o lurette
$(LIB_GC) $(LIB_OS) $(EXTRA_SOURCE_FILES) -llurette_nc -llucky_nc $(LIBS) -o lurette
##############################################################################
#
......@@ -212,7 +221,7 @@ ifndef SILDEXCC
SILDEXCC := gcc
endif
SILDEX_SOURCES_C = $(EXTRA_CFILES)
SILDEX_SOURCES_C = $(EXTRA_SOURCE_FILES)
SILDEX_OBJECT_FILES = $(LURETTE_TMP_DIR)/$(HOST_TYPE)/lurette__sut.o \
$(LURETTE_TMP_DIR)/$(HOST_TYPE)/lurette__oracle.o
......
......@@ -238,7 +238,62 @@ let (my_create_process : string -> string list -> in_channel -> out_channel ->
output_string oc (Printexc.to_string e);
flush oc;
false
(**************************************************************************)
(* The xlurette ocaml mode requires the "sut.ml" and "oracle.ml" files
to be defined. *)
let (get_ocaml_glue : string -> string) =
fun src_name ->
("
type var_type = string
let init = " ^ src_name ^ ".init
let get_input_var_name_and_type = " ^ src_name ^ ".get_input_var_name_and_type
let get_output_var_name_and_type = " ^ src_name ^ ".get_output_var_name_and_type
let step = " ^ src_name ^ ".step
let trie = " ^ src_name ^ ".step_try
")
let (gen_ocaml_glue : string -> string -> unit) =
fun user_ocaml_module target ->
let code = get_ocaml_glue user_ocaml_module in
let oc = open_out target in
let put s = output_string oc s in
put "(* Automatically generated by xlurette from ";
put user_ocaml_module;
put " *)";
put code;
close_out oc
let (gen_ocaml_sut : string -> unit) =
fun user_ocaml_module ->
let file = Filename.concat flag.tmp_dir "sut.ml" in
gen_ocaml_glue user_ocaml_module file