[analysis-scripts] improve and generalize creduce.sh

Makefile

@@ -276,6 +276,8 @@ DISTRIB_FILES:=\
       share/analysis-scripts/prologue.mk                                \
       share/analysis-scripts/README.md                                  \
       share/analysis-scripts/results_display.py                         \
+      share/analysis-scripts/script_for_creduce_fatal.sh                \
+      share/analysis-scripts/script_for_creduce_non_fatal.sh            \
       share/analysis-scripts/summary.py                                 \
       share/analysis-scripts/template.mk                                \
       $(wildcard share/emacs/*.el) share/autocomplete_frama-c           \
@@ -1943,6 +1945,8 @@ install:: install-lib-$(OCAMLBEST)
 	  share/analysis-scripts/prologue.mk \
 	  share/analysis-scripts/README.md \
 	  share/analysis-scripts/results_display.py \
+	  share/analysis-scripts/script_for_creduce_fatal.sh \
+	  share/analysis-scripts/script_for_creduce_non_fatal.sh \
 	  share/analysis-scripts/summary.py \
 	  share/analysis-scripts/template.mk \
 	  $(FRAMAC_DATADIR)/analysis-scripts

headers/header_spec.txt

@@ -134,6 +134,8 @@ share/analysis-scripts/parse-coverage.sh: .ignore
 share/analysis-scripts/prologue.mk: CEA_LGPL
 share/analysis-scripts/README.md: .ignore
 share/analysis-scripts/results_display.py: CEA_LGPL
+share/analysis-scripts/script_for_creduce_fatal.sh: .ignore
+share/analysis-scripts/script_for_creduce_non_fatal.sh: .ignore
 share/analysis-scripts/summary.py: CEA_LGPL
 share/analysis-scripts/template.mk: .ignore
 share/compliance/c11_functions.json: .ignore

share/analysis-scripts/creduce.sh

@@ -21,52 +21,71 @@
 #                                                                        #
 ##########################################################################
 
-# Script to run C-Reduce (https://embed.cs.utah.edu/creduce) when debugging
-# Frama-C crashes with a 'fatal' error, which produces a stack trace and
-# a message "Please report".
-
-### Requirements
-#
-# - C-Reduce installed in the PATH, or its path given in the
-#   environment variable CREDUCE;
-#
-# - GCC, or the path to a compiler with compatible options given in the
-#   environment variable CC;
-#
-# - Frama-C installed in the PATH, or its path given in the environment
-#   variable FRAMAC;
-#
-# - a source file + a command line which causes Frama-C to crash with
-#   a 'fatal' error (producing a stack trace).
-
-### How it works
-#
-#   creduce.sh <file.c> <command line options>
-#
-# This script creates a temporary directory named 'creducing'.
-# It copies <file.c> inside it, then runs creduce.
-# creduce runs "frama-c <command line options>" on the copied file,
-# modifying it to make it smaller while still crashing.
-#
-# When done, copy the reduced file and erase directoy 'creducing'.
+usage="
+Script to run C-Reduce (https://embed.cs.utah.edu/creduce) when debugging
+Frama-C, or when minimizing test cases resulting in a Frama-C error.
+
+# Requirements
+
+- C-Reduce installed in the PATH, or its path in environment variable CREDUCE;
+- Frama-C installed in the PATH, or the path to its 'bin' directory in
+   environment variable FRAMAC_BIN;
+- a source file + a command line which causes Frama-C to crash with
+  a 'fatal' error (producing a stack trace); can also be used when
+  Frama-C reports other errors, but in this case a separate script must be
+  completed by the user.
+
+# Basic usage
+
+  arguments: <file> <command line options>
+
+This script creates a temporary directory named 'creducing'. It copies <file>
+inside it, then runs creduce with 'frama-c <command line options>'
+on the copied file, modifying it to make it smaller while still crashing.
+
+When done, you need to copy the reduced file and erase directoy 'creducing'.
+
+# Advanced usage
+
+- if <file> is not a preprocessed (.i) source, this script
+  will retrieve the preprocessing arguments from Frama-C. It will try to
+  preprocess the file in GCC to make sure it is parseable during reduction.
+  This may cause some issues; use a preprocessed file if you can.
+
+- For "fatal" crashes (with stack trace and 'Please report...' message),
+  this script should work automatically. For other crashes (e.g. invalid
+  input), this script will copy a template to the current directory and you
+  need to fill it so that creduce will work. This usage mode requires knowing
+  how C-Reduce works.
+"
 
 if [ $# -lt 1 ]; then
-    echo "usage: $0 file.c [Frama-C options that cause a crash]"
+    echo "$usage"
     exit 1
 fi
 
+case "$1" in
+    --help) echo "$usage"; exit;;
+    --h) echo "$usage"; exit;;
+    -help) echo "$usage"; exit;;
+    -h) echo "$usage"; exit;;
+esac
+
 file="$1"
 base=$(basename "$file")
 shift
-options="$@"
+fcflags="$@"
 dir_for_reduction="creducing"
 
+script_for_creduce="./script_for_creduce.sh"
+
 if [ -z "$CREDUCE" ]; then
     CREDUCE="creduce"
 fi
 
 if ! command -v "$CREDUCE" 2>&1 >/dev/null; then
-    echo "creduce not found, put it in PATH or in environment variable CREDUCE."
+    echo "creduce not found; install it in the PATH or"
+    echo "put it in environment variable CREDUCE."
     exit 1
 fi
 
@@ -75,12 +94,28 @@ if [[ ! -f "$file" ]]; then
     exit 1
 fi
 
-if [[ $(dirname "$file") -eq "$dir_for_reduction" ]]; then
+if [[ $(dirname "$file") = "$dir_for_reduction" ]]; then
     echo "error: cannot reduce a file inside the directory used for reduction,"
     echo "       $dir_for_reduction"
     exit 1
 fi
 
+if [ -z "$FRAMAC_BIN" ]; then
+    if ! command -v "frama-c" >/dev/null; then
+        echo "error: frama-c must be in the PATH, or FRAMAC_BIN must point to"
+        echo "       the directory containing the frama-c binary"
+        exit 1
+    fi
+    FRAMAC="frama-c"
+else
+    FRAMAC="$FRAMAC_BIN/frama-c"
+fi
+echo "[info] using FRAMAC: $FRAMAC"
+
+if [ -z "$FRAMAC_SHARE" ]; then
+    FRAMAC_SHARE="$("$FRAMAC" -print-share-path)"
+fi
+
 if [[ ! "$options" =~ no-autoload-plugins ]]; then
     echo "********************************************************************"
     echo "Hint: consider using -no-autoload-plugins -load-module [modules]"
@@ -93,69 +128,97 @@ if [[ "$base" =~ \.c$ ]]; then
     echo "Hint: consider passing a preprocessed (.i) file if possible,"
     echo "      otherwise #includes may prevent further reduction"
     echo "********************************************************************"
+    # TODO: check for libc includes and suggest -print-libc
 fi
 
-mkdir -p "$dir_for_reduction"
-
-if [ -z "$FRAMAC" ]; then
-    SCRIPT_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )"
-    FRAMAC=$(realpath "$SCRIPT_DIR/../../bin/frama-c")
-    echo "[info] FRAMAC not set, using binary at: $FRAMAC"
+# Obtain cpp flags by running Frama-C with `-kernel-msg-key pp`
+if [[ "$base" =~ \.i$ ]]; then
+    # Preprocessed file: no need to get preprocessing flags
+    # TODO: check for '-machdep' option and add/remove flags accordingly
+    CPP="gcc -fsyntax-only"
 else
-    echo "[info] using FRAMAC: $FRAMAC"
+    CPP=$("$FRAMAC" -kernel-msg-key pp $fcflags "$file" 2>/dev/null | \
+          grep "preprocessing with " | \
+          sed 's|.* preprocessing with "||' | sed 's|"$||')
+    if [[ "$CPP" = "" ]]; then
+        echo "[info] Could not get preprocessing flags when running Frama-C,"
+        echo "       using default flags"
+        # TODO: check for '-machdep' option and add/remove flags accordingly
+        CPP="gcc -fsyntax-only -m32"
+    else
+        # Replace -E with -fsyntax-only to force GCC to try parsing the file;
+        # also remove Frama-C's libc; use the standard system libraries.
+        CPP=$(echo $CPP | \
+                  sed 's| -E | -fsyntax-only |' | \
+                  sed 's| -nostdinc | |' | \
+                  sed 's| -I[^ ]\+/libc | |' )
+    fi
 fi
 
-if [ -z "$FRAMAC_SHARE" ]; then
-    FRAMAC_SHARE="$("$FRAMAC" -print-share-path)"
+if [ ! -e "$script_for_creduce" ]; then
+    echo "[info] $script_for_creduce not found."
+    echo "Which kind of error are you reducing for?"
+    echo "1. Fatal crash (error message with stacktrace)"
+    echo "2. Non-fatal error"
+    read -p "Please enter 1 or 2: " errorkind
+    case $errorkind in
+        1)
+            cp "$FRAMAC_SHARE/analysis-scripts/script_for_creduce_fatal.sh" "$script_for_creduce"
+            ;;
+        2)
+            cp "$FRAMAC_SHARE/analysis-scripts/script_for_creduce_non_fatal.sh" "$script_for_creduce"
+            echo "Script copied. Please edit $script_for_creduce and re-run this script."
+            exit 0
+            ;;
+        *)
+            echo "Invalid choice, aborting."
+            exit 0
+            ;;
+    esac
 fi
 
-if [ -z "$CC" ]; then
-    CC=gcc
-    CFLAGS+="-fsyntax-only -I\"$FRAMAC_SHARE\"/libc -D__FC_MACHDEP_X86_32 -m32"
-fi
-
-echo "[info] checking syntactic validity with: $CC $CFLAGS"
+echo "[info] the following command will be used to check for syntactic validity during reduction:"
+echo "    $CPP"
 
+mkdir -p "$dir_for_reduction"
 cp "$file" "$dir_for_reduction"
+cp "$script_for_creduce" "$dir_for_reduction"
 cd "$dir_for_reduction"
 
-cat <<EOF > script_for_creduce.sh
-#!/bin/bash -e
-
-# This script is given to creduce to reduce a Frama-C crashing test case
-# (where "crashing" means a 'fatal' exception, with stack trace).
-
-set +e
-$CC $CFLAGS "$base"
-if [ \$? -ne 0 ]; then
-   exit 1
-fi
-"$FRAMAC" "$base" $options
-retcode=\$?
-# see cmdline.ml for the different exit codes returned by Frama-C
-if [ \$retcode -eq 125 -o \$retcode -eq 4 ]; then
-    exit 0
-else
-    exit 1
-fi
-set -e
-
-EOF
-
-chmod u+x script_for_creduce.sh
+# we avoid using '-i' for compatibility with macOS sed
+sed -e "s|@CPP@|$CPP|g" "$script_for_creduce" > "${script_for_creduce}.tmp"
+mv "${script_for_creduce}.tmp" "$script_for_creduce"
+sed -e "s|@FRAMAC@|$FRAMAC|g" "$script_for_creduce" > "${script_for_creduce}.tmp"
+mv "${script_for_creduce}.tmp" "$script_for_creduce"
+sed -e "s|@BASE@|$base|g" "$script_for_creduce" > "${script_for_creduce}.tmp"
+mv "${script_for_creduce}.tmp" "$script_for_creduce"
+sed -e "s|@FCFLAGS@|$fcflags|g" "$script_for_creduce" > "${script_for_creduce}.tmp"
+mv "${script_for_creduce}.tmp" "$script_for_creduce"
+chmod u+x "$script_for_creduce"
 
 trap "{ echo \"Creduce interrupted!\"; echo \"\"; echo \"(partially) reduced file: $dir_for_reduction/$base\"; exit 0; }" SIGINT
 
 echo "File being reduced: $dir_for_reduction/$base (press Ctrl+C to stop at any time)"
 
 set +e
-./script_for_creduce.sh 2>&1 >/tmp/script_for_creduce.out
+rm -rf /tmp/script_for_creduce.out
+$script_for_creduce >>/tmp/script_for_creduce.out 2>&1
 if [ $? -ne 0 ]; then
-    echo "error: script did not produce a Frama-C 'fatal' crash."
-    echo "       check the options given to Frama-C to ensure they make Frama-C crash."
+    # TODO: check if -cpp-extra-args exists and contains relative paths,
+    # and if so, warn about them
+    echo "#################################################"
+    echo "ERROR: script did not produce the expected error."
+    echo "       check the options given to Frama-C."
+    echo "       If you edited '$script_for_creduce', check it as well."
     echo ""
-    echo "Script output:"
-    cat /tmp/script_for_creduce.out
+    if [ $(wc -l /tmp/script_for_creduce.out | cut -d' ' -f1) -gt 20 ]; then
+        echo "# Script output (first 20 lines):"
+        head -n 20 /tmp/script_for_creduce.out
+        echo "(...) [truncated; full output in /tmp/script_for_creduce.out]"
+    else
+        echo "# Script output:"
+        cat /tmp/script_for_creduce.out
+    fi
     exit 1
 fi
 set -e

share/analysis-scripts/script_for_creduce_fatal.sh

+#!/bin/bash -e
+
+# Script to reduce a Frama-C crashing test case.
+
+# This script requires no modification.
+# Names between '@'s will be replaced by creduce.sh.
+
+set +e
+"@FRAMAC@" "@BASE@" @FCFLAGS@
+retcode=$?
+# see cmdline.ml for the different exit codes returned by Frama-C
+if [ $retcode -eq 125 -o $retcode -eq 4 ]; then
+    exit 0
+else
+    exit 1
+fi
+set -e

share/analysis-scripts/script_for_creduce_non_fatal.sh

+#!/bin/bash -e
+
+# Script to reduce a Frama-C non-crashing test case.
+
+# This script must be completed by the user.
+# Names between '@'s will be replaced by creduce.sh.
+# See the Frama-C User Manual for more details.
+
+cc_out=$(mktemp creduce_cc_XXXXXX.log)
+fc_out=$(mktemp creduce_fc_XXXXXX.log)
+
+# We always check that the reduced file remains valid C code.
+set -o pipefail
+@CPP@ "@BASE@" 2>&1 | tee $cc_out
+set +o pipefail
+
+### Examples of conditions to be maintained by C-Reduce; copy and adapt
+#
+# Ensure that the C file contains <expr>
+# grep -q expr "@BASE@"
+#
+# Ensure that the compiler output contains <expr>
+# grep -q <expr> "$cc_out"
+#
+###
+
+########## INSERT CONDITION(S) RELATED TO THE SOURCE HERE ##########
+
+##########
+
+"@FRAMAC@" "@BASE@" @FCFLAGS@ 2>&1 | tee $fc_out
+fc_retcode=$(echo ${PIPESTATUS[0]})
+
+### Examples of conditions to be maintained by C-Reduce; copy and adapt
+#
+# Ensure that Frama-C emits <expr>
+# grep -q <expr> "$fc_out"
+#
+# Ensure that the exit code of Frama_C is <rc>
+# test $fc_retcode -eq <rc>
+#
+###
+
+########## INSERT CONDITION(S) RELATED TO FRAMA-C HERE ##########
+
+##########
+
+### Cleanup
+rm -f $cc_out $fc_out