//! Property checking and vulnerability detection.
//!
//! Checks contract properties and detects common vulnerabilities.

use serde::{Deserialize, Serialize};

use crate::ast::{Annotation, Invariant, Property, PropertyKind};
use crate::error::{VerifierError, VerifierResult};
use crate::prover::{ProofResult, Prover, ProverConfig};
use crate::symbolic::SymbolicExecutor;
use crate::{Severity, VerificationContext};

/// Result of checking a property.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct CheckResult {
    /// Property name.
    pub name: String,
    /// Whether property was verified.
    pub verified: bool,
    /// Proof result details.
    pub proof: ProofResult,
    /// Additional messages.
    pub messages: Vec<String>,
}

impl CheckResult {
    /// Creates a new check result.
    pub fn new(name: &str, verified: bool, proof: ProofResult) -> Self {
        Self {
            name: name.to_string(),
            verified,
            proof,
            messages: Vec::new(),
        }
    }

    /// Adds a message.
    pub fn add_message(&mut self, msg: &str) {
        self.messages.push(msg.to_string());
    }

    /// Returns true if property is verified.
    pub fn is_verified(&self) -> bool {
        self.verified
    }
}

/// Vulnerability report.
#[derive(Clone, Debug, Serialize, Deserialize)]
pub struct VulnerabilityReport {
    /// Vulnerability type.
    pub vuln_type: VulnerabilityType,
    /// Severity level.
    pub severity: Severity,
    /// Description.
    pub description: String,
    /// Location (function name, line number).
    pub location: String,
    /// Suggested fix.
    pub fix: Option<String>,
}

/// Known vulnerability types.
#[derive(Clone, Copy, Debug, PartialEq, Eq, Serialize, Deserialize)]
pub enum VulnerabilityType {
    /// Integer overflow/underflow.
    IntegerOverflow,
    /// Reentrancy attack.
    Reentrancy,
    /// Unchecked external call.
    UncheckedCall,
    /// Access control issues.
    AccessControl,
    /// Front-running vulnerability.
    FrontRunning,
    /// Denial of service.
    DoS,
    /// Timestamp dependence.
    TimestampDependence,
    /// Weak randomness.
    WeakRandomness,
    /// Uninitialized storage.
    UninitializedStorage,
    /// Delegatecall to untrusted.
    DelegatecallInjection,
    /// Self-destruct reachable.
    SelfDestruct,
    /// Gas limit issues.
    GasLimit,
}

impl VulnerabilityType {
    /// Returns the default severity for this vulnerability type.
    pub fn default_severity(&self) -> Severity {
        match self {
            VulnerabilityType::Reentrancy => Severity::Critical,
            VulnerabilityType::IntegerOverflow => Severity::High,
            VulnerabilityType::UncheckedCall => Severity::High,
            VulnerabilityType::AccessControl => Severity::Critical,
            VulnerabilityType::DelegatecallInjection => Severity::Critical,
            VulnerabilityType::SelfDestruct => Severity::Critical,
            VulnerabilityType::FrontRunning => Severity::Medium,
            VulnerabilityType::DoS => Severity::Medium,
            VulnerabilityType::TimestampDependence => Severity::Low,
            VulnerabilityType::WeakRandomness => Severity::Medium,
            VulnerabilityType::UninitializedStorage => Severity::High,
            VulnerabilityType::GasLimit => Severity::Low,
        }
    }

    /// Returns a description of the vulnerability.
    pub fn description(&self) -> &'static str {
        match self {
            VulnerabilityType::Reentrancy => {
                "External call followed by state change allows reentrancy attack"
            }
            VulnerabilityType::IntegerOverflow => {
                "Arithmetic operation may overflow or underflow"
            }
            VulnerabilityType::UncheckedCall => {
                "External call return value not checked"
            }
            VulnerabilityType::AccessControl => {
                "Missing or insufficient access control"
            }
            VulnerabilityType::FrontRunning => {
                "Transaction ordering can be exploited"
            }
            VulnerabilityType::DoS => {
                "Contract can be rendered unusable"
            }
            VulnerabilityType::TimestampDependence => {
                "Reliance on block.timestamp which can be manipulated"
            }
            VulnerabilityType::WeakRandomness => {
                "Predictable random number generation"
            }
            VulnerabilityType::UninitializedStorage => {
                "Storage variable used before initialization"
            }
            VulnerabilityType::DelegatecallInjection => {
                "Delegatecall to user-controlled address"
            }
            VulnerabilityType::SelfDestruct => {
                "Contract can be destroyed by attacker"
            }
            VulnerabilityType::GasLimit => {
                "Loop or operation may exceed gas limit"
            }
        }
    }
}

