cbmc/codedetect/examples/freertos/task_verification_example.c

/*
 * FreeRTOS任务验证示例
 *
 * 本示例演示了如何使用CodeDetect系统验证FreeRTOS任务创建和管理的安全性。
 * 包括任务参数验证、栈空间检查、优先级处理等常见验证场景。
 */

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

/* 任务参数结构体 */
typedef struct {
    uint32_t task_id;
    uint32_t counter;
    uint32_t max_count;
    BaseType_t should_stop;
} TaskParameters_t;

/* 任务栈大小定义 */
#define TASK_STACK_SIZE configMINIMAL_STACK_SIZE * 2
#define TASK_PRIORITY (tskIDLE_PRIORITY + 2)

/* 全局任务句柄 */
TaskHandle_t xTaskHandle = NULL;

/**
 * @brief FreeRTOS任务函数 - 计数器任务
 *
 * 该任务演示了：
 * 1. 安全的参数处理
 * 2. NULL指针检查
 * 3. 边界检查
 * 4. 任务间通信
 * 5. 优雅的任务终止
 *
 * @param pvParameters 任务参数指针
 */
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);

    /* 任务初始化 */
    params->counter = 0;
    params->should_stop = pdFALSE;

    /* 主任务循环 */
    while (params->should_stop == pdFALSE) {
        /* 边界检查 - 防止计数器溢出 */
        if (params->counter < params->max_count) {
            params->counter++;
        } else {
            /* 达到最大值，重置计数器 */
            params->counter = 0;
        }

        /* 模拟一些工作负载 */
        vTaskDelay(pdMS_TO_TICKS(100));
    }

    /* 任务清理 */
    params->counter = 0;

    /* 任务自删除 */
    vTaskDelete(NULL);
}

/**
 * @brief 创建验证任务的函数
 *
 * @return BaseType_t 任务创建结果
 */
BaseType_t xCreateVerificationTask(void) {
    TaskParameters_t *task_params;
    BaseType_t xReturn;

    /* 分配任务参数内存 */
    task_params = (TaskParameters_t *)pvPortMalloc(sizeof(TaskParameters_t));

    if (task_params == NULL) {
        /* 内存分配失败 */
        return pdFAIL;
    }

    /* 初始化任务参数 */
    task_params->task_id = 1;
    task_params->counter = 0;
    task_params->max_count = 100;
    task_params->should_stop = pdFALSE;

    /* 创建任务 */
    xReturn = xTaskCreate(
        vCounterTask,                    /* 任务函数 */
        "CounterTask",                   /* 任务名称 */
        TASK_STACK_SIZE,                 /* 栈大小 */
        task_params,                     /* 任务参数 */
        TASK_PRIORITY,                   /* 任务优先级 */
        &xTaskHandle                     /* 任务句柄 */
    );

    if (xReturn != pdPASS) {
        /* 任务创建失败，清理资源 */
        vPortFree(task_params);
        return pdFAIL;
    }

    return pdPASS;
}

/**
 * @brief 安全的任务控制函数
 *
 * @param xStop 是否停止任务
 * @return BaseType_t 操作结果
 */
BaseType_t xControlTask(BaseType_t xStop) {
    if (xTaskHandle == NULL) {
        /* 任务句柄无效 */
        return pdFAIL;
    }

    if (xStop) {
        /* 安全的任务停止 - 通过参数控制 */
        TaskParameters_t *params;
        eTaskState state = eTaskGetState(xTaskHandle);

        if (state == eDeleted) {
            /* 任务已删除 */
            return pdFAIL;
        }

        /* 获取任务参数 */
        params = (TaskParameters_t *)pvTaskGetThreadLocalStoragePointer(xTaskHandle, 0);

        if (params != NULL) {
            /* 设置停止标志 */
            params->should_stop = pdTRUE;
            return pdPASS;
        }
    }

    return pdFAIL;
}

/**
 * @brief 任务清理函数
 */
void vCleanupTask(void) {
    if (xTaskHandle != NULL) {
        TaskParameters_t *params;

        /* 获取任务参数 */
        params = (TaskParameters_t *)pvTaskGetThreadLocalStoragePointer(xTaskHandle, 0);

        if (params != NULL) {
            /* 释放参数内存 */
            vPortFree(params);
        }

        /* 删除任务 */
        vTaskDelete(xTaskHandle);
        xTaskHandle = NULL;
    }
}

/**
 * @brief 任务状态监控函数
 *
 * @return uint32_t 当前任务状态
 */
uint32_t ulGetTaskStatus(void) {
    if (xTaskHandle == NULL) {
        return 0; /* 任务不存在 */
    }

    TaskParameters_t *params;
    params = (TaskParameters_t *)pvTaskGetThreadLocalStoragePointer(xTaskHandle, 0);

    if (params == NULL) {
        return 0; /* 参数无效 */
    }

    /* 返回任务状态信息 */
    return (params->task_id << 24) |
           (params->counter << 8) |
           (params->should_stop & 0xFF);
}

/**
 * @brief 主函数 - 演示任务创建和管理
 */
int main(void) {
    BaseType_t xResult;

    /* 创建验证任务 */
    xResult = xCreateVerificationTask();

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

    /* 让任务运行一段时间 */
    vTaskDelay(pdMS_TO_TICKS(2000));

    /* 停止任务 */
    xResult = xControlTask(pdTRUE);

    if (xResult == pdPASS) {
        /* 等待任务停止 */
        vTaskDelay(pdMS_TO_TICKS(500));
    }

    /* 清理资源 */
    vCleanupTask();

    return 0;
}

/*
 * CodeDetect验证要点：
 *
 * 1. 内存安全验证：
 *    - 参数指针有效性检查
 *    - 内存分配和释放的正确性
 *    - 栈空间使用验证
 *
 * 2. 并发安全验证：
 *    - 任务状态一致性
 *    - 共享资源访问控制
 *    - 任务同步机制
 *
 * 3. 边界验证：
 *    - 计数器溢出检查
 *    - 数组边界验证
 *    - 任务优先级范围检查
 *
 * 4. 错误处理验证：
 *    - NULL指针处理
 *    - 资源分配失败处理
 *    - 任务状态转换验证
 *
 * 5. CBMC规范生成：
 *    - 任务参数前置条件
 *    - 循环终止条件
 *    - 资源访问约束
 *    - 错误状态处理
 */