Python错误符号执行验证工具的实用性和潜力验证，测试和Python程序可靠性的新方法

可在www.sciencedirect.com在线获取理论计算机科学电子笔记339（2018）21-41www.elsevier.com/locate/entcsPEF：Python错误达米安·巴索蒂1号，其他人是M。Bordese2Tom'asHayes3FacultaddeMatema'tica，Astronom'ıa，F'ısicayComputacionUniversidadNacionaldeC'ordob a阿根廷摘要PeerCheck[1]是一种轻量级的基于库的方法，用于在面向对象语言上实现符号执行，而无需修改分析的代码。与传统的符号执行引擎不同，符号语义被构建为与目标程序一起运行的外部库他们可以完成这项任务，这要归功于python编程语言的特殊功能，它允许人们用类对象实现符号值。然而，他们的方法仅限于对原语类型的符号执行。在这项工作中，我们展示了一个扩展，它使人们能够对用户定义的类对象执行符号执行此外，我们构建了一个新的验证工具，称为PEF，它实现了所描述的技术和我们的扩展。该工具可用于验证用Python编程语言编写的程序我们使用该工具来验证它自己的代码，展示了它在生产中测试程序的潜力和实用性。我们还评估了测试知名算法和数据结构的工具。关键词：可靠性，验证，单元测试，符号执行，程序测试，程序调试，程序证明，程序验证，符号解释，测试Python程序。1介绍符号执行是一种流行的程序推理技术。它实现了一个符号语义，允许一个执行程序的符号输入代表多个具体的输入，从而同时涵盖了许多具体的单一（符号）执行路径上的执行。基于这种技术，各种工具已经成功地自动检测传统上，符号语义通过以下方式实现：• 为编程语言编写新的解释器;或• 将代码翻译成具有符号执行支持的另一种语言;或1电子邮件：damian@famaf.unc.edu.ar2电子邮件：andresb9163@gmail.com3电子邮件：tomyhayes@gmail.comhttps://doi.org/10.1016/j.entcs.2018.06.0031571-0661/© 2018作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。22D. Barsotti等人/理论计算机科学电子笔记339（2018）21• 检测目标代码。也就是说，编写一个外部程序，将指令注入到战略位置，以实现符号支持，同时保持原始解释器。例如，Java Pathfront [13]是作为JVM字节码的解释器实现的; DART[8]是x86二进制程序的解释器; Bitblaze[12]将二进制代码翻译为中间语言，CUTE[11]实现C代码指令。不幸的是，这些方法具有一些缺点。它们需要大量的代码来开发和维护。此外，它们在处理生成的或动态加载的代码时也会出现问题。最后，可能很难跟上语言的发展，并支持非标准的扩展。为了解决这些问题，PeerCheck[1]提出了一种新的替代方案。它引入了对等体系结构，其中符号执行引擎与程序一起工作。它不是定义一个新的解释器或编译器，而是简单地将符号执行引擎实现为目标语言的库。对等体系结构利用了动态和纯面向对象语言提供的功能。这个想法主要是基于他们的能力，动态分派原语运算符，如算术运算符，数组访问，条件分支测试等。然而，对等体系结构一直受到批评[14]，因为它只允许检查用原语类型实现的程序。本文证明了扩展PeerCheck来处理用户定义的类对象是可行的。该扩展为构建验证工具开辟了一条新的道路，只需很少的时间，并且仅受自动化证明器能力的限制。尽管如此，这些证明器的功能，就像SMT求解器[7]一样，正在不断发展。我们提出的技术适用于用Python编写的程序。Python是一种纯面向对象的语言，用于实现高级功能，各种系统。然而，在Python程序上实现高度的覆盖测试已经被认为是必要的，因为这种语言缺乏静态类型检查此外，我们的方法可以适用于其他面向对象的程序设计语言。为了实现我们的方法，我们实现了PEF（Python错误验证）验证工具。该工具作为上述改进的对等体系结构技术的概念证明。它是通过将Z3[6]SMT求解器与我们的Python（版本3）代码集成而开发的。该工具还实现了一个用于表达前置和后置条件、程序异常和类型限制的合同系统。本文的其余部分组织如下：在第2节中，我们给出了符号执行技术的概述。第3节描述了PEF体系结构及其子系统。第四节介绍了合同制的实施情况。第6节展示了如何使用该工具来验证它自己的代码。第7节显示了一些结果，通过应用该工具对众所周知的算法和数据结构。第8章讨论相关工作最后，第9节提出结论并讨论D. Barsotti等人/理论计算机科学电子笔记339（2018）2123∧∧未来的工作。2符号执行符号执行是由James C.王[10]为了获得可靠的软件程序。在这种技术中，通过用任意符号替换其具体输入值来模拟程序执行，从而定义替代因此，被分析的程序在其执行期间转换符号状态，而不是真实的数据对象。符号执行试图通过选择不同的满足路径约束来覆盖所有可能的执行路径，直到所有执行跟踪都被完全探索。考虑一个仅由赋值语句和条件语句（IF-THEN-ELSE）组成的程序。可视化这种技术的一种方法是将程序表示为执行树：每个节点将表示一个执行语句，每个边根据程序的执行路径表示从一个语句到下一个语句的转换该技术从根（程序开始）通过象征性地执行程序并将每个节点附加到符号状态来构建此树。符号状态包括其变量α的符号值和路径条件PC。开始时，根节点具有PC=True，并且α是从输入程序变量v1，···，vn到表示初始符号值的符号s1，···，sn给定一个符号状态σ= α，PCα，它连接到一个节点，该技术生成其子节点如下：(i) 在表示赋值语句的节点上，它创建一个具有新符号状态的新子节点。这有相同的PC，α是通过将每个赋值语句中的左侧变量替换为右侧表达式来获得的。这个表达式必须首先转换成符号表达式，用映射上定义的变量的符号表达式替换它的变量(ii) 在表示“IF e THEN S 1 ELSE S 2”语句的节点上 因此，PC被更新为PC=PCσ（e），并且新的路径条件PCJ=PCJ！（e）是创造出来的。 对于这些公式，σ（e）给出了根据α的表达式的符号值。 PC和PCJ根据它们的可满足性定义最多两个子节点，通过将具体值分配给相关的符号变量。 为了确定满足性，路径限制，自动证明器或自定义决策程序采用了如果PC和PCJ都不满足，则该路径的符号执行结束。(iii) 如果符号执行到达退出指令或错误（例如，程序失败或违反断言），则符号执行的相应实例结束，并且使用自动证明器生成满足当前符号路径条件的赋值，如前所述。24D. Barsotti等人/理论计算机科学电子笔记339（2018）211deff（total，price）：2如果总价>价格：3总计=总计-价格如果总数==0，则为4：5assert False在步骤ii中，如果两个路径条件都满足，则该方法首先选择THEN分支。 因此，树是按照DFS顺序生成的。 在这种情况下，在一个自由分支上，否则我们说这是一个强制分支。作为示例，图1显示了从图2代码生成的树。边缘标有相应的线路代码编号。Fig. 1. 执行树示例。图二.符号执行示例。如果程序包含循环或递归调用，这种技术可以推广，因为它可以在有限树中产生不便。 一个确保终止的解决方案是限制生成树的深度[10]。 溶液当树的大小很大时，也很有用，以避免可伸缩性问题。3PEF实施PEF遵循[1]中提出的对等体系结构。符号执行引擎被实现为一个语言库，它允许一个它的执行作为一个对等的目标程序。此程序由引擎执行，使用称为代理对象的特殊输入参数而不是具体值。代理对象充当符号执行技术的符号值D. Barsotti等人/理论计算机科学电子笔记339（2018）2125代理操作员回调代理对象合同PythonZ3 SMT求解器象征性执行引擎目标程序当目标程序对代理对象执行类操作时，解释器动态地向符号执行引擎分派函数调用这允许在运行时跟踪输入的变化。在需要代理对象的值的条件跳转的特定情况下，符号执行引擎再次被报告，并且它查询外部证明器（SMT求解器Z3）以决定探索哪个路由。在图3中，我们可以看到这个架构。图三. PEF架构。符号执行引擎由两个耦合的子系统实现：执行循环负责通过不同的树执行路径多次运行目标程序，而代理对象（每个类型类一个）负责跟踪符号值的变化3.1执行循环该子系统采用explore方法实现。图4显示了它的简化代码。它将目标程序和代理对象（符号输入）作为参数。循环中的每次迭代（第8行）探索执行树的新路径，并存储返回值，或抛出异常（如果有）（第12行到第14行）。它还通过拦截对print函数的调用来捕获程序的输出每当系统到达空闲分支时，它选择一条路径进行探索，并为另一条路径安排未来的分析。为了注册它们，子系统创建两个全局列表（堆栈）：• _path（在第6行初始化）它是一个布尔值列表，指出自由分支节点中的所选路径。boolean_path[i]表示路径中第i个自由分支的当前分支选择（THEN或ELSE）。因此，符号执行引擎使用此列表来调度每个探索路径。此外，同一列表用于目标程序的全面分析。26D. Barsotti等人/理论计算机科学电子笔记339（2018）211defexplore（function，args，kwargs）：2“”3探索从'function'开始的4首 字母是args和kwargs5“”6_path =[]7. have_paths_to_explore= True8虽然h a v e _paths_to_explore：9_路径条件=[]10个结果，错误=无，无11尝试：12（结果，输出）=函数（*args，**kwargs）13除了例外，如e：14错误= e15最后：16yield（args，kwargs，result，error，17个输出，_pathcondition）18当len（_path）> 0且not_path[-1]时：pop（）20if not_path：21have_paths_to_explore= False22其他：23_path[-1]= False图四、简化explore函数的代码• _pathcondition（在第9行初始化）它包含正在探索的当前路径条件（PC）。它由这个子系统初始化，然后由代理对象填充，我们将在后面展示_pathcondition [i]存储当前路径中第i个自由分支的限制。这些公式是相连的，证明者将使用其结果来决定路径条件的满足性。这些变量是子系统和代理对象之间的通信手段这允许子系统执行执行树的所有DFS路径：PEF使用存储在_path中的信息来获取要探索的新路径的前缀在每次迭代开始时（第9行），list_pathcondition被清空。然后，移除_path中的false值的post fix（第19行），并对最后一个true值取反。这个过程允许人们探索消极的分支。当_path为空时（第20行），所有分支都被探索，流程结束。此外，分支被探索到一定的深度，或者直到证明者不能确定所涉及的表达式的满足性。PEF通知用户被忽略的分支。每次符号执行发现一个函数调用时，它将被符号执行，因为它的代理对象参数（如果有的话）将通知PEF符号状态变化。返回值（通常是符号）用于继续原始执行。explore方法被编程为生成器（第16行），对于每个探索的路径，它返回一个包含以下内容的元组：• 位置和可变长度代理对象参数的列表（argsykwargs）D. Barsotti等人/理论计算机科学电子笔记339（2018）2127目标方案;• 执行路径的符号结果（result）;• 抛出的异常，如果有（错误）;• 输出写入stdout（output）• 最后一个路径条件（_pathcondition）。必须修改符号执行过程以确保终止（第2节）。这是通过限制执行树的扫描深度来完成的。默认限制取自[1]，但可以在必要时轻松更改。这个值实际上对于我们分析的示例程序是足够的。关于这些结果的更多信息将在第7节中提供。3.2代理对象面向对象的语言，如Smalltalk、Ruby或Python，将所有数据表示为对象。此外，它的操作被转换为方法调用。此外，对象的类型仅由其属性和方法的名称定义，而不管它是原始类型还是用户定义的类型。这种语言的特性被称为Duck Typing 4。 我们的工作是基于这些功能：PEF执行的目标程序取代其参数与代理对象，具有相同的方法和属性名称。因此，代理对象模拟真实对象的行为，同时跟踪程序的执行为了模拟基元类型上的二进制操作，代理对象必须模拟它们的实现。Python为二进制操作实现了“双重分派”机制。例如，表达式x + y被转换为调用x。add（y），如果x的类知道y的类（例如，当它们属于同一个类时）。如果x属于一个内置类（例如， int）和y属于不同的，Python执行替代翻译y。radd （x）（右加）通过将结果委托给y类方法。如果y的类不能解析操作，这将导致运行时错误。Python在其他类中使用了双重分派机制，例如bool：表达式a< b的初始翻译为a。 lt（b）. 然而，如果a和b属于不同的类，则操作被转换为b。 gt（a）.正如我们已经提到的，代理对象实际上是符号值。除此之外，它们在PEF中执行符号执行过程.它们的行为就像自动证明器使用代理对象收集的信息来决定目标程序执行中可以采用哪些路径PEF实现代理对象的不同类，以表示不同类型的值。例如，在图5中，我们展示了整数代理类的简化版本，而我们的实现支持与Python内置整数类相同的数值运算符和谓词集4https://en.wikipedia.org/wiki/Duck_typing。28D. Barsotti等人/理论计算机科学电子笔记339（2018）211类IntProxy（ProxyObject）：2345678910111213141516171819202122232425262728293031323334““”符号整数“definit（self，value=None）：如果value为None：self.term = smt.fresh_var（int）else：self.term = smt.make_symbolic（value）defadd（self，other）：”X. add（y）==> x+y“returnIntProxy（smt.op（其他.term））defradd（self，other）：”X. rdd（y）==> y+x“返回自我。添加（其他）defeq（self，other）：”X. eq（y）==> x==y“returnBoolProxy（smt.pred（其他.term））defreq（self，other）：”X. req（y）==>y==x“返回自我。eq（其他）图五、IntProxy类（缩写代码）代码显示了构造函数（方法init）、加法运算符（方法add、radd）和相等性测试（eq，请求）.它包含全局对象smt作为与证明器的接口。我们首先描述构造器方法。对smt.fresh_var（int）的调用（第8行）为证明器生成一个新的整数变量，从而创建一个符号值。如果传递了一个初始化值，构造函数调用方法smt.make_symbolic（value）（第10行），该方法创建一个整数常量。此外，如果初始化值已经是符号化的，则不修改地存储它然后，add（line）和eq方法返回表示路径条件中使用的整数或布尔表达式的代理对象。他们调用smt.op和smt.pred来构造它们。布尔代理对象的实现更为复杂，因为它决定了在程序的执行树中遵循哪些分支类的简化版本如图6所示。实现通过global_path和_pathcondition列表链接到执行循环（第3.1节）D. Barsotti等人/理论计算机科学电子笔记339（2018）21291类BoolProxy（ProxyObject）：2“”3符号布尔值4“”5definit（self，formula=None）：如果公式为None，则为6：7自我公式= smt.fresh_var（bool）8其他：9自我公式= smt.make_symbolic（公式）1011def不（self）：12returnBoolProxy（smt.formula（'！'，self.formula））1314defbool（self）：15#测试路径条件16true_cond=smt.solve（smt.formula（&17_路径条件，self.formula））18false_cond=smt.solve（smt.formula（&19_路径条件，20smt.formula（'！'，self.formula）21#只有一条路22iftrue_condand！false_cond：返回True24如果！true_cond和 false_cond：25returnFalse2627如果len（_path）>len（_pathcondition）：28#必须恢复以前的状态29分馆=_path[len（self._路径条件）]30如果分支：31_pathcondition.append（self.formula）32其他：33_pathcondition.append.（smt.formula（'！'、34self.formula））35返回分支3637#达到探索的最大极限38如果len（_path）>= MAX_DEPTH：39号Paramoslaexploraci'ondeestarama.40raiseMaxDepthError（）41第42集Follows the True Path43_path.append（True）44_pathcondition.append（self.formula）返回True见图6。 BoolProxy类（缩写代码）。每次条件谓词包含代理对象时，Python解释器都会调用_ bool类方法来决定必须采取哪条路径。因此，就路径的可行性向证明者咨询它决定存储在BoolProxy对象中的公式或其否定是否与_pathcondition中的其余公式一起满足（第16行到第20行）。如果仅满足这些公式中的一个（即，程序执行到达强制分支）时，该方法将相关分支的布尔值返回给解释器30D. Barsotti等人/理论计算机科学电子笔记339（2018）21(line22 至 25 ） 。 因 此 ， 目 标 程 序 的 执 行 继 续 ， 而 不 修 改 lists_path 和_pathcondition（第16行到第25行）。否则，当两套公式均令人满意时（即程序执行到达自由分支）：(i) 如果_path包含的值比path条件的长度多，则example到达了一个已经探索过的自由分支。在这种情况下，该方法根据路径中存储的分支的当前真值，将公式或其求反附加到路径条件。最后，它向解释器返回与当前运行中要执行的分支相关联的布尔值（第27到35行）。(ii) 如果超过了深度界限，那么通过抛出异常（第38行到第40行）终止此路径。(iii) 否则，该分支未被探索。因此，必须在这个测试运行中探索true分支，因此返回这个布尔值。此外，该值被添加到_path，当前公式存储在路径条件中（第43至45行）。False分支将延迟到后续运行。请注意，_path列表只在这里被修改，并由执行循环修改。3.3容器代理对象除了整数和布尔值之外，PEF还可以对列表、切片和字符串符号值执行符号执行。这些都是用代理类ListProxy、StringProxy和SliceProxy实现的。ListProxy类实现索引操作l[i]、列表更新l[i]=j、长度len（l）、列表 连 接 l+m 、 复 制l*i、插 入l.insert（i，j）、追 加l.append（i）、字典比较l m等。列表l、m和索引i、j也可以是代理对象。列表在z3中表示为数组。此外，我们必须通过添加一个符号整数来表示其大小的限制，因为Z3数组是无界的。为了将这个约束传递给Z3，我们添加了一个名为_facts的全局列表（在添加到_path和_pathcondition）。该列表定义了假设的条件”张昭说道。图7显示了ListProxy类的构造函数方法。在第10行中，该方法附加了非负的初始长度约束。所表示的长度约束可以在程序执行树中生成新的分支。图8显示了这种行为。当使用符号列表ls调用函数时，符号执行生成三个不同的路径条件：[len（ls）==0];[len（ls）>0，ls[0]< 0]和[len（ls）>0，！ls[0]< 0]（第2行）。在第一个路径中，PEF抛出IndexError异常，因为它无法在条件中计算ls[0]。在第二条路径中，符号执行执行列表更新（第3行）。最后一个路径对应于else分支。这个else分支继续循环符号列表（第5行）。第一次迭代不进行分支，因为路径条件包括约束len（ls）> 0。在接下来的迭代中，符号执行分支一个路径：一个路径返回None，另一个继续循环。在D. Barsotti等人/理论计算机科学电子笔记339（2018）21311deff（ls）：2ifls[0] 0：<3ls[0]= 04其他：5对于ls中的 j：6print（j）7return无1类ListProxy（ProxyObject）：2“”3符号列表4“”5definit（self，initial=None）：6如果非初始：7self.阵列= smt.fresh_var（array_int）8self._透镜= smt.fresh_var（int）9#总是正的长度10_facts.append（self._透镜>=0个）11其他：12self.阵列= smt.make_symbolic（initial）13自我。透镜= smt.make_symbolic（len（initial））图第七章ListProxy构造函数类（缩写代码）。见图8。 由列表长度导出的分支（示例代码）。在最后一种情况下，PEF附加条件len（ls）>i，其中i是迭代次数。这个过程一直持续到达到最大探测深度。在PEF中实现的列表代理对象不能存储不同类型的值，此外，我们目前的实现只允许我们存储符号或具体的整数值。无论如何，具体列表可以存储不同类型的具体或符号值，因为在这种情况下，没有必要在Z3中表示它们。为了支持列表上的所有操作，有必要实现中间切片。切片被广泛使用，因为它们允许提取列表段，并且它们被Python程序员广泛使用。例如，给定切片a：b，ls[a：b]是从位置a（从0开始）到位置b-1的子列表。字符串和列表具有类似的实现。字符串表示在Z3使用数组和符号整数，因为Z3不提供对这种类型的原生支持。此外，StringProxy类只具有ListProxy类提供的功能的一个子集，因为字符串不像列表那样是可变4合同制度为了提高错误检测，我们引入了一个合约系统，它可以定义要验证或施加在程序执行上的类型和属性。它的语法是非侵入性的，并遵循文档字符串约定5。我们定义了四种5https://www.python.org/dev/peps/pep-0257。32D. Barsotti等人/理论计算机科学电子笔记339（2018）21defpositive_division（i，j）：”：假设：i>0，j>0“i / jdeff（a，b）：““”：ensure：returnv>= a+b“return abs（a）+abs（b）defpolimorfic_product（a，b）：”：types：a：int，b：[int，str]“返回a * b合同的先决条件、后置条件、类型和例外。前置条件契约用于对函数的参数值施加初始约束。它们以关键字：assume：开始，然后继续使用一些由逗号分隔的布尔表达式，这些表达式被解释为公式的合取。图9显示了一个示例。见图9。 先决条件合同（示例）。在合约中，用户可以引用在目标程序的同一上下文中定义的任何输入参数或后置条件契约用于定义目标程序运行后必须满足的属性这些合约被PEF用作oracle测试来检测程序错误。它们以关键字：ensure：开始，然后继续使用一些由逗号分隔的布尔表达式，就像前置条件契约一样。图10显示了一个示例。见图10。 后置条件合同（示例）。在这种类型的合约中，关键字returnv表示目标程序的返回值。其他变量仅引用执行的初始值。Python是一种动态类型语言，缺乏明确的类型定义。为了定义程序输入的类型，我们用类型契约扩展了契约系统。这类合约允许我们根据声明的类型生成适当的图11中显示了类型合约的一个示例。见图11。 类型合同（示例）。这些合约以关键字：types：开始，并继续类型声明。语法允许我们为每个参数声明一个类型列表在D. Barsotti等人/理论计算机科学电子笔记339（2018）2133definteger_division（i，j）：”：raises：ZeroDivisionError：j==0“returni //j这种情况下，PEF对每一个执行符号执行过程。当有多个参数定义了一个以上的类型时，会为可能的类型参数的每个组合运行一个符号执行过程。虽然类型契约对于程序的符号执行是必要的，但在某些情况下，PEF能够自动推断类型• 当类方法引用变量self时，PEF推断其类型是类。• 当一个程序将一个参数声明为*args时，PEF推断它具有类型名单• 当一个类型合约定义一个列表类型的参数时，PEF会推断这是一个包含整数值的列表，因为PEF只能处理这种类型。如果无法推断参数的类型，那么PEF将抛出自己的合约类型异常。在Python中，并不是所有的异常都指向错误，因为它们有时被故意用于程序中，以传达它们的内部状态。因此，该系统包括例外合同。这些允许我们区分异常的那些用途。异常合约以关键字：raises：开始，继续Python异常的类型，并以变量的条件列表结束。如果在路径的符号执行中发生这种类型的异常，则PEF将检查假定路径条件的条件的有效性。如果它们为真，则路径被认为是正确的。在图12中，我们展示了一个例子，其中被零除不被认为是错误。见图12。 例外合同（示例）。5用户定义的代理类对等体系结构的建议有一些批评[14]，因为它只允许在原始类型上执行一次符号执行。然而，我们将展示如何扩展这种技术来生成用户定义的类对象的符号值PEF通过一个名为proxify的独特函数实现了原始类型或用户定义类的代理对象的生成。这个函数接受一个类型标识符，并返回一组代理对象。出于演示目的，图13显示了一个简化的算法代码。首先，在第2行，函数询问其参数是否是内置类型。在这种情况下，它返回相应的代理对象。因此，它返回int类型的IntProxy对象，bool类型的BoolProxy对象等。34D. Barsotti等人/理论计算机科学电子笔记339（2018）211defproxify（type）：2ifisBuiltin（type）：3返回p r o x i f y _builtin（type）4其他：5#获取合约6argTypes = TypeContract.init）7#获取全部类型参数8个argType组合= combine（argTypes）9结果=[]argTypeCombinations中的argTypesComb为1011#代理当前参数12argProxyObjs =[]13对于argTypesComb中的typeArg：14个argProxyObjs+= proxify（typeArg）15#获取全部代理参数16个argProxyObjCombinations= combine（argProxyObjs）17对于argProxyObjCombinations中的 argProxyObjsComb：18#构造函数19result += symbolicExec（type. 初始化，20个argProxyObjsComb）21返回结果图十三. proxify方法（缩写代码）。否则，如果参数是一个用户定义的类，算法将搜索在其构造函数（init）方法中定义的类型合约（第6行）。 的类型必须指定构造函数参数，以便实例化代理对象。在第8行，函数生成构造函数参数中所有可能的类型组合。这是因为类型契约可以为每个参数指定一个类型列表，如第4节所述。从第9行开始，result变量从输入类中累积可能实例化的代理对象。为此，循环（下一行）对构造函数参数类型（变量argTypesComb）的每个可能列表进行操作。对于这个列表中的每个类型，函数执行递归调用，为输入类中的每个参数返回一组代理对象。变量argProxyObjs累积接收到的对象，这些对象也可以是原始类型或用户定义类的一些实例。请注意，这些递归调用结束，因为用户定义的类最终是用内置类型实现的。然后，该函数生成由其递归调用返回的代理对象的所有可能组合（第16行）。每个组合都将是输入类的构造函数的一组符号参数。它们存储在变量argProxyObjCombinations中。一些类对象构造函数（在init方法）可以在-根据它们的参数，导出几个执行路径。这种可能性使得有必要构建一些新的构造函数参数实例。例如，在图14中，构造函数根据n的论点。 给定这个构造函数，函数proxify返回两个代理对象：s0和s1，其中s0.value== i0和s1.value== i0+5，其中i0是D. Barsotti等人/理论计算机科学电子笔记339（2018）2135类GreaterFive（object）：definit（self，n）：““”：type：n：int“如果n >5：self.value=nelse：自身值= n +5通过递归调用从n见图14。 构造函数路径（示例）。为了生成这些代理对象，函数象征性地执行输入类的构造函数（第19行 ） ， 为 每 个 执 行 路 径 获 得 该 类 的 代 理 对 象 。 象 征 性 执 行 使 用argProxyObjCombinations中存储的代理对象的每个组合作为构造函数的参数。生成的代理对象累积在result变量中，并作为函数的结果应该注意的是，这个算法有一个限制：只有在构造函数内部声明的变量才会被实例化为代理对象。因此，修改类变量或全局变量的用户定义类不能完全实例化为代理对象。这只是限制了符号执行算法的覆盖范围，可能会忽略目标程序的某些执行路径6用PEF在PEF的开发过程中，我们发现了实现代理对象方法的一些问题。这是因为内置类型的文档记录不好或所涉及操作的复杂性。因此，我们决定将此工具应用于自身。其结果是一个应用于生产软件的真实用例，显示了PEF的潜力。使用该工具作为库执行任务（PEF也可以在命令行界面中执行）。该程序可通过PEF代码（implementation_test.py文件）获得。它执行由PEF实现的代理对象方法的符号执行。然后，将每个路径的符号结果与Python中内置操作的结果该任务完全自动执行：(i) 它搜索PEF代码中代理对象的所有实现。对于每一个，它都标识了仿真的内置类。我们调用c的每个代理类，real（c）是c模拟的内置类。(ii) 给定一个类c，PEF探索其方法的执行路径。对于每个方法，PEF通过执行符号执行返回一组元组。这些元组包含一些输入代理对象、一个符号结果、一个路径条件和一个抛出的异常（如果有的话）（3.1节）。每个元组对应于一个执行路径。36D. Barsotti等人/理论计算机科学电子笔记339（2018）21(iii) 通过路径条件和符号结果，PEF可以为real（c）内置方法构建测试用例：它获得满足以下条件的变量赋值：通过使用Z3证明器来确定路径条件（获得模型）。此变量赋值用作内置方法中的具体参数。此外，通过对符号结果应用相同的赋值，可以获得预期的具体返回值。(iv) 程序使用上一步中获得的输入参数运行内置方法。 如果内置方法和路径的执行返回相同的异常，则认为路径是正确的。如果内置方法返回生成的预期值，则路径也被认为是正确的。否则，路径有错误。(v) 如果方法的任何测试用例检测到错误，则该实现被认为是不正确的。通过使用该程序，我们发现了PEF中的几个错误例如，为了构建SlideProxy类，我们必须读取函数indices这段代码是标准Python解释器CPython 6的一部分。对代码的误解导致我们的实现中出现了几个错误。多亏了这里介绍的程序，我们才能检测到它们。7结果我们用一些算法对该工具进行了评估。我们进行评估基于英特尔的笔记本电脑，配备了i5- 4258 U处理器在2.40GHz ，8 GB内存在1600 Hz，和OSX10.10。7.1快速排序图15显示了使用列表解析实现的QuickSort算法。我们在代码中包含一个可选的先决条件契约，定义列表长度。虽然这个合同不是强制性的，但它是为了分析算法而添加的不同列表大小的性能。我们开始分析探索路径的数量、生成的执行树的深度以及探索分支的百分比。在表1中，我们展示了这些结果。正如我们所看到的，探索路径的数量是列表长度的阶乘，正如预期的那样。执行树的深度是自由分支的数量。这个数字较低，因为它的增长是相对于列表大小的二次增长。最后一列显示，只需要对包含三个元素的列表执行QuickSort，就可以实现分支的完全覆盖。表2显示了相同QuickSort代码的运行时分析。这些值是采用五次执行的平均运行时间来测量的。6https://github.com/python/cpython。D. Barsotti等人/理论计算机科学电子笔记339（2018）2137defquicksort（l）："”使用列表解析的：类型：l：列表：假设：len（l）== 6：确保：returnv ==排序（returnv）“如果不是L：return[]else：pivot = l[0]lesser = [xfor xin l[1：]if x pivot] greater= [xfor xin l[1：]if x >= pivot]lesser_sorted = quicksort（lesser）greater_sorted = quicksort（greater）returnlesser_sorted + [pivot] + greater_sorted图15. 快速排序代码。列表长度探索路径树深度探索%分支0101611033221663631004246100512010100672015100表1快速排序浏览结果。该表显示了PEF分析的运行时间，以及作为独立程序运行的QuickSort算法（具体执行）。独立执行的输入参数是PEF作为测试用例返回的列表：对于每个列表大小，PEF返回覆盖执行树的具体输入列表。我们用这些测试用例计算了算法的运行时间。这个过程重复五次，结果取平均值。使用PEF的运行时分析也是五次平均。该表显示了这两个运行时间是如何随着列表大小的增加而快速增加的。这种行为是由于探索的路径数量随着这个大小而成比例地增长。38D. Barsotti等人/理论计算机科学电子笔记339（2018）21列表长度PEF运行时间[ms]独立运行时间[μs]0一六五、二十九一九五、五十九1三百零九，六十八185， 12641， 28一九六、二十四32263， 67二二一，零二410610， 27398，12562431， 881522，0464、 7· 1059430，11表2快速排序运行时间。7.2其他结果我们在几个程序上测试了PEF，这些程序可通过PEF代码（examples.py文件）获得。对于这些例子中的每一个，我们都测试了正确性属性使用合同制的项目。表3显示了五次执行的平均运行时间（以秒为单位）。该表显示了PEF分析的运行时间和独立程序（具体执行）。独立程序的输入参数是PEF作为测试用例获得的值。这些计算方法与快速排序算法相同（第7.