cbmc/codedetect/examples/freertos/queue_verification_example.c

/*
 * FreeRTOS队列验证示例
 *
 * 本示例演示了如何使用CodeDetect系统验证FreeRTOS队列操作的安全性。
 * 包括队列创建、发送、接收、溢出处理和并发访问验证。
 */

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

/* 队列配置参数 */
#define QUEUE_LENGTH 10
#define ITEM_SIZE sizeof(uint32_t)
#define MAX_QUEUE_ITEMS 100

/* 任务优先级定义 */
#define PRODUCER_PRIORITY (tskIDLE_PRIORITY + 1)
#define CONSUMER_PRIORITY (tskIDLE_PRIORITY + 2)
#define MONITOR_PRIORITY (tskIDLE_PRIORITY + 3)

/* 队列消息类型 */
typedef struct {
    uint32_t message_id;
    uint32_t data_value;
    TickType_t timestamp;
    BaseType_t is_critical;
} QueueMessage_t;

/* 队列统计信息 */
typedef struct {
    uint32_t total_sent;
    uint32_t total_received;
    uint32_t queue_full_errors;
    uint32_t queue_empty_errors;
    uint32_t checksum_errors;
} QueueStats_t;

/* 全局变量 */
QueueHandle_t xMessageQueue = NULL;
QueueHandle_t xStatsQueue = NULL;
QueueStats_t xQueueStats = {0};
TaskHandle_t xProducerTaskHandle = NULL;
TaskHandle_t xConsumerTaskHandle = NULL;
TaskHandle_t xMonitorTaskHandle = NULL;

/**
 * @brief 生产者任务 - 向队列发送消息
 *
 * 该任务演示了：
 * 1. 队列发送操作的错误处理
 * 2. 队列满状态的处理
 * 3. 消息序列号生成
 * 4. 关键消息的优先处理
 *
 * @param pvParameters 任务参数
 */
void vProducerTask(void *pvParameters) {
    QueueMessage_t xMessage;
    BaseType_t xSendResult;
    uint32_t ulMessageCounter = 0;

    /* 参数验证 */
    configASSERT(pvParameters != NULL);
    configASSERT(xMessageQueue != NULL);

    for (;;) {
        /* 构建消息 */
        xMessage.message_id = ulMessageCounter++;
        xMessage.data_value = ulMessageCounter * 2;  /* 简单的数据计算 */
        xMessage.timestamp = xTaskGetTickCount();
        xMessage.is_critical = (ulMessageCounter % 10 == 0);  /* 每10个消息一个关键消息 */

        /* 尝试发送消息 */
        if (xMessage.is_critical) {
            /* 关键消息使用更长等待时间 */
            xSendResult = xQueueSend(xMessageQueue, &xMessage, pdMS_TO_TICKS(100));
        } else {
            /* 普通消息使用较短等待时间 */
            xSendResult = xQueueSend(xMessageQueue, &xMessage, pdMS_TO_TICKS(10));
        }

        /* 更新统计信息 */
        taskENTER_CRITICAL();
        xQueueStats.total_sent++;
        if (xSendResult != pdPASS) {
            xQueueStats.queue_full_errors++;
        }
        taskEXIT_CRITICAL();

        /* 如果发送失败，记录错误但继续运行 */
        if (xSendResult != pdPASS) {
            /* 队列满，等待一段时间再试 */
            vTaskDelay(pdMS_TO_TICKS(50));
        }

        /* 控制消息生成速率 */
        vTaskDelay(pdMS_TO_TICKS(100));

        /* 防止消息计数器溢出 */
        if (ulMessageCounter >= MAX_QUEUE_ITEMS) {
            ulMessageCounter = 0;
        }
    }
}

/**
 * @brief 消费者任务 - 从队列接收消息
 *
 * 该任务演示了：
 * 1. 队列接收操作的阻塞和非阻塞模式
 * 2. 队列空状态的处理
 * 3. 消息验证和处理
 * 4. 统计信息更新
 *
 * @param pvParameters 任务参数
 */
