cbmc/codedetect/docs/examples/freertos-verification-tutorial.md

# CodeDetect FreeRTOS验证教程

## 概述

本教程专门介绍如何使用CodeDetect验证FreeRTOS应用程序的内存安全和并发正确性。

## 前提条件

- 完成基础使用教程
- FreeRTOS开发经验
- 并发编程基础

## 第一步：FreeRTOS环境设置

### 1.1 安装FreeRTOS

```bash
# 使用我们的设置脚本
./scripts/setup-freertos-example.sh

# 或者手动安装
git clone https://github.com/FreeRTOS/FreeRTOS.git
export FREERTOS_PATH=/path/to/FreeRTOS
```

### 1.2 验证FreeRTOS安装

```bash
# 检查FreeRTOS头文件
ls $FREERTOS_PATH/FreeRTOS/Source/include/

# 编译示例
cd examples/freertos
make
```

## 第二步：基本FreeRTOS验证

### 2.1 任务创建验证

考虑以下FreeRTOS任务代码：

```c
#include "FreeRTOS.h"
#include "task.h"

typedef struct {
    int task_id;
    char* name;
} TaskParameters_t;

void vCounterTask(void *pvParameters) {
    TaskParameters_t *params = (TaskParameters_t *)pvParameters;

    // 参数验证
    configASSERT(params != NULL);
    configASSERT(params->task_id > 0);

    while (1) {
        // 安全的任务逻辑
        vTaskDelay(pdMS_TO_TICKS(1000));
    }
}
```

使用CodeDetect验证：

```bash
# 生成任务规范
python -m src.main generate-spec task_verification_example.c \
    --function vCounterTask \
    --framework freertos

# 运行验证
python -m src.main verify task_verification_example.c \
    --function vCounterTask \
    --include-path $FREERTOS_PATH/FreeRTOS/Source/include
```

### 2.2 解读验证结果

**成功验证输出：**
```
VERIFICATION SUCCESSFUL
Property __CPROVER_assert: OK (parameter validation)
Property __CPROVER_assert: OK (null pointer check)
Property __CPROVER_assert: OK (task safety)
```

**常见问题：**
```
VERIFICATION FAILED
Property __CPROVER_assert: FAILED
Violated property: parameter validation
```

## 第三步：队列操作验证

### 3.1 生产者-消费者模式

```c
#include "FreeRTOS.h"
#include "queue.h"

typedef struct {
    int id;
    int value;
    int is_critical;
} Message_t;

QueueHandle_t xMessageQueue;

void vProducerTask(void *pvParameters) {
    Message_t xMessage;

    while (1) {
        xMessage.id++;
        xMessage.value = xMessage.id * 10;
        xMessage.is_critical = (xMessage.id % 10 == 0);

        if (xMessage.is_critical) {
            // 临界消息处理
            BaseType_t xSendResult = xQueueSend(xMessageQueue, &xMessage, pdMS_TO_TICKS(100));
            configASSERT(xSendResult == pdPASS);
        } else {
            xQueueSend(xMessageQueue, &xMessage, 0);
        }

        vTaskDelay(pdMS_TO_TICKS(10));
    }
}

void vConsumerTask(void *pvParameters) {
    Message_t xReceivedMessage;

    while (1) {
        if (xQueueReceive(xMessageQueue, &xReceivedMessage, pdMS_TO_TICKS(100)) == pdPASS) {
            // 安全处理接收到的消息
            configASSERT(xReceivedMessage.value >= 0);
        }
    }
}
```

### 3.2 验证队列安全性

```bash
# 验证生产者任务
python -m src.main verify queue_verification_example.c \
    --function vProducerTask \
    --framework freertos \
    --verify-concurrency

# 验证消费者任务
python -m src.main verify queue_verification_example.c \
    --function vConsumerTask \
    --framework freertos \
    --verify-concurrency

# 验证队列创建
python -m src.main verify queue_verification_example.c \
    --function main \
    --framework freertos
```

## 第四步：信号量和互斥量验证

### 4.1 资源保护模式

```c
#include "FreeRTOS.h"
#include "semphr.h"

SemaphoreHandle_t xResourceSemaphore;
int shared_resource = 0;

void vResourceUserTask(void *pvParameters) {
    while (1) {
        // 安全地获取资源
        if (xSemaphoreTake(xResourceSemaphore, pdMS_TO_TICKS(100)) == pdTRUE) {
            // 临界区开始
            shared_resource++;
            configASSERT(shared_resource > 0);

            // 模拟处理时间
            vTaskDelay(pdMS_TO_TICKS(10));

            // 释放资源
            xSemaphoreGive(xResourceSemaphore);
        }

        vTaskDelay(pdMS_TO_TICKS(50));
    }
}
```

### 4.2 验证互斥访问

```bash
# 验证资源使用
python -m src.main verify semaphore_example.c \
    --function vResourceUserTask \
    --framework freertos \
    --verify-deadlock

# 检查死锁可能性
python -m src.main analyze-deadlocks semaphore_example.c
```

## 第五步：中断处理验证

### 5.1 中断服务例程

