AI-Introduction

发表于 更新于 阅读次数： 本文字数： 3.4k 阅读时长 ≈ 6 分钟

AI: abstract Interpretation

对 _Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation_这本书的阅读笔记

介绍

抽象解释是程序静态分析的一种方法，目的是得到关于程序的一些信息。所谓“抽象“有点像”抽象代数“中的抽象（但是这个和抽代没什么关系，只是意思有点相似），就是把原来不一样但是相近的东西分成一类。举个例子，一个整数可以在程序中取很多个值，但是我们只是粗略的看，就是只看它的符号，或者只看它所属的区间，这样就能把很多不同的数据看做一个，减少推导的计算量。

对于一种数据有很多种抽象的方法，这些方法的精度不同，因此推导难度和能得到的信息强度也不一样，要想得到想要的信息需要选择合适的抽象。在第二章中我们将会学到一些用来比较不同抽象精度差别的数学工具。

Introduction

介绍，用非形式的语言介绍什么是抽象解释

抽象解释是对程序进行静态分析的一种方法。

静态分析

A static analyzer is a program that takes as input a program and outputs information about its possible behaviors, without actually executing it.

静态分析指的是和测试相对的，不运行程序得到其相关信息的一种方法，例如程序中变量的取值范围、模几同余、变量之间的关系等等。

由于停机问题的不可判定性，程序验证是不可能完全自动化的，因此必须选择放弃以下性质之一：automation, generality, or completeness

  • Deductive Methods： 演绎方法，放弃部分的自动化
  • Model Checking：模型检验，放弃通用性
  • Static Analysis：静态分析，放弃完整性，也就是说只能得到关于程序的部分信息。这是本书要讲的主要内容

抽象解释

The theory of Abstract Interpretation, is a general theory of the approximation of formal program semantics.

抽象解释是一种用来近似程序语义的通用理论。

it makes it possible to express mathematically the link between the output of a practical, approximate analysis, and the original, uncomputable program semantics.

可以从数学上表达实际的近似结果和原始的不可计算的程序语义之间的关系。

定义说的有点迷糊，我的理解是 抽象解释就是一种表达和分析程序语义的一种方法。这个后面章节应该会具体介绍。

这一章主要是通过例子大概介绍这本书的内容。

1.1 A First Static Analysis: Informal Presentation

image-20221025142959284

这是一个例子

1.1.1 Sign Analysis

符号分析，就只是分析程序中变量的符号，利用一些显而易见的性质例如 ，来推导性质，对于上面这个例子有：

image-20221025144132209

T 表示在这里符号未知。

因为符号分析只能利用程序中的符号信息，在 5: 不知道一个正数减正数是什么符号，即使我们可以肉眼看出来由于 所以 ，但是这个不属于单纯的sign information。

循环

循环内的 sign information 需要通过迭代推导，直到达到不动点。对于上面的程序，第一次进入循环时的条件是 ，第二次进入循环时，条件是 ，第三次进入循环时 条件和第二次一样，因此我们可以断定再继续推理下去得不到新的信息了，也就是说达到了不动点(fixpoint)。

1.1.2 Affine Inequalities Analysis

仿射不等式分析（不知道这里为什么用仿射这个词）

image-20221025145503759

这是比 符号分析 更加精细的推导，可以得到关于源程序更详细的信息。上图中红色的部分就是不能通过符号推理得到的。

书上这一章多次提到了 convex polyhedra （凸多面体），但是我没看出来这个和凸多面体的关系，后面章节会介绍。

1.1.3 Iterations

image-20221025150432189

抽象(abstraction)

书里面多次提到了这个单词，比如之前的符号推导是抽象，Affine Inequalities 也是抽象，这一节的 interval analysis 也是抽象，我觉得抽象就是把一个具体的变量表达成它的性质然后用这些性质去进行推理。

至于这一节为什么叫 Iterations ，可能因为要获取 1.4 a 里面的这些区间信息，就需要像 1.4 b 这样迭代。书里面管这个叫 collection semantics收集语义。

但是这样（和执行一遍程序有什么区别）就不够静态了，而且有的程序要循环无穷次怎么办？书里面还提到了一种方法叫做 convergence acceleration （收敛加速），这样可以用更少的迭代次数得到结果。（当然这一节没具体讲

1.1.4 Precision

精度

image-20221025163747730

感觉这个图想表达的是这几种分析的精度差别：

精度：符号分析 < 区间分析 < 仿射不等式分析 （< 具体执行）

More expressive abstractions generally lead to tighter over-approximations, and so, more precise results.

但是更精确的表示需要更高的计算开销，there is a trade-off

1.1.5 Soundness

翻译成可靠性比较好

S 是 specification（规格），就是这个程序正确运行需要的条件，A 是抽象，P 是这个具体的程序。我们通过将 P 抽象为 A 扩大了 P 的范围，对于 S 来说 P 是不容易验证的，而 A 相对来说比较容易验证，所以想要证明 可以先证明

image-20221025164056833

c 不是 sound 的，我们在这里不讨论

学长说 soundness 就是 “只要验证了，就是对的”

1.2 Scope and Applications

范围和应用

这一节解释我们为什么对这些抽象感兴趣（通过一些例子。

1.2.1 Safety Verification

image-20221025164356221

可以用来验证一个程序能不能被安全执行，如上图所示，a是这个程序正常执行需要满足的条件，b 是我们从程序语义通过推理得到的性质，由于 b 是满足 a 的，所以这个程序可以正确执行。

1.2.2 Pointer Analysis

对指针的分析（指针就是类似于c语言中的指针）

这里的观点是，指针也可以看做数值变量（一个基地址和一个 offset，基地址是不变的，offset可以看成一个普通变量进行分析）。

1.2.3 Shape Analysis

对于数据结构的分析？

1.2.4 Cost Analysis

image-20221025165340145

分析程序复杂度

1.2.5 Backward Analysis

image-20221025164925263

1.3 Outline

本书大纲介绍

  • chapter 2 : 数学工具介绍

  • chapter 3 : 要分析的 toy-language 介绍

  • chapter 4-5 : 介绍两类 abstraction

    firstly, non-relational domains, including signs, constants, intervals, and congruences; secondly, relational domains, including affine equalities, affine inequalities, and weakly relational domains (zones, octagons, and templates).

  • chapter 6 : 讨论抽象域的结合

  • chapter7 : 结束语