#!/usr/bin/env python3
"""
CBMC Analysis Report Generator
使用DeepSeek API分析CBMC验证结果并生成直观的分析报告
"""

import sys
import os
from datetime import datetime

# 添加父目录的父目录到路径
backend_dir = os.path.dirname(os.path.abspath(__file__))
project_root = os.path.dirname(backend_dir)
sys.path.insert(0, project_root)

from util.deepseek_wrapper import request_deepseek_engine, create_deepseek_config

def create_analysis_prompt(input_code, generated_code, cbmc_output):
    """创建用于生成分析报告的提示词"""

    prompt = f"""你是一个专业的代码分析专家，请分析以下CBMC验证结果并生成一份详细的分析报告。

原始代码：
```c
{input_code}
```

生成的CBMC断言代码：
```c
{generated_code}
```

CBMC验证输出：
```
{cbmc_output}
```

请按以下格式生成分析报告：

# 🔍 CBMC代码验证分析报告

## 📊 验证摘要
- **总体状态**: [✅验证通过/❌验证失败]
- **断言总数**: [数字]
- **通过断言**: [数字]
- **失败断言**: [数字]
- **成功率**: [百分比]

## 🎯 关键发现
### ✅ 成功验证的方面
[列出成功验证的代码特性和安全检查]

### ⚠️  发现的问题
[如果有失败，列出具体问题和建议]

## 🛡️ 安全性分析
### 内存安全
- [分析内存分配、指针操作的安全性]

### 算术安全
- [分析数值溢出、除零等算术安全问题]

### 边界检查
- [分析数组越界、缓冲区溢出等边界检查]

## 🔧 代码质量评估
### 断言质量
- [评价生成的断言是否充分和准确]

### 代码结构
- [分析代码结构的合理性]

## 💡 改进建议
1. [具体的改进建议1]
2. [具体的改进建议2]
3. [具体的改进建议3]

## 📈 风险评级
- **整体风险等级**: [🟢低风险/🟡中等风险/🔴高风险]
- **主要风险点**: [列出主要风险点]

---
*报告由CBMC SpecGen AI分析生成*
"""

    return [{"role": "user", "content": prompt}]

def generate_analysis_report(input_code, generated_code, cbmc_output):
    """生成CBMC分析报告"""
    try:
        # 创建分析提示
        messages = create_analysis_prompt(input_code, generated_code, cbmc_output)

        # 调用DeepSeek API
        config = create_deepseek_config(messages)
        response = request_deepseek_engine(config)

        if response and 'choices' in response and len(response['choices']) > 0:
            report = response['choices'][0]['message']['content']
            return {
                'success': True,
                'report': report,
                'generated_at': str(datetime.now())
            }
        else:
            return {
                'success': False,
                'error': 'API响应格式错误',
                'report': None
            }

    except Exception as e:
        return {
            'success': False,
            'error': f'生成报告时发生错误: {str(e)}',
            'report': None
        }

def parse_cbmc_results(cbmc_output):
    """解析CBMC输出，提取关键信息"""
    if not cbmc_output:
        return {
            'total_assertions': 0,
            'passed_assertions': 0,
            'failed_assertions': 0,
            'verification_successful': False,
            'errors': []
        }

    lines = cbmc_output.split('\n')
    total_assertions = 0
    passed_assertions = 0
    failed_assertions = 0
    errors = []

    for line in lines:
        if 'failed' in line.lower():
            # 提取失败数量
            if '** 0 of' in line:
                passed_assertions = int(line.split('of')[1].split('failed')[0].strip())
                total_assertions = passed_assertions
            elif 'of' in line and 'failed' in line:
                parts = line.split('of')[1].split('failed')
                failed_assertions = int(parts[0].strip())
                total_assertions = failed_assertions + int(parts[1].split()[1].strip() if '(' in parts[1] else 0)

        if 'VERIFICATION SUCCESSFUL' in line:
            passed_assertions = total_assertions
            failed_assertions = 0

        if 'ASSERTION VIOLATION' in line:
            errors.append(line.strip())
        if 'NULL DEREFERENCE' in line:
            errors.append(line.strip())
        if 'BUFFER OVERFLOW' in line:
            errors.append(line.strip())

    verification_successful = failed_assertions == 0 and total_assertions > 0

    return {
        'total_assertions': total_assertions,
        'passed_assertions': passed_assertions,
        'failed_assertions': failed_assertions,
        'verification_successful': verification_successful,
        'errors': errors
    }

if __name__ == "__main__":
    # 测试分析报告生成
    from datetime import datetime

    test_input = """#include <stdio.h>
int add(int a, int b) {
    return a + b;
}
int main() {
    int result = add(3, 4);
    printf("Result: %d\\n", result);
    return 0;
}"""

    test_generated = """#include <stdio.h>
#include <assert.h>
int add(int a, int b) {
    __CPROVER_assume(a >= -1000 && a <= 1000);
    __CPROVER_assume(b >= -1000 && b <= 1000);
    __CPROVER_assert(!__CPROVER_overflow_add(a, b), "Addition overflow check");
    int result = a + b;
    __CPROVER_assert(result == a + b, "Addition result correctness");
    return result;
}
int main() {
    assert(1 == 1);
    int result = add(3, 4);
    __CPROVER_assert(result == 7, "Expected result should be 7");
    printf("Result: %d\\n", result);
    return 0;
}"""

    test_cbmc = """CBMC version 5.95.1
Parsing test.c
Converting
Type-checking test
Generating GOTO Program
Adding CPROVER library
Generic Property Instrumentation
Starting Bounded Model Checking

** Results:
test.c function main
[main.assertion.1] line 8 main: basic sanity check: SUCCESS
[main.assertion.2] line 12 main: expected result: SUCCESS

** 0 of 2 failed
VERIFICATION SUCCESSFUL"""

    result = generate_analysis_report(test_input, test_generated, test_cbmc)
    print("分析报告生成结果:", result['success'])
    if result['success']:
        print(result['report'])
    else:
        print("错误:", result['error'])