|
| 1 | +#!/bin/bash |
| 2 | +# |
| 3 | +# This script runs CSmith to generate N examples, and for each of them: |
| 4 | +# 1. Compiles the code with the system compiler. |
| 5 | +# 2. Runs the compiled code to obtain the checksum that the CSmith test |
| 6 | +# computes. |
| 7 | +# 3. Takes that checksum to generate an assertion. |
| 8 | +# 4. Runs CBMC (for up to 90 seconds and with a loop unwinding of 257) to verify |
| 9 | +# the generated assertion. If CBMC were to come up with a counterexample, then |
| 10 | +# CBMC's symbolic execution would differ from the concrete execution of what |
| 11 | +# ought to be a fully deterministic test. Such a failing test would therefore |
| 12 | +# indicate a bug in CBMC. For such a failing case, the source code of the test |
| 13 | +# is emitted. |
| 14 | +# 5. If CBMC's execution completed successfully or timed out, the test is next |
| 15 | +# compiled using goto-cc and dumped back to C code using goto-instrument. |
| 16 | +# 6. The dumped C code is compiled using GCC and executed again, computing a |
| 17 | +# fresh checksum. |
| 18 | +# 7. This checksum is compared to the previous one to ensure that the program is |
| 19 | +# equivalent to the original test generated by CSmith. |
| 20 | +# |
| 21 | +# The number "N" of such tests run can be specified as a command-line |
| 22 | +# argument to this script. If no command-line arguments are provided, only a |
| 23 | +# single test is run. |
| 24 | +# |
| 25 | +# As a second command-line argument, a random seed can be provided. This is |
| 26 | +# primarily useful to reproduce earlier failures. When a random seed is |
| 27 | +# provided, N is forced to 1. |
| 28 | +# |
| 29 | +# The script assumes that csmith (including its development headers) is |
| 30 | +# installed (or otherwise found on the PATH). cbmc, goto-cc, and goto-instrument |
| 31 | +# must also be found via the system PATH. |
| 32 | + |
| 33 | +set -e |
| 34 | + |
| 35 | +workdir=$(mktemp -d csmith.XXX) |
| 36 | +print_dir() { |
| 37 | + echo "CSmith working directory: $workdir" |
| 38 | +} |
| 39 | + |
| 40 | +# Run a single (previously generated) test. |
| 41 | +csmith_test() { |
| 42 | + trap print_dir ERR |
| 43 | + |
| 44 | + local f=$1 |
| 45 | + local r=$(cbmc --version) |
| 46 | + local bn=`basename $f` |
| 47 | + bn=`basename $bn .c` |
| 48 | + |
| 49 | + echo "Trying $f with build $r" |
| 50 | + |
| 51 | + # Compile and run (for up to 30 seconds) the CSmith-generated test. |
| 52 | + gcc -I/usr/include/csmith -w $f -o $bn |
| 53 | + check="`timeout 30 ./$bn | sed 's/checksum = /0x/'`" |
| 54 | + if [ -z "$check" ] ; then |
| 55 | + echo "TIMEOUT while executing CSmith test" |
| 56 | + return 0 |
| 57 | + fi |
| 58 | + |
| 59 | + # Prepare the test CBMC by injecting the checksum as an assertion. |
| 60 | + gcc -E -I/usr/include/csmith -D__FRAMAC \ |
| 61 | + -D'Frama_C_dump_assert_each()'="assert($check==(crc))" $f -o $bn.i |
| 62 | + # Run the test using CBMC for up to 90 seconds, unwinding loops up to 257 |
| 63 | + # times. |
| 64 | + ec=0 |
| 65 | + /usr/bin/time -v timeout -k15 90 cbmc \ |
| 66 | + --unwind 257 --no-unwinding-assertions --object-bits 13 \ |
| 67 | + $bn.i || ec=$? |
| 68 | + if [ $ec -eq 124 ] || [ $ec -eq 137 ] ; then |
| 69 | + echo "TIMEOUT in CBMC" |
| 70 | + elif [ $ec -eq 6 ] ; then |
| 71 | + echo "Limitation in CBMC" |
| 72 | + elif [ $ec -ne 0 ] ; then |
| 73 | + cat $f |
| 74 | + return 1 |
| 75 | + fi |
| 76 | +
|
| 77 | + # Compile the test using goto-cc and dump it back to C code using |
| 78 | + # goto-instrument. |
| 79 | + goto-cc -I /usr/include/csmith $f -o $bn |
| 80 | + goto-instrument --dump-c $bn ${bn}_dumped.c |
| 81 | + # Re-compile the dumped test and execute again to confirm the checksum hasn't |
| 82 | + # changed. |
| 83 | + gcc ${bn}_dumped.c -D__CPROVER_bool=_Bool -w -o $bn |
| 84 | + check_d="`timeout 30 ./$bn | sed 's/checksum = /0x/'`" |
| 85 | + if [ -z "$check_d" ] ; then |
| 86 | + echo "TIMEOUT while executing dumped CSmith test" |
| 87 | + return 0 |
| 88 | + fi |
| 89 | + if [ "$check" != "$check_d" ] ; then |
| 90 | + echo "Checksum mismatch: GCC: $check dump-c: $check_d" |
| 91 | + cat $f |
| 92 | + return 1 |
| 93 | + fi |
| 94 | + |
| 95 | + echo "OK: $f" |
| 96 | + echo |
| 97 | +} |
| 98 | + |
| 99 | +# Generate and run a number of tests. |
| 100 | +csmith_random_test() { |
| 101 | + trap print_dir ERR |
| 102 | + |
| 103 | + local fixed_seed=$2 |
| 104 | + |
| 105 | + for i in `seq 1 $1`; do |
| 106 | + local seed=`date +%s` |
| 107 | + if [ "x$fixed_seed" != x ] ; then |
| 108 | + seed=$fixed_seed |
| 109 | + fi |
| 110 | + echo "Random seed being used: $seed" |
| 111 | + csmith --seed $seed > t_$i.c |
| 112 | + if ! csmith_test t_$i.c ; then |
| 113 | + echo "Failed test obtained with random seed $seed" |
| 114 | + return 1 |
| 115 | + fi |
| 116 | + done |
| 117 | +} |
| 118 | + |
| 119 | +# Determine the number of tests to run from the command line; the default is to |
| 120 | +# run a single test. |
| 121 | +N=$1 |
| 122 | +if [ -z $N ] ; then |
| 123 | + N=1 |
| 124 | +fi |
| 125 | + |
| 126 | +# A random seed may be provided on the command line. Really only makes sense |
| 127 | +# when N is set to 1 |
| 128 | +SEED=$2 |
| 129 | +if [ $N != 1 ] ; then |
| 130 | + echo "Only running a single test with fixed random seed" |
| 131 | + N=1 |
| 132 | +fi |
| 133 | + |
| 134 | +basedir=$PWD |
| 135 | +cd $workdir |
| 136 | +trap print_dir ERR |
| 137 | + |
| 138 | +csmith_random_test $N $SEED |
| 139 | + |
| 140 | +cd $basedir |
| 141 | +rm -rf $workdir |
0 commit comments