Fix cirrus-ci

.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

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 <err.h>
+
+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");

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 <typename _Key, typename _Tp, typename _Hash = std::hash<_Key>,
 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;
 

lib/Core/Executor.cpp

@@ -161,7 +161,7 @@ cl::opt<bool> UseTypeBasedAliasAnalysis(
 cl::opt<bool>
     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<bool>

runtime/POSIX/input_output.c

@@ -2,6 +2,7 @@
 #include <fcntl.h>
 #include <stdio.h>
 #include <stdlib.h>
+#include <sys/stat.h>
 
 /*
  * 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);

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) {

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 <fenv.h>
+#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);

runtime/klee-fp/log.c

@@ -8,9 +8,8 @@
 //===----------------------------------------------------------------------===*/
 
 #include "fenv.h"
-#include "math.h"
 
-#include <fenv.h>
+#include <math.h>
 
 #define LOG_CORNER_CASE(suffix, type, isnan_function)                          \
   int log_corner_case_##suffix(type *x) {                                      \

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

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"

scripts/replay.sh

@@ -9,6 +9,10 @@
 # 
 # ===----------------------------------------------------------------------===##
 
-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
+  TIMEOUT="timeout"
+else
+  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

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

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

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() {

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() {

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() {

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