|
|
# CodeDetect基础使用教程
|
|
|
|
|
|
## 概述
|
|
|
|
|
|
本教程将指导您完成CodeDetect的基础使用，从安装配置到运行第一次代码验证。
|
|
|
|
|
|
## 前提条件
|
|
|
|
|
|
- Python 3.8或更高版本
|
|
|
- CBMC (C Bounded Model Checker) 安装
|
|
|
- 基本的C语言知识
|
|
|
|
|
|
## 第一步：安装
|
|
|
|
|
|
### 1.1 克隆仓库
|
|
|
|
|
|
```bash
|
|
|
git clone https://github.com/your-username/codedetect.git
|
|
|
cd codedetect
|
|
|
```
|
|
|
|
|
|
### 1.2 安装Python依赖
|
|
|
|
|
|
```bash
|
|
|
pip install -r requirements.txt
|
|
|
pip install -r requirements-dev.txt
|
|
|
```
|
|
|
|
|
|
### 1.3 安装CBMC
|
|
|
|
|
|
**Ubuntu/Debian:**
|
|
|
```bash
|
|
|
sudo apt-get update
|
|
|
sudo apt-get install cbmc
|
|
|
```
|
|
|
|
|
|
**macOS:**
|
|
|
```bash
|
|
|
brew install cbmc
|
|
|
```
|
|
|
|
|
|
### 1.4 验证安装
|
|
|
|
|
|
```bash
|
|
|
# 检查CBMC安装
|
|
|
cbmc --version
|
|
|
|
|
|
# 检查Python依赖
|
|
|
python -m pytest tests/unit/ -v
|
|
|
```
|
|
|
|
|
|
## 第二步：基本使用
|
|
|
|
|
|
### 2.1 准备测试代码
|
|
|
|
|
|
创建一个简单的C文件 `test_function.c`：
|
|
|
|
|
|
```c
|
|
|
int add(int a, int b) {
|
|
|
return a + b;
|
|
|
}
|
|
|
```
|
|
|
|
|
|
### 2.2 使用命令行界面
|
|
|
|
|
|
```bash
|
|
|
# 运行代码验证
|
|
|
python -m src.main verify test_function.c
|
|
|
|
|
|
# 生成规范
|
|
|
python -m src.main generate-spec test_function.c --function add
|
|
|
|
|
|
# 运行完整分析
|
|
|
python -m src.main analyze test_function.c
|
|
|
```
|
|
|
|
|
|
### 2.3 使用Web界面
|
|
|
|
|
|
启动Web服务器：
|
|
|
|
|
|
```bash
|
|
|
python -m src.ui.web_app
|
|
|
```
|
|
|
|
|
|
然后在浏览器中访问 `http://localhost:5000`
|
|
|
|
|
|
## 第三步：验证结果解读
|
|
|
|
|
|
### 3.1 成功验证
|
|
|
|
|
|
```
|
|
|
VERIFICATION SUCCESSFUL
|
|
|
Property __CPROVER_assert: OK
|
|
|
Property __CPROVER_assert: OK
|
|
|
|
|
|
** 1 of 1 properties verified (2 PASS) **
|
|
|
```
|
|
|
|
|
|
**含义：**
|
|
|
- 所有属性都已验证通过
|
|
|
- 代码在给定条件下是安全的
|
|
|
|
|
|
### 3.2 验证失败
|
|
|
|
|
|
```
|
|
|
VERIFICATION FAILED
|
|
|
Property __CPROVER_assert: FAILED
|
|
|
|
|
|
Violated property:
|
|
|
File test.c, line 2
|
|
|
assertion
|
|
|
arr[index]
|
|
|
|
|
|
STATE:
|
|
|
- Line 2: arr[index]
|
|
|
- index: 5
|
|
|
- size: 3
|
|
|
```
|
|
|
|
|
|
**含义：**
|
|
|
- 发现了潜在的安全问题
|
|
|
- 需要修复代码或添加保护措施
|
|
|
|
|
|
## 第四步：进阶功能
|
|
|
|
|
|
### 4.1 使用突变测试
|
|
|
|
|
|
```bash
|
|
|
# 生成测试突变
|
|
|
python -m src.main mutate test_function.c --function add
|
|
|
|
|
|
# 运行突变验证
|
|
|
python -m src.main verify-mutants test_function.c
|
|
|
```
|
|
|
|
|
|
### 4.2 批量处理
|
|
|
|
|
|
```bash
|
|
|
# 处理整个目录
|
|
|
python -m src.main batch-verify ./src/
|
|
|
|
|
|
# 生成报告
|
|
|
python -m src.main generate-report --format html
|
|
|
```
|
|
|
|
|
|
### 4.3 配置文件
|
|
|
|
|
|
创建配置文件 `config.yaml`：
|
|
|
|
|
|
```yaml
|
|
|
verification:
|
|
|
cbmc:
|
|
|
options:
|
|
|
- "--bounds-check"
|
|
|
- "--pointer-check"
|
|
|
- "--unwind 10"
|
|
|
timeout: 30
|
|
|
|
|
|
generation:
|
|
|
llm:
|
|
|
model: "gpt-4"
|
|
|
temperature: 0.3
|
|
|
max_tokens: 1000
|
|
|
```
|
|
|
|
|
|
## 第五步：故障排除
|
|
|
|
|
|
### 5.1 常见问题
|
|
|
|
|
|
**CBMC未找到：**
|
|
|
```bash
|
|
|
# 确保CBMC在PATH中
|
|
|
which cbmc
|
|
|
|
|
|
# 如果没有，手动设置
|
|
|
export CBMC_PATH=/path/to/cbmc
|
|
|
```
|
|
|
|
|
|
**Python依赖问题：**
|
|
|
```bash
|
|
|
# 重新安装依赖
|
|
|
pip install --force-reinstall -r requirements.txt
|
|
|
```
|
|
|
|
|
|
**内存不足：**
|
|
|
```bash
|
|
|
# 减少验证深度
|
|
|
python -m src.main verify test.c --unwind 5
|
|
|
```
|
|
|
|
|
|
### 5.2 性能优化
|
|
|
|
|
|
- 使用 `--unwind` 限制递归深度
|
|
|
- 增加 `--timeout` 防止长时间运行
|
|
|
- 使用 `--jobs` 进行并行处理
|
|
|
|
|
|
## 第六步：最佳实践
|
|
|
|
|
|
### 6.1 编写可验证的代码
|
|
|
|
|
|
```c
|
|
|
// 好的实践：包含边界检查
|
|
|
int safe_access(int* arr, int size, int index) {
|
|
|
if (arr == NULL || size <= 0 || index < 0 || index >= size) {
|
|
|
return 0;
|
|
|
}
|
|
|
return arr[index];
|
|
|
}
|
|
|
|
|
|
// 避免的做法：没有边界检查
|
|
|
int unsafe_access(int* arr, int size, int index) {
|
|
|
return arr[index]; // 潜在的缓冲区溢出
|
|
|
}
|
|
|
```
|
|
|
|
|
|
### 6.2 规范编写建议
|
|
|
|
|
|
- 使用清晰的断言
|
|
|
- 考虑边界条件
|
|
|
- 添加前置条件
|
|
|
- 记录假设条件
|
|
|
|
|
|
### 6.3 持续集成
|
|
|
|
|
|
将CodeDetect集成到CI/CD流程中：
|
|
|
|
|
|
```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 Python
|
|
|
uses: actions/setup-python@v2
|
|
|
with:
|
|
|
python-version: 3.9
|
|
|
- name: Install dependencies
|
|
|
run: |
|
|
|
pip install -r requirements.txt
|
|
|
sudo apt-get install cbmc
|
|
|
- name: Run verification
|
|
|
run: python -m pytest tests/ -v
|
|
|
```
|
|
|
|
|
|
## 下一步
|
|
|
|
|
|
完成本教程后，您可以：
|
|
|
|
|
|
1. 阅读 [API参考文档](../api-reference.md)
|
|
|
2. 探索 [开发者指南](../developer-guide.md)
|
|
|
3. 查看 [FreeRTOS示例](../freertos-examples/)
|
|
|
4. 尝试 [高级配置选项](../configuration.md)
|
|
|
|
|
|
## 获取帮助
|
|
|
|
|
|
- 查看 [用户手册](../user-manual.md)
|
|
|
- 提交 [Issue](https://github.com/your-username/codedetect/issues)
|
|
|
- 加入社区讨论 |
