#!/bin/bash

# CBMC Environment Setup Script
# This script initializes the CBMC verification environment

set -e

# Colors for output
RED='\033[0;31m'
GREEN='\033[0;32m'
YELLOW='\033[1;33m'
BLUE='\033[0;34m'
NC='\033[0m' # No Color

print_status() {
    echo -e "${BLUE}[INFO]${NC} $1"
}

print_success() {
    echo -e "${GREEN}[SUCCESS]${NC} $1"
}

print_warning() {
    echo -e "${YELLOW}[WARNING]${NC} $1"
}

print_error() {
    echo -e "${RED}[ERROR]${NC} $1"
}

# Function to check if CBMC is available
check_cbmc() {
    print_status "Checking CBMC installation..."

    if ! command -v cbmc >/dev/null 2>&1; then
        print_error "CBMC is not installed or not in PATH"
        print_status "Please install CBMC:"
        echo "  - Ubuntu/Debian: sudo apt-get install cbmc"
        echo "  - Download from: https://github.com/diffblue/cbmc"
        exit 1
    fi

    CBMC_VERSION=$(cbmc --version 2>/dev/null | head -n1 || echo "unknown")
    print_success "CBMC found: $CBMC_VERSION"
}

# Function to create CBMC directory structure
create_cbmc_directories() {
    print_status "Creating CBMC directory structure..."

    directories=(
        "cbmc/proofs"
        "cbmc/harnesses"
        "cbmc/configs"
        "cbmc/results"
    )

    for dir in "${directories[@]}"; do
        if [ ! -d "$dir" ]; then
            mkdir -p "$dir"
            print_status "Created directory: $dir"
        fi
    done

    print_success "CBMC directories created"
}

# Function to create common Makefile
create_makefile() {
    print_status "Creating CBMC Makefile..."

    cat > cbmc/Makefile.common << 'EOF'
# Common Makefile for CBMC Verification
# This file provides common targets and variables for CBMC verification

# CBMC Configuration
CBMC ?= cbmc
CBMC_FLAGS ?= --unwinding 10 --bounds-check --pointer-check --overflow-check
CBMC_SHOW_PROPERTIES ?= --show-properties
CBMC_ERROR_TRACE ?= --trace

# Default target
.PHONY: help
help:
	@echo "Available targets:"
	@echo "  all          Run all proofs"
	@echo "  clean        Clean build artifacts"
	@echo "  <proof-name> Run specific proof"
	@echo "  show-<proof> Show properties for proof"
	@echo "  trace-<proof> Show error trace for proof"

# Run all proofs
.PHONY: all
all:
	@for proof in $(PROOFS); do \
		echo "Running proof: $$proof"; \
		$(MAKE) $$proof || exit 1; \
	done

# Clean build artifacts
.PHONY: clean
clean:
	rm -f *.out *.cbmc-out *.trace *.witness
	rm -rf cbmc-out/

# Generic proof target
%.out: %.c
	$(CBMC) $(CBMC_FLAGS) $(CBMC_SHOW_PROPERTIES) $< > $@

# Show properties
show-%: %.c
	$(CBMC) $(CBMC_SHOW_PROPERTIES) $<

# Show error trace
trace-%: %.c
	$(CBMC) $(CBMC_ERROR_TRACE) $<

# Run with specific unwinding
unwind-%: %.c
	$(CBMC) --unwinding $* $(CBMC_FLAGS) $<

# Run with specific checks
check-%: %.c
	$(CBMC) --$*-check $(CBMC_FLAGS) $<

# Memory safety checks
memory-safe: %.c
	$(CBMC) --bounds-check --pointer-check --div-by-zero-check $<

# Arithmetic checks
arithmetic-safe: %.c
	$(CBMC) --overflow-check --undefined-shift-check --signed-overflow-check $<

# Full verification
full-verify: %.c
	$(CBMC) --all-checks $(CBMC_FLAGS) $<

# Debug mode
debug: %.c
	$(CBMC) --verbosity 10 $(CBMC_FLAGS) $<

# Profile mode
profile: %.c
	$(CBMC) --json-ui $(CBMC_FLAGS) $< > profile.json
EOF

    print_success "Created cbmc/Makefile.common"
}

