kontrol env #39
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: CI | |
| on: [push] | |
| jobs: | |
| foundry-test: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| submodules: recursive | |
| - uses: foundry-rs/foundry-toolchain@v1 | |
| with: | |
| version: nightly | |
| - name: Install forge-std | |
| run: | | |
| forge install foundry-rs/forge-std --no-commit | |
| forge remappings > remappings.txt | |
| - name: Run non-Kontrol tests | |
| run: | | |
| forge test --no-match-path "src/test/kontrol/*" -vvv | |
| - name: Run snapshot without Kontrol tests | |
| run: forge snapshot --no-match-path "src/test/kontrol/*" | |
| formal-verification: | |
| runs-on: ubuntu-latest | |
| needs: foundry-test | |
| steps: | |
| - uses: actions/checkout@v4 | |
| with: | |
| fetch-depth: 0 | |
| submodules: recursive | |
| # Download and Extract K Framework | |
| - name: Download K Framework | |
| env: | |
| REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} | |
| run: | | |
| echo "Downloading K Framework..." | |
| curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o kframework.tar.gz \ | |
| https://github.com/runtimeverification/k/releases/download/v7.1.170/kframework-7.1.170-src.tar.gz | |
| echo "Validating tarball..." | |
| file kframework.tar.gz || { echo "Download failed"; exit 1; } | |
| echo "Extracting K Framework..." | |
| mkdir -p kframework | |
| tar -xzf kframework.tar.gz -C kframework --strip-components=1 || { echo "Extraction failed"; exit 1; } | |
| ls -l kframework || { echo "Extraction directory not found"; exit 1; } | |
| - name: Install Poetry | |
| uses: snok/install-poetry@v1 | |
| with: | |
| version: 1.4.0 | |
| virtualenvs-create: true | |
| # Download and Build KEVM | |
| - name: Install KEVM | |
| env: | |
| REPOSITORY_TOKEN: ${{ secrets.REPOSITORY_TOKEN }} | |
| run: | | |
| echo "Downloading KEVM..." | |
| curl -H "Authorization: token $REPOSITORY_TOKEN" -L -o evm.tar.gz \ | |
| https://github.com/runtimeverification/evm-semantics/archive/refs/tags/v1.0.753.tar.gz | |
| mkdir -p evm | |
| tar -xzf evm.tar.gz -C evm --strip-components=1 || { echo "Extraction failed"; exit 1; } | |
| cd evm | |
| make deps || true | |
| make build || true | |
| make test || true | |
| - name: Setup K Framework Environment | |
| run: | | |
| # Set absolute paths | |
| WORKSPACE="$GITHUB_WORKSPACE" | |
| K_ROOT="$WORKSPACE/kframework" | |
| K_LIB_DIR="$K_ROOT/k-distribution/lib/kframework" | |
| # Create directory if it doesn't exist (with -p to avoid errors if it exists) | |
| mkdir -p "$K_LIB_DIR" | |
| # Find k-util.sh | |
| K_UTIL=$(find "$K_ROOT" -name k-util.sh | head -n 1) | |
| if [ -z "$K_UTIL" ]; then | |
| echo "Error: k-util.sh not found" | |
| find "$K_ROOT" -type f -name "*k-util*" # Debug: look for similar files | |
| exit 1 | |
| fi | |
| echo "Found k-util.sh at: $K_UTIL" | |
| # Copy k-util.sh to the expected location (use -f to force overwrite if exists) | |
| cp -f "$K_UTIL" "$K_LIB_DIR/" | |
| # Find krun | |
| KRUN=$(find "$K_ROOT" -name krun | head -n 1) | |
| if [ -z "$KRUN" ]; then | |
| echo "Error: krun not found" | |
| find "$K_ROOT" -type f -name "*krun*" # Debug: look for similar files | |
| exit 1 | |
| fi | |
| echo "Found krun at: $KRUN" | |
| KRUN_DIR=$(dirname "$KRUN") | |
| # Export paths | |
| { | |
| echo "K_BIN=$KRUN_DIR" | |
| echo "K_LIB=$K_LIB_DIR" | |
| echo "PATH=$KRUN_DIR:$PATH" | |
| } >> $GITHUB_ENV | |
| # Debug: Show directory structure | |
| echo "K Framework directory structure:" | |
| echo "K_ROOT=$K_ROOT" | |
| echo "K_BIN=$KRUN_DIR" | |
| echo "K_LIB=$K_LIB_DIR" | |
| ls -la "$K_ROOT/k-distribution/lib" || echo "lib directory not accessible" | |
| ls -la "$K_LIB_DIR" || echo "kframework directory not accessible" | |
| # Verify k-util.sh was copied correctly | |
| if [ ! -f "$K_LIB_DIR/k-util.sh" ]; then | |
| echo "Error: Failed to copy k-util.sh to $K_LIB_DIR" | |
| exit 1 | |
| fi | |
| - name: Configure KRUN | |
| run: | | |
| # Get paths from environment | |
| K_BIN="$K_BIN" | |
| K_LIB="$K_LIB" | |
| KRUN_SCRIPT="$K_BIN/krun" | |
| if [ ! -f "$KRUN_SCRIPT" ]; then | |
| echo "Error: krun script not found at $KRUN_SCRIPT" | |
| exit 1 | |
| fi | |
| # Create backup | |
| cp "$KRUN_SCRIPT" "${KRUN_SCRIPT}.backup" | |
| # Update source path in krun script | |
| sed -i "s|source.*k-util\.sh|source \"$K_LIB/k-util.sh\"|g" "$KRUN_SCRIPT" | |
| echo "Modified krun script:" | |
| head -n 10 "$KRUN_SCRIPT" | |
| # Test k-util.sh exists | |
| if [ ! -f "$K_LIB/k-util.sh" ]; then | |
| echo "Error: k-util.sh not found at $K_LIB/k-util.sh" | |
| exit 1 | |
| fi | |
| - name: Run Formal Verification with KEVM | |
| run: | | |
| # Create results directory | |
| mkdir -p verification-results | |
| # Initialize counter for verified specs | |
| verified_count=0 | |
| for spec in src/test/kontrol/*.k; do | |
| if [ -f "$spec" ]; then | |
| echo "Verifying $spec..." | |
| if "$K_BIN/krun" \ | |
| --directory src/test/kontrol \ | |
| --debug \ | |
| --output-file "verification-results/$(basename "$spec" .k).out" \ | |
| "$spec"; then | |
| echo "✓ Verification successful for $spec" | |
| ((verified_count++)) | |
| else | |
| echo "✗ Verification failed for $spec" | |
| exit 1 | |
| fi | |
| fi | |
| done | |
| if [ $verified_count -eq 0 ]; then | |
| echo "No specification files found to verify" | |
| exit 1 | |
| else | |
| echo "Successfully verified $verified_count specification(s)" | |
| fi | |
| - name: Upload Verification Results | |
| uses: actions/upload-artifact@v3 | |
| with: | |
| name: verification-results | |
| path: verification-results/ | |
| if-no-files-found: error | |
| retention-days: 30 |