一种基于栈区内存模型的C程序别名判断算法

Alias Analysis Algorithm for C Programs Based on a Stack Memory Model

C语言中的指针导致C程序中会出现表达式别名的情况.在基于演绎推理的程序验证中,使用Hoare逻辑的赋值规则前必须消除断言中的别名.别名增加了程序验证的难度.本文根据C语言的语义提出了一种栈区内存模型,可以精确地跟踪栈区的多种类型的表达式,包括取地址、多级解引用、指针关系运算、结构体和数组等.基于上述内存模型,本文提出了一种判断别名的算法,使得验证工具在使用Hoare逻辑的赋值公理之前可以准确的消除断言中的别名.目前该模型已经在一个名为Safe-C验证器的程序验证工具中实现,并且成功验证了多例经典程序.

Pointers in the C language causes potential aliasing among expressions in a C program. In program verification based on deductive reasoning,the aliases in the assertions must be eliminated before applying the Hoare logic assignment rule. Aliasing increases the difficulty of verifying C programs. Based on C semantics,this paper proposes a memory model that can accurately trace various kind of C expressions in the stack area,including address-taking,multi-level de-reference,pointer relation operation,structure and array,etc. According to this model,this paper proposes an algorithm to identify aliases,which enables the verification tool to accurately eliminate the aliases in the assertions before using the Hoare logic assignment axiom. We have implemented the proposed model in a program verification tool named Safe-C Verifier,which has successfully verified many classic C programs.