Merge branch 'feature/basile/eacsl-dev-test-rework' into 'master'

[eacsl] Use a custom script to launch E-ACSL dev tests

See merge request frama-c/frama-c!3419

src/plugins/e-acsl/Makefile.in

@@ -204,7 +204,8 @@ TEST_DEPENDENCIES:= \
 	$(EACSL_PLUGIN_DIR)/tests/ptests_config \
 	$(EACSL_PLUGIN_DIR)/tests/test_config \
 	$(EACSL_PLUGIN_DIR)/tests/test_config_dev \
-	$(EACSL_PLUGIN_DIR)/tests/E_ACSL_test.cmo
+	$(EACSL_PLUGIN_DIR)/tests/E_ACSL_test.cmo \
+	$(EACSL_PLUGIN_DIR)/tests/wrapper.sh
 
 ifeq ($(OCAMLBEST),opt)
 TEST_DEPENDENCIES += \
@@ -332,6 +333,7 @@ EACSL_DOC_FILES = \
 EACSL_TEST_FILES = \
 	tests/test_config_dev.in \
 	tests/test_config.in \
+	tests/wrapper.sh \
 	tests/gmp-only/test_config \
 	tests/gmp-only/test_config_dev \
 	tests/full-mtracking/test_config \
@@ -453,6 +455,7 @@ EACSL_CEA_LGPL_BARE= src/*.ml src/*/*.ml src/*.mli src/*/*.mli \
 	Makefile.in configure.ac tab-in-changelog.sh \
 	scripts/*.sh \
 	tests/E_ACSL_test.ml \
+	tests/wrapper.sh \
 	man/e-acsl-gcc.sh.1
 EACSL_CEA_LGPL=$(addprefix $(EACSL_PLUGIN_DIR)/, $(EACSL_CEA_LGPL_BARE)) \
                $(EACSL_CEA_SHARE)

src/plugins/e-acsl/headers/header_spec.txt

@@ -164,6 +164,7 @@ src/project_initializer/rtl.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/project_initializer/prepare_ast.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/project_initializer/prepare_ast.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 tests/E_ACSL_test.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+tests/wrapper.sh: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 tests/test_config.in: .ignore
 tests/test_config_dev.in: .ignore
 tests/builtin/test_config: .ignore

src/plugins/e-acsl/tests/constructs/printed_data.c

@@ -4,7 +4,7 @@
 /* run.config_dev
    COMMENT: Print the data and filter the addresses of the output so that the test is deterministic.
    MACRO: ROOT_EACSL_GCC_OPTS_EXT --assert-print-data -e -DE_ACSL_DEBUG_ASSERT -F -no-unicode
-   MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|0x[0-9a-f]*$|0x000000|g"
+   MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e s/0x[0-9a-f]*$/0x000000/g
  */
 
 #include <float.h>

src/plugins/e-acsl/tests/format/test_config_dev

 COMMENT: Remove --full-mtracking once e-acsl#118 is fixed
 MACRO: ROOT_EACSL_GCC_OPTS_EXT --validate-format-strings --full-mtracking -F -variadic-no-translation
-MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|/.*/share/e-acsl|FRAMAC_SHARE/e-acsl|"
+MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e s+/.*/share/e-acsl+FRAMAC_SHARE/e-acsl+

src/plugins/e-acsl/tests/special/e-acsl-rt-debug.c

