649 lines
14 KiB
Markdown
649 lines
14 KiB
Markdown
# 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月* |