You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
cbmc/codedetect/docs/api-reference.md

1324 lines
26 KiB

This file contains ambiguous Unicode characters!

This file contains ambiguous Unicode characters that may be confused with others in your current locale. If your use case is intentional and legitimate, you can safely ignore this warning. Use the Escape button to highlight these characters.

# 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月*