基于语义的概率数据流分析的命令式程序及其概率抽象解释技术研究.

理论计算机科学电子笔记190（2007）59-77www.elsevier.com/locate/entcs数据流分析亚历山德拉·迪·皮耶罗1克里斯·汉金2赫伯特·维基基3伦敦帝国理工学院计算机系180 QueenLondon SW7 2AZ英国摘要我们提出了一个基于语义的技术分析的概率性质的命令式程序。这是经典数据流分析的概率版本。我们将这种技术应用于pWhile程序，即用简单While语言的概率版本编写的程序。作为第一步，我们引入了一个基于语法的线性运算符语义（LOS）的定义，它等价于While的标准结构运算语义。 pWhile程序的LOS可以被看作是离散时间马尔可夫链的生成器，并且扮演着与经典While的收集或跟踪语义类似的角色。然后采用概率抽象解释技术来定义奇偶校验和实时变量等关键词：概率程序，线性算子语义，概率抽象解释，数据流分析1引言典型地，经典的数据流分析（DFA）考虑控制流图中的所有路径，并且根据“meet-over-all-paths”方法来计算安全解决方案，即，所有路径对解决方案的贡献相等，而与它们被执行的可行性或可能性无关。然而，在实践中，即使是中等规模的程序也只执行程序可能执行的数十亿条路径中的一小部分。对于给定的分析，所考虑的问题的特定性质可能有助于减少路径的数量。此外，现在人们广泛认识到，考虑概率信息可以从静态分析中获得更统计或其他类型1 电子邮件地址：adip@doc.ic.ac.uk2 电子邮件地址：clh@doc.ic.ac.uk3 电子邮件地址：herbert@doc.ic.ac.uk1571-0661 © 2007由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2007.07.00560A. Di Pierro等人理论计算机科学电子笔记190（2007）59可以以程序语义中的概率的形式对信息的权重进行编码，并用于根据执行按照这种方法，在本文中，我们定义概率DFA，其解决方案在经典意义上是不安全的，但这类似于[7，8]中的方法，其中概率技术用于构建近似属性的静态分析。考虑近似而不是绝对性质对应于断言该性质直到给定的可量化误差幅度，而不是作为布尔关系。这种方法的重要性在于，它通常允许更现实的分析。 作为一个例子，一个安全属性，如confinement，永远不会被真实系统在其绝对公式中满足，断言系统是否被confined。我们展示了如何一个经典的DFA可以变成一个概率通过使用适当的收集语义。这被定义为线性空间上的线性算子，表示给定概率程序的操作配置（当前状态和要执行的指令）。我们将表明，张量积的使用是必不可少的语义的建设，以获得正确的分析结果。这是证明通过我们的概率技术的应用程序，两个经典的DFA的例子，即奇偶校验分析和活变量分析。这些例子也显示了概率分析如何比标准的经典技术产生更实际有用的信息。2可能同时我们考虑的语言是一个简单的经典而扩展的概率选择语句的语言。一种不同但等效的方法来定义概率，随机语言是使用随机分配，例如[14]。我们选择第一种方法，因为它更适合作为我们在本文中提出的治疗方法的基础。在[6]中也采用了相同的方法，其中引入了Hoare风格的证明系统来推理概率顺序程序。2.1语法我们称之为pWhile的语言的语法由下式给出S：：= skip|停止|x ← a |S1; S2|选择p1：S1或p2：S2|如果b则S1否则S2结束，如果|whilebdoSend while在概率选择构造中，我们假设pi是一些常数，表示语句Si被执行的概率;它们定义了一个概率分布，即p1+p2= 1。算术表达式a遵循通常的语法：a：：= n|X |a1年a2年其中n代表一个常量，x是一个程序变量（我们使用字体字符），而“"代表一个常用的算术运算，如”+“、”-"或"“。我们还需要具有以下形式的布尔表达式A. Di Pierro等人理论计算机科学电子笔记190（2007）5961R0 skip，σ−→1 stop，σR1档，σ−→1档，σR2<$x<$a，σ<$−→1<$stop，σ[x<$$> →[[a]]σ]<$R31S1，σ1<$S1;S2，σ<$−→p<$SJ;S2，σJ<$R3·21S1，σS;S，σ1 2p2R4·1R42R51R52R6R6·2n选择p1：S1或p2：S2，σ<$−→p1<$S1，σ<$n选择p1：S1或p2：S2，σ<$−→p2<$S2，σ<$ifbthenS1elseS2end if，σ<$−→1<$S1，σ<$ if[b]]σ=TRUEifbthenS1elseS2end if，σ<$−→1<$S2，σ<$if[b]]σ=FALSEwhilebdoSend while，σ<$−→1<$S，σ<$如果[b]]σ=真whilebdoS端while，σ−→1stop，σif [b]] σ =FALSE表1pWhile的一个概率转换系统b：：=T RUE|FALSE|欧元b|b1和b2|b1和b2|a1<>a2其中<<，注意到，对于诸如：、≤、=、≥、>之类的数学表达式，s和d的组合不具有可操作性。2.2操作语义在本节中，我们以通常的SOS风格为pWhile定义了一个小步操作语义[17]。这对应于一个概率转换系统[13]，其中状态编码关于存储器状态（程序变量的值）和存储器状态（程序变量的值）的信息和要执行的指令。转移关系是概率性的，因为从另一个配置在一个步骤中到达的配置与表示实际执行该转移的概率的数字相关联;此外，与配置的传出转移相关联的所有概率形成概率分布（即它们总和为1）。换句话说，我们根据概率的生成模型[20]定义了我们语言的操作语义，并且由此产生的执行过程是离散时间马尔可夫链[19，1]。2.2.1配置和转换我们将状态定义为从变量到值的映射σ∈State=Var →Value，62A. Di Pierro等人理论计算机科学电子笔记190（2007）59[[a]]aσ=n[[x]]aσ=σ（x） [a1<$a2]]aσ=[[a1]]aσ<$[[a2]]aσ[[TRUE]]bσ=TRUE[[FALSE]]bσ=FALSE[[<$b]]bσ=<$[[b]]bσ[[b1<$b2]]bσ=[[b1]]bσ<$[[b2]]bσ[[b1<$b2]]bσ=[[b1]]bσ<$[[b2]]bσ[[a1>a2]]bσ=[[a1]]bσ>[[a2]]bσ表2表达式算术和布尔表达式的值由函数[. ]] a和[. ]]b在表2中定义。我们将从函数[中省略索引。”当它是明确的从上下文。一个配置是由一个陈述S和一个状态σ ∈ State组成的一对S，σ ∈。概率转移关系−→p由表1中的规则定义。这些除了存在标记每个转换的概率之外，它还反映了经典while语言的典型语义。最后的状态是通过一个在配置上的循环来表示的。 这允许我们将计算建模为马尔可夫链因为它保证表示pWhile程序是一个随机矩阵（cf.第3.1节）。2.2.2抽象语法按照[16]中的方法，为了确定 对于一个程序，不管每个语句执行的实际状态的具体信息如何，我们都将一个来自集合Lab的标签与每个赋值关联起来。语句、skip语句以及出现在条件和循环语句我们称结果程序为标号程序，并定义其语法，我们称之为抽象语法，如下所示：S：：=[skipp]l|[stop]l|[x←a]l|S1;S2|[choose]lp1：S1orp2：S2|while[ b ] l do S en d while|while[b]ldoSendwhile我们将把基本标记指令称为命令，并用Cmd表示具有典型元素c1，c2，.. . ，对应于前[skip]l或[b]l，etc的状态。我们将把umeauniquelablingof commands，即我们将把l与c互换使用，其中c是带有标签l的基本指令;这有时被称为标签一致性属性[16]。程序S的控制流FS则被定义为一组对（l，lJ）或{c1，c2}，它们记录了这样一个事实，即在执行c1之后，下一个执行的命令可能是c2（从测试的具体结果中抽象出来）。原则上，可以从FS中的对l，lJ重建原始程序S的语法：我们只需要指出当测试成功或失败时采取哪个分支;并且对于概率选择，我们需要记录转移概率。如果我们这样做，S的控制流FS，有时也被称为它的抽象语法[5]，可以被视为程序语法的另一种描述。在本文中，我们将使用术语控制流和抽象语法A. Di Pierro等人理论计算机科学电子笔记190（2007）5963⎟⎜可互换地指代带标签的节目。3概率数据流分析传统上，数据流分析基于程序的图形表示，通常通过收集语义来定义。对于我们的概率语言，我们将把这种集合语义定义为线性算子（更确切地说是马尔可夫链）;这表示状态和程序语句，使得概率信息可以在分析的最终结果中适当地导出。我们将在这里考虑DFA的更常见的等式方法，并在3.1节中介绍基于这种方法和线性算子语义的概率技术。我们提出的概率DFA是过程内的（我们不处理函数或过程）。我们将展示我们的技术，提出两个经典的例子，一个向前和向后的分析，前者是具体的奇偶性分析和后者活变量分析。3.1收集语义概率转移系统具有作为矩阵的直接表示，即配置上的向量空间上的线性算子。一般来说，对于任何集合X，我们可以定义X上的向量空间V（X）为X中的元素与域W中的系数的形式线性组合的空间。我们可以将V（X）中的元素表示为向量，其中W中的系数由X索引：V（X）={（vx）x∈X|vx∈ W}。场 W 通 常 被 取 为 复 数 C 的 集 合 。 在 我 们 的 例 子 中 ， 它 简 单 地 对 应 于 [0 ，1]<$R<$C，因为我们对表示概率分布感兴趣支持集X对应于配置集Conf。在构形上表示向量空间的一个方便的方法是通过张量积运算。张量积在描述复合系统时是一个有用的工具，例如在随机系统理论、性能分析、量子物理等方面。它的性质允许我们将笛卡尔乘积V（X×Y）上的向量空间优雅地表示为V（X）<$V（Y）。 这些属性和抽象定义可以在下面找到在[18]中。具体地说，我们可以定义两个有限维矩阵的张量或克罗内克积如下。给定n×m矩阵A和k×l矩阵B，则A是nk×ml矩阵：⎛ ⎞11B.a1 nBAB =。⎝. . ..⎟⎠一个1米B. anmB本文根据程序S的抽象语法或控制流，将S的收集语义定义64A. Di Pierro等人理论计算机科学电子笔记190（2007）59T（n[skip]l1，c2n）=I<$El1，c2T（n[xi←a]l1，c2n）=A（a）<$El1，c2T（[b]l，ct）=B（b）<$El，c不T（[b]l，cf）=（I-B（b））<$El，cFPKT（[stop]l，[stop]l）=IEl，lT（[choose]l，ck）=pk·IEl，cK表3收集语义V（Cmd）= V（值1）. V（值n）在这里，我们假设一个enumeration的程序变量x1，.，xn，并且用值i表示xi的值的集合。因此，我们有V（值）= V（值1×.×值n）= V（值1）. V（值n）。对于FS中所有可能的控制流步骤，即程序S中的命令对c1，c2，我们将描述变量的可能变化，然后将这些变化与控制从一个语句到另一个语句的实际转移一起总结。换句话说，我们定义了程序S的收集语义SJ，线性算子T（C1，C2）的项，对每一对C1，C2∈ FS，T（C1，C2）将一个向量压缩比n→x∈V（State×Cmd）变换为向量压缩比s控制器的输出从C1到C2步进。 形式上： ΣSJ=∈FST（αc1，c2α）其中T可以通过张量积表示：T（c1，c2）= M（c1，c2）<$ N（c1，c2）其中，M（c1，c2n）是描述可能的状态变化的V（State）上的算子，N（c1，c2n）是描述控制流的V（Cmd）上的算子。对于所有可能的命令c1，c2∈Cmd，我们在表3中定义T（c1，c2n），其中我们使用下面解释的控制和状态运算符。请注意，表3中的最后一条规则表示了最终配置上的循环，它保证了C_S_J是一个随机矩阵，并且程序的收集语义确实是一个马尔可夫链。控制操作员在确定性的情况下，即对于命令c1，只有一个命令c2，其中c1，c2∈ FS的情况下，控制流部分N非常简单：它由所谓的矩阵单元E c 1，c 2给出，⎧对于i=c1， j=c2N（nc1，c2n）=（Ec1，c2）i，j=n0否则A. Di Pierro等人理论计算机科学电子笔记190（2007）5965这是因为[skip]l，[stop]l和[x←a]l。 这种复杂性特别适用于顺序组合中语句之间的控制流的情况。在随机选择的情况下，我们必须将控制转移算子构造为两个确定性转移之间的线性组合，从选择点到每个分支的初始标签。这是通过定义N（k，c，k）i，j=pk·Ec，ck其中c是选择命令，ck是第k个分支中的第一个命令对于tsc=[b]l，其中hiles和dif's通常都有一个转换，但是在这种情况下，我们必须在每种情况下将测试成功时实际发生的转换与测试不成功时的转换进行因此，我们在测试点定义控制流，T（C，Ct）=B（b）·（IEc，Ct）T（c，cf）=（I−B（b））·（I<$Ec，cf）如果测试成功或失败，则分别执行测试和[b]landct并执行后续在这个定义中，算子I是恒等式，测试算子B定义为：ΣB（b）=.nΣD（evk）b（v1，.，v n）= TRUEk=1其中，D（x）表示具有对角向量x的对角矩阵，并且e是单位。载体：⎧如果i=j，（ei）=000元，否则因此，D（ei）=Ei，i，如果对于某些变量值，测试b成功，则B在对角线上包含例3.1假设我们有两个变量x1和x2，它们的值都可以在0和4之间。然后[x12]l用一个25× 25的矩阵表示，表示为张量积：⎛⎞1 0 0 0 0⎜⎟⎜⎟⎛ ⎞1 0 0 0 0⎜ ⎟⎜ ⎟⎜0 1 0 0 0⎟ ⎜ 0 1 0 0 0⎟⎜ ⎟ ⎜ ⎟⎜ ⎟⊗ ⎜ ⎟⎜0 0 0 0 0⎟ ⎜ 0 0 1 0 0⎟⎜ ⎟ ⎜ ⎟⎜ ⎟ ⎜ ⎟⎜0 0 0 0 0⎟ ⎜ 0 0 0 1 0⎟⎝ ⎠ ⎝ ⎠0 0 0 0 0 0 0 0 0 166A. Di Pierro等人理论计算机科学电子笔记190（2007）59其表示x2的值对测试结果没有贡献的事实。国家运营商对于所有成本和成本，对于所有成本[x←a]，可变性不会改变，即，我们将得到M=I，即向量空间上的恒等式表示程序变量的值。在常量赋值的情况下.M（[xi←n]l1，c2）=Σi−1我k=1⎛ ⎞ΣJinJinJ.Σn我，我，k=i+1对于一般表达式a，涉及（其他）变量ΣM（[xi←a]l1，c2）=一个v，... v›→v，.，v1ina（v1，.，v n）= v其中Av1，.，vi›→v，.，vn是一个具有单个非零元素的矩阵，定义为：.i−1ΣD（evk）好吧卢恩⊗⎝Evi,v⎠ ⊗ΣD（evk）.k=1jk =i+1换句话说，如果a中的变量的值v i的特定组合产生特定结果v，则对应的矩阵Av1，.，vi›→v，.，表示该单个更新对总和有贡献。例3.2考虑两个变量x1和x2，它们都可以在{0，1，2}。那是什么？[x1←x1+1]l由一个9× 9矩阵表示，它是两个3× 3矩阵的张量积，即：⎛ ⎞ ⎛ ⎞⎜0 10⎟ ⎜1 0 0⎟M（[x ←x+1]l， c）=x⎟⊗⎜ ⎟1 12⎜0 01⎟⎜0 10⎟而⎝ ⎠0 0 0⎝ ⎠0 0 1表示为[x2←1]l⎛ ⎞ ⎛ ⎞⎜1 0 00 1 0M（[xl⎜⎟ ⎜ ⎟←1]，c）=1⎟⊗⎜0 10⎟2 20 1 0⎟⎠0 0 1⎜ ⎟⎝ ⎠0 1 0在下面的例子中，我们展示了如何为一个简单的pWhile程序S构造完整的收集语义。例3.3考虑由下式定义的程序S⎝A. Di Pierro等人理论计算机科学电子笔记190（2007）5967⎝⎝如果[x==0]a，则[x←0]b;其他[x←1]c;end if;[stop]d如果我们用a、b、c和d来枚举四个相关的程序点，并假设x只能有两个值，即0和1，那么整个程序由下式表示（其中Id表示d×d单位矩阵）：⎛⎛ ⎞ ⎞SJ=0 02014年4月·（I2Eab）+⎛⎛ ⎞ ⎞+200 000 12014年4月·（I2（c）+⎛⎛ ⎞ ⎞+10 01 0联系我们⎛⎛ ⎞ ⎞联系我们0 1Ecd⎛⎛ ⎞ ⎞1 0+Edd=0 1⎛ ⎛ ⎞⎞ ⎛ ⎛ ⎞⎞⎜⎛⎞⎜1 0 0 0 ⎟⎟⎜⎛⎞⎜0 1 0 0⎟⎟⎜ ⎜ ⎟⎟ ⎜ ⎜ ⎟⎟⎜1 0⎜ 0 1 0 0⎟⎟ ⎜1 0⎜ 0 0 0 0⎟⎟=⎠⊗⎜⎟⎟·⎜⎝⎠⊗⎜公司简介⎜ ⎜ ⎟⎟ ⎜ ⎜ ⎟⎟⎜0 0⎜ 0 0 1 0⎟⎟ ⎜0 1⎜ 0 0 0 0⎟⎟⎝ ⎝ ⎠⎠ ⎝0 0 0 1⎛ ⎛ ⎞⎞ ⎛⎝ ⎠⎠0 0 0 0⎛ ⎞⎞⎜⎛⎞⎜1 0 0 0 ⎟⎟⎜⎛⎞⎜0 0 1 0⎟⎟⎜ ⎜ ⎟⎟ ⎜ ⎜ ⎟⎟⎜0 0⎜ 0 1 0 0⎟⎟ ⎜1 0⎜ 0 0 0 0⎟⎟公司简介⎠⊗⎜⎟⎟·⎜⎝⎠⊗⎜公司简介⎜ ⎜ ⎟⎟ ⎜ ⎜ ⎟⎟⎜0 1⎜ 0 0 1 0⎟⎟ ⎜0 1⎜ 0 0 0 0⎟⎟⎝ ⎝ ⎠⎠ ⎝0 0 0 1⎝ ⎠⎠0 0 0 0⎠⎠⎠⎠68A. Di Pierro等人理论计算机科学电子笔记190（2007）59⊗⊗⎜B⎜⎟⎛ ⎛ ⎞⎞ ⎛ ⎛ ⎞⎞⎜⎛⎜0 0 0 0⎟⎟⎜⎜0 0 0 0⎜⎞⎜ ⎟⎟ ⎜⎛ ⎞ ⎜⎟⎟⎜1 0⎜ 0 0 0 1⎟⎟ ⎜0 1⎜⎟⎟公司简介⎠⊗⎜电子邮件电话：+86-021-8888888⎜ ⎜ ⎟⎟⎜⎜⎟⎟⎜1 0⎜0 0 0 0⎟⎟⎜0 1⎜⎟⎟⎝ ⎝ ⎠⎠⎝0 0 0 0⎛ ⎛ ⎞⎞0 0 0 1⎟⎟⎠⎠0 0 0 0⎜⎛⎞⎜0 0 0 0⎟⎟⎜ ⎜ ⎟⎟⎜1 0⎜ 0 0 0 0⎟⎟⎜⎝ ⎠⎜ ⎟⎟⎜ ⎜ ⎟⎟⎜0 1⎜ 0 0 0 0⎟⎟⎝ ⎝ ⎠⎠0 0 0 1⎛ ⎛ ⎞⎞⎛⎛ ⎞⎞⎜⎛⎜0 1 0 0⎟⎟⎜⎜0 0 1 0⎜⎞⎜ ⎟⎟ ⎜⎛ ⎞ ⎜⎟⎟⎜1 0⎜ 0 0 0 0⎟⎟ ⎜0 0⎜⎟⎟=⎠⊗⎜电子邮件电话：+86-021-8888888⎜ ⎜ ⎟⎟⎜⎜ ⎜ ⎟⎟⎜⎟⎟⎜ ⎟⎟⎜⎝0 0⎝ 0 0 0 0⎠⎠ ⎝0 10 0 0 00 0 0 0⎟⎟⎠⎠0 0 0 0⎛ ⎛ ⎞⎞ ⎛ ⎛ ⎞⎞⎜ ⎜0 0 0 0 ⎟⎟⎜⎜0 0 0 0⎜⎛ ⎞⎜⎟⎟ ⎜⎛ ⎞⎜⎟⎟⎜1 0⎜0 0 0 1⎟⎟⎜0 1⎜⎟⎟公司简介⎠⊗⎜电子邮件电话：+86-021-8888888⎜ ⎜ ⎟⎟⎜⎜ ⎜ ⎟⎟⎜⎟⎟⎜ ⎟⎟⎜⎝1 0⎝ 0 0 0 0⎠⎠ ⎝0 10 0 0 00 0 0 1⎟⎟⎠⎠0 0 0 0⎛ ⎛ ⎞⎞⎜⎛⎞⎜0 0 0 0⎟⎟⎜ ⎜ ⎟⎟⎜1 0⎜ 0 0 0 0⎟⎟⎜⎝ ⎠⎜ ⎟⎟⎜ ⎜ ⎟⎟⎜0 1⎜ 0 0 0 0⎟⎟⎝ ⎝ ⎠⎠0 0 0 1因此，收集语义导致以下随机矩阵：⎛ ⎞1000000... x= 0， [x== 0]a⎟⎜ ⎟⎜00010000...x= 0，[x←0]⎟拉克什茨0000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000x= 0， [x←1]⎟⎜ ⎟⎜0 0 0 1 0 0 0 0⎟...x= 0， [stop]dSJ=十万... x= 1， [x== 0]a⎜ ⎟⎜ ⎟阿夫林b00010000...x= 1，[x←0]⎜ ⎟拉克什茨⎝+=⎝⎝+A. Di Pierro等人理论计算机科学电子笔记190（2007）5969⎜0 0 0 0 0 0 0 1⎟⎝⎠0 0 0 0 0 0 0 1...x= 1，[x←1]...x= 1， [stop]d70A. Di Pierro等人理论计算机科学电子笔记190（2007）59一一GG3.2可能的抽象解释为了从收集语义中构造pWhile程序的抽象DFA方程，我们需要一种方法来抽象语义。我们的概率抽象框架提供了一种获得DFA方程的定量方法解释（PAI）[10，11]。这是（概率）程序的概率分析的一般框架，它在向量空间设置中改写了经典的抽象解释[3，4其基本思想是将抽象定义为某些适当向量空间上的某种线性算子。更确切地说，域（抽象域和具体域）是希尔伯特空间，即具有内积的向量空间。具体化的关键概念在这个框架中表示通过一个线性算子的广义逆的概念，特别是摩尔-彭罗斯伪逆（MP）的概念。这类线性逆的性质使得线性算子与它的MP对成为一个类似于经典Galois联络概念的附加算子。设C和D是两个Hilbert空间，A：C <$→ D是它们之间的有界线性映射有界线性映射A<$=G：D → C是Ai <$的Moore-Penrose伪逆AG=PA和GA=PG其中PA和PG表示正交投影（即， P=PA=P2P=PG= P2其中。[18，Ch 10]表示A和G的值域上的伴随。概率抽象解释定义为具体域C和抽象域D之间的一对线性映射A：C → D和G：D <$→ C，使得G是A的Moore-Penrose伪逆，反之亦然。如[10]所示，任何经典的抽象解释都可以通过将经典域提升到概率域（希尔伯特空间）而被视为概率抽象解释。另一种分析概率程序的方法是将经典的抽象解释技术应用于概率语义[15]。这种方法对应于经典抽象解释的特殊情况如[9]所示，更一般的PAI方法允许我们构建更多的统计信息，这更符合平均案例分析的精神。设T是希尔伯特空间V上的线性算子，表示具体程序的概率语义，设A：V →W是线性抽象函数，G=A†。于是，一个抽象语义可以在W上定义为：T#=一般临时人员。这种所谓的诱导语义保证是基于伽罗瓦连接的经典抽象的具体语义的最佳正确近似。在PAI的基于线性空间的设置中，其中经典域的顺序被度量距离的一些概念所取代，导出的抽象语义是最接近具体语义的语义[10]。A. Di Pierro等人理论计算机科学电子笔记190（2007）59714奇偶分析基于pWhile的LOS的分析的第一个例子涉及变量的奇偶性 虽然这种分析本身是否有任何实际用途是不确定的，但它肯定是一个非常有用的例子，以说明基本的方法。奇偶性分析的目的是在每个程序点确定一个变量是偶数还是奇数。这是一个简单的前向分析，其中变量的具体值被抽象为它们的奇偶校验信息。我们将考虑两个简单的程序，计算n的阶乘和n的阶乘的两倍，当程序终止时，n留在m[m←1]1;而[n>1]2做[m<$m×n]3;[n<$n−1]4end while[停止]5[m←2]1;而[n>1]2做[m<$m×n]3;[n<$n−1]4end while[停止]5在不涉及太多细节的情况下，应该很明显，经典的奇偶分析应该检测到m=2×n的奇偶性！在第二个节目的结尾当n的原始值（和奇偶校验）是“未知”时，总是偶数。然而，对第一个程序的安全经典分析将失败，因为它将在程序结束时返回这在某种意义上是相当不令人满意的，因为很明显m=n！is “nearly always” 只有在“罕见”的情况下概率程序分析的目的是对程序终止时m的奇偶性的这种直觉其思想是以与具体LOS相同的方式（重新）构造程序的抽象LOS，唯一的区别是，在抽象情况下，实现测试和赋值的（一些）操作符被其抽象版本所取代。该程序的一般方案由下式给出：T=MiIE1， 2+TT（IIE2， 3）+T（IIE2， 5）+ 一个人3， 4+INE4， 2+IIE5， 5其中第一个因子，即第一个变量，代表m，第二个变量代表n。 我们稍微滥用一下记号，用同一个符号I来表示不同维数的恒等式。每个贡献Eij中的最后一个分量是一个5× 5矩阵，它代表控制流程步骤。第一项指定程序点1处的动态：m使用i= 1， 2的算子Mi72A. Di Pierro等人理论计算机科学电子笔记190（2007）59⎜⎜⎟⎟的形式：⎛ ⎞0 1 0 0...⎜ ⎟⎜ ⎟⎛ ⎞0 0 1 0...⎜ ⎟⎜ ⎟100... 000 1 0... ⎟M1=0M2=100...00 0 1 0... ⎟⎝. . .⎠. . . .⎝. . .⎠. . . .其分别实现了m的值变为变量n保持不变，由标识I表示，控制从语句1转移到语句2。接下来的两项涉及测试[n >1]2：实际的结果只是控制转移，两个变量没有变化。然而，根据测试的结果，我们得到不同的控制流传输。测试算子实现为：⎛ ⎞ ⎛ ⎞十万1000... ⎟⎜ ⎟ ⎜ ⎟十万 0100... ⎟⎜ ⎟ ⎜ ⎟⎜ ⎟ ⎜ ⎟T T =I00 1 0. ⎟⊗ IT ⊥ =I⊗⎜0 0 0 0... ⎟⊗ I⎜ ⎟ ⎜ ⎟⎜ ⎟ ⎜ ⎟0001... 你好，我是... ⎟⎜⎝. . .⎟⎠. . . .⎜⎝. . .⎟⎠. . . .TT“过滤”了所有那些n为2，3，.的配置。而T“ 在这两种情况下，m的值和程序中的当前位置都是不相关的;这由用于定义测试操作符的恒等操作符来表示。第四项表示最复杂的算术运算，即语句[m←m×n]3。对m和n的改变是相当复杂的，因此描述m和n上的效应的算子A被给出为以下形式的ΣA=i、j（（I<$Ej，i·j<$I）（Ti<$Tj<$I））其中Tk=Ek，k对于所有k。 这可以解释如下：对于所有的对（m，n），我们首先测试m和n是否分别具有特定的值i和j（忽略当前语句标签），然后我们通过保持n（和当前语句标签）不变，但将m的值从j更改为新值i·j来执行更新。T的定义中的倒数第二项导致n的递减：A. Di Pierro等人理论计算机科学电子笔记190（2007）5973我不⊥（Shift）操作符：⎛ ⎞十万 ⎟⎜ ⎟一千零一... ⎟⎜ ⎟⎜ ⎟N=100100... ⎟⎜ ⎟⎜ ⎟0010... ⎟⎜⎝. . .⎟⎠. . . .最后一项只是将终端配置[stop]5指定为无限循环，使m和n保持不变。具体语义学两个程序都有5个程序点，这意味着控制转移矩阵是5×5矩阵。 这两个变量的状态原则上由无穷维向量表示。然而，如果我们固定一个最大输入大小n≤N，那么我们也可以限制m的最大大小。对于这个有限近似，我们可以看到V （{0，1， . . ， N！{0，1， .. . ， N}）N（{1， . . ，5}），即， 5·N·N！维向量因此，具体的（有限的）语义由相同维度的矩阵虽然稀疏，但对于N= 10，它已经是一个大约1800万×1800万的矩阵。抽象语义为了获得抽象语义，我们可以抽象两个变量，即或者，我们可以只抽象m，并使用控制变量n(the这里的while循环实际上是for循环）。在这两种情况下，T的维数都大大减少了。在第一种情况下是2· 2· 5=20，在第二种情况下是2·N·5 = 10N更准确地说：我们简单地将抽象语义T#构造为T#=M#=1， 2+T#（I/T#2、 3）+T#（I/OI/E2， 5）+A#E3， 4+IN#E4， 2+IIE5， 5即与混凝土的方式完全相同。只有少数算子表现出这种差异（而且恒等式的维数大大降低）。控制流程步骤根本没有改变，因为我们在这里只对数据流程分析感兴趣。每个运算符都是使用奇偶校验74A. Di Pierro等人理论计算机科学电子笔记190（2007）59我2不⊥不⎠⊥抽象运算符P：⎛ ⎞PT =100 10 10... ⎠10101...和它的Moore-Penrose伪逆P†。 例如：M#=P<$MP，A#=（P<$$>P<$）A（P<$P），等等。我们因此得到（如果我们抽象两个变量）：⎛ ⎞ ⎛ ⎞ ⎛ ⎞ ⎛ ⎞0 1M#=01 00 1 1 0N#=10011 0A#=10011 0抽象测试操作符T#T#依赖于有限近似，考虑. 如果我们不抽象控制变量n，我们需要更复杂的A#但测试操作符T#T#以及N#与用于具体语义数值结果使用octave这样的数值程序来实现具体的有限近似以及抽象语义是相当简单的[12]。正如预期的那样，即使使用稀疏矩阵表示，其大小也非常大;而对于N= 5的情况仍然可以解决，因此不可能处理N= 10的情况。抽象语义学不会产生这样的问题。如果我们将m抽象为偶数和奇数，但将n保留为具体的控制变量，我们可以< 取决于截点N，我们得到对于N= 10，20%，对于N= 100，2%，对于N= 1000，0.2%的机会，m在程序结束时是奇数。正如预期的那样，这准确地反映了这样一个事实，即m5实时变量分析一个更有趣的静态程序分析是经典的活变量（LV）分析，参见[16]。这是一个反向分析的例子，即控制现在必须扭转局势。为了做到这一点，我们使用原来的控制传递矩阵的转置。我们感兴趣的属性是每个程序点的变量是活的还是死的（在程序点的出口处），也就是说，在程序执行的后期阶段，变量是否有可能被使用。例如，如果有一个赋值给一个从未使用过的程序变量，那么我们可以消除这个赋值，即执行死代码消除。概率LV分析的目的是提供对稍后使用某个变量的概率的估计。一个可能的应用可能是支持缓存，变量，这是更多的M#=01⎠⎠⎠A. Di Pierro等人理论计算机科学电子笔记190（2007）5975可能被使用的变量可以被保存在“更快”的缓存中其思想是，像以前一样，将定义具体语义（描述变量值的精确变化）的运算符替换为仅记录变量是否被使用（在赋值右侧的测试b或表达式a中）或被重新定义（它出现在赋值左侧）的运算符。这基本上也发生在经典的LV分析中：如果x在赋值的右边，它会被的语义所有其他语句都不会改变变量的5.1报表内更新我们记录的关于每个变量的信息只是它是否活着，也就是说，我们需要考虑每个变量在V（{live，dead}）中的抽象状态。更新可以以与经典分析（例如[16]之后）的情况非常相似的方式指定，其中局部传递函数通常通过两个辅助函数kill和gen来定义，为每个标签返回变量集分别是死的和活的 我们可以将kill和gen算子定义为：⎛ ⎞ ⎛ ⎞K=0.010 11 0G=0.0000001 0通过使用这些运算符，我们可以通过以下抽象运算符来表示测试和赋值：[b]lJ=V（b）⎛ ⎞i−1[001 pdf 1st-31files]2016-05-21 00：01：01j=1我是Knj=i+1I）·V（a）NT，其中NT是控制流矩阵的转置，V（e）标识布尔或算术表达式e中的（自由）变量：nV（e）=j=1⎧如果xi∈FV（e）Vi（e），其中Vi（e）=否则我会。注意，我们可以通过抽象具体的算子来获得这些算子，但为了简洁5.2报表间更新我们仍然要解决的问题是在“汇合点”发生了什么即当几个（向后）控制流在一个if或while语句中的测试中聚集在一起时。要做到这一点，我们需要关于分支概率的额外信息。 这可以通过（i）实验性地从剖面图或（ii）从具体的语义，通过不抽象至少那些变量，⎠76A. Di Pierro等人理论计算机科学电子笔记190（2007）59控制流（如在前面的例子中）或（iii）通过估计这些概率的另一个抽象语义。在下文中，我们将概述基于最后一种选择的分析的基本要素。为了说明LV分析的概率版本的基本目的和结构，考虑以下两个程序：[跳过]1如果[odd（y）]2，则[x←1]3其他[y←1]4end if[y←x]5[y←2 ×x]1如果[odd（y）]2，则[x←1]3其他[y←1]4end if[y←x]5这两个程序的经典LV分析，从LVexit（5）=0开始，结果，除其他外，在第二个语句中测试开始时的活动变量的以下描述LV条目（2）={x，y}。这表明变量x和y在测试点可能都是活的。这是一个保守的结果。在一个具体的执行中，x实际上可能是不存在的：虽然在标签5处需要它，但如果测试结果失败，即如果y是偶数，它将被在第一个程序中，我们我们的目标是概率LV分析的合理结果可能是：第一个节目，LV入口1（2）={x，，y， 1}2LVentry（2）={\displaystyle\mathbb { 1}}第二个在第一种情况下，我们期望分支概率的良好估计是由测试成功或失败的概率为50：50给出的。这是一个推论，即（在没有任何进一步假设的情况下）y是偶数或奇数的概率是相同的。在第二个程序中，我们可以通过合理的奇偶分析来保证y总是偶数，尽管y的确切值是完全未知的。与经典分析的所有概率版本一样，我们可以通过记录可能性而不是概率，从概率版本（重新）构建经典结果。为此，我们只需要定义一个从V（X）到P（X）的遗忘映射，它只考虑概率分布的支持，即X中与非零概率相关联的那些元素。A. Di Pierro等人理论计算机科学电子笔记190（2007）59775.3分支概率的估计对if语句（以及类似的while循环）的分支概率的正式估计遵循以下方案：执行第一阶段分析（例如奇偶分析）以确定分支概率，然后使用这些估计进行实际分析。这意味着我们用概率选择来代替测试b，其中选择概率pT和pT由第一阶段分析确定。[skip]1[choose]2pT：[x←1]3或p：[y←1]4[y←x]5[y←2 ×x]1[选择]2pT：[x←1]3或p：[y←1]4[y←x]5从这个例子中可以看出，我们的方法使得“抽象”程序最终成为概率性程序成为必要一旦我们确定了选择概率pT和p，实际的LV分析基本上以与经典情况相同的方式执行，除了我们必须处理变量的概率分布（指示变量在某个程序点是活的的概率）而不是潜在的活变量集。为了在“conjuncience”点上结合有关活变量的信息6结论在本文中，我们提出了基于语法的概率数据的基本要素-通过概率抽象解释，取代了标准的Cousot Cousot方法的可能性分析构建的流分析。我们使用一个带有概率选择结构的小型命令式语言（即pWhile）来说明这个框架。 对于这种语言，我们提出了一个收集语义，它本质上构造了一个离散时间马尔可夫链的生成器，实现了一个pWhile程序的操作语义。这种收集语义是使用线性组合（和）和张量积“组合地”定义的，以表示状态和状态变换。利用这个结构，我们可以定义一个抽象语义作为基础，我们的分析。这种虽然将奇偶分析等分析提升到概率版本很简单，但其他分析（如活变量分析）需要两阶段分析，在实际分析之前，我们首先估计分支概率。ysis发生。进一步的工作将研究最佳抽象的问题，即。78A. Di Pierro等人理论计算机科学电子笔记190（2007）59方法来构建特别是控制变量的抽象，以获得这些分支概率的最佳估计。或者，对于次优抽象，我们也有兴趣确定这些估计的误差幅度。最后，我们计划将这种方法扩展到更高阶，例如。函数，语言和实现一个自动分析仪的原型。引用[1] Bause，F.和P. Kritzinger，[2] Bergstra，J.，A. Ponse和S. Smolka，editors，[3] Cousot ， P. and R. Cousot ， Abstract Interpretation ： A Unified Lattice Model for Static Analysis ofPrograms by Construction or Approximation of Fixpoints，1977年， 洛杉 矶， POPL'77会议 记录238-252。[4] Cousot，P. and R. Cousot，Systematic Design of Program Analysis Frameworks，in：Proceedings ofPOPL269-282.[5] Cousot，P. and R. Cousot，通过抽象解释的程序转换框架的系统设计，在：POPL'02（2002）的会议记录中178比190