diff --git a/Makefile b/Makefile index 30c1faf..5fce4ef 100644 --- a/Makefile +++ b/Makefile @@ -7,6 +7,12 @@ all: install: (cd compiler; $(MAKE) install) (cd lib; $(MAKE) install) + $(INSTALL) tools/$(BZREAX) $(INSTALL_BINDIR) + +uninstall: + (cd compiler; $(MAKE) uninstall) + (cd lib; $(MAKE) uninstall) + $(RM) $(INSTALL_BINDIR)/$(BZREAX) clean: (cd compiler; $(MAKE) clean) diff --git a/compiler/Makefile b/compiler/Makefile index 9ce2c29..434d95e 100644 --- a/compiler/Makefile +++ b/compiler/Makefile @@ -30,6 +30,9 @@ install: $(INSTALL) -d $(INSTALL_BINDIR) $(foreach t,$(BIN),$(INSTALL) $(t).$(TARGET) $(INSTALL_BINDIR)/$(t);) +uninstall: + $(foreach t,$(BIN),$(RM) $(INSTALL_BINDIR)/$(t);) + clean: $(OCAMLBUILD) -clean diff --git a/config.in b/config.in index c6339e2..cb74631 100644 --- a/config.in +++ b/config.in @@ -6,12 +6,14 @@ bindir = @bindir@ libdir = @libdir@ INSTALL= @INSTALL@ +RM=rm @SET_MAKE@ BUILD= _build COMPILER=heptc SIMULATOR=hepts CTRLNBAC2EPT_TRANSLATOR=ctrl2ept +BZREAX=bzreax INSTALL_BINDIR=$(bindir) INSTALL_LIBDIR=$(libdir)/heptagon diff --git a/configure b/configure index 8433ce6..e47b83d 100755 --- a/configure +++ b/configure @@ -588,6 +588,7 @@ LIBOBJS enable_ctrl2ept enable_simulator stdlib_dir +RM INSTALL OCAML_PKG_reatk_ctrlNbac OCAML_PKG_lablgtk2 @@ -2893,8 +2894,8 @@ if test "$OCAMLC" = "no"; then fi case "$OCAMLVERSION" in - 0.*|1.*|2.*|3.0*) - as_fn_error $? "You need Objective Caml 3.10 or higher" "$LINENO" 5;; + 0.*|1.*|2.*|3.*) + as_fn_error $? "You need Objective Caml 4.00 or higher" "$LINENO" 5;; esac @@ -4033,6 +4034,7 @@ fi + ac_config_files="$ac_config_files config" cat >confcache <<\_ACEOF diff --git a/configure.in b/configure.in index a9c64fe..0f458b1 100644 --- a/configure.in +++ b/configure.in @@ -22,8 +22,8 @@ if test "$OCAMLC" = "no"; then fi case "$OCAMLVERSION" in - 0.*|1.*|2.*|3.0*) - AC_MSG_ERROR(You need Objective Caml 3.10 or higher);; + 0.*|1.*|2.*|3.*) + AC_MSG_ERROR(You need Objective Caml 4.00 or higher);; esac AC_PROG_CAMLP4 @@ -83,6 +83,7 @@ fi AC_SUBST(INSTALL) +AC_SUBST(RM) AC_SUBST(stdlib_dir) AC_SUBST(enable_simulator) diff --git a/lib/Makefile b/lib/Makefile index 5b077da..6d1548e 100644 --- a/lib/Makefile +++ b/lib/Makefile @@ -24,6 +24,10 @@ install: all $(INSTALL) -d $(INSTALL_LIBDIR)/$(C_DIR) (cd c/; $(INSTALL) $(C_OBJ) $(INSTALL_LIBDIR)/$(C_DIR)) +uninstall: + $(foreach f,$(STDLIB_OBJ) $(STDLIB_INTERFACE),$(RM) $(INSTALL_LIBDIR)/$(f)) + $(RM) $(INSTALL_LIBDIR)/$(C_DIR)/$(C_OBJ) + clean: rm -f *.epci diff --git a/tools/bzreax b/tools/bzreax new file mode 100755 index 0000000..998a9ec --- /dev/null +++ b/tools/bzreax @@ -0,0 +1,190 @@ +#!/bin/bash +# +# Copyright (C) 2014 Nicolas Berthier +# +# This program is free software: you can redistribute it and/or modify +# it under the terms of the GNU General Public License as published by +# the Free Software Foundation, either version 3 of the License, or +# (at your option) any later version. +# +# This program is distributed in the hope that it will be useful, but +# WITHOUT ANY WARRANTY; without even the implied warranty of +# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU +# General Public License for more details. +# +# You should have received a copy of the GNU General Public License +# along with this program. If not, see +# . +# + +verbose="no"; +dry_run="no"; + +# --- + +# readlink should be available on any "recent" system: +. "$(dirname "$(readlink -f "$0")")/libvthighlight"; +cmd_beg="${term_color_cyan}"; +info_beg="${term_color_lightgreen}"; +warn_beg="${term_color_lightred}"; +err_beg="${term_color_red}${term_bold}"; +msg_end="${term_normal}${term_restore}"; + +# --- + +info () { echo -e "Info: ${info_beg}$@${msg_end}" >/dev/stderr; } +warn () { echo -e "Warn: ${warn_beg}$@${msg_end}" >/dev/stderr; } +error () { echo -e "Error: ${err_beg}$@${msg_end}" >/dev/stderr; usage; exit 1; } +execcmd () { + if test "x${verbose}" = "xyes"; then + echo -e "\$ ${cmd_beg}$@${msg_end}" >/dev/stderr; + fi; + if test "x${dry_run}" != "xyes"; then + eval "$@" || exit 1; + fi +} + +# --- + +file=""; +node=""; +reax_algo="sB"; +reax_opti=(); +reach_var=""; + +heptc_opts=(); +reax_opts=(); +gcc_opts=(); + +# chk_reach="no"; +sim="no"; + +simexec="sim"; +reax="reax"; + +usage () { + cat >/dev/stderr < [ ] [ -- ] +where available options are: + + -a | --algo Synthesis algorithm specification for ReaX (default + is "sB") + -O | --optim Optimization specification for ReaX + -r | --reach State variable for reachability enforcement + -s | --sim Generate hepts-compatible simulation code + --reax-opts Pass space-separated options to ReaX + --heptc-opts Pass space-separated options to the Heptagon compiler + --gcc-opts Pass space-separated options to the Gcc compiler + --sim-exec Name of the simulation executable (default is "sim") + -v | --verbose Display executed commands + -n | --dry Run in dry mode (implies \`--verbose') + -h | --help Display this help and exit + -- Pass all remaining args to the Heptagon compiler + +Report bugs to Nicolas Berthier +EOF + exit 0 +# -cr | --chk-reach Check reachabiltiy again after optimization +} + +# --- + +while test $# \> 0 -a "x$1" != "x--"; do + case "$1" in + -a | --algo) shift; reax_algo="'$1'";; + -O | --optim) shift; reax_opti=( -O "'$1'" );; + -r | --reach) shift; reach_var="$1";; + -s | --sim) sim="yes";; + --sim-exec) shift; simexec="$1";; + # -cr | --chk-reach) chk_reach="yes";; + --reax-opts) shift; reax_opts=( "${reax_opts[@]}" $1 );; + --heptc-opts) shift; heptc_opts=( "${heptc_opts[@]}" $1 );; + --gcc-opts) shift; gcc_opts=( "${gcc_opts[@]}" $1 );; + -v | --verbose) verbose="yes";; + -n | --dry) dry_run="yes"; verbose="yes";; + -h | --help) usage;; + *) if test "x${file}" = "x"; then file="$1"; + elif test "x${node}" = "x"; then node="$1"; + else warn "Ignoring argument \`$1'!"; + fi;; + esac; + shift; +done; +test $# \> 1 -a "x$1" = "x--" && shift; +test "x${file}" = "x" && error "Missing input file"; +test \! -r "${file}" && error "Input file not found"; + +# --- + +module="$(basename "${file}" .ept)"; +if test "x${node}" = "x"; then + node="${module}"; + info "Selecting node \`${node}'."; +fi; + +if test "x${reach_var}" != "x" -a "x${reax_algo}" = "xsB"; then + reax_algo="${reax_algo}:r"; + info "Enabling reachability enforcement (algo = \`${reax_algo}')"; +fi; + +reaxargs=(); +simargs=(); +gccargs=( -c ); + +if test "x${sim}" = "xyes"; then + simargs=( -hepts -s ${node} ); + gccargs=( -o "${simexec}" ); +fi; + +# if test "x${chk_reach}" = "xyes"; then +# chk_reach="no"; # for simpler tests. +# # if test ${#reax_opti[@]} -eq 0; then +# # warn "Disabling final check of reachability property: "\ +# # "missing optimization goals."; +# # el +# if test "x${reach_var}" = "x"; then +# warn "Disabling final check of reachability property: "\ +# "no reachabiliy property specified."; +# else +# chk_reach="yes"; # for simpler tests. +# reaxargs=( -m ); +# fi; +# fi; + +# --- + +Module="${module^}"; # uppercase first letter. + +# --- + +#export HEPTLIB="$HEPT_HOME/lib"; + +# execcmd heptc "$@" -nosink "${simargs[@]}" -target c -target ctrln "${file}"; +execcmd heptc "${heptc_opts[@]}" "$@" "${simargs[@]}" -target c -target ctrln "${file}"; +cn="${module}_ctrln/${node}.ctrln"; + +test "x${reach_var}" != "x" && \ + execcmd echo "'!reachable (not __init__ and ${reach_var});'" ">>" "${cn}"; + +execcmd "${reax}" "${reax_opts[@]}" -a "${reax_algo}" "${reax_opti[@]}" \ + "${reaxargs[@]}" -s "${cn}"; + +# if test "x${chk_reach}" = "xyes"; then +# cd="${module}_ctrln/${node}.ctrld"; +# execcmd "${reax}" "${reax_opts[@]}" -a "${reax_algo}" "${cd}"; +# fi; + +execcmd ctrl2ept -n "${Module}.${node}" -v; + +execcmd heptc "${heptc_opts[@]}" "$@" -target c "${module}_controller.ept"; + +execcmd gcc "${gcc_opts[@]}" "${gccargs[@]}" \ + -I"$HEPTLIB/c" -I"${module}_c" -I"${module}_controller_c" \ + "${module}_c/"*.c "${module}_controller_c"/*.c; + +if test -x "${simexec}" -a "x${sim}" = "xyes"; then + info "To launch the simulator, run: \`hepts -mod ${Module} -node ${node}" \ + "-exec $(dirname ${simexec})/$(basename ${simexec})'"; +fi; + +# ---