cbmc/codedetect

CodeDetect - 代码检测与形式化规范生成系统

基于大语言模型的C/C++代码自动检测和形式化规范生成系统，支持CBMC验证。

功能特性

• 🔍 智能代码分析 - 自动识别代码中的潜在问题和漏洞
• 📋 形式化规范生成 - 基于代码分析生成形式化验证规范
• ✅ CBMC集成验证 - 支持CBMC模型检测器的集成验证
• 🌐 Web用户界面 - 提供友好的Web界面进行代码上传和结果查看
• ⚡ 实时WebSocket通信 - 支持实时进度更新和结果推送
• 🔒 安全验证 - 完善的文件验证和安全检查机制
• 🧪 完整测试框架 - 包含LLM生成测试、单元测试、集成测试、性能测试
• 📊 渐进式测试用例 - 从基础算术到FreeRTOS嵌入式系统的全覆盖测试
• 🎯 质量保证机制 - 语法验证、逻辑一致性、完整性检查、质量评分

系统架构

codedetect/
├── src/
│   ├── ui/                 # Web用户界面
│   │   ├── templates/      # HTML模板
│   │   ├── static/         # 静态资源
│   │   ├── web_app.py      # Flask应用主文件
│   │   ├── utils.py        # 工具类
│   │   └── __main__.py     # CLI入口
│   ├── spec/              # 规范生成模块
│   ├── verify/            # 验证模块
│   └── utils/             # 通用工具
├── config/                # 配置文件
├── tests/                 # 测试用例
│   ├── config/            # 测试配置
│   ├── data/              # 测试数据
│   ├── unit/              # 单元测试
│   ├── integration/       # 集成测试
│   ├── performance/       # 性能测试
│   ├── tools/             # 测试工具
│   └── utils/             # 测试工具
└── scripts/              # 部署脚本

快速开始

环境要求

• Python 3.8+
• CBMC (可选，用于形式化验证)

安装步骤

1. 克隆仓库

   git clone https://gitlink.org.cn/lirenqiu/codedetect.git
   cd codedetect
   

2. 安装依赖

   # 方法1: 使用pip安装
   pip install -r requirements.txt
   
   # 方法2: 使用系统包管理器 (Ubuntu/Debian)
   sudo apt-get update
   sudo apt-get install python3-pip python3-flask
   

3. 配置环境

   cp .env.template .env
   # 编辑 .env 文件，配置API密钥等参数
   

4. 启动服务

   # 方法1: 使用启动脚本 (推荐)
   ./start_server.sh
   
   # 方法2: 使用简化版Flask应用
   python3 simple_app.py
   
   # 方法3: 使用完整版Web应用
   export PYTHONPATH=/home/hzk/桌面/Codedetection:$PYTHONPATH
   python -m src.ui.web_app
   

5. 访问界面 打开浏览器访问以下地址：

   • 主页: http://localhost:8080
   • 工作空间: http://localhost:8080/workspace
   • 上传页面: http://localhost:8080/upload

使用说明

Web界面

工作空间模式 (推荐)

1. 访问工作空间页面: http://localhost:8080/workspace
2. 在6区域统一界面中完成所有操作：
   • 代码导入: 上传C/C++文件或粘贴代码
   • 解析结果: 实时查看代码分析结果
   • 验证配置: 配置CBMC验证参数
   • 实时日志: 监控分析进度和状态
   • 控制面板: 管理工作流程
   • 结果显示: 查看规范生成、验证结果等

传统模式

1. 访问主页: http://localhost:8080
2. 点击"上传代码"进入传统上传页面
3. 选择C/C++源文件（支持.c, .cpp, .h, .hpp格式）
4. 或直接粘贴代码内容
5. 系统自动进行分析和规范生成
6. 查看详细的分析结果和验证报告

支持的文件格式

• 源文件: .c, .cpp, .h, .hpp
• 最大文件大小: 10MB
• 编码格式: UTF-8

命令行接口

# 显示帮助信息
python -m src.ui.__main__ --help

# 创建必要目录
python -m src.ui.__main__ create-dirs

# 启动Web服务器
python -m src.ui.__main__ run

# 使用简化版应用 (推荐)
python3 simple_app.py

# 使用启动脚本 (最简单)
./start_server.sh

配置说明

主要配置文件位于 config/default.yaml：

# 文件上传配置
upload:
  max_file_size: 10MB
  allowed_extensions: [.c, .cpp, .h, .hpp]
  upload_dir: uploads

# API配置
api:
  text_model: gpt-3.5-turbo
  extraction_model: gpt-4
  max_tokens: 2000

# 安全配置
security:
  enable_csp: true
  session_lifetime: 3600

核心模块

文件验证器 (FileValidator)

• 文件类型检查
• 大小限制验证
• 内容安全检查

文件管理器 (FileManager)

• 安全的文件保存
• 文件路径管理
• 清理机制

配置管理 (ConfigManager)

• YAML配置文件解析
• 环境变量支持
• 配置验证

安全特性

• CSP安全头
• 文件名安全处理
• 会话管理
• 输入验证

安全考虑

文件上传安全

• 严格的文件类型限制
• 文件大小控制
• 安全的文件名处理
• 独立的上传目录

Web安全

• Content Security Policy (CSP)
• XSS防护
• CSRF保护
• 安全的会话管理

API安全

• 环境变量配置
• API密钥管理
• 错误处理不暴露敏感信息

开发指南

项目结构

src/
├── ui/                     # Web界面模块
│   ├── templates/          # HTML模板
│   ├── static/             # CSS/JS文件
│   ├── web_app.py          # Flask应用
│   ├── utils.py            # UI工具类
│   └── __main__.py         # CLI入口
├── spec/                   # 规范生成模块
├── verify/                 # 验证模块
└── utils/                  # 通用工具

运行测试

LLM生成测试框架

CodeDetect包含完整的LLM生成测试框架，用于验证CBMC规范生成功能：

# 运行所有测试
./scripts/test-llm-generation.sh

# 运行特定类型测试
./scripts/test-llm-generation.sh basic      # 基础测试
./scripts/test-llm-generation.sh comprehensive # 全面测试
./scripts/test-llm-generation.sh unit       # 单元测试
./scripts/test-llm-generation.sh integration # 集成测试
./scripts/test-llm-generation.sh performance # 性能测试
./scripts/test-llm-generation.sh cli         # CLI测试
./scripts/test-llm-generation.sh validation  # 验证测试

# 使用自定义配置
./scripts/test-llm-generation.sh -c tests/config/test_config.yaml

# 启用详细输出
./scripts/test-llm-generation.sh -v

环境变量设置：

export SILICONFLOW_API_KEY="your_api_key_here"

传统Pytest测试

# 运行所有测试
pytest

# 运行特定测试
pytest tests/unit/
pytest tests/integration/

代码规范

• 遵循PEP 8 Python编码规范
• 使用类型注解
• 编写完整的文档字符串
• 实现单元测试覆盖

部署说明

生产环境部署

1. 环境配置

   export FLASK_ENV=production
   export FLASK_APP=src.ui.web_app
   

2. 使用Gunicorn

   gunicorn -w 4 -b 0.0.0.0:5000 src.ui.web_app:app
   

3. Nginx反向代理

   server {
       listen 80;
       server_name your-domain.com;
   
       location / {
           proxy_pass http://127.0.0.1:5000;
           proxy_set_header Host $host;
           proxy_set_header X-Real-IP $remote_addr;
       }
   }
   

Docker部署

FROM python:3.9-slim

WORKDIR /app
COPY requirements.txt .
RUN pip install -r requirements.txt

COPY . .
EXPOSE 5000

CMD ["gunicorn", "-w", "4", "-b", "0.0.0.0:5000", "src.ui.web_app:app"]

贡献指南

1. Fork本仓库
2. 创建特性分支 (git checkout -b feature/AmazingFeature)
3. 提交更改 (git commit -m 'Add some AmazingFeature')
4. 推送到分支 (git push origin feature/AmazingFeature)
5. 开启Pull Request

许可证

本项目采用MIT许可证 - 查看 LICENSE 文件了解详情。

联系方式

如有问题或建议，请通过以下方式联系：

• 提交Issue: GitLink Issues
• 邮箱: [your-email@example.com]

致谢

感谢所有为本项目做出贡献的开发者和研究人员。

---

更新日志

v1.2.0 (2024-09-14)

• 🧪 新增完整LLM生成测试框架
• 📊 添加渐进式测试用例覆盖
• ⚡ 集成性能测试和基准测试
• 🎯 实现CBMC规范验证工具
• 🔧 添加CLI测试工具和自动化脚本
• 📈 完善质量保证和评分机制

v1.1.0 (2024-09-14)

• 🚀 新增6区域统一工作空间界面
• ⚡ 集成WebSocket实时通信
• 🎨 全面升级用户界面设计
• 📱 新增响应式布局支持
• 🔧 简化安装和启动流程
• 📋 添加启动脚本自动化部署

v1.0.0 (2024-XX-XX)

• 初始版本发布
• 实现基础的代码检测功能
• 添加Web用户界面
• 集成CBMC验证支持