/// Property checker using symbolic execution and SMT solving.
pub struct PropertyChecker {
    config: ProverConfig,
    prover: Prover,
    executor: SymbolicExecutor,
}

impl PropertyChecker {
    /// Creates a new property checker.
    pub fn new(config: ProverConfig) -> Self {
        Self {
            prover: Prover::new(config.clone()),
            executor: SymbolicExecutor::new(config.clone()),
            config,
        }
    }

    /// Checks an invariant holds in all states.
    pub fn check_invariant(
        &self,
        ctx: &VerificationContext,
        inv: &Invariant,
    ) -> VerifierResult<CheckResult> {
        // Create initial symbolic state
        let state = self.executor.create_initial_state(ctx)?;

        // Prove invariant
        let proof = self.prover.prove(&inv.expr, &state)?;

        let verified = proof.is_proven();
        let mut result = CheckResult::new(&inv.name, verified, proof);

        if let Some(desc) = &inv.description {
            result.add_message(desc);
        }

        Ok(result)
    }

    /// Checks a property.
    pub fn check_property(
        &self,
        ctx: &VerificationContext,
        prop: &Property,
    ) -> VerifierResult<CheckResult> {
        match prop.kind {
            PropertyKind::Safety => self.check_safety_property(ctx, prop),
            PropertyKind::Liveness => self.check_liveness_property(ctx, prop),
            PropertyKind::Reachability => self.check_reachability(ctx, prop),
            PropertyKind::Custom => {
                // Custom properties checked like invariants
                let state = self.executor.create_initial_state(ctx)?;
                let proof = self.prover.prove(&prop.expr, &state)?;
                Ok(CheckResult::new(&prop.name, proof.is_proven(), proof))
            }
        }
    }

    /// Checks a safety property (must always hold).
    fn check_safety_property(
        &self,
        ctx: &VerificationContext,
        prop: &Property,
    ) -> VerifierResult<CheckResult> {
        // Symbolically execute all paths and check property
        let paths = self.executor.explore_all_paths(ctx)?;

        for state in &paths {
            let proof = self.prover.prove(&prop.expr, state)?;
            if !proof.is_proven() {
                return Ok(CheckResult::new(&prop.name, false, proof));
            }
        }

        Ok(CheckResult::new(
            &prop.name,
            true,
            ProofResult::Proven {
                time_ms: 0, // Aggregate time not tracked
            },
        ))
    }

    /// Checks a liveness property (must eventually hold).
    fn check_liveness_property(
        &self,
        ctx: &VerificationContext,
        prop: &Property,
    ) -> VerifierResult<CheckResult> {
        // Check if there exists a path where property holds
        let _state = self.executor.create_initial_state(ctx)?;
        let satisfiable = self.prover.check_sat(&prop.expr)?;

        if satisfiable {
            Ok(CheckResult::new(
                &prop.name,
                true,
                ProofResult::Proven { time_ms: 0 },
            ))
        } else {
            Ok(CheckResult::new(
                &prop.name,
                false,
                ProofResult::Unknown {
                    reason: "No path found where property holds".to_string(),
                    time_ms: 0,
                },
            ))
        }
    }

    /// Checks reachability (some state is reachable).
    fn check_reachability(
        &self,
        _ctx: &VerificationContext,
        prop: &Property,
    ) -> VerifierResult<CheckResult> {
        // Check if target state is reachable
        let satisfiable = self.prover.check_sat(&prop.expr)?;

        Ok(CheckResult::new(
            &prop.name,
            satisfiable,
            if satisfiable {
                ProofResult::Proven { time_ms: 0 }
            } else {
                ProofResult::Unknown {
                    reason: "State not reachable".to_string(),
                    time_ms: 0,
                }
            },
        ))
    }

