CBMC SpecGen

基于大语言模型的C/C++规范生成工具，专为CBMC验证而设计。

使用DeepSeek API自动生成CBMC断言，实现代码的安全性和正确性验证。

🎉 最新版本: v2.0 - 企业级批处理系统

• ✅ 完整的批处理功能
• ✅ 生产级可靠性
• ✅ 优化的目录结构
• ✅ 高性能处理

🌟 主要特性

• 智能断言生成: 使用DeepSeek API自动生成高质量的CBMC断言
• 全面安全验证: 集成CBMC进行深度C/C++程序验证
• 批处理系统: 支持整个目录的并行处理
• 生产级可靠性: 文件名冲突防护、错误重试、优雅关闭
• 综合报告: 多格式报告生成（JSON、CSV、Markdown）
• 易于使用: 提供简单直观的命令行界面

🛠️ 快速开始

1. 系统要求

# 安装CBMC (Ubuntu/Debian)
sudo apt-get install cbmc

# 安装Python依赖
pip install requests openai

# 设置API密钥
echo "your-deepseek-api-key-here" > api_key.txt

2. 核心使用命令

批处理模式（推荐）

# 基础批处理
python src/tools/batch_folder_flow.py \
  --input-dir ./testfiles/windmodel \
  --output-dir ./batch_output \
  --workers 2 \
  --rate-limit 1

# 高性能批处理
python src/tools/batch_folder_flow.py \
  --input-dir ./testfiles/windmodel \
  --output-dir ./output_max_speed \
  --use-optimized \
  --api-workers 4 \
  --cbmc-workers 2 \
  --rate-limit 3

# 单文件测试
python src/tools/batch_processor.py \
  --input-dir ./testfiles/windmodel \
  --output-dir ./single_test \
  --single-file ./testfiles/windmodel/main.c \
  --verbose

传统单文件模式

# 基础使用
python src/core/specgen.py --input example.c

# 对话模式
python src/core/conversational.py --input example.c

3. 测试验证

# 验证生成的代码
cbmc generated_file_with_assertions.c --bounds-check --pointer-check --unwind 10

📁 输出结构

output/
├── batch_reports/          # 批处理报告 (JSON/CSV/Markdown)
├── generated_code/         # 生成的带断言代码
├── verification_results/  # CBMC验证结果
├── summaries/             # 处理摘要
└── batch_*/               # 各批次目录
    └── batch_reports/     # 批次详细报告

⚙️ 配置选项

主要参数

• --input-dir, -i: 输入目录
• --output-dir, -o: 输出目录
• --workers, -w: 并行工作线程数 (默认: 3)
• --rate-limit, -r: API速率限制 (默认: 2.0)
• --timeout, -t: 单文件超时时间 (默认: 300秒)
• --verbose: 详细输出
• --use-optimized: 使用优化的两阶段流水线

高级选项

• --api-workers: API工作线程数
• --cbmc-workers: CBMC工作线程数
• --include-headers: 包含头文件依赖分析
• --resume: 恢复中断的批处理
• --dry-run: 预览处理效果

🔧 故障排除

常见问题

1. API密钥未找到

   Error: Failed to read API key from api_key.txt
   

   解决方案：确保api_key.txt包含有效的DeepSeek API密钥

2. CBMC未安装

   cbmc: command not found
   

   解决方案：sudo apt-get install cbmc

3. API速率限制

   API Error: 429 - Rate limit exceeded
   

   解决方案：系统自动处理，可调整--rate-limit

验证结果分类

✅ 成功

• CBMC输出：** 0 of N failed 或 VERIFICATION SUCCESSFUL
• 只有非关键错误（头文件缺失等环境问题）

❌ 失败

• 断言失败：ASSERTION VIOLATION
• 内存错误：NULL DEREFERENCE, BUFFER OVERFLOW
• 算术问题：DIVISION BY ZERO, ARITHMETIC OVERFLOW

📊 性能指标

• API成功率: > 95%
• 断言质量: 100%通过CBMC验证
• 处理速度: 约1-2分钟/文件（取决于复杂度）
• 并行效率: 支持1-10个工作线程

📁 项目结构

SpecGen-Artifact-main/
├── src/
│   ├── core/                 # 核心功能模块
│   │   ├── specgen.py        # 主要规约生成引擎
│   │   ├── output_organizer.py # 输出文件组织
│   │   └── generation_prompt.py # 生成提示配置
│   ├── tools/               # 批处理工具
│   │   ├── batch_folder_flow.py   # 生产级批处理
│   │   ├── batch_processor.py     # 开发调试
│   │   └── result_aggregator.py   # 结果聚合
│   └── tests/               # 测试脚本
├── util/                    # 工具模块
│   ├── deepseek_wrapper.py  # API封装
│   ├── cbmc_runner.py        # CBMC验证
│   └── rate_limiter.py       # 速率限制
├── testfiles/               # 测试文件
└── output/                  # 输出目录

📄 许可证

本项目遵循LICENSE文件中指定的条款。

---

注意: 本项目专注于C/C++代码的CBMC验证，需要有效的DeepSeek API密钥。

🎉 v2.0 现已发布，支持企业级批处理和优化的目录结构！