cbmc/codedetect/scripts/setup-freertos-verification.sh

#!/bin/bash
# FreeRTOS CBMC验证环境设置脚本

set -e

FREERTOS_VERSION="10.4.6"
FREERTOS_URL="https://github.com/FreeRTOS/FreeRTOS/archive/refs/tags/V${FREERTOS_VERSION}.tar.gz"
INSTALL_DIR="/opt/freertos"
CODEDETECT_DIR="$(pwd)"
FREERTOS_PATH=""

echo "🚀 开始设置FreeRTOS CBMC验证环境..."

# 检查是否已安装
if [ -d "$INSTALL_DIR" ]; then
    echo "✅ FreeRTOS已安装在 $INSTALL_DIR"
    FREERTOS_PATH="$INSTALL_DIR"
else
    # 创建安装目录
    sudo mkdir -p "$INSTALL_DIR"
    sudo chown $USER:$USER "$INSTALL_DIR"

    # 下载并解压FreeRTOS
    echo "📥 下载FreeRTOS V${FREERTOS_VERSION}..."
    cd /tmp
    wget -q "$FREERTOS_URL" -O freertos.tar.gz
    tar -xzf freertos.tar.gz

    # 复制到安装目录
    echo "📦 安装FreeRTOS..."
    cp -r "FreeRTOS-${FREERTOS_VERSION}"/* "$INSTALL_DIR/"

    # 清理
    rm -rf "FreeRTOS-${FREERTOS_VERSION}" freertos.tar.gz

    FREERTOS_PATH="$INSTALL_DIR"
    echo "✅ FreeRTOS已安装到 $INSTALL_DIR"
fi

# 设置环境变量
echo "⚙️  设置环境变量..."
if ! grep -q "FREERTOS_PATH" ~/.bashrc; then
    echo "export FREERTOS_PATH=\"$FREERTOS_PATH\"" >> ~/.bashrc
    echo "export C_INCLUDE_PATH=\"$FREERTOS_PATH/FreeRTOS/Source/include:\$FREERTOS_PATH/FreeRTOS/Plus/Source/FreeRTOS-Plus-CLI/include:\$C_INCLUDE_PATH\"" >> ~/.bashrc
fi

# 验证安装
echo "🔍 验证安装..."
if [ -f "$FREERTOS_PATH/FreeRTOS/Source/include/FreeRTOS.h" ]; then
    echo "✅ FreeRTOS.h found at $FREERTOS_PATH/FreeRTOS/Source/include/FreeRTOS.h"
else
    echo "❌ FreeRTOS.h not found"
    exit 1
fi

# 创建CBMC配置文件
echo "📝 创建CBMC配置文件..."
CONFIG_DIR="$CODEDETECT_DIR/config/freertos"
mkdir -p "$CONFIG_DIR"

cat > "$CONFIG_DIR/cbmc_config.yaml" << 'EOF'
# FreeRTOS CBMC验证配置
cbmc:
  path: "cbmc"
  timeout: 600
  unwind: 50
  depth: 30
  memory_model: "simple"
  output_format: "text"

  # FreeRTOS特定配置
  freertos_mode: true
  freertos_include_path: "/opt/freertos/FreeRTOS/Source/include"

  # 包含路径
  include_paths:
    - "/opt/freertos/FreeRTOS/Source/include"
    - "/opt/freertos/FreeRTOS/Source/portable/GCC/Linux"
    - "/opt/freertos/FreeRTOS/Source/portable/MemMang"

  # 宏定义
  define_macros:
    - "FREERTOS"
    - "CBMC"
    - "configUSE_PREEMPTION=1"
    - "configUSE_PORT_OPTIMISED_TASK_SELECTION=0"
    - "configUSE_TICKLESS_IDLE=0"
    - "configCPU_CLOCK_HZ=16000000"
    - "configTICK_RATE_HZ=1000"
    - "configMAX_PRIORITIES=5"
    - "configMINIMAL_STACK_SIZE=128"
    - "configTOTAL_HEAP_SIZE=8192"
    - "configMAX_TASK_NAME_LEN=16"
    - "configUSE_16_BIT_TICKS=0"
    - "configIDLE_SHOULD_YIELD=1"
    - "configUSE_TASK_NOTIFICATIONS=1"
    - "configUSE_MUTEXES=1"
    - "configUSE_RECURSIVE_MUTEXES=1"
    - "configUSE_COUNTING_SEMAPHORES=1"
    - "configQUEUE_REGISTRY_SIZE=8"
    - "configUSE_QUEUE_SETS=0"
    - "configUSE_TIME_SLICING=1"
    - "configUSE_NEWLIB_REENTRANT=0"
    - "configENABLE_BACKWARD_COMPATIBILITY=0"
    - "configNUM_THREAD_LOCAL_STORAGE_POINTERS=5"

  # 检查选项
  check_assertions: true
  check_overflow: true
  check_bounds: true
  check_division: true
  check_pointers: true
  check_memory_safety: true
  check_concurrency: true

  # 输出选项
  show_locations: true
  show_steps: true
  show_values: true
  show_trace: true
  verbose: false

  # 并发控制
  max_concurrent: 2

  # 缓存选项
  cache_enabled: true

# CodeDetect配置
llm:
  provider: "deepseek"
  model: "deepseek-coder"
  max_tokens: 3000
  temperature: 0.3

web:
  host: "0.0.0.0"
  port: 8080
  debug: false
  max_file_size: "10MB"
EOF

# 创建示例代码目录
echo "📝 创建示例代码..."
EXAMPLE_DIR="$INSTALL_DIR/examples"
mkdir -p "$EXAMPLE_DIR"

# 创建简单的FreeRTOS任务示例
cat > "$EXAMPLE_DIR/simple_task.c" << 'EOF'
#include <FreeRTOS.h>
#include <task.h>
#include <stdio.h>

// 任务函数
void vTaskFunction(void *pvParameters) {
    const char *pcTaskName = "Task";
    TickType_t xLastWakeTime;

    // 初始化xLastWakeTime变量
    xLastWakeTime = xTaskGetTickCount();

    for (;;) {
        // 打印任务信息
        printf("%s is running\n", pcTaskName);

        // 延迟500ms
        vTaskDelayUntil(&xLastWakeTime, pdMS_TO_TICKS(500));
    }
}

int main(void) {
    printf("FreeRTOS CBMC Verification Example\n");

    // 创建任务
    xTaskCreate(
        vTaskFunction,        // 任务函数
        "Task",                // 任务名称
        configMINIMAL_STACK_SIZE, // 堆栈大小
        NULL,                  // 任务参数
        1,                     // 任务优先级
        NULL                   // 任务句柄
    );

    // 启动调度器
    vTaskStartScheduler();

    // 正常情况下不会执行到这里
    for (;;);

    return 0;
}
EOF

# 创建队列操作示例
cat > "$EXAMPLE_DIR/queue_example.c" << 'EOF'
#include <FreeRTOS.h>
#include <task.h>
#include <queue.h>
#include <stdio.h>

// 队列句柄
QueueHandle_t xQueue;

// 发送者任务
void vSenderTask(void *pvParameters) {
    int32_t lValueToSend = 100;
    BaseType_t xStatus;

    for (;;) {
        // 发送数据到队列
        xStatus = xQueueSend(xQueue, &lValueToSend, 0);

        if (xStatus == pdPASS) {
            printf("Sent: %d\n", lValueToSend);
        }

        // 延迟1秒
        vTaskDelay(pdMS_TO_TICKS(1000));

        // 更新发送值
        lValueToSend++;
    }
}

// 接收者任务
void vReceiverTask(void *pvParameters) {
    int32_t lReceivedValue;
    BaseType_t xStatus;
    const TickType_t xTicksToWait = pdMS_TO_TICKS(100);

    for (;;) {
        // 从队列接收数据
        xStatus = xQueueReceive(xQueue, &lReceivedValue, xTicksToWait);

        if (xStatus == pdPASS) {
            printf("Received: %d\n", lReceivedValue);
        } else {
            printf("Could not receive from queue\n");
        }
    }
}

int main(void) {
    printf("FreeRTOS Queue Example\n");

    // 创建队列，长度为5，每个元素大小为int32_t
    xQueue = xQueueCreate(5, sizeof(int32_t));

    if (xQueue == NULL) {
        printf("Failed to create queue\n");
        return 1;
    }

    // 创建发送者任务
    xTaskCreate(
        vSenderTask,
        "Sender",
        configMINIMAL_STACK_SIZE,
        NULL,
        1,
        NULL
    );

    // 创建接收者任务
    xTaskCreate(
        vReceiverTask,
        "Receiver",
        configMINIMAL_STACK_SIZE,
        NULL,
        2,  // 更高优先级
        NULL
    );

    // 启动调度器
    vTaskStartScheduler();

    return 0;
}
EOF

# 创建互斥锁示例
cat > "$EXAMPLE_DIR/mutex_example.c" << 'EOF'
#include <FreeRTOS.h>
#include <task.h>
#include <semphr.h>
#include <stdio.h>

// 互斥锁句柄
SemaphoreHandle_t xMutex;

// 共享资源
int32_t lSharedVariable = 0;

// 任务函数
void vTaskFunction(void *pvParameters) {
    const char *pcTaskName = (const char *)pvParameters;
    BaseType_t xStatus;

    for (;;) {
        // 获取互斥锁
        xStatus = xSemaphoreTake(xMutex, portMAX_DELAY);

        if (xStatus == pdTRUE) {
            // 临界区开始
            int32_t lLocalCopy = lSharedVariable;
            printf("%s: Read shared variable = %d\n", pcTaskName, lLocalCopy);

            // 修改共享变量
            lLocalCopy++;
            lSharedVariable = lLocalCopy;

            printf("%s: Wrote shared variable = %d\n", pcTaskName, lSharedVariable);

            // 释放互斥锁
            xSemaphoreGive(xMutex);
        }

        // 延迟
        vTaskDelay(pdMS_TO_TICKS(1000));
    }
}

int main(void) {
    printf("FreeRTOS Mutex Example\n");

    // 创建互斥锁
    xMutex = xSemaphoreCreateMutex();

    if (xMutex == NULL) {
        printf("Failed to create mutex\n");
        return 1;
    }

    // 创建任务1
    xTaskCreate(
        vTaskFunction,
        "Task1",
        configMINIMAL_STACK_SIZE,
        (void *)"Task1",
        1,
        NULL
    );

    // 创建任务2
    xTaskCreate(
        vTaskFunction,
        "Task2",
        configMINIMAL_STACK_SIZE,
        (void *)"Task2",
        2,
        NULL
    );

    // 启动调度器
    vTaskStartScheduler();

    return 0;
}
EOF

# 创建CBMC验证脚本
cat > "$EXAMPLE_DIR/verify_with_cbmc.sh" << 'EOF'
#!/bin/bash
# FreeRTOS CBMC验证脚本

set -e

FREERTOS_PATH="/opt/freertos"
EXAMPLE_DIR="$FREERTOS_PATH/examples"
CODEDETECT_DIR="$(pwd)"

echo "🔍 开始FreeRTOS CBMC验证..."

# 检查CBMC是否可用
if ! command -v cbmc &> /dev/null; then
    echo "❌ CBMC未安装，请先安装CBMC"
    exit 1
fi

# 检查FreeRTOS路径
if [ ! -d "$FREERTOS_PATH" ]; then
    echo "❌ FreeRTOS未安装，请先运行setup-freertos-example.sh"
    exit 1
fi

# 验证简单任务示例
echo "📋 验证简单任务示例..."
cd "$EXAMPLE_DIR"
if [ -f "simple_task.c" ]; then
    echo "验证 simple_task.c..."
    cbmc --unwind 50 --depth 30 \
         -I "$FREERTOS_PATH/FreeRTOS/Source/include" \
         -I "$FREERTOS_PATH/FreeRTOS/Source/portable/GCC/Linux" \
         -I "$FREERTOS_PATH/FreeRTOS/Source/portable/MemMang" \
         -DFREERTOS -DCBMC \
         simple_task.c 2>&1 | head -20
fi

# 验证队列示例
echo "📋 验证队列示例..."
if [ -f "queue_example.c" ]; then
    echo "验证 queue_example.c..."
    cbmc --unwind 50 --depth 30 \
         -I "$FREERTOS_PATH/FreeRTOS/Source/include" \
         -I "$FREERTOS_PATH/FreeRTOS/Source/portable/GCC/Linux" \
         -I "$FREERTOS_PATH/FreeRTOS/Source/portable/MemMang" \
         -DFREERTOS -DCBMC \
         queue_example.c 2>&1 | head -20
fi

# 验证互斥锁示例
echo "📋 验证互斥锁示例..."
if [ -f "mutex_example.c" ]; then
    echo "验证 mutex_example.c..."
    cbmc --unwind 50 --depth 30 \
         -I "$FREERTOS_PATH/FreeRTOS/Source/include" \
         -I "$FREERTOS_PATH/FreeRTOS/Source/portable/GCC/Linux" \
         -I "$FREERTOS_PATH/FreeRTOS/Source/portable/MemMang" \
         -DFREERTOS -DCBMC \
         mutex_example.c 2>&1 | head -20
fi

echo "✅ FreeRTOS CBMC验证完成"

# 使用CodeDetect进行验证
if [ -d "$CODEDETECT_DIR" ]; then
    echo "🚀 使用CodeDetect进行FreeRTOS验证..."
    cd "$CODEDETECT_DIR"

    # 运行FreeRTOS特定的测试
    python -m pytest tests/integration/test_freertos_verification.py -v --tb=short
fi

echo "🎉 所有验证完成"
EOF

chmod +x "$EXAMPLE_DIR/verify_with_cbmc.sh"

# 创建README文件
cat > "$EXAMPLE_DIR/README.md" << 'EOF'
# FreeRTOS CBMC验证示例

本目录包含用于CodeDetect的FreeRTOS验证示例。

## 目录结构

- `simple_task.c` - 简单的FreeRTOS任务示例
- `queue_example.c` - 队列操作示例
- `mutex_example.c` - 互斥锁使用示例
- `verify_with_cbmc.sh` - CBMC验证脚本

## 环境设置

确保已安装以下组件：

1. **FreeRTOS**: 运行 `../scripts/setup-freertos-example.sh`
2. **CBMC**: 安装CBMC模型检查器
3. **CodeDetect**: 确保CodeDetect项目可用

## 使用方法

### 直接CBMC验证

```bash
# 验证单个文件
cbmc --unwind 50 --depth 30 -I/opt/freertos/FreeRTOS/Source/include -DFREERTOS -DCBMC simple_task.c

# 运行所有验证
./verify_with_cbmc.sh
```

### 使用CodeDetect验证

```bash
# 从CodeDetect项目根目录运行
python -m pytest tests/integration/test_freertos_verification.py -v

# 或者使用完整的工作流
python scripts/run_comprehensive_tests.sh --include freertos
```

## 示例说明

### 1. 简单任务示例
演示基本的任务创建和调度功能。

### 2. 队列示例
演示任务间通过队列进行通信。

### 3. 互斥锁示例
演示资源同步和互斥访问。

## 验证目标

- 内存安全性检查
- 空指针解引用检测
- 缓冲区溢出检查
- 数据竞争检测
- 死锁检测
- 任务调度正确性

## 故障排除

### 常见问题

1. **CBMC未找到**: 确保CBMC已安装并在PATH中
2. **FreeRTOS头文件缺失**: 检查环境变量FREERTOS_PATH设置
3. **验证超时**: 增加unwind和depth参数值

### 调试技巧

1. 使用`--show-properties`查看验证属性
2. 使用`--trace`生成详细执行轨迹
3. 使用`--xml-ui`获取结构化输出

## 扩展示例

要创建新的验证示例：

1. 创建包含FreeRTOS API调用的C文件
2. 确保包含必要的头文件
3. 定义CBMC特定的宏
4. 编写测试用例和断言

## 参考资料

- [FreeRTOS官方文档](https://www.freertos.org/)
- [CBMC用户手册](https://www.cprover.org/cbmc/)
- [CodeDetect项目文档](https://github.com/your-org/codedetect)
EOF

echo "✅ FreeRTOS CBMC验证环境设置完成"
echo "📍 FreeRTOS路径: $FREERTOS_PATH"
echo "📁 示例代码目录: $EXAMPLE_DIR"
echo "🔧 请运行 'source ~/.bashrc' 来加载环境变量"
echo "🚀 运行 './verify_with_cbmc.sh' 来验证示例代码"