Commit d69cd422 authored by Basile Desloges 's avatar Basile Desloges

Merge branch 'feature/basile/eacsl-dlmalloc-from-sources' into 'master'

[eacsl] Use dlmalloc compiled from sources

See merge request frama-c/frama-c!2897
parents 5d253f1d edf83dae
...@@ -29,6 +29,9 @@ ...@@ -29,6 +29,9 @@
ifndef FRAMAC_SHARE ifndef FRAMAC_SHARE
FRAMAC_SHARE :=$(shell frama-c-config -print-share-path) FRAMAC_SHARE :=$(shell frama-c-config -print-share-path)
endif endif
ifndef FRAMAC_LIBDIR
FRAMAC_LIBDIR :=$(shell frama-c-config -print-libpath)
endif
################### ###################
# Plug-in sources # # Plug-in sources #
...@@ -289,6 +292,7 @@ EACSL_DLMALLOC_LIBNAME = libeacsl-dlmalloc.a ...@@ -289,6 +292,7 @@ EACSL_DLMALLOC_LIBNAME = libeacsl-dlmalloc.a
EACSL_DLMALLOC_LIB = $(EACSL_LIBDIR)/$(EACSL_DLMALLOC_LIBNAME) EACSL_DLMALLOC_LIB = $(EACSL_LIBDIR)/$(EACSL_DLMALLOC_LIBNAME)
EACSL_DLMALLOC_SRC = $(EACSL_DLMALLOC_DIR)/dlmalloc.c EACSL_DLMALLOC_SRC = $(EACSL_DLMALLOC_DIR)/dlmalloc.c
EACSL_DLMALLOC_OBJ = dlmalloc.o EACSL_DLMALLOC_OBJ = dlmalloc.o
# Don't forget to update "e-acsl-gcc.sh" if the flags are updated
EACSL_DLMALLOC_FLAGS = \ EACSL_DLMALLOC_FLAGS = \
-DHAVE_MORECORE=0 \ -DHAVE_MORECORE=0 \
-DHAVE_MMAP=1 \ -DHAVE_MMAP=1 \
...@@ -485,7 +489,11 @@ EACSL_INSTALL_SCRIPTS=$(addprefix $(E_ACSL_DIR)/,$(EACSL_SCRIPTS)) ...@@ -485,7 +489,11 @@ EACSL_INSTALL_SCRIPTS=$(addprefix $(E_ACSL_DIR)/,$(EACSL_SCRIPTS))
EACSL_INSTALL_MANPAGES=$(addprefix $(E_ACSL_DIR)/,$(EACSL_MANPAGES)) 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 $(PRINT_INSTALL) E-ACSL share files
for dir in $(EACSL_C_DIRECTORIES); do \ for dir in $(EACSL_C_DIRECTORIES); do \
$(MKDIR) $(FRAMAC_DATADIR)/$$dir && \ $(MKDIR) $(FRAMAC_DATADIR)/$$dir && \
...@@ -499,8 +507,10 @@ ifneq ("$(EACSL_INSTALL_MANUAL_FILES)","") ...@@ -499,8 +507,10 @@ ifneq ("$(EACSL_INSTALL_MANUAL_FILES)","")
$(CP) $(EACSL_INSTALL_MANUAL_FILES) $(FRAMAC_DATADIR)/manuals; $(CP) $(EACSL_INSTALL_MANUAL_FILES) $(FRAMAC_DATADIR)/manuals;
endif endif
$(PRINT_INSTALL) E-ACSL libraries $(PRINT_INSTALL) E-ACSL libraries
$(MKDIR) $(LIBDIR) $(MKDIR) $(EACSL_INSTALL_LIB_DIR)
$(CP) $(EACSL_LIBDIR)/libeacsl-*.a $(LIBDIR) $(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 $(PRINT_INSTALL) E-ACSL scripts
$(MKDIR) $(BINDIR) $(MKDIR) $(BINDIR)
$(CP) $(EACSL_INSTALL_SCRIPTS) $(BINDIR)/ $(CP) $(EACSL_INSTALL_SCRIPTS) $(BINDIR)/
...@@ -519,7 +529,7 @@ uninstall:: ...@@ -519,7 +529,7 @@ uninstall::
$(PRINT_RM) E-ACSL manuals $(PRINT_RM) E-ACSL manuals
$(RM) $(FRAMAC_DATADIR)/manuals/*.pdf $(RM) $(FRAMAC_DATADIR)/manuals/*.pdf
$(PRINT_RM) E-ACSL libraries $(PRINT_RM) E-ACSL libraries
$(RM) $(LIBDIR)/libeacsl-*.a $(RM) -r $(EACSL_INSTALL_LIB_DIR)
$(PRINT_RM) E-ACSL scripts $(PRINT_RM) E-ACSL scripts
$(RM) $(EACSL_INSTALLED_SCRIPTS) $(RM) $(EACSL_INSTALLED_SCRIPTS)
$(PRINT_RM) E-ACSL man pages $(PRINT_RM) E-ACSL man pages
......
...@@ -25,6 +25,9 @@ ...@@ -25,6 +25,9 @@
Plugin E-ACSL <next-release> Plugin E-ACSL <next-release>
############################ ############################
- 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) Plugin E-ACSL 22.0 (Titanium)
############################# #############################
......
...@@ -153,7 +153,7 @@ Valid arguments are: ...@@ -153,7 +153,7 @@ Valid arguments are:
\fIfloat-to-int\fP \- casts from floating-point to integer. \fIfloat-to-int\fP \- casts from floating-point to integer.
\fIdiv\fP \- division by zero. \fIdiv\fP \- division by zero.
\fIshift\fP \- left and right shifts by a value out of bounds. \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. \fIall\fP \- all of the above.
.TP .TP
.B -A, --rte-select=\fI<OPTSTRING> .B -A, --rte-select=\fI<OPTSTRING>
...@@ -212,7 +212,39 @@ launch of the \fBE-ACSL\fP plugin. ...@@ -212,7 +212,39 @@ launch of the \fBE-ACSL\fP plugin.
add \fI<OPTS>\fP to the list of options that will be given to the \fBE-ACSL\fP add \fI<OPTS>\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<OPTS>\fP analysis. Only useful when \fB--then\fP is in use, in which case \fI<OPTS>\fP
will be placed after the \fB-then\fP on \fBFrama-C\fP's command-line. Otherwise, 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<FILE>
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<FILE>
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<FILE>
use \fI<FILE>\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<FLAGS>
compile dlmalloc library with \fI<FLAGS>\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<FILE>
output compiled dlmalloc library to \fI<FILE>\fP. Unused if
\fB--dlmalloc-from-sources\fP or \fB--dlmalloc-compile-only\fP isn't used.
.SH EXIT STATUS .SH EXIT STATUS
.TP .TP
.B 0 .B 0
......
...@@ -36,13 +36,15 @@ _eacsl_gcc() { ...@@ -36,13 +36,15 @@ _eacsl_gcc() {
--no-trace --no-trace
--ocode= --oexec= --oexec-e-acsl= --ocode= --oexec= --oexec-e-acsl=
--ld-flags= --cpp-flags= --extra-cpp-args= --ld-flags= --cpp-flags= --extra-cpp-args=
--frama-c-extra= --frama-c= --gcc= --e-acsl-share= --memory-model= --frama-c-extra= --frama-c= --gcc= --ar= --ranlib=
--e-acsl-extra= --e-acsl-share= --memory-model= --e-acsl-extra=
--compile --compile-only --print-mmodels --frama-c-only --instrumented-only --compile --compile-only --print-mmodels --frama-c-only --instrumented-only
--gmp --full-mtracking --rte= --rte-select= --no-int-overflow --gmp --full-mtracking --rte= --rte-select= --no-int-overflow
--no-stdlib --frama-c-stdlib --libc-replacements --no-stdlib --frama-c-stdlib --libc-replacements
--temporal --free-valid-address --weak-validity --validate-format-strings --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 case ${prev} in
-*) -*)
......
...@@ -274,7 +274,9 @@ LONGOPTIONS="help,compile,compile-only,debug:,ocode:,oexec:,verbose:, ...@@ -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:, 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:, 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, 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" 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 # Prefix for an error message due to wrong arguments
ERROR="ERROR parsing arguments:" ERROR="ERROR parsing arguments:"
...@@ -285,6 +287,8 @@ OPTION_CPPFLAGS= # Preprocessor flags ...@@ -285,6 +287,8 @@ OPTION_CPPFLAGS= # Preprocessor flags
OPTION_LDFLAGS= # Linker flags OPTION_LDFLAGS= # Linker flags
OPTION_FRAMAC="frama-c" # Frama-C executable name OPTION_FRAMAC="frama-c" # Frama-C executable name
OPTION_CC="gcc" # GCC 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_ECHO="set -x" # Echo executed commands to STDOUT
OPTION_INSTRUMENT=1 # Perform E-ACSL instrumentation OPTION_INSTRUMENT=1 # Perform E-ACSL instrumentation
OPTION_DEBUG= # Set Frama-C debug flag OPTION_DEBUG= # Set Frama-C debug flag
...@@ -318,6 +322,11 @@ OPTION_STACK_SIZE=32 # Size of a heap shadow space (in MB) ...@@ -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_HEAP_SIZE=128 # Size of a stack shadow space (in MB)
OPTION_KEEP_GOING= # Report failing assertions but do not abort execution OPTION_KEEP_GOING= # Report failing assertions but do not abort execution
OPTION_EXTERNAL_ASSERT="" # Use custom definition of assert function 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 SUPPORTED_MMODELS="bittree,segment" # Supported memory model names
MIN_STACK=16 # Minimal size of a tracked program stack MIN_STACK=16 # Minimal size of a tracked program stack
...@@ -352,8 +361,6 @@ Notes: ...@@ -352,8 +361,6 @@ Notes:
# Base dir of this script # Base dir of this script
BASEDIR="$(realpath `dirname $0`)" BASEDIR="$(realpath `dirname $0`)"
# Directory with contrib libraries of E-ACSL
LIBDIR="$BASEDIR/../lib"
# Run getopt # Run getopt
ARGS=`getopt -n "$ERROR" -l "$LONGOPTIONS" -o "$SHORTOPTIONS" -- "$@"` ARGS=`getopt -n "$ERROR" -l "$LONGOPTIONS" -o "$SHORTOPTIONS" -- "$@"`
...@@ -643,12 +650,47 @@ do ...@@ -643,12 +650,47 @@ do
shift shift
OPTION_NO_TRACE=1 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 esac
done done
shift; shift;
# Bail if no files to translate are given # Bail if no files to translate are given and we're not trying to only compile
if [ -z "$1" ]; then # dlmalloc
if [ -z "$1" -a "$OPTION_DLMALLOC_COMPILE_ONLY" != "1" ]; then
error "no input files"; error "no input files";
fi fi
...@@ -672,6 +714,8 @@ if [ -f "$BASEDIR/../E_ACSL.mli" ]; then ...@@ -672,6 +714,8 @@ if [ -f "$BASEDIR/../E_ACSL.mli" ]; then
`test -f "$DEVELOPMENT/META.frama-c-e_acsl" -o \ `test -f "$DEVELOPMENT/META.frama-c-e_acsl" -o \
-f "$FRAMAC_PLUGIN/META.frama-c-e_acsl"; echo $?` -f "$FRAMAC_PLUGIN/META.frama-c-e_acsl"; echo $?`
EACSL_SHARE="$DEVELOPMENT/share/e-acsl" EACSL_SHARE="$DEVELOPMENT/share/e-acsl"
EACSL_LIB="$DEVELOPMENT/lib"
EACSL_CONTRIB="$DEVELOPMENT/contrib"
# Add the project directory to FRAMAC_PLUGINS, # Add the project directory to FRAMAC_PLUGINS,
# otherwise Frama-C uses an installed version # otherwise Frama-C uses an installed version
if test -f "$DEVELOPMENT/META.frama-c-e_acsl"; then if test -f "$DEVELOPMENT/META.frama-c-e_acsl"; then
...@@ -680,7 +724,9 @@ if [ -f "$BASEDIR/../E_ACSL.mli" ]; then ...@@ -680,7 +724,9 @@ if [ -f "$BASEDIR/../E_ACSL.mli" ]; then
else else
# Installed version. FRAMAC_SHARE should not be used here as Frama-C # Installed version. FRAMAC_SHARE should not be used here as Frama-C
# and E-ACSL may not be installed to the same location # 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 fi
# Architecture-dependent flags. Since by default Frama-C uses 32-bit # Architecture-dependent flags. Since by default Frama-C uses 32-bit
...@@ -761,6 +807,81 @@ fi ...@@ -761,6 +807,81 @@ fi
CPPFLAGS="$OPTION_CPPFLAGS" CPPFLAGS="$OPTION_CPPFLAGS"
LDFLAGS="$OPTION_LDFLAGS" 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 # Extra Frama-C Flags E-ACSL needs
FRAMAC_FLAGS="$FRAMAC_FLAGS \ FRAMAC_FLAGS="$FRAMAC_FLAGS \
-remove-unused-specified-functions" -remove-unused-specified-functions"
...@@ -768,7 +889,7 @@ FRAMAC_FLAGS="$FRAMAC_FLAGS \ ...@@ -768,7 +889,7 @@ FRAMAC_FLAGS="$FRAMAC_FLAGS \
# C, CPP and LD flags for compilation of E-ACSL-generated sources # C, CPP and LD flags for compilation of E-ACSL-generated sources
EACSL_CFLAGS="$OPTION_EXTERNAL_ASSERT" EACSL_CFLAGS="$OPTION_EXTERNAL_ASSERT"
EACSL_CPPFLAGS="-I$EACSL_SHARE" EACSL_CPPFLAGS="-I$EACSL_SHARE"
EACSL_LDFLAGS="$LIBDIR/libeacsl-dlmalloc.a -lgmp -lm" EACSL_LDFLAGS="$DLMALLOC_LIB_PATH -lgmp -lm"
# Output file names # Output file names
OUTPUT_CODE="$OPTION_OUTPUT_CODE" # E-ACSL instrumented source OUTPUT_CODE="$OPTION_OUTPUT_CODE" # E-ACSL instrumented source
......
/* 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
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
/* Generated by Frama-C */
#include "stddef.h"
#include "stdio.h"
int main(void)
{
int __retres;
__retres = 0;
return __retres;
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment