C程序精确形状分析中的规范语言设计

Specification Language for Precise Shape Analysis of C Program

在一个C程序静态分析工具的实现中,设计了一种描述函数行为的规范语言,包括描述程序状态的基本断言,描述内存的谓词以及描述链表、二叉树等递归数据结构的形状谓词.该工具基于编译框架LLVM和符号执行工具KLEE,以函数为单位分析并构造函数行为规范,该过程中需要使用断言描述程序状态并按需抽象成形状谓词表示的形式.为此本文设计并实现了一系列的断言规范化和抽象化规则.通过使用描述内存的谓词以及形状谓词,该分析工具可以检测内存泄露、多次释放等内存安全问题以及进行形状分析.

This paper proposes a specification language for describing function behaviors,including assertions for program states,predicates for memory,shape predicates for lists and binary trees in a static analysis tool for C programs.The tool is based on a compiler framework LLVM and symbolic execution tool KLEE.The tool analyses and builds specifications for each function.In this process,we use an assertion language to describe program states and abstract the program states into shape predicates whenever needed.We propose a series of rules to do the normalization and abstraction on assertions.The analysis tool can check memory leaks,double free and other memory safety issues and can do shape analysis with the help of the predicates.