Test builds using clang-14 in CI

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

@@ -242,6 +242,76 @@ jobs:
       - name: Run tests
         run: cd build; ctest . -V -L CORE -j2
 
+  # This job takes approximately N minutes
+  check-ubuntu-22_04-make-clang:
+    runs-on: ubuntu-22.04
+    env:
+      CC: "ccache /usr/bin/clang"
+      CXX: "ccache /usr/bin/clang++"
+    steps:
+      - uses: actions/checkout@v3
+        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 update
+          sudo apt-get install --no-install-recommends -yq clang clang-14 gdb maven jq flex bison libxml2-utils cpanminus ccache z3
+          make -C src minisat2-download
+          cpanm Thread::Pool::Simple
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Download cvc-5 from the releases page and make sure it can be deployed
+        run: |
+          wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux
+          chmod u+x cvc5
+          mv cvc5 /usr/local/bin
+          cvc5 --version
+      - name: Prepare ccache
+        uses: actions/cache@v3
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-22.04-make-clang-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-22.04-make-clang-${{ github.ref }}
+            ${{ runner.os }}-22.04-make-clang
+      - 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: Perform C/C++ library syntax check
+        run: |
+          make -C src/ansi-c library_check
+          make -C src/cpp library_check
+      - name: Build with make
+        run: |
+          make -C src       -j2
+          make -C unit      -j2
+          make -C jbmc/src  -j2
+          make -C jbmc/unit -j2
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Run unit tests
+        run: |
+          make -C unit      test
+          make -C jbmc/unit test
+          make TAGS="[z3]" -C unit test
+      - name: Run expected failure unit tests
+        run: |
+          make TAGS="[!shouldfail]" -C unit test
+          make TAGS="[!shouldfail]" -C jbmc/unit test
+      - name: Run regression tests
+        run: |
+          make -C regression test-parallel JOBS=2
+          make -C regression/cbmc test-paths-lifo
+          env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
+          make -C jbmc/regression test-parallel JOBS=2
+
   # This job takes approximately 41 minutes
   check-ubuntu-22_04-cmake-gcc:
     runs-on: ubuntu-22.04

src/ansi-c/Makefile

