cbmc/codedetect/docs/tutorials/basic_usage.md

CodeDetect基础使用教程

概述

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

目录

1. 环境准备
2. 安装CodeDetect
3. 配置CBMC
4. 第一个验证示例
5. Web界面使用
6. API使用
7. 常见问题

环境准备

系统要求

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

必需软件

# 更新系统包管理器
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

创建虚拟环境

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

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

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

安装CodeDetect

从源码安装

# 克隆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 .

验证安装

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

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

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

配置CBMC

安装CBMC

Ubuntu/Debian

# 方法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

# 使用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安装

# 检查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代码文件

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

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

使用命令行工具

# 返回项目根目录
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. 边界检查: 验证边界条件下的行为

生成的规范大致如下：

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服务器

# 启动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提供实时更新：

// 连接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. 文件上传

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

响应示例：

{
  "success": true,
  "data": {
    "file_id": "file_123456789",
    "filename": "add_function.c",
    "size": 156,
    "functions": ["add"],
    "complexity": 0.2
  }
}

2. 代码解析

# 解析已上传的文件
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. 规范生成

# 生成验证规范
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. 运行验证

# 运行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客户端

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客户端

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())

高级示例

复杂函数验证

// 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;
}

运行验证：

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

使用突变测试

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 命令找不到 解决方案:

# 检查是否安装
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 失败 解决方案:

# 更新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验证过程超时 解决方案:

# 增加超时时间
python -m src.cli.main --file test.c --function test --timeout 60

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

Q4: 内存不足

问题: CBMC运行时内存不足 解决方案:

# 限制验证深度
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 解决方案:

# 检查端口是否被占用
netstat -tulpn | grep :8080

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

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

下一步

完成本教程后，您可以：

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

获取帮助

• 📧 邮件支持: support@codedetect.com
• 🐛 问题报告: GitHub Issues
• 📖 在线文档: docs.codedetect.com
• 💬 社区讨论: GitHub Discussions

---

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