程序分析理论

今天这篇文章主要就是介绍,具体的语法并没有特别的写出,关于约束条件也没有提及,主要通过例子简单介绍这些方法是做什么的。算法部分也就是简单逻辑和伪代码。
本篇是程序分析理论第十一篇:基于类型和响应的系统模型Type and Effect Systems。
程序分析理论第十篇抽象解释,从理论角度寻找分析程序的通用方法并找到数学依据使之可行。
程序分析理论第九篇,关于上下文敏感的引入数据的控制流分析以及控制流分析的算法:笛卡尔积算法。
本篇文章是程序分析理论部分第八篇,关于以语义为导向和基于约束的控制流分析,不仅仅有分析语义,还有部分理论证明以及最后的伪代码说明。
本文主要依据NFAs with Tagged Transitions这篇论文以及re2c自身代码进行描述。
这一篇文章是程序分析理论的理论部分的第七篇,是控制流分析部分的数学表示合理性的理论证明。
不知道大家还记不记得popmaster这道题。当初出题人用了php parser实现抽象代码树从而达到程序分析目的。之前我们只讲到数据流分析所以我使用了过程间分析的原理和函数递归的思想实现程序分析。
读完本文只需要记得phpparser基于zend’s lexical scanner,zend’s lexical scanner基于re2c。下一次我们会分析一下re2c看看究竟抽象化是怎么通过代码实现的。
这一篇文章讲的是控制流分析的抽象化和数学表示。