17 KiB

Raw Permalink Blame History Unescape Escape

CodeDetect 用户手册

简介

CodeDetect是一个基于形式化验证的C/C++代码分析和验证系统，结合了大型语言模型(LLM)和CBMC模型检查器，为开发者提供强大的代码验证工具。

主要功能

代码解析：自动分析C/C++代码结构
规范生成：使用LLM生成形式化验证规范
规范突变：智能生成变异的验证规范
CBMC验证：使用业界标准的CBMC工具进行验证
结果分析：详细的验证结果和反例分析
FreeRTOS支持：专门的嵌入式系统验证支持

系统架构

┌─────────────────┐    ┌─────────────────┐    ┌─────────────────┐
│   Web界面       │    │   REST API       │    │   WebSocket      │
└─────────────────┘    └─────────────────┘    └─────────────────┘
         │                       │                       │
         ▼                       ▼                       ▼
┌─────────────────┐    ┌─────────────────┐    ┌─────────────────┐
│   工作流管理     │    │   作业管理       │    │   实时通信       │
└─────────────────┘    └─────────────────┘    └─────────────────┘
         │                       │                       │
         ▼                       ▼                       ▼
┌─────────────────┐    ┌─────────────────┐    ┌─────────────────┐
│   代码解析       │    │   LLM生成       │    │   规范突变       │
└─────────────────┘    └─────────────────┘    └─────────────────┘
         │                       │                       │
         └───────────────────────┼───────────────────────┘
                                 ▼
                        ┌─────────────────┐
                        │   CBMC验证       │
                        └─────────────────┘

安装指南

系统要求

操作系统：Linux (推荐Ubuntu 20.04+)
Python：3.8+
内存：最少4GB，推荐8GB+
存储：最少2GB可用空间
网络：需要访问LLM服务的网络连接

依赖安装

Python依赖：

pip install -r requirements.txt

CBMC安装：

# Ubuntu/Debian
sudo apt-get install cbmc

# 或者从源码编译
git clone https://github.com/diffblue/cbmc.git
cd cbmc
mkdir build && cd build
cmake ..
make
sudo make install

FreeRTOS支持（可选）：

# 下载FreeRTOS源码
git clone https://github.com/FreeRTOS/FreeRTOS.git
export FREERTOS_PATH=/path/to/FreeRTOS

配置文件

创建或修改 config/default.yaml：

# LLM配置
llm:
  provider: "deepseek"  # 或其他支持的提供商
  model: "deepseek-coder"
  api_key: "your-api-key"
  max_tokens: 2000
  temperature: 0.3

# CBMC配置
cbmc:
  path: "cbmc"
  timeout: 300
  memory_model: "little-endian"
  output_format: "text"
  max_concurrent_jobs: 4

# Web界面配置
web:
  host: "0.0.0.0"
  port: 8080
  debug: false
  max_file_size: "10MB"
  allowed_extensions: [".c", ".cpp", ".h", ".hpp"]

# 工作流配置
workflow:
  default_mode: "standard"
  enable_parsing: true
  enable_generation: true
  enable_mutation: true
  enable_verification: true
  quality_threshold: 0.7

快速开始

启动服务

启动Web服务：

python src/ui/web_app.py

访问Web界面：打开浏览器访问 http://localhost:8080

基本使用流程

上传代码：
- 在Web界面点击"Upload"标签
- 选择C/C++文件或直接粘贴代码
- 点击"Upload"按钮
代码解析：
- 系统自动解析上传的代码
- 生成函数元数据和分析结果
- 显示在解析结果页面
生成规范：
- 基于解析结果生成CBMC验证规范
- 支持多种验证类型选择
- 可自定义生成选项
规范突变：
- 自动生成规范的变异版本
- 提高验证的覆盖率
- 支持不同突变策略
CBMC验证：
- 运行CBMC验证工具
- 生成详细的验证报告
- 包含成功/失败状态和反例

Web界面使用

主界面

CodeDetect提供6个区域的工作空间：

代码上传区：上传C/C++文件或粘贴代码
解析结果区：显示代码分析结果
规范生成区：LLM生成的验证规范
规范突变区：生成的变异规范
验证结果区：CBMC验证结果
统计分析区：验证统计和质量指标

文件上传

支持的文件类型

C源文件：.c
C++源文件：.cpp, .cxx, .cc
头文件：.h, .hpp
最大文件大小：10MB

