cbmc/codedetect/docs/user-manual.md

# CodeDetect 用户手册

## 目录

1. [简介](#简介)
2. [安装指南](#安装指南)
3. [快速开始](#快速开始)
4. [Web界面使用](#web界面使用)
5. [API参考](#api参考)
6. [高级功能](#高级功能)
7. [FreeRTOS验证](#freertos验证)
8. [故障排除](#故障排除)
9. [最佳实践](#最佳实践)

## 简介

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服务的网络连接

### 依赖安装

1. **Python依赖**：
```bash
pip install -r requirements.txt
```

2. **CBMC安装**：
```bash
# 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
```

3. **FreeRTOS支持**（可选）：
```bash
# 下载FreeRTOS源码
git clone https://github.com/FreeRTOS/FreeRTOS.git
export FREERTOS_PATH=/path/to/FreeRTOS
```

### 配置文件

创建或修改 `config/default.yaml`：

```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
```

## 快速开始

### 启动服务

1. **启动Web服务**：
```bash
python src/ui/web_app.py
```

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

### 基本使用流程

1. **上传代码**：
   - 在Web界面点击"Upload"标签
   - 选择C/C++文件或直接粘贴代码
   - 点击"Upload"按钮

2. **代码解析**：
   - 系统自动解析上传的代码
   - 生成函数元数据和分析结果
   - 显示在解析结果页面

3. **生成规范**：
   - 基于解析结果生成CBMC验证规范
   - 支持多种验证类型选择
   - 可自定义生成选项

4. **规范突变**：
   - 自动生成规范的变异版本
   - 提高验证的覆盖率
   - 支持不同突变策略

5. **CBMC验证**：
   - 运行CBMC验证工具
   - 生成详细的验证报告
   - 包含成功/失败状态和反例

## Web界面使用

### 主界面

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

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

### 文件上传

#### 支持的文件类型
- C源文件：`.c`
- C++源文件：`.cpp`, `.cxx`, `.cc`
- 头文件：`.h`, `.hpp`
- 最大文件大小：10MB

#### 上传方式
1. **文件上传**：选择本地文件上传
2. **代码粘贴**：直接在文本框中粘贴代码

### 工作空间功能

#### 1. 代码解析区
显示代码解析结果，包括：
- 函数列表和详细信息
- 变量和数据结构
- 复杂度分析
- 依赖关系

#### 2. 规范生成区
显示LLM生成的验证规范：
- 规范内容
- 生成置信度
- 验证目标
- 质量评估

#### 3. 规范突变区
显示生成的变异规范：
- 突变类型
- 突变置信度
- 与原规范的差异
- 质量评分

#### 4. 验证结果区
显示CBMC验证结果：
- 验证状态（成功/失败/超时）
- 验证时间
- 内存使用情况
- 反例信息（如果失败）

#### 5. 统计分析区
显示验证统计信息：
- 验证成功率
- 平均验证时间
- 覆盖的验证类型
- 质量趋势

### 实时进度跟踪

所有操作都支持实时进度跟踪：
- WebSocket实时更新
- 进度条显示
- 详细状态信息
- 错误消息提示

## API参考

### 认证

API使用Bearer Token认证：
```http
Authorization: Bearer your-token
```

### 端点列表

#### 文件上传
```http
POST /api/upload
Content-Type: multipart/form-data

file: [C/C++文件]
```

#### 代码解析
```http
POST /api/parse
Content-Type: application/json

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

#### 规范生成
```http
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
  }
}
```

#### 规范突变
```http
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验证
```http
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
  }
}
```

#### 工作流管理
```http
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发送实时事件：

```javascript
// 连接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专用验证

### 批量处理

#### 批量上传
```http
POST /api/upload/batch
Content-Type: multipart/form-data

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

#### 批量验证
```http
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
```http
GET /api/results/{job_id}/export?format=json
```

## FreeRTOS验证

### FreeRTOS专用功能

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

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

#### FreeRTOS验证配置
```yaml
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示例

#### 任务验证示例
```c
#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));
    }
}
```

#### 队列验证示例
```c
#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`

**解决方案**：
```bash
# 检查CBMC安装
which cbmc

# 安装CBMC
sudo apt-get install cbmc

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

#### 2. LLM服务连接失败
**错误**：`ExternalServiceError: LLM service unavailable`

**解决方案**：
```bash
# 检查网络连接
ping api.example.com

# 检查API密钥
echo $LLM_API_KEY

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

#### 3. 文件上传失败
**错误**：`ValidationError: File validation failed`

**解决方案**：
```bash
# 检查文件类型
file your_file.c

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

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

#### 4. 验证超时
**错误**：`TimeoutError: Verification timeout`

**解决方案**：
```yaml
# 增加超时时间
cbmc:
  timeout: 600  # 10分钟

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

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

### 日志调试

#### 启用调试日志
```bash
export LOG_LEVEL=DEBUG
python src/ui/web_app.py
```

#### 查看日志文件
```bash
# 查看应用日志
tail -f logs/app.log

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

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

### 性能优化

#### 内存优化
```yaml
# 限制并发作业
cbmc:
  max_concurrent_jobs: 2

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

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

#### 网络优化
```yaml
# 启用连接池
llm:
  connection_pool_size: 5

# 设置超时
llm:
  timeout: 30

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

## 最佳实践

### 代码准备

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

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

### 验证策略

#### 1. 渐进式验证
```c
// 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. 验证目标设置
```yaml
# 根据代码复杂度设置验证目标
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. 自动化测试
```yaml
# .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. 质量门控
```yaml
quality_gates:
  min_coverage: 0.8
  max_timeout_rate: 0.1
  min_success_rate: 0.9
  max_memory_usage: "2GB"
```

## 附录

### 配置文件完整示例

```yaml
# 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"
```

### 常用命令

```bash
# 启动服务
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](https://docs.codedetect.com)
- **问题报告**：[GitHub Issues](https://github.com/codedetect/codedetect/issues)
- **讨论**：[GitHub Discussions](https://github.com/codedetect/codedetect/discussions)
- **邮件**：support@codedetect.com

---

*最后更新：2024年1月*