形状图逻辑和形状系统 中国科学技术大学 报告人 陈意云

Presentation on theme: "形状图逻辑和形状系统 中国科学技术大学 报告人 陈意云"— Presentation transcript:

1 形状图逻辑和形状系统 中国科学技术大学 报告人 陈意云 0551-3607043，yiyun@ustc.edu.cn
报告人 陈意云 1

2 报 告 提 纲 形状图逻辑 形状系统 循环不变形状图的推断 复杂易变数据结构的解决方案 形状图，形状图的变换规则，形状图的语义，形状图逻辑
报 告 提 纲 形状图逻辑 形状图，形状图的变换规则，形状图的语义，形状图逻辑 形状系统 形状定义、形状推断、形状检查 循环不变形状图的推断 复杂易变数据结构的解决方案

3 形状图逻辑 形状图 描述静态声明的指针和动态分配的结构体中域指针的指向的一种有向图 能准确地表达指针之间的相等关系 直接作为指针断言
NULL指针 h  nxt . . . m个节点, m>=0 p1 p n个节点, n>=0 一个直观的单链表示意图

4 形状图逻辑 形状图：语法 描述静态声明的指针和动态分配的结构体中域指针的指向的一种有向图 能准确地表达指针之间的相等关系 直接作为指针断言
NULL指针 h  nxt . . . m个节点, m>=0 p1 p n个节点, n>=0 一个直观的单链表示意图 h nxt p1 p  m, m>=0 n, n>=0 用形状图浓缩表示为

5 形状图逻辑 形状图：语法 一个双向链表示意图 用形状图浓缩表示为 h  r . . . m -1, m>=0 l h  r
除了r和l外，没有 其他边指向双向 链表的浓缩节点

6 形状图逻辑 数据结构可以用形状图来定义（例举） c_list(h) c_list(h, e, a) 二叉树tree(h) 循环单链表
 r l h  P  tree 二叉树tree(h) 该指针满足 一个谓词  h  P  c_list nxt 循环单链表 c_list(h) 被浓缩的节点数是n, n  0 h  P c_dlist, e, a r e-1, a l (a (e>=1)) 双向循环链表 c_list(h, e, a) （一种情况） 6

7 不确定的双向链表浓缩节点的展开与折叠规则
形状图逻辑 pk表示可能 还有的其他边 形状图：等价变换规则（例举） 双向链表浓缩节点的展开与折叠规则 （点划线框称为窗口W） ( a (e>=1) ) r l e, a  e-1, a 不确定的双向链表浓缩节点的展开与折叠规则   r l pk

8 形状图逻辑 等价变换规则的应用 窗口以外部 分称为上下文 对a (n-1>0)形状图 应用规则 上下文不变 得到形状图 r
n-1, a l h 应用规则 ( a (e>=1) ) r l e, a  e-1, a 上下文不变 得到形状图 r n-2, a l h

9 形状图逻辑 形状图：蕴涵变换规则（例举） 从等价变换规则W  W1W2，可得 W1  W 和 W2  W 从 可得 从 可得
((e1==e2a1)a2)((e2==e1a2)a1) r l e1, a1  e2, a2 从 可得  ((e1==e2  a1)  a2) 从 可得  nt p1 e, a pk e-1, a  a  (e >=1) 9

10 形状图逻辑 形状图：从等价变换系统到重写系统 代数规范 形状图
各种数据结构有浓缩节点和谓词节点的展开和折叠等规则，循环不变形状图推断时需要使用 可以像研究代数规范那样来研究形状图 代数规范 形状图 1. 基于基调定义代数项集 类似地可定义形状图集 2. 代数项之间的等式 形状图的等价变换规则 3. 代数项重写系统 形状图重写系统 4. 终止性和合流性 终止性和合流性 我们系统所使用的形状图重写系统是终止和合流的

11 形状图逻辑 形状图：语义 形状图是抽象机器状态集的图形表示（只包括指针数据存储单元） 展开后得到： 是一个机器状态集的图形表示 h nxt
p1 p  m, m>=0 n, n>=0 展开后得到： h  nxt . . . m个节点, m>=0 p1 p n个节点, n>=0 是一个机器状态集的图形表示

12 形状图逻辑 形状图：语义 形状图是抽象机器状态集的图形表示（只包括指针数据存储单元） 形状图是程序状态中指针相等断言的图形表示
p1->nxt == p p(->nxt)n == NULL 形状图可以作为程序断言，形状图之间符号和就是逻辑合取和析取连接词 形状图的等价变换规则就是形状图断言的等价演算规则 h nxt p1 p  m, m>=0 n, n>=0

