z3_trace_log_gen.yml

name: Z3 Trace Log Generator

on:
  push:
    branches: [ "main" ]

  # job can also be triggered manually on GitHub
  workflow_dispatch:

jobs:
  generate_log:
    strategy: 
      matrix:
        z3version: ['4.12.2']
    
    # for versions of Z3 at least 4.9.0 we need v1.3 of the GitHub action, for older versions of Z3, 1.2.2
    runs-on: ubuntu-latest

    steps:
      - uses: actions/checkout@v3 # this copies the whole repository
        with:
          fetch-depth: 0 # needed, see GitHub Action "Changed Files"

      - name: Install Z3 for older version 
        uses: pavpanchekha/setup-z3@1.2.2 # see GitHub Action "Install Z3"
        if: ${{ matrix.z3version == '4.8.7' || matrix.z3version == '4.8.8' || matrix.z3version == '4.8.9' }}
        with:
          version: ${{ matrix.z3version }} 

      - name: Install Z3 for newer version 
        uses: pavpanchekha/setup-z3@v1.3 # see GitHub Action "Install Z3"
        if: ${{ !(matrix.z3version == '4.8.7' || matrix.z3version == '4.8.8' || matrix.z3version == '4.8.9') }}
        with:
          version: ${{ matrix.z3version }} 

      - name: Configure Z3 version environment variable
        id: configure-z3-id
        run:
          echo "z3_v_clean=$(echo "${{ matrix.z3version }}" | sed 's/\./_/g')" >> $GITHUB_OUTPUT

      - name: Cache log files
        id: cache-log
        uses: actions/cache@v3
        with:
          path: logs_z3_v${{ steps.configure-z3-id.outputs.z3_v_clean }}.tar.bz2
          key: logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-${{ github.sha }}
          restore-keys: |
            logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-

      - name: Run Z3 solver on changed smt2 files and compress 
        id: run_z3_and_upload
        env:
          CACHE_FILE: logs_z3_v${{ steps.configure-z3-id.outputs.z3_v_clean }}.tar.bz2
        run: |
          # Create the 'logs' directory
          mkdir logs
          test -f "${CACHE_FILE}" && tar -xf "${CACHE_FILE}" || echo "No cache"

          # Loop through all files and check that log exists
          for file in smt-problems/**/*.smt2; do
              test -f "$file" || break
              # Get the file hash
              file_hash=$(shasum -a 256 "$file" | cut -d' ' -f1)
              # Get the filename without extension
              base_name=$(basename "${file%.*}")
              # Log file name
              log_file_name="logs/${base_name}_fHash_${file_hash}.log"
              test -f "${log_file_name}" && continue

              rm -f "logs/${base_name}_fHash_*.log"
              echo "Processing $file to $log_file_name"
              # Run Z3 solver for the file and save the log in the 'logs' directory, TODO: `proof=true`?
              z3 trace=true proof=true trace-file-name=${log_file_name} ./$file > /dev/null || echo "!!! Error processing $file"
          done

          # Compress the 'logs' directory using bzip2
          echo "Compressing to ${CACHE_FILE}"
          tar -cjf "${CACHE_FILE}" logs/

      # TODO: not enough permission for this.
      # - name: Delete old cache
      #   run: |
      #     echo "Fetching list of cache key"
      #     cacheKeys=$(gh cache list -L 100 | cut -f 1)

      #     ## Setting this to not fail the workflow while deleting cache keys. 
      #     set +e
      #     for cacheKey in $cacheKeys; do
      #         echo "Deleting $cacheKey"
      #         gh cache delete $cacheKey -R $REPO
      #     done
      #   env:
      #     GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
      #     REPO: ${{ github.repository }}