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 (可选，用于形式化验证)

安装步骤

克隆仓库

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

安装依赖

# 方法1: 使用pip安装
pip install -r requirements.txt

# 方法2: 使用系统包管理器 (Ubuntu/Debian)
sudo apt-get update
sudo apt-get install python3-pip python3-flask

配置环境

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

启动服务

# 方法1: 使用启动脚本 (推荐)
./start_server.sh

# 方法2: 使用简化版Flask应用
python3 simple_app.py

# 方法3: 使用完整版Web应用
export PYTHONPATH=/home/hzk/桌面/Codedetection:$PYTHONPATH
python -m src.ui.web_app

访问界面 打开浏览器访问以下地址：
- 主页: http://localhost:8080
- 工作空间: http://localhost:8080/workspace
- 上传页面: http://localhost:8080/upload

使用说明

Web界面

工作空间模式 (推荐)

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

传统模式

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

支持的文件格式

源文件: .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编码规范
使用类型注解
编写完整的文档字符串
实现单元测试覆盖

部署说明

生产环境部署

环境配置

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

使用Gunicorn

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

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"]