# 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密钥
```bash
export SILICONFLOW_API_KEY=your_api_key_here
```

### 2. 运行测试
```bash
# 进入测试目录
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

### 生成的规约示例
```c
// 基础函数规约
\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. 运行测试并验证结果

### 自定义提示词
修改系统提示词以适应特定需求：
```python
messages = [
    {
        "role": "system",
        "content": "你的自定义系统提示词..."
    }
]
```

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

## 📈 性能优化

### 批量处理
使用批量生成提高效率：
```python
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参数或提供更详细的验证目标

### 调试模式
启用详细日志：
```python
import logging
logging.basicConfig(level=logging.DEBUG)
```

## 🤝 贡献指南

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

## 📄 许可证

遵循项目主要许可证。