13 形状图逻辑 形状图：断言和符号断言的演算规则（例举） 应用该规则 来源于程序中的条 件语句或循环语句 uk表示可能 还有的其他边
 u !=NULL u nxt uk  注：u和uk处于边的下方，表示访问路径 应用该规则  p1->nxt !=NULL  h nxt p1 p  h nxt p1 p 

14 形状图逻辑 形状图逻辑 一种程序逻辑，使得Hoare逻辑扩展到能用于带指针类型的语言 先考虑指针语句的推理规则，它们用于程序的形状分析
推理规则描述语句S前程序点的形状图中,窗口W1怎样变化到W2， W1的上下文G[ ]保持不变 即规则体现：{ G[W1] } S { G[W2] } 也可能涉及两个窗口 { G[W11, W12] } S { G[W21 , W22] }

15 形状图逻辑 形状分析时所用的指针语句的推理规则例举 指针赋值 u = v 的推理规则之一
分配空间语句 u = malloc(t) 的推理规则之一 u = v v nt vk  u Dangling指针 u = malloc(t) u D 结构类型t只有一个域指针f f

16 形状图逻辑 形状图逻辑中指针语句推理规则的可靠性 在有栈和堆的机器模型上
形状图是程序状态集的图形表示，也是指针断言集的图形表示，形状图的变换规则就是有效的断言演算规则 指针语句的推理规则就是相应语句操作语义的图形表示 指针语句的推理规则对操作语义可靠 u = malloc(t) u D f

17 形状图逻辑 程序验证时所用的指针语句的推理规则例举 非指针语句（ Q表示符号断言） 赋值语句x = e
使用Hoare逻辑的赋值公理，它不影响G {GQ[e/x]} x = e {GQ} 其他语句（如不涉及指针的函数调用） 也采用Hoare逻辑的规则，它也不影响G

18 形状图逻辑 程序验证时所用的指针语句的推理规则例举 指针语句 指针赋值语句u = v 本质上不改变Q，根据形状图对Q进行别名代换
前提在形状 分析时得到 程序验证时所用的指针语句的推理规则例举 指针语句 指针赋值语句u = v 本质上不改变Q，根据形状图对Q进行别名代换 Q[u/u]表示Q中u及其别名都用与之相等但不是别名的访问路径u代换 {G} u = v {G} {G  Q} u = v {G  Q[u/u]} h nxt p1 p  m, m>=0 n, n>=0 若对p1赋值，若Q 中有p1->data，则用 h(->nxt)m->data来代换

19 报 告 提 纲 形状图逻辑 形状系统 循环不变形状图的推断 复杂易变数据结构的解决方案 形状图，形状图的变换规则，形状图的语义，形状图逻辑
报 告 提 纲 形状图逻辑 形状图，形状图的变换规则，形状图的语义，形状图逻辑 形状系统 形状定义、形状推断、形状检查 循环不变形状图的推断 复杂易变数据结构的解决方案 19

20 形状图逻辑 完整的形状图逻辑的可靠性 在指针语句推理规则对操作语义可靠的基础上，还需证明 对语句和断言消除别名保持它们原来的语义或含义
在没有别名时， Hoare逻辑的赋值公理的使用是可靠的

21 形 状 系 统 设计形状系统的目的 形状系统包括 抬高合法程序的门槛，降低形状分析和程序验证的难度
形 状 系 统 设计形状系统的目的 抬高合法程序的门槛，降低形状分析和程序验证的难度 利用形状系统排除没有构造出（或操作于）程序员所声明形状的程序 形状系统包括 所允许的各种形状及其定义 形状推断规则 形状检查规则 形状系统的设计和实现基于形状图逻辑 21

22 形 状 系 统 形状推断 形状检查 形状检查的程序点 推断声明指针所在形状子图属于哪种形状 对形状子图进行折叠化简，判断其属于哪种形状
形 状 系 统 形状推断 推断声明指针所在形状子图属于哪种形状 对形状子图进行折叠化简，判断其属于哪种形状 形状检查 检查上述形状推断的结果与相关结构体类型的形状声明是否一致 形状检查的程序点 函数的调用点和返回点 循环语句的入口点和循环体的结束点 程序员指定的其他程序点，帮助发现程序错误 22

23 形 状 系 统 用例：降低循环不变形状图推断的难度 双向链表 循环迭代依次把域指针l都赋值为NULL
形 状 系 统 用例：降低循环不变形状图推断的难度 双向链表 h  r . . . l 循环迭代依次把域指针l都赋值为NULL h  r . . . l 形状系统拒绝这样的程序，因为它偏离了声明的形状 23