上传方式

文件上传：选择本地文件上传
代码粘贴：直接在文本框中粘贴代码

工作空间功能

1. 代码解析区

显示代码解析结果，包括：

函数列表和详细信息
变量和数据结构
复杂度分析
依赖关系

2. 规范生成区

显示LLM生成的验证规范：

规范内容
生成置信度
验证目标
质量评估

3. 规范突变区

显示生成的变异规范：

突变类型
突变置信度
与原规范的差异
质量评分

4. 验证结果区

显示CBMC验证结果：

验证状态（成功/失败/超时）
验证时间
内存使用情况
反例信息（如果失败）

5. 统计分析区

显示验证统计信息：

验证成功率
平均验证时间
覆盖的验证类型
质量趋势

实时进度跟踪

所有操作都支持实时进度跟踪：

WebSocket实时更新
进度条显示
详细状态信息
错误消息提示

API参考

认证

API使用Bearer Token认证：

Authorization: Bearer your-token

端点列表

文件上传

POST /api/upload
Content-Type: multipart/form-data

file: [C/C++文件]

代码解析

POST /api/parse
Content-Type: application/json

{
  "file_path": "/path/to/file.c",
  "options": {
    "include_functions": true,
    "include_variables": true,
    "complexity_analysis": true
  }
}

规范生成

POST /api/generate
Content-Type: application/json

{
  "functions": [
    {
      "name": "function_name",
      "return_type": "int",
      "parameters": [
        {"name": "param1", "type": "int"}
      ],
      "complexity_score": 0.5
    }
  ],
  "options": {
    "verification_types": ["memory_safety", "overflow_detection"],
    "include_comments": true
  }
}

规范突变

POST /api/mutate
Content-Type: application/json

{
  "specification": "void test(int x) { __CPROVER_assume(x > 0); }",
  "function_name": "test",
  "options": {
    "mutation_types": ["predicate", "boundary"],
    "max_mutations": 10,
    "quality_threshold": 0.7
  }
}

CBMC验证

POST /api/verify
Content-Type: application/json

{
  "specification": "void test(int x) { __CPROVER_assert(x > 0, \"positive\"); }",
  "function_name": "test",
  "options": {
    "verification_types": ["memory_safety"],
    "timeout": 300,
    "depth": 20
  }
}

工作流管理

POST /api/workflow
Content-Type: application/json

{
  "source_files": ["/path/to/file.c"],
  "target_functions": ["function1", "function2"],
  "workflow_config": {
    "mode": "standard",
    "enable_parsing": true,
    "enable_generation": true,
    "enable_mutation": true,
    "enable_verification": true
  }
}

WebSocket事件

系统通过WebSocket发送实时事件：

// 连接WebSocket
const socket = io('ws://localhost:8080');

// 监听作业进度
socket.on('job_progress', (data) => {
  console.log(`Job ${data.job_id} progress: ${data.progress.percentage}%`);
});

// 监听工作流更新
socket.on('workflow_update', (data) => {
  console.log(`Workflow ${data.workflow_id} status: ${data.status}`);
});

// 监听错误通知
socket.on('error_notification', (data) => {
  console.error(`Error: ${data.error_message}`);
});

高级功能

自定义验证配置

验证类型

memory_safety：内存安全验证
overflow_detection：整数溢出检测
pointer_validity：指针有效性验证
concurrency：并发性验证
array_bounds：数组边界检查

工作流模式

standard：标准验证流程
comprehensive：全面验证流程
minimal：最小验证流程
freertos_verification：FreeRTOS专用验证

批量处理

批量上传

POST /api/upload/batch
Content-Type: multipart/form-data

files: [多个C/C++文件]

批量验证

POST /api/workflow/batch
Content-Type: application/json

{
  "workflows": [
    {
      "source_files": ["/path/to/file1.c"],
      "target_functions": ["func1"],
      "workflow_config": {...}
    }
  ]
}

结果导出

导出格式

JSON：结构化数据
XML：CBMC兼容格式
HTML：可读性报告
CSV：统计数据

导出API

GET /api/results/{job_id}/export?format=json

FreeRTOS验证

FreeRTOS专用功能

CodeDetect提供专门的FreeRTOS验证支持：

支持的FreeRTOS组件

