Checkout Kani and CBMC in parallel directories and install Kani dependencies before building CBMC from source (#2161)

Author: zhassan-aws

.github/actions/setup/action.yml

@@ -5,22 +5,22 @@ inputs:
   os:
     description: In which Operating System is this running
     required: true
-  install_cbmc:
-    description: Whether to install CBMC
+  kani_dir:
+    description: Path to Kani's root directory
     required: false
-    default: 'true'
+    default: '.'
 runs:
   using: composite
   steps:
       - name: Install dependencies
-        run: ./scripts/setup/${{ inputs.os }}/install_deps.sh
+        run: cd ${{ inputs.kani_dir }} && ./scripts/setup/${{ inputs.os }}/install_deps.sh
         shell: bash
 
       - name: Install Rust toolchain
-        run: ./scripts/setup/install_rustup.sh
+        run: cd ${{ inputs.kani_dir }} && ./scripts/setup/install_rustup.sh
         shell: bash
 
       - name: Update submodules
         run: |
-          git submodule update --init --depth 1
+          cd ${{ inputs.kani_dir }} && git submodule update --init --depth 1
         shell: bash

.github/workflows/cbmc-latest.yml

@@ -21,67 +21,71 @@ jobs:
       matrix:
         os: [macos-11, ubuntu-18.04, ubuntu-20.04, ubuntu-22.04]
     steps:
-      - name: Checkout CBMC under "cbmc"
+      - name: Checkout Kani under "kani"
         uses: actions/checkout@v3
         with:
-          repository: diffblue/cbmc
-          path: cbmc
-
-      - name: Build CBMC
-        run: |
-          cd cbmc
-          cmake -S . -Bbuild -DWITH_JBMC=OFF
-          cmake --build build -- -j 4
-          sudo cmake --build build --target install
-          # Cleanup cbmc directory
-          cd ..
-          rm -rf cbmc
-
-      - name: Checkout Kani
-        uses: actions/checkout@v3
+          path: kani
 
       - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
+        uses: ./kani/.github/actions/setup
         with:
           os: ${{ matrix.os }}
-          install_cbmc: 'false'
+          kani_dir: 'kani'
 
       - name: Build Kani
+        working-directory: ./kani
         run: cargo build-dev
 
-      - name: Execute Kani regressions
-        run: ./scripts/kani-regression.sh
-
-  perf:
-    runs-on: ubuntu-20.04
-    steps:
       - name: Checkout CBMC under "cbmc"
         uses: actions/checkout@v3
         with:
           repository: diffblue/cbmc
           path: cbmc
 
       - name: Build CBMC
+        working-directory: ./cbmc
         run: |
-          cd cbmc
           cmake -S . -Bbuild -DWITH_JBMC=OFF
           cmake --build build -- -j 4
-          sudo cmake --build build --target install
-          # Cleanup cbmc directory
-          cd ..
-          rm -rf cbmc
+          # Prepend the bin directory to $PATH
+          echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH
+
+      - name: Execute Kani regressions
+        working-directory: ./kani
+        run: ./scripts/kani-regression.sh
 
-      - name: Checkout Kani
+  perf:
+    runs-on: ubuntu-20.04
+    steps:
+      - name: Checkout Kani under "kani"
         uses: actions/checkout@v3
+        with:
+          path: kani
 
       - name: Setup Kani Dependencies
-        uses: ./.github/actions/setup
+        uses: ./kani/.github/actions/setup
         with:
           os: ubuntu-20.04
-          install_cbmc: 'false'
+          kani_dir: 'kani'
 
       - name: Build Kani using release mode
+        working-directory: ./kani
         run: cargo build-dev -- --release
 
+      - name: Checkout CBMC under "cbmc"
+        uses: actions/checkout@v3
+        with:
+          repository: diffblue/cbmc
+          path: cbmc
+
+      - name: Build CBMC
+        working-directory: ./cbmc
+        run: |
+          cmake -S . -Bbuild -DWITH_JBMC=OFF
+          cmake --build build -- -j 4
+          # Prepend the bin directory to $PATH
+          echo "${GITHUB_WORKSPACE}/cbmc/build/bin" >> $GITHUB_PATH
+
       - name: Execute Kani performance tests
+        working-directory: ./kani
         run: ./scripts/kani-perf.sh