没有合适的资源?快使用搜索试试~ 我知道了~
属性文法中的优化验证数据流分析
理论计算机科学电子笔记176(2007)109-122www.elsevier.com/locate/entcs在属性文法中使用基于验证数据流分析的优化1Eric Van Wyk和Lijesh Krishnan2明尼苏达大学计算机科学与工程系摘要构建经过验证的编译器是困难的,特别是当必须执行类型检查或数据流分析等复杂分析时。类型检查和程序优化社区都开发了证明这些过程正确性的方法,并开发了分别使用验证类型系统和验证优化的工具。然而,在单个声明性框架中使用这两种分析是困难的,因为这些过程在不同的程序表示上工作:对抽象语法树的类型检查和对控制流或程序依赖图的基于数据流分析的优化。我们提出了一种属性文法规范化语言,该语言已经扩展了用于规范化属性标记控制流图的结构以及指定数据流分析的CTL和LTL-FV公式。这些公式在这些图上进行模型检查,以执行特定分析。 因此,已验证的类型规则和已验证的数据-流程分析(通过手工或自动证明工具进行验证)都可以转录成基于属性语法的单个声明性框架,以构建高置信度的语言实现。此外,属性语法规范语言是可扩展的,因此可以相对直接地为不同的时态逻辑添加新的构造,从而可以使用替代逻辑和模型检查器来指定该框架中的数据流分析关键词:编译器优化,优化验证,数据流分析,属性文法,模型检测,时态逻辑1介绍构建经过验证的或高保证的编译器是一项具有挑战性的任务;当必须执行复杂的程序分析以支持类型检查或基于数据流分析的优化时,这尤其困难,并且经常超出当前自动证明技术的能力。这些分析通常需要精确理解程序构造相互作用的微妙方式,因此即使在声明式框架中,也很难定义它们。类型理论和程序1 该研究部分由NSF CAREER Award #0347860,NSF CCF Award #0429640和麦克奈特基金会2 电子邮件:Van Wyk -evw@cs.umn.edu,Krishnan -krishnan@cs.umn.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2006.06.020110E. 凡威克湖Krishnan/Electronic Notes in Theoretical Computer Science 176(2007)109优化团体已经通过开发技术来证明它们各自的程序分析的正确性来解决这个问题要构建一个经过验证的编译器,必须编写一个编译器的规范,该规范涉及语言的所有方面,并且适合于生成正确性证明的各种分析。这方面的一个障碍是,编译器的不同方面使用不同的程序表示的不同符号来更自然地定义。例如,类型检查通常是另一方面,优化转换通常被编写为具有基于数据流分析的边条件的重写规则,并且执行数据流分析并证明其正确性与控制流图或依赖图程序表示紧密耦合。在类型检查的情况下,用于证明类型系统的可靠性(安全性)的类型规则遵循程序的抽象语法结构。因此,它们可以很容易地转录成基于属性语法的实现,从而为我们提供了高度的信心,即实现是正确的。考虑图1(a)中所示的简单类型lambda演算中函数抽象的类型规则(摘自[16Γ是将变量名映射到类型的环境。该规则指出,如果用x到类型T1的映射扩展Γ确保了项t2具有类型T2,则在环境Γ中,λx:T1.t2具有类型T1→T2 例如,如果Γ映射变量y对于类型Int,上述规则将表明表达式λx:Int.y+x具有类型Int->Int。规则(T-ABS)可以转录到Abs产生式上,用于图1(b)中所示的函数抽象。在这里,一个继承的属性env扮演了Γ的角色。EVDA表达式主体t2的环境是由envAdd扩展的EVDA表达式t(t.env)的环境,其中具有从x到类型T1的映射。t2使用其env属性来计算其type属性,然后使用该type属性来使用函数funcType为项t创建函数类型。r,x:T1t2:T2Γλx:T1.t2:T1→T2(T-ABS)生产Abst::Expr::= x::Id T1::Type t2::Expr t.type = funcType(T1,t2.type); t2.env = envAdd((x,T1),t.env);(a)(b)第(1)款Fig. 1. 类型规则(a)和属性语法实现(b)。s:v:=e跳过如果S| = AX<$E [真实U使用(v)]生产分配s::Stmt::= v::Id e::Expr s.isdead = s|AX!E[ trueU v in uses];s.uses= e.uses;(a)(b)第(1)款图二. 优化重写规则(a)和属性语法实现(b)。因此,属性语法(AG)为实现具有复杂分析(如类型检查)的语言提供了一个有吸引力的框架,因为它们提供了一个高级的E. 凡威克湖Krishnan/Electronic Notes in Theoretical Computer Science 176(2007)109111用于指定语言的语法导向语义的声明性框架。重要的是,实现可以从AG规范自动生成。我们也想把经过验证的优化,比如图2(a)中简单的该规则规定,如果s满足所示的CTL属性,则控制流程图节点s上的赋值语句v:=e可以由skip语句替换。如果在s的所有后继者上,不存在使用变量v的路径,则满足该性质。也就是说,v在未来的计算中不使用。我们在早期的论文[12]中验证了这个规则的正确性(注意,我们假设表达式没有边项)。我们可能想在属性语法中使用这种经过验证的优化来将某些赋值标记为死。要做到这一点,我们想写一个生产一样,在图。第2段(b)分段。在这里,isdead是一个布尔值的attribute anduses是一个属性,其中包含声明。当然,while循环和if-then-else语句的语句和条件必须在控制流或程序依赖图中连接,以使模型检查器能够检查此公式是否适用于特定的赋值语句。这一点在图中没有显示,但在SEC中显示。3.1.本文的主要贡献是展示如何属性文法规范语言可以扩展到允许语义分析的基础上的控制流程图的程序。特别感兴趣的是用于命令式程序的验证优化的数据流分析。我们提出了一个属性语法规范语言的扩展,称为银(见第二节)。2),包括用于构建标记控制流程图的结构,以及分别使用NuSMV [4]和支持自由变量的手工构建的LTL-FV模型检查器(Sec. 2)使用CTL和LTL-FV时序逻辑公式对这些图进行模型检查。3)。因此,在一个声明性的形式主义中,基于语法树和基于控制流图的分析都可以声明性地指定。这是非常有用的,因为这两种类型的分析都需要构建高效的高置信度编译器。一这项工作的显着特点是,银被设计为一个可扩展的语言,因此编写Silver的附加扩展以使用不同的时态逻辑和模型检查器来进行数据流分析是一个简单的过程(参见第4). (Note我们还没有建立能够读取Silver规格并证明其正确性的工具,尽管这是一个有前途的研究方向秒第5段讨论了今后的工作和相关工作,并作出结论。2属性语法和银在本节中,我们通过指定本文示例中使用的C的一个小子集(称为C−)来简要介绍我们的属性语法指定语言Silver。一个简单的C−程序如图3(a)所示。这里介绍这样一个小语言,以便提供一个相对完整的规范。3 放大图片作者:Van Wyk和David Lacey,Neil D.琼斯和卡尔·弗雷德里克森。112E. 凡威克湖Krishnan/Electronic Notes in Theoretical Computer Science 176(2007)109说明Silver和数据流分析扩展的详细信息,可以在可用空间中进行描述。int n =0;2 b =1;3 c = 3;如果(a== 1),则为45 b =5;其他6 b =2;7 while(b == 3)8 a = a +1;}(a)(b)第(1)款图3.第三章。C程序(a)及其AST和控制流程图(b)属性语法[9]通过将值(称为属性)与程序的抽象语法树(AST)中的节点相因此,非终结符用属性修饰,而产生式与定义属性值的语义函数相关联。C−的部分银规范如图所示:见图4。它定义了4个非终结符:AST根(Root)、语句列表(Stmts)、语句(Stmt)和表达式(Expr),以及标识符(Id)的单个终结符。pretty-print属性(pp)存储结构的文本表示,具有String类型,并出现在所有非终结符上。def属性的类型为String,存储由assign状态定义的标识符的名称,或者存储空字符串以指示没有定义变量,就像skip和expressions一样。属性使用的是一个字符串列表,其中包含表达式或语句引用的变量的名称,因此出现在Expr和Stmt非终结符上。产生式定义了C−的抽象语法。4它们指定了产品名称及其签名,该签名具有命名的非端子和端子符号。康-分配产生式(assignproduction)定义分配语句。它定义了名为s的Stmt节点上的pretty-print属性,该属性由标识符终端(标识符的名称)的词素(lex)和表达式e的pretty-print属性组成它将def定义为标识符其他的产品和属性定义应该是不言自明的。这里的所有属性都是合成属性,用于传播(合成)信息,使AST上升。在后面的章节中,我们定义了一些继承的属性,这些属性将信息从parent传递到子节点;这些属性通常用于将环境传递到树。[4]为了本文的目的,我们可以假设具体的语法是使用传统的解析器和扫描器生成器定义的。根seq1seq2seq3seq如果而45678号出口E. 凡威克湖Krishnan/Electronic Notes in Theoretical Computer Science 176(2007)109113非终结符根,Stmt,Stmts,Expr;终端ID;合成属性pp::String出现在{Root,Stmt,Stmts,Expr}上;合成属性def:: String出现在{Stmt,Expr}上;合成属性使用::StringList发生在{Stmt,Expr};生产根目录r::Root::= s::Stmtsr.pp=“{\n”++s.pp++“\n}\n”;生产stmt_consstmts::Stmts::= s::Stmtss::Stmts stmts.pp=s.pp++“\n”++ss.pp;production stmt_onestmts::Stmts::= s::Stmt stmts.pp= s.pp;生产if_then_elsei::Stmt::= c::Expr t::Stmt e::Stmti.pp =“if(“++ c.pp ++.生产边w::Stmt::= cond::Exprbody::Stmt w.pp =“while(“++ cond.pp.生产分配s::Stmt::= v::Id e::Exprs.pp = v.lex++"="++e.pp++“;";s.def =v.lex;s.uses= e.uses;生产跳过s::Stmt::=s.def=“”;s.usesreturn new String();生产平等e::Expr::= l::Exprr::Expr e.def=“";e.uses= append_str_list(l.uses,r.uses);生产var_refe::Expr::=v::Ide.def=“";即uses= cons_str_list(v.lex,public void run();见图4。 Silver中C−的3基于属性文法模型检测的DFA在本节中,我们将描述Silver的扩展,这些扩展允许基于控制流图的分析(特别是数据流分析)的声明性规范。这些扩展允许编写数据流分析的时序逻辑规范,并调用模型检查器来执行指定的分析。节中在图3.1中,我们展示了用于构建控制流图(CFG)并指定哪些属性标记其节点的Silver扩展。节中3.2我们描述了Sil- ver的CTL扩展,它从CFG生成NuSMV模型,并允许使用NuSMV模型检查器指定和检查CTL公式。节中3.3我们对自由变量扩展的LTL及其模型检查器的实现做了同样的事情。节中4.描述了如何实现执行CTL和LTL-FV模型检查的Silver扩展。3.1Silver中的建筑控制流程图Silver的第一个扩展允许人们轻松地指定如何构建控制流程图以及哪些属性标记其节点。这种扩展语言在图5中用于定义C程序的控制流程图。该规范的第一行表示AST中的一些Stmt和Expr节点可以用作CFG中的节点。CFG被指定为一组独特的控制流边缘覆盖AST中的特定节点。在C−中,if-then-else语句和while循环中的赋值语句节点、跳过语句节点和条件表达式节点都是CFG中的节点为了构建CFG,我们编写了额外的产品,称为“方面产品”,将额外属性的定义添加到现有产品中 这些产生式定义了在Stmt和Stmts节点上出现的CFG节点类型的合成属性条目。 这是在-114E. 凡威克湖Krishnan/Electronic Notes in Theoretical Computer Science 176(2007)109cfg节点Stmt,Expr;cfg属性def,使用;合成属性条目::CFG_node发生在{Stmt,Stmts}上;继承的属性succ::CFG_node出现在{Stmt,Stmts}上;aspect production stmt_consstmts::Stmts::= s::Stmtss::Stmtsstmts.entry= s.entry;s.succ= ss.entry;ss.succ= stmts.succ;方面生产分配s::Stmt::= v::Id e::Exprs.entry= cfg s [s.succ];方面生产if_then_else s::Stmt::= c::Expr t::Stmte::Stmts.entry= cfg cond [t.entry,e.entry];t.succ= s.succ;e.succ= s.succ;方面生产跳过s::Stmt::=s.entry= cfg s [s.succ];图五. 调用构造C-规范tribute表示CFG中的入口节点。在根产生式上,所有从stmts.entry属性可到达的节点都将是程序的CFG中的节点。为了构造entry属性的值,我们使用构造CFG后续节点的cfg继承的属性succ在CFG中为构造定义后继者。图5示出了指定CFG节点的一些产生式的示例。例如,if-then-else的CFG的入口节点是条件表达式cond,其后继是then和else语句的入口节点。该构建体可以被解释为将指定的AST节点标记为也是CFG中的节点。图3(a)中C−程序的AST示例如图3(b)所示,CFG边缘由虚线表示。没有源的边指示节点1是入口节点,并且还创建了特殊的出口节点。 条件是方框,语句是圆圈。我们还需要指出哪些属性将用于标记CFG的节点 这是必要的,因为我们实际上不会对CFG进行模型检查,而是生成它的表示以提供给NuSMV和LTL-FV模型检查器。这是使用cfg属性构造完成的在图5的例子中,我们我已经指定了def,并使用图4中的属性作为CFG属性,因为它们被用在数据流属性中,作为Secs中的示例。3.2和3.3。所有声明为CFG节点的节点(本例中为Stmt和Expr)都必须定义这些CFG属性。3.2使用NuSMV检查CFG上的CTL属性在本节中,我们将描述扩展Silver的构造,这些构造允许在CFG上检查CTL公式,并从实际检查公式的CFG构造NuSMV模型。像NuSMV这样的有限状态模型检查器要求模型指定给出所有状态变量的有限域。在我们的示例中,对应于CFG属性def和uses的NuSMV状态变量的域分别是程序中所有变量的集合以及该集合的幂集。这些集合是使用合成属性all vars(未显示)构造的;在根节点上,它的值是程序中所有变量的集合因为这些信息E. 凡威克湖Krishnan/Electronic Notes in Theoretical Computer Science 176(2007)109115继承的属性smv_model::SMV_Model发生在{Stmts,Stmt}上;方面生产根r::Root::= stmts::Stmtstmts.smv_model= smvmodelstmts.entry[def在r.all_vars上的范围,使用r.all_vars的幂集上的范围];合成属性opt_stmt::Stmt发生在Stmt上;合成属性opt_stmts:: Stmts发生在Stmts上;方面生产分配s::Stmt::= v::Id e::Expr s.opt_stmt =if s.smv_model,s.entry |=AX A [!(v.lex in uses)W(def == v.lex&&!(v.lex inuses))]then skip() else s;方面生产stmt_cons stmts::Stmts::= s::Stmt ss::Stmts stmts.opt_stmts= stmt_cons(s.opt_stmt,ss.opt_stmts);见图6。 使用CTL和NuSMV进行基于DFA的优化。需要时,在AST的根上构造CFG的NuSMV表示。这个属性及其在根上的定义如图6所示。构造smvmodelCFG入口节点用于构造NuSMV模型。 建设模型,它收集给定CFG节点的所有后继节点,并使用给定的属性范围来装饰CFG节点。cfg attributes构造指定的每个CFG节点属性都需要一个范围,在本例中为def和uses。(A)出口节点上的自循环也根据CTL的语义的要求添加,所有国家至少有一个继承国。在根上定义的继承属性smv模型(一些定义未显示)被传递到所有AST节点,以便它可以用于进行数据流分析。作为基于数据流分析的优化的一个例子,我们展示了如何(即时)死代码分析的分配生产是用来确定是否分配应改为跳过语句。合成的高阶[22]属性opt stmt和opt stmts用于构造优化程序。在根产生式中,opt stmts属性(在s::Stmts上)的值是表示优化程序的树。要确定opt stmt是否设置为skip或原始赋值语句,赋值产生式调用具有CTL中指定的属性的模型检查器。模型检查表达式的语法是M,s|其中M是模型,s是状态,f是公式。此表达式具有布尔类型。在图6中的赋值产生式上使用该构造时,模型M是继承的属性smv模型。 状态s是分配s的CFG节点。 属性f是CTL公式,它声明在所有路径(A)上,在从分配CFG节点开始的所有下一个(AX)状态上,v的 这里W是弱直到算子,与强直到算子联合与pUq不同,pWq在路径上为真,只要p始终为真,即使q永远不为真。 因此,如果v的词素从未出现在uses中,则f中的until子句为真。 因此f(正确地)标记一个变量定义为死的,如果它的赋值从未被使用。这个公式在图3(b)中编号为2和3的节点上是满足的。请注意,这个公式与第2节中的公式不同。1;这一个发现更多的死赋值语句,但也可以被验证。为了准确理解CTL公式是如何进行模型检查的,我们注意到,116E. 凡威克湖Krishnan/Electronic Notes in Theoretical Computer Science 176(2007)109对于程序中的每个赋值语句,模型检查器将以相同的模型但以不同的CTL公式被调用。公式是由属性值构造的,如v.lex。对于语句b =1;在图3中,构造的CTL公式为AXA [!(bin uses)W(def == b&&!(b在使用中)]在将该公式传递给NuSMV进行检查之前,将其转换为NuSMV表示。 因为属性def和uses没有绑定到在AST节点上,它们不会被实例化,并且它们在CFG节点上的值在模型检查期间使用。3.3检查CFG在本节中,我们将介绍Silver的第二个扩展,它通过模型检查执行DFA在这种情况下,时态逻辑是LTL-FV [10],LTL的一个版本扩展了自由变量。自由变量类似于Lacey和de Moor [11]添加到 CTL的自由变量,并用于我们的优化正确性证明[12,13]。这些逻辑的模型检查器不是返回满足模型的状态集,而是返回满足公式的自由变量的节点和替换集。对于本节中的示例LTL-FV公式,这组替换指定了所有(立即)死赋值语句。因此,模型检查器只对模型调用一次,而不是像第二节那样对每个赋值调用一次3.2.因此,模型的创建和模型检查器的调用都是在C −的根产生式上完成的。方面生产根r::Root::= stmts::Stmtsr.ltlfv_model= ltlfvmodel stmts.entry;stmts.deadResults= modelcheck r.ltlfv_model其中(def== x)&&X((!x in usesU(def== x!&&x in uses))|| 克!(x inuses)),其中[x ranging overr.all_vars];在 上面 的 产品 中 ,LTL-FV 模 型检 查 器的 模 型是 以 类 似于CTL 情 况的 方 式从stmts.entry创建的。属性deadResults被分配了一组替换,这些替换是通过使用死代码公式(本质上是上述CTL版本的LTL-FV版本)检查模型而产生的在图3中的示例C−程序的情况下,该集合是{(2, [x<$→b]),(3, [x<$→c])} LTL-FV模型检查器是有限状态,如NuSMV,因此要生成有限状态模型我们在公式中为自由变量指定了一组可能的值这里,r.allvars和前面一样,是所有变量的集合。模型检查器的结果(本例中为stmts.deadResults)作为继承属性传递给需要结果的产品前-tension提供了一个构造来检查特定的替换是否满足特定节点上的公式。此构造的语法为检查检查CFG节点上的替换项的搜索结果因此,为了知道一个赋值是否是死的,我们检查这个公式在赋值产生式的节点上是否满足,用v.lex代替x。方面生产分配s::Stmt::= v::Id e::Exprs.opt_stmt=if check s.deadResults for [x mapsto v.lex] on s.entrythen skip()else s;E. 凡威克湖Krishnan/Electronic Notes in Theoretical Computer Science 176(2007)109117在图3中程序的AST节点2上,将找到替换(2, [x<$→b]),并且检查将返回真,然后像以前一样创建优化语句。我们可以在根产生式上对多个公式进行模型检查,并通过多个继承的结果属性将结果传递给适当的节点。4实施Silver DFA扩展这项工作的一个显着特点是Silver是作为一种可扩展语言设计和构建的。因此,它可以很容易地扩展新的语言结构和语义分析这些结构。上面我们介绍了允许Silver基于两个不同的时态逻辑执行数据流分析的扩展。使用其他逻辑和模型检查器的扩展也可以直接添加。Silver属性语法规范是通过将它们转换为Haskell代码来实现的。这个Silver-to-Haskell转换器是作为一个用Silver编写的属性gram- mar实现的(对Silver的一个很好的测试是为它自己编写一个编译器。属性语法的声明性、模块化和可扩展性是实现对Silver [21]的DFA扩展要向Silver添加新的语言构造,需要添加新的产生式来定义它们的具体和抽象语法,并为Silver的抽象语法中标记非终结符的属性添加属性定义。定义CFG和DFA构造的抽象语法的产生式还指定了这些构造如何转换为用纯的、非扩展的Silver编写的属性语法规范例如,模型检查构造(|=和modelcheck)都转换为调用适当模型检查器的Silver“系统”调用。要构建适当的模型表示,每个扩展还为CFG扩展中的CFG构建产生式编写方面产生式;这些方面产生式具有指定CFG到NuSMV或LTL-FV模型语言的翻译的属性。Silver的属性语法规范和定义CFG、CTL和LTL-FV扩展的属性语法片段都被组合在一起,以创建一个扩展Silver的规范,该规范处理第2节和第3节中给出的C−规范。 事实上,CTL和LTL-FV模型检查都可以用于一个单一的编程语言规范,如果两种类型的逻辑DFA是必要的。DFA扩展结构到纯Silver的转换利用了对属性语法的增强,称为118E. 凡威克湖Krishnan/Electronic Notes in Theoretical Computer Science 176(2007)1095相关工作、未来工作和讨论5.1相关工作5.1.1通过模型检查的DFA,以及与传统方法的比较Stécien有几个人跟随他的领导。例如,Schmidt [17]表明,DFA只是对程序的这种方法的一个问题是,常用的时态逻辑是命题的,使得它们中指定的属性是程序特定的。Lacey和de Moor [11]扩展了逻辑CTL,使得数据流属性不需要用特定程序的变量来表示,而是可以用表示程序变量或其他结构(如常数)的自由变量来表示我们遵循这种方法将自由变量添加到LTL中以创建LTL-FV [10],并在3.3节中使用它。这种DFA方法的优点是,DFA问题的解决方案是在时序逻辑的相当高的抽象这在证明基于DFA的程序优化的正确性时特别有用(参见5.1.2节)。一个关键的问题是,哪些数据流分析问题可以通过模型检查来解决,这些问题可以通过传输技术(如迭代位向量算法)来解决。Ste Eschen证明了μ演算时态逻辑的一个子集足以指定所有标准的位向量迭代数据流分析,如死代码分析[19]。虽然μ演算是表达性的,数学上也很优雅,但它并不容易阅读、编写或分析。Stécilen开发了一种特定语言(类似于CTL),表达能力较低,但更容易使用。 用这种高级规范语言指定的公式然后被翻译成低级μ-演算。虽然我们考虑的逻辑(CTL和LTL-FV)代表了大多数常用的模型检查器所使用的逻辑,但它们的表达能力不如μ演算。例如,我们的扩展可以只指定立即而不是完全(或重复)的死代码消除。正如在SEC中提到的。4、Silver是一种可扩展的语言,因此可以基于不同的逻辑和模型检查器开发其他扩展,例如这里提到的那些没有什么可以阻止我们为Silver编写另一个扩展,使用μ演算的模型检查器来执行任何标准的位向量DFA。此外,应该指出的是,向CTL和LTL等逻辑添加自由变量允许我们执行诸如常数传播之类的分析,对于这些分析,位向量算法限制太多,并且需要更通用的单调DFA框架[8]。要执行常数传播,除了定义def并使用上面使用的属性来标记CFG。许多经典的数据流问题在这些逻辑的原始源中给出了使用具有自由变量的时态逻辑指定的[12,10]。E. 凡威克湖Krishnan/Electronic Notes in Theoretical Computer Science 176(2007)1091195.1.2优化验证在证明优化程序转换的正确性方面已经做了大量的工作。我们设计了一种技术来证明这种转换的正确性,当它们被指定为用CTL-FV编写的附带条件的重写规则时[12,13]。这构成了Lerner等人工作的基础[14]。他们将副条件规范语言限制在一个小的但常用的子集上,这样正确性的证明就可以自动化。别人还开发了用于证明基于DFA的程序转换的正确性的技术,例如[18]。基于翻译验证的有前途的方法,验证优化程序的语义与原始未优化程序的语义相匹配,例如[23],也已被探索。这些方法不验证转换器或优化器,而是验证其结果。5.1.3属性文法与数据流分析我们并不是第一个研究如何在属性语法框架中执行数据流分析的人。这一领域以前的工作大致可分为三类。第一类包括具有特定数据的系统-作为AG系统的一部分手动执行的流程分析。只有通过用AG的实现语言对分析进行编码,才能添加新的分析。 Tan和Lemone [20]的一个这样的系统可以计算活变量和可用的表达式数据流分析。它是用Pascal实现的,要添加新的分析,必须通过编写Pascal代码来扩展系统以执行所需的DFA。第二类包括使用Farrow [6]称之为“ad-hoc”循环属性定义[ 2 ]的系统虽然这些在传统的AG系统中是不允许的[9],但一些定义良好的循环属性定义可以通过在属性值集合上计算定点来评估。这里,数据流分析被实现为循环属性:属性值上的定点计算对应于模型检查时态逻辑公式中计算的定点。Farrow形式化了循环属性的求值机制以及保证此类计算终止的条件。基于这些技术的系统构成第三类。这种系统的例子包括MUG 2 [7]和最近的CRAG [15]和APS [3]系统。这些系统并不强制执行Farrow因此,在这些系统中可能会意外地写入非终止数据流分析我们提出了第四类,唯一(据我们所知)居住在我们的系统,使用时序逻辑来指定数据流属性和模型检查来实现由公式指定的分析。好处包括DFA的终止保证(因为时态逻辑的模型检查器总是终止),并且当使用像CTL或LTL-FV这样的逻辑时,能够在比循环属性更高的抽象级别上指定DFA。此外,Silver可以很容易地扩展到使用像μ演算这样的逻辑(参见第二节)。5.3)比CTL和LTL-FV更有表达性(见第5.3节)。5.1.1)。120E. 凡威克湖Krishnan/Electronic Notes in Theoretical Computer Science 176(2007)1095.2今后工作在本文中,我们更多地关注数据流分析的规范,而不是要执行的转换的规范。我们目前正在研究用于指定重写规则的机制,如图1(a)中所示,以便它们与DFA侧条件一起可以更直接地转录到AG规范中。本文提出的方法使用高阶属性opt stmt以自底向上的方式构造优化的程序。这类似于OPTRAN [7]中使用的重写规则的自底向上应用。来执行程序转换。这里介绍的两个逻辑不支持过程间数据流分析,但是我们计划构建对Silver的进一步扩展来执行这种类型的分析。有一些逻辑和模型检查器可用于执行过程间DFA这个Silver扩展还需要向Silver添加构造,用于在控制流程图中构建节点和边,这些节点和边指示对函数的调用和从这些函数返回的结果。需要这些来确保在对属性进行模型检查时只使用有效的调用返回路径。因为Silver是可扩展的,所以添加这样的分析是直接的。其他未来的工作解决可扩展性问题,使这里提出的想法可以采用完整的语言描述。由于控制流程图抽象通常只跟踪“程序计数器”和一小组属性,而不是所有程序变量的状态,因此程序的模型(CFG)具有合理的因此,设计用于处理非常大的状态空间的模型检查器可以容易地处理这样的模型。更值得关注的是,在CTL扩展中,NuSMV对每个赋值语句调用一次尽管NuSMV是高度调谐的,但这可能太不明智了。然而,在LTL-FV扩展中,每次分析只调用一次模型检查器。但是返回的替换集的大小可能很大并且计算起来很昂贵。需要进一步的调查,以确定是否多次调用快速模型检查器,如NuSMV是更多或更少的效率比一次调用更复杂的模型检查器的自由变量逻辑。我们还在研究如何安排和有效地执行优化。尽管使用高阶属性(上面的opt stmt和opt stmts)可以很容易地生成优化的程序,但是优化的树可能需要再次优化,就像死代码分析的情况这将重新计算许多属性,值在原始和优化的AST上相同。有几种方法可以追求更有效的实现E. 凡威克湖Krishnan/Electronic Notes in Theoretical Computer Science 176(2007)1091215.3讨论,可扩展语言的动机我们为Silver构建了这些数据流分析扩展,因为在其他研究工作中,我们需要编写高级语言规范,在单个框架中包括语法导向和基于控制流图的分析。我们使用Silver为可扩展的主机语言和语言扩展编写规范。添加新语言结构的会话,这些结构的语义分析,以及这些结构的优化(通常基于数据流分析)到宿主语言。我们指定的许多语言扩展都包含域特殊构造。示例包括将SQL嵌入到可扩展Java宿主语言中的扩展我们希望语言扩展将由这些特定领域的专家编写,但不是编程语言实现专家。因此,我们希望提供一种高级形式主义,用于指定可用于优化特定于域的构造的数据流属性时态逻辑提供了这样一种高级的形式主义。Silver的独特之处在于,它允许在一个声明性框架中,对最适合每种分析的程序表示进行复杂的语义分析。像类型检查这样的面向对象的分析是使用传统属性以自然的方式规范的,并且控制基于流图的分析(如数据流分析)是使用时态逻辑公式以自然的方式规范的。通过属性评估或模型检查对其进行的分析进行评估。由于Silver是可扩展的,因此可以以直接的方式为基于其他时态逻辑(例如上面讨论的μ演算或CaReT因此,作为新的逻辑和模型检查器的开发是有用的,在执行程序分析,他们可以很容易地纳入银。确认我们要感谢Derek Bodin在实现Silver方面所做的努力,以及匿名评论者提供的有用意见。引用[1] 巴尔河,K. Etessami和P. Madhusudan,嵌套调用和返回的时态逻辑,在:Proc.第10届系统构造和分析工具和算法(TACAS 2004),LNCS2988(2004),pp.467-481[2] Babich, W. A.和M. Jazayeri, 数 据流 分 析的 属性 方 法: 第 一部 分 。 详尽 分析 , Acta Informatica 10(1978),pp. 245-264。[3] Boyland,J.,“化学成分的描述性组成”,博士论文,加州大学伯克利分校,伯克利,加利福尼亚州(1996年)。[4] Cimatti,A.,E. M.克拉克角,澳-地 Giunchiglia和M. Roveri,NuSMV:一个新的符号模型验证器,在:Proc. Computer Aided Verification,1999,pp. 495-499.[5] Demers,A.,T. 代表和T.Teitelbaum,Incremental evaluation for attribute grammars with applicationto syntax-directed editors,in:ACM POPL Symp. (1981),pp. 第105-116页。122E. 凡威克湖Krishnan/Electronic Notes in Theoretical Computer Science 176(2007)109[6] 法罗河,自动生成循环但定义良好的属性文法的固定点查找赋值器,ACM SIGPLAN Notices21(1986)。[7] Ganzinger ,H. ,R.Giegerich , U.MonckendR.Atrulygenerativesematics-directedcompilergenerator,SIGPLAN Not. 17(1982),pp. 172-184。[8] Hecht,M.,[9] Knuth,D.E、上下文无关语言的语义学,数学系统理论2(1968),pp。12795比96[10] 克里希南湖“LTL-FV: A Temporal Logic for Specifying Data-Flow Analyses,” Master’s thesis, The[11]莱西,D.和O. de Moor,Imperative program transformation by rewriting,in:10th Intl. Conf. onQuantifier Construction,LNCS 2027(2001),pp. 52比68[12] Lacey , D. , N. D. 琼 斯 , E 。 Van Wyk 和 C. C. Frederiksen
下载后可阅读完整内容,剩余1页未读,立即下载
![application/x-rar](https://img-home.csdnimg.cn/images/20210720083606.png)
![application/msword](https://img-home.csdnimg.cn/images/20210720083327.png)
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)