任务管理：任务创建、删除、调度
队列操作：消息队列、信号量
定时器：软件定时器、硬件定时器
中断处理：中断服务例程
内存管理：堆内存分配

FreeRTOS验证配置

freertos:
  include_headers: ["FreeRTOS.h", "task.h", "queue.h"]
  config_path: "/path/to/FreeRTOSConfig.h"
  heap_size: 4096
  max_tasks: 10
  stack_size: 1024

FreeRTOS示例

任务验证示例

#include "FreeRTOS.h"
#include "task.h"

void vTaskFunction(void *pvParameters) {
    int *param = (int *)pvParameters;

    // CodeDetect将生成以下验证：
    // 1. 参数有效性检查
    // 2. 栈空间验证
    // 3. 任务生命周期验证
    // 4. 并发安全验证

    for (;;) {
        if (*param > 0) {
            (*param)--;
        }
        vTaskDelay(pdMS_TO_TICKS(100));
    }
}

队列验证示例

#include "FreeRTOS.h"
#include "queue.h"

void queue_task(void *pvParameters) {
    QueueHandle_t queue = (QueueHandle_t)pvParameters;
    uint32_t message;

    // CodeDetect将生成：
    // 1. 队列有效性验证
    // 2. 消息完整性检查
    // 3. 并发访问安全
    // 4. 队列溢出保护

    while (xQueueReceive(queue, &message, portMAX_DELAY) == pdPASS) {
        // 处理消息
    }
}

故障排除

常见问题

1. CBMC未找到

错误：CBMC installation error: cbmc not found

解决方案：

# 检查CBMC安装
which cbmc

# 安装CBMC
sudo apt-get install cbmc

# 或设置CBMC路径
export PATH=/path/to/cbmc:$PATH

2. LLM服务连接失败

错误：ExternalServiceError: LLM service unavailable

解决方案：

# 检查网络连接
ping api.example.com

# 检查API密钥
echo $LLM_API_KEY

# 检查配置文件
cat config/default.yaml | grep api_key

3. 文件上传失败

错误：ValidationError: File validation failed

解决方案：

# 检查文件类型
file your_file.c

# 检查文件大小
ls -lh your_file.c

# 检查文件权限
chmod 644 your_file.c

4. 验证超时

错误：TimeoutError: Verification timeout

解决方案：

# 增加超时时间
cbmc:
  timeout: 600  # 10分钟

# 减少验证深度
cbmc:
  depth: 10  # 降低搜索深度

# 限制验证范围
verification:
  unwind: 5  # 限制循环展开

日志调试

启用调试日志

export LOG_LEVEL=DEBUG
python src/ui/web_app.py

查看日志文件

# 查看应用日志
tail -f logs/app.log

# 查看CBMC日志
tail -f logs/cbmc.log

# 查看LLM日志
tail -f logs/llm.log

性能优化

内存优化

# 限制并发作业
cbmc:
  max_concurrent_jobs: 2

# 限制内存使用
cbmc:
  max_memory: "1GB"

# 优化搜索策略
cbmc:
  search_strategy: "breadth_first"

网络优化

# 启用连接池
llm:
  connection_pool_size: 5

# 设置超时
llm:
  timeout: 30

# 启用缓存
cache:
  enabled: true
  ttl: 3600

最佳实践

代码准备

1. 代码质量

使用清晰的函数和变量命名
添加适当的注释
避免复杂的宏定义
减少代码重复

2. 验证准备

分离验证相关的代码
添加前提条件检查
使用防御性编程
避免未定义行为

验证策略

1. 渐进式验证

// 1. 基本功能验证
int basic_function(int x) {
    return x + 1;
}

// 2. 边界条件验证
int boundary_function(int x) {
    if (x > 0 && x < 100) {
        return x * 2;
    }
    return 0;
}

// 3. 复杂逻辑验证
int complex_function(int *array, int size) {
    if (array == NULL || size <= 0) {
        return -1;
    }

    int sum = 0;
    for (int i = 0; i < size; i++) {
        sum += array[i];
    }
    return sum;
}

2. 验证目标设置

# 根据代码复杂度设置验证目标
verification:
  simple_functions:
    types: ["memory_safety"]
    timeout: 60

  complex_functions:
    types: ["memory_safety", "overflow_detection", "pointer_validity"]
    timeout: 300

  critical_functions:
    types: ["memory_safety", "overflow_detection", "pointer_validity", "concurrency"]
    timeout: 600

