testrun.sh

##########################################################################
#                                                                        #
#  This file is part of the Frama-C's E-ACSL plug-in.                    #
#                                                                        #
#  Copyright (C) 2012-2016                                               #
#    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 excluding an
#     extension (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
#   $4 - extra flags for e-acsl-gcc.sh
#   $5 - debug flag

set -e

TEST="$1" # Based name of the test file with extension stripped
PREFIX="$2" # Prefix (test suite) directory, e.g., bts, e-acsl-runtime
GMP="$3" # Whether to use a subsequent run with -e-acsl-gmp-only
EXTRA="$4" # Extra flags for e-acsl-gcc.sh
DEBUG="$5" # Debug flag

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

debug() {
  if [ -n "$DEBUG" ]; then
    echo "$1" 1>&2
  fi
}

# Error reporting
error() {
  echo "Error: $1" 1>&2
  debug "See $2 for details"
  exit 1
}

# Clean up log/output files unless the DEBUG flag is set
clean() {
    if [ -z "$DEBUG" ]; then
        rm -f $LOG.* $OUT.*
    fi
}

 # Do clean up on exit
trap "clean" EXIT HUP INT QUIT TERM

# 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="./scripts/e-acsl-gcc.sh
    --compile $TESTFILE --ocode=$ocode --logfile=$logfile
    --memory-model=$MODEL --oexec=$oexec $extra"

  debug "Run $EACSL_GCC"
  $EACSL_GCC || error "Command $EACSL_GCC failed" "$logfile"

  # Log outputs of the generated executables
  debug "Run and log native execution to $oexeclog.native"
  $oexec        > $oexeclog.native 2>&1
  debug "Run and log E-ACSL execution to $oexeclog.e-acsl"
  $oexec.e-acsl > $oexeclog.e-acsl 2>&1

  ## 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 "$EXTRA"
if test -n "$GMP"; then
  run_test "--gmp $EXTRA"
fi
exit 0