Commit 1eb78afa authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Add the possibility to call caml programs from lurette (via Dynlink).

parent 7bb02d3b
export OCAMLOPT=ocamlopt
LTOP=../../../$(HOSTTYPE)/bin/lurettetop
LIB=../../../$(HOSTTYPE)/lib
LURETTETOP=$(LTOP) --precision 2 --sut heat_ctrl.ml \
--sut-compiler ocaml \
--oracle-compiler ocaml --oracle not_a_sauna.ml \
......@@ -8,29 +9,47 @@ LURETTETOP=$(LTOP) --precision 2 --sut heat_ctrl.ml \
--step-mode Inside --local-var --no-sim2chro --seed 3 \
--do-not-show-step --old-mode
# XXX make it work!
test1:
rm -f test1.rif0 .lurette_rc
$(LURETTETOP) -go --output test1.rif0 sensors.luc && \
grep -v "lurette chronogram" test1.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test1.rif &&\
rm -f test1.res && diff -u -i test1.rif.exp test1.rif > test1.res
[ ! -s test1.res ] && make clean
#
NEW_LURETTETOP=$(LTOP) --precision 2 \
-rp "sut:ocaml:heat_ctrl.ml:" \
-rp "oracle:ocaml:not_a_sauna.ml:" \
-rp "env:lutin:env.lut:main" \
--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 \
--do-not-show-step
%.cmxs: %.ml
ocamlopt -shared -o $*.cmxs -I $(LIB) ocamlRM.cmx rif_base.cmx $*.ml
test2: heat_ctrl2.cmxs
rm -f test2.rif0 .lurette_rc
$(NEW_LURETTETOP) -go --output test2.rif0 \
-rp "sut:ocaml:heat_ctrl2.cmxs:" \
-rp "env:lutin:sensors.lut:main" && \
grep -v "lurette chronogram" test2.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test2.rif &&\
rm -f test2.res && diff -u -i test2.rif.exp test2.rif > test2.res
[ ! -s test2.res ] && make clean
test:
rm -f test.rif0 .lurette_rc
$(LURETTETOP) -go --output test.rif0 sensors.luc && \
grep -v "lurette chronogram" test.rif0 | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif &&\
rm -f test.res && diff -u -i test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
test: test1 test2
utest: utest1 utest2
utest:
cp test.rif test.rif.exp
utest1:
cp test1.rif test1.rif.exp
utest2:
cp test2.rif test2.rif.exp
......
XXX OUT OF DATE !!!
An example illustrating the use of lurette on ocaml programs.
The idea is that not all all ocaml programs can be tested via lurette:
......
open Rif_base
let (inputs :(string * string) list) = [
"T", "real";
"T1", "real";
"T2", "real";
"T3", "real"]
let (outputs :(string * string) list) = [
"Heat_on", "bool"]
let pre_res = ref false
let init _ = ()
let (step : Rif_base.subst list -> Rif_base.subst list)=
fun inputs ->
let res =
match inputs with
(_,F(f))::_ ->
if f > 9.0 then false else if f < 6.00 then true else !pre_res
| _ -> assert false
in
pre_res := res;
[ ("Heat_on", B(res)) ]
let _ =
OcamlRM.add_inputs "heat_ctrl2.cmxs" inputs;
OcamlRM.add_outputs "heat_ctrl2.cmxs" outputs;
OcamlRM.add_init "heat_ctrl2.cmxs" init;
OcamlRM.add_step "heat_ctrl2.cmxs" step
let between(x, min, max : real) : bool =
((min < x) and (x < max))
let abs(x : real) : real =
if x > 0.0 then x else -x
node toto(t:real) returns ( y:real [ -1e50 ; 1e50]) =
loop {y = t}
node main(Heat_on : bool) returns (
T : real;
T1 : real;
T2 : real;
T3 : real) =
assert abs(T-T1) < 0.5 in
assert abs(T-T2) < 0.5 in
assert abs(T-T3) < 0.5 in
between(T, 6.0, 9.0)
fby
assert (abs(T - pre T) < 1.0 ) in
loop
{ if Heat_on then T >= pre T else T <= pre T }
This diff is collapsed.
......@@ -23,7 +23,7 @@ endif
CC= $(GCC) $(DWIN32)
LIBS = unix str nums polka bdd
LIBS = unix dynlink str nums polka bdd
CLIBS = camlidl $(CLIBS_WIN32) bdd_stubs
#USE_CAMLP4 = yes
......@@ -39,6 +39,8 @@ SOURCES = $(LUTIN_SOURCES) \
$(OBJDIR)/ltopArg.ml \
$(OBJDIR)/lutinRun.mli \
$(OBJDIR)/lutinRun.ml \
$(OBJDIR)/ocamlRM.mli \
$(OBJDIR)/ocamlRM.ml \
$(OBJDIR)/lustreRun.mli \
$(OBJDIR)/lustreRun.ml \
$(OBJDIR)/ocaml.mli \
......
......@@ -68,7 +68,7 @@ let (f : LtopArg.t -> bool) =
| VerimagV6, VerimagV4 -> make_rule
| VerimagV6, VerimagV6 -> make_rule
| VerimagV4, VerimagV4 -> make_rule
| Ocaml, Ocaml -> "ocaml"
| Ocamlopt, Ocamlopt -> "ocaml"
| Sildex, VerimagV4 -> "sildex_sut"
| VerimagV4, Sildex -> "sildex_oracle"
| Sildex, Sildex -> "sildex_both"
......@@ -98,14 +98,14 @@ let (f : LtopArg.t -> bool) =
in
Unix.chdir args.tmp_dir;
putenv "SUT_DIR" args.tmp_dir;
if args.sut_compiler = Ocaml
if args.sut_compiler = Ocamlopt
then putenv "SUT" args.sut
else putenv "SUT" sut_node;
putenv "ENV" args.env;
(match args.pp with None -> () |
Some pp -> putenv "PP" ("-pp "^ (pp)));
putenv "ORACLE_DIR" oracle_dir;
if args.oracle_compiler = Ocaml then
if args.oracle_compiler = Ocamlopt then
(match args.oracle with
None-> ()
| Some str -> putenv "ORACLE" str)
......@@ -114,7 +114,7 @@ let (f : LtopArg.t -> bool) =
putenv "USER_TESTING_DIR" (args.sut_dir);
putenv "LURETTE_TMP_DIR" (args.tmp_dir);
if args.sut_compiler = Ocaml then (
if args.sut_compiler = Ocamlopt then (
let ocaml_module =
Filename.basename (chop_ext args.sut) in
let ocaml_module = String.capitalize ocaml_module in
......@@ -124,7 +124,7 @@ let (f : LtopArg.t -> bool) =
Ocaml.gen_ocaml_sut ocaml_module
);
(match args.oracle_compiler, args.oracle with
| Ocaml, Some oracle ->
| Ocamlopt, Some oracle ->
let ocaml_module = Filename.basename (chop_ext oracle) in
let ocaml_module = String.capitalize ocaml_module in
if ocaml_module = "Oracle" then
......@@ -132,13 +132,13 @@ let (f : LtopArg.t -> bool) =
"*** You cannot name your oracle 'oracle.ml', please rename it.\n"
else
Ocaml.gen_ocaml_oracle ocaml_module
| Ocaml, None ->
| Ocamlopt, None ->
Ocaml.gen_fake_ocaml_oracle ()
| _,_ -> ()
);
if
if args.sut_compiler <> Ocaml then (
if args.sut_compiler <> Ocamlopt then (
not (ExtTools.gen_stubs (Filename.concat args.sut_dir args.sut) sut_node
(if oracle = "" then "" else oracle)
(if oracle = "" then "" else oracle_node)
......
......@@ -14,19 +14,25 @@ launch 'lurettetop --help' to see the available options.
let rp_help ="
To specify a reactive program to be used in the test session, one should
use a string with the following format: \"machine_kind:compiler:file:node\"
use a string with the following format: \"machine_kind:language:file:node\"
where:
- machine_kind can be : 'sut', 'oracle', or 'env'
- compiler can be :
+ 'v4' to use the Lustre V4 compiler
+ 'v6' to use the Lustre V6 compiler
+ 'lutin' to use the Lutin interpreter
+ 'ec' to use the ecexe interpreter
+ 'ec_exe' to use a standalone executable obtained from an .ec file (*)
- language can be :
+ 'v4' to use the Lustre V4 programs
+ 'v6' to use the Lustre V6 programs
+ 'lutin' to use the Lutin programs
+ 'ocaml' to use the Ocaml programs [ocaml]
+ 'ec' to use the ec programs
+ 'ec_exe' to use a standalone executable obtained from an .ec file [ex_exe]
- file should be an existing file (compatible with the ''compiler'' field)
- node should be a node of file (if meaningful) or empty
(* ) In the 'ec_exe' mode, lurette suppose that 'file.ec' has been compiled
[ocaml] In the 'ocaml' mode, the file can be an f.ml file, or a f.cmxs file.
If an ml file is provided, lurettetop try to generate a cmxs file from it.
If your caml program depends on library, or on other files, please generate
the f.cmxs file by yourself (cf the ocaml documentation).
[ex_exe] In the 'ec_exe' mode, lurette suppose that 'file.ec' has been compiled
into an executable that is named 'file' (for instance, via ec2c -loop).
That executable must read/write its I/O using the RIF convention.
The rationale for that mode is to be able to deal with Lustre programs that
......@@ -59,7 +65,7 @@ let rp_help ="
(* compiler used to compiler sut and oracles *)
(* XXX obselete soon! *)
type compiler = VerimagV4 | VerimagV6 | Scade | ScadeGUI | Sildex | Stdin | Ocaml
type compiler = VerimagV4 | VerimagV6 | Scade | ScadeGUI | Sildex | Stdin | Ocamlopt
type step_mode = | Inside | Edges | Vertices
let step_mode_to_string = function
......@@ -80,7 +86,7 @@ type reactive_program =
| Lutin of string * string
| Socket of string * int
| SocketInit of string * int
(* | Ocaml of string *)
| Ocaml of string
let program_kind_of_string = function
| "sut" -> SUT
......@@ -372,6 +378,7 @@ let (parse_rp_string : string -> unit) =
| ["ec"; prog] -> LustreEc(prog)
| ["ec"; prog; _] -> LustreEc(prog)
| ["v4"; prog; node] -> LustreV4(prog, node)
| ["ocaml"; cmxs] -> Ocaml(cmxs)
| ["socket"; addr; port] -> Socket(addr, int_of_string port)
| ["socket_init"; addr; port] -> SocketInit(addr, int_of_string port)
| _ -> failwith ("*** Error: Unsupported kind of reactive program: \""
......@@ -406,7 +413,7 @@ let (string_to_compiler:string -> compiler option) =
| "stdin/stdout" -> Some Stdin
| "stdin" -> Some Stdin
| "Stdin" -> Some Stdin
| "ocaml" -> Some Ocaml
| "ocaml" -> Some Ocamlopt
| _ -> None
let (compiler_to_string : compiler -> string) =
......@@ -418,18 +425,7 @@ let (compiler_to_string : compiler -> string) =
| ScadeGUI -> "scade-gui"
| Sildex -> "sildex"
| Stdin -> "stdin"
| Ocaml -> "ocaml"
let (compiler_to_extension : compiler -> string) =
fun c ->
match c with
| 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? *)
| Stdin -> assert false
| Ocaml -> ".ml"
| Ocamlopt -> "ocaml"
(************************************************************************)
......
......@@ -99,7 +99,7 @@ let main_read_arg () =
| ScadeGUI
| Sildex
| Stdin
| Ocaml -> ()
| Ocamlopt -> ()
let _ = main_read_arg ()
......
......@@ -19,7 +19,7 @@ let (f : unit -> int) =
| Scade
| ScadeGUI
| Sildex
| Ocaml ->
| Ocamlopt ->
RunBin.f ()
)
with
......
......@@ -80,6 +80,7 @@ let (make_rp_list : reactive_program list ->
| LustreEcExe(prog) -> add_init [] (LustreRun.make_ec_exe prog)
| Socket(addr, port) -> add_init [] (LustreRun.make_socket addr port)
| SocketInit(addr, port) -> LustreRun.make_socket_init addr port
| Ocaml(cmxs) -> add_init [] (LustreRun.make_ocaml cmxs)
in
Util.list_split6 (List.map aux rpl)
......
......@@ -623,6 +623,10 @@ cp:
cp $(OBJDIR)/*lurette_ml_exec*a $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/lurette.cmi $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/oracle.cmi $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/rif_base.o $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/ocamlRM.o $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/rif_base.cm* $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/ocamlRM.cm* $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/sut.cmi $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/value.cmi $(LIB_INSTALL_DIR) ;\
cp $(OBJDIR)/var.cmi $(LIB_INSTALL_DIR) ;\
......
......@@ -368,6 +368,13 @@ let (make_luciole : string -> vars -> vars ->
in
kill, step
(**********************************************************************************)
let (make_dro : string -> vars * vars *
(string -> unit) * (Rif_base.subst list -> Rif_base.subst list)) =
fun dro ->
assert false
(* finish me *)
(**********************************************************************************)
(* class type ocaml_reactive_machine = *)
......@@ -377,12 +384,18 @@ let (make_luciole : string -> vars -> vars ->
(* end;; *)
let (make_ocaml : string ->
let (make_ocaml : string -> vars * vars *
(string -> unit) * (Rif_base.subst list -> Rif_base.subst list)) =
fun mlprog ->
fun cmxs ->
Dynlink.loadfile cmxs ;
(
OcamlRM.get_inputs cmxs,
OcamlRM.get_outputs cmxs,
OcamlRM.get_init cmxs,
OcamlRM.get_step cmxs
)
(* cf
http://blog.rastageeks.org/ocaml/article/dynlink-as-dlopen
http://okmij.org/ftp/ML/first-class-modules/
*)
assert false
......@@ -66,5 +66,6 @@ val make_socket_init : string -> int ->
val make_luciole : string -> vars -> vars ->
(string -> unit) * (Rif_base.subst list -> Rif_base.subst list)
val make_ocaml : string -> (string -> unit) * (Rif_base.subst list -> Rif_base.subst list)
val make_ocaml : string -> vars * vars *
(string -> unit) * (Rif_base.subst list -> Rif_base.subst list)
type t = {
inputs : (string, (string * string) list) Hashtbl.t;
outputs : (string, (string * string) list) Hashtbl.t;
init : (string, (string -> unit)) Hashtbl.t;
step : (string, (Rif_base.subst list -> Rif_base.subst list)) Hashtbl.t;
}
let it = {
inputs = Hashtbl.create 1;
outputs = Hashtbl.create 1;
init = Hashtbl.create 1;
step = Hashtbl.create 1;
}
let (add_inputs : string -> (string * string) list -> unit) =
fun cmxs l ->
Hashtbl.add it.inputs cmxs l
let (get_inputs : string -> (string * string) list) =
fun cmxs ->
Hashtbl.find it.inputs cmxs
let (add_outputs : string -> (string * string) list -> unit) =
fun cmxs l ->
Hashtbl.add it.outputs cmxs l
let (get_outputs : string -> (string * string) list) =
fun cmxs ->
Hashtbl.find it.outputs cmxs
let (add_init : string -> (string -> unit) -> unit) =
fun cmxs l ->
Hashtbl.add it.init cmxs l
let (get_init : string -> (string -> unit)) =
fun cmxs ->
Hashtbl.find it.init cmxs
let (add_step : string -> (Rif_base.subst list -> Rif_base.subst list) -> unit) =
fun cmxs l ->
Hashtbl.add it.step cmxs l
let (get_step : string -> (Rif_base.subst list -> Rif_base.subst list)) =
fun cmxs ->
Hashtbl.find it.step cmxs
val add_inputs : string -> (string * string) list -> unit
val get_inputs : string -> (string * string) list
val add_outputs : string -> (string * string) list -> unit
val get_outputs : string -> (string * string) list
val add_init : string -> (string -> unit) -> unit
val get_init : string -> (string -> unit)
val add_step : string -> (Rif_base.subst list -> Rif_base.subst list) -> unit
val get_step : string -> (Rif_base.subst list -> Rif_base.subst list)
......@@ -8,7 +8,7 @@ include $(LURETTE_PATH)/source/Makefile.ln
OCAMLNCFLAGS = -inline 10
LIBS = unix str
LIBS = unix str dynlink
CLIBS =
USE_CAMLP4 = yes
......@@ -32,6 +32,8 @@ SOURCES_OCAML = \
$(OBJDIR)/coverage.ml \
$(OBJDIR)/luciole.mli \
$(OBJDIR)/luciole.ml \
$(OBJDIR)/ocamlRM.mli \
$(OBJDIR)/ocamlRM.ml \
$(OBJDIR)/lustreRun.mli \
$(OBJDIR)/lustreRun.ml \
$(OBJDIR)/checkRif.ml
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment