You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
159 lines
5.3 KiB
159 lines
5.3 KiB
#!/usr/bin/env python3
|
|
"""
|
|
简化的CBMC分析报告生成器
|
|
使用内置的演示逻辑生成分析报告
|
|
"""
|
|
|
|
import requests
|
|
import json
|
|
from datetime import datetime
|
|
|
|
def generate_demo_analysis_report(input_code, generated_code, cbmc_output):
|
|
"""生成演示版本的AI分析报告"""
|
|
|
|
# 解析CBMC输出的基本信息
|
|
total_assertions = cbmc_output.count('SUCCESS') + cbmc_output.count('FAILED')
|
|
success_count = cbmc_output.count('SUCCESS')
|
|
failed_count = cbmc_output.count('FAILED')
|
|
|
|
# 检查代码特性
|
|
has_malloc = 'malloc' in input_code
|
|
has_pointers = '*' in input_code
|
|
has_arrays = '[' in input_code
|
|
has_loops = 'for' in input_code or 'while' in input_code
|
|
has_structs = 'struct' in input_code
|
|
|
|
# 生成风险评级
|
|
risk_factors = []
|
|
if has_malloc:
|
|
risk_factors.append("动态内存分配")
|
|
if has_pointers:
|
|
risk_factors.append("指针操作")
|
|
if has_arrays:
|
|
risk_factors.append("数组访问")
|
|
|
|
risk_level = "🟢低风险"
|
|
if len(risk_factors) >= 2:
|
|
risk_level = "🟡中等风险"
|
|
if len(risk_factors) >= 3:
|
|
risk_level = "🔴高风险"
|
|
|
|
# 生成报告内容
|
|
report = f"""# 🔍 CBMC代码验证分析报告
|
|
|
|
## 📊 验证摘要
|
|
- **总体状态**: {'✅验证通过' if failed_count == 0 else '❌验证失败'}
|
|
- **断言总数**: {total_assertions}
|
|
- **通过断言**: {success_count}
|
|
- **失败断言**: {failed_count}
|
|
- **成功率**: {round((success_count/total_assertions)*100, 1) if total_assertions > 0 else 0}%
|
|
|
|
## 🎯 关键发现
|
|
### ✅ 成功验证的方面
|
|
- 基础代码逻辑正确性验证通过
|
|
- {'内存分配安全性检查' if has_malloc else '基础算术运算'}
|
|
- {'指针操作安全性验证' if has_pointers else '变量初始化检查'}
|
|
- 边界条件和基本断言验证
|
|
|
|
### ⚠️ 发现的问题
|
|
{'无明显安全问题' if failed_count == 0 else f'发现 {failed_count} 个失败的断言，需要进一步检查'}
|
|
|
|
## 🛡️ 安全性分析
|
|
### 内存安全
|
|
- {'✅ 包含动态内存分配验证' if has_malloc else '✅ 基础内存访问安全'}
|
|
- {'✅ 指针操作已通过验证' if has_pointers else '✅ 无复杂指针操作'}
|
|
- {'✅ 数组边界检查已实现' if has_arrays else '✅ 无数组越界风险'}
|
|
|
|
### 算术安全
|
|
- ✅ 基础算术运算验证
|
|
- {'⚠️ 建议添加除零检查' if '/' in input_code and 'divide' in input_code else '✅ 无除零风险'}
|
|
- {'⚠️ 建议添加溢出检查' if '+' in input_code or '*' in input_code else '✅ 算术运算安全'}
|
|
|
|
### 边界检查
|
|
- {'✅ 循环边界条件已验证' if has_loops else '✅ 无复杂循环结构'}
|
|
- {'✅ 数组访问边界检查' if has_arrays else '✅ 无数组访问风险'}
|
|
|
|
## 🔧 代码质量评估
|
|
### 断言质量
|
|
- {'🔵 生成的断言覆盖了关键路径' if total_assertions >= 3 else '🟡 建议增加更多断言'}
|
|
- {'✅ 断言类型多样化' if has_malloc or has_pointers else '✅ 基础断言完整'}
|
|
- "断言分布合理，覆盖主要函数"
|
|
|
|
### 代码结构
|
|
- {'✅ 包含复杂数据结构' if has_structs else '✅ 代码结构清晰'}
|
|
- {'✅ 包含内存管理逻辑' if has_malloc else '✅ 简单直接的控制流'}
|
|
- {'✅ 算法逻辑正确' if has_loops else '✅ 线性执行流程'}
|
|
|
|
## 💡 改进建议
|
|
1. {'考虑添加更详细的输入验证' if has_pointers else '保持当前的代码风格'}
|
|
2. {'建议增加单元测试覆盖边界情况' if has_arrays else '可以添加更多的注释说明'}
|
|
3. {'考虑使用RAII模式管理内存' if has_malloc else '代码具有良好的可维护性'}
|
|
4. {'建议添加更详细的错误处理机制' if failed_count > 0 else '继续保持良好的编码实践'}
|
|
|
|
## 📈 风险评级
|
|
- **整体风险等级**: {risk_level}
|
|
- **主要风险点**: {', '.join(risk_factors) if risk_factors else '无明显风险点'}
|
|
- **建议措施**: {'建议进行更深入的静态分析' if len(risk_factors) >= 2 else '当前代码质量良好'}
|
|
|
|
---
|
|
*报告由CBMC SpecGen AI分析生成 | 生成时间: {datetime.now().strftime('%Y-%m-%d %H:%M:%S')}*"""
|
|
|
|
return {
|
|
'success': True,
|
|
'report': report,
|
|
'generated_at': datetime.now().isoformat()
|
|
}
|
|
|
|
if __name__ == "__main__":
|
|
# 测试分析报告生成
|
|
test_input = """#include <stdio.h>
|
|
int divide(int a, int b) {
|
|
if (b == 0) {
|
|
return -1;
|
|
}
|
|
return a / b;
|
|
}
|
|
int main() {
|
|
int result = divide(10, 2);
|
|
printf("Result: %d\\n", result);
|
|
return 0;
|
|
}"""
|
|
|
|
test_generated = """#include <stdio.h>
|
|
#include <assert.h>
|
|
int divide(int a, int b) {
|
|
if (b == 0) {
|
|
return -1;
|
|
}
|
|
return a / b;
|
|
}
|
|
int main() {
|
|
assert(1 == 1);
|
|
int result = divide(10, 2);
|
|
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: valid computation: SUCCESS
|
|
|
|
** 0 of 2 failed
|
|
VERIFICATION SUCCESSFUL"""
|
|
|
|
result = generate_demo_analysis_report(test_input, test_generated, test_cbmc)
|
|
print("分析报告生成结果:", result['success'])
|
|
if result['success']:
|
|
print(result['report'])
|
|
else:
|
|
print("错误:", result.get('error', '未知错误')) |