0HAL Id: tel-016815550https://theses.hal.science/tel-01681555v202018年1月12日提交0HAL是一个多学科开放存取档案，用于存储和传播科学研究文件，无论其是否发表。这些文件可能来自法国或国外的教学和研究机构，也可能来自公共或私人研究中心。0HAL跨学科开放存取档案旨在存储和传播法国或国外教育和研究机构、公共或私人实验室发表或未发表的研究文档。0使用可满足性模理论和凸优化找到归纳不变式0Egor George Karpenkov0引用此版本：0Egor George Karpenkov. Finding inductive invariants using satisfiability modulo theories and convexoptimization. Performance [cs.PF]. Université Grenoble Alpes, 2017. English. �NNT : 2017GREAM015�.�tel-01681555v2�0博士论文0获得学位0格勒诺布尔阿尔卑斯大学博士学位0专业：计算机科学02017年3月30日0由George EgorKarpenkov呈现0由David Monniaux博士指导的博士论文0在Verimag实验室和MSTII博士学院内准备0使用可满足性模理论和凸优化找到归纳不变式0论文于2017年3月29日公开支持，评审委员会成员有：0Sylvie Putot教授，École Polytechnique，评审 Pierre-LoïcGaroche博士，Onera，评审 DirkBeyer教授，慕尼黑大学路德维希∙马克西米利安，考官 NikolajBjørner首席研究员，微软研究，考官 Lydie duBousquet教授，格勒诺布尔阿尔卑斯大学，主席 HelmutSeidl教授，慕尼黑工业大学，考官 DavidMonniaux研究主任，法国国家科学研究中心，导师230致谢0在我完成这篇论文的过程中，我很幸运地得到了许多出色人士的帮助和建议。没有他们，这项工作将永远无法完成。对于详细和细致的校对（多次！）和提供许多有用评论，我要感谢GrigoryFedyukovich和Alexey Bakhirkin。本论文的工程贡献受益于PhilippWendler的指导，他在软件系统架构上提供了大量宝贵的建议。由于DirkBeyer的帮助，这种合作得以实现，他友好地让我在他的研究小组待了三个月。此外，我要感谢TimKing和ArieGur�nkel，感谢他们的时间和许多富有见地的对话，解释了科学探究的本质。关于使用策略迭代生成摘要的章节中的材料受到了与PeterSchrammel的富有成效的讨论的影响。此外，我要感谢我的导师DavidMonniaux，进行了许多富有成效的合作。最后，我非常感谢Kate和Andreas在这些年里给予我的爱、支持和耐心，没有他们，我将无法做到。谢谢！4Static analysis concerns itself with deriving program properties which hold universally for allprogram executions. Such properties are used for proving program properties (e.g. there neveroccurs an overflow or other runtime error regardless of a particular execution) and are almostinvariably established using inductive invariants: properties which hold for the initial state andimply themselves under the program transition, and thus hold universally due to induction.A traditional approach for finding numerical invariants is using abstract interpretation,which can be seen as interpreting the program in the abstract domain of choice, only trackingproperties of interest. Yet even in the intervals abstract domain (upper and lower bounds foreach variable) such computation does not necessarily converge, and the analysis has to resort tothe use of widenings to enforce convergence at the cost of precision.An alternative game-theoretic approach called policy iteration, guarantees to find the leastinductive invariant in the chosen abstract domain under the finite number of iterations. Yet theoriginal description of the algorithm includes a number of drawbacks: it requires converting theentire program to an equation system, does not easily integrate with other approaches, anddoes not directly benefit from known results for Kleene iteration (e.g. iteration order).Our new algorithm for running local policy iteration (LPI) instead formulates policy iterationas traditional Kleene iteration, with a widening operator that guarantees to return the leastinductive invariant in the domain after finitely many applications. Local policy iteration runs intemplate linear constraint domains which requires setting in advance the “shape” of the derivedinvariant (e.g. x + 2y for deriving x + 2y ≤ 10). Our second theoretical contribution involvesdevelopment and comparison of a number of different template synthesis strategies, and theirevaluation when used with LPI. Additionally, we present an approach for generating abstractreachability trees using abstract interpretation, enabling the construction of counterexampletraces, which in turns lets us to generate new templates using Craig interpolants.In our third contribution we bring our attention to interprocedural and potentially recursiveprograms. We develop an algorithm parameterizable with any abstract interpretation forsummary generation, and we study it’s parameterization with LPI. The resulting approach isable to generate least inductive invariants in the domain for a fixed number of summaries forrecursive programs.Our final theoretical contribution is a “formula slicing” method for finding potentiallydisjunctive inductive invariants from program fragments obtained by symbolic execution.We implement all of these techniques in the open-source state-of-the-art CPAcheckerprogram analysis framework, enabling collaboration between different analyses.The techniques mentioned above rely on satisfiability modulo theories solvers, which arecapable of giving solutions to first-order formulas over certain theories or showing that noneexists. In order to simplify communication with such tools we present the JavaSMT library,which provides a generic interface for such communication. The library has shown itself to be avaluable tool, and is already used by many researchers.50670摘要0对程序的正确静态分析是获得程序每次执行的真实属性。这些属性对于证明软件的一些重要特征是有用的，比如无溢出或其他运行时错误，无论程序的输入是什么。它们几乎总是通过归纳不变式来建立的：这些不变式是初始状态的真实属性，并且如果它们在计算的一个步骤中是真实的，那么它们在计算的下一个步骤中仍然是真实的，因此通过归纳总是真实的。抽象解释是寻找数值不变式的一种传统方法，可以将其表达为所选抽象域中程序的非标准解释，并且只考虑某些有趣的属性。即使在如区间（每个变量的下界和上界）这样简单的领域中，这种计算也不一定收敛，分析必须使用扩展算子来迫使收敛以牺牲精度。另一种方法，称为政策迭代，受博弈论启发，保证在有限次迭代后在所选抽象域中找到最强的归纳不变式。然而，该算法的原始描述存在一些弱点：它基于将程序完全转换为一个方程系统，而不与其他分析方法整合或协同。我们的新算法是政策迭代的一种局部形式，它将其放回Kleene迭代，但使用特殊的扩展算子，保证在有限次应用后在抽象域中获得最小的归纳不变式。局部政策迭代在由模式给定的线性约束域中运行，这要求预先确定不变式的“形式”（例如 x + 2y 以获得 x + 2y ≤10）。我们的第二个理论贡献是开发和比较多种模式综合策略，与局部政策迭代一起使用。此外，我们提出了一种通过抽象解释生成抽象可达树的方法，允许生成反例轨迹，然后从Craig插值中生成新的模式。我们的第三个贡献涉及程序的跨过程分析，可能是递归的。我们提出了一种为每个过程生成摘要的算法，适用于任何抽象解释，特别适用于局部政策迭代。因此，我们可以为递归程序的固定数量的摘要生成抽象域中最强的归纳不变式。我们的最后一个理论贡献是一种通过符号执行获得的公式生成可能是不交的归纳不变式的弱化方法。我们在自由软件静态分析系统CPAchecker中实现了所有这些方法，这使得分析之间可以进行通信和合作。80我们的技术使用模块化满足求解器，能够在给定一阶逻辑公式和某些理论的情况下，提供模型或证明不存在模型。为了简化与这些工具的通信，我们介绍了JavaSMT库，提供了通用接口。这个库已经为许多研究人员证明了其实用性。90目录0目录 90图目录 150表格目录 170I 准备工作 2101 简介 23 1.1 动机：软件系统的复杂性 . . . . . . . . . . . . . . . . . . . . . 2301.2传统方法确保可靠性2401.3什么是规范?2401.3.1安全性和活性2501.4停机问题和程序分析格局2501.4.1有限空间探索2501.4.2正确构建软件2601.4.3欠估计方法2601.4.4过估计方法2601.5什么是验证器输出?2701.6贡献和论文大纲2701.6.1理论贡献2801.6.2工程贡献2902背景31 2.1介绍3102.1.1章节大纲3102.1.2符号和定义3102.2程序形式化3202.3程序分析中的逻辑3402.3.1转换为公式3502.4使用公式编码查找错误3502.5证明安全3602.5.1归纳不变性3602.5.2显示归纳3702.5.3归纳断言映射3802.5.4 k-归纳3802.5.5回到安全3902.6归纳不变性从反例到归纳392.9Path Focusing and Large-Block Encoding . . . . . . . . . . . . . . . . . . . . .482.10 Configurable Program Analysis . . . . . . . . . . . . . . . . . . . . . . . . . . .502.10.1 Composite Configurable Program Analysis. . . . . . . . . . . . . . . .52IITheoretical Contributions533Local Policy Iteration553.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .553.1.1Motivation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .553.1.2Max-policy iteration . . . . . . . . . . . . . . . . . . . . . . . . . . . . .563.1.3Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .573.1.4Chapter Overview. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .573.2Background . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .583.2.1Definitions. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .583.2.2Least Invariant as a Convex Optimization Problem . . . . . . . . . . . .583.2.3Template Constraints Domains . . . . . . . . . . . . . . . . . . . . . . .603.2.4Examples of Solvable Programs . . . . . . . . . . . . . . . . . . . . . . .613.2.5Max Policy Iteration Algorithm . . . . . . . . . . . . . . . . . . . . . . .613.2.6Selecting Multiple Policies . . . . . . . . . . . . . . . . . . . . . . . . . .653.2.7Analyzing the Running Example with Policy Iteration . . . . . . . . . .673.3Local Policy Iteration (LPI) . . . . . . . . . . . . . . . . . . . . . . . . . . . . .693.3.1LPI Formalization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .703.3.2Properties of LPI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .723.4Extensions and Optimizations . . . . . . . . . . . . . . . . . . . . . . . . . . . .753.4.1Extending to Integers. . . . . . . . . . . . . . . . . . . . . . . . . . . .753.4.2Extending to Uninterpreted Functions . . . . . . . . . . . . . . . . . . .763.4.3Reducing the Number of Value Determination Constraints . . . . . . . .763.4.4Merging the Unknowns. . . . . . . . . . . . . . . . . . . . . . . . . . .773.4.5Shrinking the Search Space . . . . . . . . . . . . . . . . . . . . . . . . .783.4.6Ordering the Optimization Objectives . . . . . . . . . . . . . . . . . . .783.5Experiments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .793.5.1Timing Results . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .793.6Conclusion. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .803.6.1Future Work. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .801002.7通过抽象解释归纳不变性3902.7.1正式定义4002.7.2抽象值转换器4202.7.3收敛和扩展4302.8抽象域的进一步示例4402.8.1八边形4402.8.2多面体4502.8.3模板约束领域4502.8.4分离领域4702.8.5数值同余的抽象领域4702.8.6谓词抽象域4702.8.7其他领域484.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .834.2Enumerative Template Synthesis . . . . . . . . . . . . . . . . . . . . . . . . . .844.3Filtering Templates Using Live-Variables Analysis. . . . . . . . . . . . . . . .861104 模板合成 8304.1.1 相关工作 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8304.2.1 超越有理数 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8504.4基于插值的模板合成 . . . . . . . . . . . . . . . . . . . . . . . 8804.4.1 抽象可达性树生成。 8804.4.2 从插值生成模板。 9104.4.3 引导插值过程。 9304.5 使用凸包进行模板合成。 9404.5.1 背景：多面体域中的抽象解释。 9504.5.2 离线细化方法。 9504.5.3 在线注入方法。 9604.5.4 算法属性。 9904.6 评估。 9904.6.1 活跃变量。 9904.6.2 凸包模板合成。 10004.6.3 基于插值的模板合成。 10004.7 结论。 10105使用策略迭代生成摘要 10305.1 引言。 10305.1.1 贡献。 10505.2 相关工作。 10505.3 背景。 10605.3.1 过程间程序模型。 10605.3.2 不变量和计算模型。 10705.3.3 归纳不变量和语义方程。 10805.4 摘要作为抽象状态。 11005.5 应用策略迭代。 11005.6 使用程序内分析生成摘要。 11305.7 算法属性。 11705.8 实现。 11705.9 扩展。 11805.9.1 支持参数和返回表达式。 11805.9.2 使用预分析支持全局变量。 11805.9.3 抽象可达性树生成。 11805.9.4 生成多个摘要。 11905.9.5 大块编码支持和内联。 11905.10 评估。 11905.11 结论和未来工作。 12005.11.1 未来工作。 1206.1.2Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1246.1.3Counterexample-to-Induction Weakening Algorithm. . . . . . . . . . .1246.1.4From Weakenings to Abstract Postconditions . . . . . . . . . . . . . . .1256.2The Space of All Possible Weakenings. . . . . . . . . . . . . . . . . . . . . . .1266.2.1Eliminating Existentially Quantified Variables . . . . . . . . . . . . . . .1286.3Formula Slicing: Overall Algorithm . . . . . . . . . . . . . . . . . . . . . . . . .1286.3.1Abstract Reachability Tree. . . . . . . . . . . . . . . . . . . . . . . . .1286.3.2Example Formula Slicing Run . . . . . . . . . . . . . . . . . . . . . . . .1296.4Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1306.5Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1316.6Experiments and Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1316.7Complexity of Finding a Non-Trivial Inductive Weakening Over Literals . . . .1336.8Conclusion and Future Work. . . . . . . . . . . . . . . . . . . . . . . . . . . .1356.8.1Future Work. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .136IIIEngineering Contributions1377Implementation1397.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1397.2Software Architecture. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1397.3Installation Instructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1397.4Usage Instructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1407.4.1Configuration Options . . . . . . . . . . . . . . . . . . . . . . . . . . . .1417.4.2Looking at the Output Further . . . . . . . . . . . . . . . . . . . . . . .1417.5CPA Formulation. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1427.5.1Abstraction for LPI. . . . . . . . . . . . . . . . . . . . . . . . . . . . .1437.5.2Abstraction for Slicer . . . . . . . . . . . . . . . . . . . . . . . . . . . .1437.6Abstract Reachability Graph Generation . . . . . . . . . . . . . . . . . . . . . .1437.7Extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1447.7.1Combination with Other Configurable Program Analyses. . . . . . . .1447.7.2Combination with k-Induction. . . . . . . . . . . . . . . . . . . . . . .1477.8Conclusion. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1487.8.1Software Project and Contributors . . . . . . . . . . . . . . . . . . . . .1487.8.2Future Work. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1488JavaSMT Library1498.1Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1498.2Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1508.2.1Formula Representation . . . . . . . . . . . . . . . . . . . . . . . . . . .1508.2.3Formula Introspection . . . . . . . . . . . . . . . . . . . . . . . . . . . .1518.2.5Multithreading Support . . . . . . . . . . . . . . . . . . . . . . . . . . .1528.3Project Architecture . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1521206公式切片：从前置条件中归纳不变量 123 6.1引言。 12306.1.1 贡献。 12408.2.2 类型安全 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15008.2.4 处理中断 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1518.4Memory Management. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1528.5Case Study: Inductive Formula Weakening. . . . . . . . . . . . . . . . . . . .1538.5.1Implementation Task . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1538.5.2Implementation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1548.6Related Work . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1558.7Conclusion. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1558.7.1Future Work. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .156IVConclusion1579Conclusion1599.1Contributions Outline. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1599.2Importance of Engineering . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1599.3Future Work and Research Directions. . . . . . . . . . . . . . . . . . . . . . .1609.3.1Towards Software Systems Verification . . . . . . . . . . . . . . . . . . .160Bibliography1631314List of Figures2.1BNF Grammar of the Analyzed Language . . . . . . . . . . . . . . . . . . . . .332.2Non-Inductive Invariant Example . . . . . . . . . . . . . . . . . . . . . . . . . .372.3k-Induction Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .392.4Hasse Diagram for Sign Abstract Domain over Integers . . . . . . . . . . . . . .412.5A simple counter program and the corresponding CFA.. . . . . . . . . . . . .442.6Abstract Domains Comparison. . . . . . . . . . . . . . . . . . . . . . . . . . .452.7Template constraints domain element. . . . . . . . . . . . . . . . . . . . . . .462.8Motivating Example for Path Focusing . . . . . . . . . . . . . . . . . . . . . . .492.9Transformations required for Large Block Encoding . . . . . . . . . . . . . . . .492.10 Mot
