diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in index 4ce114193f1f0e579c3fb4a1bd4a3ebac1b7d710..ea5ce613a207ef1e95b15c12bf6a9f9a657770de 100644 --- a/src/plugins/e-acsl/Makefile.in +++ b/src/plugins/e-acsl/Makefile.in @@ -29,6 +29,9 @@ ifndef FRAMAC_SHARE FRAMAC_SHARE :=$(shell frama-c-config -print-share-path) endif +ifndef FRAMAC_LIBDIR +FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath) +endif ################### # Plug-in sources # @@ -289,6 +292,7 @@ EACSL_DLMALLOC_LIBNAME = libeacsl-dlmalloc.a EACSL_DLMALLOC_LIB = $(EACSL_LIBDIR)/$(EACSL_DLMALLOC_LIBNAME) EACSL_DLMALLOC_SRC = $(EACSL_DLMALLOC_DIR)/dlmalloc.c EACSL_DLMALLOC_OBJ = dlmalloc.o +# Don't forget to update "e-acsl-gcc.sh" if the flags are updated EACSL_DLMALLOC_FLAGS = \ -DHAVE_MORECORE=0 \ -DHAVE_MMAP=1 \ @@ -485,7 +489,11 @@ EACSL_INSTALL_SCRIPTS=$(addprefix $(E_ACSL_DIR)/,$(EACSL_SCRIPTS)) EACSL_INSTALL_MANPAGES=$(addprefix $(E_ACSL_DIR)/,$(EACSL_MANPAGES)) -install:: +EACSL_INSTALL_LIB_DIR :=$(FRAMAC_LIBDIR)/e-acsl + +EACSL_INSTALL_CONTRIB_DIR :=$(FRAMAC_DATADIR)/e-acsl/contrib + +install:: clean-install $(PRINT_INSTALL) E-ACSL share files for dir in $(EACSL_C_DIRECTORIES); do \ $(MKDIR) $(FRAMAC_DATADIR)/$$dir && \ @@ -499,8 +507,10 @@ ifneq ("$(EACSL_INSTALL_MANUAL_FILES)","") $(CP) $(EACSL_INSTALL_MANUAL_FILES) $(FRAMAC_DATADIR)/manuals; endif $(PRINT_INSTALL) E-ACSL libraries - $(MKDIR) $(LIBDIR) - $(CP) $(EACSL_LIBDIR)/libeacsl-*.a $(LIBDIR) + $(MKDIR) $(EACSL_INSTALL_LIB_DIR) + $(CP) $(EACSL_LIBDIR)/libeacsl-*.a $(EACSL_INSTALL_LIB_DIR) + $(MKDIR) $(EACSL_INSTALL_CONTRIB_DIR)/libdlmalloc + $(CP) $(EACSL_DLMALLOC_SRC) $(EACSL_INSTALL_CONTRIB_DIR)/libdlmalloc $(PRINT_INSTALL) E-ACSL scripts $(MKDIR) $(BINDIR) $(CP) $(EACSL_INSTALL_SCRIPTS) $(BINDIR)/ @@ -519,7 +529,7 @@ uninstall:: $(PRINT_RM) E-ACSL manuals $(RM) $(FRAMAC_DATADIR)/manuals/*.pdf $(PRINT_RM) E-ACSL libraries - $(RM) $(LIBDIR)/libeacsl-*.a + $(RM) -r $(EACSL_INSTALL_LIB_DIR) $(PRINT_RM) E-ACSL scripts $(RM) $(EACSL_INSTALLED_SCRIPTS) $(PRINT_RM) E-ACSL man pages diff --git a/src/plugins/e-acsl/doc/Changelog b/src/plugins/e-acsl/doc/Changelog index cdc707e9ec8846a5a4fafcc30d86d28541dfc968..bd67f1b6a3afa5b8f5f77727a51daebe5e304e4d 100644 --- a/src/plugins/e-acsl/doc/Changelog +++ b/src/plugins/e-acsl/doc/Changelog @@ -25,6 +25,9 @@ Plugin E-ACSL ############################ +- E-ACSL [2020-11-17] Update e-acsl-gcc.sh so that the library dlmalloc + can be compiled and used from sources. + ############################# Plugin E-ACSL 22.0 (Titanium) ############################# diff --git a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 index 39e15364d47e040dab2ff1715b5a31109a079ed7..e3bc300bdb9cfecd266095c95aa89fecf275b056 100644 --- a/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 +++ b/src/plugins/e-acsl/man/e-acsl-gcc.sh.1 @@ -153,7 +153,7 @@ Valid arguments are: \fIfloat-to-int\fP \- casts from floating-point to integer. \fIdiv\fP \- division by zero. \fIshift\fP \- left and right shifts by a value out of bounds. - \fpointer-call\fP \- annotate functions calls through pointers. + \fIpointer-call\fP \- annotate functions calls through pointers. \fIall\fP \- all of the above. .TP .B -A, --rte-select=\fI @@ -212,7 +212,39 @@ launch of the \fBE-ACSL\fP plugin. add \fI\fP to the list of options that will be given to the \fBE-ACSL\fP analysis. Only useful when \fB--then\fP is in use, in which case \fI\fP will be placed after the \fB-then\fP on \fBFrama-C\fP's command-line. Otherwise, -equivalent to \fB--frama-c-extra\fP +equivalent to \fB--frama-c-extra\fP. +.TP +.B --ar=\fI +the name of the \fBAR\fP executable. Only relevant with +\fB--dlmalloc-from-sources\fP. By default the first \fIar\fP executable found in +the system path is used. +.TP +.B --ranlib=\fI +the name of the \fBRANLIB\fP executable. Only relevant with +\fB--dlmalloc-from-sources\fP. By default the first \fIranlib\fP executable +found in the system path is used. +.TP +.B --with-dlmalloc=\fI +use \fI\fP instead of distributed dlmalloc library. +.TP +.B --dlmalloc-from-sources +compile and use dlmalloc library from sources instead of using the distributed +library. Incompatible with \fB--with-dlmalloc\fP. +.TP +.B --dlmalloc-compile-only +do not instrument or compile code, only compile dlmalloc library from sources. +Implies \fB--dlmalloc-from-sources\fP and incompatible with +\fB--with-dlmalloc\fP. +.TP +.B --dlmalloc-compile-flags=\fI +compile dlmalloc library with \fI\fP compile flags. Default to +\fI-O2 -g3\fP. Unused if \fB--dlmalloc-from-sources\fP or +\fB--dlmalloc-compile-only\fP isn't used. +.TP +.B --odlmalloc=\fI +output compiled dlmalloc library to \fI\fP. Unused if +\fB--dlmalloc-from-sources\fP or \fB--dlmalloc-compile-only\fP isn't used. + .SH EXIT STATUS .TP .B 0 diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp index b05f8fe127e674e8d15bae4d8787f5c43fc8b0c4..2195d4cca8d9f0cd09df9a5d0a57093c7ceff68b 100644 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.comp +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.comp @@ -36,13 +36,15 @@ _eacsl_gcc() { --no-trace --ocode= --oexec= --oexec-e-acsl= --ld-flags= --cpp-flags= --extra-cpp-args= - --frama-c-extra= --frama-c= --gcc= --e-acsl-share= --memory-model= - --e-acsl-extra= + --frama-c-extra= --frama-c= --gcc= --ar= --ranlib= + --e-acsl-share= --memory-model= --e-acsl-extra= --compile --compile-only --print-mmodels --frama-c-only --instrumented-only --gmp --full-mtracking --rte= --rte-select= --no-int-overflow --no-stdlib --frama-c-stdlib --libc-replacements --temporal --free-valid-address --weak-validity --validate-format-strings - --heap-size --stack-size" + --heap-size --stack-size + --with-dlmalloc --dlmalloc-from-sources --dlmalloc-compile-only + --dlmalloc-compile-flags --odlmalloc" case ${prev} in -*) diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh index a168729e80b5f599b2860361e400442953aa76b4..044bd8fab58bd62175ed6405651c14984df607fa 100755 --- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh +++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh @@ -274,7 +274,9 @@ LONGOPTIONS="help,compile,compile-only,debug:,ocode:,oexec:,verbose:, frama-c:,gcc:,e-acsl-share:,instrumented-only,rte:,oexec-e-acsl:, print-mmodels,rt-debug,rte-select:,then,e-acsl-extra:,check,fail-with-code:, temporal,weak-validity,stack-size:,heap-size:,rt-verbose,free-valid-address, - external-assert:,validate-format-strings,no-trace,libc-replacements" + external-assert:,validate-format-strings,no-trace,libc-replacements, + with-dlmalloc:,dlmalloc-from-sources,dlmalloc-compile-only, + dlmalloc-compile-flags:,odlmalloc:,ar:,ranlib:" SHORTOPTIONS="h,c,C,d:,D,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,I:,G:,X,a:,T,k,V" # Prefix for an error message due to wrong arguments ERROR="ERROR parsing arguments:" @@ -285,6 +287,8 @@ OPTION_CPPFLAGS= # Preprocessor flags OPTION_LDFLAGS= # Linker flags OPTION_FRAMAC="frama-c" # Frama-C executable name OPTION_CC="gcc" # GCC executable name +OPTION_AR="ar" # AR executable name +OPTION_RANLIB="ranlib" # RANLIB executable name OPTION_ECHO="set -x" # Echo executed commands to STDOUT OPTION_INSTRUMENT=1 # Perform E-ACSL instrumentation OPTION_DEBUG= # Set Frama-C debug flag @@ -318,6 +322,11 @@ OPTION_STACK_SIZE=32 # Size of a heap shadow space (in MB) OPTION_HEAP_SIZE=128 # Size of a stack shadow space (in MB) OPTION_KEEP_GOING= # Report failing assertions but do not abort execution OPTION_EXTERNAL_ASSERT="" # Use custom definition of assert function +OPTION_WITH_DLMALLOC="" # Use provided dlmalloc library +OPTION_DLMALLOC_FROM_SOURCES= # Compile dlmalloc from sources +OPTION_DLMALLOC_COMPILE_ONLY= # Only compile dlmalloc +OPTION_DLMALLOC_COMPILE_FLAGS="-O2 -g3" # Dlmalloc compilation flags +OPTION_OUTPUT_DLMALLOC="" # Name of the compiled dlmalloc SUPPORTED_MMODELS="bittree,segment" # Supported memory model names MIN_STACK=16 # Minimal size of a tracked program stack @@ -352,8 +361,6 @@ Notes: # Base dir of this script BASEDIR="$(realpath `dirname $0`)" -# Directory with contrib libraries of E-ACSL -LIBDIR="$BASEDIR/../lib" # Run getopt ARGS=`getopt -n "$ERROR" -l "$LONGOPTIONS" -o "$SHORTOPTIONS" -- "$@"` @@ -643,12 +650,47 @@ do shift OPTION_NO_TRACE=1 ;; + --ar) + shift; + OPTION_AR="$(which $1)" + shift; + ;; + --ranlib) + shift; + OPTION_RANLIB="$(which $1)" + shift; + ;; + --with-dlmalloc) + shift; + OPTION_WITH_DLMALLOC="$1" + shift; + ;; + --dlmalloc-from-sources) + shift; + OPTION_DLMALLOC_FROM_SOURCES=1 + ;; + --dlmalloc-compile-only) + shift; + OPTION_INSTRUMENT= + OPTION_DLMALLOC_COMPILE_ONLY=1 + ;; + --dlmalloc-compile-flags) + shift; + OPTION_DLMALLOC_COMPILE_FLAGS="$1" + shift; + ;; + --odlmalloc) + shift; + OPTION_OUTPUT_DLMALLOC="$1" + shift; + ;; esac done shift; -# Bail if no files to translate are given -if [ -z "$1" ]; then +# Bail if no files to translate are given and we're not trying to only compile +# dlmalloc +if [ -z "$1" -a "$OPTION_DLMALLOC_COMPILE_ONLY" != "1" ]; then error "no input files"; fi @@ -672,6 +714,8 @@ if [ -f "$BASEDIR/../E_ACSL.mli" ]; then `test -f "$DEVELOPMENT/META.frama-c-e_acsl" -o \ -f "$FRAMAC_PLUGIN/META.frama-c-e_acsl"; echo $?` EACSL_SHARE="$DEVELOPMENT/share/e-acsl" + EACSL_LIB="$DEVELOPMENT/lib" + EACSL_CONTRIB="$DEVELOPMENT/contrib" # Add the project directory to FRAMAC_PLUGINS, # otherwise Frama-C uses an installed version if test -f "$DEVELOPMENT/META.frama-c-e_acsl"; then @@ -680,7 +724,9 @@ if [ -f "$BASEDIR/../E_ACSL.mli" ]; then else # Installed version. FRAMAC_SHARE should not be used here as Frama-C # and E-ACSL may not be installed to the same location - EACSL_SHARE="$BASEDIR/../share/frama-c/e-acsl/" + EACSL_SHARE="$BASEDIR/../share/frama-c/e-acsl" + EACSL_LIB="$BASEDIR/../lib/frama-c/e-acsl" + EACSL_CONTRIB="$BASEDIR/../share/frama-c/e-acsl/contrib" fi # Architecture-dependent flags. Since by default Frama-C uses 32-bit @@ -761,6 +807,81 @@ fi CPPFLAGS="$OPTION_CPPFLAGS" LDFLAGS="$OPTION_LDFLAGS" +# Dlmalloc +if [ -n "$OPTION_WITH_DLMALLOC" ]; then + if [ "$OPTION_DLMALLOC_FROM_SOURCES" = "1" ]; then + error "use either --with-dlmalloc FILE or --dlmalloc-from-sources" + fi + if [ "$OPTION_DLMALLOC_COMPILE_ONLY" = "1" ]; then + error "use either --with-dlmalloc FILE or --dlmalloc-compile-only" + fi + + # Use provided dlmalloc library + DLMALLOC_LIB_PATH="$OPTION_WITH_DLMALLOC" +else + # Use distributed dlmalloc library + DLMALLOC_LIB_PATH="$EACSL_LIB/libeacsl-dlmalloc.a" +fi + +if [ "$OPTION_DLMALLOC_FROM_SOURCES" = "1" -o \ + "$OPTION_DLMALLOC_COMPILE_ONLY" = "1" ]; then + # Check ar and ranlib tools + check_tool "$OPTION_AR" + check_tool "$OPTION_RANLIB" + AR="$OPTION_AR" + RANLIB="$OPTION_RANLIB" + + # Create a temporary directory to build dlmalloc. That directory will be + # removed when exiting the script + DLMALLOC_TMP_DIR=$(mktemp -d) || error "unable to create temp directory." + trap 'rm -rf "$DLMALLOC_TMP_DIR"' EXIT + + DLMALLOC_SRC="$EACSL_CONTRIB/libdlmalloc/dlmalloc.c" + DLMALLOC_OBJ="$DLMALLOC_TMP_DIR/dlmalloc.o" + + if [ -n "$OPTION_OUTPUT_DLMALLOC" ]; then + DLMALLOC_LIB_PATH="$OPTION_OUTPUT_DLMALLOC" + else + DLMALLOC_LIB_PATH="$DLMALLOC_TMP_DIR/libeacsl-dlmalloc.a" + fi + + DLMALLOC_FLAGS="\ + -DHAVE_MORECORE=0 \ + -DHAVE_MMAP=1 \ + -DNO_MALLINFO=1 \ + -DNO_MALLOC_STATS=1 \ + -DMSPACES=1 \ + -DONLY_MSPACES \ + -DMALLOC_ALIGNMENT=32 \ + -DMSPACE_PREFIX=__e_acsl_ \ + $OPTION_DLMALLOC_COMPILE_FLAGS + " + + # Compile dlmalloc from sources + ($OPTION_ECHO; \ + $CC -c $DLMALLOC_SRC $DLMALLOC_FLAGS -o$DLMALLOC_OBJ) + error "fail to compile dlmalloc." $? + ($OPTION_ECHO; \ + $AR crus $DLMALLOC_LIB_PATH $DLMALLOC_OBJ) + error "fail to create dlmalloc archive library." $? + ($OPTION_ECHO; \ + $RANLIB $DLMALLOC_LIB_PATH) + error "fail to generate dlmalloc archive index." $? + + # Exit if dlmalloc-compile-only has been used + if [ "$OPTION_DLMALLOC_COMPILE_ONLY" = "1" ]; then + # If dlmalloc-compile-only is used with instrumented-only or compile, + # display a warning message + if [ -n "$OPTION_COMPILE" -o -n "$OPTION_INSTRUMENT" -o \ + -n "$OPTION_INSTRUMENTED_ONLY" ]; then + warning "--dlmalloc-compile-only was used, the instrumentation and \ +compilation of the source code won't be run." + fi + + exit 0; + fi +fi + # Extra Frama-C Flags E-ACSL needs FRAMAC_FLAGS="$FRAMAC_FLAGS \ -remove-unused-specified-functions" @@ -768,7 +889,7 @@ FRAMAC_FLAGS="$FRAMAC_FLAGS \ # C, CPP and LD flags for compilation of E-ACSL-generated sources EACSL_CFLAGS="$OPTION_EXTERNAL_ASSERT" EACSL_CPPFLAGS="-I$EACSL_SHARE" -EACSL_LDFLAGS="$LIBDIR/libeacsl-dlmalloc.a -lgmp -lm" +EACSL_LDFLAGS="$DLMALLOC_LIB_PATH -lgmp -lm" # Output file names OUTPUT_CODE="$OPTION_OUTPUT_CODE" # E-ACSL instrumented source diff --git a/src/plugins/e-acsl/tests/special/e-acsl-compile-dlmalloc.c b/src/plugins/e-acsl/tests/special/e-acsl-compile-dlmalloc.c new file mode 100644 index 0000000000000000000000000000000000000000..89c8226676ab5212917925b305c0eeb1fde5c40f --- /dev/null +++ b/src/plugins/e-acsl/tests/special/e-acsl-compile-dlmalloc.c @@ -0,0 +1,7 @@ +/* run.config_ci, run.config_dev + COMMENT: Compile dlmalloc from sources with this file + MACRO: ROOT_EACSL_GCC_OPTS_EXT --dlmalloc-from-sources + */ +int main() { + return 0; +} \ No newline at end of file diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-compile-dlmalloc.res.oracle b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-compile-dlmalloc.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..efd026311297e55d8fefb674326118e6ece88624 --- /dev/null +++ b/src/plugins/e-acsl/tests/special/oracle_ci/e-acsl-compile-dlmalloc.res.oracle @@ -0,0 +1,2 @@ +[e-acsl] beginning translation. +[e-acsl] translation done in project "e-acsl". diff --git a/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-compile-dlmalloc.c b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-compile-dlmalloc.c new file mode 100644 index 0000000000000000000000000000000000000000..5884b0f6c6078320062404a8fcf96f5158f24dc4 --- /dev/null +++ b/src/plugins/e-acsl/tests/special/oracle_ci/gen_e-acsl-compile-dlmalloc.c @@ -0,0 +1,11 @@ +/* Generated by Frama-C */ +#include "stddef.h" +#include "stdio.h" +int main(void) +{ + int __retres; + __retres = 0; + return __retres; +} + + diff --git a/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-compile-dlmalloc.e-acsl.err.log b/src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-compile-dlmalloc.e-acsl.err.log new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391