|
|
#!/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']) |
