From 9f5931a15a1c34700b51f4c14746a5c8b0dbe6cc Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Thu, 21 Oct 2021 19:04:36 +0200
Subject: [PATCH] [eacsl] Use a custom script to launch E-ACSL dev tests
---
src/plugins/e-acsl/Makefile.in | 5 +-
src/plugins/e-acsl/headers/header_spec.txt | 1 +
.../e-acsl/tests/format/test_config_dev | 2 +-
src/plugins/e-acsl/tests/test_config_dev.in | 9 +-
src/plugins/e-acsl/tests/wrapper.sh | 132 ++++++++++++++++++
5 files changed, 141 insertions(+), 8 deletions(-)
create mode 100755 src/plugins/e-acsl/tests/wrapper.sh
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 93fe3e1be9e..c80d95a5803 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/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)
diff --git a/src/plugins/e-acsl/headers/header_spec.txt b/src/plugins/e-acsl/headers/header_spec.txt
index 77c47d3113a..c260e31129e 100644
--- a/src/plugins/e-acsl/headers/header_spec.txt
+++ b/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
diff --git a/src/plugins/e-acsl/tests/format/test_config_dev b/src/plugins/e-acsl/tests/format/test_config_dev
index dd9937641ad..e561c38846b 100644
--- a/src/plugins/e-acsl/tests/format/test_config_dev
+++ b/src/plugins/e-acsl/tests/format/test_config_dev
@@ -1,3 +1,3 @@
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+
diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in
index a4b467001b8..eefa60c7fb9 100644
--- a/src/plugins/e-acsl/tests/test_config_dev.in
+++ b/src/plugins/e-acsl/tests/test_config_dev.in
@@ -1,12 +1,7 @@
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
diff --git a/src/plugins/e-acsl/tests/wrapper.sh b/src/plugins/e-acsl/tests/wrapper.sh
new file mode 100755
index 00000000000..a2862ed67aa
--- /dev/null
+++ b/src/plugins/e-acsl/tests/wrapper.sh
@@ -0,0 +1,132 @@
+#!/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
--
GitLab