简介
资料来源及食用方法@2022
简介
Getting started with static program analysis. Read this and start writing your first static program analyzer! We focus on the problem:
❓ How to automatically and efficiently guarantee software quality
静态程序分析入门。阅读此书并着手编写你的第一个静态程序分析器吧!本仓库关注一个非常重要的问题:
❓ 如何自动化地高效保障软件质量
离线阅读方式
将本仓库下载到本地(安装Git后,在命令行中执行命令
git clone https://github.com/RangerNJU/Static-Program-Analysis-Book.git
)周期性地更新,在仓库目录下执行
git pull
使用Typora等本地Markdown阅读器阅读
作业, 克隆仓库时, 推荐递归克隆子项目homework
git clone --recursive {git仓库}
表达你的声音 👂
批评的意见很有价值。 这是我第一次书写教程,一定有很多做得不好的地方。如果你觉得有值得修改或值得讨论的地方(包括但不仅限于行文风格,内容准确性,图例与解释的易读性等等),可以选择:
提issue
通过邮箱联系我(ranger.nju#gmail.com)
如果你觉得我写得不错,可以到GitHub仓库中给我一个Star,也可以在自己的社交圈子中宣传,让更多的人了解这个项目。
更新记录与里程碑事件
Oct, 2020. 设立Repo,一个月内解锁Star、Fork和PR。
Nov. 将IR与Data Flow Analysis的相关内容暂时移出仓库,更新七至十课——Interprocedural Analysis、Pointer Analysis-Introduction and Foundations。
Dec. 更新十一和十二两课——Context Sensitive Pointer Analysis,指针分析大结局。🥳 更新十三十四课介绍指针分析的安全应用Taint Analysis和使用Datalog实现声明式指针分析算法。 更新十五十六课介绍IFDS分析框架和Soundiness。
APR, 2021. 由Lancern开始英文翻译。
Sept. 新学期开始补充前八课的笔记版本。
Apr, 2022. 南京大学《软件分析》实验作业平台 “太阿” 正式发布。
Jul, 2022. “太阿”(科研版)静态程序分析框架正式发布。
图文的主体部分更新完毕,撒花~!
后续会考虑录制一些视频补充对动态例子的讲解。
这一《静态程序分析》教程对谁有用?
学生,开发者,研究者……几乎所有当代生活者都能从中受益。
学习方向与程序有关的学生。
计算机方向的学生可以通过深入学习这一领域知识而为自己建立独特的学术和就业优势,也能加深对编程的理解以降低自己写出bug的频率。
其他方向的学生既然已经开始阅读这一页面,想必对计算机方向的内容有一定兴趣。你可以通过了解这一技术,了解静态分析软件(包括其内置于编译器,集成开发环境的部分)能够为你提供怎样的功能和便利,以及如何更好地使用这些软件,以此保证你所关心的程序质量。
工作内容与程序有关的开发者。
无论你希望更好地理解Wiki上众多的开源或是闭源的静态程序分析技术,还是希望自己开发一个适用于眼下工作内容的静态程序分析器以保证程序质量,了解静态程序分析都会有所帮助。
研究领域与程序相关的研究者。 或许你希望微调研究方向,却因没有合适的入门材料而苦恼;或许你希望了解计算机领域的相关知识以期获得启发……这一教程可以作为你的入门材料或是闲暇读物。
生活与程序相关的每个人
软件质量是信息化时代的重要议题之一,在这个时代生活与工作,你一定会遇到相关的问题。
在大多数学校和企业中,没有开设该领域的课程。
什么是静态程序分析?
静态程序分析在计算机科学领域中的定位
静态程序分析是编程语言中应用层面下的一个细分领域,它是一个非常重要的核心内容。
在理论部分,考虑的是如何设计一个语言的语法和语义,如何设计语言的类型系统等等问题;有了语言的语法、语义和类型系统之后,我们需要支撑语言的运行。因此,在环境部分,需要考虑如何为运行中的程序提供运行时环境——如何设计编译器,在运行时需要怎样的支持(如内存的分配管理)等等;应用部分则关注如何保证语言所写出程序的效率、安全性和可靠性,主要考虑如何对程序进行分析,验证和合成(如何自动合成一个程序)。
编程语言的分类
当今的计算机世界,面对这样一条恶龙: 👇
数十年来语言的核心没有变化,但软件的规模和复杂性增长迅速,如何保证程序的可靠性?
尽管新的语言和特性层出不穷,但现在编程语言无非三大类 (如果你对其中的某个语言不熟悉,可以到语言的官网或英文Wiki页面查看相关示例,也可以利用搜索引擎做初步的了解。本教程内容主要关注于针对命令式语言JAVA的分析。) :
命令式(C、C++、JAVA)
逻辑式(Prolog)
静态程序分析的应用
静态程序分析即是屠龙的宝刀之一,举例来说这一技术可以处理以下问题(以下概念只需要了解,重要的应用在后文中会详细讲解。):
提高程序可靠性
Null pointer dereference, memory leak, etc.
空指针引用与内存泄漏等:几乎每个程序编写者都被这两个问题所困扰过
为编译优化提供基础技术
Dead code elimination, code motion, etc.
死代码消除:在编译器的机器无关优化环节,将不会对程序执行结果产生影响的代码(即死代码)删除。
循环不变量的代码移动:在编译器的机器无关优化环节,在保证不影响程序执行结果的情况下,将循环中的特定语句移动到循环外,使得程序运行时执行的语句数减少。更为详细的解释可以参考StackOverFlow上的回答。
有助于程序理解
IDE call hierarchy, type indication, etc.
为集成开发环境的功能提供帮助:当你使用VS/Idea/Clion/Eclipse/Android Studio等等IDE时,将鼠标悬停在代码上,IDE能够动态地分析并提示你所悬停对象的相关信息,背后使用的技术就是静态程序分析。
此外,静态程序分析技术也可以分析多线程程序,这是一个有难度的研究领域。主要困难在于处理多线程间的interleaving。本书定位入门,不会涉及相关内容。
静态程序分析的市场
在学术界,静态程序分析技术几乎可以应用于所有关于程序的研究方向。
在工业界,国外的Google,IBM等大企业已经初步建立了自己的静态程序分析团队。国内的华为和阿里等企业也正在积极寻找静态程序分析方面的人才。
无论你将来想在学术界还是工业界深入发展,学习这一领域的知识都能为你建立独特的优势。
静态程序分析与类似技术的对比
Testing shows the presence, not the absence of bugs. --Edsger W. Dijkstra
动态的软件测试和形式化语义的验证的作用与静态程序分析类似,这一部分对这三个细分方向做简单的对比。
静态程序分析
优点:在选定的精度下能够保证没有bug。这在教程中会详细介绍。
缺点:
学术门槛相对高。目前已知国内高校公开的课程资料只有北京大学,南京大学,国防科大,吉林大学的,且通俗易懂的教材稀少(详细课程及教材链接见本文末尾)。作为一门计算机专业的高年级选修课,入门和提高都较困难。
You tell me.
动态软件测试
优点:在工程中被广泛应用,并且有效。实现简单,便于自动化。
缺点:
无法保证没有bug。 这是无法遍历所有可能的程序输入的必然结果。
在当今的由多核与网络应用带来的并发环境下作用有限。 某个bug可能只在特定情况下发生,因而难以稳定地复现。如果你对并发程序的动态测试细节感兴趣,可以参考《拧龙头法测试并发程序》。(截图来自南京大学《形式化语义》课程资料)
形式化语义验证
优点:由于用数学的方法对程序做了抽象,能够保证没有bug。
缺点:
学术门槛较高,学习者必须有良好的数学基础才能入门。
验证代价较高,一般来说非常重要的项目会使用这一方式保证程序质量。甚至在操作系统这样重要的软件中,也并不一定会使用。(截图来自鸿蒙OS直播发布会)
加入项目/How to contribute
觉得有所帮助的话可以点个star支持哦。
欢迎希望添加更好的讲解资料或对教程内容进行扩充的小伙伴 fork, modify, PR
三连。
提醒:引用图片时请使用相对路径。
本地化/Localization
We'd love help translating this book! Open a new issue to start working on a new language. Feel free to start :)
其他相关项目
软件质量保障相关
前辈们写过的优秀笔记
进一步学习的资料
课程视频和阅读资料
北大熊英飞老师的《软件分析技术》课程视频公开在了这里。
CMU Jonathan Aldrich老师的《17-355/17-665/17-819 Program Analysis》(2019 Spring)。
Anders Møller and Michael I. Schwartzbach的《Static Program analysis》 以及配套的 《Lecture Notes on Static Analysis》, 视频 (推荐开启cc英文字幕)
Principles of Program Analysis
中文版本:《程序分析原理》
张健, 张超, 玄跻峰, 熊英飞, 王千祥, 梁彬, 李炼, 窦文生, 陈振邦, 陈立前, 蔡彦. 程序分析研究进展. 软件学报, 2019, 30(1): 80-109.http://www.jos.org.cn/1000-9825/5651.htm
国防科技大学陈立前老师的《高可信软件技术-程序分析部分》
吉林大学刘磊老师的《程序分析技术》24集视频(超星/尔雅学术视频,需要账号登录搜索,B站上视频不全),书籍 。算是国内最早的公开视频以及专门的教材了
东南大学李必信老师的《程序切片技术及其应用》
北京邮电大学的《源代码分析》
开源软件
最后更新于