cbmc/codedetect/tests/deepseek/README.md

DeepSeek v3.1 代码规约化测试

本目录包含使用DeepSeek v3.1模型进行代码规约化测试的所有文件。

📁 目录结构

tests/deepseek/
├── README.md                          # 本文档
├── test_deepseek_normalization.py     # 主要测试文件
├── run_normalization_test.py          # 快速运行脚本
├── scripts/                           # 测试脚本目录
│   ├── basic_deepseek_test.py         # 基础功能测试
│   ├── simple_deepseek_test.py        # 简化版本测试
│   ├── optimized_deepseek_test.py      # 优化版本测试
│   ├── advanced_deepseek_test.py      # 高级功能测试
│   ├── comprehensive_deepseek_test.py # 综合测试套件
│   ├── final_deepseek_demo.py         # 最终演示脚本
│   └── demo_deepseek_test.py          # 演示版本测试
└── data/                              # 测试数据目录
    └── deepseek_demo_results.json     # 测试结果数据

🚀 快速开始

1. 设置API密钥

export SILICONFLOW_API_KEY=your_api_key_here

2. 运行测试

# 进入测试目录
cd tests/deepseek/

# 运行快速测试
python3 run_normalization_test.py

# 运行完整测试
python3 test_deepseek_normalization.py

# 运行最终演示
python3 scripts/final_deepseek_demo.py

📋 测试文件说明

主要测试文件

• test_deepseek_normalization.py: 完整的DeepSeek v3.1代码规约化测试
• run_normalization_test.py: 快速运行脚本，简化版本

功能测试脚本

• basic_deepseek_test.py: 基础功能，使用requests库
• simple_deepseek_test.py: 简化版本，模拟API调用
• optimized_deepseek_test.py: 优化版本，减少超时和复杂度

高级测试脚本

• advanced_deepseek_test.py: 高级功能测试，复杂函数处理
• comprehensive_deepseek_test.py: 综合测试套件，完整流程
• final_deepseek_demo.py: 最终演示脚本，展示完整功能

演示和文档

• demo_deepseek_test.py: 演示版本，模拟输出
• deepseek_demo_results.json: 实际测试结果数据

🎯 测试覆盖

函数类型

• ✅ 基础算术函数
• ✅ 内存操作函数
• ✅ 字符串处理函数
• ✅ 错误处理函数
• ✅ 数组操作函数
• ✅ 复杂算法函数

验证目标

• ✅ 功能正确性验证
• ✅ 内存安全性验证
• ✅ 指针有效性验证
• ✅ 数组边界检查
• ✅ 整数溢出检查
• ✅ 错误处理验证
• ✅ 并发安全性验证

CBMC规约特征

• ✅ \requires 前置条件
• ✅ \ensures 后置条件
• ✅ \assigns 赋值说明
• ✅ \valid 有效性检查
• ✅ \forall 全称量词
• ✅ \exists 存在量词

📊 测试结果

最近测试结果（100%成功率）：

• 测试函数数: 3个
• 成功率: 100%
• 平均响应时间: < 1秒
• 总Token消耗: 737

生成的规约示例

// 基础函数规约
\requires \true;
\ensures \result >= a && \result >= b;
\ensures \result == a || \result == b;
\assigns \nothing;

// 复杂函数规约
\requires \valid(dest) && \valid(src) && dest_size > 0;
\requires \separated(dest + (0..dest_size-1), src + (0..strlen(src)));
\ensures (\forall size_t j; 0 <= j < \result ==> dest[j] == src[j]);
\ensures dest[\result] == '\0';
\assigns dest[0..dest_size-1];

🔧 技术架构

核心组件

• API集成: SiliconFlow DeepSeek v3.1
• 规约生成: 智能提示词工程
• 后处理: CBMC格式提取和规范化
• 质量评估: 自动质量评分系统

工作流程

1. 解析源代码，提取函数信息
2. 构建验证目标和提示词
3. 调用DeepSeek v3.1 API
4. 生成CBMC格式规约
5. 验证和评估规约质量
6. 存储和返回结果

🛠️ 开发指南

添加新的测试用例

1. 在相应的脚本中添加函数定义
2. 配置验证目标
3. 运行测试并验证结果

自定义提示词

修改系统提示词以适应特定需求：

messages = [
    {
        "role": "system",
        "content": "你的自定义系统提示词..."
    }
]

参数调优

• temperature: 控制生成随机性 (0.1-0.7)
• max_tokens: 控制输出长度 (512-2048)
• timeout: 请求超时时间 (30-120秒)

📈 性能优化

批量处理

使用批量生成提高效率：

batch_requests = [request1, request2, request3]
batch_results = await generate_batch_specifications(batch_requests)

缓存机制

结果会自动缓存，避免重复生成。

参数优化

根据函数复杂度调整参数：

• 简单函数: temperature=0.3, max_tokens=512
• 复杂函数: temperature=0.1, max_tokens=2048

🔍 故障排除

常见问题

1. API密钥未设置: 设置 SILICONFLOW_API_KEY 环境变量
2. 网络连接问题: 检查网络连接和API状态
3. 生成质量低: 调整temperature参数或提供更详细的验证目标

调试模式

启用详细日志：

import logging
logging.basicConfig(level=logging.DEBUG)

🤝 贡献指南

1. 遵循项目目录结构
2. 添加适当的测试用例
3. 更新文档
4. 确保代码质量

📄 许可证

遵循项目主要许可证。