cbmc/codedetect/examples/freertos/README.md

# FreeRTOS验证示例

本目录包含使用CodeDetect系统验证FreeRTOS代码的完整示例。这些示例展示了如何在实时操作系统环境中进行形式化验证，包括任务管理、队列操作、同步机制和中断处理。

## 示例概览

### 1. 任务验证示例 (`task_verification_example.c`)

**文件**: `task_verification_example.c`

**功能**: 演示FreeRTOS任务的创建、管理和验证

**验证要点**:
- 任务参数验证（NULL指针检查）
- 任务生命周期管理
- 栈空间使用验证
- 任务同步机制
- 内存安全性验证
- 任务状态一致性

**关键代码片段**:
```c
void vCounterTask(void *pvParameters) {
    TaskParameters_t *params = (TaskParameters_t *)pvParameters;

    /* 参数验证 - CodeDetect将生成相应的CBMC规范 */
    configASSERT(params != NULL);
    configASSERT(params->task_id > 0);
    configASSERT(params->max_count > 0);

    /* 任务循环 */
    while (params->should_stop == pdFALSE) {
        /* 边界检查 - 防止计数器溢出 */
        if (params->counter < params->max_count) {
            params->counter++;
        }
        vTaskDelay(pdMS_TO_TICKS(100));
    }
}
```

### 2. 队列验证示例 (`queue_verification_example.c`)

**文件**: `queue_verification_example.c`

**功能**: 演示FreeRTOS队列操作的验证

**验证要点**:
- 队列创建和删除的安全性
- 队列满和空状态的处理
- 生产者-消费者模式验证
- 并发访问安全性
- 消息完整性检查
- 队列溢出保护

**关键代码片段**:
```c
void vProducerTask(void *pvParameters) {
    if (xMessage.is_critical) {
        /* 关键消息使用更长等待时间 */
        xSendResult = xQueueSend(xMessageQueue, &xMessage, pdMS_TO_TICKS(100));
    } else {
        /* 普通消息使用较短等待时间 */
        xSendResult = xQueueSend(xMessageQueue, &xMessage, pdMS_TO_TICKS(10));
    }

    /* 错误处理 */
    if (xSendResult != pdPASS) {
        xQueueStats.queue_full_errors++;
    }
}
```

## 验证模式

### 1. 基本验证

**目标**: 验证代码的基本正确性
- 内存安全
- 空指针处理
- 边界条件
- 资源管理

**CBMC规范生成**:
```c
void test_task_safety() {
    TaskParameters_t params;
    vCounterTask(&params);
    __CPROVER_assert(params.counter >= 0, "counter_non_negative");
}
```

### 2. 并发验证

**目标**: 验证多任务环境下的安全性
- 竞态条件检测
- 死锁预防
- 数据一致性
- 同步机制验证

**CBMC规范生成**:
```c
void test_concurrent_access() {
    QueueHandle_t queue = xQueueCreate(10, sizeof(int));
    /* CodeDetect生成并发访问验证规范 */
    __CPROVER_assert(queue != NULL, "queue_creation_success");
}
```

### 3. 性能验证

**目标**: 验证实时性能要求
- 响应时间保证
- 内存使用限制
- 执行时间分析
- 资源使用效率

## CodeDetect集成

### 1. 配置文件

创建 `freertos_config.yaml`:
```yaml
freertos:
  include_headers:
    - "FreeRTOS.h"
    - "task.h"
    - "queue.h"
    - "semphr.h"
  config_path: "/path/to/FreeRTOSConfig.h"
  heap_size: 4096
  max_tasks: 10
  stack_size: 1024

verification:
  target_types: ["memory_safety", "concurrency", "overflow_detection"]
  timeout: 300
  max_concurrent_jobs: 4
```

### 2. 验证流程

1. **代码解析**: 分析FreeRTOS代码结构
2. **规范生成**: 基于LLM生成CBMC验证规范
3. **规范突变**: 生成变异规范提高覆盖率
4. **CBMC验证**: 运行形式化验证
5. **结果分析**: 生成详细验证报告

### 3. API使用示例

```python
from src.verify.cbmc_runner import CBMCRunner
from src.mutate.engine import MutationEngine

# 创建验证器
runner = CBMCRunner()
engine = MutationEngine()

# 解析FreeRTOS代码
metadata = parse_freertos_code("task_example.c")

# 生成验证规范
specifications = generate_freertos_specs(metadata)

# 生成突变规范
mutations = engine.generate_mutations(
    specifications[0],
    metadata,
    max_mutations=10
)

# 运行验证
results = []
for mutation in mutations:
    result = await runner.run_verification(
        function_metadata=metadata[0],
        source_file="task_example.c",
        specification=mutation.specification
    )
    results.append(result)
```

## 验证报告

### 典型验证结果

