From 4c3d9494d6acf1170638d6646ef22414917a051d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Jan 2023 13:09:39 +0000 Subject: [PATCH 1/7] Fix C/C++ library check command line Compiler names may include spaces (such as `ccache gcc`). --- src/ansi-c/Makefile | 2 +- src/ansi-c/library_check.sh | 4 ++-- src/cpp/Makefile | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ansi-c/Makefile b/src/ansi-c/Makefile index 170afaf0a29..e3853d20de0 100644 --- a/src/ansi-c/Makefile +++ b/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 diff --git a/src/ansi-c/library_check.sh b/src/ansi-c/library_check.sh index c73fa8b1db7..592283b59e1 100755 --- a/src/ansi-c/library_check.sh +++ b/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 diff --git a/src/cpp/Makefile b/src/cpp/Makefile index 8fb3215f584..f305b166855 100644 --- a/src/cpp/Makefile +++ b/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 From 4d7039ed2c6adb2ed12ff3464fdb91805d82b28a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Jan 2023 13:59:44 +0000 Subject: [PATCH 2/7] C library: typecast Boolean operand to int when using bitwise ops Clang warns when bitwise operations are used with Boolean operands. --- src/ansi-c/library/cprover_contracts.c | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 33b7954cb47..721d7452863 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/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 From a0c408cd707d9c7e43b61b43a1fefafd8359d00b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Jan 2023 18:18:33 +0000 Subject: [PATCH 3/7] C model library: avoid duplicate *scanf definitions glibc headers define C99 variants via asm renaming. Library checks (rightly) failed when using clang 14, reporting duplicate definitions. Fixes: #7366 --- src/ansi-c/library/stdio.c | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c index d6bfc07293e..b8fa8d45ed8 100644 --- a/src/ansi-c/library/stdio.c +++ b/src/ansi-c/library/stdio.c @@ -824,6 +824,8 @@ void perror(const char *s) /* FUNCTION: fscanf */ +#if !defined(__USE_ISOC99) || !defined(__REDIRECT) + #ifndef __CPROVER_STDIO_H_INCLUDED #include #define __CPROVER_STDIO_H_INCLUDED @@ -844,6 +846,8 @@ __CPROVER_HIDE:; return result; } +#endif + /* FUNCTION: __isoc99_fscanf */ #ifndef __CPROVER_STDIO_H_INCLUDED @@ -868,6 +872,8 @@ __CPROVER_HIDE:; /* FUNCTION: scanf */ +#if !defined(__USE_ISOC99) || !defined(__REDIRECT) + #ifndef __CPROVER_STDIO_H_INCLUDED #include #define __CPROVER_STDIO_H_INCLUDED @@ -888,6 +894,8 @@ __CPROVER_HIDE:; return result; } +#endif + /* FUNCTION: __isoc99_scanf */ #ifndef __CPROVER_STDIO_H_INCLUDED @@ -912,6 +920,8 @@ __CPROVER_HIDE:; /* FUNCTION: sscanf */ +#if !defined(__USE_ISOC99) || !defined(__REDIRECT) + #ifndef __CPROVER_STDIO_H_INCLUDED #include #define __CPROVER_STDIO_H_INCLUDED @@ -932,6 +942,8 @@ __CPROVER_HIDE:; return result; } +#endif + /* FUNCTION: __isoc99_sscanf */ #ifndef __CPROVER_STDIO_H_INCLUDED @@ -956,6 +968,8 @@ __CPROVER_HIDE:; /* FUNCTION: vfscanf */ +#if !defined(__USE_ISOC99) || !defined(__REDIRECT) + #ifndef __CPROVER_STDIO_H_INCLUDED #include #define __CPROVER_STDIO_H_INCLUDED @@ -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,6 +1114,8 @@ int __stdio_common_vfscanf( /* FUNCTION: vscanf */ +#if !defined(__USE_ISOC99) || !defined(__REDIRECT) + #ifndef __CPROVER_STDIO_H_INCLUDED #include #define __CPROVER_STDIO_H_INCLUDED @@ -1114,6 +1132,8 @@ int vscanf(const char *restrict format, va_list arg) return vfscanf(stdin, format, arg); } +#endif + /* FUNCTION: __isoc99_vscanf */ #ifndef __CPROVER_STDIO_H_INCLUDED @@ -1134,6 +1154,8 @@ __CPROVER_HIDE:; /* FUNCTION: vsscanf */ +#if !defined(__USE_ISOC99) || !defined(__REDIRECT) + #ifndef __CPROVER_STDIO_H_INCLUDED #include #define __CPROVER_STDIO_H_INCLUDED @@ -1162,6 +1184,8 @@ __CPROVER_HIDE:; return result; } +#endif + /* FUNCTION: __isoc99_vsscanf */ #ifndef __CPROVER_STDIO_H_INCLUDED From c9f576e3e5949843bd3eb4fa51e813cccecaa6d4 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Jan 2023 21:41:13 +0000 Subject: [PATCH 4/7] C model library: clang-format include guards --- src/ansi-c/library/stdio.c | 96 +++++++++++++++++++------------------- 1 file changed, 48 insertions(+), 48 deletions(-) diff --git a/src/ansi-c/library/stdio.c b/src/ansi-c/library/stdio.c index b8fa8d45ed8..ab6ade0db88 100644 --- a/src/ansi-c/library/stdio.c +++ b/src/ansi-c/library/stdio.c @@ -826,15 +826,15 @@ void perror(const char *s) #if !defined(__USE_ISOC99) || !defined(__REDIRECT) -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif +# ifndef __CPROVER_STDIO_H_INCLUDED +# include +# define __CPROVER_STDIO_H_INCLUDED +# endif -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif +# ifndef __CPROVER_STDARG_H_INCLUDED +# include +# define __CPROVER_STDARG_H_INCLUDED +# endif int fscanf(FILE *restrict stream, const char *restrict format, ...) { @@ -874,15 +874,15 @@ __CPROVER_HIDE:; #if !defined(__USE_ISOC99) || !defined(__REDIRECT) -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif +# ifndef __CPROVER_STDIO_H_INCLUDED +# include +# define __CPROVER_STDIO_H_INCLUDED +# endif -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif +# ifndef __CPROVER_STDARG_H_INCLUDED +# include +# define __CPROVER_STDARG_H_INCLUDED +# endif int scanf(const char *restrict format, ...) { @@ -922,15 +922,15 @@ __CPROVER_HIDE:; #if !defined(__USE_ISOC99) || !defined(__REDIRECT) -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif +# ifndef __CPROVER_STDIO_H_INCLUDED +# include +# define __CPROVER_STDIO_H_INCLUDED +# endif -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif +# ifndef __CPROVER_STDARG_H_INCLUDED +# include +# define __CPROVER_STDARG_H_INCLUDED +# endif int sscanf(const char *restrict s, const char *restrict format, ...) { @@ -970,15 +970,15 @@ __CPROVER_HIDE:; #if !defined(__USE_ISOC99) || !defined(__REDIRECT) -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif +# ifndef __CPROVER_STDIO_H_INCLUDED +# include +# define __CPROVER_STDIO_H_INCLUDED +# endif -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif +# ifndef __CPROVER_STDARG_H_INCLUDED +# include +# define __CPROVER_STDARG_H_INCLUDED +# endif int __VERIFIER_nondet_int(); @@ -1116,15 +1116,15 @@ int __stdio_common_vfscanf( #if !defined(__USE_ISOC99) || !defined(__REDIRECT) -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif +# ifndef __CPROVER_STDIO_H_INCLUDED +# include +# define __CPROVER_STDIO_H_INCLUDED +# endif -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif +# ifndef __CPROVER_STDARG_H_INCLUDED +# include +# define __CPROVER_STDARG_H_INCLUDED +# endif int vscanf(const char *restrict format, va_list arg) { @@ -1156,15 +1156,15 @@ __CPROVER_HIDE:; #if !defined(__USE_ISOC99) || !defined(__REDIRECT) -#ifndef __CPROVER_STDIO_H_INCLUDED -#include -#define __CPROVER_STDIO_H_INCLUDED -#endif +# ifndef __CPROVER_STDIO_H_INCLUDED +# include +# define __CPROVER_STDIO_H_INCLUDED +# endif -#ifndef __CPROVER_STDARG_H_INCLUDED -#include -#define __CPROVER_STDARG_H_INCLUDED -#endif +# ifndef __CPROVER_STDARG_H_INCLUDED +# include +# define __CPROVER_STDARG_H_INCLUDED +# endif int __VERIFIER_nondet_int(); From 11c949f082b6dc8176beac6298470069c20d3338 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 24 Jan 2023 09:26:50 +0000 Subject: [PATCH 5/7] C++ model library: fix forward declarations All functions must be declared before being used, and library checks should not fail due to duplicate definitions. --- src/cpp/library/new.c | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/src/cpp/library/new.c b/src/cpp/library/new.c index fd8261e47b4..bf3ce6f364c 100644 --- a/src/cpp/library/new.c +++ b/src/cpp/library/new.c @@ -27,8 +27,10 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size) /* FUNCTION: __new_array */ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +#ifndef LIBRARY_CHECK const void *__CPROVER_new_object = 0; __CPROVER_bool __CPROVER_malloc_is_new_array = 0; +#endif inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size) { @@ -63,9 +65,12 @@ inline void *__placement_new(__typeof__(sizeof(int)) malloc_size, void *p) /* FUNCTION: __delete */ +void __CPROVER_deallocate(void *); __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +#ifndef LIBRARY_CHECK const void *__CPROVER_new_object = 0; __CPROVER_bool __CPROVER_malloc_is_new_array = 0; +#endif inline void __delete(void *ptr) { @@ -98,9 +103,12 @@ inline void __delete(void *ptr) /* FUNCTION: __delete_array */ +void __CPROVER_deallocate(void *); __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(); +#ifndef LIBRARY_CHECK const void *__CPROVER_new_object = 0; __CPROVER_bool __CPROVER_malloc_is_new_array = 0; +#endif inline void __delete_array(void *ptr) { From 90df48968395e7b746530f6cd9333cf47b8a569b Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 24 Jan 2023 09:27:58 +0000 Subject: [PATCH 6/7] CMake builds: enable library checks for C++ model library The rules were already in place, but there was no dependency to ensure invocation. --- src/cpp/CMakeLists.txt | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/cpp/CMakeLists.txt b/src/cpp/CMakeLists.txt index 2a5b3dc3559..2e481cdb860 100644 --- a/src/cpp/CMakeLists.txt +++ b/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) From 4bd1d944a5b30df32c2977d936ed7976d18f00e1 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Jan 2023 12:54:06 +0000 Subject: [PATCH 7/7] Test builds using clang-14 in CI Ubuntu 22.04 ships version 14 of clang by default. Use it in CI (and not just clang-10, as other jobs already do). --- .github/workflows/pull-request-checks.yaml | 70 ++++++++++++++++++++++ 1 file changed, 70 insertions(+) diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 63164be8a7d..1a386631ef4 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.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