void vConsumerTask(void *pvParameters) {
    QueueMessage_t xReceivedMessage;
    BaseType_t xReceiveResult;
    uint32_t ulExpectedId = 0;

    /* 参数验证 */
    configASSERT(pvParameters != NULL);
    configASSERT(xMessageQueue != NULL);

    for (;;) {
        /* 尝试从队列接收消息 */
        xReceiveResult = xQueueReceive(xMessageQueue, &xReceivedMessage, pdMS_TO_TICKS(200));

        if (xReceiveResult == pdPASS) {
            /* 成功接收消息，进行验证 */
            taskENTER_CRITICAL();
            xQueueStats.total_received++;

            /* 验证消息序列号 */
            if (xReceivedMessage.message_id != ulExpectedId) {
                xQueueStats.checksum_errors++;
                /* 重新同步序列号 */
                ulExpectedId = xReceivedMessage.message_id + 1;
            } else {
                ulExpectedId++;
            }
            taskEXIT_CRITICAL();

            /* 处理消息（这里只是简单验证） */
            if (xReceivedMessage.data_value % 2 == 0) {
                /* 偶数值处理 */
            } else {
                /* 奇数值处理 */
            }

            /* 如果是关键消息，记录到统计队列 */
            if (xReceivedMessage.is_critical && xStatsQueue != NULL) {
                xQueueSend(xStatsQueue, &xReceivedMessage, 0);
            }
        } else {
            /* 接收超时，记录空队列错误 */
            taskENTER_CRITICAL();
            xQueueStats.queue_empty_errors++;
            taskEXIT_CRITICAL();
        }

        /* 控制处理速率 */
        vTaskDelay(pdMS_TO_TICKS(50));
    }
}

/**
 * @brief 监控任务 - 监控队列状态和统计信息
 *
 * @param pvParameters 任务参数
 */
void vMonitorTask(void *pvParameters) {
    QueueStats_t local_stats;
    UBaseType_t uxItemsWaiting;
    QueueMessage_t critical_message;

    /* 参数验证 */
    configASSERT(pvParameters != NULL);
    configASSERT(xMessageQueue != NULL);

    for (;;) {
        /* 获取队列状态 */
        uxItemsWaiting = uxQueueMessagesWaiting(xMessageQueue);

        /* 复制统计信息 */
        taskENTER_CRITICAL();
        local_stats = xQueueStats;
        taskEXIT_CRITICAL();

        /* 检查队列健康状态 */
        if (uxItemsWaiting > QUEUE_LENGTH * 0.8) {
            /* 队列接近满，需要关注 */
        }

        if (local_stats.queue_full_errors > 0 || local_stats.queue_empty_errors > 0) {
            /* 有错误发生，可能需要调整 */
        }

        /* 处理关键消息统计 */
        if (xStatsQueue != NULL) {
            while (xQueueReceive(xStatsQueue, &critical_message, 0) == pdPASS) {
                /* 处理关键消息统计 */
            }
        }

        /* 定期报告 */
        vTaskDelay(pdMS_TO_TICKS(1000));
    }
}

/**
 * @brief 创建队列验证系统
 *
 * @return BaseType_t 创建结果
 */
