linuxci: test compiling linux

.github/workflows/build-and-test-Linux.yaml

@@ -0,0 +1,53 @@
+name: Build Linux partially with CPROVER tools
+
+on:
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  CompileLinux:
+    runs-on: ubuntu-20.04
+    steps:
+      - uses: actions/checkout@v2
+        with:
+          submodules: true
+      - name: Install Packages
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -y g++ flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache
+          sudo apt-get install --no-install-recommends -y libssl-dev libelf-dev libudev-dev libpci-dev libiberty-dev autoconf
+          sudo apt-get install --no-install-recommends -y gawk jq
+
+      - name: Prepare ccache
+        uses: actions/cache@v2
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-20.04-make-${{ github.ref }}-${{ github.sha }}-KERNEL
+          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 CBMC tools
+        run: |
+          make -C src minisat2-download
+          make -C src CXX='ccache /usr/bin/g++' cbmc.dir goto-cc.dir goto-diff.dir -j2
+      - name: Print ccache stats
+        run: ccache -s
+
+      - name: Run (Docker Based) Linux Build test
+        run: integration/linux/compile_linux.sh
+
+      - uses: actions/upload-artifact@v2
+        with:
+          name: CPROVER-faultyInput
+          path: CPROVER/faultyInput/*

.github/workflows/pull-request-checks.yaml

@@ -364,7 +364,8 @@ jobs:
           # user input
           DEBIAN_FRONTEND: noninteractive
         run: |
-          pip install unidiff
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq python3-unidiff
       - name: Check updated lines of code meet linting standards
         env:
           BASE_BRANCH: ${{ github.base_ref }}

integration/linux/compile_linux.sh

@@ -0,0 +1,89 @@
+#!/bin/bash
+
+# Fail on errors
+# set -e # not for now
+
+# Show steps we execute
+set -x
+
+# This script needs to operate in the root directory of the CBMC repository
+SCRIPT=$(readlink -e "$0")
+readonly SCRIPT
+SCRIPTDIR=$(dirname "$SCRIPT")
+readonly SCRIPTDIR
+cd "$SCRIPTDIR/../.."
+
+# Build CBMC tools
+make -C src minisat2-download
+make -C src CXX='ccache /usr/bin/g++' cbmc.dir goto-cc.dir goto-diff.dir -j$(nproc)
+
+# Get one-line-scan, if we do not have it already
+[ -d one-line-scan ] || git clone https://github.com/awslabs/one-line-scan.git one-line-scan
+
+# Get Linux v5.10, if we do not have it already
+[ -d linux_5_10 ] || git clone -b v5.10 --depth=1 https://git.kernel.org/pub/scm/linux/kernel/git/stable/linux-stable.git linux_5_10
+
+# Prepare compile a part of the kernel with CBMC via one-line-scan
+ln -s goto-cc src/goto-cc/goto-ld
+ln -s goto-cc src/goto-cc/goto-as
+ln -s goto-cc src/goto-cc/goto-g++
+
+
+configure_linux ()
+{
+  pushd linux_5_10
+
+  cat > kvm-config <<EOF
+CONFIG_64BIT=y
+CONFIG_X86_64=y
+CONFIG_HIGH_RES_TIMERS=y
+CONFIG_MULTIUSER=y
+CONFIG_NET=y
+CONFIG_VIRTUALIZATION=y
+CONFIG_HYPERVISOR_GUEST=y
+CONFIG_PARAVIRT=y
+CONFIG_KVM_GUEST=y
+CONFIG_KVM=y
+CONFIG_KVM_INTEL=y
+CONFIG_KVM_AMD=y
+EOF
+  # using this failed in earlier attempts
+  export KCONFIG_ALLCONFIG=kvm-config
+
+  # using the previous configuration approach for now
+  make allnoconfig
+  popd
+}
+
+# Configure kernel, and compile all of it
+configure_linux
+make -C linux_5_10 bzImage -j $(nproc)
+ls linux_5_10/arch/x86/kvm/
+
+# Clean files we want to be able to re-compile
+find linux_5_10/arch/x86/kvm/ -name "*.o" -delete
+ls linux_5_10/arch/x86/kvm/
+
+# Compile Linux with CBMC via one-line-scan, and check for goto-cc section
+# Re-Compile with goto-cc, and measure disk space
+declare -i STATUS=0
+du -h --max-depth=1
+one-line-scan/one-line-scan \
+    --add-to-path $(pwd)/src/cbmc --add-to-path $(pwd)/src/goto-diff --add-to-path $(pwd)/src/goto-cc \
+    --cbmc \
+    --no-analysis \
+    --trunc-existing \
+    --extra-cflags -Wno-error \
+    -o CPROVER -j 5 -- \
+    make -C linux_5_10 bzImage -j $(nproc) || STATUS=$?
+du -h --max-depth=1
+
+# Check for faulty input
+ls CPROVER/faultyInput/* || true
+
+# Check for produced output in the files we deleted above
+ls linux_5_10/arch/x86/kvm/
+objdump -h linux_5_10/arch/x86/kvm/x86.o | grep "goto-cc" || STATUS=$?
+
+# Propagate failures
+exit "$STATUS"

regression/CMakeLists.txt

@@ -32,6 +32,10 @@ add_subdirectory(cpp)
 add_subdirectory(cbmc-concurrency)
 add_subdirectory(cbmc-cover)
 add_subdirectory(cbmc-incr-oneloop)
+add_subdirectory(cbmc-incr)
+add_subdirectory(cbmc-with-incr)
+add_subdirectory(array-refinement-with-incr)
+add_subdirectory(goto-instrument-wmm-core)
 add_subdirectory(goto-instrument-typedef)
 add_subdirectory(smt2_solver)
 add_subdirectory(smt2_strings)
@@ -69,6 +73,7 @@ add_subdirectory(validate-trace-xml-schema)
 add_subdirectory(cbmc-primitives)
 add_subdirectory(goto-interpreter)
 add_subdirectory(cbmc-sequentialization)
+add_subdirectory(cpp-linter)
 
 if(WITH_MEMORY_ANALYZER)
   add_subdirectory(snapshot-harness)

regression/Makefile

@@ -10,6 +10,10 @@ DIRS = cbmc \
        cbmc-concurrency \
        cbmc-cover \
        cbmc-incr-oneloop \
+       cbmc-incr \
+       cbmc-with-incr \
+       array-refinement-with-incr \
+       goto-instrument-wmm-core \
        goto-instrument-typedef \
        smt2_solver \
        smt2_strings \
@@ -42,6 +46,7 @@ DIRS = cbmc \
        cbmc-primitives \
        goto-interpreter \
        cbmc-sequentialization \
+			 cpp-linter \
        # Empty last line
 
 ifeq ($(OS),Windows_NT)

regression/array-refinement-with-incr/Array_UF1/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 11
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF10/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 1
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF11/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 1
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF12/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 2
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF13/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 1
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF14/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 6
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF15/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 11
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF16/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 2
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF17/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 9
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF18/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 11
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF19/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 3
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF2/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 5
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF20/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 12
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF3/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 3 --no-unwinding-assertions
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF4/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 2
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF5/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 2
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF6/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 3
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF7/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 3
 ^EXIT=10$

regression/array-refinement-with-incr/Array_UF8/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 6
 ^EXIT=0$

regression/array-refinement-with-incr/Array_UF9/test.desc

@@ -1,4 +1,4 @@
-CORE
+FUTURE
 main.c
 --arrays-uf-always --no-propagation --unwind-max 21
 ^EXIT=10$

regression/array-refinement-with-incr/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc> --incremental"
+)

regression/cbmc-cpp/Address_of_Method1/main.cpp

@@ -0,0 +1,18 @@
+#include <cassert>
+struct x
+{
+  void f();
+
+  static int i;
+};
+
+void x::f()
+{
+}
+
+int main()
+{
+  assert(&x::f != 0);
+
+  assert(&x::i != 0);
+}

regression/cbmc-cpp/Address_of_Method1/test.desc

@@ -0,0 +1,8 @@
+KNOWNBUG winbug macos-assert-broken
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-cpp/Anonymous_members1/main.cpp

@@ -0,0 +1,29 @@
+#include <cassert>
+typedef unsigned DWORD;
+typedef signed LONG;
+typedef long long LONGLONG;
+
+typedef union _LARGE_INTEGER {
+  struct
+  {
+    DWORD LowPart;
+    LONG HighPart;
+  };
+  struct
+  {
+    DWORD LowPart;
+    LONG HighPart;
+  } u;
+
+  LONGLONG QuadPart;
+} LARGE_INTEGER;
+
+int main()
+{
+  LARGE_INTEGER l;
+
+  l.QuadPart = 1;
+  l.LowPart = 2;
+  l.u.LowPart = 3;
+  assert(l.LowPart == 3);
+}

regression/cbmc-cpp/Anonymous_members1/test.desc

@@ -0,0 +1,8 @@
+CORE winbug macos-assert-broken
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc-cpp/Array1/main.cpp

@@ -0,0 +1,10 @@
+int y[5][4][3][2];
+
+int main()
+{
+  for(int i = 0; i < 5; i++)
+    for(int j = 0; j < 4; j++)
+      for(int k = 0; k < 3; k++)
+        for(int l = 0; l < 2; l++)
+          y[i][j][k][l] = 2;
+}