使用抽象解释对带有本地C库的Python程序进行静态类型和值分析

0HAL编号：tel-035330300https://theses.hal.science/tel-035330300提交日期：2022年1月18日0HAL是一个多学科开放存取档案，用于存储和传播科学研究文档，无论它们是否已发表。这些文档可以来自法国或国外的教育和研究机构，或来自公共或私营研究中心。0HAL（开放式多学科开放存取档案）是一个用于存储和传播研究级科学文献的多学科开放存取档案，这些文献可以是已发表或未发表的，来自法国或国外的教育和研究机构，或来自公共或私营研究中心。0使用抽象解释对带有本地C库的Python程序进行静态类型和值分析0Raphaël Monat0引用此版本：0Raphaël Monat. 使用抽象解释对带有本地C库的Python程序进行静态类型和值分析。编程语言[cs.PL].巴黎索邦大学, 2021. 英语. �NNT : 2021SORUS263�. �tel-03533030�0巴黎索邦大学博士学位论文0专业0计算机科学0计算机科学、通信和电子学学院（巴黎）0RaphaëlMonat提交0为了获得0巴黎索邦大学博士学位0论文题目：0使用抽象解释对带有本地C库的Python程序进行静态类型和值分析02021年11月22日在评审委员会面前进行的论文答辩，评审委员会成员如下：0Antoine Miné 索邦大学和法国国家科学研究中心，法国，论文导师 Isabella Mastroeni威尼斯大学，意大利，评阅人 Anders Møller 奥胡斯大学，丹麦，评阅人 EmmanuelChailloux 索邦大学和法国国家科学研究中心，法国，评审委员会主席 Francesco LogozzoFacebook西雅图，美国，考官 Peter Müller 苏黎世联邦理工学院，瑞士，考官 Alan SchmittINRIA雷恩，法国，考官0摘要0在本论文中，我们旨在从理论和实验的角度设计方法，自动检测软件中潜在的错误或证明其不存在。这种检测是通过静态分析程序的源代码而不运行它们来完成的。我们依赖于抽象解释框架来推导出可靠的、可计算的语义。特别是，我们专注于分析动态编程语言。本工作的目标是分析Python程序与本地C库的结合。0抽象解释工作流程需要一个具体的语义，该语义将被近似以创建可计算的分析。因此，我们的第一步是正式定义Python的不可计算的收集语义。这个语义依赖于之前的工作，并通过对参考解释器的源代码进行逆向工程来实现。我们特别注意使语义可解释，为语义的每个情况提供对实际实现源代码的引用。0我们已经在Mopsa框架中实现了本论文中提出的所有分析。从静态分析开发者的角度来看，Mopsa有两个目标。它旨在降低将抽象域从玩具语言提升到实际语言的成本。它还希望定义由松散耦合的抽象域组成的关系分析，这些抽象域可以相互合作。我们特别注意将所有抽象域独立定义。Mopsa的核心是与语言无关的，使其适用于分析不同的编程语言。这些分析依赖于一些通用的使用域，如数值域、动态内存分配的最新性抽象和循环迭代器。0我们首次提出了一种旨在检测Python程序中类型相关错误的分析方法。它通过推断对象的名义类型和结构类型来实现。Python的类型注解可以被重用以支持库。这种分析被细化为一种更精确的值分析，它推断出被操作的内置数值的数值不变量。这些分析依赖于我们已经适应动态编程语言情况的动态内存分配和数据结构的抽象。这两种分析都可以应用于Python开发人员使用的几千行长的真实世界基准测试。0大多数Python程序依赖于用C编写的库，以提高性能或代码重用。我们定义了一种多语言分析方法，可以检测多语言程序的每个部分中的运行时错误：Python部分、C部分以及语言之间的边界。在定义这种分析之前，我们概述了Python和C之间可用的不同互操作性机制，并为参考解释器提供的互操作性机制定义了一种收集语义。这种分析可以在几分钟内处理几千行C和Python的流行实际库的测试。0简历0在这篇论文中，我们的目标是在理论和实验上设计出一种方法，以自动检测软件中潜在的错误或证明其不存在。这些方法是静态的：它们分析程序的源代码而不执行它们。我们的工作是基于抽象解释的框架，以推导出一种安全和可决定的语义。这项工作的主要对象是动态编程语言的分析。特别是，这项工作集中在使用Python编写的程序上，这些程序可以调用用C编写的库。按照抽象解释的常规流程，我们从具体语义开始，然后对其进行逼近，以创建安全且可计算的分析。因此，我们的第一步是正式定义Python的收集语义，而不是可计算的语义。这种语义基于先前的工作，并通过对参考解释器的源代码进行逆向工程来实现。我们在每种情况下都仔细说明了语义，并在解释器中提供了相应的源代码引用。我们在名为Mopsa的软件中实现了本论文中介绍的所有分析。从静态分析的实现角度来看，Mopsa有两个目标。首先，它旨在降低从在玩具语言上运行的抽象域到实际编程语言的成本。其次，它旨在定义由弱耦合的抽象域组成的关系分析，这些域可以相互协作。我们特别注意独立定义所有抽象域。Mopsa的核心并不专门用于分析特定的编程语言，这使得Mopsa能够分析不同的编程语言。这些分析依赖于一些通用域，例如数字域和循环迭代器。我们提出了一种旨在检测Python程序中与类型相关的错误的初始分析。它通过推断对象的名义类型和结构类型来实现。Python的类型注释可以用于支持库。这个分析被细化为一个更精确的值分析，它推断出数值不变式。这两种分析都基于我们针对动态编程语言的动态内存分配机制和数据结构的抽象。我们的分析适用于Python开发人员使用的一些实际基准测试，这些测试包含几千行代码。大多数Python程序依赖于用C编写的库，以提高性能或重用现有代码。我们定义了一种多语言分析方法，可以检测多语言程序的每个部分中的运行时错误：Python部分、C部分以及语言之间的边界。在定义这种多语言分析之前，我们概述了Python和C之间可用的不同互操作性机制，并为参考解释器提供的互操作性机制定义了一种收集语义。我们的多语言分析能够在几分钟内分析几千行C和Python的流行实际库的测试。0致谢和感谢0我非常感谢Isabella Mastroeni和AndersMøller在繁忙的九月和十月同意审查这篇论文。我要感谢Emmanuel Chailloux，FrancescoLogozzo，Peter Müller和Alan Schmitt同意参加答辩委员会。0感谢Antoine进行非常丰富的讨论和宝贵的建议。感谢你不知疲倦地审阅，从细节到修正，再到改进建议和未来工作的想法。仅仅为了手稿，各个草稿上的注释总共有大约800个。感谢Abdelraouf：没有你和Mopsa，这个论文将花费更多的时间，多语言分析也不会那么容易！我仍然记得在论文初期度过的下午，为了理解Python分析的工作原理而绘制序列图。我在第11.6、11.7和11.8图中保留了这种方法来说明多语言分析。感谢你们两个始终对我的善意，尽管你们的时间表很忙，但总是能找到时间交流，并围绕Mopsa进行所有引人入胜的讨论。0感谢Alan和Pierre-Évariste在跟踪委员会期间给予的宝贵建议。0感谢Daniel Hirschkoff，Simon Castellan和Jean-MarieMadiot让我陷入了L3编程语言的魔法药水，并让我发现了程序分析的基础知识等等。0感谢Antoine的前任博士生：Caterina，Thibault，Ghiles和Matthieu，感谢你们有趣的讨论，宝贵的建议和提供的模型。祝David，Guillaume和Francesco好运。0APR是一个既友好又激励人心的环境，非常感谢303办公室（或类似的）一起走过的路程：Alice，Vincent，Marwan，Boubacar，Clément，Steven，Yi-Ting，Martin，Jules，Mehdi，Mat（t）hieu，Keanu和Pierre。感谢Romain（Demangeon）进行的所有即兴讨论，这些讨论使我们能够换换空气，并让我开始教学。还要感谢Maryse，Mathieu，Pascal，Frédéric，Tong，Emmanuel，Antoine（Genitrini），Philippe和Tali一起进行的教学。0Denis，感谢你在击剑课上提出让我帮助你进行税务逆向工程的建议。我很高兴我们能够将其发展成为一项真正的研究和向DGFiP的转移项目。这使我坚定了对形式方法“实践”方面的立场，并且对于能够追踪自己的思路感到兴趣。感谢Jonathan在撰写CC文章时提供的宝贵帮助。感谢DGFiP的工作人员的接待和耐心。0感谢Romain（Dubessy）教我如何管理击剑队。这让我在面对讨论小组时更容易发言。感谢Alex和Jean-Pierre为ECE的组织。感谢Mathilde在2019年对初学者小组的教学以及今年的接棒。感谢俱乐部的常客们度过的这些年：Adrien，Arthur，Charles，Denis（再次），Irène，José，Kim，Léo，Marion，Mathilde，Philippine，Soazic，Théo，Yoko，Vincent，...我很高兴在比赛中遇到来自欧洲各地的击剑运动员，并与来自阿姆斯特丹，迈因茨和理工大学的朋友交朋友。感谢Guillaume在大学里的击剑课程，无论起点水平如何，都能以愉快的心情改变思维方式并取得进步。也要感谢Maria（Mihaescu）和Lucas多年来提供的对抗。0感谢Maria（Boritchev），Titouan，Isao，Etienne，Victor，Arthur，Amandine，Simon和Jean-Yves一起在里昂度过的这些年。Maria，在另一个生活中，我们会尽量减少我们的答辩重复！0Loïc，Carole，我很高兴在预科时认识你们，并在我们的时间表相吻合时见到你们。感谢Fanny，Louise，Marc，Sylvain和Victor一起度过的所有时刻。0感谢我的父母和姐妹们一直以来的支持。没有你们，我永远无法走到这一步。0Laura，谢谢你的一切。0目录0摘要 i0摘要 iii0致谢和感谢 v0I 背景 101 引言 3 1.1 软件错误及其解决方法 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.1.1第一种方法：测试 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.1.2 一个不可能的定理 . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . 4 1.1.3 推理程序验证 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.1.4符号执行 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.1.5 模型检查 . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . 5 1.1.6 抽象解释的静态分析 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.2分析动态编程语言的挑战 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.3 贡献和大纲 . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . 602 抽象解释的静态分析 9 2.1 一个玩具命令式语言,  Imp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2  Imp的语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2.1 表达式的语义 . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . 11 2.2.2 语句的语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.2.3状态的比较 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.3 推断  Imp  变量的范围 . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . 16 2.3.1 区间域 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.3.2具体化 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.3.3 区间传递函数 . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . 18 2.3.4 表达式的抽象语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.3.5语句的抽象语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.3.6 基本语句 . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . 20 2.3.7 条件语句 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 2.3.8终止循环分析 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 2.3.9 通过同余改进分析 . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . 25 2.3.9.1 推导语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.3.9.2同余和区间的合作 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 2.4 扩展  Imp  及其分析 . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . 28 2.4.1 使用字符串扩展  Imp  . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2.4.2使用幽灵变量跟踪字符串长度 . . . . . . . . . . . . . . . . . . . . . . . . . . 290viii 目录02.4.3 退出循环 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2.4.4 关系不变式 . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . 33 2.4.5 字符串内容的总结 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 2.4.6结合字符串长度和总结 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 2.5 定义模块化具体化函数 . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . 39 2.5.1 通用方法 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 392.5.2 字符串总结域 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 2.5.3 字符串长度域 . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . 41 2.5.4 结合两种具体化 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 422.6 结论 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 430II 基本抽象 4503 Mopsa 47 3.1 相关工作 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 3.1.1 Infer . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48 3.1.2 TAJS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . 49 3.1.3 Frama-C . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 3.1.4 Astrée . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 3.1.5 Keidel等人的框架 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . 50 3.2 抽象语法树（AST） . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 3.2.1基本表达式和语句 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51 3.2.2 处理while循环的域 . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . 53 3.2.3 用Python和C循环扩展AST . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 543.2.4 动态重写Python和C循环 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 3.3 域 . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . 56 3.3.1 通过组合域来定义分析 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 563.3.2 域签名 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 3.3.2.1域类型和格操作（第24-33行） . . . . . . . . . . . . . . . . . . . . . 58 3.3.2.2 管理器的需求（第2-15行） . . . . . .. . . . . . . . . . . . . . . . . 58 3.3.2.3 流，全局抽象状态的包装器（第18-19行） . . . . . . . . . . . . . 58 3.3.2.4案例，后置条件和评估（第36-38行） . . . . . . . . . . . . . . . . 60 3.3.2.5表达式和语句的转换函数（第41-44行） . . . . . . . . . . . . . . 60 3.3.2.6 实用工具（第41-44行） . . . . . . . .. . . . . . . . . . . . . . . . . . 63 3.3.3 非关系域的简化情况 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 3.3.4简化乘积及其陷阱 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 63 3.3.5 域之间的通信 . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . 66 3.4 钩子 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 3.5 形式化. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 3.6 结论 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . 7004 抽象动态内存分配 73 4.1 最近使用抽象 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 4.1.1动机 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 4.1.2 具体语义 . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . 74 4.1.3 最近使用抽象 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 75 4.1.4抽象语义 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 77 4.1.5 具体化 . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . 79 4.1.5.1 最近使用抽象 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 4.1.5.2堆抽象 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 4.2 最近使用抽象的变量策略 . . . . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . 80III Pure Python Programs996Concrete Semantics of Python1016.1Concrete state . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1036.2Core language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1076.2.1Literals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1076.2.2Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1076.2.3Nominal types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1086.2.4Structural types (attributes) . . . . . . . . . . . . . . . . . . . . . . . . . . . .1106.2.5Subscript . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1116.2.6Conditionals . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1136.2.7Loops . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1136.2.8Exceptions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1156.2.9With context manager . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1166.2.10Function declaration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1186.2.11Class declaration . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1196.2.12Decorators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1196.2.13Calls . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1206.2.14Unary operators. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1206.2.15Binary operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1206.2.15.1Arithmetic operators . . . . . . . . . . . . . . . . . . . . . . . . . . .1216.2.15.2Comparison operators . . . . . . . . . . . . . . . . . . . . . . . . . .1236.2.16Other binary operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1236.3Builtin objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1256.3.1Object . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1256.3.2Functions and methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1276.3.3Type . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1306.3.4Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1326.3.5Integers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1326.3.6Range objects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1326.3.7Containers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1336.3.8Iterators. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1346.3.9super . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1346.3.10Generators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1370目录 ix04.3 抽象垃圾回收（AGC） . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 4.4 相关工作 . . . . . . . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 4.5 结论 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . 8405 抽象容器 85 5.1 动态数组 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 5.1.1 数组操作 . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 5.1.2 长度抽象 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . 87 5.1.3 汇总抽象 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 89 5.1.4 简化乘积 . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 5.1.5 变体：抽象集合 . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . . . 92 5.2 字典 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 5.2.1 字典操作 . . . . .. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 93 5.2.2 整体破坏 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .. . . . . . . 95 5.3 相关工作 . . . . . . . . . . . . . . . . . . . . . . . . . . .