diff --git a/Makefile.in b/Makefile.in
index 749e3bb066bfd0e4d2a18971ff50c1f1266c9d7a..48e6f31eef411fbc5fd075fa0757f40441c51e2e 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -7,12 +7,13 @@ datadir = ${prefix}/share
includedir = ${prefix}/include
LUSI_LIBS=include/math.lusi include/conv.lusi
+LUSI_MPFR_LIB=include/mpfr_lustre.lusi
LOCAL_BINDIR=bin
LOCAL_DOCDIR=doc/manual
lustrec:
@echo Compiling binary lustrec
- @$(OCAMLBUILD) -cflags -I,@OCAMLGRAPH_PATH@ -lflag @OCAMLGRAPH_PATH@/graph.cmxa -I src -I src/backends/C src/main_lustre_compiler.native
+ @$(OCAMLBUILD) -cflags -I,@OCAMLGRAPH_PATH@ -lflag @OCAMLGRAPH_PATH@/graph.cmxa -lflag nums.cmxa -I src -I src/backends/C -I src/plugins/scopes src/main_lustre_compiler.native
@mkdir -p $(LOCAL_BINDIR)
@mv _build/src/main_lustre_compiler.native $(LOCAL_BINDIR)/lustrec
@@ -31,7 +32,7 @@ clean:
$(OCAMLBUILD) -clean
dist-clean: clean
- @rm -f Makefile myocamlbuild.ml config.log config.status configure include/*.lusic include/math.h include/conv.h
+ @rm -f Makefile myocamlbuild.ml config.log config.status configure include/*.lusic include/math.h include/conv.h include/mpfr_lustre.h
%.lusic: %.lusi
@echo Compiling $<
@@ -39,10 +40,15 @@ dist-clean: clean
clean-lusic:
@rm -f $(LUSI_LIBS:%.lusi=%.lusic)
+ @rm -f $(LUSI_MPFR_LIB:%.lusi=%.lusic)
compile-lusi: $(LUSI_LIBS:%.lusi=%.lusic)
-install: clean-lusic compile-lusi
+compile-mpfr-lusi: $(LUSI_MPFR_LIB)
+ @echo Compiling $<
+ @$(LOCAL_BINDIR)/lustrec -verbose 0 -mpfr 1 -d include $<
+
+install: clean-lusic compile-lusi compile-mpfr-lusi
mkdir -p ${bindir}
install -m 0755 $(LOCAL_BINDIR)/* ${bindir}
mkdir -p ${includedir}/lustrec
diff --git a/configure.ac b/configure.ac
index 8ef82bad7b6abc4cdbc9a9bed7339b7ddd094765..54a3a158961ead40216e52a7f01f918692c791c5 100644
--- a/configure.ac
+++ b/configure.ac
@@ -1,9 +1,9 @@
-define([svnversion], esyscmd([sh -c "svnversion|sed "s/:.*//"|tr -d '\n'"]))dnl
-AC_INIT([lustrec], [1.1-svnversion], [ploc@garoche.net])
+define([gitversion], esyscmd([sh -c "git log --oneline | wc -l | tr -d '\n'"]))
+AC_INIT([lustrec], [1.1-gitversion], [ploc@garoche.net])
-AC_DEFINE(SVN_REVISION, "svnversion", [SVN Revision])
-AC_SUBST(SVN_REVISION)
+#AC_DEFINE(SVN_REVISION, "svnversion", [SVN Revision])
+#AC_SUBST(SVN_REVISION)
AC_CONFIG_SRCDIR([src/main_lustre_compiler.ml])
@@ -23,14 +23,15 @@ AC_ARG_WITH([ocamlgraph-path],
)
AC_SUBST(OCAMLGRAPH_PATH)
+AC_SUBST(SRC_PATH, esyscmd([sh -c "pwd" | tr -d '\n']))
AC_PATH_PROG([OCAMLC],[ocamlc],[:])
AC_MSG_CHECKING(OCaml version)
ocamlc_version=`$OCAMLC -v | grep version | rev| cut -d \ -f 1 | rev`
major=`echo $ocamlc_version | cut -d . -f 1`
minor=`echo $ocamlc_version | cut -d . -f 2`
-if (test "$major" -lt 3 -a "$minor" -lt 11 ); then
- AC_MSG_ERROR([Ocaml version must be at least 3.11. You have version $ocamlc_version])
+if (test "$major" -lt 4 -a "$minor" -lt 0 ); then
+ AC_MSG_ERROR([Ocaml version must be at least 4.0. You have version $ocamlc_version])
fi
AC_MSG_RESULT(valid ocaml version detected: $ocamlc_version)
@@ -41,14 +42,24 @@ AC_PATH_PROG([OCAMLBUILD],[ocamlbuild],[:])
# Checks for libraries. OCamlgraph
AC_MSG_CHECKING(ocamlgraph library)
- ocamlgraph_lib=`find $OCAMLGRAPH_PATH -iname graph.cmxa | grep -m 1 -o "graph.cmxa"`
+ ocamlgraph_lib=`find $OCAMLGRAPH_PATH -iname graph.cmxa -nowarn | grep -m 1 -o "graph.cmxa"`
if (test "x$ocamlgraph_lib" = xgraph.cmxa ); then
- ocamlgraph_lib_full=`find $OCAMLGRAPH_PATH -iname graph.cmxa | grep -m 1 "graph.cmxa"`
+ ocamlgraph_lib_full=`find $OCAMLGRAPH_PATH -iname graph.cmxa -nowarn | grep -m 1 "graph.cmxa"`
AC_MSG_RESULT(library detected: $ocamlgraph_lib_full )
else
AC_MSG_ERROR([ocamlgraph library not installed in $OCAMLGRAPH_PATH])
fi
+AC_CHECK_LIB(gmp, __gmpz_init,
+ [gmp=yes],
+ [AC_MSG_RESULT([GNU MP not found])
+ gmp=no])
+
+AC_CHECK_LIB(mpfr, mpfr_add, [mpfr=yes],
+ [AC_MSG_RESULT(
+[MPFR not found])
+mpfr=no])
+
# Workaround to solve an issue with ocamlbuild and C libraries.
# oCFLAGS="$CFLAGS"
@@ -87,10 +98,27 @@ AC_DEFINE_DIR([abs_datadir], [datadir])
AC_CONFIG_FILES([Makefile
src/Makefile
src/myocamlbuild.ml
- src/version.ml])
+ src/version.ml
+ test/test-compile.sh
+ ])
AC_OUTPUT
# summary
-dnl AC_MSG_NOTICE(******** Configuration ********)
+AC_MSG_NOTICE(******** Configuration ********)
+AC_MSG_NOTICE(bin path: $prefix/bin)
+AC_MSG_NOTICE(include path: $prefix/include)
+AC_MSG_NOTICE(******** Plugins ********)
+
+ if (test "x$gmp" = xyes -a "x$mpfr" = xyes ); then
+ AC_MSG_NOTICE([-mpfr option enable])
+
+ else
+ AC_MSG_WARN([MPFR option cannot be activated. Requires GMP and MPFR libs])
+
+ fi
+
+AC_MSG_NOTICE
+AC_MSG_NOTICE(******** Configuration ********)
+
diff --git a/include/arrow.h b/include/arrow.h
index 509ddc9684b0e68c0b17f0ac064cea00f93458f4..1c6284d2f031f4470d358abe8084be9a142058c3 100644
--- a/include/arrow.h
+++ b/include/arrow.h
@@ -17,6 +17,10 @@ extern struct _arrow_mem *_arrow_alloc ();
_arrow_DECLARE(attr, inst);\
_arrow_LINK(inst)
+#define _arrow_init(self) {}
+
+#define _arrow_clear(self) {}
+
#define _arrow_step(x,y,output,self) ((self)->_reg._first?((self)->_reg._first=0,(*output = x)):(*output = y))
#define _arrow_reset(self) {(self)->_reg._first = 1;}
diff --git a/lustrec.odocl b/lustrec.odocl
index 81f5ff3a428a7560cfe46bf95456ba6802d35353..84bd32c96b6a6f52411949fb78657b8a8ca5c962 100644
--- a/lustrec.odocl
+++ b/lustrec.odocl
@@ -8,6 +8,7 @@ backends/C/C_backend_makefile
backends/C/C_backend_spec
backends/C/C_backend_src
backends/Horn/Horn_backend
+plugins/scopes/Scopes
Basic_library
Causality
Clock_calculus
diff --git a/src/Makefile.in b/src/Makefile.in
index 9d7e902c678cdbd3fa7b89515f2724eeffa2bd5a..126a31f7253c95cb62dd436db79d0ecb71822650 100644
--- a/src/Makefile.in
+++ b/src/Makefile.in
@@ -1,4 +1,4 @@
-OCAMLBUILD=@OCAMLBUILD@ -classic-display -no-links
+OCAMLBUILD=@OCAMLBUILD@ -classic-display -use-ocamlfind -no-links
prefix=@prefix@
exec_prefix=@exec_prefix@
diff --git a/src/backends/C/c_backend.ml b/src/backends/C/c_backend.ml
index a6d1d711bb632c67e58a10406033b45cc095cb2a..59666b9cbdc7dee1995a6267a4eac7c91013d815 100644
--- a/src/backends/C/c_backend.ml
+++ b/src/backends/C/c_backend.ml
@@ -38,15 +38,19 @@ let gen_files funs basename prog machines dependencies header_file source_lib_fi
(* Generating Lib C file *)
print_lib_c source_lib_fmt basename prog machines dependencies;
-
+
close_out header_out;
close_out source_lib_out;
match !Options.main_node with
- | "" -> () (* No main node: we do not genenrate main nor makefile *)
+ | "" -> () (* No main node: we do not generate main nor makefile *)
| main_node -> (
match Machine_code.get_machine_opt main_node machines with
- | None -> Format.eprintf "Unable to find a main node named %s@.@?" main_node; assert false
+ | None -> begin
+ Global.main_node := main_node;
+ Format.eprintf "Code generation error: %a@." Corelang.pp_error LustreSpec.Main_not_found;
+ raise (Corelang.Error (Location.dummy_loc, LustreSpec.Main_not_found))
+ end
| Some m -> begin
let source_main_out = open_out source_main_file in
let source_main_fmt = formatter_of_out_channel source_main_out in
@@ -57,7 +61,7 @@ let gen_files funs basename prog machines dependencies header_file source_lib_fi
print_main_c source_main_fmt m basename prog machines dependencies;
(* Generating Makefile *)
- print_makefile basename main_node dependencies makefile_fmt;
+ print_makefile basename main_node dependencies makefile_fmt;
close_out source_main_out;
close_out makefile_out
diff --git a/src/backends/C/c_backend_common.ml b/src/backends/C/c_backend_common.ml
index d7674274bb1d1593a3aaa9dafbd4c0ceea1794e3..32651e4f590fbc33b39df36398851aff39c2948f 100644
--- a/src/backends/C/c_backend_common.ml
+++ b/src/backends/C/c_backend_common.ml
@@ -17,11 +17,17 @@ open Machine_code
let print_version fmt =
Format.fprintf fmt
- "/* @[<v>C code generated by %s@,SVN version number %s@,Code is %s compliant */@,@]@."
+ "/* @[<v>C code generated by %s@,Version number %s@,Code is %s compliant@,Using %s numbers */@,@]@."
(Filename.basename Sys.executable_name)
Version.number
(if !Options.ansi then "ANSI C90" else "C99")
-
+ (if !Options.mpfr then "MPFR multi-precision" else "(double) floating-point")
+
+let file_to_module_name basename =
+ let baseNAME = String.uppercase basename in
+ let baseNAME = Str.global_replace (Str.regexp "\\.\\|\\ ") "_" baseNAME in
+ baseNAME
+
(* Generation of a non-clashing name for the self memory variable (for step and reset functions) *)
let mk_self m =
let used name =
@@ -83,6 +89,8 @@ let mk_addr_var m var =
if List.exists (fun v -> v.var_id = s) vars then aux () else s
in aux ()
*)
+let pp_global_init_name fmt id = fprintf fmt "%s_INIT" id
+let pp_global_clear_name fmt id = fprintf fmt "%s_CLEAR" id
let pp_machine_memtype_name fmt id = fprintf fmt "struct %s_mem" id
let pp_machine_regtype_name fmt id = fprintf fmt "struct %s_reg" id
let pp_machine_alloc_name fmt id = fprintf fmt "%s_alloc" id
@@ -90,6 +98,8 @@ let pp_machine_static_declare_name fmt id = fprintf fmt "%s_DECLARE" id
let pp_machine_static_link_name fmt id = fprintf fmt "%s_LINK" id
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_init_name fmt id = fprintf fmt "%s_init" id
+let pp_machine_clear_name fmt id = fprintf fmt "%s_clear" id
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
let rec pp_c_dimension fmt dim =
@@ -116,16 +126,17 @@ let is_basic_c_type t =
let pp_basic_c_type fmt t =
match (Types.repr t).Types.tdesc with
- | Types.Tbool -> fprintf fmt "_Bool"
- | Types.Treal -> fprintf fmt "double"
- | Types.Tint -> fprintf fmt "int"
+ | Types.Tbool -> fprintf fmt "_Bool"
+ | Types.Treal when !Options.mpfr -> fprintf fmt "%s" Mpfr.mpfr_t
+ | Types.Treal -> fprintf fmt "double"
+ | Types.Tint -> fprintf fmt "int"
| _ -> assert false (* Not a basic C type. Do not handle arrays or pointers *)
let pp_c_type var fmt t =
let rec aux t pp_suffix =
match (Types.repr t).Types.tdesc with
| Types.Tclock t' -> aux t' pp_suffix
- | Types.Tbool | Types.Treal | Types.Tint
+ | Types.Tbool | Types.Tint | Types.Treal
-> fprintf fmt "%a %s%a" pp_basic_c_type t var pp_suffix ()
| Types.Tarray (d, t') ->
let pp_suffix' fmt () = fprintf fmt "%a[%a]" pp_suffix () pp_c_dimension d in
@@ -135,30 +146,28 @@ let pp_c_type var fmt t =
| Types.Tarrow (_, _) -> fprintf fmt "void (*%s)()" var
| _ -> 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 =
match (Types.repr t).Types.tdesc with
| Types.Tint -> pp_print_string fmt "0"
| Types.Tclock t' -> pp_c_initialize fmt t'
| Types.Tbool -> pp_print_string fmt "0"
- | Types.Treal -> pp_print_string fmt "0."
+ | Types.Treal when not !Options.mpfr -> pp_print_string fmt "0."
| Types.Tarray (d, t') when Dimension.is_dimension_const d ->
fprintf fmt "{%a}"
(Utils.fprintf_list ~sep:"," (fun fmt _ -> pp_c_initialize fmt t'))
(Utils.duplicate 0 (Dimension.size_const_dimension d))
| _ -> assert false
-
-
+ *)
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
| 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_real (c,e,s)-> pp_print_string fmt s (* Format.fprintf fmt "%ie%i" c e*)
+ (* | Const_float r -> pp_print_float fmt r *)
| Const_tag t -> pp_c_tag fmt t
| Const_array ca -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
| Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl
@@ -169,17 +178,16 @@ 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
+ match v.value_desc 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) -> (Format.eprintf "internal error: C_backend_common.pp_c_val %a@." pp_val v; assert false)
+ | Power (v, n) -> 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,
in order to avoid casting everywhere. *)
- if Types.is_array_type v.var_type
+ if Types.is_array_type v.var_type && not (Types.is_real_type v.var_type && !Options.mpfr)
then fprintf fmt "%a" pp_var v
else fprintf fmt "%s->_reg.%a" self pp_var v
| Fun (n, vl) -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl
@@ -191,9 +199,10 @@ let rec pp_c_val self pp_var fmt v =
- moreover, dereference memory array variables.
*)
let pp_c_var_read m fmt id =
+ (* mpfr_t is a static array, not treated as general arrays *)
if Types.is_address_type id.var_type
then
- if is_memory m id
+ if is_memory m id && not (Types.is_real_type id.var_type && !Options.mpfr)
then fprintf fmt "(*%s)" id.var_id
else fprintf fmt "%s" id.var_id
else
@@ -289,9 +298,9 @@ let pp_c_checks self fmt m =
let pp_registers_struct fmt m =
if m.mmemory <> []
then
- fprintf fmt "@[%a {@[%a; @]}@] _reg; "
+ fprintf fmt "@[%a {@[<v>%a;@ @]}@] _reg; "
pp_machine_regtype_name m.mname.node_id
- (Utils.fprintf_list ~sep:"; " pp_c_decl_struct_var) m.mmemory
+ (Utils.fprintf_list ~sep:";@ " pp_c_decl_struct_var) m.mmemory
else
()
@@ -302,11 +311,12 @@ let print_machine_struct fmt m =
else
begin
(* Define struct *)
- fprintf fmt "@[%a {@[%a%a%t@]};@]@."
+ fprintf fmt "@[%a {@[<v>%a%t%a%t@]};@]@."
pp_machine_memtype_name m.mname.node_id
pp_registers_struct m
- (Utils.fprintf_list ~sep:"; " pp_c_decl_instance_var) m.minstances
- (Utils.pp_final_char_if_non_empty "; " m.minstances)
+ (Utils.pp_final_char_if_non_empty "@ " m.mmemory)
+ (Utils.fprintf_list ~sep:";@ " pp_c_decl_instance_var) m.minstances
+ (Utils.pp_final_char_if_non_empty ";@ " m.minstances)
end
let print_machine_struct_from_header fmt inode =
@@ -324,6 +334,14 @@ let print_machine_struct_from_header fmt inode =
(* Prototype Printing functions *)
(********************************************************************************************)
+let print_global_init_prototype fmt baseNAME =
+ fprintf fmt "void %a ()"
+ pp_global_init_name baseNAME
+
+let print_global_clear_prototype fmt baseNAME =
+ fprintf fmt "void %a ()"
+ pp_global_clear_name baseNAME
+
let print_alloc_prototype fmt (name, static) =
fprintf fmt "%a * %a (%a)"
pp_machine_memtype_name name
@@ -338,6 +356,22 @@ let print_reset_prototype self fmt (name, static) =
pp_machine_memtype_name name
self
+let print_init_prototype self fmt (name, static) =
+ fprintf fmt "void %a (@[<v>%a%t%a *%s@])"
+ pp_machine_init_name name
+ (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static
+ (Utils.pp_final_char_if_non_empty ",@," static)
+ pp_machine_memtype_name name
+ self
+
+let print_clear_prototype self fmt (name, static) =
+ fprintf fmt "void %a (@[<v>%a%t%a *%s@])"
+ pp_machine_clear_name name
+ (Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) static
+ (Utils.pp_final_char_if_non_empty ",@," static)
+ pp_machine_memtype_name name
+ self
+
let print_stateless_prototype fmt (name, inputs, outputs) =
fprintf fmt "void %a (@[<v>@[%a%t@]@,@[%a@]@,@])"
pp_machine_step_name name
@@ -366,7 +400,17 @@ let print_stateless_C_prototype fmt (name, inputs, outputs) =
name
(Utils.fprintf_list ~sep:",@ " pp_c_decl_input_var) inputs
-
+let print_import_init fmt (Dep (local, basename, _, _)) =
+ if local then
+ let baseNAME = file_to_module_name basename in
+ fprintf fmt "%a();" pp_global_init_name baseNAME
+ else ()
+
+let print_import_clear fmt (Dep (local, basename, _, _)) =
+ if local then
+ let baseNAME = file_to_module_name basename in
+ fprintf fmt "%a();" pp_global_clear_name baseNAME
+ else ()
let print_import_prototype fmt (Dep (_, s, _, _)) =
fprintf fmt "#include \"%s.h\"@," s
@@ -383,6 +427,214 @@ let print_extern_alloc_prototypes fmt (Dep (_,_, header,_)) =
| _ -> ()
) header
+
+let pp_c_main_var_input fmt id =
+ fprintf fmt "%s" id.var_id
+
+let pp_c_main_var_output fmt id =
+ if Types.is_address_type id.var_type
+ then
+ fprintf fmt "%s" id.var_id
+ else
+ fprintf fmt "&%s" id.var_id
+
+let pp_main_call mname self fmt m (inputs: value_t list) (outputs: var_decl list) =
+ if fst (get_stateless_status m)
+ then
+ fprintf fmt "%a (%a%t%a);"
+ pp_machine_step_name mname
+ (Utils.fprintf_list ~sep:", " (pp_c_val self pp_c_main_var_input)) inputs
+ (Utils.pp_final_char_if_non_empty ", " inputs)
+ (Utils.fprintf_list ~sep:", " pp_c_main_var_output) outputs
+ else
+ fprintf fmt "%a (%a%t%a%t%s);"
+ pp_machine_step_name mname
+ (Utils.fprintf_list ~sep:", " (pp_c_val self pp_c_main_var_input)) inputs
+ (Utils.pp_final_char_if_non_empty ", " inputs)
+ (Utils.fprintf_list ~sep:", " pp_c_main_var_output) outputs
+ (Utils.pp_final_char_if_non_empty ", " outputs)
+ self
+
+let pp_c_var m self pp_var fmt var =
+ if is_memory m var
+ then
+ pp_c_val self pp_var fmt (mk_val (StateVar var) var.var_type)
+ else
+ pp_c_val self pp_var fmt (mk_val (LocalVar var) var.var_type)
+
+let pp_array_suffix fmt loop_vars =
+ Utils.fprintf_list ~sep:"" (fun fmt v -> fprintf fmt "[%s]" v) fmt loop_vars
+
+(* type directed initialization: useless wrt the lustre compilation model,
+ except for MPFR injection, where values are dynamically allocated
+*)
+let pp_initialize m self pp_var fmt var =
+ let rec aux indices fmt typ =
+ if Types.is_array_type typ
+ then
+ let dim = Types.array_type_dimension typ in
+ let idx = mk_loop_var m () in
+ fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
+ idx idx idx pp_c_dimension dim idx
+ (aux (idx::indices)) (Types.array_element_type typ)
+ else
+ let indices = List.rev indices in
+ let pp_var_suffix fmt var =
+ fprintf fmt "%a%a" (pp_c_var m self pp_var) var pp_array_suffix indices in
+ Mpfr.pp_inject_init pp_var_suffix fmt var
+ in
+ if !Options.mpfr && Types.is_real_type (Types.array_base_type var.var_type)
+ then
+ begin
+ reset_loop_counter ();
+ aux [] fmt var.var_type
+ end
+
+let pp_const_initialize pp_var fmt const =
+ let m = Machine_code.empty_machine in
+ let var = mk_val (LocalVar (Corelang.var_decl_of_const const)) const.const_type in
+ let rec aux indices value fmt typ =
+ if Types.is_array_type typ
+ then
+ let dim = Types.array_type_dimension typ in
+ let szl = Utils.enumerate (Dimension.size_const_dimension dim) in
+ let typ' = Types.array_element_type typ in
+ let value = match value with
+ | Const_array ca -> List.nth ca
+ | _ -> assert false in
+ fprintf fmt "%a"
+ (Utils.fprintf_list ~sep:"@," (fun fmt i -> aux (string_of_int i::indices) (value i) fmt typ')) szl
+ else
+ let indices = List.rev indices in
+ let pp_var_suffix fmt var =
+ fprintf fmt "%a%a" (pp_c_val "" pp_var) var pp_array_suffix indices in
+ let pp_value fmt value = pp_c_val "" pp_var fmt value in
+ begin
+ Mpfr.pp_inject_init pp_var_suffix fmt var;
+ fprintf fmt "@,";
+ Mpfr.pp_inject_real pp_var_suffix pp_c_const fmt var value
+ end
+ in
+ if !Options.mpfr && Types.is_real_type (Types.array_base_type const.const_type)
+ then
+ begin
+ reset_loop_counter ();
+ aux [] const.const_value fmt const.const_type
+ end
+
+(* type directed clear: useless wrt the lustre compilation model,
+ except for MPFR injection, where values are dynamically allocated
+*)
+let pp_clear m self pp_var fmt var =
+ let rec aux indices fmt typ =
+ if Types.is_array_type typ
+ then
+ let dim = Types.array_type_dimension typ in
+ let idx = mk_loop_var m () in
+ fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
+ idx idx idx pp_c_dimension dim idx
+ (aux (idx::indices)) (Types.array_element_type typ)
+ else
+ let indices = List.rev indices in
+ let pp_var_suffix fmt var =
+ fprintf fmt "%a%a" (pp_c_var m self pp_var) var pp_array_suffix indices in
+ Mpfr.pp_inject_clear pp_var_suffix fmt var
+ in
+ if !Options.mpfr && Types.is_real_type (Types.array_base_type var.var_type)
+ then
+ begin
+ reset_loop_counter ();
+ aux [] fmt var.var_type
+ end
+
+let pp_const_clear pp_var fmt const =
+ let m = Machine_code.empty_machine in
+ let var = Corelang.var_decl_of_const const in
+ let rec aux indices fmt typ =
+ if Types.is_array_type typ
+ then
+ let dim = Types.array_type_dimension typ in
+ let idx = mk_loop_var m () in
+ fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
+ idx idx idx pp_c_dimension dim idx
+ (aux (idx::indices)) (Types.array_element_type typ)
+ else
+ let indices = List.rev indices in
+ let pp_var_suffix fmt var =
+ fprintf fmt "%a%a" (pp_c_var m "" pp_var) var pp_array_suffix indices in
+ Mpfr.pp_inject_clear pp_var_suffix fmt var
+ in
+ if !Options.mpfr && Types.is_real_type (Types.array_base_type var.var_type)
+ then
+ begin
+ reset_loop_counter ();
+ aux [] fmt var.var_type
+ end
+
+let pp_call m self pp_read pp_write 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_read)) inputs
+ (Utils.pp_final_char_if_non_empty ", " inputs)
+ (Utils.fprintf_list ~sep:", " pp_write) 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_read)) inputs
+ (Utils.pp_final_char_if_non_empty ", " inputs)
+ (Utils.fprintf_list ~sep:", " pp_write) outputs
+
+let pp_basic_instance_call m self fmt i (inputs: value_t list) (outputs: var_decl list) =
+ pp_call m self (pp_c_var_read m) (pp_c_var_write m) fmt i inputs outputs
+(*
+ 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_instance_call m self fmt i (inputs: value_t list) (outputs: var_decl list) =
+ let pp_offset pp_var indices fmt var =
+ match indices with
+ | [] -> fprintf fmt "%a" pp_var var
+ | _ -> fprintf fmt "%a[%a]" pp_var var (Utils.fprintf_list ~sep:"][" pp_print_string) indices in
+ let rec aux indices fmt typ =
+ if Types.is_array_type typ
+ then
+ let dim = Types.array_type_dimension typ in
+ let idx = mk_loop_var m () in
+ fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
+ idx idx idx pp_c_dimension dim idx
+ (aux (idx::indices)) (Types.array_element_type typ)
+ else
+ let pp_read = pp_offset (pp_c_var_read m) indices in
+ let pp_write = pp_offset (pp_c_var_write m) indices in
+ pp_call m self pp_read pp_write fmt i inputs outputs
+ in
+ begin
+ reset_loop_counter ();
+ aux [] fmt (List.hd inputs).value_type
+ end
+
(* Local Variables: *)
(* compile-command:"make -C ../../.." *)
(* End: *)
diff --git a/src/backends/C/c_backend_header.ml b/src/backends/C/c_backend_header.ml
index ffe9575590e2e3f067856b31326073a5f09dcad7..272a3fb4df055f5a6401e3bd618cf6d0b391e769 100644
--- a/src/backends/C/c_backend_header.ml
+++ b/src/backends/C/c_backend_header.ml
@@ -34,10 +34,16 @@ module Main = functor (Mod: MODIFIERS_HDR) ->
struct
let print_import_standard fmt =
- fprintf fmt "#include \"%s/arrow.h\"@.@." Version.include_path
+ begin
+ if !Options.mpfr then
+ begin
+ fprintf fmt "#include <mpfr.h>@."
+ end;
+ fprintf fmt "#include \"%s/arrow.h\"@.@." Version.include_path
+ end
let rec print_static_val pp_var fmt v =
- match v with
+ match v.value_desc with
| Cst c -> pp_c_const fmt c
| LocalVar v -> pp_var fmt v
| Fun (n, vl) -> Basic_library.pp_c n (print_static_val pp_var) fmt vl
@@ -145,40 +151,51 @@ let print_static_alloc_macro fmt (m, attr, inst) =
inst
let print_machine_decl fmt m =
- Mod.print_machine_decl_prefix fmt m;
- if fst (get_stateless_status m) then
- begin
- fprintf fmt "extern %a;@.@."
- print_stateless_prototype
- (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
- end
- else
- begin
- (* Static allocation *)
- if !Options.static_mem
- then
- begin
- let inst = mk_instance m in
- let attr = mk_attribute m in
- fprintf fmt "%a@.%a@.%a@."
- print_static_declare_macro (m, attr, inst)
- print_static_link_macro (m, attr, inst)
- print_static_alloc_macro (m, attr, inst)
- end
- else
- begin
- (* Dynamic allocation *)
- fprintf fmt "extern %a;@.@."
- print_alloc_prototype (m.mname.node_id, m.mstatic)
- end;
- let self = mk_self m in
- fprintf fmt "extern %a;@.@."
- (print_reset_prototype self) (m.mname.node_id, m.mstatic);
+ begin
+ Mod.print_machine_decl_prefix fmt m;
+ if fst (get_stateless_status m) then
+ begin
+ fprintf fmt "extern %a;@.@."
+ print_stateless_prototype
+ (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
+ end
+ else
+ begin
+ (* Static allocation *)
+ if !Options.static_mem
+ then
+ begin
+ let inst = mk_instance m in
+ let attr = mk_attribute m in
+ fprintf fmt "%a@.%a@.%a@."
+ print_static_declare_macro (m, attr, inst)
+ print_static_link_macro (m, attr, inst)
+ print_static_alloc_macro (m, attr, inst)
+ end
+ else
+ begin
+ (* Dynamic allocation *)
+ fprintf fmt "extern %a;@.@."
+ print_alloc_prototype (m.mname.node_id, m.mstatic)
+ end;
+ let self = mk_self m in
+ fprintf fmt "extern %a;@.@."
+ (print_reset_prototype self) (m.mname.node_id, m.mstatic);
- fprintf fmt "extern %a;@.@."
- (print_step_prototype self)
- (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
- end
+ fprintf fmt "extern %a;@.@."
+ (print_step_prototype self)
+ (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs);
+
+ if !Options.mpfr then
+ begin
+ fprintf fmt "extern %a;@.@."
+ (print_init_prototype self) (m.mname.node_id, m.mstatic);
+
+ fprintf fmt "extern %a;@.@."
+ (print_clear_prototype self) (m.mname.node_id, m.mstatic);
+ end
+ end
+ end
let print_machine_alloc_decl fmt m =
Mod.print_machine_decl_prefix fmt m;
@@ -215,8 +232,7 @@ let print_machine_decl_from_header fmt inode =
print_stateless_C_prototype
(inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs)
end
- else (
- raise (Invalid_argument ("A node with declared prototype C cannot be stateful, it has to be a function")))
+ else (Format.eprintf "internal error: print_machine_decl_from_header"; assert false)
else
if inode.nodei_stateless then
begin
@@ -233,15 +249,26 @@ let print_machine_decl_from_header fmt inode =
let self = mk_new_name used "self" in
fprintf fmt "extern %a;@.@."
(print_reset_prototype self) (inode.nodei_id, static_inputs);
-
+
+ fprintf fmt "extern %a;@.@."
+ (print_init_prototype self) (inode.nodei_id, static_inputs);
+
+ fprintf fmt "extern %a;@.@."
+ (print_clear_prototype self) (inode.nodei_id, static_inputs);
+
fprintf fmt "extern %a;@.@."
(print_step_prototype self)
(inode.nodei_id, inode.nodei_inputs, inode.nodei_outputs)
end
let print_const_decl fmt cdecl =
- fprintf fmt "extern %a;@."
- (pp_c_type cdecl.const_id) cdecl.const_type
+ if !Options.mpfr && Types.is_real_type (Types.array_base_type cdecl.const_type)
+ then
+ fprintf fmt "extern %a;@."
+ (pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type)
+ else
+ fprintf fmt "extern %a;@."
+ (pp_c_type cdecl.const_id) cdecl.const_type
let rec pp_c_struct_type_field filename cpt fmt (label, tdesc) =
fprintf fmt "%a;" (pp_c_type_decl filename cpt label) tdesc
@@ -249,8 +276,10 @@ and pp_c_type_decl filename cpt var fmt tdecl =
match tdecl with
| Tydec_any -> assert false
| Tydec_int -> fprintf fmt "int %s" var
+ | Tydec_real when !Options.mpfr
+ -> fprintf fmt "%s %s" Mpfr.mpfr_t var
| Tydec_real -> fprintf fmt "double %s" var
- | Tydec_float -> fprintf fmt "float %s" var
+ (* | Tydec_float -> fprintf fmt "float %s" var *)
| Tydec_bool -> fprintf fmt "_Bool %s" var
| Tydec_clock ty -> pp_c_type_decl filename cpt var fmt ty
| Tydec_const c -> fprintf fmt "%s %s" c var
@@ -290,10 +319,9 @@ let reset_type_definitions, print_type_definition_from_header =
(********************************************************************************************)
let print_header header_fmt basename prog machines dependencies =
(* Include once: start *)
- let baseNAME = String.uppercase basename in
- let baseNAME = Str.global_replace (Str.regexp "\\.\\|\\ ") "_" baseNAME in
+ let baseNAME = file_to_module_name basename in
begin
- (* Print the svn version number and the supported C standard (C90 or C99) *)
+ (* Print the version number and the supported C standard (C90 or C99) *)
print_version header_fmt;
fprintf header_fmt "#ifndef _%s@.#define _%s@." baseNAME baseNAME;
pp_print_newline header_fmt ();
@@ -302,7 +330,7 @@ let print_header header_fmt basename prog machines dependencies =
print_import_standard header_fmt;
pp_print_newline header_fmt ();
(* imports dependencies *)
- fprintf header_fmt "/* Import Dependencies */@.";
+ fprintf header_fmt "/* Import dependencies */@.";
fprintf header_fmt "@[<v>";
List.iter (print_import_prototype header_fmt) dependencies;
fprintf header_fmt "@]@.";
@@ -314,8 +342,18 @@ let print_header header_fmt basename prog machines dependencies =
fprintf header_fmt "/* Global constant (declarations, definitions are in C file) */@.";
List.iter (fun c -> print_const_decl header_fmt (const_of_top c)) (get_consts prog);
pp_print_newline header_fmt ();
+ if !Options.mpfr then
+ begin
+ fprintf header_fmt "/* Global initialization declaration */@.";
+ fprintf header_fmt "extern %a;@.@."
+ print_global_init_prototype baseNAME;
+
+ fprintf header_fmt "/* Global clear declaration */@.";
+ fprintf header_fmt "extern %a;@.@."
+ print_global_clear_prototype baseNAME;
+ end;
(* Print the struct declarations of all machines. *)
- fprintf header_fmt "/* Struct declarations */@.";
+ fprintf header_fmt "/* Structs declarations */@.";
List.iter (print_machine_struct header_fmt) machines;
pp_print_newline header_fmt ();
(* Print the prototypes of all machines *)
@@ -329,8 +367,7 @@ let print_header header_fmt basename prog machines dependencies =
let print_alloc_header header_fmt basename prog machines dependencies =
(* Include once: start *)
- let baseNAME = String.uppercase basename in
- let baseNAME = Str.global_replace (Str.regexp "\\.\\|\\ ") "_" baseNAME in
+ let baseNAME = file_to_module_name basename in
begin
(* Print the svn version number and the supported C standard (C90 or C99) *)
print_version header_fmt;
@@ -362,14 +399,13 @@ let print_alloc_header header_fmt basename prog machines dependencies =
header. *)
let print_header_from_header header_fmt basename header =
(* Include once: start *)
- let baseNAME = String.uppercase basename in
- let baseNAME = Str.global_replace (Str.regexp "\\.\\|\\ ") "_" baseNAME in
+ let baseNAME = file_to_module_name basename in
let types = get_typedefs header in
let consts = get_consts header in
let nodes = get_imported_nodes header in
let dependencies = get_dependencies header in
begin
- (* Print the svn version number and the supported C standard (C90 or C99) *)
+ (* Print the version number and the supported C standard (C90 or C99) *)
print_version header_fmt;
fprintf header_fmt "#ifndef _%s@.#define _%s@." baseNAME baseNAME;
pp_print_newline header_fmt ();
@@ -395,8 +431,18 @@ let print_header_from_header header_fmt basename header =
fprintf header_fmt "/* Global constant (declarations, definitions are in C file) */@.";
List.iter (fun c -> print_const_decl header_fmt (const_of_top c)) consts;
pp_print_newline header_fmt ();
+ if !Options.mpfr then
+ begin
+ fprintf header_fmt "/* Global initialization declaration */@.";
+ fprintf header_fmt "extern %a;@.@."
+ print_global_init_prototype baseNAME;
+
+ fprintf header_fmt "/* Global clear declaration */@.";
+ fprintf header_fmt "extern %a;@.@."
+ print_global_clear_prototype baseNAME;
+ end;
(* Print the struct declarations of all machines. *)
- fprintf header_fmt "/* Struct declarations */@.";
+ fprintf header_fmt "/* Structs declarations */@.";
List.iter (fun node -> print_machine_struct_from_header header_fmt (imported_node_of_top node)) nodes;
pp_print_newline header_fmt ();
(* Print the prototypes of all machines *)
diff --git a/src/backends/C/c_backend_main.ml b/src/backends/C/c_backend_main.ml
index 578c6a3e4e936fba9bce0280c176566db3c4d7d5..4cfa48ea080a837d5ec5bd65294d5151a6c67d46 100644
--- a/src/backends/C/c_backend_main.ml
+++ b/src/backends/C/c_backend_main.ml
@@ -30,80 +30,140 @@ struct
(* Main related functions *)
(********************************************************************************************)
-let print_get_input fmt v =
- match (Types.repr v.var_type).Types.tdesc with
- | Types.Tint -> fprintf fmt "_get_int(\"%s\")" v.var_id
- | Types.Tbool -> fprintf fmt "_get_bool(\"%s\")" v.var_id
- | Types.Treal -> fprintf fmt "_get_double(\"%s\")" v.var_id
- | _ -> assert false
+let print_get_inputs fmt m =
+ let pi fmt (v', v) =
+ match (Types.unclock_type v.var_type).Types.tdesc with
+ | Types.Tint -> fprintf fmt "%s = _get_int(\"%s\")" v.var_id v'.var_id
+ | Types.Tbool -> fprintf fmt "%s = _get_bool(\"%s\")" v.var_id v'.var_id
+ | Types.Treal when !Options.mpfr -> fprintf fmt "mpfr_set_d(%s, _get_double(\"%s\"), %i)" v.var_id v'.var_id (Mpfr.mpfr_prec ())
+ | Types.Treal -> fprintf fmt "%s = _get_double(\"%s\")" v.var_id v'.var_id
+ | _ ->
+ begin
+ Global.main_node := !Options.main_node;
+ Format.eprintf "Code generation error: %a%a@."
+ pp_error Main_wrong_kind
+ Location.pp_loc v'.var_loc;
+ raise (Error (v'.var_loc, Main_wrong_kind))
+ end
+ in
+ List.iter2 (fun v' v -> fprintf fmt "@ %a;" pi (v', v)) m.mname.node_inputs m.mstep.step_inputs
-let print_put_outputs fmt ol =
- let po fmt o =
- match (Types.repr o.var_type).Types.tdesc with
- | Types.Tint -> fprintf fmt "_put_int(\"%s\", %s)" o.var_id o.var_id
- | Types.Tbool -> fprintf fmt "_put_bool(\"%s\", %s)" o.var_id o.var_id
- | Types.Treal -> fprintf fmt "_put_double(\"%s\", %s)" o.var_id o.var_id
+let print_put_outputs fmt m =
+ let po fmt (o', o) =
+ match (Types.unclock_type o.var_type).Types.tdesc with
+ | Types.Tint -> fprintf fmt "_put_int(\"%s\", %s)" o'.var_id o.var_id
+ | Types.Tbool -> fprintf fmt "_put_bool(\"%s\", %s)" o'.var_id o.var_id
+ | Types.Treal when !Options.mpfr -> fprintf fmt "_put_double(\"%s\", mpfr_get_d(%s, %s))" o'.var_id o.var_id (Mpfr.mpfr_rnd ())
+ | Types.Treal -> fprintf fmt "_put_double(\"%s\", %s)" o'.var_id o.var_id
| _ -> assert false
in
- List.iter (fprintf fmt "@ %a;" po) ol
+ List.iter2 (fun v' v -> fprintf fmt "@ %a;" po (v', v)) m.mname.node_outputs m.mstep.step_outputs
+
+let print_main_inout_declaration fmt m =
+ begin
+ fprintf fmt "/* Declaration of inputs/outputs variables */@ ";
+ List.iter
+ (fun v -> fprintf fmt "%a;@ " (pp_c_type v.var_id) v.var_type
+ ) m.mstep.step_inputs;
+ List.iter
+ (fun v -> fprintf fmt "%a;@ " (pp_c_type v.var_id) v.var_type
+ ) m.mstep.step_outputs
+ end
+
+let print_main_memory_allocation mname main_mem fmt m =
+ if not (fst (get_stateless_status m)) then
+ begin
+ fprintf fmt "@ /* Main memory allocation */@ ";
+ if (!Options.static_mem && !Options.main_node <> "")
+ then (fprintf fmt "%a(static,main_mem);@ " pp_machine_static_alloc_name mname)
+ else (fprintf fmt "%a *main_mem = %a();@ " pp_machine_memtype_name mname pp_machine_alloc_name mname);
+ fprintf fmt "@ /* Initialize the main memory */@ ";
+ fprintf fmt "%a(%s);@ " pp_machine_reset_name mname main_mem;
+ end
+
+let print_global_initialize fmt basename =
+ let mNAME = file_to_module_name basename in
+ fprintf fmt "@ /* Initialize global constants */@ %a();@ "
+ pp_global_init_name mNAME
+
+let print_global_clear fmt basename =
+ let mNAME = file_to_module_name basename in
+ fprintf fmt "@ /* Clear global constants */@ %a();@ "
+ pp_global_clear_name mNAME
+
+let print_main_initialize mname main_mem fmt m =
+ if not (fst (get_stateless_status m))
+ then
+ fprintf fmt "@ /* Initialize inputs, outputs and memories */@ %a%t%a%t%a(%s);@ "
+ (Utils.fprintf_list ~sep:"@ " (pp_initialize m main_mem (pp_c_var_read m))) m.mstep.step_inputs
+ (Utils.pp_newline_if_non_empty m.mstep.step_inputs)
+ (Utils.fprintf_list ~sep:"@ " (pp_initialize m main_mem (pp_c_var_read m))) m.mstep.step_outputs
+ (Utils.pp_newline_if_non_empty m.mstep.step_inputs)
+ pp_machine_init_name mname
+ main_mem
+ else
+ fprintf fmt "@ /* Initialize inputs and outputs */@ %a%t%a@ "
+ (Utils.fprintf_list ~sep:"@ " (pp_initialize m main_mem (pp_c_var_read m))) m.mstep.step_inputs
+ (Utils.pp_newline_if_non_empty m.mstep.step_inputs)
+ (Utils.fprintf_list ~sep:"@ " (pp_initialize m main_mem (pp_c_var_read m))) m.mstep.step_outputs
+
+let print_main_clear mname main_mem fmt m =
+ if not (fst (get_stateless_status m))
+ then
+ fprintf fmt "@ /* Clear inputs, outputs and memories */@ %a%t%a%t%a(%s);@ "
+ (Utils.fprintf_list ~sep:"@ " (pp_clear m main_mem (pp_c_var_read m))) m.mstep.step_inputs
+ (Utils.pp_newline_if_non_empty m.mstep.step_inputs)
+ (Utils.fprintf_list ~sep:"@ " (pp_clear m main_mem (pp_c_var_read m))) m.mstep.step_outputs
+ (Utils.pp_newline_if_non_empty m.mstep.step_inputs)
+ pp_machine_clear_name mname
+ main_mem
+ else
+ fprintf fmt "@ /* Clear inputs and outputs */@ %a%t%a@ "
+ (Utils.fprintf_list ~sep:"@ " (pp_clear m main_mem (pp_c_var_read m))) m.mstep.step_inputs
+ (Utils.pp_newline_if_non_empty m.mstep.step_inputs)
+ (Utils.fprintf_list ~sep:"@ " (pp_clear m main_mem (pp_c_var_read m))) m.mstep.step_outputs
+
+let print_main_loop mname main_mem fmt m =
+ let input_values =
+ List.map (fun v -> mk_val (LocalVar v) v.var_type)
+ m.mstep.step_inputs in
+ begin
+ fprintf fmt "@ ISATTY = isatty(0);@ ";
+ fprintf fmt "@ /* Infinite loop */@ ";
+ fprintf fmt "@[<v 2>while(1){@ ";
+ fprintf fmt "fflush(stdout);@ ";
+ fprintf fmt "%a@ %t%a"
+ print_get_inputs m
+ (fun fmt -> pp_main_call mname main_mem fmt m input_values m.mstep.step_outputs)
+ print_put_outputs m
+ end
-let print_main_fun machines m fmt =
+let print_main_code fmt basename m =
let mname = m.mname.node_id in
let main_mem =
if (!Options.static_mem && !Options.main_node <> "")
then "&main_mem"
else "main_mem" in
fprintf fmt "@[<v 2>int main (int argc, char *argv[]) {@ ";
- fprintf fmt "/* Declaration of inputs/outputs variables */@ ";
- List.iter
- (fun v -> fprintf fmt "%a = %a;@ " (pp_c_type v.var_id) v.var_type pp_c_initialize v.var_type
- ) m.mstep.step_inputs;
- List.iter
- (fun v -> fprintf fmt "%a = %a;@ " (pp_c_type v.var_id) v.var_type pp_c_initialize v.var_type
- ) m.mstep.step_outputs;
- fprintf fmt "@ /* Main memory allocation */@ ";
- if (!Options.static_mem && !Options.main_node <> "")
- then (fprintf fmt "%a(static,main_mem);@ " pp_machine_static_alloc_name mname)
- else (fprintf fmt "%a *main_mem = %a();@ " pp_machine_memtype_name mname pp_machine_alloc_name mname);
- fprintf fmt "@ /* Initialize the main memory */@ ";
- fprintf fmt "%a(%s);@ " pp_machine_reset_name mname main_mem;
- fprintf fmt "@ ISATTY = isatty(0);@ ";
- fprintf fmt "@ /* Infinite loop */@ ";
- fprintf fmt "@[<v 2>while(1){@ ";
- fprintf fmt "fflush(stdout);@ ";
- List.iter
- (fun v -> fprintf fmt "%s = %a;@ "
- v.var_id
- print_get_input v
- ) m.mstep.step_inputs;
- (match m.mstep.step_outputs with
- (* | [] -> ( *)
- (* fprintf fmt "%a(%a%t%s);@ " *)
- (* pp_machine_step_name mname *)
- (* (Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs *)
- (* (pp_final_char_if_non_empty ", " m.mstep.step_inputs) *)
- (* main_mem *)
- (* ) *)
- (* | [o] -> ( *)
- (* fprintf fmt "%s = %a(%a%t%a, %s);%a" *)
- (* o.var_id *)
- (* pp_machine_step_name mname *)
- (* (Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs *)
- (* (pp_final_char_if_non_empty ", " m.mstep.step_inputs) *)
- (* (Utils.fprintf_list ~sep:", " (fun fmt v -> fprintf fmt "&%s" v.var_id)) m.mstep.step_outputs *)
- (* main_mem *)
- (* print_put_outputs [o]) *)
- | _ -> (
- fprintf fmt "%a(%a%t%a, %s);%a"
- pp_machine_step_name mname
- (Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) m.mstep.step_inputs
- (Utils.pp_final_char_if_non_empty ", " m.mstep.step_inputs)
- (Utils.fprintf_list ~sep:", " (fun fmt v -> fprintf fmt "&%s" v.var_id)) m.mstep.step_outputs
- main_mem
- print_put_outputs m.mstep.step_outputs)
- );
- fprintf fmt "@]@ }@ ";
- fprintf fmt "return 1;";
+ print_main_inout_declaration fmt m;
+ print_main_memory_allocation mname main_mem fmt m;
+ if !Options.mpfr then
+ begin
+ print_global_initialize fmt basename;
+ print_main_initialize mname main_mem fmt m;
+ end;
+ print_main_loop mname main_mem fmt m;
+ if Scopes.Plugin.is_active () then
+ begin
+ fprintf fmt "@ %t" Scopes.Plugin.pp
+ end;
+ fprintf fmt "@]@ }@ @ ";
+ if !Options.mpfr then
+ begin
+ print_main_clear mname main_mem fmt m;
+ print_global_clear fmt basename;
+ end;
+ fprintf fmt "@ return 1;";
fprintf fmt "@]@ }@."
let print_main_header fmt =
@@ -118,7 +178,7 @@ let print_main_c main_fmt main_machine basename prog machines _ (*dependencies*)
(* Print the svn version number and the supported C standard (C90 or C99) *)
print_version main_fmt;
- print_main_fun machines main_machine main_fmt
+ print_main_code main_fmt basename main_machine
end
(* Local Variables: *)
diff --git a/src/backends/C/c_backend_makefile.ml b/src/backends/C/c_backend_makefile.ml
index 70371b40635e26fd83af6481e8ae457f4b7d9697..3bfee7e70f340fedf1efbe19333e42a5dc25cc49 100644
--- a/src/backends/C/c_backend_makefile.ml
+++ b/src/backends/C/c_backend_makefile.ml
@@ -18,7 +18,7 @@ let header_has_code header =
(fun top ->
match top.top_decl_desc with
| Const _ -> true
- | ImportedNode nd -> nd.nodei_in_lib = None
+ | ImportedNode nd -> nd.nodei_in_lib = []
| _ -> false
)
header
@@ -26,9 +26,7 @@ let header_has_code header =
let header_libs header =
List.fold_left (fun accu top ->
match top.top_decl_desc with
- | ImportedNode nd -> (match nd.nodei_in_lib with
- | None -> accu
- | Some lib -> Utils.list_union [lib] accu)
+ | ImportedNode nd -> Utils.list_union nd.nodei_in_lib accu
| _ -> accu
) [] header
@@ -73,10 +71,10 @@ let print_makefile basename nodename (dependencies: dep_t list) fmt =
(* Main binary *)
fprintf fmt "%s_%s:@." basename nodename;
- fprintf fmt "\t${GCC} -I${INC} -I. -c %s.c@." basename;
- fprintf fmt "\t${GCC} -I${INC} -I. -c %s_main.c@." basename;
+ fprintf fmt "\t${GCC} -O0 -I${INC} -I. -c %s.c@." basename;
+ fprintf fmt "\t${GCC} -O0 -I${INC} -I. -c %s_main.c@." basename;
fprintf_dependencies fmt dependencies;
- fprintf fmt "\t${GCC} -o %s_%s io_frontend.o %a %s.o %s_main.o %a@." basename nodename
+ fprintf fmt "\t${GCC} -O0 -o %s_%s io_frontend.o %a %s.o %s_main.o %a@." basename nodename
(Utils.fprintf_list ~sep:" " (fun fmt (Dep (_, s, _, _)) -> Format.fprintf fmt "%s.o" s))
(compiled_dependencies dependencies)
basename (* library .o *)
@@ -87,6 +85,8 @@ let print_makefile basename nodename (dependencies: dep_t list) fmt =
fprintf fmt "clean:@.";
fprintf fmt "\t\\rm -f *.o %s_%s@." basename nodename;
fprintf fmt "@.";
+ fprintf fmt ".PHONY: %s_%s@." basename nodename;
+ fprintf fmt "@.";
Mod.other_targets fmt basename nodename dependencies;
fprintf fmt "@.";
diff --git a/src/backends/C/c_backend_src.ml b/src/backends/C/c_backend_src.ml
index c8c06713286f0a921c669f4407bc1ccb8bcdaa36..0b08a7ebc0eb335493f65f43ca97295e0aa97363 100644
--- a/src/backends/C/c_backend_src.ml
+++ b/src/backends/C/c_backend_src.ml
@@ -30,42 +30,50 @@ 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].
*)
-let rec expansion_depth v =
- match v with
- | Cst (Const_array cl) -> 1 + List.fold_right (fun c -> max (expansion_depth (Cst c))) cl 0
- | Cst _
- | LocalVar _
- | StateVar _ -> 0
- | Fun (_, vl) -> List.fold_right (fun v -> max (expansion_depth v)) vl 0
- | Array vl -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0
- | Access (v, i) -> max 0 (expansion_depth v - 1)
- | Power (v, n) -> 0 (*1 + expansion_depth v*)
-
-let rec merge_static_loop_profiles lp1 lp2 =
- match lp1, lp2 with
- | [] , _ -> lp2
- | _ , [] -> lp1
- | p1 :: q1, p2 :: q2 -> (p1 || p2) :: merge_static_loop_profiles q1 q2
+ let rec expansion_depth v =
+ match v.value_desc with
+ | Cst cst -> expansion_depth_cst cst
+ | LocalVar _
+ | StateVar _ -> 0
+ | Fun (_, vl) -> List.fold_right (fun v -> max (expansion_depth v)) vl 0
+ | Array vl -> 1 + List.fold_right (fun v -> max (expansion_depth v)) vl 0
+ | Access (v, i) -> max 0 (expansion_depth v - 1)
+ | Power (v, n) -> 0 (*1 + expansion_depth v*)
+ and expansion_depth_cst c =
+ match c with
+ Const_array cl -> 1 + List.fold_right (fun c -> max (expansion_depth_cst c)) cl 0
+ | _ -> 0
+
+ let rec merge_static_loop_profiles lp1 lp2 =
+ match lp1, lp2 with
+ | [] , _ -> lp2
+ | _ , [] -> lp1
+ | p1 :: q1, p2 :: q2 -> (p1 || p2) :: merge_static_loop_profiles q1 q2
(* Returns a list of bool values, indicating whether the indices must be static or not *)
-let rec static_loop_profile v =
- match v with
- | Cst (Const_array cl) ->
- List.fold_right (fun c lp -> merge_static_loop_profiles lp (static_loop_profile (Cst c))) cl []
- | Cst _
- | LocalVar _
- | StateVar _ -> []
- | Fun (_, vl) -> List.fold_right (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
- | Array vl -> true :: List.fold_right (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
- | Access (v, i) -> (match (static_loop_profile v) with [] -> [] | _ :: q -> q)
- | Power (v, n) -> false :: static_loop_profile v
-
+ let rec static_loop_profile v =
+ match v.value_desc with
+ | Cst cst -> static_loop_profile_cst cst
+ | LocalVar _
+ | StateVar _ -> []
+ | Fun (_, vl) -> List.fold_right (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
+ | Array vl -> true :: List.fold_right (fun v lp -> merge_static_loop_profiles lp (static_loop_profile v)) vl []
+ | Access (v, i) -> (match (static_loop_profile v) with [] -> [] | _ :: q -> q)
+ | Power (v, n) -> false :: static_loop_profile v
+ and static_loop_profile_cst cst =
+ match cst with
+ Const_array cl -> List.fold_right
+ (fun c lp -> merge_static_loop_profiles lp (static_loop_profile_cst c))
+ cl
+ []
+ | _ -> []
+
+
let rec is_const_index v =
- match v with
+ match v.value_desc with
| Cst (Const_int _) -> true
| Fun (_, vl) -> List.for_all is_const_index vl
| _ -> false
@@ -108,7 +116,7 @@ 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_c_dimension (dimension_of_value i)
+ | LAcc i -> fprintf fmt "[%a]" pp_val i
(* Prints a suffix of loop variables for arrays *)
let pp_suffix fmt loop_vars =
@@ -121,26 +129,25 @@ let pp_suffix fmt loop_vars =
(* 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 *)
+ | Const_int i -> pp_print_int fmt i
+ | Const_real (_, _, s) -> pp_print_string fmt s
+ | 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
+ (*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.value_desc 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))
+ pp_value_suffix self var_type q pp_value fmt (mk_val (Cst (List.nth cl !r)) Type_predef.type_int)
| (_, LInt r) :: q, Array vl ->
let var_type = Types.array_element_type var_type in
pp_value_suffix self var_type q pp_value fmt (List.nth vl !r)
@@ -171,8 +178,17 @@ let rec pp_value_suffix self var_type loop_vars pp_value fmt value =
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
+let pp_c_val self pp_var fmt v =
+ pp_value_suffix self v.value_type [] pp_var fmt v
+
+let pp_basic_assign pp_var fmt typ var_name value =
+ if Types.is_real_type typ && !Options.mpfr
+ then
+ Mpfr.pp_inject_assign pp_var fmt var_name value
+ else
+ fprintf fmt "%a = %a;"
+ pp_var var_name
+ pp_var value
(* type_directed assignment: array vs. statically sized type
- [var_type]: type of variable to be assigned
@@ -180,49 +196,69 @@ let pp_c_val self pp_var fmt (t, v) =
- [value]: assigned value
- [pp_var]: printer for variables
*)
-(*
-let pp_assign_rec pp_var var_type var_name value =
- match (Types.repr var_type).Types.tdesc, value with
- | Types.Tarray (d, ty'), Array vl ->
- let szl = Utils.enumerate (Dimension.size_const_dimension d) in
- fprintf fmt "@[<v 2>{@,%a@]@,}"
- (Utils.fprintf_list ~sep:"@," (fun fmt i -> r := i; aux fmt q)) szl
- | Types.Tarray (d, ty'), Power (v, _) ->
- | Types.Tarray (d, ty'), _ ->
- | _ , _ ->
- fprintf fmt "%a = %a;"
- pp_var var_name
- (pp_value_suffix self loop_vars pp_var) value
-*)
let pp_assign m self pp_var fmt var_type var_name value =
let depth = expansion_depth value in
-(*Format.eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)
+ (*Format.eprintf "pp_assign %a %a %a %d@." Types.print_ty var_type pp_val var_name pp_val value depth;*)
let loop_vars = mk_loop_variables m var_type depth in
let reordered_loop_vars = reorder_loop_variables loop_vars in
- let rec aux fmt vars =
+ let rec aux typ fmt vars =
match vars with
| [] ->
- fprintf fmt "%a = %a;"
- (pp_value_suffix self var_type loop_vars pp_var) var_name
- (pp_value_suffix self var_type loop_vars pp_var) value
+ pp_basic_assign (pp_value_suffix self var_type loop_vars pp_var) fmt typ var_name value
| (d, LVar i) :: q ->
-(*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
+ let typ' = Types.array_element_type typ in
+ (*eprintf "pp_aux %a %s@." Dimension.pp_dimension d i;*)
fprintf fmt "@[<v 2>{@,int %s;@,for(%s=0;%s<%a;%s++)@,%a @]@,}"
- i i i Dimension.pp_dimension d i
- aux q
+ i i i pp_c_dimension d i
+ (aux typ') q
| (d, LInt r) :: q ->
-(*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
- let szl = Utils.enumerate (Dimension.size_const_dimension d) in
- fprintf fmt "@[<v 2>{@,%a@]@,}"
- (Utils.fprintf_list ~sep:"@," (fun fmt i -> r := i; aux fmt q)) szl
+ (*eprintf "pp_aux %a %d@." Dimension.pp_dimension d (!r);*)
+ let typ' = Types.array_element_type typ in
+ let szl = Utils.enumerate (Dimension.size_const_dimension d) in
+ fprintf fmt "@[<v 2>{@,%a@]@,}"
+ (Utils.fprintf_list ~sep:"@," (fun fmt i -> r := i; aux typ' fmt q)) szl
| _ -> assert false
in
begin
reset_loop_counter ();
(*reset_addr_counter ();*)
- aux fmt reordered_loop_vars
+ aux var_type fmt reordered_loop_vars;
+ (*Format.eprintf "end pp_assign@.";*)
end
+let pp_machine_reset (m: machine_t) self fmt inst =
+ let (node, static) =
+ try
+ List.assoc inst m.minstances
+ with Not_found -> (Format.eprintf "internal error: pp_machine_reset %s %s %s:@." 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 pp_machine_init (m: machine_t) self fmt inst =
+ let (node, static) =
+ try
+ List.assoc inst m.minstances
+ with Not_found -> (Format.eprintf "internal error: pp_machine_init %s %s %s@." m.mname.node_id self inst; raise Not_found) in
+ fprintf fmt "%a(%a%t%s->%s);"
+ pp_machine_init_name (node_name node)
+ (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
+ (Utils.pp_final_char_if_non_empty ", " static)
+ self inst
+
+let pp_machine_clear (m: machine_t) self fmt inst =
+ let (node, static) =
+ try
+ List.assoc inst m.minstances
+ with Not_found -> (Format.eprintf "internal error: pp_machine_clear %s %s %s@." m.mname.node_id self inst; raise Not_found) in
+ fprintf fmt "%a(%a%t%s->%s);"
+ pp_machine_clear_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
@@ -247,7 +283,7 @@ let has_c_prototype funname dependencies =
match imported_node_opt with
| 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
@@ -278,21 +314,10 @@ let pp_instance_call dependencies m self fmt i (inputs: value_t list) (outputs:
(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)) (Type_predef.type_bool, c)
+ (pp_c_val self (pp_c_var_read m)) 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)
@@ -305,15 +330,23 @@ and pp_machine_instr dependencies (m: machine_t) self fmt instr =
| MLocalAssign (i,v) ->
pp_assign
m self (pp_c_var_read m) fmt
- i.var_type (LocalVar i) v
+ i.var_type (mk_val (LocalVar i) i.var_type) v
| MStateAssign (i,v) ->
pp_assign
m self (pp_c_var_read m) fmt
- 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)))
+ i.var_type (mk_val (StateVar i) i.var_type) v
+ | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type) ->
+ pp_machine_instr dependencies m self fmt
+ (MLocalAssign (i0, mk_val (Fun (i, vl)) i0.var_type))
+ | MStep ([i0], i, vl) when has_c_prototype i dependencies ->
+ fprintf fmt "%a = %s(%a);"
+ (pp_c_val self (pp_c_var_read m)) (mk_val (LocalVar i0) i0.var_type)
+ i
+ (Utils.fprintf_list ~sep:", " (pp_c_val self (pp_c_var_read m))) vl
+ | MStep (il, i, vl) when Mpfr.is_homomorphic_fun i ->
+ pp_instance_call m self fmt i vl il
| MStep (il, i, vl) ->
- pp_instance_call dependencies m self fmt i vl il
+ pp_basic_instance_call 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
@@ -323,13 +356,18 @@ and pp_machine_instr dependencies (m: machine_t) self fmt instr =
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
+ (*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_typ, g)
+ (pp_c_val self (pp_c_var_read m)) g
(Utils.fprintf_list ~sep:"@," (pp_machine_branch dependencies m self)) hl
+ | MComment s ->
+ fprintf fmt "//%s@ " s
+
and pp_machine_branch dependencies m self fmt (t, h) =
- fprintf fmt "@[<v 2>case %a:@,%a@,break;@]" pp_c_tag t (Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) h
+ fprintf fmt "@[<v 2>case %a:@,%a@,break;@]"
+ pp_c_tag t
+ (Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) h
(********************************************************************************************)
@@ -337,9 +375,14 @@ and pp_machine_branch dependencies m self fmt (t, h) =
(********************************************************************************************)
let print_const_def fmt cdecl =
- fprintf fmt "%a = %a;@."
- (pp_c_type cdecl.const_id) cdecl.const_type
- pp_c_const cdecl.const_value
+ if !Options.mpfr && Types.is_real_type (Types.array_base_type cdecl.const_type)
+ then
+ fprintf fmt "%a;@."
+ (pp_c_type cdecl.const_id) (Types.dynamic_type cdecl.const_type)
+ else
+ fprintf fmt "%a = %a;@."
+ (pp_c_type cdecl.const_id) cdecl.const_type
+ pp_c_const cdecl.const_value
let print_alloc_instance fmt (i, (m, static)) =
@@ -374,36 +417,78 @@ let print_alloc_code fmt m =
(Utils.fprintf_list ~sep:"" print_alloc_array) array_mem
(Utils.fprintf_list ~sep:"" print_alloc_instance) m.minstances
+let print_stateless_init_code dependencies fmt m self =
+ let minit = List.map (function MReset i -> i | _ -> assert false) m.minit in
+ let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
+ fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
+ (print_init_prototype self) (m.mname.node_id, m.mstatic)
+ (* array mems *)
+ (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
+ (Utils.pp_final_char_if_non_empty ";@," array_mems)
+ (* memory initialization *)
+ (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
+ (Utils.pp_newline_if_non_empty m.mmemory)
+ (* sub-machines initialization *)
+ (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
+ (Utils.pp_newline_if_non_empty m.minit)
+
+let print_stateless_clear_code dependencies fmt m self =
+ let minit = List.map (function MReset i -> i | _ -> assert false) m.minit in
+ let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
+ fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
+ (print_clear_prototype self) (m.mname.node_id, m.mstatic)
+ (* array mems *)
+ (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
+ (Utils.pp_final_char_if_non_empty ";@," array_mems)
+ (* memory clear *)
+ (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
+ (Utils.pp_newline_if_non_empty m.mmemory)
+ (* sub-machines clear*)
+ (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
+ (Utils.pp_newline_if_non_empty m.minit)
+
let print_stateless_code dependencies fmt m =
let self = "__ERROR__" in
if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc; top_decl_owner = ""; top_decl_itf = false })
then
(* C99 code *)
- fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
+ fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%a%t%t@]@,}@.@."
print_stateless_prototype (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
(* locals *)
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) m.mstep.step_locals
(Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals)
+ (* locals initialization *)
+ (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mstep.step_locals
+ (Utils.pp_newline_if_non_empty m.mstep.step_locals)
(* check assertions *)
(pp_c_checks self) m
(* instrs *)
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.mstep.step_instrs
(Utils.pp_newline_if_non_empty m.mstep.step_instrs)
+ (* locals clear *)
+ (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mstep.step_locals
+ (Utils.pp_newline_if_non_empty m.mstep.step_locals)
(fun fmt -> fprintf fmt "return;")
else
(* C90 code *)
let (gen_locals, base_locals) = List.partition (fun v -> Types.is_generic_type v.var_type) m.mstep.step_locals in
let gen_calls = List.map (fun e -> let (id, _, _) = call_of_expr e in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
- fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
+ fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%a%t%t@]@,}@.@."
print_stateless_prototype (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs)
(* locals *)
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) base_locals
(Utils.pp_final_char_if_non_empty ";" base_locals)
+ (* locals initialization *)
+ (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mstep.step_locals
+ (Utils.pp_newline_if_non_empty m.mstep.step_locals)
(* check assertions *)
(pp_c_checks self) m
(* instrs *)
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.mstep.step_instrs
(Utils.pp_newline_if_non_empty m.mstep.step_instrs)
+ (* locals clear *)
+ (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mstep.step_locals
+ (Utils.pp_newline_if_non_empty m.mstep.step_locals)
(fun fmt -> fprintf fmt "return;")
let print_reset_code dependencies fmt m self =
@@ -417,12 +502,42 @@ let print_reset_code dependencies fmt m self =
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.minit
(Utils.pp_newline_if_non_empty m.minit)
+let print_init_code dependencies fmt m self =
+ let minit = List.map (function MReset i -> i | _ -> assert false) m.minit in
+ let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
+ fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
+ (print_init_prototype self) (m.mname.node_id, m.mstatic)
+ (* array mems *)
+ (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
+ (Utils.pp_final_char_if_non_empty ";@," array_mems)
+ (* memory initialization *)
+ (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mmemory
+ (Utils.pp_newline_if_non_empty m.mmemory)
+ (* sub-machines initialization *)
+ (Utils.fprintf_list ~sep:"@," (pp_machine_init m self)) minit
+ (Utils.pp_newline_if_non_empty m.minit)
+
+let print_clear_code dependencies fmt m self =
+ let minit = List.map (function MReset i -> i | _ -> assert false) m.minit in
+ let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
+ fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%treturn;@]@,}@.@."
+ (print_clear_prototype self) (m.mname.node_id, m.mstatic)
+ (* array mems *)
+ (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
+ (Utils.pp_final_char_if_non_empty ";@," array_mems)
+ (* memory clear *)
+ (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mmemory
+ (Utils.pp_newline_if_non_empty m.mmemory)
+ (* sub-machines clear*)
+ (Utils.fprintf_list ~sep:"@," (pp_machine_clear m self)) minit
+ (Utils.pp_newline_if_non_empty m.minit)
+
let print_step_code dependencies fmt m self =
if not (!Options.ansi && is_generic_node { top_decl_desc = Node m.mname; top_decl_loc = Location.dummy_loc; top_decl_owner = ""; top_decl_itf = false })
then
(* C99 code *)
let array_mems = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
- fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%t@]@,}@.@."
+ fprintf fmt "@[<v 2>%a {@,%a%t%a%t%a%t@,%a%a%t%a%t%t@]@,}@.@."
(print_step_prototype self) (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
(* locals *)
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) m.mstep.step_locals
@@ -430,26 +545,38 @@ let print_step_code dependencies fmt m self =
(* array mems *)
(Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
(Utils.pp_final_char_if_non_empty ";@," array_mems)
+ (* locals initialization *)
+ (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mstep.step_locals
+ (Utils.pp_newline_if_non_empty m.mstep.step_locals)
(* check assertions *)
(pp_c_checks self) m
(* instrs *)
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.mstep.step_instrs
(Utils.pp_newline_if_non_empty m.mstep.step_instrs)
+ (* locals clear *)
+ (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mstep.step_locals
+ (Utils.pp_newline_if_non_empty m.mstep.step_locals)
(fun fmt -> fprintf fmt "return;")
else
(* C90 code *)
let (gen_locals, base_locals) = List.partition (fun v -> Types.is_generic_type v.var_type) m.mstep.step_locals in
let gen_calls = List.map (fun e -> let (id, _, _) = call_of_expr e in mk_call_var_decl e.expr_loc id) m.mname.node_gencalls in
- fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
+ fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%a%t%t@]@,}@.@."
(print_step_prototype self) (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs)
(* locals *)
(Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) base_locals
(Utils.pp_final_char_if_non_empty ";" base_locals)
+ (* locals initialization *)
+ (Utils.fprintf_list ~sep:"@," (pp_initialize m self (pp_c_var_read m))) m.mstep.step_locals
+ (Utils.pp_newline_if_non_empty m.mstep.step_locals)
(* check assertions *)
(pp_c_checks self) m
(* instrs *)
(Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.mstep.step_instrs
(Utils.pp_newline_if_non_empty m.mstep.step_instrs)
+ (* locals clear *)
+ (Utils.fprintf_list ~sep:"@," (pp_clear m self (pp_c_var_read m))) m.mstep.step_locals
+ (Utils.pp_newline_if_non_empty m.mstep.step_locals)
(fun fmt -> fprintf fmt "return;")
@@ -457,6 +584,28 @@ let print_step_code dependencies fmt m self =
(* MAIN C file Printing functions *)
(********************************************************************************************)
+let print_global_init_code fmt basename prog dependencies =
+ let baseNAME = file_to_module_name basename in
+ let constants = List.map const_of_top (get_consts prog) in
+ fprintf fmt "@[<v 2>%a {@,static _Bool init = 0;@,@[<v 2>if (!init) { @,init = 1;@,%a%t%a@]@,}@,return;@]@,}@.@."
+ print_global_init_prototype baseNAME
+ (* constants *)
+ (Utils.fprintf_list ~sep:"@," (pp_const_initialize (pp_c_var_read Machine_code.empty_machine))) constants
+ (Utils.pp_final_char_if_non_empty "@," dependencies)
+ (* dependencies initialization *)
+ (Utils.fprintf_list ~sep:"@," print_import_init) dependencies
+
+let print_global_clear_code fmt basename prog dependencies =
+ let baseNAME = file_to_module_name basename in
+ let constants = List.map const_of_top (get_consts prog) in
+ fprintf fmt "@[<v 2>%a {@,static _Bool clear = 0;@,@[<v 2>if (!clear) { @,clear = 1;@,%a%t%a@]@,}@,return;@]@,}@.@."
+ print_global_clear_prototype baseNAME
+ (* constants *)
+ (Utils.fprintf_list ~sep:"@," (pp_const_clear (pp_c_var_read Machine_code.empty_machine))) constants
+ (Utils.pp_final_char_if_non_empty "@," dependencies)
+ (* dependencies initialization *)
+ (Utils.fprintf_list ~sep:"@," print_import_clear) dependencies
+
let print_machine dependencies fmt m =
if fst (get_stateless_status m) then
begin
@@ -477,17 +626,32 @@ let print_machine dependencies fmt m =
(* Reset function *)
print_reset_code dependencies fmt m self;
(* Step function *)
- print_step_code dependencies fmt m self
+ print_step_code dependencies fmt m self;
+
+ if !Options.mpfr then
+ begin
+ (* Init function *)
+ print_init_code dependencies fmt m self;
+ (* Clear function *)
+ print_clear_code dependencies fmt m self;
+ end
end
+let print_import_standard source_fmt =
+ begin
+ fprintf source_fmt "#include <assert.h>@.";
+ if not !Options.static_mem then
+ begin
+ fprintf source_fmt "#include <stdlib.h>@.";
+ end;
+ if !Options.mpfr then
+ begin
+ fprintf source_fmt "#include <mpfr.h>@.";
+ end
+ end
let print_lib_c source_fmt basename prog machines dependencies =
-
- fprintf source_fmt "#include <assert.h>@.";
- if not !Options.static_mem then
- begin
- fprintf source_fmt "#include <stdlib.h>@.";
- end;
+ print_import_standard source_fmt;
print_import_prototype source_fmt (Dep (true, basename, [], true (* assuming it is stateful *)));
pp_print_newline source_fmt ();
(* Print the svn version number and the supported C standard (C90 or C99) *)
@@ -502,7 +666,13 @@ let print_lib_c source_fmt basename prog machines dependencies =
fprintf source_fmt "@[<v>";
List.iter (fun c -> print_const_def source_fmt (const_of_top c)) (get_consts prog);
fprintf source_fmt "@]@.";
-
+ if !Options.mpfr then
+ begin
+ fprintf source_fmt "/* Global constants initialization */@.";
+ print_global_init_code source_fmt basename prog dependencies;
+ fprintf source_fmt "/* Global constants clearing */@.";
+ print_global_clear_code source_fmt basename prog dependencies;
+ end;
if not !Options.static_mem then
begin
fprintf source_fmt "/* External allocation function prototypes */@.";
diff --git a/src/backends/Horn/horn_backend.ml b/src/backends/Horn/horn_backend.ml
index 24f58617739c40f7d8d9faf751b4271ae9d57f54..61b77b59d2c562224fca065ae549e1c60a613743 100644
--- a/src/backends/Horn/horn_backend.ml
+++ b/src/backends/Horn/horn_backend.ml
@@ -50,7 +50,6 @@ let pp_conj pp fmt l =
| _ -> fprintf fmt "(and @[<v 0>%a@]@ )" (Utils.fprintf_list ~sep:" " pp) l
-
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x
let rename f = (fun v -> {v with var_id = f v.var_id } )
let rename_machine p = rename (fun n -> concat p n)
@@ -63,8 +62,13 @@ let rename_next_list = List.map rename_next
let get_machine machines node_name =
- List.find (fun m -> m.mname.node_id = node_name) machines
-
+ try
+ List.find (fun m -> m.mname.node_id = node_name) machines
+ with Not_found ->
+ begin
+ Format.eprintf "internal error: get_machine %s@." node_name;
+ assert false
+ end
let full_memory_vars machines machine =
let rec aux fst prefix m =
@@ -78,7 +82,6 @@ let full_memory_vars machines machine =
in
aux true machine.mname.node_id machine
-
let stateless_vars machines m =
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@
(rename_machine_list m.mname.node_id m.mstep.step_outputs)
@@ -111,8 +114,8 @@ let pp_horn_tag fmt t =
let rec pp_horn_const 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_real (c,e,s) -> assert false (* TODO rational pp_print_string fmt r *)
+ (* | Const_float r -> pp_print_float fmt r *)
| Const_tag t -> pp_horn_tag fmt t
| _ -> assert false
@@ -121,7 +124,7 @@ let rec pp_horn_const fmt c =
but an offset suffix may be added for array variables
*)
let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
- match v with
+ match v.value_desc with
| Cst c -> pp_horn_const fmt c
| Array _
| Access _ -> assert false (* no arrays *)
@@ -135,7 +138,7 @@ let rec pp_horn_val ?(is_lhs=false) self pp_var fmt v =
(* Prints a [value] indexed by the suffix list [loop_vars] *)
let rec pp_value_suffix self pp_value fmt value =
- match value with
+ match value.value_desc with
| Fun (n, vl) ->
Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
| _ ->
@@ -163,16 +166,16 @@ let pp_instance_call
self
(pp_horn_var m)
fmt
- o.var_type (LocalVar o) i1
+ o.var_type (mk_val (LocalVar o) o.var_type) i1
else
pp_assign
m self (pp_horn_var m) fmt
- o.var_type (LocalVar o) i2
-
+ o.var_type (mk_val (LocalVar o) o.var_type) i2
+
end
| name, _, _ ->
begin
- let target_machine = List.find (fun m -> m.mname.node_id = name) machines in
+ let target_machine = get_machine machines name in
if init then
Format.fprintf fmt "(%a %a%t%a%t%a)"
pp_machine_init_name (node_name n)
@@ -182,7 +185,7 @@ let pp_instance_call
(Utils.pp_final_char_if_non_empty " " inputs)
(* outputs *)
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
- (List.map (fun v -> LocalVar v) outputs)
+ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
(Utils.pp_final_char_if_non_empty " " outputs)
(* memories (next) *)
(Utils.fprintf_list ~sep:" " pp_var) (
@@ -197,7 +200,7 @@ let pp_instance_call
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) inputs
(Utils.pp_final_char_if_non_empty " " inputs)
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
- (List.map (fun v -> LocalVar v) outputs)
+ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
(Utils.pp_final_char_if_non_empty " " outputs)
(Utils.fprintf_list ~sep:" " pp_var) (
(rename_machine_list
@@ -220,7 +223,7 @@ let pp_instance_call
inputs
(Utils.pp_final_char_if_non_empty " " inputs)
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m)))
- (List.map (fun v -> LocalVar v) outputs)
+ (List.map (fun v -> mk_val (LocalVar v) v.var_type) outputs)
)
let pp_machine_init (m: machine_t) self fmt inst =
@@ -247,12 +250,12 @@ and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
| MLocalAssign (i,v) ->
pp_assign
m self (pp_horn_var m) fmt
- i.var_type (LocalVar i) v
+ i.var_type (mk_val (LocalVar i) i.var_type) v
| MStateAssign (i,v) ->
pp_assign
m self (pp_horn_var m) fmt
- i.var_type (StateVar i) v
- | MStep ([i0], i, vl) when Basic_library.is_internal_fun i ->
+ i.var_type (mk_val (StateVar i) i.var_type) v
+ | MStep ([i0], i, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (i, vl)) i0.var_type) ->
assert false (* This should not happen anymore *)
| MStep (il, i, vl) ->
pp_instance_call machines ~init:init m self fmt i vl il
@@ -264,6 +267,7 @@ and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
let el = try List.assoc tag_false hl with Not_found -> [] in
pp_conditional machines ~init:init m self fmt g tl el
else assert false (* enum type case *)
+ | MComment _ -> ()
(**************************************************************)
@@ -600,10 +604,6 @@ let traces_file fmt basename prog machines =
memories_old
in
- (* let pp_prefix_rev fmt prefix = *)
- (* Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix) *)
- (* in *)
-
let pp_prefix_rev fmt prefix =
Utils.fprintf_list ~sep:"." (fun fmt (id,n) -> fprintf fmt "(%s,%s)" id n.mname.node_id) fmt (List.rev prefix)
in
diff --git a/src/basic_library.ml b/src/basic_library.ml
index 7e35b8a4707702184fba76724b00c32b308f4615..e353ed28b43bbe179a2198974a0924c6da9ca0d5 100644
--- a/src/basic_library.ml
+++ b/src/basic_library.ml
@@ -111,9 +111,34 @@ let eval_env =
VE.initial
defs
-let internal_funs = ["+";"-";"*";"/";"mod";"&&";"||";"xor";"equi";"impl";"<";">";"<=";">=";"!=";"=";"uminus";"not"]
+let arith_funs = ["+";"-";"*";"/";"mod"; "uminus"]
+let bool_funs = ["&&";"||";"xor";"equi";"impl"; "not"]
+let rel_funs = ["<";">";"<=";">=";"!=";"="]
+
+let internal_funs = arith_funs@bool_funs@rel_funs
+
+let rec is_internal_fun x targs =
+(*Format.eprintf "is_internal_fun %s %a@." x Types.print_ty (List.hd targs);*)
+ match targs with
+ | [] -> assert false
+ | t::_ when Types.is_real_type t -> List.mem x internal_funs && not !Options.mpfr
+ | t::_ when Types.is_array_type t -> is_internal_fun x [Types.array_element_type t]
+ | _ -> List.mem x internal_funs
+
+let is_expr_internal_fun expr =
+ match expr.expr_desc with
+ | Expr_appl (f, e, _) -> is_internal_fun f (Types.type_list_of_type e.expr_type)
+ | _ -> assert false
+
+let is_value_internal_fun v =
+ match v.value_desc with
+ | Fun (f, vl) -> is_internal_fun f (List.map (fun v -> v.value_type) vl)
+ | _ -> assert false
+
+let is_homomorphic_fun x =
+ List.mem x internal_funs
-let is_internal_fun x =
+let is_stateless_fun x =
List.mem x internal_funs
let pp_c i pp_val fmt vl =
diff --git a/src/causality.ml b/src/causality.ml
index 00efa5430444f442100b588759a61d47b95b1269..e616ec5fee8ab2ad408c7da01534c8e193508ac5 100644
--- a/src/causality.ml
+++ b/src/causality.ml
@@ -225,7 +225,7 @@ let add_eq_dependencies mems inputs node_vars eq (g, g') =
| Expr_arrow (e1, e2) -> add_dep lhs_is_mem lhs e2 (add_dep lhs_is_mem lhs e1 g)
| Expr_when (e, c, _) -> add_dep lhs_is_mem lhs e (add_var lhs_is_mem lhs c g)
| Expr_appl (f, e, None) ->
- if Basic_library.is_internal_fun f
+ if Basic_library.is_expr_internal_fun rhs
(* tuple component-wise dependency for internal operators *)
then
List.fold_right (add_dep lhs_is_mem lhs) (expr_list_of_expr e) g
@@ -278,7 +278,7 @@ module NodeDep = struct
| Expr_pre e
| Expr_when (e,_,_) -> get_expr_calls prednode e
| Expr_appl (id,e, _) ->
- if not (Basic_library.is_internal_fun id) && prednode id
+ if not (Basic_library.is_expr_internal_fun expr) && prednode id
then ESet.add expr (get_expr_calls prednode e)
else (get_expr_calls prednode e)
diff --git a/src/clock_calculus.ml b/src/clock_calculus.ml
index ee201a880f60b37691cf4e0f8e6ec1566000628b..879d4313f800333e05c8f07368d7d7cd748e867c 100755
--- a/src/clock_calculus.ml
+++ b/src/clock_calculus.ml
@@ -608,7 +608,7 @@ and clock_subtyping_arg env ?(sub=true) real_arg formal_clock =
(* computes clocks for node application *)
and clock_appl env f args clock_reset loc =
let args = expr_list_of_expr args in
- if Basic_library.is_internal_fun f && List.exists is_tuple_expr args
+ if Basic_library.is_homomorphic_fun f && List.exists is_tuple_expr args
then
let args = Utils.transpose_list (List.map expr_list_of_expr args) in
Clocks.clock_of_clock_list (List.map (fun args -> clock_call env f args clock_reset loc) args)
diff --git a/src/clocks.ml b/src/clocks.ml
index a172d89783d18989e1a7fe23376afbe5d7301602..7b703487051ed2a74c7f8fb896e51613e52f05db 100755
--- a/src/clocks.ml
+++ b/src/clocks.ml
@@ -123,6 +123,9 @@ let rec print_ck_long fmt ck =
let new_id = ref (-1)
+let rec bottom =
+ { cdesc = Clink bottom; cid = -666; cscoped = false }
+
let new_ck desc scoped =
incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped}
diff --git a/src/compiler_common.ml b/src/compiler_common.ml
index f375d06a707913c8bf92272e6a9b2aaf7a7d9922..44dd47a7c831618f51f8e59b26733ebebc45d5a3 100644
--- a/src/compiler_common.ml
+++ b/src/compiler_common.ml
@@ -14,6 +14,13 @@ open Format
open LustreSpec
open Corelang
+let check_main () =
+ if !Options.main_node = "" then
+ begin
+ eprintf "Code generation error: %a@." pp_error No_main_specified;
+ raise (Error (Location.dummy_loc, No_main_specified))
+ end
+
let create_dest_dir () =
begin
if not (Sys.file_exists !Options.dest_dir) then
@@ -43,7 +50,7 @@ let parse_header own filename =
close_in h_in;
header
with
- | (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc ->
+ | (Parse.Error err) as exc ->
Parse.report_error err;
raise exc
| Corelang.Error (loc, err) as exc -> (
@@ -69,7 +76,7 @@ let parse_source source_name =
close_in s_in;
prog
with
- | (Lexer_lustre.Error err) | (Parse.Syntax_err err) as exc ->
+ | (Parse.Error err) as exc ->
Parse.report_error err;
raise exc
| Corelang.Error (loc, err) as exc ->
@@ -78,6 +85,16 @@ let parse_source source_name =
Location.pp_loc loc;
raise exc
+let expand_automata decls =
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. expanding automata@ ");
+ try
+ Automata.expand_decls decls
+ with (Corelang.Error (loc, err)) as exc ->
+ eprintf "Automata error: %a%a@."
+ Corelang.pp_error err
+ Location.pp_loc loc;
+ raise exc
+
let check_stateless_decls decls =
Log.report ~level:1 (fun fmt -> fprintf fmt ".. checking stateless/stateful status@ ");
try
@@ -88,6 +105,16 @@ let check_stateless_decls decls =
Location.pp_loc loc;
raise exc
+let force_stateful_decls decls =
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. forcing stateful status@ ");
+ try
+ Stateless.force_prog decls
+ with (Stateless.Error (loc, err)) as exc ->
+ eprintf "Stateless status error: %a%a@."
+ Stateless.pp_error err
+ Location.pp_loc loc;
+ raise exc
+
let type_decls env decls =
Log.report ~level:1 (fun fmt -> fprintf fmt ".. typing@ ");
let new_env =
diff --git a/src/corelang.ml b/src/corelang.ml
index 857209ec6e00c1a1a4a8b3ebfa2596ea7b8ea9c7..07eeff427b0000814893c5c81461783d93619d78 100755
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -245,14 +245,14 @@ let mktop = mktop_decl Location.dummy_loc Version.include_path false
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
-let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float})
+(* let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float}) *)
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})
let type_table =
Utils.create_hashtable 20 [
Tydec_int , top_int_type;
Tydec_bool , top_bool_type;
- Tydec_float, top_float_type;
+ (* Tydec_float, top_float_type; *)
Tydec_real , top_real_type
]
@@ -270,7 +270,7 @@ let print_type_table fmt () =
let rec is_user_type typ =
match typ with
| Tydec_int | Tydec_bool | Tydec_real
- | Tydec_float | Tydec_any | Tydec_const _ -> false
+ (* | Tydec_float *) | Tydec_any | Tydec_const _ -> false
| Tydec_clock typ' -> is_user_type typ'
| _ -> true
@@ -289,7 +289,7 @@ let rec coretype_equal ty1 ty2 =
| _ , Tydec_const _ -> coretype_equal ty2 ty1
| Tydec_int , Tydec_int
| Tydec_real , Tydec_real
- | Tydec_float , Tydec_float
+ (* | Tydec_float , Tydec_float *)
| Tydec_bool , Tydec_bool -> true
| Tydec_clock ty1 , Tydec_clock ty2 -> coretype_equal ty1 ty2
| Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
@@ -461,7 +461,7 @@ let rec dimension_of_expr expr =
match expr.expr_desc with
| Expr_const c -> dimension_of_const expr.expr_loc c
| Expr_ident id -> mkdim_ident expr.expr_loc id
- | Expr_appl (f, args, None) when Basic_library.is_internal_fun f ->
+ | Expr_appl (f, args, None) when Basic_library.is_expr_internal_fun expr ->
let k = Types.get_static_value (Env.lookup_value Basic_library.type_env f) in
if k = None then raise InvalidDimension;
mkdim_appl expr.expr_loc f (List.map dimension_of_expr (expr_list_of_expr args))
@@ -501,7 +501,7 @@ let mk_new_node_name nd id =
mk_new_name used id
let get_var id var_list =
- List.find (fun v -> v.var_id = id) var_list
+ List.find (fun v -> v.var_id = id) var_list
let get_node_var id node =
get_var id (get_node_vars node)
@@ -579,7 +579,7 @@ let get_node_interface nd =
nodei_stateless = nd.node_dec_stateless;
nodei_spec = nd.node_spec;
nodei_prototype = None;
- nodei_in_lib = None;
+ nodei_in_lib = [];
}
(************************************************************************)
@@ -624,16 +624,15 @@ let rec rename_carrier rename cck =
let eq_replace_rhs_var pvar fvar eq =
let pvar l = List.exists pvar l in
let rec replace lhs rhs =
- { rhs with expr_desc = replace_desc lhs rhs.expr_desc }
- and replace_desc lhs rhs_desc =
+ { rhs with expr_desc =
match lhs with
| [] -> assert false
- | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc
+ | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs.expr_desc else rhs.expr_desc
| _ ->
- (match rhs_desc with
+ (match rhs.expr_desc with
| Expr_tuple tl ->
Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
- | Expr_appl (f, arg, None) when Basic_library.is_internal_fun f ->
+ | Expr_appl (f, arg, None) when Basic_library.is_expr_internal_fun rhs ->
let args = expr_list_of_expr arg in
Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
| Expr_array _
@@ -643,8 +642,8 @@ let rec rename_carrier rename cck =
| Expr_ident _
| Expr_appl _ ->
if pvar lhs
- then expr_desc_replace_var fvar rhs_desc
- else rhs_desc
+ then expr_desc_replace_var fvar rhs.expr_desc
+ else rhs.expr_desc
| Expr_ite (c, t, e) -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
| Expr_arrow (e1, e2) -> Expr_arrow (replace lhs e1, replace lhs e2)
| Expr_fby (e1, e2) -> Expr_fby (replace lhs e1, replace lhs e2)
@@ -654,6 +653,7 @@ let rec rename_carrier rename cck =
| Expr_merge (i, hl) -> let i' = if pvar lhs then fvar i else i
in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
)
+ }
in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
@@ -792,15 +792,15 @@ let pp_prog_clock fmt prog =
Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
let pp_error fmt = function
- | Main_not_found ->
- fprintf fmt "cannot compile node %s: could not find the node definition.@."
- !Options.main_node
+ Main_not_found ->
+ fprintf fmt "Could not find the definition of main node %s.@."
+ !Global.main_node
| Main_wrong_kind ->
fprintf fmt
- "name %s does not correspond to a (non-imported) node definition.@."
- !Options.main_node
+ "Node %s does not correspond to a valid main node definition.@."
+ !Global.main_node
| No_main_specified ->
- fprintf fmt "no main node specified.@."
+ fprintf fmt "No main node specified (use -node option)@."
| Unbound_symbol sym ->
fprintf fmt
"%s is undefined.@."
@@ -844,7 +844,7 @@ let mk_internal_node id =
nodei_stateless = Types.get_static_value ty <> None;
nodei_spec = spec;
nodei_prototype = None;
- nodei_in_lib = None;
+ nodei_in_lib = [];
})
let add_internal_funs () =
@@ -927,10 +927,8 @@ let rec substitute_expr vars_to_replace defs e =
*)
let rec get_expr_calls nodes e =
- get_calls_expr_desc nodes e.expr_desc
-and get_calls_expr_desc nodes expr_desc =
let get_calls = get_expr_calls nodes in
- match expr_desc with
+ match e.expr_desc with
| Expr_const _
| Expr_ident _ -> Utils.ISet.empty
| Expr_tuple el
@@ -944,7 +942,7 @@ and get_calls_expr_desc nodes expr_desc =
| Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
| Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty hl
| Expr_appl (i, e', i') ->
- if Basic_library.is_internal_fun i then
+ if Basic_library.is_expr_internal_fun e then
(get_calls e')
else
let calls = Utils.ISet.add i (get_calls e') in
diff --git a/src/corelang.mli b/src/corelang.mli
index d4a1d5689f2c337a4698c3f420e02f7970acd843..e68fded179067dee8febe6aaeabb5796e26eb83f 100755
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -29,6 +29,8 @@ val mktop_decl: Location.t -> ident -> bool -> top_decl_desc -> top_decl
val mkpredef_call: Location.t -> ident -> expr list -> expr
val mk_new_name: (ident -> bool) -> ident -> ident
val mk_new_node_name: node_desc -> ident -> ident
+val mktop: top_decl_desc -> top_decl
+
val node_table : (ident, top_decl) Hashtbl.t
val print_node_table: Format.formatter -> unit -> unit
@@ -134,7 +136,7 @@ val copy_prog: top_decl list -> top_decl list
val mkeexpr: Location.t -> expr -> eexpr
val merge_node_annot: node_annot -> node_annot -> node_annot
val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr
-val update_expr_annot: ident -> expr -> LustreSpec.expr_annot -> expr
+val update_expr_annot: ident -> expr -> expr_annot -> expr
(* val mkpredef_call: Location.t -> ident -> eexpr list -> eexpr*)
(* Local Variables: *)
diff --git a/src/env.ml b/src/env.ml
index 31111bb59225979aae7d0254c583a75e8cf8e371..9fc32db2e9504a8e0406f90f3529d3ed01e9f70c 100755
--- a/src/env.ml
+++ b/src/env.ml
@@ -13,6 +13,7 @@
clock-calculus. *)
open Utils
+type 'a t = 'a IMap.t
(* Same namespace for nodes, variables and constants *)
let initial = IMap.empty
diff --git a/src/inliner.ml b/src/inliner.ml
index 1a2dd1034d7042c705fcf0392db24650e23cca93..50ac9b813e24b47d88c8f60d439bde55a431d0c8 100644
--- a/src/inliner.ml
+++ b/src/inliner.ml
@@ -64,6 +64,7 @@ We select the called node equations and variables.
the resulting expression is tuple_of_renamed_outputs
TODO: convert the specification/annotation/assert and inject them
+DONE: annotations
TODO: deal with reset
*)
let inline_call node orig_expr args reset locals caller =
@@ -136,10 +137,14 @@ in
})
node.node_asserts
in
+ let annots' =
+ Plugins.inline_annots rename node.node_annot
+ in
expr,
inputs'@outputs'@locals'@locals,
assign_inputs::eqs',
- asserts'
+ asserts',
+ annots'
@@ -156,27 +161,27 @@ let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
let inline_node = inline_node ~selection_on_annotation:selection_on_annotation in
let inline_tuple el =
- List.fold_right (fun e (el_tail, locals, eqs, asserts) ->
- let e', locals', eqs', asserts' = inline_expr e locals node nodes in
- e'::el_tail, locals', eqs'@eqs, asserts@asserts'
- ) el ([], locals, [], [])
+ List.fold_right (fun e (el_tail, locals, eqs, asserts, annots) ->
+ let e', locals', eqs', asserts', annots' = inline_expr e locals node nodes in
+ e'::el_tail, locals', eqs'@eqs, asserts@asserts', annots@annots'
+ ) el ([], locals, [], [], [])
in
let inline_pair e1 e2 =
- let el', l', eqs', asserts' = inline_tuple [e1;e2] in
+ let el', l', eqs', asserts', annots' = inline_tuple [e1;e2] in
match el' with
- | [e1'; e2'] -> e1', e2', l', eqs', asserts'
+ | [e1'; e2'] -> e1', e2', l', eqs', asserts', annots'
| _ -> assert false
in
let inline_triple e1 e2 e3 =
- let el', l', eqs', asserts' = inline_tuple [e1;e2;e3] in
+ let el', l', eqs', asserts', annots' = inline_tuple [e1;e2;e3] in
match el' with
- | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts'
+ | [e1'; e2'; e3'] -> e1', e2', e3', l', eqs', asserts', annots'
| _ -> assert false
in
match expr.expr_desc with
| Expr_appl (id, args, reset) ->
- let args', locals', eqs', asserts' = inline_expr args locals node nodes in
+ let args', locals', eqs', asserts', annots' = inline_expr args locals node nodes in
if List.exists (check_node_name id) nodes && (* the current node call is provided
as arguments nodes *)
(not selection_on_annotation || is_inline_expr expr) (* and if selection on annotation is activated,
@@ -188,68 +193,70 @@ let rec inline_expr ?(selection_on_annotation=false) expr locals node nodes =
with Not_found -> (assert false) in
let called = node_of_top called in
let called' = inline_node called nodes in
- let expr, locals', eqs'', asserts'' =
+ let expr, locals', eqs'', asserts'', annots'' =
inline_call called' expr args' reset locals' node in
- expr, locals', eqs'@eqs'', asserts'@asserts''
+ expr, locals', eqs'@eqs'', asserts'@asserts'', annots'@annots''
else
(* let _ = Format.eprintf "Not inlining call to %s@." id in *)
{ expr with expr_desc = Expr_appl(id, args', reset)},
locals',
eqs',
- asserts'
+ asserts',
+ annots'
(* For other cases, we just keep the structure, but convert sub-expressions *)
| Expr_const _
- | Expr_ident _ -> expr, locals, [], []
+ | Expr_ident _ -> expr, locals, [], [], []
| Expr_tuple el ->
- let el', l', eqs', asserts' = inline_tuple el in
- { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts'
+ let el', l', eqs', asserts', annots' = inline_tuple el in
+ { expr with expr_desc = Expr_tuple el' }, l', eqs', asserts', annots'
| Expr_ite (g, t, e) ->
- let g', t', e', l', eqs', asserts' = inline_triple g t e in
- { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts'
+ let g', t', e', l', eqs', asserts', annots' = inline_triple g t e in
+ { expr with expr_desc = Expr_ite (g', t', e') }, l', eqs', asserts', annots'
| Expr_arrow (e1, e2) ->
- let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
- { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts'
+ let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
+ { expr with expr_desc = Expr_arrow (e1', e2') } , l', eqs', asserts', annots'
| Expr_fby (e1, e2) ->
- let e1', e2', l', eqs', asserts' = inline_pair e1 e2 in
- { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts'
+ let e1', e2', l', eqs', asserts', annots' = inline_pair e1 e2 in
+ { expr with expr_desc = Expr_fby (e1', e2') }, l', eqs', asserts', annots'
| Expr_array el ->
- let el', l', eqs', asserts' = inline_tuple el in
- { expr with expr_desc = Expr_array el' }, l', eqs', asserts'
+ let el', l', eqs', asserts', annots' = inline_tuple el in
+ { expr with expr_desc = Expr_array el' }, l', eqs', asserts', annots'
| Expr_access (e, dim) ->
- let e', l', eqs', asserts' = inline_expr e locals node nodes in
- { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts'
+ let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
+ { expr with expr_desc = Expr_access (e', dim) }, l', eqs', asserts', annots'
| Expr_power (e, dim) ->
- let e', l', eqs', asserts' = inline_expr e locals node nodes in
- { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts'
+ let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
+ { expr with expr_desc = Expr_power (e', dim) }, l', eqs', asserts', annots'
| Expr_pre e ->
- let e', l', eqs', asserts' = inline_expr e locals node nodes in
- { expr with expr_desc = Expr_pre e' }, l', eqs', asserts'
+ let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
+ { expr with expr_desc = Expr_pre e' }, l', eqs', asserts', annots'
| Expr_when (e, id, label) ->
- let e', l', eqs', asserts' = inline_expr e locals node nodes in
- { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts'
+ let e', l', eqs', asserts', annots' = inline_expr e locals node nodes in
+ { expr with expr_desc = Expr_when (e', id, label) }, l', eqs', asserts', annots'
| Expr_merge (id, branches) ->
- let el, l', eqs', asserts' = inline_tuple (List.map snd branches) in
+ let el, l', eqs', asserts', annots' = inline_tuple (List.map snd branches) in
let branches' = List.map2 (fun (label, _) v -> label, v) branches el in
- { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts'
+ { expr with expr_desc = Expr_merge (id, branches') }, l', eqs', asserts', annots'
and inline_node ?(selection_on_annotation=false) node nodes =
try copy_node (Hashtbl.find inline_table node.node_id)
with Not_found ->
let inline_expr = inline_expr ~selection_on_annotation:selection_on_annotation in
- let new_locals, eqs, asserts =
- List.fold_left (fun (locals, eqs, asserts) eq ->
- let eq_rhs', locals', new_eqs', asserts' =
+ let new_locals, eqs, asserts, annots =
+ List.fold_left (fun (locals, eqs, asserts, annots) eq ->
+ let eq_rhs', locals', new_eqs', asserts', annots' =
inline_expr eq.eq_rhs locals node nodes
in
- locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts
- ) (node.node_locals, [], node.node_asserts) (get_node_eqs node)
+ locals', { eq with eq_rhs = eq_rhs' }::new_eqs'@eqs, asserts'@asserts, annots'@annots
+ ) (node.node_locals, [], node.node_asserts, node.node_annot) (get_node_eqs node)
in
let inlined =
{ node with
node_locals = new_locals;
node_stmts = List.map (fun eq -> Eq eq) eqs;
node_asserts = asserts;
+ node_annot = annots;
}
in
begin
@@ -363,6 +370,11 @@ let witness filename main_name orig inlined type_env clock_env =
in
let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
let new_prog = others@nodes_origs@nodes_inlined@main in
+(*
+ let _ = Typing.type_prog type_env new_prog in
+ let _ = Clock_calculus.clock_prog clock_env new_prog in
+*)
+
let witness_file = (Options.get_witness_dir filename) ^ "/" ^ "inliner_witness.lus" in
let witness_out = open_out witness_file in
let witness_fmt = Format.formatter_of_out_channel witness_out in
@@ -387,7 +399,6 @@ let global_inline basename prog type_env clock_env =
| _ -> main_opt, nodes, top::others)
prog (None, [], [])
in
-
(* Recursively each call of a node in the top node is replaced *)
let main_node = Utils.desome main_node in
let main_node' = inline_all_calls main_node other_nodes in
diff --git a/src/lexerLustreSpec.mll b/src/lexerLustreSpec.mll
index da4ca6caeab124ec8928ca365b423c35b634e4fc..869aa31dddc2531ae5534c2242a6a6ed073aec62 100644
--- a/src/lexerLustreSpec.mll
+++ b/src/lexerLustreSpec.mll
@@ -15,9 +15,9 @@
open Parser_lustre
open Utils
- let str_buf = Buffer.create 1024
-
exception Error of Location.t
+
+ let str_buf = Buffer.create 1024
(* As advised by Caml documentation. This way a single lexer rule is
used to handle all the possible keywords. *)
@@ -44,7 +44,7 @@ let keyword_table =
"wcet", WCET;
"int", TINT;
"bool", TBOOL;
- "float", TFLOAT;
+ (* "float", TFLOAT; *)
"real", TREAL;
"clock", TCLOCK;
"not", NOT;
@@ -86,11 +86,12 @@ rule token = parse
token lexbuf }
| blank +
{token lexbuf}
- | '-'? ['0'-'9'] ['0'-'9']* '.' ['0'-'9']*
- {FLOAT (float_of_string (Lexing.lexeme lexbuf))}
+ | (('-'? ['0'-'9'] ['0'-'9']* as l) '.' (['0'-'9']* as r)) as s
+ {REAL (Num.num_of_string (l^r), String.length r, s)}
+ | (('-'? ['0'-'9']+ as l) '.' (['0'-'9']+ as r) ('E'|'e') (('+'|'-') ['0'-'9'] ['0'-'9']* as exp)) as s
+ {REAL (Num.num_of_string (l^r), String.length r + -1 * int_of_string exp, s)}
| '-'? ['0'-'9']+
{INT (int_of_string (Lexing.lexeme lexbuf)) }
- | '-'? ['0'-'9']+ '.' ['0'-'9']+ ('E'|'e') ('+'|'-') ['0'-'9'] ['0'-'9'] as s {REAL s}
(* | '/' (['_' 'A'-'Z' 'a'-'z'] ['A'-'Z' 'a'-'z' '_' '0'-'9']* '/')+ as s
{IDENT s}
*)
@@ -126,10 +127,10 @@ rule token = parse
| "^" {POWER}
| '"' { Buffer.clear str_buf; string_parse lexbuf }
| eof { EOF }
- | _ { raise (Error (Location.curr lexbuf)) }
+ | _ { raise (Parse.Error (Location.curr lexbuf, Unexpected_eof)) }
and comment_line n = parse
| eof
- { raise (Error (Location.curr lexbuf)) }
+ { raise (Parse.Error (Location.curr lexbuf, Unfinished_comment)) }
| "(*"
{ comment_line (n+1) lexbuf }
| "*)"
@@ -139,6 +140,7 @@ and comment_line n = parse
comment_line n lexbuf }
| _ { comment_line n lexbuf }
and string_parse = parse
+ | eof { raise (Parse.Error (Location.curr lexbuf, Unfinished_string)) }
| "\\\"" as s { Buffer.add_string str_buf s; string_parse lexbuf}
| '"' { STRING (Buffer.contents str_buf) }
| _ as c { Buffer.add_char str_buf c; string_parse lexbuf }
@@ -146,18 +148,20 @@ and string_parse = parse
{
let annot s =
- let lb = Lexing.from_string s in
+ let lexbuf = Lexing.from_string s in
try
- Parser_lustre.lustre_annot(* ParserLustreSpec.lustre_annot *) token lb
+ Parser_lustre.lustre_annot(* ParserLustreSpec.lustre_annot *) token lexbuf
with Parsing.Parse_error as _e -> (
Format.eprintf "Lexing error at position %a:@.unexpected token %s@.@?"
- (fun fmt p -> Format.fprintf fmt "%s l%i c%i" p.Lexing.pos_fname p.Lexing.pos_lnum p.Lexing.pos_cnum) lb.Lexing.lex_curr_p
- (Lexing.lexeme lb);
- raise Parsing.Parse_error)
+ (fun fmt p -> Format.fprintf fmt "%s l%i c%i" p.Lexing.pos_fname p.Lexing.pos_lnum p.Lexing.pos_cnum) lexbuf.Lexing.lex_curr_p
+ (Lexing.lexeme lexbuf);
+ raise (Error (Location.curr lexbuf)))
let spec s =
- let lb = Lexing.from_string s in
- Parser_lustre.lustre_spec (*ParserLustreSpec.lustre_spec*) token lb
-
+ let lexbuf = Lexing.from_string s in
+ try
+ Parser_lustre.lustre_spec (*ParserLustreSpec.lustre_spec*) token lexbuf
+ with Parsing.Parse_error ->
+ raise (Error (Location.curr lexbuf))
}
diff --git a/src/lexer_lustre.mll b/src/lexer_lustre.mll
index 6fa09b53675bcf7fb9888084e80b7496ab849656..8f01a25b51282b94e22c1444d80dccc583733919 100755
--- a/src/lexer_lustre.mll
+++ b/src/lexer_lustre.mll
@@ -13,8 +13,6 @@
open Parser_lustre
open Utils
-exception Error of Location.t
-
(* As advised by Caml documentation. This way a single lexer rule is
used to handle all the possible keywords. *)
let keyword_table =
@@ -48,7 +46,7 @@ let keyword_table =
"type", TYPE;
"int", TINT;
"bool", TBOOL;
- "float", TFLOAT;
+ (* "float", TFLOAT; *)
"real", TREAL;
"clock", TCLOCK;
"not", NOT;
@@ -75,13 +73,13 @@ let make_annot lexbuf s =
try
let ann = LexerLustreSpec.annot s in
ANNOT ann
- with _ -> (Format.eprintf "Impossible to parse the following annotation:@.%s@.@?" s; exit 1)
+ with LexerLustreSpec.Error loc -> raise (Parse.Error (Location.shift (Location.curr lexbuf) loc, Annot_error s))
let make_spec lexbuf s =
try
let ns = LexerLustreSpec.spec s in
NODESPEC ns
- with _ -> (Format.eprintf "Impossible to parse the following node specification:@.%s@.@?" s; exit 1)
+ with LexerLustreSpec.Error loc -> raise (Parse.Error (Location.shift (Location.curr lexbuf) loc, Node_spec_error s))
}
@@ -108,11 +106,12 @@ rule token = parse
token lexbuf }
| blank +
{token lexbuf}
-| ['0'-'9'] ['0'-'9']* '.' ['0'-'9']*
- {FLOAT (float_of_string (Lexing.lexeme lexbuf))}
+| ((['0'-'9']+ as l) '.' (['0'-'9']* as r) ('E'|'e') (('+'|'-')? ['0'-'9']+ as exp)) as s
+ {REAL (Num.num_of_string (l^r), String.length r + -1 * int_of_string exp , s)}
+| ((['0'-'9']+ as l) '.' (['0'-'9']* as r)) as s
+ {REAL (Num.num_of_string (l^r), String.length r, s)}
| ['0'-'9']+
{INT (int_of_string (Lexing.lexeme lexbuf)) }
-| ['0'-'9']+ '.' ['0'-'9']+ ('E'|'e') ('+'|'-') ['0'-'9'] ['0'-'9']* as s {REAL s}
| "tel." {TEL}
| "tel;" {TEL}
| "#open" { OPEN }
@@ -158,11 +157,11 @@ rule token = parse
| "^" {POWER}
| '"' {QUOTE}
| eof { EOF }
-| _ { raise (Error (Location.curr lexbuf)) }
+| _ { raise (Parse.Error (Location.curr lexbuf, Undefined_token (Lexing.lexeme lexbuf))) }
and comment n = parse
| eof
- { raise (Error (Location.curr lexbuf)) }
+ { raise (Parse.Error (Location.curr lexbuf, Unfinished_comment)) }
| "(*"
{ comment (n+1) lexbuf }
| "*)"
@@ -173,10 +172,12 @@ and comment n = parse
| _ { comment n lexbuf }
and annot_singleline = parse
+ | eof { make_annot lexbuf (Buffer.contents buf) }
| newline { incr_line lexbuf; make_annot lexbuf (Buffer.contents buf) }
| _ as c { Buffer.add_char buf c; annot_singleline lexbuf }
and annot_multiline n = parse
+ | eof { raise (Parse.Error (Location.curr lexbuf, Unfinished_annot)) }
| "*)" as s {
if n > 0 then
(Buffer.add_string buf s; annot_multiline (n-1) lexbuf)
@@ -187,10 +188,12 @@ and annot_multiline n = parse
| _ as c { Buffer.add_char buf c; annot_multiline n lexbuf }
and spec_singleline = parse
+ | eof { make_spec lexbuf (Buffer.contents buf) }
| newline { incr_line lexbuf; make_spec lexbuf (Buffer.contents buf) }
| _ as c { Buffer.add_char buf c; spec_singleline lexbuf }
and spec_multiline n = parse
+ | eof { raise (Parse.Error (Location.curr lexbuf, Unfinished_node_spec)) }
| "*)" as s { if n > 0 then
(Buffer.add_string buf s; spec_multiline (n-1) lexbuf)
else
diff --git a/src/liveness.ml b/src/liveness.ml
index 21b716df1f8f441f41ea8846e0748fc601b454c7..23bd59449713ec8472605153f35c2cafb4b547e1 100755
--- a/src/liveness.ml
+++ b/src/liveness.ml
@@ -115,7 +115,7 @@ let remove_roots ctx =
(* checks whether a variable is aliasable,
depending on its (address) type *)
let is_aliasable var =
- Types.is_address_type var.var_type
+ (not (!Options.mpfr && Types.is_real_type var.var_type)) && Types.is_address_type var.var_type
(* checks whether a variable [v] is an input of the [var] equation, with an address type.
if so, [var] could not safely reuse/alias [v], should [v] be dead in the caller node,
diff --git a/src/location.ml b/src/location.ml
index 3b99fde85aaad526085523e45b2fb4142846bfa0..ea2584c399e9667110102d447c56ae073bfa6c11 100755
--- a/src/location.ml
+++ b/src/location.ml
@@ -34,7 +34,20 @@ let init lexbuf fname =
Lexing.pos_bol = 0;
Lexing.pos_cnum = 0;
}
-
+
+let shift_pos pos1 pos2 =
+ assert (pos1.Lexing.pos_fname = pos2.Lexing.pos_fname);
+ {Lexing.pos_fname = pos1.Lexing.pos_fname;
+ Lexing.pos_lnum = pos1.Lexing.pos_lnum + pos2.Lexing.pos_lnum;
+ Lexing.pos_bol = pos1.Lexing.pos_bol + pos2.Lexing.pos_bol;
+ Lexing.pos_cnum =if pos2.Lexing.pos_lnum = 1 then pos1.Lexing.pos_cnum + pos2.Lexing.pos_cnum else pos2.Lexing.pos_cnum
+ }
+
+let shift loc1 loc2 =
+ {loc_start = shift_pos loc1.loc_start loc2.loc_start;
+ loc_end = shift_pos loc1.loc_start loc2.loc_end
+ }
+
let symbol_rloc () =
{
loc_start = Parsing.symbol_start_pos ();
diff --git a/src/lusic.ml b/src/lusic.ml
index a1835f38ee08f805f466479480baf0acaa7c8c00..76ed1611815d7ecba6ed48cdf5878e67cdf4dedd 100644
--- a/src/lusic.ml
+++ b/src/lusic.ml
@@ -33,7 +33,7 @@ let extract_header dirname basename prog =
let owner = dirname ^ "/" ^ basename in
List.fold_right
(fun decl header ->
-(*Format.eprintf "Lusic.extract_header: owner = %s decl_owner = %s@." owner decl.top_decl_owner;*)
+ (*Format.eprintf "Lusic.extract_header: header = %B, owner = %s, decl_owner = %s@." decl.top_decl_itf owner decl.top_decl_owner;*)
if decl.top_decl_itf || decl.top_decl_owner <> owner then header else
match decl.top_decl_desc with
| Node nd -> { decl with top_decl_desc = ImportedNode (Corelang.get_node_interface nd) } :: header
@@ -51,6 +51,7 @@ let write_lusic lusi (header : top_decl list) basename extension =
let target_name = basename ^ extension in
let outchan = open_out_bin target_name in
begin
+ (*Format.eprintf "write_lusic: %i items.@." (List.length header);*)
Marshal.to_channel outchan (Version.number, lusi : string * bool) [];
Marshal.to_channel outchan (header : top_decl list) [];
close_out outchan
@@ -89,6 +90,7 @@ let print_lusic_to_h basename extension =
let h_fmt = formatter_of_out_channel h_out in
begin
assert (not lusic.obsolete);
+ (*Format.eprintf "lusic to h: %i items.@." (List.length lusic.contents);*)
Typing.uneval_prog_generics lusic.contents;
Clock_calculus.uneval_prog_generics lusic.contents;
Header.print_header_from_header h_fmt (Filename.basename basename) lusic.contents;
diff --git a/src/lustreSpec.ml b/src/lustreSpec.ml
index 4202fe412f55ae631629b0dd34dc4c3b0490cec0..991c5ed7102f5071d178efd3bce0c383da5e725f 100644
--- a/src/lustreSpec.ml
+++ b/src/lustreSpec.ml
@@ -24,7 +24,7 @@ and type_dec_desc =
| Tydec_any
| Tydec_int
| Tydec_real
- | Tydec_float
+ (* | Tydec_float *)
| Tydec_bool
| Tydec_clock of type_dec_desc
| Tydec_const of ident
@@ -50,8 +50,7 @@ and clock_dec_desc =
type constant =
| Const_int of int
- | Const_real of string
- | Const_float of float
+ | Const_real of Num.num * int * string (* (a, b, c) means a * 10^-b. c is the original string *)
| Const_array of constant list
| Const_tag of label
| Const_string of string (* used only for annotations *)
@@ -188,7 +187,7 @@ type imported_node_desc =
nodei_stateless: bool;
nodei_spec: node_annot option;
nodei_prototype: string option;
- nodei_in_lib: string option;
+ nodei_in_lib: string list;
}
type const_desc =
@@ -220,6 +219,33 @@ type dep_t = Dep of
* (top_decl list)
* bool (* is stateful *)
+
+(************ Machine code types *************)
+
+type value_t =
+ {
+ value_desc: value_t_desc;
+ value_type: Types.type_expr;
+ value_annot: expr_annot option
+ }
+and value_t_desc =
+ | Cst of constant
+ | LocalVar of var_decl
+ | StateVar of var_decl
+ | Fun of ident * value_t list
+ | Array of value_t list
+ | Access of value_t * value_t
+ | Power of value_t * value_t
+
+type instr_t =
+ | MLocalAssign of var_decl * value_t
+ | MStateAssign of var_decl * value_t
+ | MReset of ident
+ | MStep of var_decl list * ident * value_t list
+ | MBranch of value_t * (label * instr_t list) list
+ | MComment of string
+
+
type error =
Main_not_found
| Main_wrong_kind
diff --git a/src/machine_code.ml b/src/machine_code.ml
index cd1fc9d71d48603edb1b71966c2bba042deb6b66..770462ff4b7088c55b7492162cfa652291ba8ca3 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -21,25 +21,9 @@ module OrdVarDecl:Map.OrderedType with type t=var_decl =
module ISet = Set.Make(OrdVarDecl)
-type value_t =
- | Cst of constant
- | LocalVar of var_decl
- | StateVar of var_decl
- | Fun of ident * value_t list
- | Array of value_t list
- | Access of value_t * value_t
- | Power of value_t * value_t
-
-type instr_t =
- | MLocalAssign of var_decl * value_t
- | MStateAssign of var_decl * value_t
- | MReset of ident
- | MStep of var_decl list * ident * value_t list
- | MBranch of value_t * (label * instr_t list) list
-
let rec pp_val fmt v =
- match v with
- | Cst c -> Printers.pp_const fmt c
+ match v.value_desc with
+ | Cst c -> Printers.pp_const fmt c
| LocalVar v -> Format.pp_print_string fmt v.var_id
| StateVar v -> Format.pp_print_string fmt v.var_id
| Array vl -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val) vl
@@ -61,6 +45,7 @@ let rec pp_instr fmt i =
Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
pp_val g
(Utils.fprintf_list ~sep:"@," pp_branch) hl
+ | MComment s -> Format.pp_print_string fmt s
and pp_branch fmt (t, h) =
Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," pp_instr) h
@@ -119,6 +104,12 @@ let pp_machine fmt m =
(fun fmt -> match m.mspec with | None -> () | Some spec -> Printers.pp_spec fmt spec)
(Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
+let rec is_const_value v =
+ match v.value_desc with
+ | Cst _ -> true
+ | Fun (id, args) -> Basic_library.is_value_internal_fun v && List.for_all is_const_value args
+ | _ -> false
+
(* Returns the declared stateless status and the computed one. *)
let get_stateless_status m =
(m.mname.node_dec_stateless, Utils.desome m.mname.node_stateless)
@@ -177,29 +168,73 @@ let arrow_top_decl =
top_decl_loc = Location.dummy_loc
}
+let mk_val v t = { value_desc = v;
+ value_type = t;
+ value_annot = None }
+
let arrow_machine =
let state = "_first" in
let var_state = dummy_var_decl state (Types.new_ty Types.Tbool) in
let var_input1 = List.nth arrow_desc.node_inputs 0 in
let var_input2 = List.nth arrow_desc.node_inputs 1 in
let var_output = List.nth arrow_desc.node_outputs 0 in
+ let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in
+ let t_arg = Types.new_univar () in (* TODO Xavier: c'est bien la bonne def ? *)
{
mname = arrow_desc;
mmemory = [var_state];
mcalls = [];
minstances = [];
- minit = [MStateAssign(var_state, Cst (const_of_bool true))];
- mconst = [];
+ minit = [MStateAssign(var_state, cst true)];
mstatic = [];
+ mconst = [];
mstep = {
step_inputs = arrow_desc.node_inputs;
step_outputs = arrow_desc.node_outputs;
step_locals = [];
step_checks = [];
- step_instrs = [conditional (StateVar var_state)
- [MStateAssign(var_state, Cst (const_of_bool false));
- MLocalAssign(var_output, LocalVar var_input1)]
- [MLocalAssign(var_output, LocalVar var_input2)] ];
+ step_instrs = [conditional (mk_val (StateVar var_state) Type_predef.type_bool)
+ [MStateAssign(var_state, cst false);
+ MLocalAssign(var_output, mk_val (LocalVar var_input1) t_arg)]
+ [MLocalAssign(var_output, mk_val (LocalVar var_input2) t_arg)] ];
+ step_asserts = [];
+ };
+ mspec = None;
+ mannot = [];
+ }
+
+let empty_desc =
+ {
+ node_id = arrow_id;
+ node_type = Types.bottom;
+ node_clock = Clocks.bottom;
+ node_inputs= [];
+ node_outputs= [];
+ node_locals= [];
+ node_gencalls = [];
+ node_checks = [];
+ node_asserts = [];
+ node_stmts= [];
+ node_dec_stateless = true;
+ node_stateless = Some true;
+ node_spec = None;
+ node_annot = []; }
+
+let empty_machine =
+ {
+ mname = empty_desc;
+ mmemory = [];
+ mcalls = [];
+ minstances = [];
+ minit = [];
+ mstatic = [];
+ mconst = [];
+ mstep = {
+ step_inputs = [];
+ step_outputs = [];
+ step_locals = [];
+ step_checks = [];
+ step_instrs = [];
step_asserts = [];
};
mspec = None;
@@ -233,14 +268,21 @@ let translate_ident node (m, si, j, d, s) id =
try (* id is a node var *)
let var_id = get_node_var id node in
if ISet.exists (fun v -> v.var_id = id) m
- then StateVar var_id
- else LocalVar var_id
+ then mk_val (StateVar var_id) var_id.var_type
+ else mk_val (LocalVar var_id) var_id.var_type
with Not_found ->
try (* id is a constant *)
- LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)))
+ let vdecl = (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))) in
+ mk_val (LocalVar vdecl) vdecl.var_type
with Not_found ->
(* id is a tag *)
- Cst (Const_tag id)
+ (* DONE construire une liste des enum declarés et alors chercher dedans la liste
+ qui contient id *)
+ try
+ let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
+ mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
+ with Not_found -> (Format.eprintf "internal error: Machine_code.translate_ident %s" id;
+ assert false)
let rec control_on_clock node ((m, si, j, d, s) as args) ck inst =
match (Clocks.repr ck).cdesc with
@@ -292,36 +334,36 @@ let specialize_op expr =
| "C" -> specialize_to_c expr
| _ -> expr
-let rec translate_expr ?(ite=false) node ((m, si, j, d, s) as args) expr =
+let rec translate_expr node ((m, si, j, d, s) as args) expr =
let expr = specialize_op expr in
- match expr.expr_desc with
- | Expr_const v -> Cst v
- | Expr_ident x -> translate_ident node args x
- | Expr_array el -> Array (List.map (translate_expr node args) el)
- | Expr_access (t, i) -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))
- | Expr_power (e, n) -> Power (translate_expr node args e, translate_expr node args (expr_of_dimension n))
- | Expr_tuple _
- | Expr_arrow _
- | Expr_fby _
- | Expr_pre _ -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
- | Expr_when (e1, _, _) -> translate_expr node args e1
- | Expr_merge (x, _) -> raise NormalizationError
- | Expr_appl (id, e, _) when Basic_library.is_internal_fun id ->
- let nd = node_from_name id in
- Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
- | Expr_ite (g,t,e) -> (
- (* special treatment depending on the active backend. For horn backend, ite
- are preserved in expression. While they are removed for C or Java
- backends. *)
- match !Options.output with
- | "horn" ->
- Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
- | ("C" | "java") when ite ->
- Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
- | _ ->
- (Format.eprintf "option:%s@." !Options.output; Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
- )
- | _ -> raise NormalizationError
+ let value_desc =
+ match expr.expr_desc with
+ | Expr_const v -> Cst v
+ | Expr_ident x -> (translate_ident node args x).value_desc
+ | Expr_array el -> Array (List.map (translate_expr node args) el)
+ | Expr_access (t, i) -> Access (translate_expr node args t, translate_expr node args (expr_of_dimension i))
+ | Expr_power (e, n) -> Power (translate_expr node args e, translate_expr node args (expr_of_dimension n))
+ | Expr_tuple _
+ | Expr_arrow _
+ | Expr_fby _
+ | Expr_pre _ -> (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
+ | Expr_when (e1, _, _) -> (translate_expr node args e1).value_desc
+ | Expr_merge (x, _) -> raise NormalizationError
+ | Expr_appl (id, e, _) when Basic_library.is_expr_internal_fun expr ->
+ let nd = node_from_name id in
+ Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
+ | Expr_ite (g,t,e) -> (
+ (* special treatment depending on the active backend. For horn backend, ite
+ are preserved in expression. While they are removed for C or Java
+ backends. *)
+ match !Options.output with | "horn" ->
+ Fun ("ite", [translate_expr node args g; translate_expr node args t; translate_expr node args e])
+ | "C" | "java" | _ ->
+ (Printers.pp_expr Format.err_formatter expr; Format.pp_print_flush Format.err_formatter (); raise NormalizationError)
+ )
+ | _ -> raise NormalizationError
+ in
+ mk_val value_desc expr.expr_type
let translate_guard node args expr =
match expr.expr_desc with
@@ -334,8 +376,7 @@ let rec translate_act node ((m, si, j, d, s) as args) (y, expr) =
conditional g [translate_act node args (y, t)]
[translate_act node args (y, e)]
| Expr_merge (x, hl) -> MBranch (translate_ident node args x, List.map (fun (t, h) -> t, [translate_act node args (y, h)]) hl)
- | _ ->
- MLocalAssign (y, translate_expr node args expr)
+ | _ -> MLocalAssign (y, translate_expr node args expr)
let reset_instance node args i r c =
match r with
@@ -371,7 +412,7 @@ let translate_eq node ((m, si, j, d, s) as args) eq =
d,
control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)
- | p , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) ->
+ | p , Expr_appl (f, arg, r) when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
let var_p = List.map (fun v -> get_node_var v node) p in
let el = expr_list_of_expr arg in
let vl = List.map (translate_expr node args) el in
@@ -421,7 +462,7 @@ let translate_eq node ((m, si, j, d, s) as args) eq =
)
| _ ->
begin
- Format.eprintf "unsupported equation: %a@?" Printers.pp_node_eq eq;
+ Format.eprintf "internal error: Machine_code.translate_eq %a@?" Printers.pp_node_eq eq;
assert false
end
@@ -444,9 +485,9 @@ let find_eq xl eqs =
to the computed schedule [sch]
*)
let sort_equations_from_schedule nd sch =
-(*Format.eprintf "%s schedule: %a@."
- nd.node_id
- (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch;*)
+ (* Format.eprintf "%s schedule: %a@." *)
+ (* nd.node_id *)
+ (* (Utils.fprintf_list ~sep:" ; " Scheduling.pp_eq_schedule) sch; *)
let split_eqs = Splitting.tuple_split_eq_list (get_node_eqs nd) in
let eqs_rev, remainder =
List.fold_left
@@ -554,32 +595,49 @@ let get_const_assign m id =
with Not_found -> assert false
-let value_of_ident m id =
+let value_of_ident loc m id =
(* is is a state var *)
try
- StateVar (List.find (fun v -> v.var_id = id) m.mmemory)
+ let v = List.find (fun v -> v.var_id = id) m.mmemory
+ in mk_val (StateVar v) v.var_type
with Not_found ->
- try (* id is a node var *)
- LocalVar (get_node_var id m.mname)
+ try (* id is a node var *)
+ let v = get_node_var id m.mname
+ in mk_val (LocalVar v) v.var_type
with Not_found ->
try (* id is a constant *)
- LocalVar (Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id)))
+ let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))
+ in mk_val (LocalVar c) c.var_type
with Not_found ->
(* id is a tag *)
- Cst (Const_tag id)
+ let t = Const_tag id
+ in mk_val (Cst t) (Typing.type_const loc t)
+
+(* type of internal fun used in dimension expression *)
+let type_of_value_appl f args =
+ if List.mem f Basic_library.arith_funs
+ then (List.hd args).value_type
+ else Type_predef.type_bool
let rec value_of_dimension m dim =
match dim.Dimension.dim_desc with
- | Dimension.Dbool b -> Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))
- | Dimension.Dint i -> Cst (Const_int i)
- | Dimension.Dident v -> value_of_ident m v
- | Dimension.Dappl (f, args) -> Fun (f, List.map (value_of_dimension m) args)
- | Dimension.Dite (i, t, e) -> Fun ("ite", List.map (value_of_dimension m) [i; t; e])
+ | Dimension.Dbool b ->
+ mk_val (Cst (Const_tag (if b then Corelang.tag_true else Corelang.tag_false))) Type_predef.type_bool
+ | Dimension.Dint i ->
+ mk_val (Cst (Const_int i)) Type_predef.type_int
+ | Dimension.Dident v -> value_of_ident dim.Dimension.dim_loc m v
+ | Dimension.Dappl (f, args) ->
+ let vargs = List.map (value_of_dimension m) args
+ in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs)
+ | Dimension.Dite (i, t, e) ->
+ (match List.map (value_of_dimension m) [i; t; e] with
+ | [vi; vt; ve] -> mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type
+ | _ -> assert false)
| Dimension.Dlink dim' -> value_of_dimension m dim'
| _ -> assert false
let rec dimension_of_value value =
- match value with
+ match value.value_desc with
| Cst (Const_tag t) when t = Corelang.tag_true -> Dimension.mkdim_bool Location.dummy_loc true
| Cst (Const_tag t) when t = Corelang.tag_false -> Dimension.mkdim_bool Location.dummy_loc false
| Cst (Const_int i) -> Dimension.mkdim_int Location.dummy_loc i
diff --git a/src/main_lustre_compiler.ml b/src/main_lustre_compiler.ml
index a0d5b62313c826a5a41deca08c5922e62fa700e3..a44cd04ccd44517e18d5acdb37062d60d59baba8 100644
--- a/src/main_lustre_compiler.ml
+++ b/src/main_lustre_compiler.ml
@@ -15,8 +15,10 @@ open Log
open Utils
open LustreSpec
open Compiler_common
+
+exception StopPhase1 of program
-let usage = "Usage: lustrec [options] <source-file>"
+let usage = "Usage: lustrec [options] \x1b[4msource file\x1b[0m"
let extensions = [".ec"; ".lus"; ".lusi"]
@@ -86,19 +88,12 @@ let compile_source_to_header prog computed_types_env computed_clocks_env dirname
end
+(* From prog to prog *)
+let stage1 prog dirname basename =
+ (* Removing automata *)
+ let prog = expand_automata prog in
-(* compile a .lus source file *)
-let rec compile_source dirname basename extension =
-
- Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
-
- (* Parsing source *)
- let prog = parse_source (dirname ^ "/" ^ basename ^ extension) in
-
- (* 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);
+ 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
@@ -120,26 +115,40 @@ let rec compile_source dirname basename extension =
in
(* Checking stateless/stateful status *)
- check_stateless_decls prog;
+ if Scopes.Plugin.is_active () then
+ force_stateful_decls prog
+ else
+ check_stateless_decls prog;
(* Typing *)
let computed_types_env = type_decls type_env prog in
-
+
(* Clock calculus *)
let computed_clocks_env = clock_decls clock_env prog in
(* Generating a .lusi header file only *)
if !Options.lusi then
- begin
- let lusi_ext = extension ^ "i" in
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@," (dirname ^ "/" ^ basename ^ lusi_ext));
- print_lusi prog dirname basename lusi_ext;
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
- exit 0
- end;
+ (* We stop here the processing and produce the current prog. It will be
+ exported as a lusi *)
+ raise (StopPhase1 prog);
+ (* Optimization of prog:
+ - Unfold consts
+ - eliminate trivial expressions
+ *)
+ (*
+ let prog =
+ if !Options.const_unfold || !Options.optimization >= 5 then
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. eliminating constants and aliases@,");
+ Optimize_prog.prog_unfold_consts prog
+ end
+ else
+ prog
+ in
+ *)
(* Delay calculus *)
- (* TO BE DONE LATER (Xavier)
+ (*
if(!Options.delay_calculus)
then
begin
@@ -159,13 +168,8 @@ let rec compile_source dirname basename extension =
(* Compatibility with Lusi *)
(* Checking the existence of a lusi (Lustre Interface file) *)
- (match !Options.output with
- "C" ->
- begin
- let extension = ".lusi" in
- compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
- end
- |_ -> ());
+ let extension = ".lusi" in
+ compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
Typing.uneval_prog_generics prog;
Clock_calculus.uneval_prog_generics prog;
@@ -184,12 +188,13 @@ let rec compile_source dirname basename extension =
!Options.main_node
orig prog type_env clock_env
end;
-
-(*Format.eprintf "Inliner.global_inline<<@.%a@.>>@." Printers.pp_prog prog;*)
+
(* Computes and stores generic calls for each node,
only useful for ANSI C90 compliant generic node compilation *)
if !Options.ansi then Causality.NodeDep.compute_generic_calls prog;
- (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with Corelang.Node nd -> Format.eprintf "%s calls %a" id Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
+ (*Hashtbl.iter (fun id td -> match td.Corelang.top_decl_desc with
+ Corelang.Node nd -> Format.eprintf "%s calls %a" id
+ Causality.NodeDep.pp_generic_calls nd | _ -> ()) Corelang.node_table;*)
(* Normalization phase *)
Log.report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
@@ -197,8 +202,22 @@ let rec compile_source dirname basename extension =
if !Options.output = "lustre" then
Normalization.unfold_arrow_active := false;
let prog = Normalization.normalize_prog prog in
+ Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
+ let prog =
+ if !Options.mpfr
+ then
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. targetting MPFR library@,");
+ Mpfr.inject_prog prog
+ end
+ else
+ begin
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. keeping FP numbers@,");
+ prog
+ end in
Log.report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
+
(* Checking array accesses *)
if !Options.check then
begin
@@ -206,35 +225,33 @@ let rec compile_source dirname basename extension =
Access.check_prog prog;
end;
+ prog, dependencies
+
+(* from source to machine code, with optimization *)
+let stage2 prog =
(* Computation of node equation scheduling. It also breaks dependency cycles
and warns about unused input or memory variables *)
Log.report ~level:1 (fun fmt -> fprintf fmt ".. scheduling@,");
let prog, node_schs = Scheduling.schedule_prog prog in
- Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_warning_unused node_schs);
+ Log.report ~level:1 (fun fmt -> fprintf fmt "%a" Scheduling.pp_warning_unused node_schs);
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_schedule node_schs);
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_fanin_table node_schs);
+ Log.report ~level:5 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Scheduling.pp_dep_graph node_schs);
Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
- (* Optimization of prog:
- - Unfold consts
- - eliminate trivial expressions
- *)
- let prog =
- if !Options.optimization >= 5 then
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. constants elimination@,");
- Optimize_prog.prog_unfold_consts prog
- end
- else
- prog
- in
+
+ (* TODO Salsa optimize prog:
+ - emits warning for programs with pre inside expressions
+ - make sure each node arguments and memory is bounded by a local annotation
+ - introduce fresh local variables for each real pure subexpression
+ *)
(* DFS with modular code generation *)
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
+ 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@]@,"
+ Log.report ~level:4 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
(Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
- machine_code);
+ machine_code);
(* Optimize machine code *)
let machine_code =
@@ -246,41 +263,66 @@ let rec compile_source dirname basename extension =
else
machine_code
in
-
(* Optimize machine code *)
- let machine_code =
+ let machine_code, removed_table =
if !Options.optimization >= 2 && !Options.output <> "horn" then
begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 1)@,");
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 1)@ ");
Optimize_machine.machines_unfold (Corelang.get_consts prog) node_schs machine_code
end
else
- machine_code
- in
+ machine_code, IMap.empty
+ in
(* Optimize machine code *)
- let machine_code =
+ let machine_code =
if !Options.optimization >= 3 && !Options.output <> "horn" then
begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 2)@,");
- Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code node_schs)
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. machines optimization (phase 2)@ ");
+ let node_schs = Scheduling.remove_prog_inlined_locals removed_table node_schs in
+ let reuse_tables = Scheduling.compute_prog_reuse_table node_schs in
+ Optimize_machine.machines_fusion (Optimize_machine.machines_reuse_variables machine_code reuse_tables)
end
else
machine_code
in
+
+ (* Salsa optimize machine code *)
+ (*
+ let machine_code =
+ if !Options.salsa_enabled then
+ begin
+ check_main ();
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. salsa machines optimization (phase 3)@ ");
+ (* Selecting float constants for Salsa *)
+ let constEnv = List.fold_left (
+ fun accu c_topdecl ->
+ match c_topdecl.top_decl_desc with
+ | Const c when Types.is_real_type c.const_type ->
+ (c.const_id, c.const_value) :: accu
+ | _ -> accu
+ ) [] (Corelang.get_consts prog)
+ in
+ List.map
+ (Machine_salsa_opt.machine_t2machine_t_optimized_by_salsa constEnv)
+ machine_code
+ end
+ else
+ machine_code
+ in
+ Log.report ~level:3 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@ "
+ (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
+ machine_code);
+ *)
+ 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 *)
+(* printing code *)
+let stage3 prog machine_code dependencies basename =
let basename = Filename.basename basename in
let destname = !Options.dest_dir ^ "/" ^ basename in
- let _ = match !Options.output with
- | "C" ->
- begin
+ match !Options.output with
+ "C" ->
+ begin
let alloc_header_file = destname ^ "_alloc.h" in (* Could be changed *)
let source_lib_file = destname ^ ".c" in (* Could be changed *)
let source_main_file = destname ^ "_main.c" in (* Could be changed *)
@@ -292,7 +334,7 @@ let rec compile_source dirname basename extension =
end
| "java" ->
begin
- failwith "Sorry, but not yet supported !"
+ (Format.eprintf "internal error: sorry, but not yet supported !"; assert false)
(*let source_file = basename ^ ".java" in
Log.report ~level:1 (fun fmt -> fprintf fmt ".. opening file %s@,@?" source_file);
let source_out = open_out source_file in
@@ -301,7 +343,7 @@ let rec compile_source dirname basename extension =
Java_backend.translate_to_java source_fmt basename normalized_prog machine_code;*)
end
| "horn" ->
- begin
+ begin
let source_file = destname ^ ".smt2" in (* Could be changed *)
let source_out = open_out source_file in
let fmt = formatter_of_out_channel source_out in
@@ -309,7 +351,7 @@ let rec compile_source dirname basename extension =
Horn_backend.translate fmt basename prog machine_code;
(* Tracability file if option is activated *)
if !Options.traces then (
- let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
+ let traces_file = destname ^ ".traces" in (* Could be changed *)
let traces_out = open_out traces_file in
let fmt = formatter_of_out_channel traces_out in
Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
@@ -327,12 +369,64 @@ let rec compile_source dirname basename extension =
end
| _ -> assert false
+
+(* compile a .lus source file *)
+let rec compile_source dirname basename extension =
+ let source_name = dirname ^ "/" ^ basename ^ extension in
+
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
+
+ (* Parsing source *)
+ let prog = parse_source source_name in
+
+ let prog =
+ if !Options.mpfr then
+ Mpfr.mpfr_module::prog
+ else
+ prog
+ in
+ let prog, dependencies =
+ try
+ stage1 prog dirname basename
+ with StopPhase1 prog -> (
+ if !Options.lusi then
+ begin
+ let lusi_ext = extension ^ "i" in
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@," (basename ^ lusi_ext));
+ print_lusi prog dirname basename lusi_ext;
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
+ exit 0
+ end
+ else
+ assert false
+ )
in
- begin
- Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
- (* We stop the process here *)
- exit 0
- end
+
+ let machine_code =
+ stage2 prog
+ in
+ 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 =
+ if Scopes.Plugin.is_active () then
+ Scopes.Plugin.process_scopes !Options.main_node prog machine_code
+ else
+ machine_code
+ in
+
+ stage3 prog machine_code dependencies basename;
+ Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
+ (* We stop the process here *)
+ exit 0
let compile dirname basename extension =
match extension with
@@ -356,12 +450,22 @@ let anonymous filename =
raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
let _ =
+ Global.initialize ();
Corelang.add_internal_funs ();
try
Printexc.record_backtrace true;
- Arg.parse Options.options anonymous usage
+
+ let options = Options.options @
+ List.flatten (
+ List.map Options.plugin_opt [
+ Scopes.Plugin.name, Scopes.Plugin.activate, Scopes.Plugin.options
+ ]
+ )
+ in
+
+ Arg.parse options anonymous usage
with
- | Parse.Syntax_err _ | Lexer_lustre.Error _
+ | Parse.Error _
| Types.Error (_,_) | Clocks.Error (_,_)
| Corelang.Error _ (*| Task_set.Error _*)
| Causality.Cycle _ -> exit 1
diff --git a/src/normalization.ml b/src/normalization.ml
index 30e4066f57552477226934afcb04387730be9769..968fb2cc91be5da771271f536af3b8566b05d135 100644
--- a/src/normalization.ml
+++ b/src/normalization.ml
@@ -127,16 +127,29 @@ let mk_expr_alias node (defs, vars) expr =
(* Create an alias for [expr], if [expr] is not already an alias (i.e. an ident)
and [opt] is true *)
-let mk_expr_alias_opt opt node defvars expr =
+let mk_expr_alias_opt opt node (defs, vars) expr =
+(*Format.eprintf "mk_expr_alias_opt %B %a %a %a@." opt Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
match expr.expr_desc with
| Expr_ident alias ->
- defvars, expr
+ (defs, vars), expr
| _ ->
- if opt
- then
- mk_expr_alias node defvars expr
- else
- defvars, expr
+ match get_expr_alias defs expr with
+ | Some eq ->
+ let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
+ (defs, vars), replace_expr aliases expr
+ | None ->
+ if opt
+ then
+ let new_aliases =
+ List.map2
+ (mk_fresh_var node expr.expr_loc)
+ (Types.type_list_of_type expr.expr_type)
+ (Clocks.clock_list_of_clock expr.expr_clock) in
+ let new_def =
+ mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
+ in (new_def::defs, new_aliases@vars), replace_expr new_aliases expr
+ else
+ (defs, vars), expr
(* Create a (normalized) expression from [ref_e],
replacing description with [norm_d],
@@ -159,7 +172,7 @@ let rec normalize_list alias node offsets norm_element defvars elist =
) elist (defvars, [])
let rec normalize_expr ?(alias=true) node offsets defvars expr =
-(* Format.eprintf "normalize %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
+(*Format.eprintf "normalize %B %a:%a [%a]@." alias Printers.pp_expr expr Types.print_ty expr.expr_type (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
match expr.expr_desc with
| Expr_const _
| Expr_ident _ -> defvars, unfold_offsets expr offsets
@@ -180,7 +193,7 @@ let rec normalize_expr ?(alias=true) node offsets defvars expr =
normalize_list alias node offsets (fun alias -> normalize_expr ~alias:alias) defvars elist in
defvars, mk_norm_expr offsets expr (Expr_tuple norm_elist)
| Expr_appl (id, args, None)
- when Basic_library.is_internal_fun id
+ when Basic_library.is_homomorphic_fun id
&& Types.is_array_type expr.expr_type ->
let defvars, norm_args =
normalize_list
@@ -192,7 +205,7 @@ let rec normalize_expr ?(alias=true) node offsets defvars expr =
(expr_list_of_expr args)
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_internal_fun id ->
+ | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
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) ->
@@ -203,7 +216,7 @@ let rec normalize_expr ?(alias=true) node offsets defvars expr =
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 && not (Basic_library.is_internal_fun id)) node defvars norm_expr
+ mk_expr_alias_opt (alias && 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) -> (* 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) ->
@@ -251,7 +264,7 @@ and normalize_branches node offsets defvars hl =
hl (defvars, [])
and normalize_array_expr ?(alias=true) node offsets defvars expr =
-(* Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
+ (*Format.eprintf "normalize_array %B %a [%a]@." alias Printers.pp_expr expr (Utils.fprintf_list ~sep:"," Dimension.pp_dimension) offsets;*)
match expr.expr_desc with
| Expr_power (e1, d) when offsets = [] ->
let defvars, norm_e1 = normalize_expr node offsets defvars e1 in
@@ -262,7 +275,7 @@ and normalize_array_expr ?(alias=true) node offsets defvars expr =
| Expr_array elist when offsets = [] ->
let defvars, norm_elist = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars elist in
defvars, mk_norm_expr offsets expr (Expr_array norm_elist)
- | Expr_appl (id, args, None) when Basic_library.is_internal_fun id ->
+ | Expr_appl (id, args, None) when Basic_library.is_expr_internal_fun expr ->
let defvars, norm_args = normalize_list alias node offsets (fun _ -> normalize_array_expr ~alias:true) defvars (expr_list_of_expr args) in
defvars, mk_norm_expr offsets expr (Expr_appl (id, expr_of_expr_list args.expr_loc norm_args, None))
| _ -> normalize_expr ~alias:alias node offsets defvars expr
@@ -310,6 +323,7 @@ let decouple_outputs node defvars eq =
defvars', {eq with eq_lhs = lhs' }
let rec normalize_eq node defvars eq =
+(*Format.eprintf "normalize_eq %a@." Types.print_ty eq.eq_rhs.expr_type;*)
match eq.eq_rhs.expr_desc with
| Expr_pre _
| Expr_fby _ ->
@@ -321,7 +335,7 @@ let rec normalize_eq node defvars eq =
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
let norm_eq = { eq with eq_rhs = norm_rhs } in
(norm_eq::defs', vars')
- | Expr_appl (id, _, None) when Basic_library.is_internal_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
+ | Expr_appl (id, _, None) when Basic_library.is_homomorphic_fun id && Types.is_array_type eq.eq_rhs.expr_type ->
let (defs', vars'), norm_rhs = normalize_array_expr ~alias:false node [] defvars eq.eq_rhs in
let norm_eq = { eq with eq_rhs = norm_rhs } in
(norm_eq::defs', vars')
@@ -353,10 +367,10 @@ let normalize_node node =
List.fold_left (
fun (vars, def_accu, assert_accu) assert_ ->
let assert_expr = assert_.assert_expr in
- let (defs, vars'), expr =
- normalize_expr
- ~alias:true
- node
+ let (defs, vars'), expr =
+ normalize_expr
+ ~alias:false
+ node
[] (* empty offset for arrays *)
([], vars) (* defvar only contains vars *)
assert_expr
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index 48a36f9645d02443478077b6814609477a868e6a..c87b86b76823f051d468924071381605adeb0dc3 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -26,7 +26,8 @@ let pp_elim fmt elim =
let rec eliminate elim instr =
let e_expr = eliminate_expr elim in
- match instr with
+ match instr with
+ | MComment _ -> instr
| MLocalAssign (i,v) -> MLocalAssign (i, e_expr v)
| MStateAssign (i,v) -> MStateAssign (i, e_expr v)
| MReset i -> instr
@@ -41,50 +42,55 @@ let rec eliminate elim instr =
)
and eliminate_expr elim expr =
- match expr with
- | StateVar v
+ match expr.value_desc with
| LocalVar v -> (try IMap.find v.var_id elim with Not_found -> expr)
- | Fun (id, vl) -> Fun (id, List.map (eliminate_expr elim) vl)
- | Array(vl) -> Array(List.map (eliminate_expr elim) vl)
- | Access(v1, v2) -> Access(eliminate_expr elim v1, eliminate_expr elim v2)
- | Power(v1, v2) -> Power(eliminate_expr elim v1, eliminate_expr elim v2)
- | Cst _ -> expr
+ | Fun (id, vl) -> {expr with value_desc = Fun (id, List.map (eliminate_expr elim) vl)}
+ | Array(vl) -> {expr with value_desc = Array(List.map (eliminate_expr elim) vl)}
+ | Access(v1, v2) -> { expr with value_desc = Access(eliminate_expr elim v1, eliminate_expr elim v2)}
+ | Power(v1, v2) -> { expr with value_desc = Power(eliminate_expr elim v1, eliminate_expr elim v2)}
+ | Cst _ | StateVar _ -> 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
+ List.fold_left
+ (fun res -> (function | Index i -> mk_val (Access (res, value_of_dimension m i))
+ (Types.array_element_type res.value_type)
+ | Field f -> Format.eprintf "internal error: not yet implemented !"; assert false))
+ expr offset
-let rec simplify_cst_expr m offset cst =
+let rec simplify_cst_expr m offset typ cst =
match offset, cst with
| [] , _
- -> Cst cst
+ -> mk_val (Cst cst) typ
| 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))
+ -> let elt_typ = Types.array_element_type typ in
+ simplify_cst_expr m q elt_typ (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))
+ -> let elt_typ = Types.array_element_type typ in
+ unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify_cst_expr m q elt_typ) cl)) typ)
| Field f :: q, Const_struct fl
- -> simplify_cst_expr m q (List.assoc f fl)
+ -> let fld_typ = Types.struct_field_type typ f in
+ simplify_cst_expr m q fld_typ (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
+ match offset, expr.value_desc 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 (id, vl) when Basic_library.is_value_internal_fun expr
+ -> mk_val (Fun (id, List.map (simplify offset) vl)) expr.value_type
| _ , Fun _
| _ , StateVar _
| _ , LocalVar _ -> unfold_expr_offset m offset expr
- | _ , Cst cst -> simplify_cst_expr m offset cst
+ | _ , Cst cst -> simplify_cst_expr m offset expr.value_type 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)
+ | Index i :: q, Array vl -> unfold_expr_offset m [Index i] (mk_val (Array (List.map (simplify q) vl)) expr.value_type)
(*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
@@ -97,15 +103,15 @@ let rec simplify_instr_offset m 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)
+ | MComment _ -> instr
and simplify_instrs_offset m instrs =
List.map (simplify_instr_offset m) instrs
let is_scalar_const c =
match c with
- | Const_int _
| Const_real _
- | Const_float _
+ | Const_int _
| Const_tag _ -> true
| _ -> false
@@ -119,7 +125,6 @@ let is_unfoldable_expr fanin expr =
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
@@ -128,7 +133,7 @@ let is_unfoldable_expr fanin expr =
| _ , Const_array _ -> false
| _ -> assert false in
let rec unfold offset expr =
- match offset, expr with
+ match offset, expr.value_desc with
| _ , Cst cst -> unfold_const offset cst
| _ , LocalVar _
| _ , StateVar _ -> true
@@ -139,28 +144,22 @@ let is_unfoldable_expr fanin expr =
-> 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
+ | _ , Fun (id, vl) when fanin < 2 && Basic_library.is_value_internal_fun expr
-> List.for_all (unfold offset) vl
| _ , Fun _ -> false
| _ -> assert false
in unfold [] expr
-let unfoldable_assign fanin v expr =
+let basic_unfoldable_assign fanin v expr =
try
let d = Hashtbl.find fanin v.var_id
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
-*)
+ (if !Options.mpfr then Mpfr.unfoldable_value expr else true)
+&& basic_unfoldable_assign fanin v expr
+
let merge_elim elim1 elim2 =
let merge k e1 e2 =
match e1, e2 with
@@ -189,8 +188,8 @@ and instr_unfold fanin instrs elim instr =
(* Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;*)
match instr with
(* Simple cases*)
- | MStep([v], id, vl) when Basic_library.is_internal_fun id
- -> instr_unfold fanin instrs elim (MLocalAssign (v, Fun (id, vl)))
+ | MStep([v], id, vl) when Basic_library.is_value_internal_fun (mk_val (Fun (id, vl)) v.var_type)
+ -> instr_unfold fanin instrs elim (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type))
| MLocalAssign(v, expr) when unfoldable_assign fanin v expr
-> (IMap.add v.var_id expr elim, instrs)
| MBranch(g, hl) when false
@@ -242,26 +241,29 @@ let machine_unfold fanin elim machine =
mconst = mconst;
minstances = minstances;
mcalls = mcalls;
- }
+ },
+ elim_vars
let instr_of_const top_const =
let const = const_of_top top_const in
let vdecl = mkvar_decl Location.dummy_loc (const.const_id, mktyp Location.dummy_loc Tydec_any, mkclock Location.dummy_loc Ckdec_any, true, None) in
let vdecl = { vdecl with var_type = const.const_type }
- in MLocalAssign (vdecl, Cst const.const_value)
+ in MLocalAssign (vdecl, mk_val (Cst const.const_value) vdecl.var_type)
let machines_unfold consts node_schs machines =
- List.map
- (fun m ->
- let fanin = (IMap.find m.mname.node_id node_schs).Scheduling.fanin_table in
- let elim_consts, _ = instrs_unfold fanin IMap.empty (List.map instr_of_const consts)
- in machine_unfold fanin elim_consts m)
+ List.fold_right (fun m (machines, removed) ->
+ let fanin = (IMap.find m.mname.node_id node_schs).Scheduling.fanin_table in
+ let elim_consts, _ = instrs_unfold fanin IMap.empty (List.map instr_of_const consts) in
+ let (m, removed_m) = machine_unfold fanin elim_consts m in
+ (m::machines, IMap.add m.mname.node_id removed_m removed)
+ )
machines
+ ([], IMap.empty)
let get_assign_lhs instr =
match instr with
- | MLocalAssign(v, _) -> LocalVar v
- | MStateAssign(v, _) -> StateVar v
+ | MLocalAssign(v, e) -> mk_val (LocalVar v) e.value_type
+ | MStateAssign(v, e) -> mk_val (StateVar v) e.value_type
| _ -> assert false
let get_assign_rhs instr =
@@ -277,7 +279,7 @@ let is_assign instr =
| _ -> false
let mk_assign v e =
- match v with
+ match v.value_desc with
| LocalVar v -> MLocalAssign(v, e)
| StateVar v -> MStateAssign(v, e)
| _ -> assert false
@@ -315,18 +317,19 @@ let subst_instr subst instrs instr =
let e = get_assign_rhs instr in
try
let instr' = List.find (fun instr' -> is_assign instr' && get_assign_rhs instr' = e) instrs in
- match v with
+ match v.value_desc with
| LocalVar v ->
IMap.add v.var_id (get_assign_lhs instr') subst, instrs
- | StateVar v ->
- (match get_assign_lhs instr' with
+ | StateVar stv ->
+ let lhs = get_assign_lhs instr' in
+ (match lhs.value_desc with
| LocalVar v' ->
- let instr = eliminate subst (mk_assign (StateVar v) (LocalVar v')) in
+ let instr = eliminate subst (mk_assign v lhs) in
subst, instr :: instrs
- | StateVar v' ->
- let subst_v' = IMap.add v'.var_id (StateVar v) IMap.empty in
+ | StateVar stv' ->
+ let subst_v' = IMap.add stv'.var_id v IMap.empty in
let instrs' = snd (List.fold_right (fun instr (ok, instrs) -> (ok || instr = instr', if ok then instr :: instrs else if instr = instr' then instrs else eliminate subst_v' instr :: instrs)) instrs (false, [])) in
- IMap.add v'.var_id (StateVar v) subst, instr :: instrs'
+ IMap.add stv'.var_id v subst, instr :: instrs'
| _ -> assert false)
| _ -> assert false
with Not_found -> subst, instr :: instrs
@@ -341,8 +344,8 @@ let subst_instr subst instrs instr =
let rec instr_cse (subst, instrs) instr =
match instr with
(* Simple cases*)
- | MStep([v], id, vl) when Basic_library.is_internal_fun id
- -> instr_cse (subst, instrs) (MLocalAssign (v, Fun (id, vl)))
+ | MStep([v], id, vl) when Basic_library.is_internal_fun id (List.map (fun v -> v.value_type) vl)
+ -> instr_cse (subst, instrs) (MLocalAssign (v, mk_val (Fun (id, vl)) v.var_type))
| MLocalAssign(v, expr) when is_unfoldable_expr 2 expr
-> (IMap.add v.var_id expr subst, instr :: instrs)
| _ when is_assign instr
@@ -384,8 +387,8 @@ let machines_cse machines =
(* checks whether an [instr] is skip and can be removed from program *)
let rec instr_is_skip instr =
match instr with
- | MLocalAssign (i, LocalVar v) when i = v -> true
- | MStateAssign (i, StateVar v) when i = v -> true
+ | MLocalAssign (i, { value_desc = (LocalVar v) ; _}) when i = v -> true
+ | MStateAssign (i, { value_desc = StateVar v; _}) when i = v -> true
| MBranch (g, hl) -> List.for_all (fun (_, il) -> instrs_are_skip il) hl
| _ -> false
and instrs_are_skip instrs =
@@ -396,8 +399,8 @@ let instr_cons instr cont =
let rec instr_remove_skip instr cont =
match instr with
- | MLocalAssign (i, LocalVar v) when i = v -> cont
- | MStateAssign (i, StateVar v) when i = v -> cont
+ | MLocalAssign (i, { value_desc = LocalVar v; _ }) when i = v -> cont
+ | MStateAssign (i, { value_desc = StateVar v; _ }) when i = v -> cont
| MBranch (g, hl) -> MBranch (g, List.map (fun (h, il) -> (h, instrs_remove_skip il [])) hl) :: cont
| _ -> instr::cont
@@ -405,17 +408,18 @@ and instrs_remove_skip instrs cont =
List.fold_right instr_remove_skip instrs cont
let rec value_replace_var fvar value =
- match value with
+ match value.value_desc with
| Cst c -> value
- | LocalVar v -> LocalVar (fvar v)
+ | LocalVar v -> { value with value_desc = LocalVar (fvar v) }
| StateVar v -> value
- | Fun (id, args) -> Fun (id, List.map (value_replace_var fvar) args)
- | Array vl -> Array (List.map (value_replace_var fvar) vl)
- | Access (t, i) -> Access(value_replace_var fvar t, i)
- | Power (v, n) -> Power(value_replace_var fvar v, n)
+ | Fun (id, args) -> { value with value_desc = Fun (id, List.map (value_replace_var fvar) args) }
+ | Array vl -> { value with value_desc = Array (List.map (value_replace_var fvar) vl)}
+ | Access (t, i) -> { value with value_desc = Access(value_replace_var fvar t, i)}
+ | Power (v, n) -> { value with value_desc = Power(value_replace_var fvar v, n)}
let rec instr_replace_var fvar instr cont =
match instr with
+ | MComment _ -> instr_cons instr cont
| MLocalAssign (i, v) -> instr_cons (MLocalAssign (fvar i, value_replace_var fvar v)) cont
| MStateAssign (i, v) -> instr_cons (MStateAssign (i, value_replace_var fvar v)) cont
| MReset i -> instr_cons instr cont
@@ -457,10 +461,10 @@ let machine_reuse_variables m reuse =
with Not_found -> v in
machine_replace_variables fvar m
-let machines_reuse_variables prog node_schs =
+let machines_reuse_variables prog reuse_tables =
List.map
(fun m ->
- machine_reuse_variables m (Utils.IMap.find m.mname.node_id node_schs).Scheduling.reuse_table
+ machine_reuse_variables m (Utils.IMap.find m.mname.node_id reuse_tables)
) prog
let rec instr_assign res instr =
@@ -476,8 +480,8 @@ and instrs_assign res instrs =
let rec instr_constant_assign var instr =
match instr with
- | MLocalAssign (i, Cst (Const_tag _))
- | MStateAssign (i, Cst (Const_tag _)) -> i = var
+ | MLocalAssign (i, { value_desc = Cst (Const_tag _); _ })
+ | MStateAssign (i, { value_desc = Cst (Const_tag _); _ }) -> i = var
| MBranch (g, hl) -> List.for_all (fun (h, b) -> instrs_constant_assign var b) hl
| _ -> false
@@ -486,8 +490,8 @@ and instrs_constant_assign var instrs =
let rec instr_reduce branches instr1 cont =
match instr1 with
- | MLocalAssign (_, Cst (Const_tag c)) -> instr1 :: (List.assoc c branches @ cont)
- | MStateAssign (_, Cst (Const_tag c)) -> instr1 :: (List.assoc c branches @ cont)
+ | MLocalAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
+ | MStateAssign (_, { value_desc = Cst (Const_tag c); _}) -> instr1 :: (List.assoc c branches @ cont)
| MBranch (g, hl) -> MBranch (g, List.map (fun (h, b) -> (h, instrs_reduce branches b [])) hl) :: cont
| _ -> instr1 :: cont
@@ -502,9 +506,9 @@ let rec instrs_fusion instrs =
| []
| [_] ->
instrs
- | i1::(MBranch (LocalVar v, hl))::q when instr_constant_assign v i1 ->
+ | i1::(MBranch ({ value_desc = LocalVar v; _}, hl))::q when instr_constant_assign v i1 ->
instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q)
- | i1::(MBranch (StateVar v, hl))::q when instr_constant_assign v i1 ->
+ | i1::(MBranch ({ value_desc = StateVar v; _}, hl))::q when instr_constant_assign v i1 ->
instr_reduce (List.map (fun (h, b) -> h, instrs_fusion b) hl) i1 (instrs_fusion q)
| i1::i2::q ->
i1 :: instrs_fusion (i2::q)
diff --git a/src/options.ml b/src/options.ml
index 16ada24b2e0d51f8a03eb87cb560dc4d86a7c99a..8f40a9cf8d214c12799e8ee19d2171007adac83d 100755
--- a/src/options.ml
+++ b/src/options.ml
@@ -33,24 +33,36 @@ let witnesses = ref false
let optimization = ref 2
let lusi = ref false
let print_reuse = ref false
-let traces = ref false
+let const_unfold = ref false
+let mpfr = ref false
+let mpfr_prec = ref 0
-let horntraces = ref false
+let traces = ref false
let horn_cex = ref false
let horn_query = ref true
+let salsa_enabled = ref true
+let set_mpfr prec =
+ if prec > 0 then (
+ mpfr := true;
+ mpfr_prec := prec;
+ salsa_enabled := false; (* We deactivate salsa *)
+ )
+ else
+ failwith "mpfr requires a positive integer"
+
let options =
[ "-d", Arg.Set_string dest_dir,
- "uses the specified directory as root for generated/imported object and C files (default: .)";
- "-node", Arg.Set_string main_node, "specifies the main node";
+ "uses the specified directory \x1b[4mdir\x1b[0m as root for generated/imported object and C files <default: .>";
+ "-node", Arg.Set_string main_node, "specifies the \x1b[4mmain\x1b[0m node";
"-init", Arg.Set delay_calculus, "performs an initialisation analysis for Lustre nodes <default: no analysis>";
"-dynamic", Arg.Clear static_mem, "specifies a dynamic allocation scheme for main Lustre node <default: static>";
- "-ansi", Arg.Set ansi, "specifies that generated C code is ansi C90 compliant <default: C99>";
"-check-access", Arg.Set check, "checks at runtime that array accesses always lie within bounds <default: no check>";
+ "-mpfr", Arg.Int set_mpfr, "replaces FP numbers by the MPFR library multiple precision numbers with a precision of \x1b[4mprec\x1b[0m bits <default: keep FP numbers>";
"-lusi", Arg.Set lusi, "only generates a .lusi interface source file from a Lustre source <default: no generation>";
"-no-spec", Arg.Unit (fun () -> spec := "no"), "do not generate any specification";
- "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend (default)";
+ "-acsl-spec", Arg.Unit (fun () -> spec := "acsl"), "generates an ACSL encoding of the specification. Only meaningful for the C backend <default>";
"-c-spec", Arg.Unit (fun () -> spec := "c"), "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
"-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
"-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
@@ -59,15 +71,20 @@ let options =
"-horn-query", Arg.Unit (fun () -> output := "horn"; horn_query:=true), "generate queries in generated Horn file. Enable the horn backend (work in progress)";
"-print_reuse", Arg.Set print_reuse, "prints variable reuse policy";
"-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
- "-inline", Arg.Set global_inline, "inline all node calls (require a main node)";
+ "-inline", Arg.Unit (fun () -> global_inline := true; const_unfold := true), "inline all node calls (require a main node). Implies constant unfolding";
"-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
"-print_types", Arg.Set print_types, "prints node types";
"-print_clocks", Arg.Set print_clocks, "prints node clocks";
- "-O", Arg.Set_int optimization, " changes optimization level <default: 2>";
- "-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";
+ "-O", Arg.Set_int optimization, "changes optimization \x1b[4mlevel\x1b[0m <default: 2>";
+ "-verbose", Arg.Set_int verbose_level, "changes verbose \x1b[4mlevel\x1b[0m <default: 1>";
"-version", Arg.Unit print_version, " displays the version";]
+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 get_witness_dir filename =
(* Make sure the directory exists *)
let dir = !dest_dir ^ "/" ^ (Filename.basename filename) ^ "_witnesses" in
diff --git a/src/parse.ml b/src/parse.ml
index 0bd7e961720a77974906bca2d534e7a57f9dc659..84ac6b3a049d18fb8080c5bd68237f36be1d681d 100755
--- a/src/parse.ml
+++ b/src/parse.ml
@@ -8,16 +8,40 @@
(* version 2.1. *)
(* *)
(********************************************************************)
-
-exception Syntax_err of Location.t
-
open Format
open LustreSpec
open Corelang
-let report_error loc =
- Location.print loc;
- print_string "Syntax error\n"
+type error =
+ | Undefined_token of string
+ | Unexpected_eof
+ | Unfinished_string
+ | Unfinished_comment
+ | Syntax_error
+ | Unfinished_annot
+ | Unfinished_node_spec
+ | Annot_error of string
+ | Node_spec_error of string
+
+exception Error of (Location.t * error)
+
+
+let pp_error fmt err =
+ match err with
+ | Unexpected_eof -> fprintf fmt "unexpected end of file"
+ | Undefined_token tok -> fprintf fmt "undefined token '%s'" tok
+ | Unfinished_string -> fprintf fmt "unfinished string"
+ | Unfinished_comment -> fprintf fmt "unfinished comment"
+ | Syntax_error -> fprintf fmt "syntax error"
+ | Unfinished_annot -> fprintf fmt "unfinished annotation"
+ | Unfinished_node_spec -> fprintf fmt "unfinished node specification"
+ | Annot_error s -> fprintf fmt "impossible to parse the following annotation:@.%s@.@?" s
+ | Node_spec_error s -> fprintf fmt "Impossible to parse the following node specification:@.%s@.@?" s
+
+let report_error (loc, err) =
+ eprintf "Syntax error: %a%a@."
+ pp_error err
+ Location.pp_loc loc
let header parsing_fun token_fun lexbuf =
try
@@ -27,7 +51,7 @@ let header parsing_fun token_fun lexbuf =
with
| Parsing.Parse_error ->
let loc = Location.curr lexbuf in
- raise (Syntax_err loc)
+ raise (Error (loc, Syntax_error))
let prog parsing_fun token_fun lexbuf =
try
@@ -37,7 +61,7 @@ let prog parsing_fun token_fun lexbuf =
with
| Parsing.Parse_error ->
let loc = Location.curr lexbuf in
- raise (Syntax_err loc)
+ raise (Error (loc, Syntax_error))
(* Local Variables: *)
(* compile-command:"make -C .." *)
diff --git a/src/parser_lustre.mly b/src/parser_lustre.mly
index ab4b17667086efaad40d2814e96f9ac39145e80e..bc50bc6401167bdba79949392c0a64fc2b3dfbc0 100755
--- a/src/parser_lustre.mly
+++ b/src/parser_lustre.mly
@@ -18,9 +18,10 @@ open Parse
let get_loc () = Location.symbol_rloc ()
+let mkident x = x, get_loc ()
let mktyp x = mktyp (get_loc ()) x
let mkclock x = mkclock (get_loc ()) x
-let mkvar_decl x = mkvar_decl (get_loc ()) ~orig:true x
+let mkvar_decl x loc = mkvar_decl loc ~orig:true x
let mkexpr x = mkexpr (get_loc ()) x
let mkeexpr x = mkeexpr (get_loc ()) x
let mkeq x = mkeq (get_loc ()) x
@@ -52,8 +53,8 @@ let rec fby expr n init =
%}
%token <int> INT
-%token <string> REAL
-%token <float> FLOAT
+%token <Num.num * int * string> REAL
+
%token <string> STRING
%token AUTOMATON STATE UNTIL UNLESS RESTART RESUME LAST
%token STATELESS ASSERT OPEN QUOTE FUNCTION
@@ -69,7 +70,7 @@ let rec fby expr n init =
%token MERGE FBY WHEN WHENNOT EVERY
%token NODE LET TEL RETURNS VAR IMPORTED SENSOR ACTUATOR WCET TYPE CONST
%token STRUCT ENUM
-%token TINT TFLOAT TREAL TBOOL TCLOCK
+%token TINT TREAL TBOOL TCLOCK
%token RATE DUE
%token EQ LT GT LTE GTE NEQ
%token AND OR XOR IMPL
@@ -116,6 +117,9 @@ let rec fby expr n init =
%start lustre_spec
%type <LustreSpec.node_annot> lustre_spec
+%start signed_const
+%type <LustreSpec.constant> signed_const
+
%%
module_ident:
@@ -135,8 +139,8 @@ node_ident_decl:
node_ident { push_node $1; $1 }
vdecl_ident:
- UIDENT { $1 }
-| IDENT { $1 }
+ UIDENT { mkident $1 }
+| IDENT { mkident $1 }
const_ident:
UIDENT { $1 }
@@ -180,7 +184,7 @@ state_annot:
top_decl_header:
| CONST cdecl_list { List.rev ($2 true) }
-| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_opt SCOL
+| nodespec_list state_annot node_ident LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR prototype_opt in_lib_list SCOL
{let nd = mktop_decl true (ImportedNode
{nodei_id = $3;
nodei_type = Types.new_var ();
@@ -198,15 +202,15 @@ prototype_opt:
{ None }
| PROTOTYPE node_ident { Some $2}
-in_lib_opt:
-{ None }
-| LIB module_ident {Some $2}
+in_lib_list:
+{ [] }
+| LIB module_ident in_lib_list { $2::$3 }
top_decl:
| CONST cdecl_list { List.rev ($2 false) }
| nodespec_list state_annot node_ident_decl LPAR vdecl_list SCOL_opt RPAR RETURNS LPAR vdecl_list SCOL_opt RPAR SCOL_opt locals LET stmt_list TEL
{
- let stmts, asserts, annots = $16 in
+ let stmts, asserts, annots = $16 in
(* Declaring eqs annots *)
List.iter (fun ann ->
List.iter (fun (key, _) ->
@@ -214,26 +218,26 @@ top_decl:
) ann.annots
) annots;
(* Building the node *)
- let nd = mktop_decl false (Node
- {node_id = $3;
- node_type = Types.new_var ();
- node_clock = Clocks.new_var true;
- node_inputs = List.rev $5;
- node_outputs = List.rev $10;
- node_locals = List.rev $14;
- node_gencalls = [];
- node_checks = [];
- node_asserts = asserts;
- node_stmts = stmts;
- node_dec_stateless = $2;
- node_stateless = None;
- node_spec = $1;
- node_annot = annots})
- in
- pop_node ();
+ let nd = mktop_decl false (Node
+ {node_id = $3;
+ node_type = Types.new_var ();
+ node_clock = Clocks.new_var true;
+ node_inputs = List.rev $5;
+ node_outputs = List.rev $10;
+ node_locals = List.rev $14;
+ node_gencalls = [];
+ node_checks = [];
+ node_asserts = asserts;
+ node_stmts = stmts;
+ node_dec_stateless = $2;
+ node_stateless = None;
+ node_spec = $1;
+ node_annot = annots})
+ in
+ pop_node ();
(*add_node $3 nd;*) [nd] }
-
- nodespec_list:
+
+nodespec_list:
{ None }
| NODESPEC nodespec_list {
(function
@@ -264,7 +268,7 @@ typeconst:
TINT array_typ_decl { $2 Tydec_int }
| TBOOL array_typ_decl { $2 Tydec_bool }
| TREAL array_typ_decl { $2 Tydec_real }
-| TFLOAT array_typ_decl { $2 Tydec_float }
+/* | TFLOAT array_typ_decl { $2 Tydec_float } */
| type_ident array_typ_decl { $2 (Tydec_const $1) }
| TBOOL TCLOCK { Tydec_clock Tydec_bool }
| IDENT TCLOCK { Tydec_clock (Tydec_const $1) }
@@ -313,8 +317,8 @@ assert_:
| ASSERT expr SCOL {mkassert ($2)}
eq:
- ident_list EQ expr SCOL {mkeq (List.rev $1,$3)}
-| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev $2,$5)}
+ ident_list EQ expr SCOL {mkeq (List.rev (List.map fst $1), $3)}
+| LPAR ident_list RPAR EQ expr SCOL {mkeq (List.rev (List.map fst $2), $5)}
lustre_spec:
| contract EOF { $1 }
@@ -369,8 +373,8 @@ dim_list:
expr:
/* constants */
INT {mkexpr (Expr_const (Const_int $1))}
-| REAL {mkexpr (Expr_const (Const_real $1))}
-| FLOAT {mkexpr (Expr_const (Const_float $1))}
+| REAL {let c,e,s = $1 in mkexpr (Expr_const (Const_real (c,e,s)))}
+/* | FLOAT {mkexpr (Expr_const (Const_float $1))}*/
/* Idents or type enum tags */
| IDENT { mkexpr (Expr_ident $1) }
| tag_ident { mkexpr (Expr_ident $1) (*(Expr_const (Const_tag $1))*) }
@@ -395,13 +399,13 @@ expr:
{(*mkexpr (Expr_fby ($1,$3))*)
mkexpr (Expr_arrow ($1, mkexpr (Expr_pre $3)))}
| expr WHEN vdecl_ident
- {mkexpr (Expr_when ($1,$3,tag_true))}
+ {mkexpr (Expr_when ($1,fst $3,tag_true))}
| expr WHENNOT vdecl_ident
- {mkexpr (Expr_when ($1,$3,tag_false))}
+ {mkexpr (Expr_when ($1,fst $3,tag_false))}
| expr WHEN tag_ident LPAR vdecl_ident RPAR
- {mkexpr (Expr_when ($1, $5, $3))}
+ {mkexpr (Expr_when ($1, fst $5, $3))}
| MERGE vdecl_ident handler_expr_list
- {mkexpr (Expr_merge ($2,$3))}
+ {mkexpr (Expr_merge (fst $2,$3))}
/* Applications */
| node_ident LPAR expr RPAR
@@ -497,12 +501,12 @@ signed_const_struct:
signed_const:
INT {Const_int $1}
-| REAL {Const_real $1}
-| FLOAT {Const_float $1}
+| REAL {let c,e,s =$1 in Const_real (c,e,s)}
+/* | FLOAT {Const_float $1} */
| tag_ident {Const_tag $1}
| MINUS INT {Const_int (-1 * $2)}
-| MINUS REAL {Const_real ("-" ^ $2)}
-| MINUS FLOAT {Const_float (-1. *. $2)}
+| MINUS REAL {let c,e,s = $2 in Const_real (Num.minus_num c, e, "-" ^ s)}
+/* | MINUS FLOAT {Const_float (-1. *. $2)} */
| LCUR signed_const_struct RCUR { Const_struct $2 }
| LBRACKET signed_const_array RBRACKET { Const_array $2 }
@@ -567,11 +571,11 @@ vdecl_list:
vdecl:
ident_list COL typeconst clock
- { List.map (fun id -> mkvar_decl (id, mktyp $3, $4, false, None)) $1 }
+ { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None) loc) $1 }
| CONST ident_list /* static parameters don't have clocks */
- { List.map (fun id -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None)) $2 }
+ { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, None) loc) $2 }
| CONST ident_list COL typeconst /* static parameters don't have clocks */
- { List.map (fun id -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None)) $2 }
+ { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, None) loc) $2 }
local_vdecl_list:
local_vdecl {$1}
@@ -579,13 +583,13 @@ local_vdecl_list:
local_vdecl:
/* Useless no ?*/ ident_list
- { List.map (fun id -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None)) $1 }
+ { List.map (fun (id, loc) -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false, None) loc) $1 }
| ident_list COL typeconst clock
- { List.map (fun id -> mkvar_decl (id, mktyp $3, $4, false, None)) $1 }
+ { List.map (fun (id, loc) -> mkvar_decl (id, mktyp $3, $4, false, None) loc) $1 }
| CONST vdecl_ident EQ expr /* static parameters don't have clocks */
- { [ mkvar_decl ($2, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4) ] }
+ { let (id, loc) = $2 in [ mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, true, Some $4) loc] }
| CONST vdecl_ident COL typeconst EQ expr /* static parameters don't have clocks */
- { [ mkvar_decl ($2, mktyp $4, mkclock Ckdec_any, true, Some $6) ] }
+ { let (id, loc) = $2 in [ mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true, Some $6) loc] }
cdecl_list:
cdecl SCOL { (fun itf -> [$1 itf]) }
diff --git a/src/printers.ml b/src/printers.ml
index f2cb78de90939b4e16689b82c89f8a199bdfdfdf..769dd1a8234951f914ac38d97327588ea651d42f 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -16,12 +16,16 @@ open Utils
(* Prints [v] as [pp_fun] would do, but adds a backslash at each end of line,
following the C convention for multiple lines macro *)
let pp_as_c_macro pp_fun fmt v =
- let (out, flush, newline, spaces) = pp_get_all_formatter_output_functions fmt () in
- let macro_newline () = (out "\\" 0 1; newline ()) in
+ let formatter_out_funs = pp_get_formatter_out_functions fmt () in
+ let macro_newline () =
+ begin
+ formatter_out_funs.out_string "\\" 0 1;
+ formatter_out_funs.out_newline ()
+ end in
begin
- pp_set_all_formatter_output_functions fmt out flush macro_newline spaces;
+ pp_set_formatter_out_functions fmt { formatter_out_funs with out_newline = macro_newline };
pp_fun fmt v;
- pp_set_all_formatter_output_functions fmt out flush newline spaces;
+ pp_set_formatter_out_functions fmt formatter_out_funs;
end
let rec print_dec_struct_ty_field fmt (label, cty) =
@@ -30,8 +34,7 @@ and print_dec_ty fmt cty =
match (*get_repr_type*) cty with
| Tydec_any -> fprintf fmt "Any"
| Tydec_int -> fprintf fmt "int"
- | Tydec_real
- | Tydec_float -> fprintf fmt "real"
+ | Tydec_real -> fprintf fmt "real"
| Tydec_bool -> fprintf fmt "bool"
| Tydec_clock cty' -> fprintf fmt "%a clock" print_dec_ty cty'
| Tydec_const c -> fprintf fmt "%s" c
@@ -57,8 +60,8 @@ let rec pp_struct_const_field fmt (label, c) =
and pp_const 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_real (c, e, s) -> pp_print_string fmt s (*if e = 0 then pp_print_int fmt c else if e < 0 then Format.fprintf fmt "%ie%i" c (-e) else Format.fprintf fmt "%ie-%i" c e *)
+ (* | Const_float r -> pp_print_float fmt r *)
| Const_tag t -> pp_print_string fmt t
| Const_array ca -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
| Const_struct fl -> Format.fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
@@ -131,7 +134,7 @@ and pp_eexpr fmt e =
and pp_expr_annot fmt expr_ann =
let pp_annot fmt (kwds, ee) =
- Format.fprintf fmt "(*! %t: %a *)"
+ Format.fprintf fmt "(*! %t: %a; *)"
(fun fmt -> match kwds with | [] -> assert false | [x] -> Format.pp_print_string fmt x | _ -> Format.fprintf fmt "/%a/" (fprintf_list ~sep:"/" Format.pp_print_string) kwds)
pp_eexpr ee
in
@@ -205,7 +208,7 @@ and pp_var_type_dec_desc fmt tdesc =
| Tydec_any -> fprintf fmt "<any>"
| Tydec_int -> fprintf fmt "int"
| Tydec_real -> fprintf fmt "real"
- | Tydec_float -> fprintf fmt "float"
+ (* | Tydec_float -> fprintf fmt "float" *)
| Tydec_bool -> fprintf fmt "bool"
| Tydec_clock t -> fprintf fmt "%a clock" pp_var_type_dec_desc t
| Tydec_const t -> fprintf fmt "%s" t
diff --git a/src/scheduling.ml b/src/scheduling.ml
index 8238aa7c8e69fbca13cc7a478ea27dfbf6b39ccf..d2d608e6100e9ed8ffecb251bbdc765ce1c5237a 100644
--- a/src/scheduling.ml
+++ b/src/scheduling.ml
@@ -17,14 +17,18 @@ open Causality
type schedule_report =
{
+ (* the scheduled node *)
+ node : node_desc;
(* a schedule computed wrt the dependency graph *)
schedule : ident list list;
(* the set of unused variables (no output or mem depends on them) *)
unused_vars : ISet.t;
(* the table mapping each local var to its in-degree *)
fanin_table : (ident, int) Hashtbl.t;
+ (* the dependency graph *)
+ dep_graph : IdentDepGraph.t;
(* the table mapping each assignment to a reusable variable *)
- reuse_table : (ident, var_decl) Hashtbl.t
+ (*reuse_table : (ident, var_decl) Hashtbl.t*)
}
(* Topological sort with a priority for variables belonging in the same equation lhs.
@@ -125,7 +129,7 @@ let filter_original n vl =
if vdecl.var_orig then v :: res else res) vl []
let schedule_node n =
- let node_vars = get_node_vars n in
+ (* let node_vars = get_node_vars n in *)
try
let eq_equiv = ExprDep.node_eq_equiv n in
let eq_equiv v1 v2 =
@@ -134,13 +138,6 @@ let schedule_node n =
with Not_found -> false in
let n', g = global_dependency n in
- Log.report ~level:5
- (fun fmt ->
- Format.fprintf fmt
- "dependency graph for node %s: %a"
- n'.node_id
- pp_dep_graph g
- );
(* TODO X: extend the graph with inputs (adapt the causality analysis to deal with inputs
compute: coi predecessors of outputs
@@ -152,17 +149,17 @@ let schedule_node n =
let sort = topological_sort eq_equiv g in
let unused = Liveness.compute_unused_variables n gg in
let fanin = Liveness.compute_fanin n gg in
+ { node = n'; schedule = sort; unused_vars = unused; fanin_table = fanin; dep_graph = gg; }
- let (disjoint, reuse) =
- if !Options.optimization >= 3
- then
- let disjoint = Disjunction.clock_disjoint_map node_vars in
- (disjoint,
- Liveness.compute_reuse_policy n sort disjoint gg)
- else
- (Hashtbl.create 1,
- Hashtbl.create 1) in
+ with (Causality.Cycle vl) as exc ->
+ let vl = filter_original n vl in
+ pp_error Format.err_formatter vl;
+ raise exc
+let compute_node_reuse_table report =
+ let disjoint = Disjunction.clock_disjoint_map (get_node_vars report.node) in
+ let reuse = Liveness.compute_reuse_policy report.node report.schedule disjoint report.dep_graph in
+(*
if !Options.print_reuse
then
begin
@@ -186,24 +183,44 @@ let schedule_node n =
Liveness.pp_reuse_policy reuse
);
end;
- n', { schedule = sort; unused_vars = unused; fanin_table = fanin; reuse_table = reuse }
- with (Causality.Cycle vl) as exc ->
- let vl = filter_original n vl in
- pp_error Format.err_formatter vl;
- raise exc
+*)
+ reuse
+
let schedule_prog prog =
List.fold_right (
fun top_decl (accu_prog, sch_map) ->
match top_decl.top_decl_desc with
| Node nd ->
- let nd', report = schedule_node nd in
- {top_decl with top_decl_desc = Node nd'}::accu_prog,
+ let report = schedule_node nd in
+ {top_decl with top_decl_desc = Node report.node}::accu_prog,
IMap.add nd.node_id report sch_map
| _ -> top_decl::accu_prog, sch_map
)
prog
([],IMap.empty)
+
+
+let compute_prog_reuse_table report =
+ IMap.map compute_node_reuse_table report
+
+(* removes inlined local variables from schedule report,
+ which are now useless *)
+let remove_node_inlined_locals locals report =
+ let is_inlined v = IMap.exists (fun l _ -> v = l) locals in
+ let schedule' =
+ List.fold_right (fun heads q -> let heads' = List.filter (fun v -> not (is_inlined v)) heads
+ in if heads' = [] then q else heads'::q)
+ report.schedule [] in
+ begin
+ IMap.iter (fun v _ -> Hashtbl.remove report.fanin_table v) locals;
+ IMap.iter (fun v _ -> let iv = ExprDep.mk_instance_var v
+ in Liveness.replace_in_dep_graph v iv report.dep_graph) locals;
+ { report with schedule = schedule' }
+ end
+
+let remove_prog_inlined_locals removed reuse =
+ IMap.mapi (fun id -> remove_node_inlined_locals (IMap.find id removed)) reuse
let pp_eq_schedule fmt vl =
match vl with
@@ -222,7 +239,13 @@ let pp_schedule fmt node_schs =
let pp_fanin_table fmt node_schs =
IMap.iter
(fun nd report ->
- Format.fprintf fmt "%s : %a" nd Liveness.pp_fanin report.fanin_table)
+ Format.fprintf fmt "%s: %a" nd Liveness.pp_fanin report.fanin_table)
+ node_schs
+
+let pp_dep_graph fmt node_schs =
+ IMap.iter
+ (fun nd report ->
+ Format.fprintf fmt "%s dependency graph: %a" nd pp_dep_graph report.dep_graph)
node_schs
let pp_warning_unused fmt node_schs =
@@ -236,11 +259,12 @@ let pp_warning_unused fmt node_schs =
(fun u ->
let vu = get_node_var u nd in
if vu.var_orig
- then Format.fprintf fmt "Warning: variable '%s' seems unused@.%a@." u Location.pp_loc vu.var_loc)
+ then Format.fprintf fmt " Warning: variable '%s' seems unused@, %a@,@," u Location.pp_loc vu.var_loc)
unused
)
node_schs
+
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/splitting.ml b/src/splitting.ml
index e830b614526893b5df3fabf83b73506f885d68af..a41001d31ef3792557cf3b98f51be218cf39dd13 100644
--- a/src/splitting.ml
+++ b/src/splitting.ml
@@ -21,7 +21,7 @@ let rec tuple_split_expr expr =
| Expr_ident _ -> [expr]
| Expr_tuple elist -> elist
| Expr_appl (id, args, r) ->
- if Basic_library.is_internal_fun id
+ if Basic_library.is_homomorphic_fun id
then
let args_list = List.map tuple_split_expr (expr_list_of_expr args) in
List.map
diff --git a/src/stateless.ml b/src/stateless.ml
index 3148e032dbe599d42776636a814c04a92499afe0..10acf40c03139383fb3266103f9defcd42d95c82 100755
--- a/src/stateless.ml
+++ b/src/stateless.ml
@@ -13,8 +13,9 @@ open LustreSpec
open Corelang
type error =
-| Stateful_kwd of ident
-| Stateful_imp of ident
+| Stateful_kwd of ident
+| Stateful_imp of ident
+| Stateful_ext_C of ident
exception Error of Location.t * error
@@ -34,7 +35,7 @@ let rec check_expr expr =
| Expr_merge (i, hl) -> List.for_all (fun (t, h) -> check_expr h) hl
| Expr_appl (i, e', i') ->
check_expr e' &&
- (Basic_library.is_internal_fun i || check_node (node_from_name i))
+ (Basic_library.is_stateless_fun i || check_node (node_from_name i))
and compute_node nd =
List.for_all (fun eq -> check_expr eq.eq_rhs) (get_node_eqs nd)
and check_node td =
@@ -50,12 +51,28 @@ and check_node td =
else (nd.node_dec_stateless <- stateless; stateless)
end
| Some stl -> stl)
- | ImportedNode nd -> nd.nodei_stateless
+ | ImportedNode nd ->
+ begin
+ (if nd.nodei_prototype = Some "C" && not nd.nodei_stateless
+ then raise (Error (td.top_decl_loc, Stateful_ext_C nd.nodei_id)));
+ nd.nodei_stateless
+ end
| _ -> true
let check_prog decls =
List.iter (fun td -> ignore (check_node td)) decls
+
+let force_prog decls =
+ let force_node td =
+ match td.top_decl_desc with
+ | Node nd -> (
+ nd.node_dec_stateless <- false;
+ nd.node_stateless <- Some false)
+ | _ -> ()
+ in
+ List.iter (fun td -> ignore (force_node td)) decls
+
let check_compat_decl decl =
match decl.top_decl_desc with
| ImportedNode nd ->
@@ -75,13 +92,17 @@ let check_compat header =
let pp_error fmt err =
match err with
| Stateful_kwd nd ->
- Format.fprintf fmt
- "node %s should be stateless but is actually stateful.@."
- nd
+ Format.fprintf fmt
+ "node %s should be stateless but is actually stateful.@."
+ nd
| Stateful_imp nd ->
- Format.fprintf fmt
- "node %s is declared stateless but is actually stateful.@."
- nd
+ Format.fprintf fmt
+ "node %s is declared stateless but is actually stateful.@."
+ nd
+ | Stateful_ext_C nd ->
+ Format.fprintf fmt
+ "node %s with declared prototype C cannot be stateful, it has to be a function.@."
+ nd
(* Local Variables: *)
(* compile-command:"make -C .." *)
diff --git a/src/type_predef.ml b/src/type_predef.ml
index 0690be222ffd8afb77707d1437f84f12290e3ac5..e9c1cfb2370fe42acfc6e395a43ea053d49291d1 100755
--- a/src/type_predef.ml
+++ b/src/type_predef.ml
@@ -26,7 +26,6 @@ let type_arrow ty1 ty2 = new_ty (Tarrow (ty1, ty2))
let type_array d ty = new_ty (Tarray (d, ty))
let type_static d ty = new_ty (Tstatic (d, ty))
-
let type_unary_bool_op =
new_ty (Tarrow (type_bool, type_bool))
diff --git a/src/types.ml b/src/types.ml
index 299131ffe81e9efb3e213be30960da4161c875fa..8c4bf2def9d14484fcbe63bdd4dfc29ee3ea40ba 100755
--- a/src/types.ml
+++ b/src/types.ml
@@ -173,6 +173,9 @@ let pp_error fmt = function
let new_id = ref (-1)
+let rec bottom =
+ { tdesc = Tlink bottom; tid = -666 }
+
let new_ty desc =
incr new_id; {tdesc = desc; tid = !new_id }
@@ -198,14 +201,30 @@ let get_field_type ty label =
| Tstruct fl -> (try Some (List.assoc label fl) with Not_found -> None)
| _ -> None
-let is_numeric_type ty =
+let rec is_scalar_type ty =
+ match (repr ty).tdesc with
+ | Tstatic (_, ty) -> is_scalar_type ty
+ | Tbool
+ | Tint
+ | Treal -> true
+ | _ -> false
+
+let rec is_numeric_type ty =
match (repr ty).tdesc with
+ | Tstatic (_, ty) -> is_numeric_type ty
| Tint
| Treal -> true
| _ -> false
-let is_bool_type ty =
+let rec is_real_type ty =
+ match (repr ty).tdesc with
+ | Tstatic (_, ty) -> is_real_type ty
+ | Treal -> true
+ | _ -> false
+
+let rec is_bool_type ty =
match (repr ty).tdesc with
+ | Tstatic (_, ty) -> is_bool_type ty
| Tbool -> true
| _ -> false
@@ -288,7 +307,7 @@ let rec array_base_type ty =
| _ -> ty
let is_address_type ty =
- is_array_type ty || is_struct_type ty
+ is_array_type ty || is_struct_type ty || (is_real_type ty && !Options.mpfr)
let rec is_generic_type ty =
match (dynamic_type ty).tdesc with
@@ -313,10 +332,11 @@ let type_of_type_list tyl =
else
List.hd tyl
-let type_list_of_type ty =
+let rec type_list_of_type ty =
match (repr ty).tdesc with
- | Ttuple tl -> tl
- | _ -> [ty]
+ | Tstatic (_, ty) -> type_list_of_type ty
+ | Ttuple tl -> tl
+ | _ -> [ty]
(** [is_polymorphic ty] returns true if [ty] is polymorphic. *)
let rec is_polymorphic ty =
diff --git a/src/typing.ml b/src/typing.ml
index 747240eedc75ad237749555b438d1f0291a77f85..d20b3c0ffaa2177dcda5f6d555cf49c3fa39d5b6 100755
--- a/src/typing.ml
+++ b/src/typing.ml
@@ -103,7 +103,7 @@ let rec type_coretype type_dim cty =
| Tydec_any -> new_var ()
| Tydec_int -> Type_predef.type_int
| Tydec_real -> Type_predef.type_real
- | Tydec_float -> Type_predef.type_real
+ (* | Tydec_float -> Type_predef.type_real *)
| Tydec_bool -> Type_predef.type_bool
| Tydec_clock ty -> Type_predef.type_clock (type_coretype type_dim ty)
| Tydec_const c -> Type_predef.type_const c
@@ -261,7 +261,7 @@ and type_const loc c =
match c with
| Const_int _ -> Type_predef.type_int
| Const_real _ -> Type_predef.type_real
- | Const_float _ -> Type_predef.type_real
+ (* | Const_float _ -> Type_predef.type_real *)
| Const_array ca -> let d = Dimension.mkdim_int loc (List.length ca) in
let ty = new_var () in
List.iter (fun e -> try_unify ty (type_const loc e) loc) ca;
@@ -344,7 +344,7 @@ and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
*)
and type_appl env in_main loc const f args =
let targs = List.map (type_expr env in_main const) args in
- if Basic_library.is_internal_fun f && List.exists is_tuple_type targs
+ if Basic_library.is_homomorphic_fun f && List.exists is_tuple_type targs
then
try
let targs = Utils.transpose_list (List.map type_list_of_type targs) in
@@ -575,14 +575,13 @@ let type_var_decl vd_env env vdecl =
let type_dim d =
begin
type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
-
Dimension.eval Basic_library.eval_env eval_const d;
end in
let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
let ty_static =
if vdecl.var_dec_const
- then Type_predef.type_static (Dimension.mkdim_var ()) ty
+ then Type_predef.type_static (Dimension.mkdim_var ()) ty
else ty in
(match vdecl.var_dec_value with
| None -> ()
diff --git a/src/utils.ml b/src/utils.ml
index 7be8bb142fc4715106acb29d9c8e8cdc10dd9dac..ee8d9dd6d0aacfba6fc7b75553235644e643dcb1 100755
--- a/src/utils.ml
+++ b/src/utils.ml
@@ -36,7 +36,8 @@ module IMap = Map.Make(IdentModule)
module ISet = Set.Make(IdentModule)
-let desome x = match x with Some x -> x | None -> failwith "desome"
+exception DeSome
+let desome x = match x with Some x -> x | None -> raise DeSome
let option_map f o =
match o with
diff --git a/test/test-compile.sh b/test/test-compile.sh
old mode 100755
new mode 100644
index ceafcdd05e5c58cd76f85a3f8f96b010c283cf8d..f68224e87dff90e98ea45ee1012242b2015bc05e
--- a/test/test-compile.sh
+++ b/test/test-compile.sh
@@ -5,16 +5,18 @@ eval set -- $(getopt -n $0 -o "-aciwvh:" -- "$@")
declare c i w h a v
declare -a files
-#SRC_PREFIX="../.."
-SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
+SRC_PREFIX=/home/thirioux/RECHERCHE/lustrec-tests/
+#SRC_PREFIX=`svn info --xml | grep wcroot | sed "s/<[^>]*>//g"`/lustre_compiler
NOW=`date "+%y%m%d%H%M"`
-report=`pwd`/report-$NOW
-#LUSTREC="../../_build/src/lustrec"
+report=`pwd`/report-1.1-440-$NOW
LUSTREC=lustrec
mkdir -p build
build=`pwd`"/build"
gcc_compile() {
+ if [ $verbose -gt 1 ]; then
+ echo "gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ $1.c > /dev/null"
+ fi
gcc -c -Wall -Wno-unused-but-set-variable -I ../../include/ "$1".c > /dev/null;
if [ $? -ne 0 ]; then
rgcc="INVALID";
@@ -24,6 +26,9 @@ gcc_compile() {
}
lustrec_compile() {
+ if [ $verbose -gt 1 ]; then
+ echo "$LUSTREC $@"
+ fi
$LUSTREC "$@";
if [ $? -ne 0 ]; then
rlustrec="INVALID";
@@ -112,37 +117,59 @@ inline_compile_with_check () {
while IFS=, read -r file main opts
do
name=`basename "$file" .lus`
- if [ "$name" = "$file" ]; then
- return 0
+ ext=".lus"
+ if [ `dirname "$file"`/"$name" = "$file" ]; then
+ name=`basename "$file" .lusi`
+ ext=".lusi"
fi
dir=${SRC_PREFIX}/`dirname "$file"`
pushd $dir > /dev/null
- lustrec_compile -d $build -verbose 0 $opts -inline -witnesses -node $main $name".lus"
- pushd $build > /dev/null
- gcc_compile "$name"
+ 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
+ popd > /dev/null
+ pushd $build > /dev/null
- popd > /dev/null
+ if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
+ gcc_compile "$name";
+ else
+ rgcc="NONE"
+ fi
# Cheching witness
- pushd $build > /dev/null
- 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
- rinlining="VALID";
- elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
- rinlining="ERROR";
- elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
- rinlining="UNKNOWN";
- else
- rinlining="INVALID/TIMEOUT"
- fi
- if [ $verbose -gt 0 ]; then
- echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
- else
- 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
+
+ if [ "$main" != "" ] && [ $ext = ".lus" ] && [ "$opts" != "-lusi" ]; then
+ mv ${name}_witnesses/inliner_witness.lus ${name}_inliner_witness.lus
+ lustrec_compile -verbose 0 -horn-traces -node check ${name}_inliner_witness.lus
+ z3="`z3 -T:10 ${name}_inliner_witness.smt2 | xargs`"
+ if [ "x`echo $z3 | grep -o unsat`" == "xunsat" ]; then
+ rinlining="VALID";
+ elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
+ rinlining="ERROR";
+ elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
+ rinlining="UNKNOWN";
+ elif [ "x`echo $z3 | xargs | grep -o timeout`" == "xtimeout" ]; then
+ rinlining="TIMEOUT"
+ else
+ rinlining="INVALID"
+ fi
+ else
+ rinlining="NONE"
+ fi
+ popd > /dev/null
+
+ if [ $verbose -gt 0 ]; then
+ echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report;
+ else
+ echo "lustrec inlined ($rlustrec), gcc ($rgcc), inlining check ($rinlining), $dir, ${name}${ext}, node $main" | column -t -s',' | tee -a $report | grep "TIMEOUT\|INVALID\|ERROR\|UNKNOWN"
+ fi
done < $file_list
}
@@ -159,18 +186,24 @@ check_prop () {
# Checking horn backend
if [ "$main" != "" ]; then
- lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts -node $main $name".lus";
+ lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts -node $main $name".lus";
else
- lustrec_compile -horn-traces -horn-queries -d $build -verbose 0 $opts $name".lus"
+ lustrec_compile -horn-traces -horn-query -d $build -verbose 0 $opts $name".lus"
fi
# 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
- rhorn="INVALID";
+ z3="`z3 -T:10 ${build}/${name}.smt2 | xargs`"
+ if [ "x`echo $z3 | grep -o unsat`" == "xunsat" ]; then
+ rhorn="VALID";
+ elif [ "x`echo $z3 | xargs | grep -o error`" == "xerror" ]; then
+ rhorn="ERROR";
+ elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
+ rhorn="UNKNOWN";
+ elif [ "x`echo $z3 | xargs | grep -o timeout`" == "xtimeout" ]; then
+ rhorn="TIMEOUT"
else
- rhorn="VALID"
+ rhorn="INVALID"
fi
if [ $verbose -gt 0 ]; then
echo "lustrec ($rlustrec), horn-pdr ($rhorn), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;
diff --git a/test/tests_ok_dev.list b/test/tests_ok_dev.list
index 527cdab142267edcc74df69888b9c6a9bc2d69d5..098d691fbc01586908cd26ea6c2c1520ef3ccec1 100644
--- a/test/tests_ok_dev.list
+++ b/test/tests_ok_dev.list
@@ -1,6 +1,7 @@
./tests/tuples/tuples1.lus
./tests/tuples/tuples2.lus
./tests/arrays_arnaud/dummy_lib.lusi
+./tests/arrays_arnaud/arrays.lusi
./tests/arrays_arnaud/arrays.lus,,-check-access
./tests/arrays_arnaud/RelOpMatrix.lus
./tests/arrays_arnaud/access1.lus,,-check-access
@@ -20,6 +21,7 @@
./tests/clocks/oversampling0.lus,,-lusi
./tests/clocks/oversampling0.lusi
./tests/clocks/oversampling0.lus
+./tests/clocks/oversampling0.lus,,-O 3
./tests/lusic/test2.lusi
./tests/lusic/test1.lusi
./tests/lusic/test1.lus,as_soon_as