@@ -109,7 +109,7 @@ else
   platform_unavail = library/java.io.c library/threads.c
 endif
 library_check: library/*.c
-	./library_check.sh $(CC) $(filter-out $(platform_unavail), $^)
+	./library_check.sh "$(CC)" $(filter-out $(platform_unavail), $^)
 	touch $@
 
 cprover_library.inc: library/converter$(EXEEXT) library/*.c

src/ansi-c/library/cprover_contracts.c

@@ -210,8 +210,8 @@ __CPROVER_HIDE:;
 CAR_SET_CONTAINS_LOOP:
   while(idx != 0)
   {
-    incl |= candidate.is_writable & elem->is_writable &
-            __CPROVER_same_object(elem->lb, candidate.lb) &
+    incl |= (int)candidate.is_writable & (int)elem->is_writable &
+            (int)__CPROVER_same_object(elem->lb, candidate.lb) &
             (__CPROVER_POINTER_OFFSET(elem->lb) <=
              __CPROVER_POINTER_OFFSET(candidate.lb)) &
             (__CPROVER_POINTER_OFFSET(candidate.ub) <=
@@ -798,7 +798,7 @@ __CPROVER_HIDE:;
   while(idx != 0)
   {
     incl |=
-      elem->is_writable & __CPROVER_same_object(elem->lb, ptr) &
+      (int)elem->is_writable & (int)__CPROVER_same_object(elem->lb, ptr) &
       (__CPROVER_POINTER_OFFSET(elem->lb) <= offset) &
       (__CPROVER_POINTER_OFFSET(ub) <= __CPROVER_POINTER_OFFSET(elem->ub));
     ++elem;
@@ -1045,8 +1045,9 @@ __CPROVER_HIDE:;
     // call free only iff the pointer is valid preconditions are met
     // skip checks on r_ok, dynamic_object and pointer_offset
     __CPROVER_bool preconditions =
-      (ptr == 0) | (__CPROVER_r_ok(ptr, 0) & __CPROVER_DYNAMIC_OBJECT(ptr) &
-                    (__CPROVER_POINTER_OFFSET(ptr) == 0));
+      (ptr == 0) |
+      ((int)__CPROVER_r_ok(ptr, 0) & (int)__CPROVER_DYNAMIC_OBJECT(ptr) &
+       (__CPROVER_POINTER_OFFSET(ptr) == 0));
     // If there is aliasing between the pointers in the freeable set,
     // and we attempt to free again one of the already freed pointers,
     // the r_ok condition above will fail, preventing us to deallocate

src/ansi-c/library/stdio.c

@@ -824,15 +824,17 @@ void perror(const char *s)
 
 /* FUNCTION: fscanf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
+#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
 
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
+#  ifndef __CPROVER_STDIO_H_INCLUDED
+#    include <stdio.h>
+#    define __CPROVER_STDIO_H_INCLUDED
+#  endif
+
+#  ifndef __CPROVER_STDARG_H_INCLUDED
+#    include <stdarg.h>
+#    define __CPROVER_STDARG_H_INCLUDED
+#  endif
 
 int fscanf(FILE *restrict stream, const char *restrict format, ...)
 {
@@ -844,6 +846,8 @@ __CPROVER_HIDE:;
   return result;
 }
 
+#endif
+
 /* FUNCTION: __isoc99_fscanf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
@@ -868,15 +872,17 @@ __CPROVER_HIDE:;
 
 /* FUNCTION: scanf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
+#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
 
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
+#  ifndef __CPROVER_STDIO_H_INCLUDED
+#    include <stdio.h>
+#    define __CPROVER_STDIO_H_INCLUDED
+#  endif
+
+#  ifndef __CPROVER_STDARG_H_INCLUDED
+#    include <stdarg.h>
+#    define __CPROVER_STDARG_H_INCLUDED
+#  endif
 
 int scanf(const char *restrict format, ...)
 {
@@ -888,6 +894,8 @@ __CPROVER_HIDE:;
   return result;
 }
 
+#endif
+
 /* FUNCTION: __isoc99_scanf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
@@ -912,15 +920,17 @@ __CPROVER_HIDE:;
 
 /* FUNCTION: sscanf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
+#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
 
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
+#  ifndef __CPROVER_STDIO_H_INCLUDED
+#    include <stdio.h>
+#    define __CPROVER_STDIO_H_INCLUDED
+#  endif
+
+#  ifndef __CPROVER_STDARG_H_INCLUDED
+#    include <stdarg.h>
+#    define __CPROVER_STDARG_H_INCLUDED
+#  endif
 
 int sscanf(const char *restrict s, const char *restrict format, ...)
 {
@@ -932,6 +942,8 @@ __CPROVER_HIDE:;
   return result;
 }
 
+#endif
+
 /* FUNCTION: __isoc99_sscanf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
@@ -956,15 +968,17 @@ __CPROVER_HIDE:;
 
 /* FUNCTION: vfscanf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
+#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
 
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
+#  ifndef __CPROVER_STDIO_H_INCLUDED
+#    include <stdio.h>
+#    define __CPROVER_STDIO_H_INCLUDED
+#  endif
+
+#  ifndef __CPROVER_STDARG_H_INCLUDED
+#    include <stdarg.h>
+#    define __CPROVER_STDARG_H_INCLUDED
+#  endif
 
 int __VERIFIER_nondet_int();
 
@@ -998,6 +1012,8 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
   return result;
 }
 
+#endif
+
 /* FUNCTION: __isoc99_vfscanf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
@@ -1098,22 +1114,26 @@ int __stdio_common_vfscanf(
 
 /* FUNCTION: vscanf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
+#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
 
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
+#  ifndef __CPROVER_STDIO_H_INCLUDED
+#    include <stdio.h>
+#    define __CPROVER_STDIO_H_INCLUDED
+#  endif
+
+#  ifndef __CPROVER_STDARG_H_INCLUDED
+#    include <stdarg.h>
+#    define __CPROVER_STDARG_H_INCLUDED
+#  endif
 
 int vscanf(const char *restrict format, va_list arg)
 {
   __CPROVER_HIDE:;
   return vfscanf(stdin, format, arg);
 }
 
+#endif
+
 /* FUNCTION: __isoc99_vscanf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED
@@ -1134,15 +1154,17 @@ __CPROVER_HIDE:;
 
 /* FUNCTION: vsscanf */
 
