kontrol env #40
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" | |
| echo "Current directory structure before setup:" | |
| ls -R "$K_ROOT" | |
| # Try to locate existing directories | |
| echo "Searching for existing k-util.sh..." | |
| find "$K_ROOT" -name k-util.sh | |
| echo "Searching for existing krun..." | |
| find "$K_ROOT" -name krun | |
| # Check directory structure | |
| echo "Checking directory structure..." | |
| ls -la "$K_ROOT/k-distribution" || echo "k-distribution not found" | |
| ls -la "$K_ROOT/k-distribution/lib" || echo "lib directory not found" | |
| # Find k-util.sh first | |
| K_UTIL=$(find "$K_ROOT" -name k-util.sh | head -n 1) | |
| if [ -z "$K_UTIL" ]; then | |
| echo "Error: k-util.sh not found" | |
| exit 1 | |
| fi | |
| echo "Found k-util.sh at: $K_UTIL" | |
| # Get the directory where k-util.sh currently resides | |
| K_UTIL_DIR=$(dirname "$K_UTIL") | |
| echo "k-util.sh directory: $K_UTIL_DIR" | |
| # Find krun | |
| KRUN=$(find "$K_ROOT" -name krun | head -n 1) | |
| if [ -z "$KRUN" ]; then | |
| echo "Error: krun not found" | |
| exit 1 | |
| fi | |
| echo "Found krun at: $KRUN" | |
| KRUN_DIR=$(dirname "$KRUN") | |
| echo "krun directory: $KRUN_DIR" | |
| # Use the existing directory structure instead of creating new ones | |
| K_LIB="$K_UTIL_DIR" | |
| # Export paths | |
| { | |
| echo "K_BIN=$KRUN_DIR" | |
| echo "K_LIB=$K_LIB" | |
| echo "PATH=$KRUN_DIR:$PATH" | |
| } >> $GITHUB_ENV | |
| # Debug: Show final paths | |
| echo "Final K Framework paths:" | |
| echo "K_BIN=$KRUN_DIR" | |
| echo "K_LIB=$K_LIB" | |
| echo "PATH=$KRUN_DIR:$PATH" | |
| # Verify k-util.sh is accessible | |
| if [ ! -f "$K_LIB/k-util.sh" ]; then | |
| echo "Error: Cannot access k-util.sh at $K_LIB/k-util.sh" | |
| 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 |