From d4257dc8b55583399385151566f65f919efa4b64 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 16 May 2024 14:02:12 +0200 Subject: [PATCH 01/12] Install lit and tabulate via brew on macOS --- scripts/build/p-klee-osx.inc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/build/p-klee-osx.inc b/scripts/build/p-klee-osx.inc index 12893fbbb4..b909b18304 100644 --- a/scripts/build/p-klee-osx.inc +++ b/scripts/build/p-klee-osx.inc @@ -7,7 +7,7 @@ install_build_dependencies_klee() { brew install doxygen graphviz fi - pip3 install --user --upgrade lit tabulate + brew install python-tabulate lit brew install pkg-config brew install coreutils From 3a4dcb142119d024fd69cfc8d3d3d3f156c11182 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 16 May 2024 14:58:01 +0200 Subject: [PATCH 02/12] Use LLVM 14 for the macOS CI target --- .github/workflows/build.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/build.yaml b/.github/workflows/build.yaml index 8267591b19..2a5aa24aee 100644 --- a/.github/workflows/build.yaml +++ b/.github/workflows/build.yaml @@ -151,8 +151,8 @@ jobs: macOS: runs-on: macos-latest env: + LLVM_VERSION: 14 BASE: /tmp - LLVM_VERSION: 13 SOLVERS: STP UCLIBC_VERSION: 0 USE_TCMALLOC: 0 From 8c1edf7767a36f96b2323d882c1ca48dac7e0e2f Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 16 May 2024 18:31:36 +0200 Subject: [PATCH 03/12] Fix/update LLVM path on macOS --- scripts/build/p-llvm-osx.inc | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/build/p-llvm-osx.inc b/scripts/build/p-llvm-osx.inc index 731b14f5fa..020c52a18a 100644 --- a/scripts/build/p-llvm-osx.inc +++ b/scripts/build/p-llvm-osx.inc @@ -9,13 +9,13 @@ install_binary_artifact_llvm () { is_installed_llvm() { # Check if llvm-config with the right version exists LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" - [[ -f "/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/llvm-config" ]] + [[ -f "/opt/homebrew/opt/llvm@${LLVM_VERSION_MAJOR}/bin/llvm-config" ]] } setup_artifact_variables_llvm() { LLVM_VERSION_MAJOR="${LLVM_VERSION/.*/}" - LLVM_CONFIG="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/llvm-config" - BITCODE_CC="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/clang" - BITCODE_CXX="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/bin/clang++" - LLVM_INSTALL="/usr/local/opt/llvm@${LLVM_VERSION_MAJOR}/" + LLVM_CONFIG="/opt/homebrew/opt/llvm@${LLVM_VERSION_MAJOR}/bin/llvm-config" + BITCODE_CC="/opt/homebrew/opt/llvm@${LLVM_VERSION_MAJOR}/bin/clang" + BITCODE_CXX="/opt/homebrew/opt/llvm@${LLVM_VERSION_MAJOR}/bin/clang++" + LLVM_INSTALL="/opt/homebrew/opt/llvm@${LLVM_VERSION_MAJOR}/" } From b1d44aca704f639bb7bfb6f069a7b55ad49245c4 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sat, 25 May 2024 14:08:58 +0100 Subject: [PATCH 04/12] Fix test case that currently fails on Apple Silicon, where sizeof(long double) == sizeof(double) --- test/Feature/LongDoubleSupport.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/test/Feature/LongDoubleSupport.c b/test/Feature/LongDoubleSupport.c index 62cbc1b885..359fd05c9d 100644 --- a/test/Feature/LongDoubleSupport.c +++ b/test/Feature/LongDoubleSupport.c @@ -34,7 +34,11 @@ int main() { assert(N0 == 6); assert(N1 == 9); - assert(N2 == 13); + // This is the case on Apple Silicon + if (sizeof(long double) == sizeof(double)) + assert(N2 == 9); + else + assert(N2 == 13); return 0; } From a38cf4bc948ec6087db6be6a4e7ca9146747d547 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sat, 1 Jun 2024 16:54:21 +0100 Subject: [PATCH 05/12] Inline assembly is not supported on Apple Silicon, so disabling these tests on macOS --- test/Feature/InlineAsm.c | 4 ++++ test/Feature/RaiseAsm.c | 4 ++++ test/Feature/asm_lifting.ll | 3 +++ 3 files changed, 11 insertions(+) diff --git a/test/Feature/InlineAsm.c b/test/Feature/InlineAsm.c index 25e0e72e7e..ae549ae5cd 100644 --- a/test/Feature/InlineAsm.c +++ b/test/Feature/InlineAsm.c @@ -1,7 +1,11 @@ +// Not supported on Apple Silicon +// REQUIRES: not-darwin + // RUN: %clang %s -emit-llvm %O0opt -c -g -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --external-calls=all --exit-on-error --output-dir=%t.klee-out %t.bc > %t.output.log 2>&1 +#include "klee/klee.h" #include int main() { diff --git a/test/Feature/RaiseAsm.c b/test/Feature/RaiseAsm.c index be6c5c7356..e180564137 100644 --- a/test/Feature/RaiseAsm.c +++ b/test/Feature/RaiseAsm.c @@ -1,7 +1,11 @@ +// Not supported on Apple Silicon +// REQUIRES: not-darwin + // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --exit-on-error %t1.bc +#include "klee/klee.h" #include typedef unsigned short uint16; diff --git a/test/Feature/asm_lifting.ll b/test/Feature/asm_lifting.ll index a3893d438e..246ae881c7 100644 --- a/test/Feature/asm_lifting.ll +++ b/test/Feature/asm_lifting.ll @@ -1,3 +1,6 @@ +; Not supported on Apple Silicon +; REQUIRES: not-darwin + ; RUN: %llvmas %s -f -o %t1.bc ; RUN: rm -rf %t.klee-out ; RUN: %klee --output-dir=%t.klee-out --optimize=false --split-calls=false %t1.bc From 3c091abdf78db8c2679e6a451468199384a491e4 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sat, 1 Jun 2024 16:55:29 +0100 Subject: [PATCH 06/12] Moving inline assembly tests to a separate directory --- test/{Feature => InlineAsm}/InlineAsm.c | 0 test/{Feature => InlineAsm}/RaiseAsm.c | 0 test/{Feature => InlineAsm}/asm_lifting.ll | 0 3 files changed, 0 insertions(+), 0 deletions(-) rename test/{Feature => InlineAsm}/InlineAsm.c (100%) rename test/{Feature => InlineAsm}/RaiseAsm.c (100%) rename test/{Feature => InlineAsm}/asm_lifting.ll (100%) diff --git a/test/Feature/InlineAsm.c b/test/InlineAsm/InlineAsm.c similarity index 100% rename from test/Feature/InlineAsm.c rename to test/InlineAsm/InlineAsm.c diff --git a/test/Feature/RaiseAsm.c b/test/InlineAsm/RaiseAsm.c similarity index 100% rename from test/Feature/RaiseAsm.c rename to test/InlineAsm/RaiseAsm.c diff --git a/test/Feature/asm_lifting.ll b/test/InlineAsm/asm_lifting.ll similarity index 100% rename from test/Feature/asm_lifting.ll rename to test/InlineAsm/asm_lifting.ll From 1286b9124858dbdd45417c91ffdf2b9fe49fb6bd Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sat, 1 Jun 2024 16:57:48 +0100 Subject: [PATCH 07/12] Moved variable argument tests to separate directory --- test/{Feature => VarArgs}/FunctionAliasVarArg.c | 0 test/{Feature => VarArgs}/VarArg.c | 0 test/{Feature => VarArgs}/VarArgAlignment.c | 0 test/{Feature => VarArgs}/VarArgByVal.c | 0 test/{Feature => VarArgs}/VarArgByValReported.c | 0 test/{Feature => VarArgs}/VarArgLongDouble.c | 0 6 files changed, 0 insertions(+), 0 deletions(-) rename test/{Feature => VarArgs}/FunctionAliasVarArg.c (100%) rename test/{Feature => VarArgs}/VarArg.c (100%) rename test/{Feature => VarArgs}/VarArgAlignment.c (100%) rename test/{Feature => VarArgs}/VarArgByVal.c (100%) rename test/{Feature => VarArgs}/VarArgByValReported.c (100%) rename test/{Feature => VarArgs}/VarArgLongDouble.c (100%) diff --git a/test/Feature/FunctionAliasVarArg.c b/test/VarArgs/FunctionAliasVarArg.c similarity index 100% rename from test/Feature/FunctionAliasVarArg.c rename to test/VarArgs/FunctionAliasVarArg.c diff --git a/test/Feature/VarArg.c b/test/VarArgs/VarArg.c similarity index 100% rename from test/Feature/VarArg.c rename to test/VarArgs/VarArg.c diff --git a/test/Feature/VarArgAlignment.c b/test/VarArgs/VarArgAlignment.c similarity index 100% rename from test/Feature/VarArgAlignment.c rename to test/VarArgs/VarArgAlignment.c diff --git a/test/Feature/VarArgByVal.c b/test/VarArgs/VarArgByVal.c similarity index 100% rename from test/Feature/VarArgByVal.c rename to test/VarArgs/VarArgByVal.c diff --git a/test/Feature/VarArgByValReported.c b/test/VarArgs/VarArgByValReported.c similarity index 100% rename from test/Feature/VarArgByValReported.c rename to test/VarArgs/VarArgByValReported.c diff --git a/test/Feature/VarArgLongDouble.c b/test/VarArgs/VarArgLongDouble.c similarity index 100% rename from test/Feature/VarArgLongDouble.c rename to test/VarArgs/VarArgLongDouble.c From 3d766e6523d083c9023dab79706205c337a8c171 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sat, 1 Jun 2024 17:08:56 +0100 Subject: [PATCH 08/12] Variadic functions are not currently supported on Apple Silicon --- test/VarArgs/FunctionAliasVarArg.c | 3 +++ test/VarArgs/VarArg.c | 3 +++ test/VarArgs/VarArgAlignment.c | 3 +++ test/VarArgs/VarArgByVal.c | 3 +++ test/VarArgs/VarArgByValReported.c | 3 +++ test/VarArgs/VarArgLongDouble.c | 3 +++ 6 files changed, 18 insertions(+) diff --git a/test/VarArgs/FunctionAliasVarArg.c b/test/VarArgs/FunctionAliasVarArg.c index 423c251669..5098a93fd1 100644 --- a/test/VarArgs/FunctionAliasVarArg.c +++ b/test/VarArgs/FunctionAliasVarArg.c @@ -1,3 +1,6 @@ +// Variadic functions are not currently supported on Apple Silicon +// REQUIRES: not-darwin + // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out -function-alias=printf:highlight_prefix_printf %t.bc 2>&1 | FileCheck --check-prefix=CHECK-HIGHLIGHT %s diff --git a/test/VarArgs/VarArg.c b/test/VarArgs/VarArg.c index 042e565198..42fec8ac73 100644 --- a/test/VarArgs/VarArg.c +++ b/test/VarArgs/VarArg.c @@ -1,3 +1,6 @@ +// Variadic functions are not currently supported on Apple Silicon +// REQUIRES: not-darwin + /* This test needs deterministic allocation with enough spacing between the allocations. Otherwise, if by coincidence the allocated vararg memory object is directly before another valid diff --git a/test/VarArgs/VarArgAlignment.c b/test/VarArgs/VarArgAlignment.c index b6523bf70b..583c0cfd72 100644 --- a/test/VarArgs/VarArgAlignment.c +++ b/test/VarArgs/VarArgAlignment.c @@ -1,3 +1,6 @@ +// Variadic functions are not currently supported on Apple Silicon +// REQUIRES: not-darwin + /* This test is for the alignment of variadic arguments. In particular, on x86 arguments > 8 bytes (long double arguments in test1) should be 16-byte aligned, unless they are passed byval with diff --git a/test/VarArgs/VarArgByVal.c b/test/VarArgs/VarArgByVal.c index d8c753fd37..533c12cca4 100644 --- a/test/VarArgs/VarArgByVal.c +++ b/test/VarArgs/VarArgByVal.c @@ -1,3 +1,6 @@ +// Variadic functions are not currently supported on Apple Silicon +// REQUIRES: not-darwin + /* This test checks that KLEE correctly handles variadic arguments with the byval attribute */ diff --git a/test/VarArgs/VarArgByValReported.c b/test/VarArgs/VarArgByValReported.c index 5a09497a60..00498afd77 100644 --- a/test/VarArgs/VarArgByValReported.c +++ b/test/VarArgs/VarArgByValReported.c @@ -1,3 +1,6 @@ +// Variadic functions are not currently supported on Apple Silicon +// REQUIRES: not-darwin + /* This is the test reported in https://github.com/klee/klee/issues/189, checking the correctness of variadic arguments passed with the byval attribute */ diff --git a/test/VarArgs/VarArgLongDouble.c b/test/VarArgs/VarArgLongDouble.c index b0dff0e847..59492fb386 100644 --- a/test/VarArgs/VarArgLongDouble.c +++ b/test/VarArgs/VarArgLongDouble.c @@ -1,3 +1,6 @@ +// Variadic functions are not currently supported on Apple Silicon +// REQUIRES: not-darwin + // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out %t.bc | FileCheck %s From 2696542459f763aa0fe592f7ab9a27c0aa92e8ad Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sat, 1 Jun 2024 17:27:58 +0100 Subject: [PATCH 09/12] The test currently fails on the macOS version used in the CI: the compiler does not generate a call to __ubsan_handle_invalid_builtin. This seems to be an issue with Clang rather than KLEE. --- test/Feature/ubsan/ubsan_builtin.c | 3 +++ 1 file changed, 3 insertions(+) diff --git a/test/Feature/ubsan/ubsan_builtin.c b/test/Feature/ubsan/ubsan_builtin.c index 54f0b853ea..b400bd687f 100644 --- a/test/Feature/ubsan/ubsan_builtin.c +++ b/test/Feature/ubsan/ubsan_builtin.c @@ -1,3 +1,6 @@ +// The test currently fails on the macOS version used in the CI: the compiler does not generate a call to __ubsan_handle_invalid_builtin. This seems to be an issue with Clang rather than KLEE. +// REQUIRES: not-darwin + // RUN: %clang %s -fsanitize=builtin -w -emit-llvm -g %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s From 34449f23ee1546a9ed88934ab74bde643029b96f Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Sat, 1 Jun 2024 17:48:23 +0100 Subject: [PATCH 10/12] Move test/Feature/ubsan to test/UBSan as for the tests of other features --- test/{Feature/ubsan => UBSan}/ubsan_alignment-assumption.c | 0 .../ubsan => UBSan}/ubsan_alignment-assumption_with_offset.c | 0 test/{Feature/ubsan => UBSan}/ubsan_alignment-type-mismatch.c | 0 test/{Feature/ubsan => UBSan}/ubsan_array_bounds.c | 0 test/{Feature/ubsan => UBSan}/ubsan_bool.c | 0 test/{Feature/ubsan => UBSan}/ubsan_builtin.c | 0 test/{Feature/ubsan => UBSan}/ubsan_enum.cpp | 0 test/{Feature/ubsan => UBSan}/ubsan_float_cast_overflow.c | 0 test/{Feature/ubsan => UBSan}/ubsan_float_divide_by_zero.c | 0 .../{Feature/ubsan => UBSan}/ubsan_implicit_integer_sign_change.c | 0 .../ubsan => UBSan}/ubsan_implicit_signed_integer_truncation.c | 0 .../ubsan => UBSan}/ubsan_implicit_unsigned_integer_truncation.c | 0 test/{Feature/ubsan => UBSan}/ubsan_integer_divide_by_zero.c | 0 test/{Feature/ubsan => UBSan}/ubsan_nonnull_attribute.c | 0 test/{Feature/ubsan => UBSan}/ubsan_null.c | 0 test/{Feature/ubsan => UBSan}/ubsan_nullability_arg.c | 0 test/{Feature/ubsan => UBSan}/ubsan_nullability_assign.c | 0 test/{Feature/ubsan => UBSan}/ubsan_nullability_return.c | 0 ..._pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c | 0 ...inter_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c | 0 ...san_pointer_overflow-applying_nonzero_offset_to_null_pointer.c | 0 .../ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c | 0 .../ubsan => UBSan}/ubsan_pointer_overflow-pointer_arithmetic.c | 0 test/{Feature/ubsan => UBSan}/ubsan_return.cpp | 0 test/{Feature/ubsan => UBSan}/ubsan_returns_nonnull_attribute.c | 0 test/{Feature/ubsan => UBSan}/ubsan_shift_base.c | 0 test/{Feature/ubsan => UBSan}/ubsan_shift_exponent.c | 0 test/{Feature/ubsan => UBSan}/ubsan_signed_integer_overflow.c | 0 test/{Feature/ubsan => UBSan}/ubsan_unreachable.c | 0 test/{Feature/ubsan => UBSan}/ubsan_unsigned_integer_overflow.c | 0 test/{Feature/ubsan => UBSan}/ubsan_unsigned_shift_base.c | 0 test/{Feature/ubsan => UBSan}/ubsan_vla_bound.c | 0 32 files changed, 0 insertions(+), 0 deletions(-) rename test/{Feature/ubsan => UBSan}/ubsan_alignment-assumption.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_alignment-assumption_with_offset.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_alignment-type-mismatch.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_array_bounds.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_bool.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_builtin.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_enum.cpp (100%) rename test/{Feature/ubsan => UBSan}/ubsan_float_cast_overflow.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_float_divide_by_zero.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_implicit_integer_sign_change.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_implicit_signed_integer_truncation.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_implicit_unsigned_integer_truncation.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_integer_divide_by_zero.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_nonnull_attribute.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_null.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_nullability_arg.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_nullability_assign.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_nullability_return.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_pointer_overflow-pointer_arithmetic.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_return.cpp (100%) rename test/{Feature/ubsan => UBSan}/ubsan_returns_nonnull_attribute.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_shift_base.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_shift_exponent.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_signed_integer_overflow.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_unreachable.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_unsigned_integer_overflow.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_unsigned_shift_base.c (100%) rename test/{Feature/ubsan => UBSan}/ubsan_vla_bound.c (100%) diff --git a/test/Feature/ubsan/ubsan_alignment-assumption.c b/test/UBSan/ubsan_alignment-assumption.c similarity index 100% rename from test/Feature/ubsan/ubsan_alignment-assumption.c rename to test/UBSan/ubsan_alignment-assumption.c diff --git a/test/Feature/ubsan/ubsan_alignment-assumption_with_offset.c b/test/UBSan/ubsan_alignment-assumption_with_offset.c similarity index 100% rename from test/Feature/ubsan/ubsan_alignment-assumption_with_offset.c rename to test/UBSan/ubsan_alignment-assumption_with_offset.c diff --git a/test/Feature/ubsan/ubsan_alignment-type-mismatch.c b/test/UBSan/ubsan_alignment-type-mismatch.c similarity index 100% rename from test/Feature/ubsan/ubsan_alignment-type-mismatch.c rename to test/UBSan/ubsan_alignment-type-mismatch.c diff --git a/test/Feature/ubsan/ubsan_array_bounds.c b/test/UBSan/ubsan_array_bounds.c similarity index 100% rename from test/Feature/ubsan/ubsan_array_bounds.c rename to test/UBSan/ubsan_array_bounds.c diff --git a/test/Feature/ubsan/ubsan_bool.c b/test/UBSan/ubsan_bool.c similarity index 100% rename from test/Feature/ubsan/ubsan_bool.c rename to test/UBSan/ubsan_bool.c diff --git a/test/Feature/ubsan/ubsan_builtin.c b/test/UBSan/ubsan_builtin.c similarity index 100% rename from test/Feature/ubsan/ubsan_builtin.c rename to test/UBSan/ubsan_builtin.c diff --git a/test/Feature/ubsan/ubsan_enum.cpp b/test/UBSan/ubsan_enum.cpp similarity index 100% rename from test/Feature/ubsan/ubsan_enum.cpp rename to test/UBSan/ubsan_enum.cpp diff --git a/test/Feature/ubsan/ubsan_float_cast_overflow.c b/test/UBSan/ubsan_float_cast_overflow.c similarity index 100% rename from test/Feature/ubsan/ubsan_float_cast_overflow.c rename to test/UBSan/ubsan_float_cast_overflow.c diff --git a/test/Feature/ubsan/ubsan_float_divide_by_zero.c b/test/UBSan/ubsan_float_divide_by_zero.c similarity index 100% rename from test/Feature/ubsan/ubsan_float_divide_by_zero.c rename to test/UBSan/ubsan_float_divide_by_zero.c diff --git a/test/Feature/ubsan/ubsan_implicit_integer_sign_change.c b/test/UBSan/ubsan_implicit_integer_sign_change.c similarity index 100% rename from test/Feature/ubsan/ubsan_implicit_integer_sign_change.c rename to test/UBSan/ubsan_implicit_integer_sign_change.c diff --git a/test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c b/test/UBSan/ubsan_implicit_signed_integer_truncation.c similarity index 100% rename from test/Feature/ubsan/ubsan_implicit_signed_integer_truncation.c rename to test/UBSan/ubsan_implicit_signed_integer_truncation.c diff --git a/test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c b/test/UBSan/ubsan_implicit_unsigned_integer_truncation.c similarity index 100% rename from test/Feature/ubsan/ubsan_implicit_unsigned_integer_truncation.c rename to test/UBSan/ubsan_implicit_unsigned_integer_truncation.c diff --git a/test/Feature/ubsan/ubsan_integer_divide_by_zero.c b/test/UBSan/ubsan_integer_divide_by_zero.c similarity index 100% rename from test/Feature/ubsan/ubsan_integer_divide_by_zero.c rename to test/UBSan/ubsan_integer_divide_by_zero.c diff --git a/test/Feature/ubsan/ubsan_nonnull_attribute.c b/test/UBSan/ubsan_nonnull_attribute.c similarity index 100% rename from test/Feature/ubsan/ubsan_nonnull_attribute.c rename to test/UBSan/ubsan_nonnull_attribute.c diff --git a/test/Feature/ubsan/ubsan_null.c b/test/UBSan/ubsan_null.c similarity index 100% rename from test/Feature/ubsan/ubsan_null.c rename to test/UBSan/ubsan_null.c diff --git a/test/Feature/ubsan/ubsan_nullability_arg.c b/test/UBSan/ubsan_nullability_arg.c similarity index 100% rename from test/Feature/ubsan/ubsan_nullability_arg.c rename to test/UBSan/ubsan_nullability_arg.c diff --git a/test/Feature/ubsan/ubsan_nullability_assign.c b/test/UBSan/ubsan_nullability_assign.c similarity index 100% rename from test/Feature/ubsan/ubsan_nullability_assign.c rename to test/UBSan/ubsan_nullability_assign.c diff --git a/test/Feature/ubsan/ubsan_nullability_return.c b/test/UBSan/ubsan_nullability_return.c similarity index 100% rename from test/Feature/ubsan/ubsan_nullability_return.c rename to test/UBSan/ubsan_nullability_return.c diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c b/test/UBSan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c similarity index 100% rename from test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c rename to test/UBSan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer.c diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c b/test/UBSan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c similarity index 100% rename from test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c rename to test/UBSan/ubsan_pointer_overflow-applying_nonzero_offset_to_nonnull_pointer_10.c diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c b/test/UBSan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c similarity index 100% rename from test/Feature/ubsan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c rename to test/UBSan/ubsan_pointer_overflow-applying_nonzero_offset_to_null_pointer.c diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c b/test/UBSan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c similarity index 100% rename from test/Feature/ubsan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c rename to test/UBSan/ubsan_pointer_overflow-applying_zero_offset_to_null_pointer.c diff --git a/test/Feature/ubsan/ubsan_pointer_overflow-pointer_arithmetic.c b/test/UBSan/ubsan_pointer_overflow-pointer_arithmetic.c similarity index 100% rename from test/Feature/ubsan/ubsan_pointer_overflow-pointer_arithmetic.c rename to test/UBSan/ubsan_pointer_overflow-pointer_arithmetic.c diff --git a/test/Feature/ubsan/ubsan_return.cpp b/test/UBSan/ubsan_return.cpp similarity index 100% rename from test/Feature/ubsan/ubsan_return.cpp rename to test/UBSan/ubsan_return.cpp diff --git a/test/Feature/ubsan/ubsan_returns_nonnull_attribute.c b/test/UBSan/ubsan_returns_nonnull_attribute.c similarity index 100% rename from test/Feature/ubsan/ubsan_returns_nonnull_attribute.c rename to test/UBSan/ubsan_returns_nonnull_attribute.c diff --git a/test/Feature/ubsan/ubsan_shift_base.c b/test/UBSan/ubsan_shift_base.c similarity index 100% rename from test/Feature/ubsan/ubsan_shift_base.c rename to test/UBSan/ubsan_shift_base.c diff --git a/test/Feature/ubsan/ubsan_shift_exponent.c b/test/UBSan/ubsan_shift_exponent.c similarity index 100% rename from test/Feature/ubsan/ubsan_shift_exponent.c rename to test/UBSan/ubsan_shift_exponent.c diff --git a/test/Feature/ubsan/ubsan_signed_integer_overflow.c b/test/UBSan/ubsan_signed_integer_overflow.c similarity index 100% rename from test/Feature/ubsan/ubsan_signed_integer_overflow.c rename to test/UBSan/ubsan_signed_integer_overflow.c diff --git a/test/Feature/ubsan/ubsan_unreachable.c b/test/UBSan/ubsan_unreachable.c similarity index 100% rename from test/Feature/ubsan/ubsan_unreachable.c rename to test/UBSan/ubsan_unreachable.c diff --git a/test/Feature/ubsan/ubsan_unsigned_integer_overflow.c b/test/UBSan/ubsan_unsigned_integer_overflow.c similarity index 100% rename from test/Feature/ubsan/ubsan_unsigned_integer_overflow.c rename to test/UBSan/ubsan_unsigned_integer_overflow.c diff --git a/test/Feature/ubsan/ubsan_unsigned_shift_base.c b/test/UBSan/ubsan_unsigned_shift_base.c similarity index 100% rename from test/Feature/ubsan/ubsan_unsigned_shift_base.c rename to test/UBSan/ubsan_unsigned_shift_base.c diff --git a/test/Feature/ubsan/ubsan_vla_bound.c b/test/UBSan/ubsan_vla_bound.c similarity index 100% rename from test/Feature/ubsan/ubsan_vla_bound.c rename to test/UBSan/ubsan_vla_bound.c From dd2a2b504907bda1cb96b75cba2e89b2d301ef06 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Tue, 4 Jun 2024 23:01:49 +0200 Subject: [PATCH 11/12] ci: Disable a couple of tests for Apple Silicon --- test/Replay/libkleeruntest/replay_invalid_klee_choose.c | 3 +++ test/UBSan/ubsan_pointer_overflow-pointer_arithmetic.c | 3 +++ 2 files changed, 6 insertions(+) diff --git a/test/Replay/libkleeruntest/replay_invalid_klee_choose.c b/test/Replay/libkleeruntest/replay_invalid_klee_choose.c index 9f114d74d9..352145d9b8 100644 --- a/test/Replay/libkleeruntest/replay_invalid_klee_choose.c +++ b/test/Replay/libkleeruntest/replay_invalid_klee_choose.c @@ -1,3 +1,6 @@ +// FIXME: The test currently fails on Apple Silicon +// REQUIRES: not-darwin + // RUN: %clang -DBOUND_VALUE=32 -DFORCE_VALUE=20 %s -emit-llvm -g %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --search=dfs %t.bc diff --git a/test/UBSan/ubsan_pointer_overflow-pointer_arithmetic.c b/test/UBSan/ubsan_pointer_overflow-pointer_arithmetic.c index 549a9627d9..cc15ecafca 100644 --- a/test/UBSan/ubsan_pointer_overflow-pointer_arithmetic.c +++ b/test/UBSan/ubsan_pointer_overflow-pointer_arithmetic.c @@ -1,3 +1,6 @@ +// FIXME: The test currently fails on Apple Silicon +// REQUIRES: not-darwin + // RUN: %clang %s -fsanitize=pointer-overflow -emit-llvm -g %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --emit-all-errors --ubsan-runtime %t.bc 2>&1 | FileCheck %s From dcec67aec9de2e0ef58d45578e68b572f51474e7 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Tue, 4 Jun 2024 23:24:24 +0200 Subject: [PATCH 12/12] ci: Fix cirrus ci --- .cirrus.yml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/.cirrus.yml b/.cirrus.yml index 04451afda4..8cf8a8383f 100644 --- a/.cirrus.yml +++ b/.cirrus.yml @@ -6,13 +6,13 @@ task: deps_script: - sed -i.bak -e 's/quarterly/latest/' /etc/pkg/FreeBSD.conf - env ASSUME_ALWAYS_YES=yes pkg update -f - - env ASSUME_ALWAYS_YES=yes pkg install -y llvm11 gmake z3 cmake pkgconf google-perftools python3 py39-sqlite3 py39-tabulate nlohmann-json bash coreutils immer + - env ASSUME_ALWAYS_YES=yes pkg install -y llvm13 gmake z3 cmake pkgconf google-perftools python3 py311-sqlite3 py311-tabulate nlohmann-json bash coreutils immer build_script: - mkdir build - cd build - - cmake -DLLVM_DIR=/usr/local/llvm11 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DIMMER_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON .. + - cmake -DLLVM_DIR=/usr/local/llvm13 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_SRC_DIR=/usr/local -DIMMER_SRC_DIR=/usr/local -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON .. - gmake test_script: - - sed -i.bak -e 's/lit\./lit11\./' test/lit.cfg + - sed -i.bak -e 's/lit\./lit13\./' test/lit.cfg - cd build - gmake check