面向对象程序共享分析中的线性性探讨

可在www.sciencedirect.com在线获取理论计算机科学电子笔记322（2016）3-18www.elsevier.com/locate/entcs面向对象程序共享分析中线性性的利用Gianluca Amato Maria Chiara Meo Francesca Scozzari意大利佩斯卡拉Chieti-Pescara大学经济系摘要提出了一种基于抽象解释的面向对象程序共享分析方法。当两个变量绑定到重叠的数据结构时，它们共享。我们表明，共享分析可以大大受益于线性分析。我们提出了一个包括混叠，线性和共享信息的组合域。我们使用基于图形的别名信息表示，自然编码共享和线性信息，并定义所有必要的操作符，用于分析类Java语言。保留字：共享分析，线性，别名，面向对象编程。1介绍在面向对象的语言中，程序变量通常绑定到可能重叠的Java程序就是这种情况，其对象存储在称为堆的共享内存中。发现两个数据结构是否可能重叠是共享分析的范围。这些信息用于程序的并行化和分布：不重叠的数据结构允许在不同的处理器上执行方法，使用不相交的内存。此外，它对改进其他类型的分析，如形状、指针、类和循环分析也非常有用。对于逻辑程序（例如，[10，9，12，8，5，2]），并且关于这个主题的大量文献一直是设计我们用于共享分析的增强抽象域的起点。特别是，使用线性属性[7，9，12，11，3，4]已被证明在处理共享信息时非常有用（参见[6]进行比较评估）。我们展示了如何同样的想法可以改写，以加强共享分析面向对象的程序。我们提出了一种新的共享，混叠和线性特性的综合分析，1电子邮件：{gamato，cmeo，fscozzari}@unich.it[2]作者感谢Fausto Spoto提供的有益建议。http://dx.doi.org/10.1016/j.entcs.2016.03.0021571-0661/© 2016作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。4G. Amato等人/理论计算机科学电子笔记322（2016）3v2图1.一、一个具体的状态，变量为v0，v1，v2，v3，v4。Lr图二、图中具体状态的抽象1.一、基于抽象解释的类Java程序，灵感来自逻辑程序上的相应领域。面向对象程序中的具体状态通常由框架和内存来描述，框架是从变量到内存位置（或空）的映射，内存是从位置到对象的映射。我们的想法是将具体的状态抽象成一种新的图，我们称之为ALP图。例如，给定具有两个字段l和r的类Tree，图1中的状态被抽象为图2中的ALP图。所有的ALP图最多有两个层次：第一个层次的节点被标记为一个或多个变量，而第二个层次的节点没有标记。第一级节点可能有用字段名称标记的传出和传入边，而第二级节点没有传出边。请注意，变量v0和v3所指向的数据结构是以相同的方式抽象的，因为我们没有考虑整个数据结构。1.0.1别名和空值。ALP图可以对变量和字段的定义为空进行编码。如果一个变量在图中不作为标签出现，则它定义为null，而一个字段v0。当不存在离开v0节点的标记有f的边时，f为例如，v1。根据图，r是定义为零的。二、该图还编码了定义的弱别名：两个变量（或两个字段）在指向同一位置（可能为空）时是弱别名。在ALP图中，这意味着它们是同一个节点。例如，图1中的变量v3和v4在同一节点中。 此外，场v2。l和v 2。r被抽象为 单个节点。v0Lrv1Lv3v4LrG. Amato等人/理论计算机科学电子笔记322（2016）35v7v8lrlv9Lrv10Lr图3.第三章。一个具体的状态，变量为v7，v8，v9，v10。见图4。 图3中的具体状态的抽象。1.0.2分享信息。我们有兴趣代表可能的共享信息。我们说两个位置共享，是指从它们可以到达一个共同的位置。 考虑图1中描绘的具体状态。3 .第三章。 这里是V7。R和V8。l被绑定到两个不同的数据结构，它们重叠，因为v7。R. R. R和V8。L. L. 我被束缚在同一个物体上：我们说V7。R和V8。我分享。在抽象图中，我们用两个节点之间的（无向）边来例如，图3中的共享信息由边连接v7捕获。R和V8。图中的l。四、 为了使图尽可能简单，我们省略了可以导出的共享信息，例如v7和v8之间的边。1.0.3线性信息。我们说一个位置是非线性的，当有两个不同的路径从它开始，并达到一个共同的位置。考虑例如图3。从V9开始。r，我们通过v 9到达相同的对象。R. R. L. r或v9. R.R. R. L. 所以我们说V9。R是非线性的。很容易注意到，v9也是非线性的。 一般来说，当一个场v。f是非线性的，变量v也是非线性的。我们用自环来表示可能的非线性信息。例如，图中变量v9和v103是抽象的，如图。四、1.1的示例程序我们在图5中的示例程序的帮助下显示了线性信息的相关性。6G. Amato等人/理论计算机科学电子笔记322（2016）3−≥\||⊆Tree makeTree（n：I n t e g e r）with m：I n teger i s {M =0的整数倍;如果（n个= m）出来=null;其他int n =new Tree;出去 L=int n（n）;出去 R=int n（n）;虚空useTree（）其中m：树，t：树，t l：树，左：树，r i g h t：树i s { m= 10;t = makeTree（m）;tl = t . l ;右= t l . r ; left =t l . l;}} }个文件夹图五. 示例程序L出来LrM左权RTLL不LrLrR(a) 由makeTree方法返回的ALP(b) ALP图表示useTree方法结束时的状态。第一行中的所有节点都是第一级节点，即使有边指向它们。图第六章 示例程序的两个ALP图makeTree方法构建一个深度为n的完整树，其节点都是不同的。实际上，通过使用ALP图进行自底向上的静态分析，我们可以很容易地推断出，对于任何输入n2、makeTree返回一个数据结构，可以用图6a中的图形来描述，其中标签out表示方法的返回值。因为out之间没有无向边。我出去了。r的意思是out。我出去了。R不分享此外，由于没有自循环，一切都保证是线性的。尤其是，out。L.我出去了。L. R不分享useTree方法调用makeTree并提取两个不共享的子树。详细地说，在useTree方法中，由于我们知道t是线性的，我们可以推断tl也是线性 由于tl是线性的，它的场为tl。R和TL。我不分享，所以左右不分享。注意，不需要线性来证明t。l和t。r不要分享（分享就足够了）。 当我们想更深入地证明t时，我们需要线性。L. l和t。L. R不分享t的线性在这里证明左和右不共享是在useTree方法结束时的堆可以用图1中的图来描述6b.2预赛我们用[v1t1，.， 其中dom（f）={v1，.， vn}并且f（vi）=ti，其中i=1，.，n. 它的更新是f [w1d1，.，wm <$→dm]，其中域可以扩大。我们用f s（f-s）表示f对s dom（f）（对dom（f）s）的限制。一对中的两个分量用*分隔。对S =a*b的定义默默地定义了对选择器s. a和s.b。G. Amato等人/理论计算机科学电子笔记322（2016）37∈ KJ.∈ K ∈ V∈ K∈ V2.1语言我们使用[15]中定义的类Java面向对象语言，它是Java的规范化版本，具有向下转换，我们使用上转换扩展2.1.1语法.每个程序都有一组变量（或标识符）V和一组有限的类（或类型）K，它们由子类关系≤排序，使得K*≤是偏序集。 的集合V包括特殊变量this、res、out。由于我们不允许多重继承，因此对于任何类κ∈ K，集合{κJ|kJ≥k}是一条链。类型环境是从有限的变量集到关联类的映射。类型环境集是TypEnv={τ：V → K| dom（τ）是有限的}。任何类别κ定义了一个类型环境F（κ），它将类κ的域（包括κ中定义的域和超类继承的域）映射到它们的类型。为了便于标记，我们要求场不能在子类中重新定义这意味着如果f∈domF（κ），且κJ≤κ，则f∈domF（κJ）且F（κ）（f）=F（κ）（f）例2.1对于1.1节中的程序例子，K={Tree，Tree}有一个最优排序。进一步证明了F（Tree）=[l <$→Tree，r<$→Tree]和F（Tree）=[].表达式和命令是Java表达式和命令的规范化版本我们要求所有类型转换都是显式的，这样在任何赋值中v：=exp的类型都是v和 经验一致。 对于形式参数和实际参数也是如此。 这不是一个限制，因为我们允许向上和向下转换。表达式和命令的语法为：exp：：= nullκ|新κ|v|v. F|（κ）v|v. m（v1， . ，vn）com：：= v：= exp|诉f：= exp| {com;···; com}| if v = w then com else com |if v = null then com else com其中k和 v，w，v1，.，当它们出现在同一分句中时，它们是不同的。每个方法κ。一个类κ的m用这样的语句定义，κ0m（w1：κ1， . ，wn：κn），其中wn+1：κn+1， . ，wn+m：κn+m是com其中w1， . ，wn，wn+1， . ，wn+m你是与众不同的，你既不是这样，也不是这样，也不是这样。它们的声明类型是κ1，...，κn，κn+1，...，κn+m。 该方法还可以使用κ 0类型的变量来保存其返回值。我们定义身体（κ。m）=com和returnType（κ. m）= κ0。8G. Amato等人/理论计算机科学电子笔记322（2016）3∈τ最终状态：C_）：com<$→（→）。τ τE<$）›→›→2.1.2语义语言的语义是通过框架、对象和记忆来定义的定义如下：帧τ={φ|φ∈dom（τ）›→Loc{null}}Obj={κ*φ|k∈ K，φ∈FrameF（k）}Memory ={μ ∈ Loc → Obj|dom（μ）是有限的}其中Loc是无限多个位置。框架将变量（标识符）绑定到位置或null。内存将这些位置绑定到对象，对象包含类标记和字段的框架。 类κ的新对象是new（κ）=κ *φ，其中对于每个vdom（F（κ））φ（v）= null。具有类型环境τ的可能状态的集合是φ τ={φ*μ|φ∈帧τ，μ∈存储器，φ *μ：τ}其中φ*μ：τ意味着φ*μ在类型环境τ中是良好类型的。例2.2设τ={v7<$→Tree，v8<$→Tree}，并考虑所描述的状态φ*μ图3中的我们有φ={v7<$→l0，v8l1}，μ={l0 Tree*{l<$→l2，r<$→l3}，l1 Tree*{l<$→l4，r<$→ null}，l2树*{l<$→null，r<$→ null}，l3<$→树*{l<$→null，r<$→l5}，l4<$→Tree*{l<$→l6，r<$→null}，l5→<$Tree*{l<$→null，r<$→l7}，l6树 *{l <$→ l7，r <$→ null}，l7<$→树 *{l <$→ null，r <$→null}}。表达式的表示是部分映射I_：exp（τ从初始状态到最终状态的表达式（ττ + exp），包含一个持有表达式值的变量res，其中τ+exp=τ[res typeτ（exp）]，类型τ（exp）是exp的静态类型。命令的表示是从初始到我τ每个方法κ。m由从输入到输出状态的部分函数表示，并且解释I将方法映射到状态上的部分函数，使得I（κ. m）：k输入（κ. m）→λscope（κ. m），具有类型环境：input（κ. m）=[this] → κ，w1 κ1，.，wn<$→κn]s co pe（κ. m）=输入（κ. m）[out<$]→κ0，w1Jwn+1<$→κn+1， . ，wn+m→››→κ1，.，wnJκn+ m]κn，其中w1J， . ..每个wiJ在开始时被分配给对应的wi的相同值G. Amato等人/理论计算机科学电子笔记322（2016）39方法的执行，并且以后永远不会更改。10G. Amato等人/理论计算机科学电子笔记322（2016）3∈∈∈∈∈∈∈∈例2.3考虑1.1节中的makeTree方法。 我们有这个输入（树。makeTree）=[this<$→ Tree，n<$→树]树（Tree）makeTree）= input（Tree. makeTree）[out<$→ Tree，nJ ，m<$→].3可达性、共享、线性和混叠我们在这里正式的概念，可达性，共享，线性和别名的对象。在后面的部分中，我们将使用这些概念来介绍新的抽象域ALP。下面的定义将在后面简化符号定 义 3.1 （ 位 置 域 ） 给 定 σ=φ * μπτ ， ldom （ μ ） ，f 是 一 个 标 识 符 ，f<$=f1， . ，f在一个可能为空的i个标识符的序列中，当它们存在时，我们写：• L. f对于μ（l）.φ（f），它是从l通过场f可达的位置;• L. f′代表l。f 1 fn;如果f′为空，则l。f′=l。现在我们引入一些符号来尽可能统一地处理变量和它们的场。定义3.2（合格场和标识符）给定一个类型环境τ，我们称合格场为对v。f其中vdom（τ）和fdom（F（τ（v），我们称限定恒等式为dom（τ）中的变量或限定场。我们用Qτ和Iτ分别表示合格场和标识符的集合。值得注意的是，我们只考虑变量声明类型中的字段，而不考虑实际类型中的字段。 这种选择虽然可能会降低分析的精度，但简化了抽象和具体语义之间的对应关系，并可能提高分析的速度例3.3在例2.2中，合格场为Qτ={v 7. 1，第7节。r，v 8. l，v 8。r}而合格的标识符是Iτ={v7，v8}<$Qτ。定义3.4（合格场的符号）如果σ= φ*μπτ且v。fQτ，为了变量的一致性，我们定义：• τ（v. f）= F（τ（v））（f），即，变量v的字段f的声明类型;• φ（v. f）= nullif φ（v）= null，φ（v. f）=φ（v）。f，否则，这是变量v中字段f所指向的位置。定义3.5（共享、线性和混叠）设στ和i1，i2Iτ。我们说：• 当φ（i1）/=null/=φ（i2）且re是ref<$1，f<$2时，i1和i2共享σ，使得φ（i1）. f<$1=φ（i2）。f'2null;• i1在σ中是非线性的，当φ（i1） 为零且re为ref<$1时，f′2使得φ（i1）.f<$1=φ（i1）. f<$2/=null;否则，i1被认为是线性的。G. Amato等人/理论计算机科学电子笔记322（2016）311∈∈• 当φ（i1）= φ（i2）时，i1和i2在σ中（弱）混叠.例3.6在例2.2之后，场v 7. R与V8共享。L. 因此，V7和V8共用. l和v8。第七场。l和v 8。r只与自己和各自的父母分享。所有的标识符都是线性的。在图3的例子中，我们有v 9。r和v10不是线性的。一个合格的标识符Iτ与自己共享，当且仅当它不为空。此外，使得φ（i）=null的每个i I τ都是线性的，并且不与任何其他标识符共享。必须注意的是，如果两个合格的标识符的静态类型不允许它们绑定到重叠的数据结构，那么它们可能永远无法共享。类似地，某些合格的标识符被迫是线性的。例3.7在1.1节的例子中，我们有一棵树不是一个树，一个树不是一棵树，它们没有任何可以共享的域。因此，任何Tree类型的标识符永远不能与任何Tree类型的标识符共享。此外，任何类型的标识符只能是线性的。我们用NL表示其实例可以是非线性的类的集合，用SH表示可以共享的类对的集合。NL和SH都可以仅通过键入信息来计算。4新抽象域在本节中，我们使用前面介绍的共享，线性和别名的概念来定义一个新的抽象域，称为ALP（AliasingL inearityP airs sharing），用于分析Java类程序。4.1混叠图我们首先定义一个基本的域，对定义的别名和定义的空值进行编码。定义4.1（预混叠图）类型环境τ上的预混叠图是有向图G=N * E *l，使得：• N是节点的集合;• EN× V×N是有向边的集合，每个边由一个标识符标记;• l：dom（τ）~N是从变量到节点的部分映射;附加条件是• <$n∈N，<$f ∈ V，最多有一条由f标记的n的出边，• <$n∈N， <$f∈ V，若 <$n，f，nJ<$∈E，则存在v ∈dom（τ）使得l（v）=n和v. f ∈Qτ。我们写n1−→fn2而不是n1，f，n2<$。当它是明确的从科恩文本，我们用N、E和l表示G.N、G.E和G.l。 此外，我们将Gi.N，Gi.E和Gi.l乘Ni，Ei，li，并且类似地对于G.12G. Amato等人/理论计算机科学电子笔记322（2016）3.联系我们∈⊥∈n∈N{τ（i）|i∈I<$l（i）=n}Gτττ τ（n）={τ（i）|i∈I<$τG−→∈≤⊥∈ G ∈≤F定义4.2（l的扩展）给定一个预混叠图G = N * E *l，我们在合格域v上扩展l。f∈Qτ，n如果l（v）= l（v）fl（v.f）=n∈E否则，预混叠图的思想是，给定一个标识符i Iτ，l（i）=意味着i定义为空，而l（i）=l（j）意味着i和j要么都为空，要么都是混叠的。这意味着要定义下面的前序。定义4.3（预混叠图上的给定G1，G2∈ Gτ，我们说G1 ≤G2i ∈Gτ，• 对每个i，IJ∈Iτ，l2（i）=l2（IJ）<$l1（i）=l1（IJ）;• 对每个i ∈ Iτ，l2（i）= l1（i）=.请注意，给定其预期含义，一些预混叠图包含冗余信息。例如，可以移除未被任何合格标识符标记的节点。相反，两个不可比较类型的标识符i1，i2只有在它们都为null时才可能是（弱）别名。因此，我们限制我们的注意力的预混叠图，提出了一些额外的正则性条件。定义4.4（别名图）别名图是一个预别名图G，使得对于所有的 ，是一个非空链。我们用类型环境上的别名图集表示，l（i）= n}的节点n的类型，并通过n ∈G（n）={τ（w）|w∈ dom（τ）<$l（w）= n}只能由变量推断的类型给定一个具体的状态σττ，我们可以把它抽象成一个传递相关信息的别名图。定义4.5给定σ=φ*μ∈Gτ，我们将σ的抽象定义为一个别名图αa（σ）=G∈ Gτ，其中• N={l ∈ Loc |i ∈ Iτ.φ（i）= l};• 对任意v∈dom（τ），当φ（v）/= null时，l（v）=φ（v），否则l（v）=φ（v）;• llJ∈ Ei <$i存在v ∈ dom（τ）使得l（v）= l，v. f∈ Qτ和l. f =lJ∈N我们说Gτ是σ的正确抽象τiG. 注意，如果αa（σ）G和l（i）=，则φ（i）= null，因此l实际上可以用来表示定义的零性。此外，如果l（i1）= l（i2），则φ（i1）= φ（i2）Loc或φ（i1）= φ（i2）= null。因此，l实际上编码了变量之间的定义弱混叠。.G. Amato等人/理论计算机科学电子笔记322（2016）313- -∈∈{} ∈∈{} ∈∈f14.2ALP图别名图是程序状态的一部分的非常具体的表示，它可以通过单个字段访问从变量到达。相反，对共享和线性概括了状态的全局属性我们希望向别名图添加可能的共享和可能的非线性信息定义4.6（预ALPs图）预ALPs图G=G *sh*nl是具有集合sh {{n，m}的预混叠图G。|n，m ∈ N}和一个集合nl <$N.当上下文清楚时，我们表示G.G，G。sh，G. nl乘G，sh，nl和我，我，我。sh，Gi. nlbyGi，shi，nli.类似地，对于G.前ALP图中的集合sh编码可能的对共享，而nl编码可能的非线性。特别地，当l（i），l（j）sh，而i可以是非线性的，当l（i）nl. 这建议将别名图上的前序扩展到ALP图，如下所示：命题4.7（pre-ALP图的预排序）Pre-ALP图通过G1≤ G2且I ∈ Iτ. l1（i）∈ nl 1<$l2（i）∈ nl 2，i，j∈Iτ。 {l1（i），l1（j）}∈s h1<${l2（i），l2（j）}∈s h2。由于混叠、非线性和共享相互作用的方式，并非所有的前ALP图都有意义。特别地，一些共享和非线性信息可以由其他信息导出。 例如，如果n是G中的一个节点，则n应该在sh中，否则任何标识符都是s. t。l（i）=n被强制为空，并且G可以通过删除节点n来简化。其他非线性或共享信息是冗余的，因为由于所考虑的类层次结构，它在实践中不可能发生：对n，msh使得类τG（n）和τG（m）不能共享，或者变量nnl使得τG（n）/NL。我们想把注意力限制在那些显式地显示所有隐含和冗余信息的前ALP定义4.8（ALPs图） ALPs图G是一个准 ALPs图，其中• G是一个混叠图;• 【详细】|n ∈ N} n;• 若G中存在涉及n的非空回路，则n∈nl;• 若{n，m} ∈sh，则（τG（n），τG（m））∈SH;• 若n∈nl，则τG（n）∈NL;• cl G（sh * nl）= sh * nl。这里，clG（sh，nl）是在分量排序下的最小对shJ*nlJ，使得• {n，m}∈shJ<$nJ−→fn<${nJ，m}∈sh J;F2• n-→m1，n-→m2，f1/=f2，{m1，m2}∈shj<$n∈NLJ;14G. Amato等人/理论计算机科学电子笔记322（2016）3∈∈∈∈α α：α（S）→ALPα（S）=τ τ{∈|联系我们τ• n∈nlJ<$nJ−→fn<$nJ∈nlJ。我们用ALP τ表示类型环境τ上的ALP图的集合。给定一个具体的状态σττ，我们可以把它抽象成一个传递相关信息的别名图。定义4.9（ALP图上的抽象映射）给定σ=φ * μπτ，我们将σ的抽象定义为α（σ）=αa（σ）*sh*nl，其中sh={{l1，l2}<$N|L1和L2共享σ}，nl ={l∈N| l在σ中不是线性的。当α（σ）≤ G时，称G是σ的正确抽象.设σ=φ*μ，α（σ）≤G，若i1，i2∈Iτ分担σ，则{l（i1），l（i2）}∈sh.此外，如果i Iτ在σ中是非线性的，则l（i）nl。因此，G实际上编码了变量之间可能的共享和非线性。命题4.10 ALP图的预序集有最小元素T，最大元素T，lub Y和glb Ω。我们可以定义一个具体化映射γ：ALPsτ→α（γτ），它将别名图映射到它们表示为γ（G）=σΣτα（σ）G.如果我们举起地图在定义4.9中，将一个可加映射转化为σ∈Sα（σ），则α和γ构成Galois联络.5一个抽象的ALPs语义。给出了域ALPτ上的抽象语义。我们为标准语义中的每个具体操作符提供了正确的抽象对应物。解释的绝对对应物是ALP解释，定义如下。定义5.1ALP解释I将方法映射到全函数，使得I（κ. m）：ALP输入（κ. 米）的ALP范围（κ. m）对于每个方法κ。M.5.1表达式的抽象表示表达式和命令的抽象表示是根据它们的语法组成的。定义5.2令τ描述作用域中的变量，I是ALP解释。图7定义了表达式（方法调用除外）的ALP表示：exp<$→（ALPτALP sτ+exp）。我们简要地解释了抽象语义算子相对于相应的具体语义算子的行为。 null κ的具体语义将null存储在变量res中。因此，在抽象语义中，我们只需要在类型环境中添加新的变量res，而不需要修改抽象状态。new κ的具体语义在res中存储了对新对象o的引用，其字段为null。 其他变量不变。因为o只能从G. Amato等人/理论计算机科学电子笔记322（2016）315（000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000⎧⎨我⎨ττSE（Ⅲ）τ我我IG）=GIG）=N{nnew}El[res<$→nnew]sh{{nnew}}nl（000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000G）=NEl[res<$→l（v）]shnl（（1）（1）（）=的B.G.⎩如果τ（l（v））<${κ}不是链如果l（v）=1SEv. f）（）=1000000⎩如果l（v）=1如果我（v. f）=0见图7。 ALP对表达式的解释。res，变量res仅与其自身共享，并且明显是线性的。因此，我们只需要添加一个标记为res的新节点，而不需要删除共享或非线性信息。v的具体语义只是使res成为v的别名。 由于v和res的类型一致，我们只需要将变量v添加到res的同一节点。其 他 变量不变。当它被定义时，cast（κ）v将v的值存储在res中。当l（v）不为空时，我们使用一个辅助算子add（G，n，κ），它将标签res添加到节点l（v），并可能为不是v的域的res域添加新节点。在这种情况下，我们可以利用线性的概念事实上，当v是线性的时，我们知道res的场不能彼此共享，并且是线性的。v的具体语义。f在res中存储v的场f的值，前提是v不为空。 当v f不为空，这基本上相当于前面情况的相同5.2命令的抽象表示定 义 5.3 让 τ 描 述作 用 域 中的 变 量 ， I 是 一个 ALP 解 释。 图 8 显 示 了 命令SCI<$_）：com<$→（ALPτ <$→）的ALP表示ALPs τ）。v：=exp的具体语义计算exp并将其结果存储到v中。因此，最终的抽象状态是通过首先计算Iexp，然后将res重命名为v来获得的。某些节点可能会变成未标记的节点，必须将其删除。 这是通过辅助操作prune来完成的，该操作删除不必要的信息，特别是未标记的节点和不在变量声明类型中的字段。V的评价。f：=exp是抽象语义中最复杂的运算，因为我们必须考虑到v可能别名为许多不同的节点。候选变量是那些与l（v）共享并具有兼容类型的变量，用Vcomp表示对于Vcomp中的每个变量标记的节点，我们在Nnew中添加一个新的新鲜节点，该节点由Enew中的边（由字段f标记）指向。最后，添加所有可能的共享和非线性对于 表达式的结果定义为空的特殊情况，我们做了稍微不同的处理。add（G，l（v），κ）否则add（G，l（v. f），τ（v.（f）其他GG16G. Amato等人/理论计算机科学电子笔记322（2016）3τSCv. f：=exp）（x我们的团队|{\fn方正粗倩简体\fs12\b1\bord1\shad1\3cH2F2F2F}ττ⊥}⎪⎩sh′什新山nl ′newn′（x）n'（x）Nnew，l'（x. （f）nl′））否则.{{n}}{n′} |n∈Nnew，{l′（x. f），n′} ∈s h′}<${{n<$'（x），n<$'（y）} |n∈N（x），n∈N（y）τSCI<$v：=exp）（G）=prune（（N′E′l′[v<$→l′（res），res<$→n]）sh′nl′）⎧⎪⊥“如果l”（v）=“”cl（prune（（N⎪Nnew我的天s h′s hnewnl ′{n'（x）|n∈Nnew，l′（x. f）∈nl′}））G）=cl（prune（（N′⎪如果l′（v）/=π且l′（res）=πNnew如果v= null，则SCI1（G）=2.SCI<$cm1）（G）如果l（v）=lτττthencomelsecomSCI<$com1）（G|v=nul l）YSCI<$cm2）（G）否则SCI如果v=w我（G）=.SCI<$cm1）（G）如果l（v）=l（w）ττ我我τ然后comelsecomSCI<$com1）（G|v=w）YSCI<$cm2）（G）否则SC{com1;.. . ;comp}）=（λs∈ALPsτ.s）ΔSCτcomp）Δ· · ·ΔSCτcom1）其中G′=SEI（exp）（G），Vcomp={x∈dom（τ）|l′（x） l′（v），{x，v}∈sh′，{τG'（l′（x）），τG'（l′（v）}是链}Nnew={n n='（x）|x∈Vcom p，f∈dom（F（G′（l′（x），l′（x. f）/=l′（res）}新的不同维数Edel ={l′（v）−→fl′（v.f）} <${l′（x）−→fl′（x. f）∈E′|x∈ Vcomp}Enew={l′（x）−→fn'|x∈Vcom p，n'∈Nnew}（x）s hnew={{n'（x），n′} |n∈Nnew，{l′（x. f），n′} ∈sh′}联系我们_联系我 们 |n∈Nnew，{l′（x. f），l′（y. f）} ∈sh}恩纽 =E新{l′（v）−→fl′（res）}s h′new={{n，n′} |{l′（v），n} ∈sh′和{l′（res），n′} ∈s h′}{{n}}{n′} |nn∈'（x）∈Nne w，{l′（res），n′} ∈s h′}nnl′new={n∈N′|{n，l′（v）} ∈sh′} <${n <$'（x）|nn∈'（x）∈Nne w}如果{res，v} ∈s h′或res∈nl ′{n∈N′|{n，l′（v）}∈sh ′，{res，n}∈ sh′}否则见图8。 命令的ALP解释类似的情况也出现在[14]中。为了确定条件“如果v = null“的正确近似， 我 们 检 查 l （ v ） 是 否= 。如果是这种情况，那么我们知道v为null，我们计算com1。否则，我们计算两个分支并计算lub。当评估第一个bran ch时，我们可以通过使用辅助运算器G来提高精度|v=null，返回程序状态{φ * μ}的正确近似值|α（φ * μ）≤Gφ（v）=null，即，这些状态被G正确地近似，其中v为零。类似地，对于条件“if v =w“，其中我们使用另一个辅助运算符G|返 回 程序状态集合{φ*μ}的正确近 似 |α（φ*μ）≤ G <$φ（v）= φ（w）}。 用ALPs上的函数复合来表示命令的复合，其中当p=0时需要恒等映射λs ∈ ALPsτ.s.5.3方法调用当一个方法V。m被调用，检查v的类，并为m选择正确的重载方法抽象域只包含v的运行时类的部分信息，因为我们只知道v的类必须小于与v混叠的任何变量的类，即小于τG（l（v））。我们在计算图9中的方法调用的抽象语义时利用了这12G. Amato等人/理论计算机科学电子笔记322（2016）317些信息。在实践中，我们保守地假设τG（l（v））的任何子类中的每个方法m18G. Amato等人/理论计算机科学电子笔记322（2016）3τGJ输入（κ. 米）的联系我们SEIv. m（v1， . ，vn））（G）=.⊥Y{matchv. m（G，I（ κ.m）（G′如果l（v）=1）的情况）|K≤τG（l（v））}，否则其中l输入= [this <$→l（v），w1<$→ l（v1），.， wn l（vn）}]和G′ = prune（N E linputsh nl）.见图9。 方法的ALP解释可以被称为。请注意，仅在κ的超类中定义的方法已经在κ中被考虑。当退出方法调用时，我们需要将out重命名为res，因为从调用者的角度来看，被调用者的返回值（out）是方法调用表达式（res）的值。 我们将使用一个辅助操作match，它在给定初始状态和最终状态的情况下，更新初始状态，试图猜测抽象状态中变量的可能匹配。定理5.4图7、图8和图9中的抽象表示是正确的。此外，在给定ALP解释I的情况下，ALP解释上的Transformer返回新的ALP解释IJ，使得我scope（κ.米）的体（κ. m））n（λ∈ALPs.N *E*l*sh*nl）是c或rect，其中relJ=l[w1Jl（w1）， .，wnJl（wn）]。抽象指称语义是这个Transformer的最小定点，它是正确的。在[15]中使用的具体指称语义例5.5考虑Tree方法。1.1节中的makeTree，其中树（Tree）makeTree）=[this<$→Tree，n<$$> →树，nJ<$<$→树，m ›→树，out ›→树]。根据定理5.4，我们可以从最小信息ALPs中计算一个新的ALPs解释I（Tree.makeTree）=λG. 树（Tree）makeTree）：1、树。makeTree）（G）=N{nm，nout}* E*l[nJ<$$> →l（n），out<$→nout，m<$→nm]*shshJ*nl其中，如果l（n）=，则shJ=，否则sh j= nm，l（n）。 现在，从1、树。makeTree），我们可以计算一个新的解释如下：2、树。makeTree）（G）=N<${nm，nout，nout.l，nout.r，}* E*l[nJ<$→l（n），out<$→nout，out.l<$→nout.l，out.r<$→nout.r，m<$→nm]*shshJ{{nout，nout.l}，{nout，nout.r}}*nl这是最小的固定点。 相对于l（n）/= null的情况，抽象状态IJ（κ. m）=SCG. Amato等人/理论计算机科学电子笔记322（2016）3191、树。makeTree）（G）和I2（Tree. makeTree）（G）的计算结果如图10所示。20G. Amato等人/理论计算机科学电子笔记322（2016）3n，n(a)第一次迭代。（b）第二次迭代。图10. makeTree方法的ALP解释6结论本文提出了一种新的抽象域ALP，它结合了面向对象语言的别名、线性和共享分析，并提供了所有必要的抽象操作。我们在SEC展示。1.1一个简单的例子，其中线性在证明两个子树不共享中起着重要作用面向对象语言的共享属性已经在一些工作中进行了研究，而它在逻辑编程的背景下进行了深入研究，通常与线性分析相结合。据我们所知，这是第一次尝试将Java程序的共享与线性结合起来。我们还计划将ALP实现为Jandom静态分析器的抽象域[1]。在[15]中，作者提出了一个简单的（对）共享域在[13]中，作者扩展了这个领域，提出了（集）共享，空性和类的组合分析。本文的主要内容是：这些建议包括：• 除了对共享之外，ALP• 信息是在环境中的变量所指向的对象的字段级别上编码的，而不仅仅是在变量级别上。在[14]中，作者提出了一个分析面向对象语言的框架这些域的对象类似于别名图，但不限于两个级别。通过加宽来保证终止。这些域可以通过为图的叶子提供类型信息来丰富。但是，它们不考虑共享或线性特性。与线性信息的结合使我们能够提高赋值块、方法调用以及递归的分析精度这是一个根本性问题，在以前的任何分析中都没有考虑到事实上，重要的一点是线性信息允许我们区分树和DAG（直接无环图）。例如，图5中makeTree的结果是一棵树。然而，在任何抽象域中的树的抽象表示仅包含关于可达性、共享性、无环性、空性、独特性和别名的信息，不能与DAG的抽象区分开来。例如，数据结构t2：Tree（）t2 =new Tree（）t2。l =new Tree（）t