BaseType_t xCreateQueueVerificationSystem(void) {
    BaseType_t xReturn = pdPASS;

    /* 创建主消息队列 */
    xMessageQueue = xQueueCreate(QUEUE_LENGTH, ITEM_SIZE);
    if (xMessageQueue == NULL) {
        return pdFAIL;
    }

    /* 创建统计信息队列 */
    xStatsQueue = xQueueCreate(QUEUE_LENGTH / 2, sizeof(QueueMessage_t));
    if (xStatsQueue == NULL) {
        vQueueDelete(xMessageQueue);
        xMessageQueue = NULL;
        return pdFAIL;
    }

    /* 初始化统计信息 */
    memset(&xQueueStats, 0, sizeof(QueueStats_t));

    /* 创建生产者任务 */
    xReturn = xTaskCreate(
        vProducerTask,
        "Producer",
        configMINIMAL_STACK_SIZE,
        NULL,
        PRODUCER_PRIORITY,
        &xProducerTaskHandle
    );

    if (xReturn != pdPASS) {
        goto cleanup;
    }

    /* 创建消费者任务 */
    xReturn = xTaskCreate(
        vConsumerTask,
        "Consumer",
        configMINIMAL_STACK_SIZE,
        NULL,
        CONSUMER_PRIORITY,
        &xConsumerTaskHandle
    );

    if (xReturn != pdPASS) {
        goto cleanup;
    }

    /* 创建监控任务 */
    xReturn = xTaskCreate(
        vMonitorTask,
        "Monitor",
        configMINIMAL_STACK_SIZE,
        NULL,
        MONITOR_PRIORITY,
        &xMonitorTaskHandle
    );

    if (xReturn != pdPASS) {
        goto cleanup;
    }

    return pdPASS;

cleanup:
    /* 清理已创建的资源 */
    if (xProducerTaskHandle != NULL) {
        vTaskDelete(xProducerTaskHandle);
        xProducerTaskHandle = NULL;
    }

    if (xConsumerTaskHandle != NULL) {
        vTaskDelete(xConsumerTaskHandle);
        xConsumerTaskHandle = NULL;
    }

    if (xMonitorTaskHandle != NULL) {
        vTaskDelete(xMonitorTaskHandle);
        xMonitorTaskHandle = NULL;
    }

    vQueueDelete(xStatsQueue);
    xStatsQueue = NULL;
    vQueueDelete(xMessageQueue);
    xMessageQueue = NULL;

    return pdFAIL;
}

/**
 * @brief 停止队列验证系统
 */
void vStopQueueVerificationSystem(void) {
    /* 删除所有任务 */
    if (xProducerTaskHandle != NULL) {
        vTaskDelete(xProducerTaskHandle);
        xProducerTaskHandle = NULL;
    }

    if (xConsumerTaskHandle != NULL) {
        vTaskDelete(xConsumerTaskHandle);
        xConsumerTaskHandle = NULL;
    }

    if (xMonitorTaskHandle != NULL) {
        vTaskDelete(xMonitorTaskHandle);
        xMonitorTaskHandle = NULL;
    }

    /* 删除队列 */
    if (xStatsQueue != NULL) {
        vQueueDelete(xStatsQueue);
        xStatsQueue = NULL;
    }

    if (xMessageQueue != NULL) {
        vQueueDelete(xMessageQueue);
        xMessageQueue = NULL;
    }
}

/**
 * @brief 获取队列统计信息
 *
 * @param pxStats 输出统计信息
 * @return BaseType_t 操作结果
 */
BaseType_t xGetQueueStats(QueueStats_t *pxStats) {
    if (pxStats == NULL) {
        return pdFAIL;
    }

    taskENTER_CRITICAL();
    *pxStats = xQueueStats;
    taskEXIT_CRITICAL();

    return pdPASS;
}

/**
 * @brief 主函数 - 演示队列验证系统
 */
int main(void) {
    BaseType_t xResult;
    QueueStats_t xStats;

    /* 创建队列验证系统 */
    xResult = xCreateQueueVerificationSystem();

    if (xResult != pdPASS) {
        /* 系统创建失败 */
        return -1;
    }

    /* 让系统运行一段时间 */
    vTaskDelay(pdMS_TO_TICKS(5000));

    /* 获取统计信息 */
    xResult = xGetQueueStats(&xStats);

    if (xResult == pdPASS) {
        /* 可以在这里处理统计信息 */
        (void)xStats;  /* 避免未使用变量警告 */
    }

    /* 停止系统 */
    vStopQueueVerificationSystem();

    return 0;
}

/*
 * CodeDetect验证要点：
 *
 * 1. 队列安全验证：
 *    - 队列创建和删除的正确性
 *    - 队列满和空状态的处理
 *    - 队列大小和消息大小的验证
 *
 * 2. 并发访问验证：
 *    - 多任务并发访问队列的安全性
 *    - 关键区域的保护
 *    - 统计信息的一致性
 *
 * 3. 内存安全验证：
 *    - 消息结构的边界检查
 *    - 队列缓冲区溢出检测
 *    - NULL指针验证
 *
 * 4. 错误处理验证：
 *    - 队列操作失败的处理
 *    - 资源不足的情况处理
 *    - 任务同步和通信
 *
 * 5. CBMC规范生成：
 *    - 队列操作的前置条件
 *    - 消息完整性约束
 *    - 并发访问的安全性保证
 *    - 错误恢复路径
 */