Fix macos ci (#201)

* Use a virtual environment for Python3 while testing under MacOS

With Python3.12, brew requires a virtualenv for external python packages.
Setup and use such an environment for testing under MacOS.

While there is a `tabulate` package in brew, installing it won't install the library only the command line tool `tabulate`.
Therefore, we install `tabulate` via `pip install`.

Remove unnecessary package upgrade.

* Fix bug in PATH cleaning, more robust installation detection

The previous implementation gobbled up the first entry of the PATH by interpreting the second argument as pattern.
New implementation avoids this and is more robust in detecting existing KLEE installations.

* Mark variadic argument tests as requiring x86_64

* Update VarArgByValOld.c

---------

Co-authored-by: Martin Nowack <m.nowack@imperial.ac.uk>

Author: misonijnik

.github/workflows/build.yaml

@@ -168,13 +168,13 @@ jobs:
       - name: Install newer version of Bash
         run: brew install bash
       - name: Checkout KLEE source code
-        uses: actions/checkout@v3
-        with:
-          submodules: recursive
+        uses: actions/checkout@v4
+      - name: Create virtualenv for Python3 (PEP 668)
+        run:  python3 -m venv .venv
       - name: Build KLEE
-        run: scripts/build/build.sh klee --debug --install-system-deps
+        run:  source .venv/bin/activate && echo "$(which tabulate)" && scripts/build/build.sh klee --debug --install-system-deps
       - name: Run tests
-        run: scripts/build/run-tests.sh /tmp/klee_build* --debug
+        run:  source .venv/bin/activate && scripts/build/run-tests.sh /tmp/klee_build* --debug
 
   Docker:
     runs-on: ubuntu-latest

scripts/build/p-klee-osx.inc

@@ -1,17 +1,15 @@
 # Build dependencies
 install_build_dependencies_klee() {
-  brew upgrade python               # upgrade to Python 3
-  brew link --overwrite python
-
   if [[ $(to_bool "${ENABLE_DOXYGEN}") -eq 1 ]]; then
     brew install doxygen graphviz
   fi
 
-  brew install python-tabulate lit
+  # Install `lit` required for testing
+  brew install lit
 
   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"
-}
+
+  # Install package in virtual environment
+  python3 -m pip install "tabulate"
+}

scripts/build/run-tests.sh

@@ -37,10 +37,14 @@ run_tests() {
   # TODO change to pinpoint specific directory
   cd "${build_dir}"
 
-  # Remove klee from PATH
-  export PATH=${PATH/":/home/klee/klee_build/bin"/}
+  # Remove klee from PATH. The goal is that for test cases klee is referenced via `%klee` not accidently being picked up via PATH
   if which klee; then
-    return 1 # should not happen
+    full_path_to_klee="$(which klee)"
+    target_directory="$(dirname "${full_path_to_klee}")"
+    PATH=${PATH/$target_directory/}
+    if which klee; then
+      return 1 # should not happen
+    fi
   fi
 
   ###############################################################################

test/Feature/VarArgByValOld.c

@@ -1,3 +1,6 @@
+// Variadic functions are only supported on x86_64
+// REQUIRES: x86_64
+
 // REQUIRES: lt-llvm-15.0
 /* This test checks that KLEE correctly handles variadic arguments with the
    byval attribute */