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