Merge branch 'feature/andre/creduce-more' into 'master'

[analysis-scripts] improve and generalize creduce.sh

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

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

bin/frama-c-script

@@ -37,6 +37,11 @@ usage() {
    echo "      and non-POSIX external libraries."
    echo "      (run 'frama-c -machdep help' to get the list of machdeps)."
    echo ""
+   echo "  - creduce <args>"
+   echo "      Use the external tool C-Reduce to minimize C files when"
+   echo "      debugging crashes and fatal errors. Run without arguments for"
+   echo "      more details."
+   echo ""
    echo "  - estimate-difficulty file..."
    echo "      Applies several heuristics to try and estimate the difficulty"
    echo "      of analyzing the specified files with Frama-C."
@@ -259,6 +264,10 @@ case "$command" in
         shift;
         "${FRAMAC_SHARE}"/analysis-scripts/normalize_jcdb.py "$@";
         ;;
+    "creduce")
+        shift;
+        ${FRAMAC_SHARE}/analysis-scripts/creduce.sh "$@";
+        ;;
     *)
         echo "error: unrecognized command: $command";
         exit 1

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,93 @@
 #                                                                        #
 ##########################################################################
 
-# 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".
+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 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).
+# Requirements
 
-### How it works
-#
-#   creduce.sh <file.c> <command line options>
+- 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: <script options> <file> <Frama-C 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 directory 'creducing'.
+
+# Script options
+
+Note: these options must be placed _before_ all other arguments.
+
+--help: show this help message.
+
+--ignore-parsability: do not check that each reduced program conforms to
+                      a gcc parsability check; helps avoid issues due to
+                      preprocessing flags.
+
+# 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.
+"
+
+#### Command-line and environment validation
 #
-# 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'.
+
+ignore_parsability=0
+while [ $# -ge 1 ]; do
+    case "$1" in
+        --help) echo "$usage"; exit;;
+        --h) echo "$usage"; exit;;
+        -help) echo "$usage"; exit;;
+        -h) echo "$usage"; exit;;
+        --ignore-parsability)
+            ignore_parsability=1
+            shift
+            ;;
+        *) break;;
+    esac
+done
 
 if [ $# -lt 1 ]; then
-    echo "usage: $0 file.c [Frama-C options that cause a crash]"
-    exit 1
+    echo "$usage"
+    exit
 fi
 
 file="$1"
 base=$(basename "$file")
 shift
-options="$@"
+
 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 +116,57 @@ if [[ ! -f "$file" ]]; then
     exit 1
 fi
 
-if [[ $(dirname "$file") -eq "$dir_for_reduction" ]]; then
+too_many_sources=""
+for f in "$@"; do
+    if [ -e "$f" ]; then
+        too_many_sources+=" $f"
+    fi
+done
+if [ ! -z "$too_many_sources" ]; then
+    echo "error: too many sources; only the first argument must be a file: $file"
+    echo "       remove these from the command-line:$too_many_sources"
+    exit 1
+fi
+
+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 ! sed --version >/dev/null 2>&1; then
+    echo "[info] sed is not GNU, trying gsed..."
+    if command -v gsed >/dev/null; then
+        echo "[info] gsed found, using it."
+        SED="gsed"
+    else
+        echo "error: GNU sed is required but was not found (neither sed nor gsed)"
+        exit 1
+    fi
+else
+    SED="sed"
+fi
+
+#
+#
+#### End of command-line and environment validation
+
 if [[ ! "$options" =~ no-autoload-plugins ]]; then
     echo "********************************************************************"
     echo "Hint: consider using -no-autoload-plugins -load-module [modules]"
@@ -93,69 +179,106 @@ 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"
+    set +e
+    cpp_output=$("$FRAMAC" -print-cpp-commands "$@" "$file" 2>/dev/null)
+    cpp_retcode=$?
+    set -e
+    if [ $cpp_retcode -ne 0 ]; then
+        echo "error trying to get preprocessing flags (exit code: $cpp_retcode): $FRAMAC -print-cpp-commands $@ $file"
+        exit $cpp_retcode
+    fi
+    CPP=$(echo "$cpp_output" | \
+          "$SED" -n '/Preprocessing command:/{n;p;}' | "$SED" "s|'.*' -o '.*'||")
+    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"
+if [ "$ignore_parsability" -eq 0 ]; then
+    echo "[info] the following command will be used to check for syntactic validity during reduction:"
+    echo "    $CPP"
 fi
 
-echo "[info] checking syntactic validity with: $CC $CFLAGS"
-
+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
+if [ "$ignore_parsability" -eq 0 ]; then
+    "$SED" -i "s|@CPP@|$CPP|g" "$script_for_creduce"
 else
-    exit 1
+    "$SED" -i "s|^.*@CPP@.*$||g" "$script_for_creduce"
 fi
-set -e
-
-EOF
-
-chmod u+x script_for_creduce.sh
+"$SED" -i "s|@FRAMAC@|$FRAMAC|g" "$script_for_creduce"
+"$SED" -i "s|@BASE@|$base|g" "$script_for_creduce"
+"$SED" -i "s|@FCFLAGS@|$(echo $@ | tr "'" "\\'")|g" "$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
+trap '{ echo "Creduce interrupted!"; echo ""; echo "(partially) reduced file: $dir_for_reduction/$base"; exit 0; }' SIGINT
 
+echo ""
 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
@@ -163,3 +286,4 @@ set -e
 "$CREDUCE" script_for_creduce.sh "$base"
 
 echo "Finished reducing file: $dir_for_reduction/$base"
+echo "Remember to remove 'script_for_creduce.sh' after you are done."

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 ##########
+
+##########
+
+set -o pipefail
+"@FRAMAC@" "@BASE@" @FCFLAGS@ 2>&1 | tee $fc_out
+fc_retcode=$(echo ${PIPESTATUS[0]})
+set +o pipefail
+
+### 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