24 形 状 系 统 形状系统和类型系统的比较 看似相似但有本质区别 类型系统：给出对静态程序文本的上下文有关的约束，不涉及语言的操作语义
形 状 系 统 形状系统和类型系统的比较 看似相似但有本质区别 类型系统：给出对静态程序文本的上下文有关的约束，不涉及语言的操作语义 形状系统：给出对程序动态地构造的数据结构的形状限制，它依赖于语言的操作语义 类型系统：定型规则是结构化的（根据语言构造的各子构造的类型来确定该语言构造的类型） 形状系统：形状推断和形状检查是根据各节点的连接方式来推断所构成的形状以及它是否被认可 24

25 报 告 提 纲 形状图逻辑 形状系统 循环不变形状图的推断 复杂易变数据结构的解决方案 形状图，形状图的变换规则，形状图的语义，形状图逻辑
报 告 提 纲 形状图逻辑 形状图，形状图的变换规则，形状图的语义，形状图逻辑 形状系统 形状定义、形状推断、形状检查 循环不变形状图的推断 复杂易变数据结构的解决方案 25

26 循环不变形状图的推断 用例子来解释 例子：有序单链表的节点插入函数 1、节点类型声明 程序员声明各种递归结构体类型参与构建的易变
typedef struct listnode { Node *: LIST next; int data; } Node; 程序员声明各种递归结构体类型参与构建的易变 数据结构的形状