-#ifndef __CPROVER_STDIO_H_INCLUDED
-#include <stdio.h>
-#define __CPROVER_STDIO_H_INCLUDED
-#endif
+#if !defined(__USE_ISOC99) || !defined(__REDIRECT)
 
-#ifndef __CPROVER_STDARG_H_INCLUDED
-#include <stdarg.h>
-#define __CPROVER_STDARG_H_INCLUDED
-#endif
+#  ifndef __CPROVER_STDIO_H_INCLUDED
+#    include <stdio.h>
+#    define __CPROVER_STDIO_H_INCLUDED
+#  endif
+
+#  ifndef __CPROVER_STDARG_H_INCLUDED
+#    include <stdarg.h>
+#    define __CPROVER_STDARG_H_INCLUDED
+#  endif
 
 int __VERIFIER_nondet_int();
 
@@ -1162,6 +1184,8 @@ __CPROVER_HIDE:;
   return result;
 }
 
+#endif
+
 /* FUNCTION: __isoc99_vsscanf */
 
 #ifndef __CPROVER_STDIO_H_INCLUDED

src/ansi-c/library_check.sh

@@ -12,8 +12,8 @@ for f in "$@"; do
     perl -p -i -e 's/(_mm_.fence)/s$1/' __libcheck.c
     perl -p -i -e 's/(__sync_)/s$1/' __libcheck.c
     perl -p -i -e 's/(__atomic_)/s$1/' __libcheck.c
-    "$CC" -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
-    "$CC" -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i \
+    $CC -std=gnu99 -E -include library/cprover.h -D__CPROVER_bool=_Bool -D__CPROVER_thread_local=__thread -DLIBRARY_CHECK -o __libcheck.i __libcheck.c
+    $CC -S -Wall -Werror -pedantic -Wextra -std=gnu99 __libcheck.i \
       -o __libcheck.s -Wno-unused-label -Wno-unknown-pragmas
     ec="${?}"
     rm __libcheck.s __libcheck.i __libcheck.c

src/cpp/CMakeLists.txt

@@ -24,13 +24,24 @@ endif()
 
 ################################################################################
 
+set(extra_dependencies
+    ${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc
+    ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp
+)
+
+if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+    list(REMOVE_ITEM
+         extra_dependencies
+         ${CMAKE_CURRENT_BINARY_DIR}/library-check.stamp)
+endif()
+
 file(GLOB_RECURSE sources "*.cpp" "*.h")
 add_library(cpp ${sources})
 
 set_source_files_properties(
         ${sources}
         PROPERTIES
-        OBJECT_DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/cprover_library.inc"
+        OBJECT_DEPENDS "${extra_dependencies}"
 )
 
 generic_includes(cpp)

src/cpp/Makefile

@@ -69,7 +69,7 @@ cprover_library$(OBJEXT): cprover_library.inc
 	$(MAKE) -C ../ansi-c library/converter$(EXEEXT)
 
 library_check: library/*.c
-	../ansi-c/library_check.sh $(CC) $^
+	../ansi-c/library_check.sh "$(CC)" $^
 	touch $@
 
 cprover_library.inc: ../ansi-c/library/converter$(EXEEXT) library/*.c