# Function to create sample configuration files
create_config_files() {
    print_status "Creating CBMC configuration files..."

    # Create verification configuration template
    cat > cbmc/configs/verification.yaml << 'EOF'
# CBMC Verification Configuration Template

# Default verification options
default_options:
  unwinding: 10
  timeout: 300
  memory_model: "precise"
  object_bits: 8

# Check types to enable
checks:
  pointer_check: true
  overflow_check: true
  bounds_check: true
  assertion_check: true
  div_by_zero_check: true
  undefined_shift_check: true
  signed_overflow_check: true
  floating_point_check: false
  termination_check: false

# Verification strategies
strategies:
  memory_safety:
    checks: ["pointer", "bounds", "div_by_zero"]
    description: "Focus on memory safety properties"

  arithmetic_safety:
    checks: ["overflow", "undefined_shift", "signed_overflow"]
    description: "Focus on arithmetic safety properties"

  full_verification:
    checks: ["pointer", "bounds", "overflow", "assertion", "div_by_zero"]
    description: "Comprehensive verification"

# FreeRTOS specific configuration
freertos:
  include_paths:
    - "FreeRTOS/Source/include"
    - "FreeRTOS/Source/portable/GCC/Linux"

  defines:
    - "projCOVERAGE_TEST=0"
    - "INCLUDE_uxTaskGetStackHighWaterMark=0"

  unwinding: 15
  timeout: 600
EOF

    # Create proof configuration template
    cat > cbmc/configs/proof-template.yaml << 'EOF'
# Proof Configuration Template
# Copy this file and customize for your specific proof

proof_name: "example_proof"
source_file: "example.c"
function: "example_function"

# CBMC options
options:
  unwinding: 10
  timeout: 300
  memory_model: "precise"

# Properties to verify
properties:
  memory_safety: true
  arithmetic_safety: true
  user_assertions: true

# Harness generation
harness:
  create_main: true
  input_ranges:
    - name: "input_param"
      min: 0
      max: 100
      type: "int"

# Expected results
expected:
  status: "SUCCESSFUL"  # SUCCESSFUL, FAILED, or UNKNOWN
  verification_time: "< 60s"
EOF

    print_success "Created CBMC configuration templates"
}

# Function to create sample harness template
create_harness_templates() {
    print_status "Creating CBMC harness templates..."

    # Create basic harness template
    cat > cbmc/harnesses/harness-template.c << 'EOF'
/*
 * CBMC Harness Template
 * This template provides a basic structure for CBMC test harnesses
 */

#include <stddef.h>
#include <stdint.h>

// Function to be tested (replace with actual function)
// extern int target_function(int param1, void* ptr);

// Input constraints
#define MAX_INPUT_SIZE 1024
#define MIN_VALUE 0
#define MAX_VALUE 1000

// Helper functions for CBMC verification
void __CPROVER_assert(int cond, const char* msg) {
    if (!cond) {
        // Assertion failed - CBMC will generate counterexample
    }
}

// Nondeterministic input generation
int nondet_int();
void* nondet_void_ptr();
size_t nondet_size_t();

// Main harness function
int main() {
    // Generate nondeterministic inputs
    int input_param = nondet_int();
    void* input_ptr = nondet_void_ptr();
    size_t size = nondet_size_t();

    // Input constraints
    __CPROVER_assume(input_param >= MIN_VALUE && input_param <= MAX_VALUE);
    __CPROVER_assume(size <= MAX_INPUT_SIZE);

    // Pointer validity assumptions
    if (input_ptr != NULL) {
        __CPROVER_assume(__CPROVER_r_ok(input_ptr, size));
    }

    // Call function under test
    // int result = target_function(input_param, input_ptr);

    // Postcondition checks
    // __CPROVER_assert(result >= 0, "Function should return non-negative value");

    return 0;
}
EOF

    # Create FreeRTOS-specific harness template
    cat > cbmc/harnesses/freertos-harness-template.c << 'EOF'
/*
 * FreeRTOS CBMC Harness Template
 * Template for verifying FreeRTOS functions with CBMC
 */

#include <stddef.h>
#include <stdint.h>

// FreeRTOS includes (adjust paths as needed)
// #include "FreeRTOS.h"
// #include "task.h"

// CBMC helper functions
void __CPROVER_assert(int cond, const char* msg);
void __CPROVER_assume(int cond);

// Nondeterministic functions
UBaseType_t nondet_UBaseType_t();
TaskHandle_t nondet_TaskHandle_t();
void* nondet_void_ptr();
TickType_t nondet_TickType_t();

// FreeRTOS constraints
#define MAX_TASKS 10
#define MAX_PRIORITY (configMAX_PRIORITIES - 1)

int main() {
    // Generate nondeterministic inputs for FreeRTOS functions
    UBaseType_t uxPriority = nondet_UBaseType_t();
    TaskHandle_t *pxCreatedTask = nondet_TaskHandle_t();
    char *pcName = "TestTask";
    uint32_t usStackDepth = configMINIMAL_STACK_SIZE;
    void *pvParameters = nondet_void_ptr();

    // FreeRTOS-specific constraints
    __CPROVER_assume(uxPriority <= MAX_PRIORITY);
    __CPROVER_assume(usStackDepth >= configMINIMAL_STACK_SIZE);
    __CPROVER_assume(usStackDepth <= 8192);

    // Task handle array assumption
    TaskHandle_t xTaskHandleArray[MAX_TASKS];
    if (pxCreatedTask != NULL) {
        __CPROVER_assume(__CPROVER_r_ok(pxCreatedTask, sizeof(TaskHandle_t)));
    }

    // Call FreeRTOS function (example: xTaskCreate)
    /*
    BaseType_t xResult = xTaskCreate(
        vTaskFunction,
        pcName,
        usStackDepth,
        pvParameters,
        uxPriority,
        pxCreatedTask
    );
    */

    // Postcondition checks
    // __CPROVER_assert(xResult == pdPASS || xResult == errCOULD_NOT_ALLOCATE_REQUIRED_MEMORY,
    //                "Task creation should return valid status");

    return 0;
}
EOF

    print_success "Created CBMC harness templates"
}

