# CodeDetect API参考文档 本文档提供了CodeDetect系统所有API接口的详细参考,包括REST API、WebSocket事件、内部模块API和配置API。 ## 目录 1. [REST API](#rest-api) 2. [WebSocket事件](#websocket事件) 3. [内部模块API](#内部模块api) 4. [配置API](#配置api) 5. [错误代码](#错误代码) 6. [身份验证](#身份验证) 7. [速率限制](#速率限制) --- ## REST API ### 基础信息 - **基础URL**: `http://localhost:8080/api` - **内容类型**: `application/json` - **认证方式**: Bearer Token - **字符编码**: UTF-8 ### 通用响应格式 所有API响应都遵循以下格式: ```json { "success": true, "data": {}, "message": "操作成功", "timestamp": "2024-01-01T00:00:00Z", "request_id": "req_123456789" } ``` 错误响应格式: ```json { "success": false, "error": { "code": "VALIDATION_ERROR", "message": "请求参数验证失败", "details": {} }, "timestamp": "2024-01-01T00:00:00Z", "request_id": "req_123456789" } ``` ### 文件上传API #### POST /api/upload 上传C/C++文件进行验证。 **请求**: ```http POST /api/upload Content-Type: multipart/form-data file: [C/C++文件] ``` **响应**: ```json { "success": true, "data": { "file_id": "file_123456789", "filename": "test.c", "size": 1024, "type": "c", "uploaded_at": "2024-01-01T00:00:00Z", "checksum": "sha256:abc123...", "temporary_url": "/api/files/file_123456789" } } ``` **错误代码**: - `INVALID_FILE_TYPE`: 不支持的文件类型 - `FILE_TOO_LARGE`: 文件大小超过限制 - `UPLOAD_FAILED`: 上传失败 - `STORAGE_ERROR`: 存储错误 #### POST /api/upload/batch 批量上传多个文件。 **请求**: ```http POST /api/upload/batch Content-Type: multipart/form-data files: [多个C/C++文件] ``` **响应**: ```json { "success": true, "data": { "batch_id": "batch_123456789", "files": [ { "file_id": "file_123456789", "filename": "test1.c", "status": "success" }, { "file_id": "file_987654321", "filename": "test2.c", "status": "success" } ], "total_files": 2, "successful_uploads": 2 } } ``` ### 代码解析API #### POST /api/parse 解析上传的C/C++代码。 **请求**: ```json { "file_path": "/path/to/file.c", "options": { "include_functions": true, "include_variables": true, "include_macros": true, "include_types": true, "complexity_analysis": true, "dependency_analysis": true, "max_functions": 100, "parse_comments": false } } ``` **响应**: ```json { "success": true, "data": { "file_info": { "filename": "test.c", "size": 1024, "lines": 42, "encoding": "utf-8" }, "functions": [ { "name": "add", "return_type": "int", "parameters": [ { "name": "a", "type": "int", "default_value": null }, { "name": "b", "type": "int", "default_value": null } ], "line_start": 1, "line_end": 3, "complexity_score": 0.2, "cyclomatic_complexity": 1, "has_side_effects": false, "is_recursive": false, "calls": [], "called_by": [] } ], "variables": [ { "name": "global_var", "type": "int", "scope": "global", "is_const": false, "is_volatile": false, "initial_value": "0" } ], "types": [ { "name": "Point", "kind": "struct", "fields": [ { "name": "x", "type": "int" }, { "name": "y", "type": "int" } ] } ], "complexity": { "overall_score": 0.3, "max_function_complexity": 0.2, "average_complexity": 0.15, "lines_of_code": 42, "comment_ratio": 0.1 }, "dependencies": [ { "header": "stdio.h", "type": "system", "functions": ["printf", "scanf"] } ] } } ``` #### POST /api/parse/batch 批量解析多个文件。 **请求**: ```json { "file_paths": ["/path/to/file1.c", "/path/to/file2.c"], "options": { "include_functions": true, "cross_file_analysis": true } } ``` ### 规范生成API #### POST /api/generate 基于解析结果生成CBMC验证规范。 **请求**: ```json { "functions": [ { "name": "add", "return_type": "int", "parameters": [ {"name": "a", "type": "int"}, {"name": "b", "type": "int"} ], "complexity_score": 0.2 } ], "options": { "verification_types": ["memory_safety", "overflow_detection"], "include_comments": true, "generate_harness": true, "max_specifications": 10, "confidence_threshold": 0.7, "target_platform": "generic" } } ``` **响应**: ```json { "success": true, "data": { "specifications": [ { "id": "spec_123456789", "function_name": "add", "type": "memory_safety", "specification": "void add_harness() {\n int a = nondet_int();\n int b = nondet_int();\n int result = add(a, b);\n __CPROVER_assert(result >= a && result >= b, \"overflow_check\");\n}", "confidence": 0.85, "description": "内存安全验证:检查整数溢出", "preconditions": ["a != INT_MIN", "b != INT_MIN"], "postconditions": ["result >= a", "result >= b"], "generated_at": "2024-01-01T00:00:00Z" } ], "generation_stats": { "total_specifications": 2, "average_confidence": 0.82, "generation_time": 1.23, "verification_types_covered": ["memory_safety", "overflow_detection"] } } } ``` #### GET /api/generate/templates 获取可用的规范模板。 **响应**: ```json { "success": true, "data": { "templates": [ { "id": "memory_safety", "name": "内存安全验证", "description": "验证内存访问安全性", "category": "safety", "target_types": ["pointer_operations", "array_access", "memory_allocation"] }, { "id": "overflow_detection", "name": "整数溢出检测", "description": "检测整数运算溢出", "category": "safety", "target_types": ["arithmetic_operations", "bitwise_operations"] } ] } } ``` ### 规范突变API #### POST /api/mutate 生成验证规范的变异版本。 **请求**: ```json { "specification": "void test(int x) { __CPROVER_assume(x > 0); }", "function_name": "test", "options": { "mutation_types": ["predicate", "boundary", "arithmetic"], "max_mutations": 10, "quality_threshold": 0.7, "preserve_semantics": true, "generate_coverage": true } } ``` **响应**: ```json { "success": true, "data": { "mutations": [ { "id": "mut_123456789", "specification": "void test(int x) { __CPROVER_assume(x >= 0); }", "mutation_type": "predicate", "confidence": 0.9, "quality_score": 0.85, "description": "边界条件突变:包含等于0的情况", "changes": [ { "type": "operator_change", "from": ">", "to": ">=", "line": 1 } ], "coverage_improvement": 0.15 } ], "mutation_stats": { "total_mutations": 8, "average_quality": 0.78, "types_used": ["predicate", "boundary"], "generation_time": 0.45 } } } ``` #### GET /api/mutate/types 获取可用的突变类型。 **响应**: ```json { "success": true, "data": { "mutation_types": [ { "id": "predicate", "name": "谓词突变", "description": "修改条件表达式中的运算符", "applicable_to": ["assumptions", "assertions"] }, { "id": "boundary", "name": "边界突变", "description": "调整边界条件值", "applicable_to": ["bounds", "limits"] }, { "id": "arithmetic", "name": "算术突变", "description": "修改算术运算", "applicable_to": ["arithmetic_expressions"] } ] } } ``` ### CBMC验证API #### POST /api/verify 运行CBMC验证。 **请求**: ```json { "specification": "void test(int x) { __CPROVER_assert(x > 0, \"positive\"); }", "function_name": "test", "source_file": "/path/to/file.c", "options": { "verification_types": ["memory_safety"], "timeout": 300, "depth": 20, "unwind": 10, "max_threads": 4, "cbmc_options": [ "--bounds-check", "--pointer-check", "--div-by-zero-check" ] } } ``` **响应**: ```json { "success": true, "data": { "result": { "status": "success", "execution_time": 2.34, "memory_used": "256MB", "verification_depth": 15, "properties_checked": 5, "counterexamples": [], "statistics": { "total_vccs": 42, "passed_vccs": 42, "failed_vccs": 0, "timeout_vccs": 0 }, "cbmc_output": "CBMC verification output...", "trace": [], "coverage": { "lines_covered": 15, "branches_covered": 8, "functions_covered": 1, "coverage_percentage": 85.5 } }, "job_info": { "job_id": "job_123456789", "started_at": "2024-01-01T00:00:00Z", "completed_at": "2024-01-01T00:00:02Z", "queue_time": 0.1, "processing_time": 2.24 } } } ``` #### POST /api/verify/batch 批量验证多个规范。 **请求**: ```json { "verifications": [ { "specification": "void test1() { }", "function_name": "test1", "source_file": "file1.c" }, { "specification": "void test2() { }", "function_name": "test2", "source_file": "file2.c" } ], "options": { "max_concurrent": 4, "timeout_per_job": 300 } } ``` ### 工作流API #### POST /api/workflow 启动完整的验证工作流。 **请求**: ```json { "source_files": ["/path/to/file.c"], "target_functions": ["add", "multiply"], "workflow_config": { "mode": "standard", "enable_parsing": true, "enable_generation": true, "enable_mutation": true, "enable_verification": true, "quality_threshold": 0.7, "max_mutations": 10, "timeout": 600 } } ``` **响应**: ```json { "success": true, "data": { "workflow_id": "wf_123456789", "status": "running", "steps": [ { "id": "parse", "name": "代码解析", "status": "completed", "started_at": "2024-01-01T00:00:00Z", "completed_at": "2024-01-01T00:00:01Z", "result": { "functions_found": 5 } }, { "id": "generate", "name": "规范生成", "status": "in_progress", "started_at": "2024-01-01T00:00:01Z" } ], "progress": { "total_steps": 4, "completed_steps": 1, "current_step": 2, "percentage": 25.0 } } } ``` #### GET /api/workflow/{workflow_id} 获取工作流状态。 **响应**: ```json { "success": true, "data": { "workflow_id": "wf_123456789", "status": "completed", "steps": [ { "id": "parse", "name": "代码解析", "status": "completed", "result": {"functions_found": 5} }, { "id": "generate", "name": "规范生成", "status": "completed", "result": {"specifications_generated": 8} }, { "id": "mutate", "name": "规范突变", "status": "completed", "result": {"mutations_generated": 15} }, { "id": "verify", "name": "CBMC验证", "status": "completed", "result": {"verifications_completed": 23} } ], "final_results": { "total_verifications": 23, "successful_verifications": 20, "failed_verifications": 3, "average_confidence": 0.82, "total_time": 45.67 } } } ``` ### 作业管理API #### GET /api/jobs 获取作业列表。 **参数**: - `status`: 作业状态筛选 (`running`, `completed`, `failed`, `timeout`) - `limit`: 返回结果数量限制 (默认: 50) - `offset`: 分页偏移量 (默认: 0) **响应**: ```json { "success": true, "data": { "jobs": [ { "job_id": "job_123456789", "type": "verification", "status": "completed", "created_at": "2024-01-01T00:00:00Z", "started_at": "2024-01-01T00:00:01Z", "completed_at": "2024-01-01T00:00:05Z", "duration": 4.23, "progress": 100.0, "result_summary": { "status": "success", "execution_time": 3.45 } } ], "pagination": { "total": 1, "limit": 50, "offset": 0, "has_more": false } } } ``` #### GET /api/jobs/{job_id} 获取特定作业详情。 #### DELETE /api/jobs/{job_id} 取消运行中的作业。 ### 结果导出API #### GET /api/results/{job_id}/export 导出验证结果。 **参数**: - `format`: 导出格式 (`json`, `xml`, `html`, `csv`) **响应**: 根据format参数返回相应格式的数据。 #### GET /api/results/{job_id}/report 生成验证报告。 **响应**: ```json { "success": true, "data": { "report": { "summary": { "total_verifications": 10, "successful": 8, "failed": 2, "timeout": 0, "success_rate": 80.0 }, "detailed_results": [...], "recommendations": [...], "statistics": {...} }, "generated_at": "2024-01-01T00:00:00Z" } } ``` --- ## WebSocket事件 ### 连接信息 - **URL**: `ws://localhost:8080/ws` - **协议**: WebSocket - **认证**: 通过Query参数传递token `ws://localhost:8080/ws?token=YOUR_TOKEN` ### 事件类型 #### job_progress 作业进度更新事件。 ```javascript { "event": "job_progress", "data": { "job_id": "job_123456789", "progress": { "percentage": 45.2, "current_step": "verification", "estimated_remaining": 120.5, "details": { "completed_verifications": 5, "total_verifications": 10 } }, "timestamp": "2024-01-01T00:00:00Z" } } ``` #### workflow_update 工作流状态更新事件。 ```javascript { "event": "workflow_update", "data": { "workflow_id": "wf_123456789", "status": "completed", "current_step": "verify", "progress": 100.0, "results": { "total_time": 45.67, "successful_verifications": 20 }, "timestamp": "2024-01-01T00:00:00Z" } } ``` #### verification_result 验证结果事件。 ```javascript { "event": "verification_result", "data": { "job_id": "job_123456789", "function_name": "add", "specification_id": "spec_123456789", "result": { "status": "success", "execution_time": 2.34, "properties_checked": 5 }, "timestamp": "2024-01-01T00:00:00Z" } } ``` #### error_notification 错误通知事件。 ```javascript { "event": "error_notification", "data": { "error_code": "CBMC_TIMEOUT", "error_message": "CBMC验证超时", "job_id": "job_123456789", "severity": "warning", "suggestions": [ "增加超时时间", "减少验证深度", "简化验证条件" ], "timestamp": "2024-01-01T00:00:00Z" } } ``` #### system_status 系统状态更新事件。 ```javascript { "event": "system_status", "data": { "status": "healthy", "load": { "cpu_usage": 45.2, "memory_usage": 67.8, "active_jobs": 3, "queue_length": 5 }, "timestamp": "2024-01-01T00:00:00Z" } } ``` --- ## 内部模块API ### MutationEngine #### 类: MutationEngine ```python class MutationEngine: def __init__(self, config: Optional[Dict] = None): """初始化突变引擎 Args: config: 突变引擎配置 """ async def generate_mutations( self, specification: str, function_metadata: List[Dict], max_mutations: int = 10, mutation_types: Optional[List[MutationType]] = None, quality_threshold: float = 0.7 ) -> List[CBMCMutation]: """生成规范突变 Args: specification: 原始规范字符串 function_metadata: 函数元数据列表 max_mutations: 最大突变数量 mutation_types: 突变类型列表 quality_threshold: 质量阈值 Returns: 突变结果列表 """ def get_supported_mutation_types(self) -> List[MutationType]: """获取支持的突变类型 Returns: 支持的突变类型列表 """ def evaluate_mutation_quality( self, original_spec: str, mutated_spec: str, mutation_type: MutationType ) -> float: """评估突变质量 Args: original_spec: 原始规范 mutated_spec: 突变后规范 mutation_type: 突变类型 Returns: 质量评分 (0.0-1.0) """ ``` ### CBMCRunner #### 类: CBMCRunner ```python class CBMCRunner: def __init__(self, config: Optional[Dict] = None): """初始化CBMC运行器 Args: config: CBMC运行器配置 """ async def run_verification( self, function_metadata: Dict, source_file: str, specification: str, timeout: int = 300, verification_types: Optional[List[str]] = None, cbmc_options: Optional[List[str]] = None ) -> VerificationResult: """运行CBMC验证 Args: function_metadata: 函数元数据 source_file: 源文件路径 specification: 验证规范 timeout: 超时时间(秒) verification_types: 验证类型列表 cbmc_options: CBMC命令行选项 Returns: 验证结果 """ async def cancel_verification(self, job_id: str) -> bool: """取消验证任务 Args: job_id: 任务ID Returns: 是否成功取消 """ def get_verification_status(self, job_id: str) -> Optional[Dict]: """获取验证状态 Args: job_id: 任务ID Returns: 任务状态信息 """ ``` ### CodeParser #### 类: CodeParser ```python class CodeParser: def __init__(self, config: Optional[Dict] = None): """初始化代码解析器 Args: config: 解析器配置 """ def parse_file(self, file_path: str) -> ParseResult: """解析C/C++文件 Args: file_path: 文件路径 Returns: 解析结果 """ def parse_code(self, code: str, filename: str = "temp.c") -> ParseResult: """解析代码字符串 Args: code: 代码字符串 filename: 文件名(用于错误信息) Returns: 解析结果 """ def get_function_metadata(self, function_name: str) -> Optional[Dict]: """获取函数元数据 Args: function_name: 函数名 Returns: 函数元数据 """ ``` --- ## 配置API ### 配置管理 #### GET /api/config 获取当前配置。 **响应**: ```json { "success": true, "data": { "llm": { "provider": "deepseek", "model": "deepseek-coder", "max_tokens": 2000, "temperature": 0.3 }, "cbmc": { "path": "cbmc", "timeout": 300, "depth": 20 }, "web": { "host": "0.0.0.0", "port": 8080, "debug": false } } } ``` #### PUT /api/config 更新配置。 **请求**: ```json { "llm": { "temperature": 0.4 }, "cbmc": { "timeout": 600 } } ``` ### 环境变量 #### GET /api/config/environment 获取环境变量配置。 **响应**: ```json { "success": true, "data": { "LLM_API_KEY": "***configured***", "CBMC_PATH": "/usr/bin/cbmc", "LOG_LEVEL": "INFO", "MAX_FILE_SIZE": "10MB" } } ``` --- ## 错误代码 ### 通用错误代码 | 代码 | 描述 | HTTP状态码 | |------|------|------------| | `INTERNAL_ERROR` | 内部服务器错误 | 500 | | `VALIDATION_ERROR` | 请求参数验证失败 | 400 | | `AUTHENTICATION_ERROR` | 身份验证失败 | 401 | | `AUTHORIZATION_ERROR` | 权限不足 | 403 | | `NOT_FOUND` | 资源未找到 | 404 | | `RATE_LIMIT_EXCEEDED` | 速率限制超出 | 429 | ### 业务错误代码 | 代码 | 描述 | 解决方案 | |------|------|----------| | `INVALID_FILE_TYPE` | 不支持的文件类型 | 仅支持.c, .cpp, .h, .hpp文件 | | `FILE_TOO_LARGE` | 文件大小超过限制 | 文件大小应小于10MB | | `PARSE_ERROR` | 代码解析失败 | 检查代码语法错误 | | `CBMC_NOT_FOUND` | CBMC工具未找到 | 安装CBMC或配置路径 | | `CBMC_TIMEOUT` | CBMC验证超时 | 增加超时时间或简化验证 | | `LLM_SERVICE_ERROR` | LLM服务错误 | 检查LLM服务状态和API密钥 | | `MUTATION_FAILED` | 突变生成失败 | 检查规范格式和参数 | | `VERIFICATION_FAILED` | 验证失败 | 检查代码和规范 | --- ## 身份验证 ### Bearer Token认证 所有API请求都需要在Header中包含Bearer Token: ```http Authorization: Bearer your-api-token ``` ### Token获取 通过登录接口获取token: ```http POST /api/auth/login Content-Type: application/json { "username": "admin", "password": "password" } ``` **响应**: ```json { "success": true, "data": { "token": "eyJ0eXAiOiJKV1QiLCJhbGciOiJIUzI1NiJ9...", "expires_in": 3600, "token_type": "Bearer" } } ``` ### Token刷新 ```http POST /api/auth/refresh Authorization: Bearer your-token ``` --- ## 速率限制 ### 限制规则 - **默认限制**: 每分钟100个请求 - **文件上传**: 每分钟10个文件 - **CBMC验证**: 每分钟5个验证任务 - **WebSocket**: 每秒100条消息 ### 响应头 API响应包含以下速率限制信息: ```http X-RateLimit-Limit: 100 X-RateLimit-Remaining: 95 X-RateLimit-Reset: 1640995200 ``` ### 超出限制 超出速率限制时返回429状态码: ```json { "success": false, "error": { "code": "RATE_LIMIT_EXCEEDED", "message": "速率限制超出,请稍后重试", "retry_after": 60 } } ``` --- ## 使用示例 ### Python客户端示例 ```python import requests import json # 配置 BASE_URL = "http://localhost:8080/api" TOKEN = "your-api-token" HEADERS = { "Authorization": f"Bearer {TOKEN}", "Content-Type": "application/json" } # 上传文件 with open("test.c", "rb") as f: files = {"file": f} response = requests.post( f"{BASE_URL}/upload", files=files, headers={"Authorization": f"Bearer {TOKEN}"} ) upload_result = response.json() # 解析代码 parse_request = { "file_path": "test.c", "options": { "include_functions": True, "complexity_analysis": True } } response = requests.post( f"{BASE_URL}/parse", json=parse_request, headers=HEADERS ) parse_result = response.json() # 生成规范 generate_request = { "functions": parse_result["data"]["functions"], "options": { "verification_types": ["memory_safety", "overflow_detection"] } } response = requests.post( f"{BASE_URL}/generate", json=generate_request, headers=HEADERS ) generate_result = response.json() # 运行验证 for spec in generate_result["data"]["specifications"]: verify_request = { "specification": spec["specification"], "function_name": spec["function_name"], "source_file": "test.c" } response = requests.post( f"{BASE_URL}/verify", json=verify_request, headers=HEADERS ) verify_result = response.json() print(f"验证结果: {verify_result}") ``` ### JavaScript客户端示例 ```javascript class CodeDetectClient { constructor(baseUrl, token) { this.baseUrl = baseUrl; this.token = token; this.headers = { 'Authorization': `Bearer ${token}`, 'Content-Type': 'application/json' }; } async uploadFile(file) { const formData = new FormData(); formData.append('file', file); const response = await fetch(`${this.baseUrl}/upload`, { method: 'POST', headers: { 'Authorization': `Bearer ${this.token}` }, body: formData }); return response.json(); } async parseCode(filePath, options = {}) { const response = await fetch(`${this.baseUrl}/parse`, { method: 'POST', headers: this.headers, body: JSON.stringify({ file_path: filePath, options }) }); return response.json(); } async generateSpecifications(functions, options = {}) { const response = await fetch(`${this.baseUrl}/generate`, { method: 'POST', headers: this.headers, body: JSON.stringify({ functions, options }) }); return response.json(); } async runVerification(specification, functionName, sourceFile, options = {}) { const response = await fetch(`${this.baseUrl}/verify`, { method: 'POST', headers: this.headers, body: JSON.stringify({ specification, function_name: functionName, source_file: sourceFile, options }) }); return response.json(); } } // 使用示例 const client = new CodeDetectClient('http://localhost:8080/api', 'your-token'); // WebSocket连接 const ws = new WebSocket('ws://localhost:8080/ws?token=your-token'); ws.onmessage = (event) => { const data = JSON.parse(event.data); console.log('收到消息:', data); }; ``` --- *最后更新: 2024年1月*