run_tests.sh

#!/bin/bash

# Script to run KLEE symbolic tests for Raft protocol verification

set -e  # Exit on error

echo "======================================================="
echo "  Running Raft KLEE Symbolic Tests                     "
echo "======================================================="

# Change to test harness directory
cd examples/raft/test_harness || { 
    echo "Error: Could not find examples/raft/test_harness directory" >&2
    exit 1
}

# Clean any previous builds
echo "Cleaning previous builds..."
make clean || echo "Warning: make clean failed (may be OK if nothing to clean)"

# Build and run KLEE test if KLEE is available
echo -e "\n======================================================="
echo "  Building and running KLEE symbolic test                "
echo "======================================================="

# Check if KLEE is available directly
if command -v klee &> /dev/null; then
    echo "KLEE found in system path, running directly..."
    if ! make klee; then
        echo "Error: Failed to build KLEE bytecode" >&2
        exit 1
    fi
    
    echo "Running KLEE symbolic execution..."
    if ! make run-klee; then
        echo "Error: KLEE execution failed" >&2
        exit 1
    fi

# Check if Docker is available
elif command -v docker &> /dev/null; then
    echo "KLEE not found in path, attempting to run via Docker..."
    echo "Building KLEE bytecode..."
    
    if ! docker run --rm -v "$(pwd):/workdir" klee/klee:latest bash -c \
        "cd /workdir && clang -I /klee/include -emit-llvm -c -g -O0 -Wno-everything raft_klee_test.c -o raft_klee_test.bc"; then
        echo "Error: Failed to build KLEE bytecode with Docker" >&2
        exit 1
    fi
    
    echo "Running KLEE symbolic execution..."
    if ! docker run --rm -v "$(pwd):/workdir" klee/klee:latest bash -c \
        "cd /workdir && klee --libc=uclibc --posix-runtime raft_klee_test.bc"; then
        echo "Error: KLEE execution failed in Docker" >&2
        exit 1
    fi
else
    echo "Error: Neither KLEE nor Docker found. Cannot run symbolic tests." >&2
    echo "Please install KLEE or Docker to run tests." >&2
    exit 1
fi

# Check results
echo -e "\n======================================================="
echo "  Test Results                                          "
echo "======================================================="

# Find the latest KLEE output directory (klee-out-* or klee-last)
KLEE_OUT_DIR=""
if [ -L "klee-last" ]; then
    KLEE_OUT_DIR="klee-last"
elif [ -d "klee-out-0" ]; then
    KLEE_OUT_DIR="klee-out-0"
fi

if [ -n "$KLEE_OUT_DIR" ] && [ -d "$KLEE_OUT_DIR" ]; then
    echo "KLEE tests completed. Results in $KLEE_OUT_DIR/"
    
    # Count test cases and errors
    TEST_COUNT=$(ls "$KLEE_OUT_DIR"/test*.ktest 2>/dev/null | wc -l | tr -d ' ')
    ERROR_COUNT=$(ls "$KLEE_OUT_DIR"/test*.err 2>/dev/null | wc -l | tr -d ' ')
    
    echo "Number of test cases: $TEST_COUNT"
    echo "Number of errors found: $ERROR_COUNT"
    
    # Check for specific assertion failures
    if [ -f "$KLEE_OUT_DIR/warnings.txt" ]; then
        if grep -q "assertion failed" "$KLEE_OUT_DIR/warnings.txt" 2>/dev/null; then
            echo -e "\nWarning: Some assertions failed. Check $KLEE_OUT_DIR/warnings.txt for details."
        fi
    fi
    
    # Check for info file and display summary if available
    if [ -f "$KLEE_OUT_DIR/info" ]; then
        echo -e "\nKLEE Summary:"
        grep -E "(explored paths|completed paths|total instructions)" "$KLEE_OUT_DIR/info" 2>/dev/null || true
    fi
else
    echo "Warning: No KLEE test results found in expected directories."
fi

echo -e "\nAll tests completed."
echo "To analyze results in detail, run: python3 analyze_klee_results.py $KLEE_OUT_DIR"