From 7a408d9bedfd0082e1430f057fc8bd979b5abee8 Mon Sep 17 00:00:00 2001
From: Kostyantyn Vorobyov <kostyantyn.vorobyov@cea.fr>
Date: Wed, 3 Feb 2016 18:04:33 +0100
Subject: [PATCH] Brought forward changes from the segment-model remote: -
structural changes to e-acsl wrapper script - --memory-model option in
the e-acsl wrapper script that allows switching between different
memory models - added script to facilitate runs of e-acsl during
testing (scripts/testrun.sh)
---
src/plugins/e-acsl/scripts/e-acsl-gcc.sh | 168 +++++++++++++++++------
src/plugins/e-acsl/scripts/testrun.sh | 97 +++++++++++++
2 files changed, 226 insertions(+), 39 deletions(-)
create mode 100755 src/plugins/e-acsl/scripts/testrun.sh
diff --git a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
index dae2bc058f4..24ef7b8816d 100755
--- a/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+++ b/src/plugins/e-acsl/scripts/e-acsl-gcc.sh
@@ -46,18 +46,25 @@ check_tool() {
# Getopt options
LONGOPTIONS="help,compile,compile-only,print,debug:,ocode:,oexec:,verbose:, \
- frama-c-only,extra-cpp-args,rtl,frama-c-stdlib,full-mmodel,gmp,quiet,logfile:,
- ld-flags:,cpp-flags:,frama-c-extra:"
-SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,R,L,M,l:,e:,g,q,s:,F:"
+ frama-c-only,extra-cpp-args:,frama-c-stdlib,full-mmodel,gmp,quiet,logfile:,
+ ld-flags:,cpp-flags:,frama-c-extra:,memory-model:,production,no-stdlib,
+ debug-log:"
+SHORTOPTIONS="h,c,C,p,d:,o:,O:,v:,f,E:,L,M,l:,e:,g,q,s:,F:,m:,P,N,D:"
# Prefix for an error message due to wrong arguments
ERROR="ERROR parsing arguments:"
+# Frama-C
+FRAMAC="`check_tool 'frama-c'`"
+FRAMAC_CONGIG="`check_tool 'frama-c-config'`"
+FRAMAC_FLAGS=""
+FRAMA_C_SHARE="`$FRAMAC_CONGIG -print-share-path`"
+
# Architecture-dependent flags. Since by default Frama-C uses 32-bit
# architecture we need to make sure that same architecture is used for
# instrumentation and for compilation.
MACHDEPFLAGS="`getconf LONG_BIT`"
# Check if getconf gives out the value accepted by Frama-C/GCC
-echo "$MACHDEPFLAGS" | grep '16\|32\|64' \
+echo "$MACHDEPFLAGS" | grep '16\|32\|64' 2>&1 >/dev/null \
|| error "$MACHDEPFLAGS-bit architecture not supported"
# -machdep option sent to frama-c
MACHDEP="-machdep gcc_x86_$MACHDEPFLAGS"
@@ -66,39 +73,58 @@ CPPMACHDEP="-D__FC_MACHDEP_X86_$MACHDEPFLAGS"
# GCC machine option
GCCMACHDEP="-m$MACHDEPFLAGS"
+# Macro that identifies E-ACSL compilation. Passed to Framac and GCC runs
+# but not to the original compilation
+EACSL_MACRO_ID="__E_ACSL__"
+
# Gcc
CC="`check_tool 'gcc'`"
CFLAGS="-std=c99 $GCCMACHDEP -g3 -O2 -pedantic -fno-builtin -Wall \
-Wno-long-long \
-Wno-attributes \
+ -Wno-unused \
+ -Wno-unused-function \
-Wno-unused-result \
-Wno-unused-value \
-Wno-unused-function \
-Wno-unused-variable \
-Wno-unused-but-set-variable \
- -Wno-implicit-function-declaration \
- -Wno-attributes"
+ -Wno-implicit-function-declaration"
CPPFLAGS=""
LDFLAGS=""
-# Frama-C
-FRAMAC="`check_tool 'frama-c'`"
-FRAMAC_CONGIG="`check_tool 'frama-c-config'`"
-FRAMAC_FLAGS="-implicit-function-declaration ignore"
# E-ACSL source that needed for compilation
-FRAMA_C_SHARE="`$FRAMAC_CONGIG -print-share-path`"
EACSL_SHARE="$FRAMA_C_SHARE/e-acsl"
-RTL="$EACSL_SHARE/e_acsl.c \
- $EACSL_SHARE/memory_model/e_acsl_mmodel.c \
- $EACSL_SHARE/memory_model/e_acsl_bittree.c \
+RTL_BITTREE="\
+ $EACSL_SHARE/e_acsl.c \
+ $EACSL_SHARE/memory_model/e_acsl_mmodel.c \
+ $EACSL_SHARE/memory_model/e_acsl_bittree.c \
+"
+RTL_SPLAYTREE="\
+ $EACSL_SHARE/e_acsl.c \
+ $EACSL_SHARE/memory_model/e_acsl_splay_tree.c \
+ $EACSL_SHARE/memory_model/e_acsl_mmodel.c \
+"
+RTL_TREE="\
+ $EACSL_SHARE/e_acsl.c \
+ $EACSL_SHARE/memory_model/e_acsl_tree.c \
+ $EACSL_SHARE/memory_model/e_acsl_mmodel.c \
+"
+RTL_LIST="\
+ $EACSL_SHARE/e_acsl.c \
+ $EACSL_SHARE/memory_model/e_acsl_list.c \
+ $EACSL_SHARE/memory_model/e_acsl_mmodel.c \
"
-# CPP and LD flags for compilation of E-ACSL-generated sources
-EACSL_CPP_FLAGS="
- -D__FC_errno=(*__errno_location())
- -D__builtin_printf=printf
- -D__builtin_memcpy=memcpy"
-EACSL_LD_FLAGS="-lgmp -lm"
+RTL="$RTL_BITTREE"
+
+# C, CPP and LD flags for compilation of E-ACSL-generated sources
+EACSL_CFLAGS=""
+EACSL_CPPFLAGS="
+ -I$EACSL_SHARE
+ -D$EACSL_MACRO_ID
+ -D__FC_errno=(*__errno_location())"
+EACSL_LDFLAGS="-lgmp -lm"
# Variables holding getopt options
OPTION_FRAMAC_EXTRA= # Extra Frama-C options
@@ -114,7 +140,14 @@ OPTION_EACSL="-e-acsl -then-last" # Specifies E-ACSL run
OPTION_FRAMA_STDLIB="-no-frama-c-stdlib" # Use Frama-C stdlib
OPTION_FULL_MMODEL= # Instrument as much as possible
OPTION_GMP= # Use GMP integers everywhere
-OPTION_EXTRA_CPP="-I$FRAMA_C_SHARE/libc $CPPMACHDEP" # Extra CPP flags
+OPTION_DEBUG_MACRO="-DE_ACSL_DEBUG" # Debug macro
+OPTION_DEBUG_LOG_MACRO="" # Specification of debug log file
+# The following option controls whether to use gcc builtins
+# (e.g., __builtin_strlen) in RTL or fall back to custom implementations
+# of standard functions.
+OPTION_BUILTINS="-DE_ACSL_BUILTINS"
+# Extra CPP flags for frama-c
+OPTION_EXTRA_CPP="-D$EACSL_MACRO_ID -I$FRAMA_C_SHARE/libc $CPPMACHDEP"
manpage() {
echo "NAME"
@@ -134,38 +167,56 @@ manpage() {
echo " compile input files as if they were generated by E-ACSL"
echo " -p, --print"
echo " output the code generated by E-ACSL to STDOUT"
- echo " -d, --debug <N>"
+ echo " -d, --debug=<N>"
echo " pass a value to Frama-C -debug option"
- echo " -o, --ocode <FILENAME>"
+ echo " -o, --ocode=<FILENAME>"
echo " name of the output source file, defaults to a.out.frama.c"
- echo " -O, --oexec <FILENAME>"
+ echo " -O, --oexec=<FILENAME>"
echo " name of the executable generated from the un-instrumented code."
echo " Executable compiled from the E-ACSL instrumented sources is"
echo " appended .e.acsl suffix. Defaults to a.out and a.out.e-acsl"
- echo " -v, --verbose <N>"
+ echo " -v, --verbose=<N>"
echo " pass a value to Frama-C -verbose option"
echo " -f, --frama-c-only"
echo " run input source files through Frama-C without E-ACSL"
- echo " -E, --extra-cpp-args <FLAGS>"
+ echo " -E, --extra-cpp-args=<FLAGS>"
echo " pass additional arguments to the Frama-C pre-processor"
- echo " -R, --rtl"
- echo " output E_ACSL runtime libraries to STDOUT"
echo " -L, --frama-c-stdlib"
echo " use Frama-C standard library"
echo " -M, --full-mmodel"
echo " maximise memory-related instrumentation"
echo " -g, --gmp"
echo " always use GMP integers instead of C integral types"
- echo " -l, --ld-flags <FLAGS>"
+ echo " -l, --ld-flags=<FLAGS>"
echo " pass the specified flags to the linker"
- echo " -e, --cpp-flags <FLAGS>"
+ echo " -e, --cpp-flags=<FLAGS>"
echo " pass the specified flags to the pre-processor (compile-time)"
echo " -q, --quiet"
echo " suppress any output except for errors and warnings"
- echo " -s, --logfile <FILE>"
+ echo " -s, --logfile=<FILE>"
echo " redirect all output to a given log file"
echo " -F, --frama-c-extra <OPTION>"
echo " pass an extra option to frama-c invocation"
+ echo " -m, --memory-model=<bittree|tree|list|splaytree>"
+ echo " memory model (i.e., runtime library) to be used at compile time."
+ echo " Valid arguments are:"
+ echo " bittree - memory modelling using a Patricie trie ADT"
+ echo " splaytree - memory modelling using a splay tree ADT"
+ echo " list - memory modelling using a linked-list ADT"
+ echo " tree - memory modelling using a binary tree ADT"
+ echo " -P, --production"
+ echo " Compile optimized executatle without debug features"
+ echo " -N, --no-stdlib"
+ echo " If specified the E-ACSL run-time library uses custom "
+ echo " implementations of standard library functions (such as memset)."
+ echo " By default GCC builtins are used (e.g., __builtin_memset)."
+ echo " -D, --debug-log=<FILE>"
+ echo " Specify the name of the file for logging of debugging output of"
+ echo " modified modified executables. If '-' is specified then the"
+ echo " output is redirected to the standard error stream. By default "
+ echo " /tmp/e-acsl.log file is used. Note that this option is meaningful"
+ echo " in the absence of the -P flag, which diables debug logging for "
+ echo " performance reasons."
echo ""
echo "EXAMPLES:"
echo " # Instrument foo.c and output the instrumented code to a.out.frama.c"
@@ -275,7 +326,7 @@ do
# Additional CPP arguments
--extra-cpp-args|-E)
shift;
- OPTION_EXTRA_CPP="$OPTION_EXTRA_CPP$1"
+ OPTION_EXTRA_CPP="$OPTION_EXTRA_CPP $1"
shift;
;;
# Additional flags passed to the linker
@@ -303,11 +354,6 @@ do
shift;
OPTION_EACSL=
;;
- # Output the RTL files
- --rtl|-R)
- echo $RTL
- exit 0;
- ;;
# Do use Frama-C stdlib, which is the default behaviour of Frama-C
--frama-c-stdlib|-L)
shift;
@@ -323,6 +369,41 @@ do
shift;
OPTION_GMP="-e-acsl-gmp-only"
;;
+ -P|--production)
+ shift;
+ OPTION_DEBUG_MACRO=""
+ ;;
+ -N|--no-stdlib)
+ shift;
+ OPTION_BUILTINS=""
+ ;;
+ -D|--debug-log)
+ shift;
+ OPTION_DEBUG_LOG_MACRO="-DE_ACSL_DEBUG_LOG=$1"
+ shift;
+ ;;
+ -m|--memory-model)
+ shift;
+ mmodel="$1"
+ shift;
+ case $mmodel in
+ bittree)
+ RTL="$RTL_BITTREE"
+ ;;
+ splaytree)
+ RTL="$RTL_SPLAYTREE"
+ ;;
+ tree)
+ RTL="$RTL_TREE"
+ ;;
+ list)
+ RTL="$RTL_LIST"
+ ;;
+ *)
+ error "Unknown model memory model: '$mmodel'"
+ ;;
+ esac
+ ;;
esac
done
shift;
@@ -368,8 +449,17 @@ if test -n "$OPTION_COMPILE" ; then
OPTION_OCODE="$@"
fi
# Compile and link E-ACSL-instrumented file
- ($OPTION_ECHO; $CC $CPPFLAGS $CFLAGS $EACSL_CPP_FLAGS $RTL \
- "$OPTION_OCODE" -o "$OPTION_OEXEC.e-acsl" $LDFLAGS $EACSL_LD_FLAGS)
+ ($OPTION_ECHO; \
+ $CC \
+ $CFLAGS $CPPFLAGS \
+ $EACSL_CFLAGS $EACSL_CPPFLAGS \
+ $RTL \
+ $OPTION_DEBUG_MACRO \
+ $OPTION_DEBUG_LOG_MACRO \
+ $OPTION_BUILTINS \
+ -o "$OPTION_OEXEC.e-acsl" \
+ "$OPTION_OCODE" \
+ $LDFLAGS $EACSL_LDFLAGS)
error "fail to compile/link instrumented code: $@" $?;
fi
exit 0;
diff --git a/src/plugins/e-acsl/scripts/testrun.sh b/src/plugins/e-acsl/scripts/testrun.sh
new file mode 100755
index 00000000000..3bcfe997c86
--- /dev/null
+++ b/src/plugins/e-acsl/scripts/testrun.sh
@@ -0,0 +1,97 @@
+##########################################################################
+# #
+# This file is part of the Frama-C's E-ACSL plug-in. #
+# #
+# Copyright (C) 2012-2015 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It 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 Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file license/LGPLv2.1). #
+# #
+##########################################################################
+
+#!/bin/sh -e
+
+# Convenience script for running tests with E-ACSL. Given a source file the
+# sequence is as follows:
+# 1. Perform E-ACSL instrumentation
+# 2. Compile instrumented and original files
+# 3. Compare outputs of the above
+
+# Arguments:
+# $1 - base name of the source file to use (e.g., addrOf)
+# $2 - base name of the test suite directory the test file is located in.
+# (for instance e-acsl-runtime). Provided that ROOT is the directory
+# holding the E-ACSL repository there should be either:
+# $ROOT/test/e-acsl-runtime/addrOf.i or
+# $ROOT/test/e-acsl-runtime/addrOf.c
+# $3 - if specified this script re-runs test sequence generating using
+# -e-acsl-gmp-only option
+
+PREFIX="$1" # Prefix (test suite) directory, e.g., bts, e-acsl-runtime
+TEST="$2" # Based name of the test file with extension stripped
+GMP="$3" # Whether to use a subsequent run with -e-acsl-gmp-only
+
+ROOTDIR="`readlink -f $(dirname $0)/../`" # Root directory of the repository
+TESTDIR="$ROOTDIR/tests/$PREFIX"
+RESDIR=$TESTDIR/result # result directory within the test suite
+TESTFILE=`ls $TESTDIR/$TEST.[ic]` # Source test file
+MODEL="bittree" # Memory model to link against.
+
+LOG="$RESDIR/$TEST.testrun" # Base name for log files
+OUT="$RESDIR/gen_$TEST" # Base name for output
+RUNS=1
+
+# Remove all old logs and executables before running new tests
+rm -f $LOG.* $OUT.*
+
+# Error reporting
+error() {
+ echo "Error: $1" 1>&2
+ echo "See $2 for details" 1>&2
+ exit 1
+}
+
+# Instrument the given test using e-acsl-gcc.sh and compare outputs of the
+# executables generated from instrumented and non-instrumented sources
+run_test() {
+ local ocode=$OUT.$RUNS.c # Generated source file
+ local logfile=$LOG.$RUNS.elog # Log file for e-acsl-gcc.sh output
+ local oexec=$OUT.$RUNS.out # Generated executable name
+ local oexeclog=$LOG.$RUNS.rlog # Log for executable output
+ local extra="$1" # Additional arguments to e-acsl-gcc.sh
+
+ # Command for instrumenting the source file and compiling the original
+ # and the instrumented code
+ EACSL_GCC="e-acsl-gcc.sh
+ --compile $TESTFILE --ocode=$ocode --logfile=$logfile
+ --memory-model=$MODEL --oexec=$oexec $extra"
+
+ $EACSL_GCC || error "Command $EACSL_GCC failed" "$logfile"
+
+ # Log outputs of the generated executables
+ $oexec 2>&1 > $oexeclog.native
+ $oexec.e-acsl 2>&1 > $oexeclog.e-acsl
+
+ ## Make sure that instrumented and uninstrumented programs have same outputs
+ diff $oexeclog.native $oexeclog.e-acsl ||
+ error "Output of programs before and after instrumentation differ" \
+ "output of $oexec and $oexec.e-acsl"
+
+ RUNS=$((RUNS+1))
+}
+
+run_test
+if test -n "$GMP"; then
+ run_test "--gmp"
+fi
--
GitLab