@@ -5,7 +5,7 @@
 /* run.config_dev
   MACRO: ROOT_EACSL_GCC_OPTS_EXT --rt-debug --rt-verbose --full-mtracking
   COMMENT: Filter the addresses of the output so that the test is deterministic.
-  MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e "s|0x[0-9a-f-]*|0x0000-0000-0000|g" | @SEDCMD@ -e "s|Offset: [0-9-]*|Offset: xxxx|g"
+  MACRO: ROOT_EACSL_EXEC_FILTER @SEDCMD@ -e s_0x[0-9a-f-]*_0x0000-0000-0000_g | @SEDCMD@ -e s_Offset:\s[0-9-]*_Offset:xxxxx_g
  */
 int main() {
   return 0;

src/plugins/e-acsl/tests/special/oracle_dev/e-acsl-rt-debug.e-acsl.err.log

 >>> HEAP ---------------------
    Application: 128 MB [0x0000-0000-0000, 0x0000-0000-0000]
-   Primary    : 128 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
-   Secondary  : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
+   Primary    : 128 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+   Secondary  : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
 >>> STACK --------------------
    Application: 16 MB [0x0000-0000-0000, 0x0000-0000-0000]
-   Primary    : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
-   Secondary  : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
+   Primary    : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+   Secondary  : 16 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
 >>> GLOBAL -------------------
    Application: 0 MB [0x0000-0000-0000, 0x0000-0000-0000]
-   Primary    : 0 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
-   Secondary  : 0 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
+   Primary    : 0 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+   Secondary  : 0 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
 >>> TLS ----------------------
    Application: 64 MB [0x0000-0000-0000, 0x0000-0000-0000]
-   Primary    : 64 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
-   Secondary  : 64 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset: xxxx }
+   Primary    : 64 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
+   Secondary  : 64 MB [0x0000-0000-0000, 0x0000-0000-0000]{ Offset:xxxxx }
 >>> --------------------------

src/plugins/e-acsl/tests/test_config_dev.in

 NOFRAMAC: only the EXEC command below is useful in this config
 MACRO: SEDCMD @SEDCMD@
-MACRO: DEST @PTEST_RESULT@/@PTEST_NAME@
-MACRO: OUT @PTEST_NAME@.res.log
-MACRO: ERR @PTEST_NAME@.err.log
 MACRO: EACSL_ERR @PTEST_NAME@.e-acsl.err.log
 
-COMMENT: Define the following macro to "no" in a test to stop the execution of `e-acsl-gcc.sh`
-MACRO: ROOT_EACSL_GCC_ENABLE yes
 COMMENT: Default options for `e-acsl-gcc.sh`
 MACRO: ROOT_EACSL_GCC_MISC_OPTS -q -X --no-assert-print-data
 COMMENT: Default options for the frama-c invocation
@@ -14,7 +9,7 @@ MACRO: ROOT_EACSL_GCC_FC_EXTRA -journal-disable -verbose 0
 
 PLUGIN: E_ACSL eva,scope,variadic rtegen
 
-EXEC: LOG @EACSL_ERR@ if test "@ROOT_EACSL_GCC_ENABLE@" = "yes"; then ./scripts/e-acsl-gcc.sh -I @frama-c-exe@ -c @ROOT_EACSL_GCC_MISC_OPTS@ --frama-c-extra="@PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@ @ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" @ROOT_EACSL_GCC_OPTS_EXT@ -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl 2>&1 1>/dev/null | @ROOT_EACSL_EXEC_FILTER@ > @PTEST_RESULT@/@EACSL_ERR@; fi
+EXEC: LOG @EACSL_ERR@ ./tests/wrapper.sh "@frama-c-exe@" "@PTEST_RESULT@" "@PTEST_NAME@" "@PTEST_FILE@" "@EACSL_ERR@" "@ROOT_EACSL_GCC_MISC_OPTS@ @ROOT_EACSL_GCC_OPTS_EXT@" "@PTEST_DEFAULT_OPTIONS@ @PTEST_LOAD_OPTIONS@ @ROOT_EACSL_GCC_FC_EXTRA@ @ROOT_EACSL_GCC_FC_EXTRA_EXT@" "@ROOT_EACSL_EXEC_FILTER@"
 
 COMMENT: These next macros can be redefined in a test file
 COMMENT: Define the following macro in a test to pass extra options to the frama-c invocation
@@ -22,4 +17,6 @@ MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT
 COMMENT: Define the following macro in a test to pass extra options to `e-acsl-gcc.sh`
 MACRO: ROOT_EACSL_GCC_OPTS_EXT
 COMMENT: Define the following macro in a test to filter the output of the test execution
+COMMENT: You can chain several filters by separating commands with |. However sed cannot
+COMMENT: use | as a delimiter, please use / or another character instead.
 MACRO: ROOT_EACSL_EXEC_FILTER cat

src/plugins/e-acsl/tests/wrapper.sh

