26 KiB

Raw Permalink Blame History Unescape Escape

CodeDetect API参考文档

本文档提供了CodeDetect系统所有API接口的详细参考，包括REST API、WebSocket事件、内部模块API和配置API。

REST API

基础信息

基础URL: http://localhost:8080/api
内容类型: application/json
认证方式: Bearer Token
字符编码: UTF-8

通用响应格式

所有API响应都遵循以下格式：

{
  "success": true,
  "data": {},
  "message": "操作成功",
  "timestamp": "2024-01-01T00:00:00Z",
  "request_id": "req_123456789"
}

错误响应格式：

{
  "success": false,
  "error": {
    "code": "VALIDATION_ERROR",
    "message": "请求参数验证失败",
    "details": {}
  },
  "timestamp": "2024-01-01T00:00:00Z",
  "request_id": "req_123456789"
}

文件上传API

POST /api/upload

上传C/C++文件进行验证。

请求:

POST /api/upload
Content-Type: multipart/form-data

file: [C/C++文件]

响应:

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

批量上传多个文件。

请求:

POST /api/upload/batch
Content-Type: multipart/form-data

files: [多个C/C++文件]

响应:

{
  "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++代码。

请求:

{
  "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
  }
}

响应:

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

批量解析多个文件。

请求:

{
  "file_paths": ["/path/to/file1.c", "/path/to/file2.c"],
  "options": {
    "include_functions": true,
    "cross_file_analysis": true
  }
}

规范生成API

POST /api/generate

基于解析结果生成CBMC验证规范。

请求:

{
  "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"
  }
}

响应:

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

获取可用的规范模板。

响应:

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

生成验证规范的变异版本。

请求:

{
  "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
  }
}

响应:

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

获取可用的突变类型。

响应:

{
  "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验证。

请求:

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

响应:

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

批量验证多个规范。

请求:

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

启动完整的验证工作流。

请求:

{
  "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
  }
}

响应:

{
  "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}

获取工作流状态。

响应:

{
  "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)

响应:

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

生成验证报告。

响应:

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

作业进度更新事件。

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

工作流状态更新事件。

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

验证结果事件。

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

错误通知事件。

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

系统状态更新事件。

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

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

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

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

获取当前配置。

响应:

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

更新配置。

请求:

{
  "llm": {
    "temperature": 0.4
  },
  "cbmc": {
    "timeout": 600
  }
}

环境变量

GET /api/config/environment

获取环境变量配置。

响应:

{
  "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：

Authorization: Bearer your-api-token

Token获取

通过登录接口获取token：

POST /api/auth/login
Content-Type: application/json

{
  "username": "admin",
  "password": "password"
}

响应:

{
  "success": true,
  "data": {
    "token": "eyJ0eXAiOiJKV1QiLCJhbGciOiJIUzI1NiJ9...",
    "expires_in": 3600,
    "token_type": "Bearer"
  }
}

Token刷新

POST /api/auth/refresh
Authorization: Bearer your-token

速率限制

限制规则

默认限制: 每分钟100个请求
文件上传: 每分钟10个文件
CBMC验证: 每分钟5个验证任务
WebSocket: 每秒100条消息

响应头

API响应包含以下速率限制信息：

X-RateLimit-Limit: 100
X-RateLimit-Remaining: 95
X-RateLimit-Reset: 1640995200

超出限制

超出速率限制时返回429状态码：

{
  "success": false,
  "error": {
    "code": "RATE_LIMIT_EXCEEDED",
    "message": "速率限制超出，请稍后重试",
    "retry_after": 60
  }
}

使用示例

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客户端示例

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月

26 KiB Raw Permalink Blame History Unescape Escape