From 0d59bdc426c8a01536f79bdc4be0184e3c3447b2 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhik Date: Sun, 31 Dec 2023 02:09:40 +0400 Subject: [PATCH 1/6] [fix] Fix the template argument --- include/klee/ADT/Incremental.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/include/klee/ADT/Incremental.h b/include/klee/ADT/Incremental.h index 6f16fd0867..d5a77defa8 100644 --- a/include/klee/ADT/Incremental.h +++ b/include/klee/ADT/Incremental.h @@ -192,7 +192,7 @@ class inc_uset { } }; - using idMap = std::unordered_map<_Value, MinFrameIds, _Hash, _Pred, _Alloc>; + using idMap = std::unordered_map<_Value, MinFrameIds, _Hash, _Pred>; using citerator = typename idMap::const_iterator; idMap ids; FrameId current_frame = 0; @@ -302,7 +302,7 @@ template , class inc_umap { private: std::unordered_map<_Key, _Tp, _Hash, _Pred, _Alloc> map; - using idMap = std::unordered_map<_Key, FrameIds, _Hash, _Pred, _Alloc>; + using idMap = std::unordered_map<_Key, FrameIds, _Hash, _Pred>; idMap ids; FrameId current_frame = 0; From fb329ebd0ad4f8565a8ee2cd75942b0c51ef8e11 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhik Date: Sun, 31 Dec 2023 02:12:57 +0400 Subject: [PATCH 2/6] [fix] Add arm float constants --- runtime/klee-fp/fenv.c | 19 ------------------- runtime/klee-fp/fenv.h | 29 ++++++++++++++++++++++++++++- runtime/klee-fp/log.c | 3 +-- 3 files changed, 29 insertions(+), 22 deletions(-) diff --git a/runtime/klee-fp/fenv.c b/runtime/klee-fp/fenv.c index 0a70f90f34..c5dda37789 100644 --- a/runtime/klee-fp/fenv.c +++ b/runtime/klee-fp/fenv.c @@ -9,25 +9,6 @@ #include "fenv.h" #include "klee/klee.h" -// Define the constants. Don't include `fenv.h` here to avoid -// polluting the Intrinsic module. -#if defined(__x86_64__) || defined(__i386__) -// These are the constants used by glibc and musl for x86_64 and i386 -enum { - FE_TONEAREST = 0, - FE_DOWNWARD = 0x400, - FE_UPWARD = 0x800, - FE_TOWARDZERO = 0xc00, - - // Our own implementation defined values. - // Do we want this? Although it's allowed by - // the standard it won't be replayable on native - // binaries. -}; -#else -#error Architecture not supported -#endif - int fegetround(void) { enum KleeRoundingMode rm = klee_get_rounding_mode(); switch (rm) { diff --git a/runtime/klee-fp/fenv.h b/runtime/klee-fp/fenv.h index 3cb7728f20..a833ac75c1 100644 --- a/runtime/klee-fp/fenv.h +++ b/runtime/klee-fp/fenv.h @@ -9,7 +9,34 @@ #ifndef KLEE_FENV_H #define KLEE_FENV_H -#include "klee/klee.h" + +#if defined(__x86_64__) || defined(__i386__) +#include +#elif defined(__arm64__) || defined(__arm__) +enum { + FE_TONEAREST = 0x0, + FE_UPWARD = 0x1, + FE_DOWNWARD = 0x2, + FE_TOWARDZERO = 0x3, + + // Our own implementation defined values. + // Do we want this? Although it's allowed by + // the standard it won't be replayable on native + // binaries. +}; +enum { + FE_INVALID = 0x01, + FE_DIVBYZERO = 0x02, + FE_OVERFLOW = 0x04, + FE_UNDERFLOW = 0x08, + FE_INEXACT = 0x10, + FE_DENORMAL = 0x80, + FE_ALL_EXCEPT = FE_DIVBYZERO | FE_INEXACT | FE_INVALID | FE_OVERFLOW | + FE_UNDERFLOW | FE_DENORMAL +}; +#else +#error Architecture not supported +#endif int fegetround(void); int fesetround(int rm); diff --git a/runtime/klee-fp/log.c b/runtime/klee-fp/log.c index 77f3d3a12f..62d54db47b 100644 --- a/runtime/klee-fp/log.c +++ b/runtime/klee-fp/log.c @@ -8,9 +8,8 @@ //===----------------------------------------------------------------------===*/ #include "fenv.h" -#include "math.h" -#include +#include #define LOG_CORNER_CASE(suffix, type, isnan_function) \ int log_corner_case_##suffix(type *x) { \ From 73467f454de850a8c458786e1e9de926c3846fd3 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhik Date: Sun, 31 Dec 2023 17:20:39 +0400 Subject: [PATCH 3/6] [chore] Disable tests with uint128 type on not-x86_64 targets --- test/Feature/uint128.c | 1 + test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c | 1 + test/lit.cfg | 1 + 3 files changed, 3 insertions(+) diff --git a/test/Feature/uint128.c b/test/Feature/uint128.c index efa5915beb..98676474c7 100644 --- a/test/Feature/uint128.c +++ b/test/Feature/uint128.c @@ -1,3 +1,4 @@ +// REQUIRES: target-x86_64 // RUN: %clang %s -emit-llvm %O0opt -c -g -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out %t1.bc 2>&1 | FileCheck %s diff --git a/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c b/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c index f0261d2008..4b2d6b79fc 100644 --- a/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c +++ b/test/Industry/CoverageErrorCall/btor2c-lazyMod.mul6.c @@ -1,5 +1,6 @@ // It requires bitwuzla because the script currently runs with bitwuzla solver backend // REQUIRES: bitwuzla +// REQUIRES: target-x86_64 // RUN: %kleef --property-file=%S/coverage-error-call.prp --max-memory=7000000000 --max-cputime-soft=30 --64 --write-ktests %s 2>&1 | FileCheck %s // CHECK: KLEE: WARNING: 100.00% Reachable Reachable diff --git a/test/lit.cfg b/test/lit.cfg index d2af70f065..8ccd841160 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -260,6 +260,7 @@ else: # m32 support config.available_features.add('{}target-x86'.format('' if config.target_triple.find("i386") != -1 else 'not-')) +config.available_features.add('{}target-x86_64'.format('' if config.target_triple.find("x86_64") != -1 else 'not-')) config.available_features.add('{}32bit-support'.format('' if config.have_32bit_support else 'not-')) From 14882fce509a073a2186c97a5bb97dabc4bda0a3 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhik Date: Wed, 3 Jan 2024 17:35:11 +0400 Subject: [PATCH 4/6] [fix] Disable test on darwin due to stack overflow --- test/ArrayOpt/test_nier.c | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/test/ArrayOpt/test_nier.c b/test/ArrayOpt/test_nier.c index 154f72d854..55ecac126f 100644 --- a/test/ArrayOpt/test_nier.c +++ b/test/ArrayOpt/test_nier.c @@ -1,5 +1,6 @@ // REQUIRES: not-asan // REQUIRES: not-msan +// REQUIRES: not-darwin // Ignore msan: Generates a large stack trace > 8k but not a stack overflow for larger stacks // RUN: %clang %s -emit-llvm %O0opt -c -o %t.bc // RUN: rm -rf %t.klee-out @@ -18,8 +19,8 @@ // RUN: %klee --write-kqueries --output-dir=%t.klee-out --optimize-array=all %t.bc 2>&1 | FileCheck %s -check-prefix=CHECK -check-prefix=CHECK-OPT_I // RUN: test -f %t.klee-out/test000001.kquery // RUN: test -f %t.klee-out/test000002.kquery -// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR // RUN: not FileCheck %s -input-file=%t.klee-out/test000002.kquery -check-prefix=CHECK-CONST_ARR +// RUN: not FileCheck %s -input-file=%t.klee-out/test000001.kquery -check-prefix=CHECK-CONST_ARR // CHECK-OPT_I: KLEE: WARNING: OPT_I: successful // CHECK-OPT_V: KLEE: WARNING: OPT_V: successful From 39bd3e492d97a0a583d61a61d031af78db7798be Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhik Date: Thu, 4 Jan 2024 19:27:33 +0400 Subject: [PATCH 5/6] [ci] Update `.cirrus.yml` --- .cirrus.yml | 8 ++++---- include/klee-test-comp.c | 12 ++++++++++++ lib/Core/Executor.cpp | 2 +- runtime/POSIX/input_output.c | 18 ++++++++++++++++++ scripts/build/p-klee-linux-ubuntu.inc | 1 + scripts/build/p-klee-osx.inc | 1 + scripts/replay.sh | 13 ++++++++++--- .../ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c | 7 ++++--- .../Industry/CoverageBranches/CostasArray-17.c | 11 ++++++----- .../CoverageBranches/egcd3-ll_valuebound10.c | 11 ++++++----- test/Industry/CoverageBranches/lit.local.cfg | 2 +- test/Industry/CoverageBranches/matrix-2-2.c | 10 +++++----- ...cr.3.ufo.UNBOUNDED.pals+Problem12_label00.c | 12 ++++++------ test/Industry/egcd3-ll_valuebound10.c | 10 +++++----- test/Solver/CallComputeValue.c | 4 ++-- test/lit.cfg | 9 +++++++++ test/regression/2023-03-27-lib-function.c | 8 ++++++-- 17 files changed, 97 insertions(+), 42 deletions(-) diff --git a/.cirrus.yml b/.cirrus.yml index 828f667364..c0c113987c 100644 --- a/.cirrus.yml +++ b/.cirrus.yml @@ -1,16 +1,16 @@ task: freebsd_instance: matrix: - - image_family: freebsd-12-3-snap - - image_family: freebsd-13-1-snap + - image_family: freebsd-13-2-snap + - image_family: freebsd-14-0-snap 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 + - env ASSUME_ALWAYS_YES=yes pkg install -y llvm11 gmake z3 cmake pkgconf google-perftools python3 py39-sqlite3 py39-tabulate nlohmann-json bash coreutils build_script: - mkdir build - cd build - - cmake -DLLVM_DIR=/usr/local/llvm11 -DMAKE_BINARY=/usr/local/bin/gmake -DENABLE_TCMALLOC:BOOL=true -DENABLE_POSIX_RUNTIME:BOOL=ON -DENABLE_SOLVER_Z3:BOOL=true -DENABLE_SYSTEM_TESTS:BOOL=ON .. + - cmake -DLLVM_DIR=/usr/local/llvm11 -DMAKE_BINARY=/usr/local/bin/gmake -DJSON_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 diff --git a/include/klee-test-comp.c b/include/klee-test-comp.c index 34e805e588..3013b7d669 100644 --- a/include/klee-test-comp.c +++ b/include/klee-test-comp.c @@ -22,6 +22,18 @@ void __assert_fail(const char *assertion, const char *file, unsigned int line, void klee_prefer_cex(void *, uintptr_t); #endif +#if defined(__APPLE__) || defined(__FreeBSD__) +#include + +extern void abort(void); +void __assert_fail(const char *failedexpr, const char *file, unsigned int line, + const char *fn) { + warnx("assertion \"%s\" failed: file \"%s\", line %u%s%s%s", failedexpr, file, + line, fn ? ", function: \"" : "", fn ? fn : "", fn ? "\"" : ""); + abort(); +} +#endif + int __VERIFIER_nondet_int(void) { int x; klee_make_symbolic(&x, sizeof(x), "int"); diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index de6a5bef3f..575e8299cd 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -161,7 +161,7 @@ cl::opt UseTypeBasedAliasAnalysis( cl::opt AlignSymbolicPointers("align-symbolic-pointers", cl::desc("Makes symbolic pointers aligned according" - "to the used type system (default=true)"), + "to the used type system (default=false)"), cl::init(false), cl::cat(ExecCat)); cl::opt diff --git a/runtime/POSIX/input_output.c b/runtime/POSIX/input_output.c index afed9e3d0d..14daa68af8 100644 --- a/runtime/POSIX/input_output.c +++ b/runtime/POSIX/input_output.c @@ -2,6 +2,7 @@ #include #include #include +#include /* * Return the (stdio) flags for a given mode. Store the flags @@ -53,8 +54,13 @@ FILE *fopen(const char *file, const char *mode) { if ((f = open(file, oflags)) < 0) return NULL; } +#ifndef __FreeBSD__ fp->_fileno = f; fp->_mode = oflags; +#else + fp->_file = f; + fp->_flags = oflags; +#endif return fp; } @@ -68,7 +74,11 @@ int get_file_descriptor(FILE *stream) { if (stream == stderr) { return 2; } +#ifndef __FreeBSD__ return stream->_fileno; +#else + return stream->_file; +#endif } int fgetc(FILE *stream) { @@ -86,6 +96,7 @@ int fgetc(FILE *stream) { } } +#ifndef __FreeBSD__ int getc(FILE *stream) { if (stream == NULL) { return 0; @@ -100,6 +111,7 @@ int getc(FILE *stream) { return EOF; } } +#endif size_t fread(void *buffer, size_t size, size_t count, FILE *stream) { if (stream == NULL) { @@ -137,7 +149,9 @@ char *fgets(char *s, int n, FILE *stream) { return s; } +#ifndef __FreeBSD__ int getchar(void) { return getc(stdin); } +#endif char *gets(char *s) { char *p = s; @@ -174,6 +188,7 @@ int fputc(int c, FILE *stream) { } } +#ifndef __FreeBSD__ int putc(int c, FILE *stream) { if (stream == NULL) { return 0; @@ -188,6 +203,7 @@ int putc(int c, FILE *stream) { return EOF; } } +#endif size_t fwrite(const void *buffer, size_t size, size_t count, FILE *stream) { if (stream == NULL) { @@ -221,7 +237,9 @@ int fputs(const char *str, FILE *stream) { return 1; } +#ifndef __FreeBSD__ int putchar(int c) { return putc(c, stdout); } +#endif int puts(const char *str) { int write_code = fputs(str, stdout); diff --git a/scripts/build/p-klee-linux-ubuntu.inc b/scripts/build/p-klee-linux-ubuntu.inc index a67a061615..70af8dc110 100644 --- a/scripts/build/p-klee-linux-ubuntu.inc +++ b/scripts/build/p-klee-linux-ubuntu.inc @@ -12,6 +12,7 @@ install_build_dependencies_klee() { python3-wheel pkg-config cmake-data + coreutils ) if [[ "${SOLVERS:-}" == "metaSMT" ]]; then diff --git a/scripts/build/p-klee-osx.inc b/scripts/build/p-klee-osx.inc index 4f5b063599..12893fbbb4 100644 --- a/scripts/build/p-klee-osx.inc +++ b/scripts/build/p-klee-osx.inc @@ -10,6 +10,7 @@ install_build_dependencies_klee() { pip3 install --user --upgrade lit tabulate brew install pkg-config + brew install coreutils # Get path of package location base_path=$(python3 -m site --user-base) export PATH="${base_path}/bin:$PATH" diff --git a/scripts/replay.sh b/scripts/replay.sh index 2673c91e4a..4b1f4b8cc4 100755 --- a/scripts/replay.sh +++ b/scripts/replay.sh @@ -9,6 +9,13 @@ # # ===----------------------------------------------------------------------===## -for f in `find $1 -name "*.ktest" -type f`; do - KLEE_RUN_TEST_ERRORS_NON_FATAL=STOP KTEST_FILE=$f timeout 1 $2 -done +if [[ "$OSTYPE" == "linux-gnu"* ]]; then + for f in `find $1 -name "*.ktest" -type f`; do + KLEE_RUN_TEST_ERRORS_NON_FATAL=STOP KTEST_FILE=$f timeout 1 $2 + done +else + for f in `find $1 -name "*.ktest" -type f`; do + KLEE_RUN_TEST_ERRORS_NON_FATAL=STOP KTEST_FILE=$f gtimeout 1 $2 + done +fi +exit 0 diff --git a/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c b/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c index fff21e4d2b..fe61b84c59 100644 --- a/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c +++ b/test/Industry/CoverageBranches/ChenFlurMukhopadhyay-2012SAS-Fig1-alloca.c @@ -2,20 +2,21 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --delete-dead-loops=false --use-forked-solver=false -max-memory=6008 --cex-cache-validity-cores --only-output-states-covering-new=true --dump-states-on-halt=all %t1.bc 2>&1 | FileCheck -check-prefix=CHECK %s -// RUN: rm -f %t*.gcda %t*.gcno %t*.gcov +// RUN: rm -f ./%gcov-files-path*.gcda ./%gcov-files-path*.gcno ./%gcov-files-path*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage // RUN: %replay %t.klee-out %t_runner -// RUN: gcov -b %t_runner-%basename_t > %t.cov.log +// RUN: gcov -b %gcov-files-path > %t.cov.log // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK-COV %s // Branch coverage 100%, the number of branches is 2: -// CHECK-COV: Lines executed:100.00% of 11 +// CHECK-COV: Lines executed:100.00% of 1{{1|2}} // CHECK-COV-NEXT: Branches executed:100.00% of 2 // CHECK-COV-NEXT: Taken at least once:100.00% of 2 #include "klee-test-comp.c" +#define alloca(size) __builtin_alloca (size) extern int __VERIFIER_nondet_int(void); int main() { diff --git a/test/Industry/CoverageBranches/CostasArray-17.c b/test/Industry/CoverageBranches/CostasArray-17.c index 6f2bcea325..7fc3bafe93 100644 --- a/test/Industry/CoverageBranches/CostasArray-17.c +++ b/test/Industry/CoverageBranches/CostasArray-17.c @@ -2,25 +2,25 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --optimize-aggressive --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=all --search=dfs %t1.bc -// RUN: rm -f %t*.gcda %t*.gcno %t*.gcov +// RUN: rm -f ./%gcov-files-path*.gcda ./%gcov-files-path*.gcno ./%gcov-files-path*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage // RUN: %replay %t.klee-out %t_runner -// RUN: gcov -b %t_runner-%basename_t > %t.cov.log +// RUN: gcov -b %gcov-files-path > %t.cov.log // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --optimize=true --emit-all-errors --only-output-states-covering-new=true --dump-states-on-halt=all --search=dfs %t1.bc -// RUN: rm -f %t*.gcda %t*.gcno %t*.gcov +// RUN: rm -f ./%gcov-files-path*.gcda ./%gcov-files-path*.gcno ./%gcov-files-path*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage // RUN: %replay %t.klee-out %t_runner -// RUN: gcov -b %t_runner-%basename_t > %t.cov.log +// RUN: gcov -b %gcov-files-path > %t.cov.log // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s // Branch coverage 100%, the number of branches is 2: -// CHECK: Lines executed:{{(0\.7[0-9])}}% of 1545 +// CHECK: Lines executed:{{(0\.7[0-9])|(99\.94)}}% of 1545 // CHECK-NEXT: Branches executed:100.00% of 2 // CHECK-NEXT: Taken at least once:100.00% of 2 @@ -44,6 +44,7 @@ int __VERIFIER_nondet_int(); #ifdef GCOV extern void __gcov_dump(void); +extern void exit(int exit_code) __attribute__((noreturn)); #endif void abort_prog() { diff --git a/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c b/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c index 9d433194b3..a3846f9ec0 100644 --- a/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c +++ b/test/Industry/CoverageBranches/egcd3-ll_valuebound10.c @@ -2,22 +2,23 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state %t1.bc -// RUN: rm -f %t*.gcda %t*.gcno %t*.gcov +// RUN: rm -f ./%gcov-files-path*.gcda ./%gcov-files-path*.gcno ./%gcov-files-path*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage // RUN: %replay %t.klee-out %t_runner -// RUN: gcov -b %t_runner-%basename_t > %t.cov.log +// RUN: gcov -b %gcov-files-path > %t.cov.log // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s -// CHECK: Lines executed:87.93% of 58 -// CHECK-NEXT: Branches executed:100.00% of 18 -// CHECK-NEXT: Taken at least once:83.33% of 18 +// CHECK: Lines executed:{{87\.93|89\.83}}% of 5{{8|9}} +// CHECK-NEXT: Branches executed:100.00% of 1{{8|4}} +// CHECK-NEXT: Taken at least once:{{83\.33|85\.71}}% of 1{{8|4}} #include "klee-test-comp.c" /* extended Euclid's algorithm */ extern void abort(void); #ifdef GCOV extern void __gcov_dump(void); +extern void exit( int exit_code ) __attribute__((noreturn)); #endif void dump() { diff --git a/test/Industry/CoverageBranches/lit.local.cfg b/test/Industry/CoverageBranches/lit.local.cfg index ad131f8f64..95cecce749 100644 --- a/test/Industry/CoverageBranches/lit.local.cfg +++ b/test/Industry/CoverageBranches/lit.local.cfg @@ -4,5 +4,5 @@ def getRoot(config): return getRoot(config.parent) rootConfig = getRoot(config) -if config.have_asan or config.have_ubsan or config.have_msan or config.target_triple.find("darwin") != -1: +if config.have_asan or config.have_ubsan or config.have_msan: config.unsupported = True diff --git a/test/Industry/CoverageBranches/matrix-2-2.c b/test/Industry/CoverageBranches/matrix-2-2.c index 6170da72fe..879b4560ac 100644 --- a/test/Industry/CoverageBranches/matrix-2-2.c +++ b/test/Industry/CoverageBranches/matrix-2-2.c @@ -2,24 +2,24 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=all --max-cycles=2 --optimize=true --emit-all-errors --delete-dead-loops=false --use-forked-solver=false -max-memory=6008 --cex-cache-validity-cores --only-output-states-covering-new=true --dump-states-on-halt=all --use-sym-size-alloc=true --symbolic-allocation-threshold=8192 %t1.bc 2>&1 -// RUN: rm -f %t*.gcda %t*.gcno %t*.gcov +// RUN: rm -f ./%gcov-files-path*.gcda ./%gcov-files-path*.gcno ./%gcov-files-path*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage // RUN: %replay %t.klee-out %t_runner -// RUN: gcov -b %t_runner-%basename_t > %t.cov.log +// RUN: gcov -b %gcov-files-path > %t.cov.log // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK-COV %s // Branch coverage is greater 80%: -// CHECK-COV: Lines executed:9{{([0-9]\.[0-9][0-9])}}% of 24 +// CHECK-COV: Lines executed:{{(9[0-9]\.[0-9][0-9])|(100\.00)}}% of 2{{4|5}} // CHECK-COV-NEXT: Branches executed:100.00% of 16 -// CHECK-COV-NEXT: Taken at least once:{{([8-9][0-9]\.[0-9][0-9])}}% of 16 +// CHECK-COV-NEXT: Taken at least once:{{([8-9][0-9]\.[0-9][0-9])|(100\.00)}}% of 16 #include "klee-test-comp.c" -extern void exit(int); extern void abort(void); #ifdef GCOV extern void __gcov_dump(void); +extern void exit(int); #endif void dump() { diff --git a/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c b/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c index c1fc602469..5e7399e6ee 100644 --- a/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c +++ b/test/Industry/CoverageBranches/pals_lcr.3.ufo.UNBOUNDED.pals+Problem12_label00.c @@ -1,18 +1,17 @@ -// REQUIRES: z3 // RUN: %clang %s -emit-llvm %O0opt -g -c -o %t1.bc // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --optimize-aggressive=false --track-coverage=branches --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=3s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state --use-iterative-deepening-search=max-cycles --max-cycles=4 %t1.bc -// RUN: rm -f %t*.gcda %t*.gcno %t*.gcov +// RUN: rm -f ./%gcov-files-path*.gcda ./%gcov-files-path*.gcno ./%gcov-files-path*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage // RUN: %replay %t.klee-out %t_runner -// RUN: gcov -b %t_runner-%basename_t > %t.cov.log +// RUN: gcov -b %gcov-files-path > %t.cov.log // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s -// CHECK: Lines executed:{{(9[0-9]\.[0-9][0-9])}}% of 4114 -// CHECK-NEXT: Branches executed:{{(9[0-9]\.[0-9][0-9])}}% of 13404 -// CHECK-NEXT: Taken at least once:{{(8[0-9]\.[0-9][0-9])}}% of 13404 +// CHECK: Lines executed:{{(9[0-9]\.[0-9][0-9])}}% of 41{{(1|5)(3|4)}} +// CHECK-NEXT: Branches executed:{{(9[0-9]\.[0-9][0-9])}}% of {{13404|11628}} +// CHECK-NEXT: Taken at least once:{{([8-9][0-9]\.[0-9][0-9])}}% of {{13404|11628}} // This file is part of the SV-Benchmarks collection of verification tasks: // https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks @@ -35,6 +34,7 @@ extern void exit(int); extern void abort(void); #ifdef GCOV extern void __gcov_dump(void); +extern void exit(int exit_code) __attribute__((noreturn)); #endif void dump() { diff --git a/test/Industry/egcd3-ll_valuebound10.c b/test/Industry/egcd3-ll_valuebound10.c index 5811f1f44d..bc6c06f982 100644 --- a/test/Industry/egcd3-ll_valuebound10.c +++ b/test/Industry/egcd3-ll_valuebound10.c @@ -3,17 +3,17 @@ // RUN: rm -rf %t.klee-out // RUN: %klee --output-dir=%t.klee-out --delete-dead-loops=false --emit-all-errors --mock-all-externals --use-forked-solver=false --max-memory=6008 --optimize --skip-not-lazy-initialized --output-source=false --output-stats=true --output-istats=true -istats-write-interval=90s --use-sym-size-alloc=true --cex-cache-validity-cores --symbolic-allocation-threshold=8192 --max-solver-time=5s --track-coverage=branches --use-iterative-deepening-search=max-cycles --cover-on-the-fly=false --delay-cover-on-the-fly=400000 --only-output-states-covering-new --dump-states-on-halt=all --search=dfs --search=random-state %t1.bc -// RUN: rm -f %t*.gcda %t*.gcno %t*.gcov +// RUN: rm -f ./%gcov-files-path*.gcda ./%gcov-files-path*.gcno ./%gcov-files-path*.gcov // RUN: %cc -DGCOV %s %libkleeruntest -Wl,-rpath %libkleeruntestdir -o %t_runner --coverage // RUN: %replay %t.klee-out %t_runner -// RUN: gcov -b %t_runner-%basename_t > %t.cov.log +// RUN: gcov -b %gcov-files-path > %t.cov.log // RUN: FileCheck --input-file=%t.cov.log --check-prefix=CHECK %s // Branch coverage 100%, the number of branches is 1: -// CHECK: Lines executed:87.93% of 58 -// CHECK-NEXT: Branches executed:100.00% of 18 -// CHECK-NEXT: Taken at least once:83.33% of 18 +// CHECK: Lines executed:{{(8[0-9]\.[0-9][0-9])}}% of 5{{8|9}} +// CHECK-NEXT: Branches executed:100.00% of 1{{8|4}} +// CHECK-NEXT: Taken at least once:{{(8[0-9]\.[0-9][0-9])}}% of 1{{8|4}} #include "klee-test-comp.c" /* extended Euclid's algorithm */ diff --git a/test/Solver/CallComputeValue.c b/test/Solver/CallComputeValue.c index 3e0dbe408f..36ca85cf1e 100644 --- a/test/Solver/CallComputeValue.c +++ b/test/Solver/CallComputeValue.c @@ -1,7 +1,7 @@ // REQUIRES: z3 // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --search=bfs --solver-backend=z3-tree --max-solvers-approx-tree-inc=4 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false %t1.bc 2>&1 | FileCheck %s +// RUN: %klee --output-dir=%t.klee-out --search=bfs --solver-backend=z3-tree --max-solvers-approx-tree-inc=4 --debug-crosscheck-core-solver=z3 --debug-z3-validate-models --debug-assignment-validating-solver --use-cex-cache=false --use-lazy-initialization=only %t1.bc 2>&1 | FileCheck %s #include "klee/klee.h" @@ -17,5 +17,5 @@ int main() { return 2; } -// CHECK: KLEE: done: completed paths = 17 +// CHECK: KLEE: done: completed paths = {{3|5}} // CHECK: KLEE: done: partially completed paths = 0 diff --git a/test/lit.cfg b/test/lit.cfg index 8ccd841160..55adadf5cc 100644 --- a/test/lit.cfg +++ b/test/lit.cfg @@ -173,6 +173,15 @@ config.substitutions.append( config.substitutions.append( ('%libcxx_include', getattr(config, 'libcxx_include_dir', None))) +if config.target_triple.find("darwin") != -1: + config.substitutions.append( + ('%gcov-files-path', '%basename_t') + ) +else: + config.substitutions.append( + ('%gcov-files-path', '%t_runner-%basename_t') + ) + # Add feature for the LLVM version in use, so it can be tested in REQUIRES and # XFAIL checks. We also add "not-XXX" variants, for the same reason. known_llvm_versions = { "9.0", "10.0", "11.0", "11.1", "12.0", "13.0", "14.0" } diff --git a/test/regression/2023-03-27-lib-function.c b/test/regression/2023-03-27-lib-function.c index 4754267431..90df4b41a4 100644 --- a/test/regression/2023-03-27-lib-function.c +++ b/test/regression/2023-03-27-lib-function.c @@ -11,6 +11,10 @@ #include #include +#ifdef __FreeBSD__ +#include +#endif + #ifdef INET_NTOP const char *inet_ntop(int af, const void *restrict src, char *restrict dst, socklen_t size) { @@ -22,8 +26,8 @@ const char *inet_ntop(int af, const void *restrict src, int main(int argc, char **argv) { inet_ntop(0, 0, 0, 0); - // CHECK_INTERNAL-NOT: calling external: inet_ntop - // CHECK_EXTERNAL: calling external: inet_ntop + // CHECK_INTERNAL-NOT: calling external: {{inet_ntop|__inet_ntop}} + // CHECK_EXTERNAL: calling external: {{inet_ntop|__inet_ntop}} #ifdef INET_PTON struct in_addr inaddr; inet_pton(AF_INET, "10.1.0.29", &inaddr); From be56ae2227a728b794b7e6166a4cfc2413f8bb30 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhik Date: Thu, 18 Jan 2024 01:40:56 +0400 Subject: [PATCH 6/6] [fix] Use `find -exec` --- scripts/replay.sh | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/scripts/replay.sh b/scripts/replay.sh index 4b1f4b8cc4..8a4a426efb 100755 --- a/scripts/replay.sh +++ b/scripts/replay.sh @@ -10,12 +10,9 @@ # ===----------------------------------------------------------------------===## if [[ "$OSTYPE" == "linux-gnu"* ]]; then - for f in `find $1 -name "*.ktest" -type f`; do - KLEE_RUN_TEST_ERRORS_NON_FATAL=STOP KTEST_FILE=$f timeout 1 $2 - done + TIMEOUT="timeout" else - for f in `find $1 -name "*.ktest" -type f`; do - KLEE_RUN_TEST_ERRORS_NON_FATAL=STOP KTEST_FILE=$f gtimeout 1 $2 - done + TIMEOUT="gtimeout" fi +find $1 -name "*.ktest" -type f -exec bash -c 'KLEE_RUN_TEST_ERRORS_NON_FATAL=STOP KTEST_FILE=$1 $3 1 $2' bash {} $2 $TIMEOUT \; exit 0