结果分析

1. 成功验证

检查验证覆盖率
分析时间性能
比较不同验证策略

2. 失败验证

分析反例路径
检查前置条件
修复代码问题

3. 超时处理

简化验证条件
增加超时时间
分解复杂函数

持续集成

1. 自动化测试

# .github/workflows/verify.yml
name: Code Verification
on: [push, pull_request]

jobs:
  verify:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v2
      - name: Setup CodeDetect
        run: |
          pip install -r requirements.txt
          sudo apt-get install cbmc          
      - name: Run Verification
        run: |
          python scripts/run-verification.py src/          
      - name: Generate Report
        run: |
          python scripts/generate-report.py

2. 质量门控

quality_gates:
  min_coverage: 0.8
  max_timeout_rate: 0.1
  min_success_rate: 0.9
  max_memory_usage: "2GB"

附录

配置文件完整示例

# config/default.yaml
llm:
  provider: "deepseek"
  model: "deepseek-coder"
  api_key: "${LLM_API_KEY}"
  max_tokens: 2000
  temperature: 0.3
  timeout: 30
  retry_attempts: 3

cbmc:
  path: "cbmc"
  timeout: 300
  memory_model: "little-endian"
  output_format: "text"
  max_concurrent_jobs: 4
  search_strategy: "depth_first"
  unwind: 10
  depth: 20

web:
  host: "0.0.0.0"
  port: 8080
  debug: false
  max_file_size: "10MB"
  allowed_extensions: [".c", ".cpp", ".h", ".hpp"]
  session_timeout: 3600

workflow:
  default_mode: "standard"
  enable_parsing: true
  enable_generation: true
  enable_mutation: true
  enable_verification: true
  quality_threshold: 0.7
  max_mutations: 20
  max_selected_mutations: 10

freertos:
  include_headers: ["FreeRTOS.h", "task.h", "queue.h", "semphr.h"]
  config_path: "${FREERTOS_PATH}/FreeRTOSConfig.h"
  heap_size: 4096
  max_tasks: 10
  stack_size: 1024

cache:
  enabled: true
  ttl: 3600
  max_size: 1000

logging:
  level: "INFO"
  file: "logs/app.log"
  max_size: "10MB"
  backup_count: 5

quality_gates:
  min_coverage: 0.8
  max_timeout_rate: 0.1
  min_success_rate: 0.9
  max_memory_usage: "2GB"

常用命令

# 启动服务
python src/ui/web_app.py

# 运行测试
pytest tests/

# 生成文档
python scripts/generate-docs.py

# 清理缓存
python scripts/cleanup.py

# 查看系统状态
curl http://localhost:8080/api/status

# 查看帮助
python src/ui/web_app.py --help

支持和社区

文档：https://docs.codedetect.com
问题报告：GitHub Issues
讨论：GitHub Discussions
邮件：support@codedetect.com

最后更新：2024年1月

17 KiB Raw Permalink Blame History Unescape Escape

CodeDetect 用户手册

目录

简介

主要功能

系统架构

安装指南

系统要求

依赖安装

配置文件

快速开始

启动服务

基本使用流程

Web界面使用

主界面

文件上传

支持的文件类型

上传方式

工作空间功能

1. 代码解析区

2. 规范生成区

3. 规范突变区

4. 验证结果区

5. 统计分析区

实时进度跟踪

API参考

认证

端点列表

文件上传

代码解析

规范生成

规范突变

CBMC验证

工作流管理

WebSocket事件

高级功能

自定义验证配置

验证类型

工作流模式

批量处理

批量上传

批量验证

结果导出

导出格式

导出API

FreeRTOS验证

FreeRTOS专用功能

支持的FreeRTOS组件

FreeRTOS验证配置

FreeRTOS示例

任务验证示例

队列验证示例

故障排除

常见问题

1. CBMC未找到

2. LLM服务连接失败

3. 文件上传失败

4. 验证超时

日志调试

启用调试日志

查看日志文件

性能优化

内存优化

网络优化

最佳实践

代码准备

1. 代码质量

2. 验证准备

验证策略

1. 渐进式验证

2. 验证目标设置

结果分析

1. 成功验证

2. 失败验证

3. 超时处理

持续集成

1. 自动化测试

2. 质量门控

附录

配置文件完整示例

17 KiB

Raw Permalink Blame History Unescape Escape