cbmc/codedetect/docs/tutorials/basic_usage.md

# CodeDetect基础使用教程

## 概述

本教程将指导您完成CodeDetect的基础使用，从安装配置到运行第一次代码验证。

## 目录

1. [环境准备](#环境准备)
2. [安装CodeDetect](#安装codedetect)
3. [配置CBMC](#配置cbmc)
4. [第一个验证示例](#第一个验证示例)
5. [Web界面使用](#web界面使用)
6. [API使用](#api使用)
7. [常见问题](#常见问题)

## 环境准备

### 系统要求

- **操作系统**: Linux (推荐Ubuntu 20.04+), macOS 10.15+, Windows 10+ (WSL2)
- **Python**: 3.8+
- **内存**: 最少4GB，推荐8GB+
- **存储**: 最少2GB可用空间

### 必需软件

```bash
# 更新系统包管理器
sudo apt update && sudo apt upgrade -y

# 安装Python和pip
sudo apt install python3 python3-pip python3-venv -y

# 安装Git
sudo apt install git -y

# 安装构建工具
sudo apt install build-essential cmake -y
```

### 创建虚拟环境

```bash
# 创建项目目录
mkdir codedetect-workspace
cd codedetect-workspace

# 创建Python虚拟环境
python3 -m venv codedetect-env
source codedetect-env/bin/activate

# 验证虚拟环境
python --version
pip --version
```

## 安装CodeDetect

### 从源码安装

```bash
# 克隆CodeDetect仓库
git clone https://github.com/codedetect/codedetect.git
cd codedetect

# 安装开发依赖
pip install -r requirements.txt
pip install -r requirements-dev.txt

# 安装CodeDetect
pip install -e .
```

### 验证安装

```bash
# 验证CodeDetect安装
python -c "import src; print('CodeDetect installed successfully')"

# 检查CBMC是否可用
cbmc --version

# 如果CBMC未安装，请参考CBMC集成指南
```

## 配置CBMC

### 安装CBMC

#### Ubuntu/Debian
```bash
# 方法1: 使用apt安装
sudo apt install cbmc -y

# 方法2: 从源码编译（推荐最新版本）
sudo apt install build-essential cmake flex bison -y
git clone https://github.com/diffblue/cbmc.git
cd cbmc
mkdir build && cd build
cmake ..
make -j$(nproc)
sudo make install
```

#### macOS
```bash
# 使用Homebrew安装
brew install cbmc

# 或从源码编译
brew install cmake flex bison
git clone https://github.com/diffblue/cbmc.git
cd cbmc
mkdir build && cd build
cmake ..
make -j$(nproc)
sudo make install
```

### 验证CBMC安装

```bash
# 检查CBMC版本
cbmc --version

# 创建简单测试文件
cat > test.c << 'EOF'
int add(int a, int b) {
    return a + b;
}
EOF

# 测试CBMC基本功能
cbmc test.c --function add --show-properties
```

## 第一个验证示例

### 创建C代码文件

```bash
# 创建示例代码目录
mkdir examples && cd examples

# 创建简单的加法函数
cat > add_function.c << 'EOF'
/**
 * 简单的加法函数
 * @param a 第一个整数
 * @param b 第二个整数
 * @return 两数之和
 */
int add(int a, int b) {
    return a + b;
}
EOF
```

### 使用命令行工具

```bash
# 返回项目根目录
cd ../../

# 使用CodeDetect CLI进行验证
python -m src.cli.main --file examples/add_function.c --function add

# 或者使用测试运行脚本
chmod +x scripts/run_tests.sh
./scripts/run_tests.sh --module=verify --verbose
```

### 预期输出

```
🚀 CodeDetect CLI
================
📁 正在解析文件: examples/add_function.c
🔍 找到函数: add
📋 生成验证规范...
✅ 规范生成完成
🔬 运行CBMC验证...
✅ 验证成功!
📊 结果摘要:
- 状态: 成功
- 执行时间: 0.45s
- 验证属性: 3
- 通过属性: 3
- 失败属性: 0
```

### 理解验证结果

CodeDetect会自动生成CBMC验证规范，包括：

1. **输入约束**: 限制输入参数范围以防止溢出
2. **基本正确性**: 验证函数返回预期结果
3. **边界检查**: 验证边界条件下的行为

生成的规范大致如下：

```c
void add_test() {
    int a = __CPROVER_nondet_int();
    int b = __CPROVER_nondet_int();

    // 添加合理的边界约束
    __CPROVER_assume(a >= -1000 && a <= 1000);
    __CPROVER_assume(b >= -1000 && b <= 1000);

    int result = add(a, b);

    // 验证基本正确性
    __CPROVER_assert(result == a + b, "addition_correct");

    // 验证溢出检查
    if (a > 0 && b > 0) {
        __CPROVER_assert(result > a, "no_positive_overflow");
    }
    if (a < 0 && b < 0) {
        __CPROVER_assert(result < a, "no_negative_overflow");
    }
}
```

## Web界面使用

### 启动Web服务器

```bash
# 启动CodeDetect Web界面
python -m src.ui.app --host 0.0.0.0 --port 8080 --debug
```

### 访问Web界面

打开浏览器访问: `http://localhost:8080`

### 使用步骤

1. **文件上传**
   - 点击"Upload File"按钮
   - 选择C源文件
   - 支持多文件上传

2. **代码解析**
   - 系统自动解析代码结构
   - 识别函数和变量
   - 显示复杂度分析

3. **验证配置**
   - 选择要验证的函数
   - 配置验证参数
   - 选择验证类型

4. **运行验证**
   - 点击"Start Verification"按钮
   - 实时查看验证进度
   - 查看详细结果

5. **结果分析**
   - 查看验证状态
   - 分析失败原因
   - 下载详细报告

### WebSocket实时通信

Web界面使用WebSocket提供实时更新：

```javascript
// 连接WebSocket
const socket = new WebSocket('ws://localhost:8080/ws');

// 监听验证进度
socket.onmessage = (event) => {
    const data = JSON.parse(event.data);
    if (data.event === 'verification_progress') {
        updateProgress(data.data.progress);
    }
};

// 发送验证请求
function startVerification(fileId, functionId) {
    socket.send(JSON.stringify({
        event: 'start_verification',
        data: {
            file_id: fileId,
            function_id: functionId
        }
    }));
}
```

## API使用

### REST API基础

#### 1. 文件上传

```bash
# 使用curl上传文件
curl -X POST http://localhost:8080/api/upload \
  -F "file=@examples/add_function.c" \
  -H "Authorization: Bearer your-api-token"
```

响应示例：
```json
{
  "success": true,
  "data": {
    "file_id": "file_123456789",
    "filename": "add_function.c",
    "size": 156,
    "functions": ["add"],
    "complexity": 0.2
  }
}
```

#### 2. 代码解析

```bash
# 解析已上传的文件
curl -X POST http://localhost:8080/api/parse \
  -H "Content-Type: application/json" \
  -H "Authorization: Bearer your-api-token" \
  -d '{
    "file_id": "file_123456789"
  }'
```

#### 3. 规范生成

```bash
# 生成验证规范
curl -X POST http://localhost:8080/api/generate \
  -H "Content-Type: application/json" \
  -H "Authorization: Bearer your-api-token" \
  -d '{
    "file_id": "file_123456789",
    "functions": [{"name": "add", "complexity_score": 0.2}]
  }'
```

#### 4. 运行验证

```bash
# 运行CBMC验证
curl -X POST http://localhost:8080/api/verify \
  -H "Content-Type: application/json" \
  -H "Authorization: Bearer your-api-token" \
  -d '{
    "file_id": "file_123456789",
    "function_name": "add",
    "specification": "void add_test() { ... }"
  }'
```

### Python客户端

```python
import asyncio
import aiohttp
import json

class CodeDetectClient:
    def __init__(self, base_url="http://localhost:8080", api_token="your-token"):
        self.base_url = base_url
        self.headers = {"Authorization": f"Bearer {api_token}"}

    async def upload_file(self, file_path):
        """上传文件"""
        async with aiohttp.ClientSession() as session:
            with open(file_path, 'rb') as f:
                data = aiohttp.FormData()
                data.add_field('file', f, filename=file_path.name)

                async with session.post(
                    f"{self.base_url}/api/upload",
                    headers=self.headers,
                    data=data
                ) as response:
                    return await response.json()

    async def verify_function(self, file_id, function_name):
        """验证函数"""
        async with aiohttp.ClientSession() as session:
            payload = {
                "file_id": file_id,
                "function_name": function_name
            }

            async with session.post(
                f"{self.base_url}/api/verify",
                headers=self.headers,
                json=payload
            ) as response:
                return await response.json()

# 使用示例
async def main():
    client = CodeDetectClient()

    # 上传文件
    upload_result = await client.upload_file("examples/add_function.c")
    file_id = upload_result["data"]["file_id"]

    # 验证函数
    verification_result = await client.verify_function(file_id, "add")
    print(f"验证结果: {verification_result}")

if __name__ == "__main__":
    asyncio.run(main())
```

### WebSocket客户端

```python
import asyncio
import websockets
import json

async def websocket_client():
    uri = "ws://localhost:8080/ws"

    async with websockets.connect(uri) as websocket:
        # 发送验证请求
        request = {
            "event": "start_verification",
            "data": {
                "file_id": "file_123456789",
                "function_name": "add"
            }
        }
        await websocket.send(json.dumps(request))

        # 监听实时更新
        async for message in websocket:
            data = json.loads(message)
            print(f"收到消息: {data['event']}")

            if data['event'] == 'verification_progress':
                progress = data['data']['progress']
                print(f"验证进度: {progress}%")

            elif data['event'] == 'verification_result':
                result = data['data']
                print(f"验证完成: {result['status']}")
                break

if __name__ == "__main__":
    asyncio.run(websocket_client())
```

## 高级示例

### 复杂函数验证

```c
// complex_function.c
#include <stdlib.h>
#include <string.h>

/**
 * 数组处理函数
 * @param arr 输入数组
 * @param size 数组大小
 * @param value 要查找的值
 * @return 找到的索引，未找到返回-1
 */
int find_index(int* arr, int size, int value) {
    if (!arr || size <= 0) {
        return -1;
    }

    for (int i = 0; i < size; i++) {
        if (arr[i] == value) {
            return i;
        }
    }

    return -1;
}
```

运行验证：

```bash
python -m src.cli.main --file examples/complex_function.c --function find_index
```

### 使用突变测试

```python
from src.mutate.engine import MutationEngine
from src.verify.cbmc_runner import CBMCRunner

async def mutation_example():
    # 创建突变引擎
    engine = MutationEngine()

    # 基础规范
    base_spec = """
    void find_index_test() {
        int arr[5] = {1, 2, 3, 4, 5};
        int size = 5;
        int value = 3;
        int result = find_index(arr, size, value);
        __CPROVER_assert(result == 2, "find_correct");
    }
    """

    # 函数元数据
    metadata = [{
        "name": "find_index",
        "complexity_score": 0.6,
        "parameters": [
            {"name": "arr", "type": "int*"},
            {"name": "size", "type": "int"},
            {"name": "value", "type": "int"}
        ]
    }]

    # 生成突变
    mutations = engine.generate_mutations(
        base_spec,
        metadata,
        max_mutations=5
    )

    print(f"生成了 {len(mutations)} 个突变规范")

    # 运行验证
    runner = CBMCRunner()
    for i, mutation in enumerate(mutations):
        print(f"\n突变 {i+1}:")
        print(f"类型: {mutation.mutation_type}")
        print(f"置信度: {mutation.confidence:.2f}")

        result = await runner.run_verification(
            function_metadata={"name": "find_index"},
            source_file="examples/complex_function.c",
            specification=mutation.specification
        )

        print(f"结果: {result.status}")

if __name__ == "__main__":
    asyncio.run(mutation_example())
```

## 常见问题

### Q1: CBMC安装失败

**问题**: `cbmc --version` 命令找不到
**解决方案**:
```bash
# 检查是否安装
which cbmc

# 如果未安装，从源码编译
git clone https://github.com/diffblue/cbmc.git
cd cbmc && mkdir build && cd build
cmake ..
make -j$(nproc)
sudo make install
```

### Q2: Python依赖安装失败

**问题**: `pip install -r requirements.txt` 失败
**解决方案**:
```bash
# 更新pip
pip install --upgrade pip

# 使用国内镜像源
pip install -r requirements.txt -i https://pypi.tuna.tsinghua.edu.cn/simple/

# 逐个安装依赖
pip install pytest aiohttp flask flask-socketio
```

### Q3: 验证超时

**问题**: CBMC验证过程超时
**解决方案**:
```bash
# 增加超时时间
python -m src.cli.main --file test.c --function test --timeout 60

# 或者调整CBMC参数
cbmc test.c --function test --unwind 5 --depth 10
```

### Q4: 内存不足

**问题**: CBMC运行时内存不足
**解决方案**:
```bash
# 限制验证深度
cbmc test.c --function test --depth 5

# 或者增加系统内存
# 在Linux上创建swap文件
sudo fallocate -l 2G /swapfile
sudo chmod 600 /swapfile
sudo mkswap /swapfile
sudo swapon /swapfile
```

### Q5: Web界面无法访问

**问题**: 浏览器无法访问 `http://localhost:8080`
**解决方案**:
```bash
# 检查端口是否被占用
netstat -tulpn | grep :8080

# 使用其他端口
python -m src.ui.app --port 8081

# 检查防火墙设置
sudo ufw status
sudo ufw allow 8080
```

## 下一步

完成本教程后，您可以：

1. **探索更多示例** 查看 `examples/` 目录中的更多验证示例
2. **学习FreeRTOS验证** 参考 [FreeRTOS验证教程](freertos_verification.md)
3. **阅读开发者指南** 了解如何扩展和定制CodeDetect
4. **运行完整测试套件** 使用 `scripts/run_tests.sh all` 运行所有测试

## 获取帮助

- 📧 **邮件支持**: support@codedetect.com
- 🐛 **问题报告**: [GitHub Issues](https://github.com/codedetect/codedetect/issues)
- 📖 **在线文档**: [docs.codedetect.com](https://docs.codedetect.com)
- 💬 **社区讨论**: [GitHub Discussions](https://github.com/codedetect/codedetect/discussions)

---

*本教程最后更新: 2024年1月*