4.5 KiB

Raw Permalink Blame History Unescape Escape

CodeDetect基础使用教程

概述

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

前提条件

Python 3.8或更高版本
CBMC (C Bounded Model Checker) 安装
基本的C语言知识

第一步：安装

1.1 克隆仓库

git clone https://github.com/your-username/codedetect.git
cd codedetect

1.2 安装Python依赖

pip install -r requirements.txt
pip install -r requirements-dev.txt

1.3 安装CBMC

Ubuntu/Debian:

sudo apt-get update
sudo apt-get install cbmc

macOS:

brew install cbmc

1.4 验证安装

# 检查CBMC安装
cbmc --version

# 检查Python依赖
python -m pytest tests/unit/ -v

第二步：基本使用

2.1 准备测试代码

创建一个简单的C文件 test_function.c：

int add(int a, int b) {
    return a + b;
}

2.2 使用命令行界面

# 运行代码验证
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服务器：

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 使用突变测试

# 生成测试突变
python -m src.main mutate test_function.c --function add

# 运行突变验证
python -m src.main verify-mutants test_function.c

4.2 批量处理

# 处理整个目录
python -m src.main batch-verify ./src/

# 生成报告
python -m src.main generate-report --format html

4.3 配置文件

创建配置文件 config.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未找到：

# 确保CBMC在PATH中
which cbmc

# 如果没有，手动设置
export CBMC_PATH=/path/to/cbmc

Python依赖问题：

# 重新安装依赖
pip install --force-reinstall -r requirements.txt

内存不足：

# 减少验证深度
python -m src.main verify test.c --unwind 5

5.2 性能优化

使用 --unwind 限制递归深度
增加 --timeout 防止长时间运行
使用 --jobs 进行并行处理

第六步：最佳实践

6.1 编写可验证的代码

// 好的实践：包含边界检查
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流程中：

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

下一步

完成本教程后，您可以：

获取帮助

查看用户手册
提交 Issue
加入社区讨论

4.5 KiB Raw Permalink Blame History Unescape Escape