```c
#include "FreeRTOS.h"
#include "task.h"
#include "queue.h"

QueueHandle_t xInterruptQueue;

void vExternalInterruptHandler(void) {
    BaseType_t xHigherPriorityTaskWoken = pdFALSE;
    uint32_t interrupt_status = 0;

    // 安全的中断处理
    taskENTER_CRITICAL_FROM_ISR();
    interrupt_status = read_interrupt_register();
    taskEXIT_CRITICAL_FROM_ISR();

    // 发送消息到任务
    xQueueSendFromISR(xInterruptQueue, &interrupt_status, &xHigherPriorityTaskWoken);

    portYIELD_FROM_ISR(xHigherPriorityTaskWoken);
}
```

### 5.2 验证中断安全性

```bash
# 验证中断处理
python -m src.main verify interrupt_example.c \
    --function vExternalInterruptHandler \
    --framework freertos \
    --verify-interrupt-safety
```

## 第六步：系统级验证

### 6.1 完整系统验证

```bash
# 验证整个FreeRTOS应用程序
python -m src.main batch-verify ./freertos_app/ \
    --framework freertos \
    --include-path $FREERTOS_PATH/FreeRTOS/Source/include \
    --verify-concurrency \
    --verify-deadlock \
    --verify-memory-safety

# 生成系统级报告
python -m src.main generate-system-report ./freertos_app/ \
    --format html \
    --include-concurrency-analysis
```

### 6.2 性能分析

```bash
# 分析任务调度
python -m src.main analyze-scheduling freertos_app.c

# 检查资源使用
python -m src.main analyze-resource-usage freertos_app.c
```

## 第七步：故障排除

### 7.1 常见FreeRTOS验证问题

**FreeRTOS头文件未找到：**
```bash
# 设置正确的包含路径
export FREERTOS_INCLUDE_PATH=$FREERTOS_PATH/FreeRTOS/Source/include:$FREERTOS_PATH/FreeRTOS-Plus/Source/FreeRTOS-Plus-CLI/include

# 验证命令
python -m src.main verify test.c --include-path $FREERTOS_INCLUDE_PATH
```

**并发验证超时：**
```bash
# 减少验证深度
python -m src.main verify test.c --unwind 5 --concurrency-depth 3

# 增加超时时间
python -m src.main verify test.c --timeout 120
```

**内存模型问题：**
```bash
# 使用简化的内存模型
python -m src.main verify test.c --memory-model simple

# 禁用某些检查
python -m src.main verify test.c --no-pointer-check
```

### 7.2 FreeRTOS特定配置

创建FreeRTOS配置文件 `freertos_config.yaml`：

```yaml
freertos:
  include_paths:
    - "$FREERTOS_PATH/FreeRTOS/Source/include"
    - "$FREERTOS_PATH/FreeRTOS/Plus/Source/FreeRTOS-Plus-CLI/include"

  verification:
    max_tasks: 10
    max_queues: 5
    max_semaphores: 5
    max_interrupts: 3

  analysis:
    check_deadlocks: true
    check_priority_inversion: true
    check_stack_overflow: true
    check_resource_leaks: true

  memory_model:
    heap_size: 1024
    stack_size: 128
    configASSERT: true
```

## 第八步：最佳实践

### 8.1 FreeRTOS安全编程

```c
// 好的实践：安全的任务创建
TaskHandle_t xTaskHandle = NULL;
BaseType_t xResult = xTaskCreate(
    vTaskFunction,
    "TaskName",
    configMINIMAL_STACK_SIZE,
    pvParameters,
    tskIDLE_PRIORITY + 1,
    &xTaskHandle
);
configASSERT(xResult == pdPASS);

// 避免的做法：不检查创建结果
xTaskCreate(vTaskFunction, "TaskName", 128, pvParameters, 1, NULL);
```

### 8.2 队列安全使用

```c
// 好的实践：安全的队列操作
BaseType_t xResult = xQueueSend(xQueue, &data, pdMS_TO_TICKS(100));
if (xResult != pdPASS) {
    // 处理队列满的情况
}

// 避免的做法：不检查返回值
xQueueSend(xQueue, &data, portMAX_DELAY);
```

### 8.3 中断安全设计

```c
// 好的实践：中断安全
void vInterruptHandler(void) {
    uint32_t status;

    taskENTER_CRITICAL_FROM_ISR();
    status = read_register();
    taskEXIT_CRITICAL_FROM_ISR();

    // 快速处理并返回
}

// 避免的做法：在中断中执行耗时操作
void vBadInterruptHandler(void) {
    // 长时间处理
    for (int i = 0; i < 1000; i++) {
        complex_operation();
    }
}
```

## 高级主题

### 实时性分析
- 任务响应时间验证
- 调度器行为分析
- 优先级反转检测

### 内存安全
- 堆栈使用验证
- 内存泄漏检测
- 缓冲区溢出检查

### 系统验证
- 启动序列验证
- 错误处理验证
- 系统状态机验证

## 总结

FreeRTOS验证需要考虑并发性、实时性和内存安全等多个方面。通过CodeDetect，您可以：

1. 验证任务安全性
2. 检查队列操作
3. 分析信号量使用
4. 验证中断处理
5. 进行系统级分析

## 下一步

- 查看 [FreeRTOS示例](../../examples/freertos/)
- 阅读 [CBMC集成指南](../cbmc-integration-guide.md)
- 探索 [高级配置选项](../configuration.md)