|
|
# LLM生成测试配置文件
|
|
|
# 用于配置测试环境、参数设置和质量阈值
|
|
|
|
|
|
# 测试全局配置
|
|
|
test:
|
|
|
# 基本设置
|
|
|
timeout: 120 # 单个测试超时时间（秒）
|
|
|
max_retries: 3 # 最大重试次数
|
|
|
parallel_workers: 3 # 并发工作线程数
|
|
|
save_intermediate: true # 保存中间结果
|
|
|
validate_specs: true # 验证生成的规范
|
|
|
quality_threshold: 0.7 # 质量分数阈值
|
|
|
|
|
|
# 输出设置
|
|
|
output_dir: "test_results" # 测试结果输出目录
|
|
|
save_detailed_logs: true # 保存详细日志
|
|
|
generate_html_report: true # 生成HTML报告
|
|
|
log_level: "INFO" # 日志级别
|
|
|
|
|
|
# 性能测试设置
|
|
|
performance:
|
|
|
enable_monitoring: true # 启用性能监控
|
|
|
track_memory: true # 跟踪内存使用
|
|
|
track_cpu: true # 跟踪CPU使用
|
|
|
sample_interval: 1.0 # 采样间隔（秒）
|
|
|
|
|
|
# 重试设置
|
|
|
retry:
|
|
|
base_delay: 1.0 # 基础延迟（秒）
|
|
|
max_delay: 30.0 # 最大延迟（秒）
|
|
|
backoff_factor: 2.0 # 退避因子
|
|
|
|
|
|
# 质量评估设置
|
|
|
quality:
|
|
|
enable_syntax_check: true # 启用语法检查
|
|
|
enable_logic_check: true # 启用逻辑检查
|
|
|
enable_completeness_check: true # 启用完整性检查
|
|
|
weight_syntax: 0.3 # 语法权重
|
|
|
weight_logic: 0.3 # 逻辑权重
|
|
|
weight_completeness: 0.4 # 完整性权重
|
|
|
|
|
|
# 解析器配置
|
|
|
parser:
|
|
|
# C预处理器设置
|
|
|
use_cpp: true # 使用C预处理器
|
|
|
cpp_path: "cpp" # 预处理器路径
|
|
|
extra_cpp_args: [] # 额外预处理器参数
|
|
|
|
|
|
# 包含路径
|
|
|
include_paths:
|
|
|
- "/usr/include"
|
|
|
- "/usr/local/include"
|
|
|
- "/opt/homebrew/include" # macOS Homebrew
|
|
|
|
|
|
# 宏定义
|
|
|
defines:
|
|
|
FREERTOS: "1"
|
|
|
INCLUDE_FREERTOS_TASK_C_ADDITIONS_H: "1"
|
|
|
|
|
|
# FreeRTOS支持
|
|
|
support_freertos: true
|
|
|
|
|
|
# 缓存设置
|
|
|
cache_enabled: true # 启用AST缓存
|
|
|
cache_size: 100 # 缓存大小
|
|
|
|
|
|
# LLM配置
|
|
|
llm:
|
|
|
# API设置
|
|
|
api_key: "${SILICONFLOW_API_KEY}" # API密钥（从环境变量读取）
|
|
|
base_url: "https://api.siliconflow.cn/v1" # API基础URL
|
|
|
model: "deepseek-ai/DeepSeek-V3.1" # 模型名称
|
|
|
|
|
|
# 请求设置
|
|
|
timeout: 120 # 请求超时时间（秒）
|
|
|
max_retries: 3 # 最大重试次数
|
|
|
retry_delay: 1.0 # 重试延迟（秒）
|
|
|
rate_limit_delay: 5.0 # 速率限制延迟（秒）
|
|
|
|
|
|
# 生成参数
|
|
|
temperature: 0.7 # 温度参数
|
|
|
max_tokens: 4096 # 最大令牌数
|
|
|
top_p: 0.95 # Top-p采样
|
|
|
|
|
|
# 并发设置
|
|
|
max_concurrent_requests: 3 # 最大并发请求数
|
|
|
|
|
|
# 提示模板
|
|
|
prompts:
|
|
|
system_role: "You are a formal verification expert specializing in CBMC specification generation for C/C++ code."
|
|
|
|
|
|
# 验证目标模板
|
|
|
verification_goals:
|
|
|
functional_correctness: "Ensure the function behaves correctly according to its specification"
|
|
|
memory_safety: "Ensure no memory corruption, leaks, or invalid access"
|
|
|
buffer_overflow: "Ensure no buffer overflows or underflows"
|
|
|
null_pointer: "Ensure proper null pointer handling"
|
|
|
integer_overflow: "Ensure no integer overflow or underflow"
|
|
|
array_bounds: "Ensure array access is within bounds"
|
|
|
task_safety: "Ensure thread/task safety in concurrent environments"
|
|
|
concurrency: "Ensure correct behavior in multi-threaded contexts"
|
|
|
resource_leaks: "Ensure no resource leaks (memory, file handles, etc.)"
|
|
|
|
|
|
# 函数类型模板
|
|
|
function_templates:
|
|
|
basic: "templates/basic_function.j2"
|
|
|
pointer: "templates/pointer_function.j2"
|
|
|
array: "templates/array_function.j2"
|
|
|
string: "templates/string_function.j2"
|
|
|
freertos: "templates/freertos_function.j2"
|
|
|
complex: "templates/complex_function.j2"
|
|
|
|
|
|
# 验证器配置
|
|
|
validator:
|
|
|
# 验证规则设置
|
|
|
rules:
|
|
|
syntax:
|
|
|
enabled: true
|
|
|
strict_mode: false
|
|
|
allow_warnings: true
|
|
|
|
|
|
logic:
|
|
|
enabled: true
|
|
|
check_contradictions: true
|
|
|
check_tautologies: true
|
|
|
|
|
|
completeness:
|
|
|
enabled: true
|
|
|
require_requires: true
|
|
|
require_ensures: true
|
|
|
require_parameter_coverage: true
|
|
|
|
|
|
quality:
|
|
|
enabled: true
|
|
|
min_quality_score: 0.5
|
|
|
check_readability: true
|
|
|
check_complexity: true
|
|
|
|
|
|
# CBMC特定设置
|
|
|
cbmc:
|
|
|
supported_clauses:
|
|
|
- "requires"
|
|
|
- "ensures"
|
|
|
- "assigns"
|
|
|
- "valid"
|
|
|
- "valid_read"
|
|
|
- "forall"
|
|
|
- "exists"
|
|
|
- "invariant"
|
|
|
- "axiom"
|
|
|
- "behavior"
|
|
|
- "complete"
|
|
|
- "disjoint"
|
|
|
|
|
|
syntax_patterns:
|
|
|
- "\\\\requires.*;"
|
|
|
- "\\\\ensures.*;"
|
|
|
- "\\\\assigns.*;"
|
|
|
- "\\\\valid.*;"
|
|
|
- "\\\\valid_read.*;"
|
|
|
|
|
|
# 测试用例配置
|
|
|
test_cases:
|
|
|
# 基础测试用例
|
|
|
basic:
|
|
|
enabled: true
|
|
|
complexity_level: "basic"
|
|
|
timeout: 60
|
|
|
max_retries: 2
|
|
|
quality_threshold: 0.8
|
|
|
|
|
|
# 中等复杂度测试用例
|
|
|
intermediate:
|
|
|
enabled: true
|
|
|
complexity_level: "intermediate"
|
|
|
timeout: 90
|
|
|
max_retries: 3
|
|
|
quality_threshold: 0.7
|
|
|
|
|
|
# 高级测试用例
|
|
|
advanced:
|
|
|
enabled: true
|
|
|
complexity_level: "advanced"
|
|
|
timeout: 120
|
|
|
max_retries: 3
|
|
|
quality_threshold: 0.6
|
|
|
|
|
|
# 领域特定测试用例
|
|
|
domain_specific:
|
|
|
freertos:
|
|
|
enabled: true
|
|
|
complexity_level: "advanced"
|
|
|
timeout: 150
|
|
|
quality_threshold: 0.7
|
|
|
|
|
|
embedded:
|
|
|
enabled: true
|
|
|
complexity_level: "intermediate"
|
|
|
timeout: 120
|
|
|
quality_threshold: 0.7
|
|
|
|
|
|
# 性能测试配置
|
|
|
performance:
|
|
|
# 基准测试设置
|
|
|
benchmark:
|
|
|
iterations: 10 # 基准测试迭代次数
|
|
|
warmup_iterations: 2 # 预热迭代次数
|
|
|
enable_monitoring: true # 启用性能监控
|
|
|
|
|
|
# 并发测试设置
|
|
|
concurrency:
|
|
|
test_levels: [1, 3, 5, 10] # 并发级别测试
|
|
|
request_count: 20 # 每个级别的请求数
|
|
|
|
|
|
# 复杂度测试设置
|
|
|
complexity:
|
|
|
test_levels: ["basic", "intermediate", "advanced"]
|
|
|
samples_per_level: 5 # 每个复杂度级别的样本数
|
|
|
|
|
|
# 报告设置
|
|
|
reporting:
|
|
|
generate_charts: true # 生成图表
|
|
|
save_raw_data: true # 保存原始数据
|
|
|
format: ["json", "html"] # 报告格式
|
|
|
|
|
|
# 资源监控
|
|
|
monitoring:
|
|
|
track_memory: true # 跟踪内存使用
|
|
|
track_cpu: true # 跟踪CPU使用
|
|
|
track_network: true # 跟踪网络使用
|
|
|
sample_interval: 0.5 # 采样间隔
|
|
|
|
|
|
# 日志配置
|
|
|
logging:
|
|
|
level: "INFO" # 日志级别
|
|
|
format: "%(asctime)s - %(name)s - %(levelname)s - %(message)s" # 日志格式
|
|
|
file_logging: true # 启用文件日志
|
|
|
log_file: "test_logs/llm_test.log" # 日志文件路径
|
|
|
max_file_size: "10MB" # 最大文件大小
|
|
|
backup_count: 5 # 备份文件数量
|
|
|
|
|
|
# 组件日志级别
|
|
|
loggers:
|
|
|
test_runner: "INFO"
|
|
|
llm_generator: "INFO"
|
|
|
c_parser: "WARNING"
|
|
|
ast_extractor: "WARNING"
|
|
|
validator: "INFO"
|
|
|
performance: "DEBUG"
|
|
|
|
|
|
# 输出配置
|
|
|
output:
|
|
|
# 报告格式
|
|
|
formats:
|
|
|
- "json"
|
|
|
- "html"
|
|
|
- "csv"
|
|
|
|
|
|
# 详细程度
|
|
|
verbosity: "normal" # minimal, normal, detailed
|
|
|
|
|
|
# 保存设置
|
|
|
save_intermediate: true # 保存中间结果
|
|
|
save_failed_specs: true # 保存失败的规范
|
|
|
save_performance_data: true # 保存性能数据
|
|
|
|
|
|
# 目录结构
|
|
|
directories:
|
|
|
base: "test_results"
|
|
|
reports: "reports"
|
|
|
logs: "logs"
|
|
|
specifications: "specs"
|
|
|
performance: "performance"
|
|
|
validation: "validation"
|
|
|
|
|
|
# 开发配置（仅在开发环境中使用）
|
|
|
development:
|
|
|
# 模式设置
|
|
|
mock_api: false # 模拟API（用于离线测试）
|
|
|
debug_mode: false # 调试模式
|
|
|
verbose_output: false # 详细输出
|
|
|
|
|
|
# 测试数据设置
|
|
|
test_data:
|
|
|
use_cached_data: true # 使用缓存数据
|
|
|
cache_duration: 3600 # 缓存持续时间（秒）
|
|
|
regenerate_on_failure: true # 失败时重新生成
|
|
|
|
|
|
# 调试工具
|
|
|
debugging:
|
|
|
enable_tracing: false # 启用跟踪
|
|
|
save_request_data: true # 保存请求数据
|
|
|
save_response_data: true # 保存响应数据
|
|
|
profile_performance: true # 性能分析 |
