262 lines
4.5 KiB
Markdown
262 lines
4.5 KiB
Markdown
# 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)
|
||
- 加入社区讨论 |