From ad4774b0ab1728d9b99aba1c40b7d770eb955fb5 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Wed, 14 Mar 2018 16:07:48 -0700
Subject: [PATCH] - Normalization parameters (alias and unfold_array) are now
provided as parameter - program type renamed as program_t - Initiating the
lustrev tool with dependencies to z3 and seal.
---
Makefile.in | 6 +-
configure.ac | 54 +++++-
src/Makefile.in | 10 +-
src/_tags.in | 10 +-
src/algebraicLoop.ml | 5 +-
src/backends/backends.ml | 25 +++
src/compiler_stages.ml | 10 +-
src/corelang.mli | 18 +-
src/lustreSpec.ml | 2 +-
src/main_lustre_compiler.ml | 4 +-
src/main_lustre_testgen.ml | 6 +-
src/main_lustre_verifier.ml | 135 +++++++++++++
src/normalization.ml | 62 +++---
src/options_management.ml | 11 ++
src/pluginList.ml.in | 2 +-
src/pluginType.ml | 2 +-
src/plugins.ml | 14 +-
src/plugins/salsa/salsa_plugin.ml | 2 +-
src/plugins/scopes/scopes.ml | 2 +-
src/tools/seal_verifier.ml | 13 ++
.../semantics/cPS_lustre_generator.ml | 2 +-
.../stateflow/semantics/cPS_transformer.ml | 4 +-
src/tools/stateflow/sf_sem.ml | 5 +-
src/tools/zustre_verifier.ml | 181 ++++++++++++++++++
src/verifierList.ml.in | 6 +
src/verifierType.ml | 20 ++
src/verifiers.ml | 48 +++++
27 files changed, 579 insertions(+), 80 deletions(-)
create mode 100644 src/main_lustre_verifier.ml
create mode 100644 src/tools/seal_verifier.ml
create mode 100644 src/tools/zustre_verifier.ml
create mode 100644 src/verifierList.ml.in
create mode 100644 src/verifierType.ml
create mode 100644 src/verifiers.ml
diff --git a/Makefile.in b/Makefile.in
index fe82f551..d26bfde0 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -8,7 +8,7 @@ LUSI_LIBS=include/lustrec_math.lusi include/simulink_math_fcn.lusi include/conv.
LUSI_MPFR_LIB=include/mpfr_lustre.lusi
LOCAL_BINDIR=bin
LOCAL_DOCDIR=doc/manual
-BIN_TARGETS = lustrec lustret @lustresf_target@
+BIN_TARGETS = lustrec lustret lustrev @lustresf_target@
DEFAULT_TEST_TARGET=COMPIL_LUS\|MAKE\|BIN\|DIFF
DEFAULT_EXCLUDE_TEST=LUSTRET
@@ -23,6 +23,10 @@ lustret:
@echo Compiling binary lustret
@make -C src lustret
+lustrev:
+ @echo Compiling binary lustrev
+ @make -C src lustrev
+
@lustresf@
configure: configure.ac
diff --git a/configure.ac b/configure.ac
index c918eba7..5a253935 100644
--- a/configure.ac
+++ b/configure.ac
@@ -55,7 +55,7 @@ dnl AC_MSG_RESULT(Hourrah: ocamlfind found!)
# Checks for libraries.
# OCamlgraph
-AC_MSG_CHECKING(ocaml libraries required)
+AC_MSG_CHECKING(ocaml libraries required (ocamlgraph cmdliner fmt logs num))
AS_IF([ocamlfind query ocamlgraph cmdliner fmt logs num >/dev/null 2>&1],
[],[AC_MSG_ERROR(A few ocaml library required. opam install ocamlgraph cmdliner fmt logs num should solve the issue)],
)
@@ -67,6 +67,36 @@ AS_IF([ocamlfind query yojson >/dev/null 2>&1],
[yojson=yes; AC_MSG_RESULT(yes)],[yojson=no; AC_MSG_WARN(Yojson required for lustresf. opam install yojson should solve the issue)],
)
+# Seal
+AC_MSG_CHECKING(seal library (optional))
+AS_IF([ocamlfind query seal >/dev/null 2>&1],
+ [seal=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
+)
+AS_IF([test "x$seal" = "xyes"], [
+ AC_SUBST(LUSTREV_SEAL, "(module Seal_verifier.Verifier : VerifierType.S);")
+ AC_SUBST(LUSTREV_SEAL_TAG, "<**/*>: package(seal)")
+])
+
+# z3
+AC_MSG_CHECKING(z3 library (optional))
+AS_IF([ocamlfind query z3 >/dev/null 2>&1],
+ [z3=yes; AC_MSG_RESULT(yes)],[seal=no; AC_MSG_RESULT(no)],
+)
+AS_IF([test "x$z3" = "xyes"], [
+ AC_SUBST(LUSTREV_ZUSTRE, "(module Zustre_verifier.Verifier : VerifierType.S);")
+ AC_SUBST(LUSTREV_Z3_TAG, "<**/*>: package(z3)")
+])
+
+# Tiny
+AC_MSG_CHECKING(tiny library (optional))
+AS_IF([ocamlfind query tiny >/dev/null 2>&1],
+ [tiny=yes; AC_MSG_RESULT(yes)],[tiny=no; AC_MSG_RESULT(no)],
+)
+AS_IF([test "x$tiny" = "xyes"], [
+ AC_SUBST(LUSTREV_TINY, "(module Tiny_verifier.Verifier : VerifierType.S);")
+ AC_SUBST(LUSTREV_TINY_TAG, "<**/*>: package(tiny)")
+])
+
# Salsa
AC_ARG_ENABLE(salsa, [AS_HELP_STRING([--disable-salsa],
[disable Salsa plugin. Enabled by default if available.])])
@@ -79,7 +109,7 @@ AS_IF([ocamlfind query salsa >/dev/null 2>&1],
AS_IF([test "x$enable_salsa" != "xno"], [
if (test "x$salsa" = xyes ); then
- AC_SUBST(SALSA, "(module Salsa_plugin.Plugin : PluginType.PluginType);")
+ AC_SUBST(SALSA, "(module Salsa_plugin.Plugin : PluginType.S);")
AC_SUBST(SALSA_TAG, "<**/*.native> or <plugins/salsa/*.cm?> : package(salsa)")
fi
])
@@ -156,6 +186,7 @@ AC_CONFIG_FILES([Makefile
src/Makefile
src/version.ml
src/pluginList.ml
+ src/verifierList.ml
src/_tags
src/ocaml_utils.ml
])
@@ -190,6 +221,25 @@ AC_MSG_NOTICE(******** Plugins ********)
AC_MSG_NOTICE([lustresf not available])
fi
fi
+AC_MSG_NOTICE(******** Verifiers ********)
+
+ if (test "x$seal" = "xyes"); then
+ AC_MSG_NOTICE([Seal enabled])
+ else
+ AC_MSG_NOTICE([Seal disabled. Require Seal library])
+ fi
+
+ if (test "x$z3" = xyes); then
+ AC_MSG_NOTICE([Zustre enabled])
+ else
+ AC_MSG_NOTICE([Zustre disabled. Require Z3 ocaml library])
+ fi
+
+ if (test "x$tiny" = xyes); then
+ AC_MSG_NOTICE([Tiny enabled])
+ else
+ AC_MSG_NOTICE([Tiny disabled. Require Tiny library])
+ fi
AC_MSG_NOTICE(****** Regression Tests ******)
if (test "x$valid_test_path" = xfalse); then
diff --git a/src/Makefile.in b/src/Makefile.in
index 59e3ce97..57be0099 100644
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -10,7 +10,7 @@ LUSI_LIBS=include/math.lusi include/conv.lusi
LOCAL_BINDIR=../bin
LOCAL_DOCDIR=../doc/manual
-all: lustrec lustret
+all: lustrec lustret lustrev
lustrec:
@echo Compiling binary lustrec
@@ -24,6 +24,12 @@ lustret:
@mkdir -p $(LOCAL_BINDIR)
@mv _build/main_lustre_testgen.native $(LOCAL_BINDIR)/lustret
+lustrev:
+ @echo Compiling binary lustrev
+ @$(OCAMLBUILD) main_lustre_verifier.native
+ @mkdir -p $(LOCAL_BINDIR)
+ @mv _build/main_lustre_verifier.native $(LOCAL_BINDIR)/lustrev
+
@lustresf_src@
doc:
@@ -47,4 +53,4 @@ dist-clean: clean
install:
make -C .. install
-.PHONY: compile-lusi doc dot lustrec lustret lustrec.odocl clean install dist-clean tests
+.PHONY: compile-lusi doc dot lustrec lustret lustrev lustrec.odocl clean install dist-clean tests
diff --git a/src/_tags.in b/src/_tags.in
index 7e6e8b8d..d91fd0d0 100644
--- a/src/_tags.in
+++ b/src/_tags.in
@@ -10,6 +10,7 @@ true: bin_annot, color(always)
"plugins/scopes": include
"plugins/mpfr": include
"features/machine_types": include
+"tools": include
"tools/stateflow": include
"tools/stateflow/common": include
"tools/stateflow/semantics": include
@@ -23,9 +24,7 @@ true: bin_annot, color(always)
# packages
<**/*.native> : package(ocamlgraph)
<**/*.native> : use_str
-<**/main_lustre_compiler.native>: use_unix
-<**/main_lustre_testgen.native> : use_unix
-<**/sf_sem.native> : use_unix
+<**/*.native> : use_unix
<**/*.native> : package(num)
<**/*.ml> : package(logs)
<**/*.native> : package(logs)
@@ -45,6 +44,11 @@ true: bin_annot, color(always)
# Plugin dependencies
@SALSA_TAG@
+# Available solvers
+@LUSTREV_SEAL_TAG@
+@LUSTREV_TINY_TAG@
+@LUSTREV_Z3_TAG@
+
# Local Variables:
# mode: conf
# End:
diff --git a/src/algebraicLoop.ml b/src/algebraicLoop.ml
index 36ca3590..66cc1f8d 100644
--- a/src/algebraicLoop.ml
+++ b/src/algebraicLoop.ml
@@ -157,7 +157,8 @@ let fast_stages_processing prog =
(* Clock calculus *)
let _ (*computed_clocks_env*) = Compiler_common.clock_decls clock_env prog in
(* Normalization *)
- let prog = Normalization.normalize_prog ~backend:!Options.output prog in
+ let params = Backends.get_normalization_params () in
+ let prog = Normalization.normalize_prog params prog in
(* Mini stage 2 : Scheduling *)
let res = Scheduling.schedule_prog prog in
Options.verbose_level := !Options.verbose_level + 2;
@@ -272,7 +273,7 @@ let rec solving_node max_inlines prog nd existing_al partitions =
Alarms contain the list of inlining performed or advised for each node.
This could be provided as a feedback to the user.
*)
-let clean_al prog : program * bool * report =
+let clean_al prog : program_t * bool * report =
let max_inlines = !Options.al_nb_max in
(* We iterate over each node *)
let _, prog, al_list =
diff --git a/src/backends/backends.ml b/src/backends/backends.ml
index 1fe68038..b0d4f817 100644
--- a/src/backends/backends.ml
+++ b/src/backends/backends.ml
@@ -16,6 +16,31 @@ let is_functional () =
| "horn" | "lustre" | "acsl" | "emf" -> true
| _ -> false
+
+(* Special treatment of arrows in lustre backend. We want to keep them *)
+let unfold_arrow () =
+ match !Options.output with
+ | "lustre" -> false
+ | _ -> true
+
+(* Forcing ite normalization *)
+let alias_ite () =
+ match !Options.output with
+ | "emf" -> true
+ | _ -> false
+
+(* Forcing basic functions normalization *)
+let alias_internal_fun () =
+ match !Options.output with
+ | "emf" -> true
+ | _ -> false
+
+let get_normalization_params () = {
+ Normalization.unfold_arrow_active = unfold_arrow ();
+ force_alias_ite = alias_ite ();
+ force_alias_internal_fun = alias_internal_fun ();
+ }
+
(* Local Variables: *)
(* compile-command: "make -k -C .." *)
diff --git a/src/compiler_stages.ml b/src/compiler_stages.ml
index dfc92c78..40e8945b 100644
--- a/src/compiler_stages.ml
+++ b/src/compiler_stages.ml
@@ -3,7 +3,7 @@ open Utils
open Compiler_common
open LustreSpec
-exception StopPhase1 of program
+exception StopPhase1 of program_t
let dynamic_checks () =
match !Options.output, !Options.spec with
@@ -22,7 +22,7 @@ let compile_source_to_header prog computed_types_env computed_clocks_env dirname
begin
Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
- Lusic.print_lusic_to_h destname lusic_ext
+ if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext
end
else
let lusic = Lusic.read_lusic destname lusic_ext in
@@ -31,7 +31,7 @@ let compile_source_to_header prog computed_types_env computed_clocks_env dirname
Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
(*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
- Lusic.print_lusic_to_h destname lusic_ext
+ if !Options.output = "C" then Lusic.print_lusic_to_h destname lusic_ext
end
else
begin
@@ -47,7 +47,7 @@ let compile_source_to_header prog computed_types_env computed_clocks_env dirname
(* From prog to prog *)
-let stage1 prog dirname basename =
+let stage1 params prog dirname basename =
(* Updating parent node information for variables *)
Compiler_common.update_vdecl_parents_prog prog;
@@ -175,7 +175,7 @@ let stage1 prog dirname basename =
(* Normalization phase *)
Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
- let prog = Normalization.normalize_prog ~backend:!Options.output prog in
+ let prog = Normalization.normalize_prog params prog in
Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
let prog =
diff --git a/src/corelang.mli b/src/corelang.mli
index da1f8161..70418e57 100755
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -110,9 +110,9 @@ val expr_to_eexpr: expr -> eexpr
val add_internal_funs: unit -> unit
-val pp_prog_type : Format.formatter -> program -> unit
+val pp_prog_type : Format.formatter -> program_t -> unit
-val pp_prog_clock : Format.formatter -> program -> unit
+val pp_prog_clock : Format.formatter -> program_t -> unit
val const_of_top: top_decl -> const_desc
val node_of_top: top_decl -> node_desc
@@ -120,12 +120,12 @@ val imported_node_of_top: top_decl -> imported_node_desc
val typedef_of_top: top_decl -> typedef_desc
val dependency_of_top: top_decl -> (bool * ident)
-val get_nodes : program -> top_decl list
-val get_imported_nodes : program -> top_decl list
-val get_consts : program -> top_decl list
-val get_typedefs: program -> top_decl list
-val get_dependencies : program -> top_decl list
-(* val prog_unfold_consts: program -> program *)
+val get_nodes : program_t -> top_decl list
+val get_imported_nodes : program_t -> top_decl list
+val get_consts : program_t -> top_decl list
+val get_typedefs: program_t -> top_decl list
+val get_dependencies : program_t -> top_decl list
+(* val prog_unfold_consts: program_t -> program_t *)
val rename_static: (ident -> Dimension.dim_expr) -> type_dec_desc -> type_dec_desc
val rename_carrier: (ident -> ident) -> clock_dec_desc -> clock_dec_desc
@@ -142,7 +142,7 @@ val rename_eq : (ident -> ident) -> (ident -> ident) -> eq -> eq
(** val rename_aut f_node f_var aut *)
val rename_aut : (ident -> ident) -> (ident -> ident) -> automata_desc -> automata_desc
(** rename_prog f_node f_var prog *)
-val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program -> program
+val rename_prog: (ident -> ident) -> (ident -> ident) -> (ident -> ident) -> program_t -> program_t
val substitute_expr: var_decl list -> eq list -> expr -> expr
diff --git a/src/lustreSpec.ml b/src/lustreSpec.ml
index e6f5ab2d..4fb08d08 100644
--- a/src/lustreSpec.ml
+++ b/src/lustreSpec.ml
@@ -211,7 +211,7 @@ type top_decl =
top_decl_itf: bool; (* header or source file ? *)
top_decl_loc: Location.t} (* the location where it is defined *)
-type program = top_decl list
+type program_t = top_decl list
type dep_t = Dep of
bool
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index 51af25f9..715b29ac 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -71,10 +71,12 @@ let rec compile_source dirname basename extension =
else
prog
in
+ let params = Backends.get_normalization_params () in
+
let prog, dependencies =
Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
try
- Compiler_stages.stage1 prog dirname basename
+ Compiler_stages.stage1 params prog dirname basename
with Compiler_stages.StopPhase1 prog -> (
if !Options.lusi then
begin
diff --git a/src/main_lustre_testgen.ml b/src/main_lustre_testgen.ml
index c872f2c4..aa247146 100644
--- a/src/main_lustre_testgen.ml
+++ b/src/main_lustre_testgen.ml
@@ -45,7 +45,8 @@ let testgen_source dirname basename extension =
(* Parsing source *)
let prog = parse_source source_name in
- let prog, dependencies = Compiler_stages.stage1 prog dirname basename in
+ let params = Backends.get_normalization_params () in
+ let prog, dependencies = Compiler_stages.stage1 params prog dirname basename in
(* Two cases
- generation of coverage conditions
@@ -73,7 +74,8 @@ let testgen_source dirname basename extension =
(2) produced as EMF
*)
Options.output := "emf";
- let prog_mcdc = Normalization.normalize_prog ~backend:"emf" prog_mcdc in
+ let params = Backends.get_normalization_params () in
+ let prog_mcdc = Normalization.normalize_prog params prog_mcdc in
let machine_code = Compiler_stages.stage2 prog_mcdc in
let source_emf = source_file ^ ".emf" in
let source_out = open_out source_emf in
diff --git a/src/main_lustre_verifier.ml b/src/main_lustre_verifier.ml
new file mode 100644
index 00000000..23f7eae2
--- /dev/null
+++ b/src/main_lustre_verifier.ml
@@ -0,0 +1,135 @@
+(********************************************************************)
+(* *)
+(* The LustreC compiler toolset / The LustreC Development Team *)
+(* Copyright 2012 - -- ONERA - CNRS - INPT *)
+(* *)
+(* LustreC is free software, distributed WITHOUT ANY WARRANTY *)
+(* under the terms of the GNU Lesser General Public License *)
+(* version 2.1. *)
+(* *)
+(********************************************************************)
+
+open Format
+open Log
+open Compiler_common
+
+open Utils
+open LustreSpec
+
+
+let usage = "Usage: lustrev [options] \x1b[4msource file\x1b[0m"
+
+let extensions = [".ec"; ".lus"; ".lusi"]
+
+
+(* verify a .lus source file
+
+we have multiple "backends"
+- zustre: linked to z3/spacer. Shall preserve the structure and rely on contracts. Produces both a lustre model with new properties, maybe as a lusi with lustre contract, and a JSON summarizing the results and providing tests cases or counter examples if any
+
+- seal: linked to seal. Require global inline and main node
+ focuses only on the selected node (the main)
+ map the machine code into SEAL datastructure and compute invariants
+ - provides the node and its information (typical point of interest for taylor expansion, range for inputs, existing invariants, computation error for the node content)
+ - simplification of program through taylor expansion
+ - scaling when provided with typical ranges (not required to be sound for the moment)
+ - computation of lyapunov invariants
+ - returns an annotated node with invariants and a JSON to explain computation
+ - could also returns plots
+
+- tiny: linked to tiny library to perform floating point analyses
+ shall be provided with ranges for inputs or local variables (memories)
+
+*)
+let rec verify dirname basename extension =
+ let source_name = dirname ^ "/" ^ basename ^ extension in
+
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");
+
+ (* Parsing source *)
+ let prog = parse_source source_name in
+
+ (* Checking which solver is active *)
+ let verifier = Verifiers.get_active () in
+ let module Verifier = (val verifier : VerifierType.S) in
+
+
+ (* Normalizing it *)
+ let prog, dependencies =
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
+ try
+ let params = Verifier.get_normalization_params () in
+ Compiler_stages.stage1 params prog dirname basename
+ with Compiler_stages.StopPhase1 prog -> (
+ assert false
+ )
+ in
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@]@,");
+ Log.report ~level:3 (fun fmt -> fprintf fmt ".. Normalized program:@ %a@ "Printers.pp_prog prog);
+
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
+
+ let machine_code =
+ Compiler_stages.stage2 prog
+ in
+
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
+ Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ "Machine_code.pp_machines machine_code);
+
+ if Scopes.Plugin.show_scopes () then
+ begin
+ let all_scopes = Scopes.compute_scopes prog !Options.main_node in
+ (* Printing scopes *)
+ if !Options.verbose_level >= 1 then
+ Format.printf "Possible scopes are:@ ";
+ Format.printf "@[<v>%a@ @]@ @?" Scopes.print_scopes all_scopes;
+ exit 0
+
+ end;
+
+ let machine_code = Plugins.refine_machine_code prog machine_code in
+
+ assert (dependencies = []); (* Do not handle deps yet *)
+ Verifier.run basename prog machine_code;
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
+ (* We stop the process here *)
+ exit 0
+ end
+
+
+let anonymous filename =
+ let ok_ext, ext = List.fold_left
+ (fun (ok, ext) ext' ->
+ if not ok && Filename.check_suffix filename ext' then
+ true, ext'
+ else
+ ok, ext)
+ (false, "") extensions in
+ if ok_ext then
+ let dirname = Filename.dirname filename in
+ let basename = Filename.chop_suffix (Filename.basename filename) ext in
+ verify dirname basename ext
+ else
+ raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
+
+let _ =
+ Global.initialize ();
+ Corelang.add_internal_funs ();
+ try
+ Printexc.record_backtrace true;
+
+ let options = Options_management.lustrev_options @ (Verifiers.options ()) in
+
+ Arg.parse options anonymous usage
+ with
+ | Parse.Error _
+ | Types.Error (_,_) | Clocks.Error (_,_) -> exit 1
+ | Corelang.Error (_ (* loc *), kind) (*| Task_set.Error _*) -> exit (Error.return_code kind)
+ (* | Causality.Error _ -> exit (Error.return_code Error.AlgebraicLoop) *)
+ | Sys_error msg -> (eprintf "Failure: %s@." msg); exit 1
+ | exc -> (track_exception (); raise exc)
+
+(* Local Variables: *)
+(* compile-command:"make -C .." *)
+(* End: *)
diff --git a/src/normalization.ml b/src/normalization.ml
index ef6048fd..3b0ac65c 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -29,10 +29,19 @@ open Format
definitions.
*)
-(* Two global variables *)
-let unfold_arrow_active = ref true
-let force_alias_ite = ref false
-let force_alias_internal_fun = ref false
+type param_t =
+ {
+ unfold_arrow_active: bool;
+ force_alias_ite: bool;
+ force_alias_internal_fun: bool;
+ }
+
+let params = ref
+ {
+ unfold_arrow_active = false;
+ force_alias_ite = false;
+ force_alias_internal_fun =false;
+ }
let expr_true loc ck =
@@ -230,7 +239,7 @@ let rec normalize_expr ?(alias=true) ?(alias_basic=false) node offsets defvars e
in
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
| Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr
- && not (!force_alias_internal_fun || alias_basic) ->
+ && not (!params.force_alias_internal_fun || alias_basic) ->
let defvars, norm_args = normalize_expr ~alias:true node offsets defvars args in
defvars, mk_norm_expr offsets expr (Expr_appl (id, norm_args, None))
| Expr_appl (id, args, r) ->
@@ -248,10 +257,10 @@ let rec normalize_expr ?(alias=true) ?(alias_basic=false) node offsets defvars e
let defvars, norm_expr = normalize_expr node [] defvars norm_expr in
normalize_expr ~alias:alias node offsets defvars norm_expr
else
- mk_expr_alias_opt (alias && (!force_alias_internal_fun || alias_basic
+ mk_expr_alias_opt (alias && (!params.force_alias_internal_fun || alias_basic
|| not (Basic_library.is_expr_internal_fun expr)))
node defvars norm_expr
- | Expr_arrow (e1,e2) when !unfold_arrow_active && not (is_expr_once expr) ->
+ | Expr_arrow (e1,e2) when !params.unfold_arrow_active && not (is_expr_once expr) ->
(* Here we differ from Colaco paper: arrows are pushed to the top *)
normalize_expr ~alias:alias node offsets defvars (unfold_arrow expr)
| Expr_arrow (e1,e2) ->
@@ -328,7 +337,7 @@ and normalize_cond_expr ?(alias=true) node offsets defvars expr =
| Expr_merge (c, hl) ->
let defvars, norm_hl = normalize_branches node offsets defvars hl in
defvars, mk_norm_expr offsets expr (Expr_merge (c, norm_hl))
- | _ when !force_alias_ite ->
+ | _ when !params.force_alias_ite ->
(* Forcing alias creation for then/else expressions *)
let defvars, norm_expr =
normalize_expr ~alias:alias node offsets defvars expr
@@ -506,34 +515,15 @@ let normalize_decl decl =
decl'
| Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
-let normalize_prog ?(backend="C") decls =
- let old_unfold_arrow_active = !unfold_arrow_active in
- let old_force_alias_ite = !force_alias_ite in
- let old_force_alias_internal_fun = !force_alias_internal_fun in
-
+let normalize_prog p decls =
(* Backend specific configurations for normalization *)
- let _ =
- match backend with
- | "lustre" ->
- (* Special treatment of arrows in lustre backend. We want to keep them *)
- unfold_arrow_active := false;
- | "emf" -> (
- (* Forcing ite normalization *)
- force_alias_ite := true;
- force_alias_internal_fun := true;
- )
- | _ -> () (* No fancy options for other backends *)
- in
+ params := p;
(* Main algorithm: iterates over nodes *)
- let res = List.map normalize_decl decls in
-
- (* Restoring previous settings *)
- unfold_arrow_active := old_unfold_arrow_active;
- force_alias_ite := old_force_alias_ite;
- force_alias_internal_fun := old_force_alias_internal_fun;
- res
-
- (* Local Variables: *)
-(* compile-command:"make -C .." *)
-(* End: *)
+ List.map normalize_decl decls
+
+
+ (* Local Variables: *)
+ (* compile-command:"make -C .." *)
+ (* End: *)
+
diff --git a/src/options_management.ml b/src/options_management.ml
index bdda79c7..2a13ae16 100644
--- a/src/options_management.ml
+++ b/src/options_management.ml
@@ -135,10 +135,21 @@ let lustret_options =
"-no-mutation-suffix", Arg.Set no_mutation_suffix, "does not rename node with the _mutant suffix"
]
+let lustrev_options =
+ common_options @
+ [
+ "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inlines all node calls (require a main node). Implies constant unfolding";
+ "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
+]
+
+
let plugin_opt (name, activate, options) =
( "-" ^ name , Arg.Unit activate, "activate plugin " ^ name ) ::
(List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)
+let verifier_opt (name, activate, options) =
+ ( "-" ^ name , Arg.Unit activate, "run verifier " ^ name ) ::
+ (List.map (fun (opt, act, desc) -> "-" ^ name ^ opt, act, desc) options)
let get_witness_dir filename =
(* Make sure the directory exists *)
diff --git a/src/pluginList.ml.in b/src/pluginList.ml.in
index e9aa0b53..6efbd219 100644
--- a/src/pluginList.ml.in
+++ b/src/pluginList.ml.in
@@ -1,5 +1,5 @@
let plugins =
[
- (module Scopes.Plugin : PluginType.PluginType);
+ (module Scopes.Plugin : PluginType.S);
@SALSA@
]
diff --git a/src/pluginType.ml b/src/pluginType.ml
index 5f76b708..84b82bfe 100644
--- a/src/pluginType.ml
+++ b/src/pluginType.ml
@@ -1,4 +1,4 @@
-module type PluginType =
+module type S =
sig
val name: string
val activate: unit -> unit
diff --git a/src/plugins.ml b/src/plugins.ml
index c110ee13..1d0e55c0 100644
--- a/src/plugins.ml
+++ b/src/plugins.ml
@@ -7,32 +7,32 @@ let options () =
List.flatten (
List.map Options_management.plugin_opt (
List.map (fun m ->
- let module M = (val m : PluginType.PluginType) in
+ let module M = (val m : PluginType.S) in
(M.name, M.activate, M.options)
) plugins
))
let check_force_stateful () =
List.exists (fun m ->
- let module M = (val m : PluginType.PluginType) in
+ let module M = (val m : PluginType.S) in
M.check_force_stateful ()
) plugins
let refine_machine_code prog machine_code =
List.fold_left (fun accu m ->
- let module M = (val m : PluginType.PluginType) in
+ let module M = (val m : PluginType.S) in
M.refine_machine_code prog accu
) machine_code plugins
let c_backend_main_loop_body_prefix basename mname fmt () =
- List.iter (fun (m: (module PluginType.PluginType)) ->
- let module M = (val m : PluginType.PluginType) in
+ List.iter (fun (m: (module PluginType.S)) ->
+ let module M = (val m : PluginType.S) in
M.c_backend_main_loop_body_prefix basename mname fmt ()) plugins
let c_backend_main_loop_body_suffix fmt () =
- List.iter (fun (m: (module PluginType.PluginType)) ->
- let module M = (val m : PluginType.PluginType) in
+ List.iter (fun (m: (module PluginType.S)) ->
+ let module M = (val m : PluginType.S) in
M.c_backend_main_loop_body_suffix fmt ()) plugins
(* Specific treatment of annotations when inlining, specific of declared plugins *)
diff --git a/src/plugins/salsa/salsa_plugin.ml b/src/plugins/salsa/salsa_plugin.ml
index eed8bf6e..7f575845 100644
--- a/src/plugins/salsa/salsa_plugin.ml
+++ b/src/plugins/salsa/salsa_plugin.ml
@@ -39,4 +39,4 @@ module Plugin =
machine_code
- end: PluginType.PluginType)
+ end: PluginType.S)
diff --git a/src/plugins/scopes/scopes.ml b/src/plugins/scopes/scopes.ml
index df009347..58396442 100644
--- a/src/plugins/scopes/scopes.ml
+++ b/src/plugins/scopes/scopes.ml
@@ -239,7 +239,7 @@ let update_machine machine =
module Plugin : (
sig
- include PluginType.PluginType
+ include PluginType.S
val show_scopes: unit -> bool
end) =
struct
diff --git a/src/tools/seal_verifier.ml b/src/tools/seal_verifier.ml
new file mode 100644
index 00000000..22a19fc9
--- /dev/null
+++ b/src/tools/seal_verifier.ml
@@ -0,0 +1,13 @@
+let active = ref false
+
+module Verifier =
+ (struct
+ include VerifierType.Default
+ let name = "seal"
+ let options = []
+ let activate () = active := true
+ let is_active () = !active
+ let run basename prog machines = ()
+
+ end: VerifierType.S)
+
diff --git a/src/tools/stateflow/semantics/cPS_lustre_generator.ml b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
index 06088873..891bb983 100644
--- a/src/tools/stateflow/semantics/cPS_lustre_generator.ml
+++ b/src/tools/stateflow/semantics/cPS_lustre_generator.ml
@@ -321,7 +321,7 @@ struct
in tr
let mkcomponent :
- type c. c call_t -> c -> t -> LustreSpec.program =
+ type c. c call_t -> c -> t -> LustreSpec.program_t =
fun call args ->
fun tr ->
reset_loc ();
diff --git a/src/tools/stateflow/semantics/cPS_transformer.ml b/src/tools/stateflow/semantics/cPS_transformer.ml
index d47dfc4e..3199d6be 100644
--- a/src/tools/stateflow/semantics/cPS_transformer.ml
+++ b/src/tools/stateflow/semantics/cPS_transformer.ml
@@ -78,8 +78,8 @@ sig
val eval_act : (module ThetaType with type t = t) -> act_t -> t
val eval_cond : cond_t -> t -> t -> t
(* val mktransformer : t -> unit *)
- val mkprincipal : t -> LustreSpec.program
- val mkcomponent : 'c call_t -> 'c -> t -> LustreSpec.program
+ val mkprincipal : t -> LustreSpec.program_t
+ val mkcomponent : 'c call_t -> 'c -> t -> LustreSpec.program_t
end
module type ComparableTransformerType =
diff --git a/src/tools/stateflow/sf_sem.ml b/src/tools/stateflow/sf_sem.ml
index 0f7bd182..bcc10983 100644
--- a/src/tools/stateflow/sf_sem.ml
+++ b/src/tools/stateflow/sf_sem.ml
@@ -80,8 +80,9 @@ let _ =
let auto_out = open_out auto_file in
let auto_fmt = Format.formatter_of_out_channel auto_out in
Format.fprintf auto_fmt "%a@." Printers.pp_prog prog;
-
- let prog, deps = Compiler_stages.stage1 prog "" "" in
+
+ let params = Backends.get_normalization_params () in
+ let prog, deps = Compiler_stages.stage1 params prog "" "" in
Format.printf "%a@." Printers.pp_prog prog;
let noauto_file = "sf_gen_test_noauto.lus" in (* Could be changed *)
diff --git a/src/tools/zustre_verifier.ml b/src/tools/zustre_verifier.ml
new file mode 100644
index 00000000..31e0de9b
--- /dev/null
+++ b/src/tools/zustre_verifier.ml
@@ -0,0 +1,181 @@
+open LustreSpec
+open Machine_code
+open Format
+open Horn_backend_common
+open Horn_backend
+
+let active = ref false
+let ctx = ref (Z3.mk_context [])
+
+let bool_sort = Z3.Boolean.mk_sort !ctx
+let int_sort = Z3.Arithmetic.Integer.mk_sort !ctx
+let real_sort = Z3.Arithmetic.Real.mk_sort !ctx
+
+let const_sorts = Hashtbl.create 13
+let get_const_sort ty_name =
+ Hashtbl.find const_sorts ty_name
+
+let decl_sorts () =
+ Hashtbl.iter (fun typ decl ->
+ match typ with
+ | Tydec_const var ->
+ (match decl.top_decl_desc with
+ | TypeDef tdef -> (
+ match tdef.tydef_desc with
+ | Tydec_enum tl ->
+ let new_sort = Z3.Enumeration.mk_sort_s !ctx var tl in
+ Hashtbl.add const_sorts var new_sort
+ | _ -> assert false
+ )
+ | _ -> assert false
+ )
+ | _ -> ()) Corelang.type_table
+
+
+let rec type_to_sort t =
+ if Types.is_bool_type t then bool_sort else
+ if Types.is_int_type t then int_sort else
+ if Types.is_real_type t then real_sort else
+ match (Types.repr t).Types.tdesc with
+ | Types.Tconst ty -> get_const_sort ty
+ | Types.Tclock t -> type_to_sort t
+ | Types.Tarray(dim,ty) -> Z3.Z3Array.mk_sort !ctx int_sort (type_to_sort ty)
+ | Types.Tstatic(d, ty)-> type_to_sort ty
+ | Types.Tarrow _
+ | _ -> Format.eprintf "internal error: pp_type %a@."
+ Types.print_ty t; assert false
+
+
+let decl_var id =
+ Z3.FuncDecl.mk_func_decl_s !ctx id.var_id [] (type_to_sort id.var_type)
+
+let decl_machine machines m =
+ if m.Machine_code.mname.node_id = Machine_code.arrow_id then
+ (* We don't print arrow function *)
+ ()
+ else
+ begin
+ let _ = List.map decl_var
+ (
+ (inout_vars machines m)@
+ (rename_current_list (full_memory_vars machines m)) @
+ (rename_mid_list (full_memory_vars machines m)) @
+ (rename_next_list (full_memory_vars machines m)) @
+ (rename_machine_list m.mname.node_id m.mstep.step_locals)
+ )
+ in
+ ()
+ (*
+ if is_stateless m then
+ begin
+ (* Declaring single predicate *)
+ fprintf fmt "(declare-rel %a (%a))@."
+ pp_machine_stateless_name m.mname.node_id
+ (Utils.fprintf_list ~sep:" " pp_type)
+ (List.map (fun v -> v.var_type) (inout_vars machines m));
+
+ match m.mstep.step_asserts with
+ | [] ->
+ begin
+
+ (* Rule for single predicate *)
+ fprintf fmt "; Stateless step rule @.";
+ fprintf fmt "@[<v 2>(rule (=> @ ";
+ ignore (pp_machine_instrs machines ([] (* No reset info for stateless nodes *) ) m fmt m.mstep.step_instrs);
+ fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
+ pp_machine_stateless_name m.mname.node_id
+ (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (inout_vars machines m);
+ end
+ | assertsl ->
+ begin
+ let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
+
+ fprintf fmt "; Stateless step rule with Assertions @.";
+ (*Rule for step*)
+ fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
+ ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
+ fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
+ pp_machine_stateless_name m.mname.node_id
+ (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
+
+ end
+
+ end
+ else
+ begin
+ (* Declaring predicate *)
+ fprintf fmt "(declare-rel %a (%a))@."
+ pp_machine_reset_name m.mname.node_id
+ (Utils.fprintf_list ~sep:" " pp_type)
+ (List.map (fun v -> v.var_type) (reset_vars machines m));
+
+ fprintf fmt "(declare-rel %a (%a))@."
+ pp_machine_step_name m.mname.node_id
+ (Utils.fprintf_list ~sep:" " pp_type)
+ (List.map (fun v -> v.var_type) (step_vars machines m));
+
+ pp_print_newline fmt ();
+
+ (* Rule for reset *)
+ fprintf fmt "@[<v 2>(rule (=> @ %a@ (%a @[<v 0>%a)@]@]@.))@.@."
+ (pp_machine_reset machines) m
+ pp_machine_reset_name m.mname.node_id
+ (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (reset_vars machines m);
+
+ match m.mstep.step_asserts with
+ | [] ->
+ begin
+ fprintf fmt "; Step rule @.";
+ (* Rule for step*)
+ fprintf fmt "@[<v 2>(rule (=> @ ";
+ ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
+ fprintf fmt "@ (%a @[<v 0>%a)@]@]@.))@.@."
+ pp_machine_step_name m.mname.node_id
+ (Utils.fprintf_list ~sep:"@ " (pp_horn_var m)) (step_vars machines m);
+ end
+ | assertsl ->
+ begin
+ let pp_val = pp_horn_val ~is_lhs:true m.mname.node_id (pp_horn_var m) in
+ (* print_string pp_val; *)
+ fprintf fmt "; Step rule with Assertions @.";
+
+ (*Rule for step*)
+ fprintf fmt "@[<v 2>(rule (=> @ (and @ ";
+ ignore (pp_machine_instrs machines [] m fmt m.mstep.step_instrs);
+ fprintf fmt "@. %a)@ (%a @[<v 0>%a)@]@]@.))@.@." (pp_conj pp_val) assertsl
+ pp_machine_step_name m.mname.node_id
+ (Utils.fprintf_list ~sep:" " (pp_horn_var m)) (step_vars machines m);
+ end
+
+
+ end
+ *) end
+
+
+module Verifier =
+ (struct
+ include VerifierType.Default
+ let name = "zustre"
+ let options = []
+ let activate () = (
+ active := true;
+ Options.output := "horn";
+ )
+ let is_active () = !active
+
+ let get_normalization_params () =
+ (* make sure the output is "Horn" *)
+ assert(!Options.output = "horn");
+ Backends.get_normalization_params ()
+
+ let run basename prog machines =
+ let machines = Machine_code.arrow_machine::machines in
+ let machines = preprocess machines in
+ decl_sorts ();
+ List.iter (decl_machine machines) (List.rev machines);
+
+
+ ()
+
+ end: VerifierType.S)
+
diff --git a/src/verifierList.ml.in b/src/verifierList.ml.in
new file mode 100644
index 00000000..322949a2
--- /dev/null
+++ b/src/verifierList.ml.in
@@ -0,0 +1,6 @@
+let verifiers =
+ [
+ @LUSTREV_SEAL@
+ @LUSTREV_ZUSTRE@
+ @LUSTREV_TINY@
+ ]
diff --git a/src/verifierType.ml b/src/verifierType.ml
new file mode 100644
index 00000000..6f2f56d1
--- /dev/null
+++ b/src/verifierType.ml
@@ -0,0 +1,20 @@
+module type S =
+sig
+ val name: string
+ val activate: unit -> unit
+ val is_active: unit -> bool
+ val options: (string * Arg.spec * string) list
+ val get_normalization_params: unit -> Normalization.param_t
+ val run: string -> LustreSpec.program_t -> Machine_code.machine_t list -> unit
+end
+
+module Default =
+ struct
+
+ let get_normalization_params () = {
+ Normalization.unfold_arrow_active = true;
+ force_alias_ite = false;
+ force_alias_internal_fun = false;
+ }
+
+ end
diff --git a/src/verifiers.ml b/src/verifiers.ml
new file mode 100644
index 00000000..3ad61be5
--- /dev/null
+++ b/src/verifiers.ml
@@ -0,0 +1,48 @@
+open LustreSpec
+
+open VerifierList
+
+let active = ref None
+
+let options () =
+ List.flatten (
+ List.map Options_management.verifier_opt (
+ List.map (fun m ->
+ let module M = (val m : VerifierType.S) in
+ (M.name, M.activate, M.options)
+ ) verifiers
+ ))
+
+let verifier_list verifiers =
+ List.fold_left (fun acc m ->
+ let module M = (val m : VerifierType.S) in
+ (if acc = "" then "" else acc ^ ", ") ^ M.name
+ ) "" verifiers
+
+let get_active () =
+ match !active with
+ | None ->
+ begin
+ (* check that a single one is active and register it *)
+ let found =
+ List.fold_left (fun found m ->
+ let module M = (val m : VerifierType.S) in
+ if M.is_active () then
+ m::found
+ else
+ found
+ ) [] verifiers
+ in
+ match found with
+ | [] -> raise (Sys_error ("Please select one verifier in " ^ verifier_list verifiers))
+ | [m] -> active := Some m; m
+ | _ -> raise (Sys_error ("Too many selected verifiers: " ^ verifier_list found))
+ end
+
+ | Some m -> m
+
+
+
+ (* Local Variables: *)
+ (* compile-command:"make -C .." *)
+ (* End: *)
--
GitLab