+#!/bin/bash
+##########################################################################
+#                                                                        #
+#  This file is part of the Frama-C's E-ACSL plug-in.                    #
+#                                                                        #
+#  Copyright (C) 2012-2020                                               #
+#    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 licenses/LGPLv2.1).            #
+#                                                                        #
+##########################################################################
+
+# Wrapper script to compile a test file and execute the resulting binary
+
+# Base dir of this script
+BASEDIR="$(realpath `dirname $0`)"
+
+help() {
+  printf "wrapper.sh - run e-acsl-gcc.sh and the resulting binary to test E-ACSL
+Usage: $0 framac_exe result_dir test_name test_file output_name opts fc_opts filter_cmd
+Args:
+  framac_exe    @frama-c-exe@ in test_config
+  result_dir    @PTEST_RESULT@ in test_config
+  test_name     @PTEST_NAME@ in test_config
+  test_file     @PTEST_FILE@ in test_config
+  output_name   Output file given to LOG in test_config
+  opts          Options for e-acsl-gcc.sh
+  fc_opts       Options for Frama-C
+  filter_cmd    Command to filter the output of the resulting binary
+" >&2
+  exit 1
+}
+
+if [[ $# -ne 8 ]]; then
+  printf "Error: wrong number of arguments: 8 expected, got $#\n\n" >&2
+  help
+fi
+
+# Name the arguments of the script
+framac_exe=$1
+result_dir=$2
+test_name=$3
+test_file=$4
+output_name=$5
+opts=$6
+fc_opts=$7
+filter_cmd=$8
+
+# Derive output logs from the arguments
+out_log=$result_dir/$test_name.res.log
+err_log=$result_dir/$test_name.err.log
+exec_out_log=$result_dir/$test_name.exec_out.log
+exec_err_log=$result_dir/$test_name.exec_err.log
+output_log=$result_dir/$output_name
+
+# Compile the test file
+$BASEDIR/../scripts/e-acsl-gcc.sh -I $framac_exe \
+  -c $opts \
+  --frama-c-extra="$fc_opts" \
+  -o $result_dir/$test_name.gcc.c \
+  -O $result_dir/$test_name \
+  $test_file \
+  1>$out_log \
+  2>$err_log
+
+# Check compilation return code and exit script in case of error
+if [[ $? -ne 0 ]]; then
+  error_code=$?
+  printf "Error while executing e-acsl-gcc.sh\n" > $output_log
+  printf "\nSTDOUT:\n" >> $output_log
+  cat $out_log >> $output_log
+  printf "\nSTDERR:\n" >> $output_log
+  cat $err_log >> $output_log
+  exit $error_code
+fi
+
+# Execute the compiled test file
+$result_dir/$test_name.e-acsl 1>$exec_out_log 2>$exec_err_log
+
+# Check execution return code and exit script in case of error
+if [[ $? -ne 0 ]]; then
+  error_code=$?
+  printf "Error while executing $result_dir/$test_name.e-acsl\n" > $output_log
+  printf "\nSTDOUT:\n" >> $output_log
+  cat $exec_out_log >> $output_log
+  printf "\nSTDERR:\n" >> $output_log
+  cat $exec_err_log >> $output_log
+  exit $error_code
+fi
+
+# No error while executing the script, filter stderr before saving it to the
+# output log
+
+## Create temporary files
+tmp_filter_input=$(mktemp) || (printf "unable to create temp file\n" > $output_log && exit 1)
+tmp_filter_output=$(mktemp) || (printf "unable to create temp file\n" > $output_log && exit 1)
+cp $exec_err_log $tmp_filter_input
+
+## Split the filter command on character | to extract the subcommands and apply
+## the filters one at a time
+IFS='|' read -ra filters <<< "$filter_cmd"
+for filter in "${filters[@]}"; do
+  cat $tmp_filter_input | $filter > $tmp_filter_output
+  if [[ $? -ne 0 ]]; then
+    error_code=$?
+    printf "Error while filtering output with command '$filter'\n" > $output_log
+    printf "\nFILTER INPUT:\n" >> $output_log
+    cat $tmp_filter_input >> $output_log
+    printf "\nFILTER OUTPUT:\n" >> $output_log
+    cat $tmp_filter_output >> $output_log
+    exit $error_code
+  fi
+  cp $tmp_filter_output $tmp_filter_input
+done
+
+## Filtering done, copy output to the output log and remove temporary files
+cp $tmp_filter_output $output_log
+rm $tmp_filter_input
+rm $tmp_filter_output
+
+exit 0