    /// Checks a function annotation (pre/post conditions).
    pub fn check_annotation(
        &self,
        ctx: &VerificationContext,
        ann: &Annotation,
    ) -> VerifierResult<CheckResult> {
        // Get function signature
        let _func = ctx.functions.get(&ann.function).ok_or_else(|| {
            VerifierError::UnknownFunction(ann.function.clone())
        })?;

        let state = self.executor.create_initial_state(ctx)?;

        // Check that preconditions imply postconditions
        for pre in &ann.requires {
            for post in &ann.ensures {
                let proof = self.prover.prove_implication(pre, post, &state)?;
                if !proof.is_proven() {
                    return Ok(CheckResult::new(&ann.function, false, proof));
                }
            }
        }

        Ok(CheckResult::new(
            &ann.function,
            true,
            ProofResult::Proven { time_ms: 0 },
        ))
    }

    /// Detects vulnerabilities in a contract.
    pub fn detect_vulnerabilities(
        &self,
        ctx: &VerificationContext,
    ) -> VerifierResult<Vec<VulnerabilityReport>> {
        let mut vulns = Vec::new();

        // Check each function for vulnerabilities
        for (name, func) in &ctx.functions {
            // Check for reentrancy
            if self.check_reentrancy_pattern(func) {
                vulns.push(VulnerabilityReport {
                    vuln_type: VulnerabilityType::Reentrancy,
                    severity: Severity::Critical,
                    description: VulnerabilityType::Reentrancy.description().to_string(),
                    location: name.clone(),
                    fix: Some("Use checks-effects-interactions pattern".to_string()),
                });
            }

            // Check for unchecked calls
            if self.check_unchecked_call_pattern(func) {
                vulns.push(VulnerabilityReport {
                    vuln_type: VulnerabilityType::UncheckedCall,
                    severity: Severity::High,
                    description: VulnerabilityType::UncheckedCall.description().to_string(),
                    location: name.clone(),
                    fix: Some("Check return value of external calls".to_string()),
                });
            }

            // Check for integer overflow (if no SafeMath)
            if self.check_overflow_pattern(func) {
                vulns.push(VulnerabilityReport {
                    vuln_type: VulnerabilityType::IntegerOverflow,
                    severity: Severity::High,
                    description: VulnerabilityType::IntegerOverflow.description().to_string(),
                    location: name.clone(),
                    fix: Some("Use SafeMath or Solidity 0.8+".to_string()),
                });
            }
        }

        Ok(vulns)
    }

    /// Checks for reentrancy vulnerability pattern.
    fn check_reentrancy_pattern(&self, _func: &crate::FunctionSig) -> bool {
        // Pattern: external call followed by state change
        // Simplified check - full implementation would analyze CFG
        false
    }

    /// Checks for unchecked external call pattern.
    fn check_unchecked_call_pattern(&self, _func: &crate::FunctionSig) -> bool {
        // Pattern: call() without checking return value
        false
    }

    /// Checks for integer overflow pattern.
    fn check_overflow_pattern(&self, _func: &crate::FunctionSig) -> bool {
        // Pattern: arithmetic without overflow checks
        false
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_vulnerability_type_severity() {
        assert_eq!(
            VulnerabilityType::Reentrancy.default_severity(),
            Severity::Critical
        );
        assert_eq!(
            VulnerabilityType::TimestampDependence.default_severity(),
            Severity::Low
        );
    }

    #[test]
    fn test_check_result() {
        let result = CheckResult::new(
            "test_prop",
            true,
            ProofResult::Proven { time_ms: 100 },
        );
        assert!(result.is_verified());
        assert_eq!(result.name, "test_prop");
    }

    #[test]
    fn test_property_checker_creation() {
        let checker = PropertyChecker::new(ProverConfig::default());
        assert_eq!(checker.config.timeout_ms, 30000);
    }
}