# Function to test CBMC installation
test_cbmc() {
    print_status "Testing CBMC installation..."

    # Create simple test file
    cat > cbmc/test-simple.c << 'EOF'
#include <stddef.h>

int simple_function(int *ptr, int size) {
    if (ptr == NULL || size <= 0) {
        return -1;
    }

    if (size > 100) {
        return -2;
    }

    for (int i = 0; i < size; i++) {
        ptr[i] = i;
    }

    return 0;
}

int main() {
    int arr[50];
    return simple_function(arr, 50);
}
EOF

    # Test CBMC execution
    if cd cbmc && cbmc --unwind 10 --bounds-check --pointer-check test-simple.c >/dev/null 2>&1; then
        print_success "CBMC test passed"
        rm -f test-simple.c test-simple.out
    else
        print_warning "CBMC test failed or produced warnings"
        print_status "Check CBMC installation and try again"
    fi
}

# Function to show usage
show_usage() {
    echo "Usage: $0 [OPTIONS]"
    echo ""
    echo "Options:"
    echo "  -h, --help     Show this help message"
    echo "  -t, --test      Run CBMC tests"
    echo "  -f, --force     Force recreation of existing files"
    echo ""
    echo "This script sets up the CBMC verification environment."
}

# Main function
main() {
    local run_tests=false
    local force_recreate=false

    # Parse command line arguments
    while [[ $# -gt 0 ]]; do
        case $1 in
            -h|--help)
                show_usage
                exit 0
                ;;
            -t|--test)
                run_tests=true
                shift
                ;;
            -f|--force)
                force_recreate=true
                shift
                ;;
            *)
                print_error "Unknown option: $1"
                show_usage
                exit 1
                ;;
        esac
    done

    print_status "Setting up CBMC environment..."
    print_status "================================"

    # Check CBMC installation
    check_cbmc

    # Create directory structure
    create_cbmc_directories

    # Create configuration files
    if [ "$force_recreate" = true ] || [ ! -f "cbmc/Makefile.common" ]; then
        create_makefile
    else
        print_warning "cbmc/Makefile.common already exists"
    fi

    if [ "$force_recreate" = true ] || [ ! -f "cbmc/configs/verification.yaml" ]; then
        create_config_files
    else
        print_warning "CBMC configuration files already exist"
    fi

    if [ "$force_recreate" = true ] || [ ! -f "cbmc/harnesses/harness-template.c" ]; then
        create_harness_templates
    else
        print_warning "CBMC harness templates already exist"
    fi

    # Run tests if requested
    if [ "$run_tests" = true ]; then
        test_cbmc
    fi

    print_success ""
    print_success "CBMC environment setup completed!"
    print_success ""
    print_status "CBMC directory structure:"
    echo "  cbmc/Makefile.common    - Common build rules"
    echo "  cbmc/configs/           - Configuration files"
    echo "  cbmc/harnesses/         - Test harness templates"
    echo "  cbmc/proofs/            - Proof files directory"
    echo "  cbmc/results/           - Verification results"
    print_success ""
}

# Run main function
main "$@"