```
=== FreeRTOS任务验证报告 ===

文件: task_verification_example.c
函数: vCounterTask
验证时间: 2.34s

✅ 内存安全: 通过
  - 无空指针解引用
  - 无缓冲区溢出
  - 无内存泄漏

✅ 并发安全: 通过
  - 任务同步正确
  - 无数据竞争
  - 栈空间充足

✅ 边界检查: 通过
  - 计数器溢出保护
  - 参数范围验证
  - 循环终止条件

⚠️  性能警告:
  - 任务延时时间较长 (100ms)
  - 栈使用率较高 (85%)

建议:
1. 考虑减少任务延时以提高响应性
2. 增加栈大小或优化内存使用
```

## 高级验证场景

### 1. 中断处理验证

```c
void vISR_Handler(void) {
    BaseType_t xHigherPriorityTaskWoken = pdFALSE;

    /* 中断安全的关键区域 */
    taskENTER_CRITICAL_FROM_ISR();

    /* 处理中断 */
    xQueueSendFromISR(xQueue, &data, &xHigherPriorityTaskWoken);

    taskEXIT_CRITICAL_FROM_ISR();

    /* 必要时进行任务切换 */
    portYIELD_FROM_ISR(xHigherPriorityTaskWoken);
}
```

**验证要点**:
- 中断上下文安全性
- 关键区域保护
- 任务切换时机
- 数据一致性保证

### 2. 内存管理验证

```c
void* pvAllocateManagedMemory(size_t xSize) {
    void* pvReturn = pvPortMalloc(xSize);

    if (pvReturn != NULL) {
        /* 追踪内存分配 */
        vTrackAllocation(pvReturn, xSize);
    }

    return pvReturn;
}
```

**验证要点**:
- 内存分配失败处理
- 内存泄漏检测
- 堆空间溢出保护
- 内存对齐要求

### 3. 信号量和互斥量验证

```c
void vProtectedFunction(void) {
    /* 获取互斥量 */
    if (xSemaphoreTake(xMutex, portMAX_DELAY) == pdTRUE) {
        /* 受保护的代码区域 */
        vCriticalOperation();

        /* 释放互斥量 */
        xSemaphoreGive(xMutex);
    }
}
```

**验证要点**:
- 死锁预防
- 优先级反转
- 资源泄漏
- 超时处理

## 最佳实践

### 1. 代码编写

- **参数验证**: 始终验证函数参数
- **错误处理**: 正确处理FreeRTOS API返回值
- **资源管理**: 确保分配的资源被正确释放
- **并发安全**: 使用适当的同步机制

### 2. 验证策略

- **增量验证**: 先验证基本功能，再验证复杂场景
- **边界测试**: 重点测试边界条件和错误情况
- **性能分析**: 监控内存使用和执行时间
- **覆盖率最大化**: 使用突变测试提高验证覆盖率

### 3. 配置优化

```yaml
# 生产环境验证配置
verification:
  depth: 25          # 增加搜索深度
  unwind: 15         # 增加循环展开
  timeout: 600       # 增加超时时间
  max_memory: "2GB"  # 增加内存限制

freertos:
  max_tasks: 20      # 支持更多任务
  stack_size: 2048   # 更大的栈空间
  heap_size: 8192    # 更大的堆空间
```

## 故障排除

### 常见问题

1. **CBMC超时**
   ```
   解决方案:
   - 减少验证深度 (--depth 15)
   - 增加超时时间 (--timeout 600)
   - 限制循环展开 (--unwind 5)
   ```

2. **内存不足**
   ```
   解决方案:
   - 增加可用内存
   - 简化验证条件
   - 分批验证功能
   ```

3. **验证失败**
   ```
   解决方案:
   - 检查反例路径
   - 验证前置条件
   - 增强错误处理
   - 修改算法逻辑
   ```

### 调试技巧

1. **逐步验证**: 先验证简单函数，再验证复杂逻辑
2. **日志分析**: 启用详细日志输出分析问题
3. **反例分析**: 仔细分析CBMC生成的反例
4. **参数调优**: 根据代码复杂度调整验证参数

## 扩展示例

### 1. 复杂任务间通信

创建 `complex_communication_example.c` 演示：
- 多个生产者和消费者
- 优先级调度
- 事件通知机制
- 复杂数据结构传递

### 2. 定时器和定时服务

创建 `timer_verification_example.c` 演示：
- 软件定时器验证
- 硬件定时器集成
- 定时器回调安全性
- 时间精度保证

### 3. 外设驱动验证

创建 `driver_verification_example.c` 演示：
- 硬件抽象层验证
- DMA操作安全性
- 中断驱动处理
- 外设配置验证

## 贡献指南

我们欢迎社区贡献新的FreeRTOS验证示例：

1. **创建示例**: 在本目录添加新的`.c`文件
2. **添加文档**: 包含详细的说明和验证要点
3. **测试验证**: 确保示例可以通过验证
4. **提交PR**: 通过GitHub提交Pull Request

## 许可证

本示例代码遵循与主项目相同的许可证条款。

---

*最后更新: 2024年1月*