Add CSmith GitHub action

Run 10 randomly generated CSmith tests as a GitHub action to perform an
integration test involving CBMC and goto-instrument --dump-c. Each test
is first compiled and run using GCC to obtain a checksum, which is then
included as an assertion for CBMC to verify.

Author: tautschnig

.github/workflows/csmith.yaml

@@ -0,0 +1,45 @@
+name: Run CSmith
+
+on:
+  pull_request:
+    branches: [ develop ]
+
+jobs:
+  CompileXen:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get install --no-install-recommends -y build-essential flex bison maven ccache
+          sudo apt-get install --no-install-recommends -y csmith libcsmith-dev
+          make -C src minisat2-download
+      - name: Prepare ccache
+        uses: actions/cache@v2
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-20.04-make-${{ github.ref }}-${{ github.sha }}
+          restore-keys: |
+            ${{ runner.os }}-20.04-make-${{ github.ref }}
+            ${{ runner.os }}-20.04-make
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build with make
+        run: |
+          make -C src CXX='ccache /usr/bin/g++' cbmc.dir goto-cc.dir goto-instrument.dir -j2
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Run 10 randomly-generated CSmith tests
+        run: |
+          export PATH=$PWD/src/cbmc:$PWD/src/goto-cc:$PWD/src/goto-instrument:$PATH
+          scripts/csmith.sh 10

scripts/csmith.sh

@@ -0,0 +1,78 @@
+#!/bin/bash
+
+set -e
+
+workdir=$(mktemp -d csmith.XXX)
+print_dir() {
+  echo "CSmith working directory: $workdir"
+}
+
+csmith_test() {
+  trap print_dir ERR
+
+  local f=$1
+  local r=$(cbmc --version)
+  local bn=`basename $f`
+  bn=`basename $bn .c`
+
+  echo "Trying $f with build $r"
+
+  gcc -I/usr/include/csmith -w $f -o $bn
+  check="`timeout 30 ./$bn | sed 's/checksum = /0x/'`"
+  if [ -z "$check" ] ; then
+    echo "TIMEOUT while executing CSmith test"
+    return 0
+  fi
+
+  gcc -E -I/usr/include/csmith -D__FRAMAC \
+    -D'Frama_C_dump_assert_each()'="assert($check==(crc))" $f -o $bn.i
+  ec=0
+  /usr/bin/time -v timeout -k15 90 cbmc --unwind 257 --no-unwinding-assertions --object-bits 13 $bn.i || ec=$?
+  if [ $ec -eq 124 ] || [ $ec -eq 137 ] ; then
+    echo "TIMEOUT in CBMC"
+  elif [ $ec -eq 6 ] ; then
+    echo "Limitation in CBMC"
+  elif [ $ec -ne 0 ] ; then
+    cat $f
+    return 1
+  fi
+
+  goto-cc -I /usr/include/csmith $f -o $bn
+  goto-instrument --dump-c $bn ${bn}_dumped.c
+  gcc ${bn}_dumped.c -D__CPROVER_bool=_Bool -w -o $bn
+  check_d="`timeout 30 ./$bn | sed 's/checksum = /0x/'`"
+  if [ -z "$check_d" ] ; then
+    echo "TIMEOUT while executing dumped CSmith test"
+    return 0
+  fi
+  if [ "$check" != "$check_d" ] ; then
+    echo "Checksum mismatch: GCC: $check dump-c: $check_d"
+    cat $f
+    return 1
+  fi
+
+  echo "OK: $f"
+  echo
+}
+
+csmith_random_test() {
+  trap print_dir ERR
+
+  for i in `seq 1 $1`; do
+    csmith > t_$i.c
+    csmith_test t_$i.c
+  done
+}
+
+N=$1
+if [ -z $N ] ; then
+  N=1
+fi
+
+basedir=$PWD
+cd $workdir
+
+csmith_random_test $N
+
+cd $basedir
+rm -rf $workdir