《第4章-抽象解释》由会员分享，可在线阅读，更多相关《第4章-抽象解释（21页珍藏版）》请在金锄头文库上搜索。
1、第第4章章 抽象解释抽象解释内容概述内容概述以一种独立于编程语言的方式，介绍抽象解释的以一种独立于编程语言的方式，介绍抽象解释的一些本质概念一些本质概念将将“程序分析对语言语义是正确的程序分析对语言语义是正确的”这个概念公这个概念公式化式化用用“加宽和收缩技术加宽和收缩技术”来获得最小不动点的较好来获得最小不动点的较好的近似，并使所需计算步数得到限制的近似，并使所需计算步数得到限制用用“伽罗瓦连接和伽罗瓦插入伽罗瓦连接和伽罗瓦插入”来把代价较大的来把代价较大的属性空间用代价较小的属性空间来代替属性空间用代价较小的属性空间来代替伽罗瓦连接可以通过一种系统的方式来构造，可伽罗瓦连接可以通过一种系统
2、的方式来构造，可用来从一种分析的规范导出另一种分析的规范用来从一种分析的规范导出另一种分析的规范第第4章章 抽象解释抽象解释内容概述内容概述用用“伽罗瓦连接和伽罗瓦插入伽罗瓦连接和伽罗瓦插入”来把代价较大的来把代价较大的属属性空间用代价较小的属性空间来代替性空间用代价较小的属性空间来代替有时，属性完全格有时，属性完全格L上的计算代价太大，甚至不上的计算代价太大，甚至不可计算，因此需用较简单的完全格可计算，因此需用较简单的完全格M来代替来代替L必须有一种用必须有一种用M来描述来描述L的方法，并将采用的方法，并将采用M的的分析替代采用分析替代采用L的分析的分析伽罗瓦连接和伽罗瓦插入是用来表达程序的
3、属性伽罗瓦连接和伽罗瓦插入是用来表达程序的属性空间空间L、属性空间属性空间M之间联系的一种工具之间联系的一种工具第第4章章 抽象解释抽象解释抽象解释抽象解释在程序静态分析中，用于构造和逼近程序不动点在程序静态分析中，用于构造和逼近程序不动点语义的理论语义的理论使用抽象对象域上的计算抽象来逼近程序指称的使用抽象对象域上的计算抽象来逼近程序指称的具体对象域上的计算，使得程序抽象执行的结果具体对象域上的计算，使得程序抽象执行的结果能够反映出程序真实运行的部分信息能够反映出程序真实运行的部分信息本质上是在计算效率和计算精度之间取得均衡，本质上是在计算效率和计算精度之间取得均衡，以损失计算精度来求得计算
4、的可行性，再通过迭以损失计算精度来求得计算的可行性，再通过迭代计算来增强计算精度代计算来增强计算精度第第4章章 抽象解释抽象解释4.1 节节将将“程序分析对语言的语义是正确的程序分析对语言的语义是正确的”这个这个概念公式化概念公式化方式方式1：正确性关系：正确性关系R : V L true, false正确性标准：正确性标准：R在程序计算过程中保持在程序计算过程中保持可接受的正确性关系可接受的正确性关系增加两个条件增加两个条件1、属性值、属性值 l 越小（偏序）越精确越小（偏序）越精确2、存在描述一个值、存在描述一个值 v 的最好属性值的最好属性值 l第第4章章 抽象解释抽象解释4.1 节节将
5、将“程序分析对语言的语义是正确的程序分析对语言的语义是正确的”这个这个概念公式化概念公式化方式方式2：表示函数：表示函数 ： V L， 将将 v 映射到表示它的最好属性值映射到表示它的最好属性值 l两种方式之间的等价两种方式之间的等价从从 可以定义相关的可接受可以定义相关的可接受R从可接受从可接受R可以定义相关的可以定义相关的 第第4章章 抽象解释抽象解释4.1 节节将将“程序分析对语言的语义是正确的程序分析对语言的语义是正确的”这个这个概念公式化概念公式化举例举例数据流分析：常量传播数据流分析：常量传播控制流分析：运行时变量所指称的函数控制流分析：运行时变量所指称的函数适度的推广适度的推广语
6、言语义：程序参数和结果属于不同的论域语言语义：程序参数和结果属于不同的论域程序属性：描述它们的属性则也属于不同的论域程序属性：描述它们的属性则也属于不同的论域正确性关系：相应地，由两个关系正确性关系：相应地，由两个关系R1和和R2组成组成表示函数：相应地，由两个表示函数表示函数：相应地，由两个表示函数 1和和 2组成组成第第4章章 抽象解释抽象解释4.2 节节用加宽和收缩技术来获得最小不动点的较好用加宽和收缩技术来获得最小不动点的较好近似，并使所需计算步数得到限制近似，并使所需计算步数得到限制加宽算子加宽算子上界算子上界算子上界算子作用到一个序列，得到一个上升序列上界算子作用到一个序列，得到一
7、个上升序列加宽算子加宽算子1、对上升序列加宽得到的序列能够稳定、对上升序列加宽得到的序列能够稳定2、对单调函数、对单调函数f 的迭代序列的迭代序列(fn( )n，用加宽算，用加宽算子加宽后得到的序列会稳定，并且子加宽后得到的序列会稳定，并且 lfp(f ) 第第4章章 抽象解释抽象解释4.2 节节用加宽和收缩技术来获得最小不动点的较好用加宽和收缩技术来获得最小不动点的较好近似，并使所需计算步数得到限制近似，并使所需计算步数得到限制收缩算子收缩算子受受f (lfp (f) lfp (f)的启发的启发注意，收缩算子并不是一个下界算子注意，收缩算子并不是一个下界算子对下降序列收缩得到的序列能够稳定，
8、稳定后的对下降序列收缩得到的序列能够稳定，稳定后的值值 lfp(f )第第4章章 抽象解释抽象解释4.3 节节伽罗瓦连接和伽罗瓦插入是表达程序的属伽罗瓦连接和伽罗瓦插入是表达程序的属性空间性空间L和属性空间和属性空间M之间联系的一种工具之间联系的一种工具L和和M的例子的例子(P(Z), ), (Interval, ), (Range, ), (P(Sign), )伽罗瓦连接的定义伽罗瓦连接的定义抽象函数和具体函数抽象函数和具体函数它们以及它们的复合要满足的性质它们以及它们的复合要满足的性质1、一种表示方式称为伽罗瓦连接、一种表示方式称为伽罗瓦连接2、另一种表示方式称为、另一种表示方式称为adj
9、unction第第4章章 抽象解释抽象解释4.3 节节伽罗瓦连接和伽罗瓦插入是表达程序的属伽罗瓦连接和伽罗瓦插入是表达程序的属性空间性空间L和属性空间和属性空间M之间联系的一种工具之间联系的一种工具伽罗瓦连接的定义伽罗瓦连接的定义抽象函数抽象函数 和具体函数和具体函数 它们以及它们的复合要满足的性质它们以及它们的复合要满足的性质1、一种表示方式称为伽罗瓦连接、一种表示方式称为伽罗瓦连接2、另一种表示方式称为、另一种表示方式称为adjunction用表示函数用表示函数 来定义来定义伽罗瓦连接伽罗瓦连接用抽取函数用抽取函数 来定义伽罗瓦连接来定义伽罗瓦连接第第4章章 抽象解释抽象解释4.3 节节A
10、dditive function f(l1 1 l2) = f(l1) 2 f(l2)Multiplicative function f(l1 1 l2) = f(l1) 2 f(l2)Complete additive f(1Y ) = 2 f(l ) | l Y Complete multiplicative f(1Y ) = 2 f(l ) | l Y 第第4章章 抽象解释抽象解释4.3 节节伽罗瓦连接和伽罗瓦插入是表达程序的属伽罗瓦连接和伽罗瓦插入是表达程序的属性空间性空间L和属性空间和属性空间M之间联系的一种工具之间联系的一种工具伽罗瓦连接的性质伽罗瓦连接的性质这些性质用来证明了，采
11、用了这些性质用来证明了，采用了(P(Sign), )，则不，则不用用(Interval, )的原因（改用的原因（改用(Range, )）伽罗瓦连接是正确的概念伽罗瓦连接是正确的概念V和和L间可接受正确性关系间可接受正确性关系 + L和和M间伽罗瓦连接间伽罗瓦连接 V和和M间可接受正确性关系间可接受正确性关系第第4章章 抽象解释抽象解释4.3 节节伽罗瓦连接和伽罗瓦插入是表达程序的属伽罗瓦连接和伽罗瓦插入是表达程序的属性空间性空间L和属性空间和属性空间M之间联系的一种工具之间联系的一种工具伽罗瓦插入伽罗瓦插入因为因为M比比L粗略，因此粗略，因此L的若干个元素很可能都由的若干个元素很可能都由M的某
12、个元素描述，且的某个元素描述，且M不应该有多余的元素不应该有多余的元素这样的伽罗瓦连接称为伽罗瓦插入这样的伽罗瓦连接称为伽罗瓦插入伽罗瓦插入的性质（新增性质）伽罗瓦插入的性质（新增性质）具体函数具体函数 一定是内射的一定是内射的抽象函数抽象函数 一定是满射的一定是满射的第第4章章 抽象解释抽象解释4.3 节节伽罗瓦连接和伽罗瓦插入是表达程序的属伽罗瓦连接和伽罗瓦插入是表达程序的属性空间性空间L和属性空间和属性空间M之间联系的一种工具之间联系的一种工具压缩算子压缩算子用来从伽罗瓦连接构造伽罗瓦插入用来从伽罗瓦连接构造伽罗瓦插入将伽罗瓦连接的具体函数将伽罗瓦连接的具体函数 改造为内射函数改造为内射
13、函数可以用规范伽罗瓦连接的抽取函数可以用规范伽罗瓦连接的抽取函数 来定义压缩来定义压缩算子算子第第4章章 抽象解释抽象解释4.4 节节伽罗瓦连接可按一种系统的方式来构造，从使用伽罗瓦连接可按一种系统的方式来构造，从使用较简单属性的程序分析得到使用复杂属性的分析较简单属性的程序分析得到使用复杂属性的分析函数复合（顺序复合）函数复合（顺序复合）两个伽罗瓦连接的复合仍然是一个伽罗瓦连接两个伽罗瓦连接的复合仍然是一个伽罗瓦连接属性二元组属性二元组独立属性方法独立属性方法：P(L1) P(L2) 相关属性方法：相关属性方法： P(L1 L2) 独立属性方法会丢失精度独立属性方法会丢失精度第第4章章 抽象
14、解释抽象解释4.4 节节伽罗瓦连接可按一种系统的方式来构造，从使用伽罗瓦连接可按一种系统的方式来构造，从使用较简单属性的程序分析得到使用复杂属性的分析较简单属性的程序分析得到使用复杂属性的分析函数空间函数空间全函数空间全函数空间单调函数空间单调函数空间同时完成不同性质的分析同时完成不同性质的分析直积（独立属性方法）直积（独立属性方法）直接张量积（使用相关属性方法）直接张量积（使用相关属性方法）第第4章章 抽象解释抽象解释4.4 节节伽罗瓦连接可按一种系统的方式来构造，从使用伽罗瓦连接可按一种系统的方式来构造，从使用较简单属性的程序分析得到使用复杂属性的分析较简单属性的程序分析得到使用复杂属性的
15、分析将直积压缩将直积压缩被压缩的直积（成为伽罗瓦插入）被压缩的直积（成为伽罗瓦插入）被压缩的直接张量积（成为伽罗瓦插入）被压缩的直接张量积（成为伽罗瓦插入）第第4章章 抽象解释抽象解释4.5 节节试图用在时间、空间或终止性行为上更好的试图用在时间、空间或终止性行为上更好的近似计算来取代一种计算时，伽罗瓦连接是近似计算来取代一种计算时，伽罗瓦连接是有用的有用的使用使用M的分析被用来取代使用的分析被用来取代使用L的分析的分析M的使用是为获得的使用是为获得L中最小不动点计算的较好近中最小不动点计算的较好近似似导出运算导出运算沿抽象函数沿抽象函数的的诱导诱导沿具体函数的诱导沿具体函数的诱导第第4章章
16、抽象解释抽象解释4.5 节节试图用在时间、空间或终止性行为上更好的试图用在时间、空间或终止性行为上更好的近似计算来取代一种计算时，伽罗瓦连接是近似计算来取代一种计算时，伽罗瓦连接是有用的有用的沿抽象函数的诱导沿抽象函数的诱导从一个分析函数和两个伽罗瓦连接诱导出来从一个分析函数和两个伽罗瓦连接诱导出来导出分析中的不动点：从导出分析中的不动点：从M上不动点的计算来得上不动点的计算来得到到L上不动点的一个近似上不动点的一个近似第第4章章 抽象解释抽象解释4.5 节节试图用在时间、空间或终止性行为上更好的试图用在时间、空间或终止性行为上更好的近似计算来取代一种计算时，伽罗瓦连接是近似计算来取代一种计算
17、时，伽罗瓦连接是有用的有用的在数据流分析中的应用在数据流分析中的应用单调框架的推广（不要求满足上升链条件、不要单调框架的推广（不要求满足上升链条件、不要求迁移函数空间是由所有单调函数构成的空间）求迁移函数空间是由所有单调函数构成的空间）实例实例A和和B：它们迁移函数之间的区别和联系：它们迁移函数之间的区别和联系它们解之间的联系它们解之间的联系例子：状态集合分析和常量传播分析之间的联系例子：状态集合分析和常量传播分析之间的联系第第4章章 抽象解释抽象解释4.5 节节试图用在时间、空间或终止性行为上更好的试图用在时间、空间或终止性行为上更好的近似计算来取代一种计算时，伽罗瓦连接是近似计算来取代一种计算时，伽罗瓦连接是有用的有用的沿具体函数的诱导沿具体函数的诱导用另一种方式来获得最小不动点的近似用另一种方式来获得最小不动点的近似