27 循环不变形状图的推断 2、函数代码 Node* insert( Node* head, int data) {
Node * ptr, * ptr1, * ret, * p; int j; p = malloc(Node*); p->data = data; p->next = NULL; if (head == NULL) { /* 空表情况 */ } else if (p->data <= head->data) { /* 作为第一个节点*/ } else {/* 插在表中或表尾*/ ptr1 = head; ptr = head->next; j = 1; while( (ptr != NULL) && ( ptr->data < p->data ) ) { ptr1 = ptr; ptr = ptr -> next; j = j+1; } … … /* 以下略去*/ 27

28 循环不变形状图的推断 3、程序员提供函数前后条件和循环不变式 length(head, next) == m  /* 前条件 */
i:1..m-1.(head(->next)i-1->data <= head(->next)i->data) Node* insert( Node* head, int m, int data) { … … if (head == NULL) { … … } else if (p->data <= head->data) { … … } else { ptr1 = head; ptr = head->next; j = 1; while( (ptr != NULL) && ( ptr->data < p->data ) ) { ptr1 = ptr; ptr = ptr -> next; j = j+1; } length(head, next) == m + 1  /* 后条件 */ 28

29 循环不变形状图的推断 循环不变式，分成搜索到表中和表尾两种情况：
… … ptr1 = head; ptr = head->next; j = 1; while( (ptr != NULL) && ( ptr->data < p->data ) ) { ptr1 = ptr; ptr = ptr -> next; j = j+1; } 循环不变式，分成搜索到表中和表尾两种情况： (ptr != NULL  ptr1->data < p->data  j >= 1  i:1..j-1.(head(->next)i-1->data <= head(->next)i->data)  ptr1->data <= ptr->data  i:1..m-j-1.(ptr(->next)i-1->data <= ptr(->next)i->data) )  (ptr == NULL  ptr1->data < p->data  j >= 1  i:1..j-1.(head(->next)i-1->data <=head(->next)i->data) ) 所提供断言无需包括涉及形状的断言 29

30 循环不变形状图的推断 函数入口点和循环前程序点的形状图
Node* insert( Node* head, int m, int data) { … … if (head == NULL) { … … } else if (p->data <= head->data) { … … } else { ptr1 = head; ptr = head->next; j = 1; while( (ptr != NULL) && ( ptr->data < p->data ) ) { ptr1 = ptr; ptr = ptr -> next; j = j+1; } head next  m, m>=0 m-1, m-1>=0 head next  ptr1 ptr p  函数入口点和循环前程序点的形状图 30

31 循环不变形状图的推断 4、循环不变形状图 while( (ptr != NULL) && ( ptr->data < p->data ) ) { ptr1 = ptr; ptr = ptr -> next; j = j+1; } j-1, j-1>=0 m-j, m-j>=0 head next ptr1 ptr  p  31

32 循环不变形状图的推断 循环不变形状图推断的算法框架 对于循环：while (B) S （1）计算循环前条件G0 = Gpre。i = 0
（2）根据形状图逻辑的规则计算Gi ， 使得{Gi  B} S {Gi+1 } （3）应用抽象规则计算Gi+1，使得 Gi+1 Gi+1 （4）若Gi+1  G0…Gi，则G0…Gi是循环不变形状图；否则，i = i + 1，转（2） 32

33 循环不变形状图的推断 保证算法终止的措施一：使用虚拟变量 对于“应用抽象规则计算Gi+1，使得 Gi+1 Gi+1
循环的特点：遍历或生成的节点应该能浓缩 保证能抽象的措施：为循环体的每条执行路径都设有累计该路径执行次数的虚拟变量，先用虚拟变量进行抽象 目前系统的不足：尚未用程序分析技术去寻找含声明变量的线性表达式，以代替虚拟变量 p n   h m-j, m-j>=0 p1 p2 j-1, j-1>=0 33

34 循环不变形状图的推断 保证算法终止的措施二：形状检查 双向链表 循环迭代依次把域指针l都赋值为NULL
h  r . . . l 循环迭代依次把域指针l都赋值为NULL h  r . . . l 形状系统拒绝这样的程序，因为它偏离了声明的形状 34

35 循环不变形状图的推断 保证算法终止的措施三：限制整型表达式 将程序员提供的与形状有关的整型表达式限制到线性表达式
在形状分析中产生的也是线性表达式 p n   h m-j, m-j>=0 p1 p2 j-1, j-1>=0 35

36 循环不变形状图的推断 算法终止的理由 声明指针的个数有限 相邻2个声明指针所指向节点之间的节点数有限 （不超过3个）
在循环体结束点能形成的不等价形状图有限 P p l r q s tree 36

37 报 告 提 纲 形状图逻辑 形状系统 循环不变形状图的推断 复杂易变数据结构的解决方案 形状图，形状图的变换规则，形状图的语义，形状图逻辑
报 告 提 纲 形状图逻辑 形状图，形状图的变换规则，形状图的语义，形状图逻辑 形状系统 形状定义、形状推断、形状检查 循环不变形状图的推断 复杂易变数据结构的解决方案 37

38 复杂易变数据结构的解决方案 数据结构的嵌套 例：双向链表的每个节点都有一个单链表 解决办法： 1、程序员声明域指针的不同作用
h  r . . . l s next  解决办法： 1、程序员声明域指针的不同作用 2、限定这些单链表都是表长不确定的单链表 38

39 复杂易变数据结构的解决方案 有附加单链表的数据结构 例：用附加单链表把数据结构上的部分节点链起来 困难之处：附加单链指针的指向不能静态确定
h  r . . . l a s 困难之处：附加单链指针的指向不能静态确定 解决办法： 1、将附加单链从主链上剥离，建一个虚拟单链表 39

40 复杂易变数据结构的解决方案 有附加单链表的数据结构 例：用附件单链表把数据结构上的部分节点链起来 困难之处：附加单链指针的指向不能静态确定
h  r . . . l s a 困难之处：附加单链指针的指向不能静态确定 解决办法： 1、将附加单链从主链上剥离，建一个虚拟单链表 2、程序员声明附加链指针，增加一些编程约束 40

41 复杂易变数据结构的解决方案 有确定的附加指针的数据结构
例如：队列，带父节点指针的二叉树，left-child right-sibling tree with two kinds of backward links 解决办法： 1、已经定义的5种数据结构作为骨架 2、程序员描述附加指针与骨架上指针之间的关系 3、骨架形状的正确性由形状系统完成 4、从（2）的描述产生附加指针的检查代码

42 复杂易变数据结构的解决方案 例：带父节点指针的二叉树 描述父节点指针和 骨架二叉树的指针之间的关系 s  p_tree(s) 
s == NULL  s != NULL  s->parent == NULL  ptree(s) ptree(s)  (s->left != NULL  s->left->parent == s  ptree(s->left))  (s->right!=NULL  s->right->parent==s ptree(s->right)) … …. …. …. s  42

43 作 业 1、模仿二叉排序树的归纳定义，给出二叉平衡树（见严蔚敏等，数据结构（C语言版）》，清华大学出版社）的归纳定义。
作 业 1、模仿二叉排序树的归纳定义，给出二叉平衡树（见严蔚敏等，数据结构（C语言版）》，清华大学出版社）的归纳定义。 2、除了课堂上已经提到的外，你认为C语言还有哪些数据类型、语言构造和其它语言特征是不利于程序验证的，简述你的理由。 截止时间：7月22日24点 43

44 小 结 从下面几个角度尝试程序验证工具的研发 特色之处 用程序分析所得信息来支持程序验证 降低程序员使用难度 降低自动定理证明器的难度
小 结 从下面几个角度尝试程序验证工具的研发 用程序分析所得信息来支持程序验证 降低程序员使用难度 降低自动定理证明器的难度 特色之处 设计了一种形状图逻辑，优点： 1、直观 2、易于把握全局的指针信息 3、在程序分析的实现中，推理比较简单 4、对自动定理证明有较好的支持 44

45 谢 谢 ！