diff --git a/AUTHORS b/AUTHORS
index 8335327685e97105082c8510d8e9094d025944e0..034c98aca58ef0e5aba6ab8c091b04ccf6180b54 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -1,5 +1,4 @@
Pierre-Loïc Garoche - ONERA, France
Xavier Thirioux - ENSEEIHT/INPT, France
-Temesghen Kahsai - NASA Ames / CMU, US
-
+Temesghen Kahsai - CMU/NASA, USA
Inital Typing/Clocking by Julien Forget - LIFL, France
diff --git a/autom4te.cache/output.0 b/autom4te.cache/output.0
index b2f7212ea97a594e1d0a7c9cf0e820083fb777d7..82dd0bc950cd8b1829d6dd907bd1d94ee156eca2 100644
--- a/autom4te.cache/output.0
+++ b/autom4te.cache/output.0
@@ -1,6 +1,6 @@
@%:@! /bin/sh
@%:@ Guess values for system-dependent variables and create Makefiles.
-@%:@ Generated by GNU Autoconf 2.69 for lustrec 1.0-Unversioned directory.
+@%:@ Generated by GNU Autoconf 2.69 for lustrec 1.1-Unversioned directory.
@%:@
@%:@ Report bugs to <ploc@garoche.net>.
@%:@
@@ -579,8 +579,8 @@ MAKEFLAGS=
# Identity of this package.
PACKAGE_NAME='lustrec'
PACKAGE_TARNAME='lustrec'
-PACKAGE_VERSION='1.0-Unversioned directory'
-PACKAGE_STRING='lustrec 1.0-Unversioned directory'
+PACKAGE_VERSION='1.1-Unversioned directory'
+PACKAGE_STRING='lustrec 1.1-Unversioned directory'
PACKAGE_BUGREPORT='ploc@garoche.net'
PACKAGE_URL=''
@@ -1179,7 +1179,7 @@ if test "$ac_init_help" = "long"; then
# Omit some internal or obsolete options to make the list less imposing.
# This message is too long to be a string in the A/UX 3.1 sh.
cat <<_ACEOF
-\`configure' configures lustrec 1.0-Unversioned directory to adapt to many kinds of systems.
+\`configure' configures lustrec 1.1-Unversioned directory to adapt to many kinds of systems.
Usage: $0 [OPTION]... [VAR=VALUE]...
@@ -1240,7 +1240,7 @@ fi
if test -n "$ac_init_help"; then
case $ac_init_help in
- short | recursive ) echo "Configuration of lustrec 1.0-Unversioned directory:";;
+ short | recursive ) echo "Configuration of lustrec 1.1-Unversioned directory:";;
esac
cat <<\_ACEOF
@@ -1314,7 +1314,7 @@ fi
test -n "$ac_init_help" && exit $ac_status
if $ac_init_version; then
cat <<\_ACEOF
-lustrec configure 1.0-Unversioned directory
+lustrec configure 1.1-Unversioned directory
generated by GNU Autoconf 2.69
Copyright (C) 2012 Free Software Foundation, Inc.
@@ -1331,7 +1331,7 @@ cat >config.log <<_ACEOF
This file contains any messages produced by compilers while
running configure, to aid debugging if configure makes a mistake.
-It was created by lustrec $as_me 1.0-Unversioned directory, which was
+It was created by lustrec $as_me 1.1-Unversioned directory, which was
generated by GNU Autoconf 2.69. Invocation command line was
$ $0 $@
@@ -2401,7 +2401,7 @@ cat >>$CONFIG_STATUS <<\_ACEOF || ac_write_fail=1
# report actual input values of CONFIG_FILES etc. instead of their
# values after options handling.
ac_log="
-This file was extended by lustrec $as_me 1.0-Unversioned directory, which was
+This file was extended by lustrec $as_me 1.1-Unversioned directory, which was
generated by GNU Autoconf 2.69. Invocation command line was
CONFIG_FILES = $CONFIG_FILES
@@ -2454,7 +2454,7 @@ _ACEOF
cat >>$CONFIG_STATUS <<_ACEOF || ac_write_fail=1
ac_cs_config="`$as_echo "$ac_configure_args" | sed 's/^ //; s/[\\""\`\$]/\\\\&/g'`"
ac_cs_version="\\
-lustrec config.status 1.0-Unversioned directory
+lustrec config.status 1.1-Unversioned directory
configured by $0, generated by GNU Autoconf 2.69,
with options \\"\$ac_cs_config\\"
diff --git a/autom4te.cache/requests b/autom4te.cache/requests
index 08824a4d1e410a2a1cd4bee417eb9c664722cc44..82f32b43f9c57b901a39431dc13f2ad1206c0e80 100644
--- a/autom4te.cache/requests
+++ b/autom4te.cache/requests
@@ -14,63 +14,63 @@
'configure.ac'
],
{
+ '_LT_AC_TAGCONFIG' => 1,
+ 'AM_PROG_F77_C_O' => 1,
+ 'AC_INIT' => 1,
+ 'm4_pattern_forbid' => 1,
+ '_AM_COND_IF' => 1,
+ 'AC_CANONICAL_TARGET' => 1,
+ 'AC_SUBST' => 1,
+ 'AC_CONFIG_LIBOBJ_DIR' => 1,
+ 'AC_FC_SRCEXT' => 1,
+ 'AC_CANONICAL_HOST' => 1,
+ 'AC_PROG_LIBTOOL' => 1,
+ 'AM_INIT_AUTOMAKE' => 1,
+ 'AM_PATH_GUILE' => 1,
+ 'AC_CONFIG_SUBDIRS' => 1,
+ 'AM_AUTOMAKE_VERSION' => 1,
'LT_CONFIG_LTDL_DIR' => 1,
- 'AC_FC_FREEFORM' => 1,
- 'm4_pattern_allow' => 1,
- 'AM_SILENT_RULES' => 1,
- 'AM_GNU_GETTEXT_INTL_SUBDIR' => 1,
+ 'AC_REQUIRE_AUX_FILE' => 1,
+ 'AC_CONFIG_LINKS' => 1,
+ 'm4_sinclude' => 1,
'LT_SUPPORTED_TAG' => 1,
- 'AC_CONFIG_FILES' => 1,
- 'AM_PROG_MOC' => 1,
- 'AH_OUTPUT' => 1,
+ 'AM_MAINTAINER_MODE' => 1,
+ 'AM_NLS' => 1,
'AC_FC_PP_DEFINE' => 1,
- 'AC_CANONICAL_SYSTEM' => 1,
- 'AC_PROG_LIBTOOL' => 1,
+ 'AM_GNU_GETTEXT_INTL_SUBDIR' => 1,
+ 'AM_MAKEFILE_INCLUDE' => 1,
'_m4_warn' => 1,
- 'AC_SUBST_TRACE' => 1,
- 'AC_CANONICAL_TARGET' => 1,
- 'AM_POT_TOOLS' => 1,
- 'm4_include' => 1,
- 'AM_MAINTAINER_MODE' => 1,
+ 'AM_PROG_CXX_C_O' => 1,
+ '_AM_COND_ENDIF' => 1,
+ '_AM_MAKEFILE_INCLUDE' => 1,
+ 'AM_ENABLE_MULTILIB' => 1,
+ 'AM_SILENT_RULES' => 1,
+ 'AM_PROG_MOC' => 1,
+ 'AC_CONFIG_FILES' => 1,
'include' => 1,
- 'AC_CANONICAL_BUILD' => 1,
'LT_INIT' => 1,
- 'AM_GNU_GETTEXT' => 1,
- 'AC_REQUIRE_AUX_FILE' => 1,
- 'AM_INIT_AUTOMAKE' => 1,
- '_AM_COND_ELSE' => 1,
- 'm4_sinclude' => 1,
'AM_PROG_AR' => 1,
- 'AM_PROG_CC_C_O' => 1,
- 'AM_PROG_F77_C_O' => 1,
- '_LT_AC_TAGCONFIG' => 1,
- 'AM_MAKEFILE_INCLUDE' => 1,
+ 'AM_GNU_GETTEXT' => 1,
+ 'AC_LIBSOURCE' => 1,
+ 'AM_PROG_FC_C_O' => 1,
+ 'AC_CANONICAL_BUILD' => 1,
+ 'AC_FC_FREEFORM' => 1,
+ 'AH_OUTPUT' => 1,
'AC_FC_PP_SRCEXT' => 1,
+ '_AM_SUBST_NOTMAKE' => 1,
+ 'AC_CONFIG_AUX_DIR' => 1,
'sinclude' => 1,
- 'AM_PROG_FC_C_O' => 1,
- 'AC_CONFIG_LIBOBJ_DIR' => 1,
- 'AM_PROG_CXX_C_O' => 1,
- 'AC_CONFIG_SUBDIRS' => 1,
- 'm4_pattern_forbid' => 1,
- 'AC_LIBSOURCE' => 1,
- 'AC_INIT' => 1,
+ 'AM_PROG_CC_C_O' => 1,
+ 'm4_pattern_allow' => 1,
'AM_XGETTEXT_OPTION' => 1,
- 'AC_CANONICAL_HOST' => 1,
- 'AC_FC_SRCEXT' => 1,
- '_AM_SUBST_NOTMAKE' => 1,
- 'AM_PATH_GUILE' => 1,
- 'AC_CONFIG_LINKS' => 1,
- 'AC_SUBST' => 1,
- 'AM_AUTOMAKE_VERSION' => 1,
- 'AM_NLS' => 1,
- 'AM_ENABLE_MULTILIB' => 1,
- 'AC_CONFIG_HEADERS' => 1,
- '_AM_COND_ENDIF' => 1,
- '_AM_MAKEFILE_INCLUDE' => 1,
+ 'AC_CANONICAL_SYSTEM' => 1,
'AM_CONDITIONAL' => 1,
+ 'AC_CONFIG_HEADERS' => 1,
'AC_DEFINE_TRACE_LITERAL' => 1,
- 'AC_CONFIG_AUX_DIR' => 1,
- '_AM_COND_IF' => 1
+ 'AM_POT_TOOLS' => 1,
+ 'm4_include' => 1,
+ '_AM_COND_ELSE' => 1,
+ 'AC_SUBST_TRACE' => 1
}
], 'Autom4te::Request' )
);
diff --git a/autom4te.cache/traces.0 b/autom4te.cache/traces.0
index c52956e0f6fc48dc2cb63ea4f9784a34566a1529..71d42a8087eefdef501af539f83c33159e2ffb03 100644
--- a/autom4te.cache/traces.0
+++ b/autom4te.cache/traces.0
@@ -1,4 +1,4 @@
-m4trace:configure.ac:2: -1- AC_INIT([lustrec], [1.0-svnversion], [ploc@garoche.net])
+m4trace:configure.ac:2: -1- AC_INIT([lustrec], [1.1-svnversion], [ploc@garoche.net])
m4trace:configure.ac:2: -1- m4_pattern_forbid([^_?A[CHUM]_])
m4trace:configure.ac:2: -1- m4_pattern_forbid([_AC_])
m4trace:configure.ac:2: -1- m4_pattern_forbid([^LIBOBJS$], [do not use LIBOBJS directly, use AC_LIBOBJ (see section `AC_LIBOBJ vs LIBOBJS'])
@@ -167,7 +167,7 @@ m4trace:configure.ac:84: -1- AC_SUBST_TRACE([abs_datadir])
m4trace:configure.ac:84: -1- m4_pattern_allow([^abs_datadir$])
m4trace:configure.ac:84: -1- AC_DEFINE_TRACE_LITERAL([abs_datadir])
m4trace:configure.ac:84: -1- m4_pattern_allow([^abs_datadir$])
-m4trace:configure.ac:90: -1- AC_CONFIG_FILES([Makefile
+m4trace:configure.ac:87: -1- AC_CONFIG_FILES([Makefile
src/Makefile
src/myocamlbuild.ml
src/version.ml])
diff --git a/configure.ac b/configure.ac
index 058ebe449e3d098d335ee0f251b79e999308d528..8ef82bad7b6abc4cdbc9a9bed7339b7ddd094765 100644
--- a/configure.ac
+++ b/configure.ac
@@ -1,5 +1,5 @@
define([svnversion], esyscmd([sh -c "svnversion|sed "s/:.*//"|tr -d '\n'"]))dnl
-AC_INIT([lustrec], [1.0-svnversion], [ploc@garoche.net])
+AC_INIT([lustrec], [1.1-svnversion], [ploc@garoche.net])
AC_DEFINE(SVN_REVISION, "svnversion", [SVN Revision])
diff --git a/share/FindLustre.cmake b/share/FindLustre.cmake
index ee9a6098e7c63f5510bb3eee3f7f8612e006c65a..bb0cfb4fced4eb3027892d9f6d329c9c68362999 100644
--- a/share/FindLustre.cmake
+++ b/share/FindLustre.cmake
@@ -15,7 +15,15 @@
# The module defines some functions:
# Lustre_Compile([NODE <Lustre Main Node>]
# LUS_FILES <Lustre files>
-# [USER_C_FILES <C files>])
+# [USER_C_FILES <C files>]
+# [VERBOSE <level>]
+# LIBNAME <libraryName>)
+#
+# When used the Lustre_Compile macro define the variable
+# LUSTRE_GENERATED_C_FILES_<libraryName> in the parent scope
+# so that the caller can get (if needed) the list of Lustre generated files.
+# The VERBOSE level is a numeric value passed directly to the -verbose
+# command line option of the lustre compiler
#
if(LUSTRE_PATH_HINT)
@@ -65,7 +73,7 @@ find_path(LUSTRE_INCLUDE_DIR
include(CMakeParseArguments)
function(Lustre_Compile)
set(options "")
- set(oneValueArgs NODE LIBNAME)
+ set(oneValueArgs NODE LIBNAME VERBOSE)
set(multiValueArgs LUS_FILES USER_C_FILES)
cmake_parse_arguments(LUS "${options}" "${oneValueArgs}" "${multiValueArgs}" ${ARGN})
@@ -81,6 +89,13 @@ function(Lustre_Compile)
set(LUSTRE_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/lus_${LUS_LIBNAME}")
endif()
+ if (LUS_VERBOSE)
+ set(LUSTRE_VERBOSE_OPT "-verbose ${LUS_VERBOSE}")
+ else()
+ # the default is to be quiet.
+ set(LUSTRE_VERBOSE_OPT "-verbose;0")
+ endif()
+
file(MAKE_DIRECTORY ${LUSTRE_OUTPUT_DIR})
set(GLOBAL_LUSTRE_GENERATED_C_FILES "")
# create list of generated C files in parent scope
@@ -97,7 +112,7 @@ function(Lustre_Compile)
set(LUSTRE_GENERATED_FILES ${LUSTRE_GENERATED_FILES} ${LUSTRE_OUTPUT_DIR}/${L}.lusic)
add_custom_command(
OUTPUT ${LUSTRE_GENERATED_FILES}
- COMMAND ${LUSTRE_COMPILER} ${LUSTRE_NODE_OPT} -d ${LUSTRE_OUTPUT_DIR} ${LFILE}
+ COMMAND ${LUSTRE_COMPILER} ${LUSTRE_VERBOSE_OPT} ${LUSTRE_NODE_OPT} -d ${LUSTRE_OUTPUT_DIR} ${LFILE}
DEPENDS ${LFILE}
WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
COMMENT "Compile Lustre source(s): ${LFILE} (generates: ${LUSTRE_GENERATED_FILES})."
@@ -109,6 +124,7 @@ function(Lustre_Compile)
add_library(${LUS_LIBNAME} SHARED
${GLOBAL_LUSTRE_GENERATED_C_FILES} ${LUS_USER_C_FILES}
)
+ set_target_properties(${LUS_LIBNAME} PROPERTIES COMPILE_FLAGS "-std=c99")
set(LUSTRE_GENERATED_C_FILES_${LUS_LIBNAME} "${GLOBAL_LUSTRE_GENERATED_C_FILES}" PARENT_SCOPE)
message(STATUS "Lustre: Added rule for building lustre library: ${LUS_LIBNAME}")
endfunction(Lustre_Compile)
diff --git a/src/Makefile b/src/Makefile
index 9a025882f1941b627171805963d5ba05deb9c633..e5cdef415b4a4906451690fb866d02300a6d106b 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -1,4 +1,4 @@
-OCAMLBUILD=/opt/local/bin/ocamlbuild -classic-display -no-links
+OCAMLBUILD=/Users/teme/.opam/4.02.1/bin/ocamlbuild -classic-display -no-links
prefix=/usr/local
exec_prefix=${prefix}
diff --git a/src/automata.ml b/src/automata.ml
index 14efabf885faf0c41b3f7b887ab0b612ac95fb86..ec08590c1031c4f56becd266b48f213f17d52dcd 100755
--- a/src/automata.ml
+++ b/src/automata.ml
@@ -68,7 +68,16 @@ let expr_of_exit loc restart state conds tag =
mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag))
let rec unless_read reads handler =
+ let res =
List.fold_left (fun read (_, c, _, _) -> get_expr_vars read c) reads handler.hand_unless
+ in
+(
+(*
+Format.eprintf "unless_reads %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements reads);
+Format.eprintf "unless_reads' %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res);
+*)
+res
+)
let rec until_read reads handler =
List.fold_left (fun read (_, c, _, _) -> get_expr_vars read c) reads handler.hand_until
@@ -79,8 +88,19 @@ let rec handler_read reads handler =
List.fold_left (fun read stmt ->
match stmt with
| Eq eq -> get_expr_vars read eq.eq_rhs
- | Aut aut -> List.fold_left handler_read read aut.aut_handlers ) reads handler.hand_stmts
- in ISet.diff allvars locals
+ | Aut aut -> automata_read read aut) reads handler.hand_stmts
+ in let res = ISet.diff allvars locals
+ in
+(
+(*
+Format.eprintf "handler_allvars %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements allvars);
+Format.eprintf "handler_read %s = %a@." handler.hand_state (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) (ISet.elements res);
+*)
+res
+)
+
+and automata_read reads aut =
+ List.fold_left (fun read handler -> until_read (handler_read (unless_read read handler) handler) handler) reads aut.aut_handlers
let rec handler_write writes handler =
let locals = List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty handler.hand_locals in
@@ -117,6 +137,7 @@ let vars_of_aut_state aut_state =
[aut_state.incoming_r'; aut_state.incoming_r; aut_state.actual_r; aut_state.incoming_s'; as_clock aut_state.incoming_s; as_clock aut_state.actual_s]
let node_of_unless nused used node aut_id aut_state handler =
+(*Format.eprintf "node_of_unless %s@." node.node_id;*)
let inputs = unless_read ISet.empty handler in
let var_inputs = aut_state.incoming_r :: aut_state.incoming_s :: (node_vars_of_idents node inputs) in
let var_outputs = aut_state.actual_r :: aut_state.actual_s :: [] in
@@ -160,12 +181,13 @@ let mk_frename used outputs =
(fun name -> try IMap.find name table with Not_found -> name)
let node_of_assign_until nused used node aut_id aut_state handler =
+(*Format.eprintf "node_of_assign_until %s@." node.node_id;*)
let writes = handler_write ISet.empty handler in
let inputs = ISet.diff (handler_read (until_read ISet.empty handler) handler) writes in
let frename = mk_frename used writes in
let var_inputs = node_vars_of_idents node inputs in
let new_var_locals = node_vars_of_idents node writes in
- let var_outputs = node_vars_of_idents node writes in
+ let var_outputs = List.sort IdentModule.compare (node_vars_of_idents node writes) in
let new_var_outputs = List.map (fun vdecl -> { vdecl with var_id = frename vdecl.var_id }) var_outputs in
let new_output_eqs = List.map2 (fun o o' -> Eq (mkeq handler.hand_loc ([o'.var_id], mkident handler.hand_loc o.var_id))) var_outputs new_var_outputs in
let until_expr = List.fold_right add_branch handler.hand_until (mkidentpair handler.hand_loc aut_state.actual_r.var_id aut_state.actual_s.var_id) in
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index 82241ae23412fb9262a2711dbf81967f6029a5d6..d7674274bb1d1593a3aaa9dafbd4c0ceea1794e3 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -92,8 +92,22 @@ let pp_machine_static_alloc_name fmt id = fprintf fmt "%s_ALLOC" id
let pp_machine_reset_name fmt id = fprintf fmt "%s_reset" id
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
-let pp_c_dimension fmt d =
- fprintf fmt "%a" Dimension.pp_dimension d
+let rec pp_c_dimension fmt dim =
+ match dim.Dimension.dim_desc with
+ | Dimension.Dident id ->
+ fprintf fmt "%s" id
+ | Dimension.Dint i ->
+ fprintf fmt "%d" i
+ | Dimension.Dbool b ->
+ fprintf fmt "%B" b
+ | Dimension.Dite (i, t, e) ->
+ fprintf fmt "((%a)?%a:%a)"
+ pp_c_dimension i pp_c_dimension t pp_c_dimension e
+ | Dimension.Dappl (f, args) ->
+ fprintf fmt "%a" (Basic_library.pp_c f pp_c_dimension) args
+ | Dimension.Dlink dim' -> fprintf fmt "%a" pp_c_dimension dim'
+ | Dimension.Dvar -> fprintf fmt "_%s" (Utils.name_of_dimension dim.Dimension.dim_id)
+ | Dimension.Dunivar -> fprintf fmt "'%s" (Utils.name_of_dimension dim.Dimension.dim_id)
let is_basic_c_type t =
match (Types.repr t).Types.tdesc with
@@ -119,7 +133,7 @@ let pp_c_type var fmt t =
| Types.Tstatic (_, t') -> fprintf fmt "const "; aux t' pp_suffix
| Types.Tconst ty -> fprintf fmt "%s %s" ty var
| Types.Tarrow (_, _) -> fprintf fmt "void (*%s)()" var
- | _ -> eprintf "internal error: pp_c_type %a@." Types.print_ty t; assert false
+ | _ -> eprintf "internal error: C_backend_common.pp_c_type %a@." Types.print_ty t; assert false
in aux t (fun fmt () -> ())
let rec pp_c_initialize fmt t =
@@ -138,6 +152,7 @@ let rec pp_c_initialize fmt t =
let pp_c_tag fmt t =
pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
+
(* Prints a constant value *)
let rec pp_c_const fmt c =
match c with
@@ -154,11 +169,12 @@ let rec pp_c_const fmt c =
but an offset suffix may be added for array variables
*)
let rec pp_c_val self pp_var fmt v =
+ (*Format.eprintf "C_backend_common.pp_c_val %a@." pp_val v;*)
match v with
| Cst c -> pp_c_const fmt c
| Array vl -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
| Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
- | Power (v, n) -> assert false
+ | Power (v, n) -> (Format.eprintf "internal error: C_backend_common.pp_c_val %a@." pp_val v; assert false)
| LocalVar v -> pp_var fmt v
| StateVar v ->
(* array memory vars are represented by an indirection to a local var with the right type,
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index ba897830184f13741ef9edc443d6d6313c26e44a..c8c06713286f0a921c669f4407bc1ccb8bcdaa36 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -30,6 +30,7 @@ struct
(* Instruction Printing functions *)
(********************************************************************************************)
+
(* Computes the depth to which multi-dimension array assignments should be expanded.
It equals the maximum number of nested static array constructions accessible from root [v].
*)
@@ -101,32 +102,77 @@ let reorder_loop_variables loop_vars =
List.partition (function (d, LInt _) -> true | _ -> false) loop_vars
in
var_loops @ int_loops
-
+
(* Prints a one loop variable suffix for arrays *)
let pp_loop_var fmt lv =
match snd lv with
| LVar v -> fprintf fmt "[%s]" v
| LInt r -> fprintf fmt "[%d]" !r
- | LAcc i -> fprintf fmt "[%a]" pp_val i
+ | LAcc i -> fprintf fmt "[%a]" pp_c_dimension (dimension_of_value i)
(* Prints a suffix of loop variables for arrays *)
let pp_suffix fmt loop_vars =
Utils.fprintf_list ~sep:"" pp_loop_var fmt loop_vars
-(* Prints a [value] indexed by the suffix list [loop_vars] *)
-let rec pp_value_suffix self loop_vars pp_value fmt value =
+(* Prints a value expression [v], with internal function calls only.
+ [pp_var] is a printer for variables (typically [pp_c_var_read]),
+ but an offset suffix may be added for array variables
+*)
+(* Prints a constant value before a suffix (needs casting) *)
+let rec pp_c_const_suffix var_type fmt c =
+ match c with
+ | Const_int i -> pp_print_int fmt i
+ | Const_real r -> pp_print_string fmt r
+ | Const_float r -> pp_print_float fmt r
+ | Const_tag t -> pp_c_tag fmt t
+ | Const_array ca -> let var_type = Types.array_element_type var_type in
+ fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_c_const_suffix var_type)) ca
+ | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> (pp_c_const_suffix (Types.struct_field_type var_type f)) fmt c)) fl
+ | Const_string _ -> assert false (* string occurs in annotations not in C *)
+
+
+(* Prints a [value] of type [var_type] indexed by the suffix list [loop_vars] *)
+let rec pp_value_suffix self var_type loop_vars pp_value fmt value =
+(*Format.eprintf "pp_value_suffix: %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars;*)
match loop_vars, value with
+ | (x, LAcc i) :: q, _ when is_const_index i ->
+ let r = ref (Dimension.size_const_dimension (Machine_code.dimension_of_value i)) in
+ pp_value_suffix self var_type ((x, LInt r)::q) pp_value fmt value
+ | (_, LInt r) :: q, Cst (Const_array cl) ->
+ let var_type = Types.array_element_type var_type in
+ pp_value_suffix self var_type q pp_value fmt (Cst (List.nth cl !r))
| (_, LInt r) :: q, Array vl ->
- pp_value_suffix self q pp_value fmt (List.nth vl !r)
+ let var_type = Types.array_element_type var_type in
+ pp_value_suffix self var_type q pp_value fmt (List.nth vl !r)
+ | loop_var :: q, Array vl ->
+ let var_type = Types.array_element_type var_type in
+ Format.fprintf fmt "(%a[]){%a }%a" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix self var_type q pp_value)) vl pp_suffix [loop_var]
+ | [] , Array vl ->
+ let var_type = Types.array_element_type var_type in
+ Format.fprintf fmt "(%a[]){%a }" (pp_c_type "") var_type (Utils.fprintf_list ~sep:", " (pp_value_suffix self var_type [] pp_value)) vl
| _ :: q, Power (v, n) ->
- pp_value_suffix self q pp_value fmt v
+ pp_value_suffix self var_type q pp_value fmt v
| _ , Fun (n, vl) ->
- Basic_library.pp_c n (pp_value_suffix self loop_vars pp_value) fmt vl
+ Basic_library.pp_c n (pp_value_suffix self var_type loop_vars pp_value) fmt vl
| _ , Access (v, i) ->
- pp_value_suffix self ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_value fmt v
- | _ , _ ->
- let pp_var_suffix fmt v = fprintf fmt "%a%a" pp_value v pp_suffix loop_vars in
- pp_c_val self pp_var_suffix fmt value
+ let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in
+ pp_value_suffix self var_type ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_value fmt v
+ | _ , LocalVar v -> Format.fprintf fmt "%a%a" pp_value v pp_suffix loop_vars
+ | _ , StateVar v ->
+ (* array memory vars are represented by an indirection to a local var with the right type,
+ in order to avoid casting everywhere. *)
+ if Types.is_array_type v.var_type
+ then Format.fprintf fmt "%a%a" pp_value v pp_suffix loop_vars
+ else Format.fprintf fmt "%s->_reg.%a%a" self pp_value v pp_suffix loop_vars
+ | _ , Cst cst -> pp_c_const_suffix var_type fmt cst
+ | _ , _ -> (Format.eprintf "internal error: C_backend_src.pp_value_suffix %a %a %a@." Types.print_ty var_type Machine_code.pp_val value pp_suffix loop_vars; assert false)
+
+(* Subsumes C_backend_common.pp_c_val to cope with aggressive substitution
+ which may yield constant arrays in expressions.
+ Type is needed to correctly print constant arrays.
+ *)
+let pp_c_val self pp_var fmt (t, v) =
+ pp_value_suffix self t [] pp_var fmt v
(* type_directed assignment: array vs. statically sized type
- [var_type]: type of variable to be assigned
@@ -157,8 +203,8 @@ let pp_assign m self pp_var fmt var_type var_name value =
match vars with
| [] ->
fprintf fmt "%a = %a;"
- (pp_value_suffix self loop_vars pp_var) var_name
- (pp_value_suffix self loop_vars pp_var) value
+ (pp_value_suffix self var_type loop_vars pp_var) var_name
+ (pp_value_suffix self var_type loop_vars pp_var) value
| (d, LVar i) :: q ->
(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
@@ -177,36 +223,6 @@ let pp_assign m self pp_var fmt var_type var_name value =
aux fmt reordered_loop_vars
end
-let pp_instance_call m self fmt i (inputs: value_t list) (outputs: var_decl list) =
- try (* stateful node instance *)
- let (n,_) = List.assoc i m.minstances in
- fprintf fmt "%a (%a%t%a%t%s->%s);"
- pp_machine_step_name (node_name n)
- (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
- (Utils.pp_final_char_if_non_empty ", " inputs)
- (Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs
- (Utils.pp_final_char_if_non_empty ", " outputs)
- self
- i
- with Not_found -> (* stateless node instance *)
- let (n,_) = List.assoc i m.mcalls in
- fprintf fmt "%a (%a%t%a);"
- pp_machine_step_name (node_name n)
- (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
- (Utils.pp_final_char_if_non_empty ", " inputs)
- (Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs
-
-let pp_machine_reset (m: machine_t) self fmt inst =
- let (node, static) =
- try
- List.assoc inst m.minstances
- with Not_found -> (Format.eprintf "pp_machine_reset %s %s %s: internal error@," m.mname.node_id self inst; raise Not_found) in
- fprintf fmt "%a(%a%t%s->%s);"
- pp_machine_reset_name (node_name node)
- (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
- (Utils.pp_final_char_if_non_empty ", " static)
- self inst
-
let has_c_prototype funname dependencies =
let imported_node_opt = (* We select the last imported node with the name funname.
The order of evaluation of dependencies should be
@@ -232,9 +248,51 @@ let has_c_prototype funname dependencies =
| None -> false
| Some nd -> (match nd.nodei_prototype with Some "C" -> true | _ -> false)
+let pp_instance_call dependencies m self fmt i (inputs: value_t list) (outputs: var_decl list) =
+ try (* stateful node instance *)
+ let (n,_) = List.assoc i m.minstances in
+ let (input_types, _) = Typing.get_type_of_call n in
+ let inputs = List.combine input_types inputs in
+ fprintf fmt "%a (%a%t%a%t%s->%s);"
+ pp_machine_step_name (node_name n)
+ (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
+ (Utils.pp_final_char_if_non_empty ", " inputs)
+ (Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs
+ (Utils.pp_final_char_if_non_empty ", " outputs)
+ self
+ i
+ with Not_found -> (* stateless node instance *)
+ let (n,_) = List.assoc i m.mcalls in
+ let (input_types, output_types) = Typing.get_type_of_call n in
+ let inputs = List.combine input_types inputs in
+ if has_c_prototype i dependencies
+ then (* external C function *)
+ let outputs = List.map2 (fun t v -> t, LocalVar v) output_types outputs in
+ fprintf fmt "%a = %s(%a);"
+ (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) outputs
+ i
+ (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
+ else
+ fprintf fmt "%a (%a%t%a);"
+ pp_machine_step_name (node_name n)
+ (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) inputs
+ (Utils.pp_final_char_if_non_empty ", " inputs)
+ (Utils.fprintf_list ~sep:", " (pp_c_var_write m)) outputs
+
+let pp_machine_reset (m: machine_t) self fmt inst =
+ let (node, static) =
+ try
+ List.assoc inst m.minstances
+ with Not_found -> (Format.eprintf "pp_machine_reset %s %s %s: internal error@," m.mname.node_id self inst; raise Not_found) in
+ fprintf fmt "%a(%a%t%s->%s);"
+ pp_machine_reset_name (node_name node)
+ (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
+ (Utils.pp_final_char_if_non_empty ", " static)
+ self inst
+
let rec pp_conditional dependencies (m: machine_t) self fmt c tl el =
fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
- (pp_c_val self (pp_c_var_read m)) c
+ (pp_c_val self (pp_c_var_read m)) (Type_predef.type_bool, c)
(Utils.pp_newline_if_non_empty tl)
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) tl
(Utils.pp_newline_if_non_empty el)
@@ -254,23 +312,20 @@ and pp_machine_instr dependencies (m: machine_t) self fmt instr =
i.var_type (StateVar i) v
| MStep ([i0], i, vl) when Basic_library.is_internal_fun i ->
pp_machine_instr dependencies m self fmt (MLocalAssign (i0, Fun (i, vl)))
- | MStep ([i0], i, vl) when has_c_prototype i dependencies ->
- fprintf fmt "%a = %s(%a);"
- (pp_c_val self (pp_c_var_read m)) (LocalVar i0)
- i
- (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) vl
| MStep (il, i, vl) ->
- pp_instance_call m self fmt i vl il
- | MBranch (g,hl) ->
- if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
+ pp_instance_call dependencies m self fmt i vl il
+ | MBranch (_, []) -> (Format.eprintf "internal error: C_backend_src.pp_machine_instr %a@." pp_instr instr; assert false)
+ | MBranch (g, hl) ->
+ if let t = fst (List.hd hl) in t = tag_true || t = tag_false
then (* boolean case, needs special treatment in C because truth value is not unique *)
(* may disappear if we optimize code by replacing last branch test with default *)
let tl = try List.assoc tag_true hl with Not_found -> [] in
let el = try List.assoc tag_false hl with Not_found -> [] in
pp_conditional dependencies m self fmt g tl el
else (* enum type case *)
+ let g_typ = Typing.type_const Location.dummy_loc (Const_tag (fst (List.hd hl))) in
fprintf fmt "@[<v 2>switch(%a) {@,%a@,}@]"
- (pp_c_val self (pp_c_var_read m)) g
+ (pp_c_val self (pp_c_var_read m)) (g_typ, g)
(Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl
and pp_machine_branch dependencies m self fmt (t, h) =
diff --git a/src/backends/Horn/horn_backend.ml b/src/backends/Horn/horn_backend.ml
index d5350cd00ce270c2a9928c059210d6679eac4cd7..24f58617739c40f7d8d9faf751b4271ae9d57f54 100644
--- a/src/backends/Horn/horn_backend.ml
+++ b/src/backends/Horn/horn_backend.ml
@@ -1,3 +1,4 @@
+(********************************************************************)
(* *)
(* The LustreC compiler toolset / The LustreC Development Team *)
(* Copyright 2012 - -- ONERA - CNRS - INPT *)
@@ -46,7 +47,7 @@ let pp_conj pp fmt l =
match l with
[] -> assert false
| [x] -> pp fmt x
- | _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:"\n\t" pp) l
+ | _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l
diff --git a/src/basic_library.ml b/src/basic_library.ml
index 9a878922126664b4e80048e16c1a76bfda12610f..7e35b8a4707702184fba76724b00c32b308f4615 100644
--- a/src/basic_library.ml
+++ b/src/basic_library.ml
@@ -127,7 +127,7 @@ let pp_c i pp_val fmt vl =
| "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
| "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
- | _ -> failwith i
+ | _ -> (Format.eprintf "internal error: Basic_library.pp_c %s@." i; assert false)
let pp_java i pp_val fmt vl =
match i, vl with
@@ -140,7 +140,7 @@ let pp_java i pp_val fmt vl =
| "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
| "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2
| _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
- | _ -> assert false
+ | _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert false)
let pp_horn i pp_val fmt vl =
match i, vl with
@@ -158,7 +158,7 @@ let pp_horn i pp_val fmt vl =
| "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
| "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
| _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
- | _ -> assert false
+ | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
(* | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
*)
diff --git a/src/causality.ml b/src/causality.ml
index 19c429e1bc1974f530fa90b740976505f45cf971..00efa5430444f442100b588759a61d47b95b1269 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -216,8 +216,8 @@ let add_eq_dependencies mems inputs node_vars eq (g, g') =
| Expr_fby (e1, e2) -> add_dep true lhs e2 (add_dep false lhs e1 g)
| Expr_pre e -> add_dep true lhs e g
| Expr_ident x -> add_var lhs_is_mem lhs x (add_clock lhs_is_mem lhs rhs.expr_clock g)
- | Expr_access (e1, _)
- | Expr_power (e1, _) -> add_dep lhs_is_mem lhs e1 g
+ | Expr_access (e1, d)
+ | Expr_power (e1, d) -> add_dep lhs_is_mem lhs e1 (add_dep lhs_is_mem lhs (expr_of_dimension d) g)
| Expr_array a -> List.fold_right (add_dep lhs_is_mem lhs) a g
| Expr_tuple t -> List.fold_right2 (fun l r -> add_dep lhs_is_mem [l] r) lhs t g
| Expr_merge (c, hl) -> add_var lhs_is_mem lhs c (List.fold_right (fun (_, h) -> add_dep lhs_is_mem lhs h) hl g)
@@ -526,12 +526,13 @@ let merge_with g1 g2 =
IdentDepGraph.iter_edges (fun s t -> IdentDepGraph.add_edge g1 s t) g2
end
+let world = "!!_world"
+
let add_external_dependency outputs mems g =
- let caller ="!!_world" in
begin
- IdentDepGraph.add_vertex g caller;
- ISet.iter (fun o -> IdentDepGraph.add_edge g caller o) outputs;
- ISet.iter (fun m -> IdentDepGraph.add_edge g caller m) mems;
+ IdentDepGraph.add_vertex g world;
+ ISet.iter (fun o -> IdentDepGraph.add_edge g world o) outputs;
+ ISet.iter (fun m -> IdentDepGraph.add_edge g world m) mems;
end
let global_dependency node =
diff --git a/src/liveness.ml b/src/liveness.ml
index 026331ee5e281803070ef6fee8718cebc5337418..21b716df1f8f441f41ea8846e0748fc601b454c7 100755
--- a/src/liveness.ml
+++ b/src/liveness.ml
@@ -81,6 +81,9 @@ let node_reusable_variables node =
Disjunction.CISet.empty
node.node_locals
+let kill_instance_variables ctx inst =
+ IdentDepGraph.remove_vertex ctx.dep_graph inst
+
let kill_root ctx head =
IdentDepGraph.iter_succ (IdentDepGraph.remove_edge ctx.dep_graph head.var_id) ctx.dep_graph head.var_id
@@ -89,6 +92,7 @@ let kill_root ctx head =
- [evaluated] is the set of already evaluated variables,
wrt the scheduling
- does only remove edges, not variables themselves
+ - yet, instance variables are removed
*)
let remove_roots ctx =
let rem = ref true in
@@ -97,10 +101,12 @@ let remove_roots ctx =
do
rem := false;
let all_roots = graph_roots ctx.dep_graph in
- let frontier_roots = Disjunction.CISet.filter (fun v -> List.mem v.var_id all_roots) !remaining in
- if not (Disjunction.CISet.is_empty frontier_roots) then
+ let inst_roots, var_roots = List.partition (fun v -> ExprDep.is_instance_var v && v <> Causality.world) all_roots in
+ let frontier_roots = Disjunction.CISet.filter (fun v -> List.mem v.var_id var_roots) !remaining in
+ if not (Disjunction.CISet.is_empty frontier_roots && inst_roots = []) then
begin
rem := true;
+ List.iter (kill_instance_variables ctx) inst_roots;
Disjunction.CISet.iter (kill_root ctx) frontier_roots;
remaining := Disjunction.CISet.diff !remaining frontier_roots
end
diff --git a/src/lustreSpec.ml b/src/lustreSpec.ml
index 79c9f5d4b1f9fdd2c31204b2b9f8eac8540ce1de..4202fe412f55ae631629b0dd34dc4c3b0490cec0 100644
--- a/src/lustreSpec.ml
+++ b/src/lustreSpec.ml
@@ -132,6 +132,11 @@ type node_annot = {
behaviors: (string * eexpr list * eexpr list * Location.t) list;
spec_loc: Location.t;
}
+
+type offset =
+| Index of Dimension.dim_expr
+| Field of label
+
type assert_t =
{
assert_expr: expr;
diff --git a/src/machine_code.ml b/src/machine_code.ml
index fb0035985cfde269c586595e945cff75d0bf68c2..cd1fc9d71d48603edb1b71966c2bba042deb6b66 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -496,7 +496,7 @@ let translate_decl nd sch =
assert (ISet.is_empty m0);
assert (init0 = []);
assert (Utils.IMap.is_empty j0);
- let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, s0) sorted_eqs in
+ let m, init, j, locals, s = translate_eqs nd (m0, init0, j0, locals0, []) sorted_eqs in
let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
{
mname = nd;
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index 870b0b1579f6b3725e8374b3beac013ec8a463e4..a0d5b62313c826a5a41deca08c5922e62fa700e3 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -98,6 +98,8 @@ let rec compile_source dirname basename extension =
(* Removing automata *)
let prog = Automata.expand_decls prog in
+ Log.report ~level:4 (fun fmt -> fprintf fmt "After automata expansion:@.@[<v 2>@ %a@]@," Printers.pp_prog prog);
+
(* Importing source *)
let _ = Modules.load_program ISet.empty prog in
@@ -230,6 +232,10 @@ let rec compile_source dirname basename extension =
Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
let machine_code = Machine_code.translate_prog prog node_schs in
+ Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
+ (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
+ machine_code);
+
(* Optimize machine code *)
let machine_code =
if !Options.optimization >= 4 && !Options.output <> "horn" then
@@ -241,10 +247,6 @@ let rec compile_source dirname basename extension =
machine_code
in
- Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
- (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
- machine_code);
-
(* Optimize machine code *)
let machine_code =
if !Options.optimization >= 2 && !Options.output <> "horn" then
@@ -266,10 +268,12 @@ let rec compile_source dirname basename extension =
machine_code
in
-
- Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
- (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
- machine_code);
+ if !Options.optimization >= 2 then
+ begin
+ Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
+ (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
+ machine_code);
+ end;
(* Printing code *)
let basename = Filename.basename basename in
diff --git a/src/myocamlbuild.ml b/src/myocamlbuild.ml
index c8bb75e0f96ebdddceebf0c0587367dfa9197330..f06c1af2064202a7554142b96de532323a13b67f 100644
--- a/src/myocamlbuild.ml
+++ b/src/myocamlbuild.ml
@@ -5,7 +5,7 @@ open Command
dispatch begin function
| After_rules ->
(* We declare external libraries *)
- ocaml_lib ~extern:true ~dir:"/Users/Teme/.opam/system/lib/ocamlgraph" "graph";
+ ocaml_lib ~extern:true ~dir:"/Users/teme/.opam/4.02.1/lib/ocamlgraph" "graph";
if @CC_NOASNEEDED@ then
flag ["ocaml"; "link"]
(S [A"-cclib";A"-Wl,--no-as-needed"]);
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 4bf910ace1068483c3301a103ae9cdd4a539ccc2..48a36f9645d02443478077b6814609477a868e6a 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -16,6 +16,7 @@ open Causality
open Machine_code
open Dimension
+
let pp_elim fmt elim =
begin
Format.fprintf fmt "{ /* elim table: */@.";
@@ -52,6 +53,54 @@ and eliminate_expr elim expr =
let eliminate_dim elim dim =
Dimension.expr_replace_expr (fun v -> try dimension_of_value (IMap.find v elim) with Not_found -> mkdim_ident dim.dim_loc v) dim
+let unfold_expr_offset m offset expr =
+ List.fold_left (fun res -> (function Index i -> Access(res, value_of_dimension m i) | Field f -> failwith "not yet implemented")) expr offset
+
+let rec simplify_cst_expr m offset cst =
+ match offset, cst with
+ | [] , _
+ -> Cst cst
+ | Index i :: q, Const_array cl when Dimension.is_dimension_const i
+ -> simplify_cst_expr m q (List.nth cl (Dimension.size_const_dimension i))
+ | Index i :: q, Const_array cl
+ -> unfold_expr_offset m [Index i] (Array (List.map (simplify_cst_expr m q) cl))
+ | Field f :: q, Const_struct fl
+ -> simplify_cst_expr m q (List.assoc f fl)
+ | _ -> (Format.eprintf "internal error: Optimize_machine.simplify_cst_expr %a@." Printers.pp_const cst; assert false)
+
+let simplify_expr_offset m expr =
+ let rec simplify offset expr =
+ match offset, expr with
+ | Field f ::q , _ -> failwith "not yet implemented"
+ | _ , Fun (id, vl) when Basic_library.is_internal_fun id
+ -> Fun (id, List.map (simplify offset) vl)
+ | _ , Fun _
+ | _ , StateVar _
+ | _ , LocalVar _ -> unfold_expr_offset m offset expr
+ | _ , Cst cst -> simplify_cst_expr m offset cst
+ | _ , Access (expr, i) -> simplify (Index (dimension_of_value i) :: offset) expr
+ | [] , _ -> expr
+ | Index _ :: q, Power (expr, _) -> simplify q expr
+ | Index i :: q, Array vl when Dimension.is_dimension_const i
+ -> simplify q (List.nth vl (Dimension.size_const_dimension i))
+ | Index i :: q, Array vl -> unfold_expr_offset m [Index i] (Array (List.map (simplify q) vl))
+ | _ -> (Format.eprintf "internal error: Optimize_machine.simplify_expr_offset %a@." pp_val expr; assert false)
+ (*Format.eprintf "simplify_expr %a %a = %a@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset pp_val res; res)
+ with e -> (Format.eprintf "simplify_expr %a %a = <FAIL>@." pp_val expr (Utils.fprintf_list ~sep:"" Printers.pp_offset) offset; raise e*)
+ in simplify [] expr
+
+let rec simplify_instr_offset m instr =
+ match instr with
+ | MLocalAssign (v, expr) -> MLocalAssign (v, simplify_expr_offset m expr)
+ | MStateAssign (v, expr) -> MStateAssign (v, simplify_expr_offset m expr)
+ | MReset id -> instr
+ | MStep (outputs, id, inputs) -> MStep (outputs, id, List.map (simplify_expr_offset m) inputs)
+ | MBranch (cond, brl)
+ -> MBranch(simplify_expr_offset m cond, List.map (fun (l, il) -> l, simplify_instrs_offset m il) brl)
+
+and simplify_instrs_offset m instrs =
+ List.map (simplify_instr_offset m) instrs
+
let is_scalar_const c =
match c with
| Const_int _
@@ -60,23 +109,58 @@ let is_scalar_const c =
| Const_tag _ -> true
| _ -> false
-let basic_unfoldable_expr expr =
- match expr with
- | Cst c when is_scalar_const c -> true
- | LocalVar _
- | StateVar _ -> true
- | _ -> false
+(* An instruction v = expr may (and will) be unfolded iff:
+ - either expr is atomic
+ (no complex expressions, only const, vars and array/struct accesses)
+ - or v has a fanin <= 1 (used at most once)
+*)
+let is_unfoldable_expr fanin expr =
+ let rec unfold_const offset cst =
+ match offset, cst with
+ | _ , Const_int _
+ | _ , Const_real _
+ | _ , Const_float _
+ | _ , Const_tag _ -> true
+ | Field f :: q, Const_struct fl -> unfold_const q (List.assoc f fl)
+ | [] , Const_struct _ -> false
+ | Index i :: q, Const_array cl when Dimension.is_dimension_const i
+ -> unfold_const q (List.nth cl (Dimension.size_const_dimension i))
+ | _ , Const_array _ -> false
+ | _ -> assert false in
+ let rec unfold offset expr =
+ match offset, expr with
+ | _ , Cst cst -> unfold_const offset cst
+ | _ , LocalVar _
+ | _ , StateVar _ -> true
+ | [] , Power _
+ | [] , Array _ -> false
+ | Index i :: q, Power (v, _) -> unfold q v
+ | Index i :: q, Array vl when Dimension.is_dimension_const i
+ -> unfold q (List.nth vl (Dimension.size_const_dimension i))
+ | _ , Array _ -> false
+ | _ , Access (v, i) -> unfold (Index (dimension_of_value i) :: offset) v
+ | _ , Fun (id, vl) when fanin < 2 && Basic_library.is_internal_fun id
+ -> List.for_all (unfold offset) vl
+ | _ , Fun _ -> false
+ | _ -> assert false
+ in unfold [] expr
let unfoldable_assign fanin v expr =
try
let d = Hashtbl.find fanin v.var_id
- in basic_unfoldable_expr expr ||
+ in is_unfoldable_expr d expr
+ with Not_found -> false
+(*
+let unfoldable_assign fanin v expr =
+ try
+ let d = Hashtbl.find fanin v.var_id
+ in is_basic_expr expr ||
match expr with
| Cst c when d < 2 -> true
| Fun (id, _) when d < 2 && Basic_library.is_internal_fun id -> true
| _ -> false
with Not_found -> false
-
+*)
let merge_elim elim1 elim2 =
let merge k e1 e2 =
match e1, e2 with
@@ -141,6 +225,8 @@ let machine_unfold fanin elim machine =
(*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "machine_unfold %a@." pp_elim elim);*)
let elim_consts, mconst = instrs_unfold fanin elim machine.mconst in
let elim_vars, instrs = instrs_unfold fanin elim_consts machine.mstep.step_instrs in
+ let instrs = simplify_instrs_offset machine instrs in
+ let checks = List.map (fun (loc, check) -> loc, eliminate_expr elim_vars check) machine.mstep.step_checks in
let locals = List.filter (fun v -> not (IMap.mem v.var_id elim_vars)) machine.mstep.step_locals in
let minstances = List.map (static_call_unfold elim_consts) machine.minstances in
let mcalls = List.map (static_call_unfold elim_consts) machine.mcalls
@@ -150,7 +236,8 @@ let machine_unfold fanin elim machine =
mstep = {
machine.mstep with
step_locals = locals;
- step_instrs = instrs
+ step_instrs = instrs;
+ step_checks = checks
};
mconst = mconst;
minstances = minstances;
@@ -256,7 +343,7 @@ let rec instr_cse (subst, instrs) instr =
(* Simple cases*)
| MStep([v], id, vl) when Basic_library.is_internal_fun id
-> instr_cse (subst, instrs) (MLocalAssign (v, Fun (id, vl)))
- | MLocalAssign(v, expr) when basic_unfoldable_expr expr
+ | MLocalAssign(v, expr) when is_unfoldable_expr 2 expr
-> (IMap.add v.var_id expr subst, instr :: instrs)
| _ when is_assign instr
-> subst_instr subst instrs instr
diff --git a/src/parser_lustre.mly b/src/parser_lustre.mly
index 2251db4bc5b4d103af4787f6ec79bdaf2b121e79..ab4b17667086efaad40d2814e96f9ac39145e80e 100755
--- a/src/parser_lustre.mly
+++ b/src/parser_lustre.mly
@@ -257,7 +257,7 @@ typ_def_rhs:
| STRUCT LCUR field_list RCUR { Tydec_struct (List.rev $3) }
array_typ_decl:
- { fun typ -> typ }
+ %prec POWER { fun typ -> typ }
| POWER dim array_typ_decl { fun typ -> $3 (Tydec_array ($2, typ)) }
typeconst:
diff --git a/src/printers.ml b/src/printers.ml
index 92ea74489687b3ecad93b2337611ee24d0344b87..f2cb78de90939b4e16689b82c89f8a199bdfdfdf 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -332,7 +332,12 @@ let pp_lusi_header fmt basename prog =
fprintf fmt "(* by Lustre-C compiler version %s, %a *)@." Version.number pp_date (Unix.gmtime (Unix.time ()));
fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@.@.";
List.iter (fprintf fmt "%a@." pp_lusi) prog
-
+
+let pp_offset fmt offset =
+ match offset with
+ | Index i -> fprintf fmt "[%a]" Dimension.pp_dimension i
+ | Field f -> fprintf fmt ".%s" f
+
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/types.ml b/src/types.ml
index c61f25f3f638aafe608e57234c96ae75ab642423..299131ffe81e9efb3e213be30960da4161c875fa 100755
--- a/src/types.ml
+++ b/src/types.ml
@@ -251,6 +251,14 @@ let rec is_struct_type ty =
| Tstatic (_, ty') -> is_struct_type ty'
| _ -> false
+let struct_field_type ty field =
+ match (dynamic_type ty).tdesc with
+ | Tstruct fields ->
+ (try
+ List.assoc field fields
+ with Not_found -> assert false)
+ | _ -> assert false
+
let rec is_array_type ty =
match (repr ty).tdesc with
| Tarray _ -> true
diff --git a/src/typing.ml b/src/typing.ml
index 45d81bd9b8f1bf7852c1e8c2ec86797edffad516..747240eedc75ad237749555b438d1f0291a77f85 100755
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -336,9 +336,6 @@ and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
(*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*)
try_unify ~sub:sub formal_type real_type loc
-and type_ident env in_main loc const id =
- type_expr env in_main const (expr_of_ident id loc)
-
(* typing an application implies:
- checking that const formal parameters match real const (maybe symbolic) arguments
- checking type adequation between formal and real arguments
@@ -452,7 +449,9 @@ and type_expr env in_main const expr =
| Some c ->
check_constant expr.expr_loc const false;
type_subtyping_arg env in_main const c Type_predef.type_bool);
- let touts = type_appl env in_main expr.expr_loc const id (expr_list_of_expr args) in
+ let args_list = expr_list_of_expr args in
+ let touts = type_appl env in_main expr.expr_loc const id args_list in
+ args.expr_type <- new_ty (Ttuple (List.map (fun a -> a.expr_type) args_list));
expr.expr_type <- touts;
touts
| Expr_fby (e1,e2)
@@ -697,6 +696,16 @@ let rec type_top_decl env decl =
| TypeDef _ -> List.fold_left type_top_decl env (consts_of_enum_type decl)
| Open _ -> env
+let get_type_of_call decl =
+ match decl.top_decl_desc with
+ | Node nd ->
+ let (in_typ, out_typ) = split_arrow nd.node_type in
+ type_list_of_type in_typ, type_list_of_type out_typ
+ | ImportedNode nd ->
+ let (in_typ, out_typ) = split_arrow nd.nodei_type in
+ type_list_of_type in_typ, type_list_of_type out_typ
+ | _ -> assert false
+
let type_prog env decls =
try
List.fold_left type_top_decl env decls
diff --git a/src/version.ml b/src/version.ml
index e07864bc3cef0614dbe82179e68ad55496e4f03b..4ad27e23bce48856ae46946d2cc570f20fae97a7 100644
--- a/src/version.ml
+++ b/src/version.ml
@@ -1,5 +1,5 @@
-let number = "1.0-Unversioned directory"
+let number = "1.1-Unversioned directory"
let prefix = "/usr/local"
diff --git a/test/Makefile b/test/Makefile
index 932c082ac0420c740293b9614ac0db6f379e256b..e576624e403095f2b23657ccb0078a0bbb5e0c7c 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -4,12 +4,10 @@ test-compile:
@bash ./test-compile.sh -a -v 2 tests_ok.list
@rm build/*.o
-horn:
- @bash ./regression.sh -r -v 2 horn_regression.list
-
clean:
@rm -rf build
@for i in `find . -iname *.lusi`; do grep generated $$i > /dev/null; if [ $$? -eq 0 ]; then rm $$i; fi; done
distclean: clean
- @rm -rf horn-report*
+ @rm -rf report*
+
diff --git a/test/test-compile.sh b/test/test-compile.sh
index 158a0cb2a865c4c23863e63ceac168c391746d8c..ceafcdd05e5c58cd76f85a3f8f96b010c283cf8d 100755
--- a/test/test-compile.sh
+++ b/test/test-compile.sh
@@ -14,6 +14,23 @@ LUSTREC=lustrec
mkdir -p build
build=`pwd`"/build"
+gcc_compile() {
+ gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null;
+ if [ $? -ne 0 ]; then
+ rgcc="INVALID";
+ else
+ rgcc="VALID"
+ fi
+}
+
+lustrec_compile() {
+ $LUSTREC "$@";
+ if [ $? -ne 0 ]; then
+ rlustrec="INVALID";
+ else
+ rlustrec="VALID"
+ fi
+}
base_compile() {
while IFS=, read -r file main opts
@@ -26,51 +43,27 @@ base_compile() {
fi
dir=${SRC_PREFIX}/`dirname "$file"`
pushd $dir > /dev/null
- if [ "$main" != "" ]; then
- $LUSTREC -d $build -verbose 0 $opts -node $main "$name""$ext";
- if [ $? -ne 0 ]; then
- rlustrec1="INVALID";
- else
- rlustrec1="VALID"
- fi
- pushd $build > /dev/null
- if [ $ext = ".lus" ]; then
- gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
- if [ $? -ne 0 ]; then
- rgcc1="INVALID";
- else
- rgcc1="VALID"
- fi
+
+ if [ "$main" != "" ]; then
+ lustrec_compile -d $build -verbose 0 $opts -node $main $name$ext;
else
- rgcc1="NONE"
+ lustrec_compile -d $build -verbose 0 $opts $name$ext
fi
- popd > /dev/null
- else
- $LUSTREC -d $build -verbose 0 $opts "$name""$ext";
- if [ $? -ne 0 ]; then
- rlustrec1="INVALID";
- else
- rlustrec1="VALID"
- fi
pushd $build > /dev/null
- if [ $ext = ".lus" ]; then
- gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
- if [ $? -ne 0 ]; then
- rgcc1="INVALID";
- else
- rgcc1="VALID"
- fi
+
+ if [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
+ gcc_compile "$name";
else
- rgcc1="NONE"
+ rgcc="NONE"
fi
popd > /dev/null
- fi
- popd > /dev/null
- if [ $verbose -gt 0 ]; then
- echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
- else
- echo "lustrec ($rlustrec1), gcc($rgcc1), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
- fi;
+ popd > /dev/null
+
+ if [ $verbose -gt 0 ]; then
+ echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
+ else
+ echo "lustrec ($rlustrec), gcc($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
+ fi;
done < $file_list
}
@@ -78,35 +71,40 @@ inline_compile () {
while IFS=, read -r file main opts
do
name=`basename "$file" .lus`
+ ext=".lus"
if [ `dirname "$file"`/"$name" = "$file" ]; then
- return 0
+ name=`basename "$file" .lusi`
+ ext=".lusi"
fi
dir=${SRC_PREFIX}/`dirname "$file"`
-
pushd $dir > /dev/null
-# Checking inlining
- $LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
- if [ $? -ne 0 ]; then
- rlustrec2="INVALID";
- else
- rlustrec2="VALID"
- fi
- pushd $build > /dev/null
- gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
- if [ $? -ne 0 ]; then
- rgcc2="INVALID";
- else
- rgcc2="VALID"
- fi
- popd > /dev/null
- if [ $verbose -gt 0 ]; then
- echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
- else
- echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
- fi;
- popd > /dev/null
-done < $file_list
+ if [ "$main" != "" ]; then
+ lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name$ext;
+ else
+ if [ "$ext" = ".lusi" ]; then
+ lustrec_compile -d $build -verbose 0 $opts $name$ext;
+ else
+ rlustrec="NONE"
+ rgcc="NONE"
+ fi
+ fi
+ pushd $build > /dev/null
+
+ if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
+ gcc_compile "$name";
+ else
+ rgcc="NONE"
+ fi
+ popd > /dev/null
+ popd > /dev/null
+
+ if [ $verbose -gt 0 ]; then
+ echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
+ else
+ echo "lustrec inlined ($rlustrec), gcc ($rgcc), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
+ fi;
+ done < $file_list
}
inline_compile_with_check () {
@@ -119,23 +117,15 @@ inline_compile_with_check () {
fi
dir=${SRC_PREFIX}/`dirname "$file"`
pushd $dir > /dev/null
- $LUSTREC -d $build -verbose 0 $opts -inline -witnesses -node $main "$name".lus;
- if [ $? -ne 0 ]; then
- rlustrec2="INVALID";
- else
- rlustrec2="VALID"
- fi
+ lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name".lus"
+
pushd $build > /dev/null
- gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$name".c > /dev/null
- if [ $? -ne 0 ]; then
- rgcc2="INVALID";
- else
- rgcc2="VALID"
- fi
+ gcc_compile "$name"
+
popd > /dev/null
# Cheching witness
pushd $build > /dev/null
- $LUSTREC -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus
+ lustrec_compile -verbose 0 -horn-traces -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus
popd > /dev/null
z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
@@ -146,11 +136,11 @@ inline_compile_with_check () {
rinlining="UNKNOWN";
else
rinlining="INVALID/TIMEOUT"
- fi
+ fi
if [ $verbose -gt 0 ]; then
- echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
+ echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
else
- echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
+ echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
fi
popd > /dev/null
done < $file_list
@@ -166,19 +156,15 @@ check_prop () {
fi
dir=${SRC_PREFIX}/`dirname "$file"`
pushd $dir > /dev/null
-
+
# Checking horn backend
if [ "$main" != "" ]; then
- $LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
- else
- $LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts "$name".lus
- fi
- if [ $? -ne 0 ]; then
- rlustrec="INVALID";
+ lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main $name".lus";
else
- rlustrec="VALID"
+ lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts $name".lus"
fi
- # echo "z3 $build/$name".smt2
+
+ # echo "z3 $build/$name".smt2
# TODO: This part of the script has to be optimized
z3 -T:10 "$build/$name".smt2 | grep unsat > /dev/null
if [ $? -ne 0 ]; then
@@ -195,36 +181,6 @@ check_prop () {
done < $file_list
}
-check_horn () {
- while IFS=, read -r file main opts
- do
- name=`basename "$file" .lus`
- if [ "$name" = "$file" ]; then
- return 0
- fi
- dir=${SRC_PREFIX}/`dirname "$file"`
- pushd $dir > /dev/null
-
- # Checking horn backend
- if [ "$main" != "" ]; then
- $LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main "$name".lus;
- else
- $LUSTREC -horn-traces -horn-queries -d $build -verbose 0 $opts "$name".lus
- fi
- if [ $? -ne 0 ]; then
- rlustrec="INVALID";
- else
- rlustrec="VALID"
- fi
- if [ $verbose -gt 0 ]; then
- echo "lustrec ($rlustrec), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
- else
- echo "lustrec ($rlustrec), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report | grep "INVALID\|ERROR\|UNKNOWN"
- fi
- popd > /dev/null
-done < $file_list
-}
-
usage () {
echo "usage: $0 [-aciwh] file_list"
echo "-a: perform all steps"
@@ -232,7 +188,6 @@ echo "-c: basic compilation"
echo "-i: compile with inline mode"
echo "-w: compile with inline mode. Check the inlining with z3"
echo "-h: check files with the horn-pdf backend (requires z3)"
-echo "-r: regression test for horn backend"
echo "-v <int>: verbose level"
}
@@ -246,7 +201,6 @@ while [ $# -gt 0 ] ; do
-c) nobehavior=0; c=1 ; shift ;;
-i) nobehavior=0; i=1 ; shift ;;
-w) nobehavior=0; w=1 ; shift ;;
- -r) nobehavior=0; r=1 ; shift ;;
-h) nobehavior=0; h=1 ; shift ;;
--) shift ;;
-*) echo "bad option '$1'" ; exit 1 ;;
@@ -263,11 +217,16 @@ if [ ${#files} -eq 0 ] ; then
exit 1
fi
+# cleaning directory $build
+
+rm -f "$build"/* 2> /dev/null
+
+# executing tests
+
[ ! -z "$c" ] && base_compile
[ ! -z "$i" ] && inline_compile
[ ! -z "$w" ] && inline_compile_with_check
[ ! -z "$h" ] && check_prop
-[ ! -z "$r" ] && check_horn
[ "$nobehavior" -eq 1 ] && echo "Must provide an argument in [aciwh]" && usage
@@ -276,3 +235,4 @@ fi
#if [ $? -ne 1 ];then
# rm ../${file}i
#fi
+
diff --git a/test/tests_ok.list b/test/tests_ok.list
index 2ec653a5c064302bbbb9db1e299858ba54c82f9f..0d2a2b8c26f43ad97ab063e7e150d278799b7d5f 100644
--- a/test/tests_ok.list
+++ b/test/tests_ok.list
@@ -894,21 +894,38 @@
./tests/kind_fmcad08/large/ccp20.lus,top
./tests/kind_fmcad08/large/ccp11.lus,top
./tests/kind_fmcad08/large/cruise_controller_21.lus,top
+./tests/tuples/tuples1.lus
+./tests/tuples/tuples2.lus
./tests/arrays_arnaud/dummy_lib.lusi
./tests/arrays_arnaud/arrays.lus,,-check-access
./tests/arrays_arnaud/RelOpMatrix.lus
./tests/arrays_arnaud/access1.lus,,-check-access
+./tests/arrays_arnaud/generic1.lus,,-lusi
+./tests/arrays_arnaud/generic1.lusi
./tests/arrays_arnaud/generic1.lus
./tests/arrays_arnaud/generic2.lus
./tests/arrays_arnaud/generic3.lus,top,-dynamic -check-access
+./tests/clocks/clocks1.lus,,-lusi
+./tests/clocks/clocks1.lusi
./tests/clocks/clocks1.lus
./tests/clocks/clocks2.lus
+./tests/clocks/clocks6.lus
+./tests/clocks/clocks7.lus
+./tests/clocks/clocks8.lus
+./tests/clocks/clocks9.lus
+./tests/clocks/oversampling0.lus,,-lusi
+./tests/clocks/oversampling0.lusi
./tests/clocks/oversampling0.lus
./tests/lusic/test2.lusi
./tests/lusic/test1.lusi
./tests/lusic/test1.lus,as_soon_as
./tests/lusic/test2.lus
./tests/automata/aut1.lus
+./tests/automata/heater3.lus
+./tests/automata/heater4.lus
+./tests/linear_ctl/libarrays.lusi
+./tests/linear_ctl/ex1_mat.lus
+./tests/linear_ctl/ex1_mat_xt.lus
./tests/linear_ctl/ex8sat.lus,top
./tests/linear_ctl/ex2reset.lus,top
./tests/linear_ctl/lp_iir_9600_2.lus,top