7.3 KiB

Raw Permalink Blame History Unescape Escape

DeepSeek v3.1 代码规约化测试

本项目提供了使用 DeepSeek v3.1 模型对 C/C++ 代码进行形式化规约生成的测试工具。

功能特性

🔗 DeepSeek v3.1 集成: 使用 SiliconFlow API 调用 DeepSeek v3.1 模型
📝 CBMC 规约生成: 自动生成 CBMC 格式形式化验证规约
🎯 多维度验证: 支持功能正确性、内存安全、溢出检查等验证目标
🚀 批量处理: 支持单个和批量函数规约生成
📊 质量评估: 自动评估生成规约的质量
🌊 流式生成: 支持实时流式规约生成

快速开始

1. 设置 API 密钥

export SILICONFLOW_API_KEY=your_api_key_here

2. 运行快速测试

# 简单测试
python run_normalization_test.py

# 完整测试
python test_deepseek_normalization.py

3. 示例输出

🚀 DeepSeek v3.1 代码规约化快速测试
==================================================
📡 连接模型: deepseek-ai/DeepSeek-V3.1
🔍 检查API状态...
✅ API健康 (响应时间: 1.23s)

📝 函数: add_numbers
🎯 目标: 生成形式化验证规约

⏳ 正在生成规约...

✅ 生成成功!
📊 质量评分: 0.92
⏱️  生成时间: 2.45s
🔤 使用Token: 156

📋 生成的CBMC规约:
----------------------------------------
\\requires \\valid(a) && \\valid(b);
\\ensures \\result == a + b;
\\assigns \\nothing;
----------------------------------------

测试用例

基础算术函数

int add_numbers(int a, int b) {
    return a + b;
}

安全加法函数（带溢出检查）

bool safe_add(int a, int b, int *result) {
    if (result == NULL) {
        return false;
    }

    if (a > 0 && b > INT_MAX - a) {
        return false; // 正数溢出
    }
    if (a < 0 && b < INT_MIN - a) {
        return false; // 负数溢出
    }

    *result = a + b;
    return true;
}

数组操作函数

void array_copy(int *dest, const int *src, size_t size) {
    if (dest == NULL || src == NULL) {
        return;
    }

    for (size_t i = 0; i < size; i++) {
        dest[i] = src[i];
    }
}

生成的 CBMC 规约示例

简单函数规约

\\requires \\valid(a) && \\valid(b);
\\ensures \\result == a + b;
\\assigns \\nothing;

复杂函数规约

\\requires \\valid(result) &&
         ((a > 0 && b > 0) ==> a <= INT_MAX - b) &&
         ((a < 0 && b < 0) ==> a >= INT_MIN - b);
\\ensures \\result == true ==> *result == a + b;
\\assigns *result;

验证目标支持

functional_correctness: 功能正确性验证
memory_safety: 内存安全性验证
pointer_validity: 指针有效性验证
integer_overflow: 整数溢出检查
array_bounds: 数组边界检查
error_handling: 错误处理验证
division_safety: 除法安全性检查

质量评估指标

语法正确性: CBMC 规约语法是否正确
完整性: 是否覆盖所有验证目标
精确性: 规约是否准确反映函数行为
一致性: 前置条件和后置条件是否一致

配置选项

环境变量

SILICONFLOW_API_KEY: API 密钥（必需）
SILICONFLOW_BASE_URL: API 基础 URL（可选，默认：https://api.siliconflow.cn/v1）

模型参数

model: 使用的模型（默认：deepseek-ai/DeepSeek-V3.1）
temperature: 生成温度（默认：0.7）
max_tokens: 最大 Token 数（默认：4096）
timeout: 请求超时时间（默认：120秒）

错误处理

常见错误及解决方案

API 密钥未设置

❌ 错误: 未设置 SILICONFLOW_API_KEY 环境变量
✅ 解决方案: export SILICONFLOW_API_KEY=your_api_key

API 连接失败

❌ API 不健康: Connection timeout
✅ 解决方案: 检查网络连接和 API 密钥有效性

生成质量低

📊 质量评分: 0.45
✅ 解决方案: 调整 temperature 参数或提供更详细的验证目标

高级功能

1. 批量规约生成

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

2. 流式生成

async for chunk in generator.stream_specification(request):
    print(chunk, end='', flush=True)

3. 规约优化

refined_result = await generator.refine_specification(
    original_spec=spec,
    function_info=function_info,
    issues=issues,
    suggestions=suggestions
)

4. 统计信息

stats = generator.get_generation_stats()
print(f"总规约数: {stats['total_specifications']}")
print(f"平均质量: {stats['average_quality']:.2f}")

文件结构

Codedetection/
├── test_deepseek_normalization.py    # 完整测试脚本
├── run_normalization_test.py         # 快速测试脚本
├── DEEPSEEK_TEST_README.md           # 本文档
└── src/spec/
    └── llm_generator.py               # 核心 LLM 生成器

技术架构

核心组件

LLMGenerator: 主要的规约生成器类
GenerationRequest: 生成请求封装
GenerationResult: 生成结果封装
PromptBuilder: 提示词构建器
SpecValidator: 规约验证器

工作流程

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

扩展开发

添加新的验证目标

在 GenerationRequest 的 verification_goals 中添加新的目标类型：

verification_goals=[
    'functional_correctness',
    'memory_safety',
    'custom_verification_goal'  # 新目标
]

自定义提示词

修改 src/spec/prompt_builder.py 中的提示词模板，或使用 context 参数传递自定义提示词。

集成其他模型

修改 LLMGenerator 类的初始化参数，支持其他 LLM 模型：

generator = LLMGenerator(
    model='your-custom-model',
    base_url='your-api-endpoint'
)

性能优化

1. 并发处理

使用批量生成功能提高处理效率：

# 并发处理多个函数
batch_requests = [create_request(func) for func in functions]
results = await generator.generate_batch_specifications(batch_requests)

2. 缓存机制

启用结果缓存避免重复生成：

# 生成结果会自动缓存
result = await generator.generate_specification(request)

3. 参数调优

根据使用场景调整生成参数：

# 高精度模式（适合复杂函数）
generator.temperature = 0.3
generator.max_tokens = 8192

# 快速模式（适合简单函数）
generator.temperature = 0.7
generator.max_tokens = 2048

故障排除

日志调试

启用详细日志：

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

API 问题

检查 API 状态和配额：

health = await generator.health_check()
print(f"API 状态: {health['status']}")
print(f"响应时间: {health['api_response_time']:.2f}s")

质量问题

分析低质量规约的原因：

if result.validation_result:
    print(f"验证错误: {result.validation_result.errors}")
    print(f"改进建议: {result.validation_result.suggestions}")

贡献指南

Fork 项目
创建功能分支
提交更改
推送到分支
创建 Pull Request

许可证

本项目采用 MIT 许可证。

7.3 KiB Raw Permalink Blame History Unescape Escape