关于在Frama-C框架中添加sizeof T[n]支持的技术问询

问题概述 #

C语言中sizeof(T[n])是变长数组（VLA）的显式构造，常用于malloc这类动态分配场景，但Frama-C 29.0 [Copper]对该语法的支持存在限制：内核会直接拒绝此类代码，报错提示数组长度非编译时常量，且当前仅允许变长数组的第一维度为变量。

示例1（内核拒绝） #

#include <stdlib.h>

int *foo(int n, int x)
{
    int *a = malloc(sizeof(int[n]));
    a[n - 1] = x;
    return a;
}

内核报错信息：

[kernel] mem.c:5: User Error: 
  Array length n is not a compile-time constant,
  and currently VLAs may only have their first dimension as variable.

示例2（GCC可编译但Frama-C拒绝） #

#include <assert.h>
#include <stdlib.h>

int *foo(int n, int x)
{
    int (*a)[n] = malloc(sizeof(int[n]));
    assert(sizeof(*a) == sizeof(int[n]));
    (*a)[n - 1] = x;
    return (*a);
}

以下针对实现基础支持的难度、内核修改点、Eva适配方案及临时解决方法逐一说明：

实现基础支持的难度 #

基础支持的实现难度为中等：无需重构整个类型系统，但需要修改内核的类型检查逻辑、sizeof表达式求值机制，同时适配Eva分析域的内存建模。若仅针对sizeof(T[n])用于malloc参数的场景，可缩小修改范围，进一步降低复杂度。

内核层面需要的支持 #

• 类型检查逻辑修改

  • 放宽sizeof操作数的VLA限制：当前内核仅允许VLA作为数组类型的第一维度，需修改kernel/typing模块的相关检查，允许sizeof直接接受T[n]形式的VLA类型。
  • 新增sizeof(VLA)的类型推导规则：明确sizeof(T[n])的类型为size_t，语义等价于sizeof(T) * n，其中n为运行时变量。

• sizeof表达式求值机制扩展

  • 在kernel/eval模块中添加VLA类型的sizeof求值逻辑：当操作数为T[n]时，将其转换为sizeof(T) * n的算术表达式，而非直接报错。
  • 处理运行时变量依赖：将n的符号值纳入表达式的依赖集合，确保后续分析（如Eva）能跟踪该值的范围。

• AST节点适配

  • 确保抽象语法树（AST）能正确表示sizeof(T[n])节点，无需将其拆分为复杂的数组类型声明。

Eva分析域的适配开发 #

Eva作为Frama-C的抽象解释器，需修改内存分配建模逻辑以利用sizeof(T[n])的特性：

• 内存块大小跟踪

  • 当malloc参数为sizeof(T[n])时，将分配的内存块大小关联到sizeof(T) * n的符号表达式，而非仅记录常量值或模糊范围。
  • 在eva/malloc.c模块中添加VLA sizeof表达式的处理逻辑，提取变量n并与分配的内存块绑定。

• 指针与内存块的关联

  • 针对指向VLA的指针（如int (*a)[n]），跟踪指针指向的VLA类型信息（包括长度n），确保后续(*a)[n-1]这类访问能被正确做边界检查。
  • 扩展Eva的指针域，支持携带VLA长度信息，避免函数返回时丢失关键数据（如示例2中return (*a)时，需将VLA长度传递给返回指针）。

• 抽象状态更新

  • 在抽象状态中记录VLA长度的符号值范围，确保内存访问时能进行有效边界检查，避免误报越界错误。

让示例代码临时工作的方法（非完整支持） #

若仅需让示例代码通过Frama-C内核检查并完成基础分析，可采用以下临时方案：

• 手动展开sizeof(T[n])语义
  将示例1中的malloc(sizeof(int[n]))替换为malloc(sizeof(int) * n)，内核即可正常接受：

  #include <stdlib.h>
  
  int *foo(int n, int x)
  {
      int *a = malloc(sizeof(int) * n);
      a[n - 1] = x;
      return a;
  }
  

  此方案本质是手动实现sizeof(T[n])的等价逻辑，避开Frama-C的VLA限制。

• 临时修改内核检查逻辑（仅实验用）
  定位到内核中检查VLA维度的代码（如kernel/typing/type_utils.ml），注释掉对非第一维度VLA的检查逻辑，可临时让sizeof(T[n])通过内核校验。此方法仅适合实验场景，不建议用于正式分析。

内容的提问来源于stack exchange，提问作者invertedPanda