基于多目标优化算法的string smt求解器测试

SMT求解器，但是很少SMT求解器性能缺陷的研究。由于字符串理论作为一种出现较晚的求解器理论，并且存在着大量复杂的语法，使得StringSMT求解器中包含大量潜在的缺陷。在现有的研究中，我们观察到在生成触发StringSMT求解器性能缺陷的测试用例中存在两个：指导信息和多样性。在本文中，我们提出了一种多目标优化MulStringFuzz，用于检测字符串求解器的性能缺陷。MulStringFuzz的独特之处在挤距离计算方法，通过拥挤算子筛选从而确保生成的测试用例的多样性。MulStringFuzz能够有效的检测StringSMT求解器的性能缺陷，我们的方法生成的测试用例可以覆盖5000行StringSMT求解器性能缺陷的测试用例数是其他方法字符串SMT求解器的性能缺陷。Multi-objectiveEvolutionaryAlgorithmforStringSMTSolverStringSatisfiabilityModuloTheories(SMT)solveriswidelyusedinacademiaandindustry.Theruntimeefficiencyofmanysoftwareisaffectedbytheperformanceofthesolver.AlthoughmanystudieshavebeenconductedtotestSMTsolvers,theymainlyfocusondetectsoundnessbugsofSMTsolvers.However,afewresearchattachimportancetodetectperformancedefectsofSMTstringsolvers.Althoughtheexistingapproachgeneratesinstancethattakesalongtimeforagivensolvertosolvethroughgeneticalgorithms,testcoveragecannotbeguaranteedduetolackofbootinformation.Inaddition,shortageofdiversityassessmentmayresultintheemergenceofstructurallyidenticalindividualsintheInthispaper,weproposeamulti-objectiveevolutionaryalgorithm,MulstringFuzz,whichisusedtoautomaticallygeneratetestcasestoautomaticallydetectperformancedefectsofstringSMTsolvers.WeobservedtwochallengesingeneratingtestcasesthattriggerperformancedefectsinStringSMTsolvers:guidanceinformationbarriersanddiversitybarriers.Inthispaper,weproposeamulti-objectiveoptimizationalgorithm,MulStringFuzz,todetectperformancedefectsofstringsolvers.MulStringFuzzisuniqueinitsmulti-objectiveoptimizationandmaintenanceofpopulationdiversity.Todealwiththeguidanceinformationbarrier,MulStringFuzzusesthreeobjectivefunctions:theelapsedtimedifferencebetweenthetargetsolverandthereferencesolver,codecoverage,andthecomplexityoftestcasestoguidetestcasegeneration.Inordertosolvethediversitybarrier,weproposeacrowdingdistancecalculationmethodbasedonsolverdynamictrackinglog,andfilterindividualsthroughcrowdingoperatorstoensurethediversityofgeneratedtestcases.Weevaluatedtheeffectivenessofthealgorithminextensiveexperiments,whichshowedthatMulStringFuzzeffectivelydetectedperformancedefectsinStringSMTsolvers.Ourmethodgeneratedtestcasescoveringnearly5,000linesofcode.Theresultingresultsetgenerated3.25timesasmanytestcasesthatcouldtriggeraperformancedefectintheStringSMTsolverthantheothermethods.Byyzingthespatialdistributionoftheresultset,thecrowdingdistancecalculationmethodbasedondynamictrackinglogofsolverproposedbyuscaneffectivelyincreasethediversityofindividualsinthepopulation.ThisshowsthatourmethodcandetectperformancedefectsofstringSMTsolvermoreeffectively.：WriteCriterion;TypesetFormat;Master’sDegree 绪 研究背 满足性模理 SMT求解器与SMT- 模糊测 多目标演化算法算 研究内容以及主要贡 组织结 本章小 相关工 求解器的错误分 传统测试方 基于语法的模糊测 基于搜索的模糊测 基于突变的模糊测 基于逻辑近似变形的测 本章小 基于多目标优化的求解器性能检测方 动 框 定 适应度函数评 运行时间分 代码覆盖率得 测试用例复杂 遗传算 验证、程序缺陷检测、优化问题求解、云计算和云、静态分析等等[6-10]。这些领域的问题都可以被建模为约束可满足问题，SMT在这类问题的表述和求解上都有着突出SMT求解器的影响，检测字符串SMT求解器的缺陷至关重要。验证、线性逻辑约束优化问题求解等一些前沿的研究领域中有着很突出的优势[3]。自动生成测试用例是保证软件测试质量的法。通过自动生成测试用例，可以SMT的测试用例自动生成技术主要分为两个部分。第一步径的可满足行，在这一步需要使用到SMT。为了使用SMT求解器来检测路径，需要将路径信息转化为SMT来进行检查。程序缺陷检测的主要思想是检测程序在一个给定的界限中是否满足所规定的安全SMT的有界模型检测方法(bounddmodelhking，MC)方法[4]。其主要思想是在系统中通过限定的界限不断地得到验证条件。界限地含义是将源程序中地循环结构展开KSMT否安全属性。程序分析与验证同样使用到SMT求解器方法是一SMT求解器的形式化方法。受到Floyd和Hoare弗洛伊德-霍尔逻辑(Floyd-Hoarelogic)的影响，SMT方法的逐渐扩。这种方法的基础思想来源于Floyd和Hoare。在这一过程中通过设置前置条件、控制循环不变量和限制后置条件，将其形式化为SMT实例中的断言语SMT以其丰富的背景理论和高效的组合背景理论求解技术成为了可满足性问题求解领域的。目标应用程序的性能和正确性都会收到求解器的影响，例如在符号计算程序信息时无法得到正确的结果。在工业界的求解器也有着大量的应用场景，包括火箭轨迹规划、城市资源配送路线分配等等方面，如果求解器的健全性出现问题，SMT求解器的正确性至多的研究聚焦于SMT求解器的测管大家已经发现了很多求解器的bug，但对于一个SMT求解器方向上表现得很有前景。研究背可满足性模理论（satisfiabilitymtheories,SMT）是判定一阶逻辑在组合背景理论下的可满足性问题。SMT问题正是在可满足性问题（TheSatisfiabilityProblem,SAT）的基础上扩展而来。SAT问题是命题逻辑的可满足性判定问题，最典型的是布尔可一个命题逻辑f，f由子句集S组成。其中的每一条其中子句集是由一组布尔VV的值决定了子句是否是可满足的。当存在一组逻辑变量的赋么就称之可满足的。反之，被称为不可满足的。判定fSAT问题的SAT问题进行求解，这时就需要可基本算法混合不同理论的方法，但是求解能力有限。随着2000年前后SAT速度大幅提升，转而以SAT为中心的方法。首先1999年出现Eager方法SMT问题编码SAT问题（例如32位整数32个单位变量编码），引入符号替代函数调用，使用布尔变量替代等式，同时为传递性添加约束。该方法有着一定的优点：通过将SMT预处理为等效的SAT，可以直接使用SAT求解器，并且随着时间的推移可以利用他们理论的求解算法，并且模块化程度不高，每种理论都要设计单独的编码方法，不同味着布尔SAT求解器必须发现更明显的试试。随后出现了Lazy方法，通过交用SAT求解器和各种求解器来解决SMT只需要实现公共接口就可以集成到SMT求解器中。DPLLSAT求解器，后者又通过定义明确的接口与理论求解器交互。理论求解器在探索的布尔搜索空间时，只需要担心检查从SAT求解器够给参与和分析。也就是说它必须能够从已经确立的事实中推断出新的事实，并在理论是提供对不可行的简洁出现，理论求解器必须使增量和可回溯的。DPLL算法的前提是不同理论的之间没有共享变量，不同的理论之间通过接口的函数或者谓词，理论具备stablyinfinite属性和凸包的，接口属性就只需要烤炉变量之间的等价关系。这种等价关系使有限的，可以遍历。NelsonOppen等人在中证明了SMT求解器。国外的各种科研机构都投身于此，例如微、软研究院麻省理工大学等等。这些机构研SMT求解器包Z3、STP等等。但是大多数商Z3CVC4SMT求解器已被用作计算集科学中1988Barton提出。一方面，他将种群中适应度较低的抛弃。种群中适应度高得可以通过交叉变异操作生成新1.1演化算法的流程图Fig. FlowchartofEvolutionary（1）定义和种群初始化。在算法开始之前，需要通过一定的编码方式（整数、索。一般情况下这组需要尽可能地分布在解空间，防止算法陷入局部最优。xyxy。（ondomintedSolution）间拥挤距离得这些解可能地分散帕累托沿面地不位置。比典型SGA-2，在遗传算法的基础上，采用非支配排序的概念将所有的个体划分在不同的前沿面上，然后利用拥挤距离来进一步的为同一前沿面上的进行排序。多目标演化算法相比于传统的算法的一个优点是能够得到一个最有的解集，而不是单单一个最优解。StringSMTST社区研究的重点对象。这也就导致字符试StringSMT求解器，但它们主要集中在检测其健全性错误上，只有极少数的工作专注于测试StringSMT求解器的性能问题。是该工作只支持位向量和数组理论，并不支持字符串理论。AlexandraBugariu[19]提出了一种支持字符串理论的测试方法，它生成具有已知真值的简单，并通过其变换规则推导出更复杂、可等效满足的。这两项研究都是通过生成大量的SMT实例，并记录了在过程中触发超时的测试用例。换句话说，发现的测试用例是测试SMT求解器的生成具有字符串约束的SMT实例。与其他方法相比StringFuzz在查找触发超时的测试StringSMT求解器的性能缺陷方面仍然存在两个主要:引导信息和多样性的。段的集。在像StingFuzz这样的遗传算法中，单个通过交叉操作交换，形成新的型。这样可以将一个长持续时间的结构转换为多个，这些被SMT求解为了应对这些，在本文中，我们提出了MulStringFuzz（用于字符串SMT求解器测试的多目标进化算法）SMT求解器性能缺陷。所框架结合了多目标和多样性机制，分别应对上述。一方面，为了解决引导信息，我们考虑三个目标，即与参考求解器的运行时差异、代码覆盖率得分和MulStringFuzz的基本思想是在搜索过程中使用多个优化目标来增强引导信息。我们将三个优化目标定义为适应度函数：求解器的运行时差异、代码覆盖率得分和SMT在着丰富的。主要贡本出以下贡献：我们提出了一种基于多目标进化算法MulStringFuzz用于自动生成测试用例来检测字符串SMT求解器的性能缺陷。使用目标求解器与参考求解器运情况作为指导信息，我们的算法可以保证测试SMT求解器的覆盖率；通过降低的MulString-Fuzz。结果表明，本文中的方法生成的测试用例可以覆盖的代码，测试用例的复杂度大大降低。利用求解器的动态日志组织结第一章节，介绍了可满足性模理论和SMT求解器的相关概念，阐述了SMT求解器的广泛应用以及求解器测试的重要性。介绍了本文着重关注的StringSMT求解器测试中存在的主要，并介绍了本问为了解决这些算法和框架。最后总结了SMT测试用例的运行时间分数、代码覆盖率得分和测试用第五章节，对本文算法的拓展和有效性的分析。本章小SMT求解器的相关研究背景，并介绍了相关的SMT求解器测试中的研究中存在的挑近些年来已经有很多研究工作聚焦在StringSMT求解器的测试中。本文调研了与测试和性能问题CyrilleArtho使用基于模型的测试(MBT)来测API调用的顺序和不同的系统配置[41]、NiemetzAPI模糊框架[42]SMT求解器的API使用问题等问题并没有展开详细说明。求解器的错误分2.1SMT求解器可能出现的错误分类。表左侧是测试用例应该返回的全性错误、不完整、和超时。

2.1SMTTab. ClassesofbugsinSMTACDEBACDEBCDEAB类两种错误。这两种错误求解器的的表现都是返回了错误的可满足性。A类错误是指求解器对于可满足的实例返回不可满足，B类错误是指求SMT求解器的程序分析器出现严重的错误。例如，考虑一个软件验证器（例如，Dafny[35]）或一个测试用例（例如，KLEE[19]），它们使用SMT求解器计满足。如果是B类错误，我们可以通过简单得评估求解器返回的模型来判断。假设求解器这个新的测试用例返回了flase，那就说明求解器存在B类错误。求解器有一定的概率会，也就是D类错误。在这种情况下求解器并不会返传统测试方SMT求解器的开发者发布求解器的测试套件或者人工编写测试用例对求解器进试。在求解器的初始版本时使用配套的测试套件测试效果因此这种方法并无法有效的检测出SMT求解器的缺陷。基于语法的模糊布尔运算符组合，直到只剩下一个根。使用一定数量随机生成组合成SMT求种方法可以发现SMT求解器的关键错误。满足或者不可满足的SMT，并用这些作为黑盒测试的输入。的构建分为Dominik[16]等人提出了一种语义融合的方法，他们的关键思想是融合两个现有可满足的（或者是不可满足的，将其转化为一个新的。这个新的结合了其祖ST求解器。为了保持在融合的过的可满足性是已知的，算法使用了两种基本的转化：融合函数和量x和y数f构成新量，这个函数fz倒回变量x、y。基于这两种函数就可以可满足和不可满足融合起SMT基于搜索的模糊SMT的测试用例，虽首先尝试基于搜索的模糊测试的是3的开发人员。他们首先将FuzST拓展到了字STrigu[]。工主要转化构，包了种生成结和八种转化方，可以更转换基用例或从法随机生成。在此础上，们提出使遗法搜超试的通过StinFz构初始的，以求解运行时间作适应度函数估，然后使用转器对测试用进行改变通过遗传算法的搜索，最终找到了3求解器中两个实现错误以及触发3性能缺陷的测试Joseph等人将强化学习与遗传算法结合提出了一个强化学习驱动的模糊测试工具习技术。具体的实施方法是一个语法表，这个列表可能使两个求解器之间差异最大化或者导致被测试求解器出现故障的语法结构。在每次生成遵守语法G的测工作只专注于生成各种一阶作为输入，但是忽略了SMT求解器的算法配置空间。应突变策略来促进搜索效率。给定相同的SMT如果一个选项的不同值导致求解器果集中。实验证明这种方法也是有效的，并且发现了大量z3和cvc4的缺陷。基于突变的模糊Muhd[20-25]Storm工具是一种用于检测SMT求解器中关键错误的突变测试用例。该工具不需要语法从头开始合成实例。恰恰与之相反，Storm的灵感来自与最先进的突变模糊（例如AFL），它通过改变现有的SMT测试用（也被称作）来程分为三个阶段：碎片化，生成和生成测试用例。在碎片化的过Storm会抽取谓词、碎片化的放到初始池中。文件越多，初始池中非平凡、难段被随机选择，通过逻辑AND和NOT拼接成新的。从本质上讲该阶段丰富了现有公些的组合生成新的SMT测试用例。这种方法可以利用最小的布尔但是语法完整的碎片生成新的，这样就可以构造可满足的测试用例来解决机问题。式中符合类型的运算符进行变异，以生成类型良好的突变。然后将这些突变作用域SMT求解器的测试用例。基于这种思想，他们开发了OpFuzz工具用于对SMT求解器的压力测试。OpFuzz利用类型感知运算符变异来生成测试用例输入给求解器，通过比较该测试用例在不同SMT求解器上表现出的结果并报告不一致的表现。OpFuzz需要一组和两个求解器作为输入，在算法运行的过收集触发错误的测试用例。算法开始时首先从一组种选取一个随机进行初始化，对该种的运算符了断言或者，就把这个测试用例加入到错误集合中。该工作的关键点是运算符基于逻辑近似变形的测除了上述的一些方法外，还有法通过数学上的逻辑近似来辅助测试SMT求解器[27-33]。该方法认为测试求解器的主要目的是测试机和输入的可满足性。测目标程序在多个输入及其预期输出方面的必要属性。如果SMT求解器了变形SMT问题的语义丰富性，有效地近似各种理论中的至关重要但具有些关系可以与不同的布尔连接词以复杂的方式组合。SMT问题可以描述为：项和文字。得与相似性过高，而简单的近给定中的问题可能导致非确定变异，使得的可满足性无法预测。因此作者提出了两种策略：符号谓词转换和事实谓词注入，分别通过改变谓词符号和注入片段来近似文字。在做近之前需要将转化系来对中的谓词进行近。但是这种近方式无法改变文件的结构，也就无法 本章小器的扩展时就无法应用差分测试的方法。例如Z3求解器中的“assert-soft”无法通过CVC4求解。使用机引导的方法可以通过合成可满足性已知的去进试。但是由于SMT问题固有语义的复杂性，现有的机引导技术着通用性的问题。StringSMTSMT动SMT是一阶理论的决策问题，包括整数、位向量、浮点数、string等。SMT求解String理论的开源求解器。求解器验证输SMT测试用例并返SAT/UNSAT。如果SMT求解器经过计算确定测试用例的逻辑是可以满足，就会返回SAT。否则，求解器会返回UNSAT。当SMT求解器经过长时间的计算无法得到实例的答案时，就会出现性能图3.1Fig. 性能测试的基准套件。与其他成求解器理论相比，字符串理论在基准测试方面任然此外，专门的求解器竞赛P包括许多求解器测试基准。然而关于字符串理论的测试用例很少，几乎没有检测性能缺陷的测试用例。这些都导致在检测StringSMT求解器性能缺陷方面仍然存在很大的空白。StringFuzz中提出了一种基于遗传算法的方法，它可以生成一个给定求解器需要很长时间才能求解的实例。该方法以目标求解现优秀的并删除其他。在这个方法中突变时完全随机的。图3.2Fig. 四个SMT测试用例作为在图3.1-图3.4中呈现。A和B是在StringFuzz遗传算法中通过交叉或变异操作生成。Z3str3求解器需要0.21077秒来验证A，但是B只需要0.20428秒就可以被验证。如果我们仅以时间作为单个的优化目标，在选择的过B将会被淘汰，无法参与后续的进化过程。图3.3Fig. 然而我们注意到B在运行时覆盖的代码行数比A多811行。有趣的是，通过交换节点“var”和节点“8b8”，我们可以将B转换为C，这个测试用例可以作为优化目标，可以充分搜索解空间，找到触发性能缺陷的结构。同时，我们继续研究D，它是C通过删除断言语句转换而来的。触发超时问题的结构是“(assert($>$(str.indexOf"+]YAPKJ8b8"var2var3)(var0)))”。我设SMT测试用例的复杂性也可以用作优化目标，这将有助于我们减少测试用例的大图3.4Fig. 它可以不断地参与之后的变异。如果节点再次交换，D生成一个包含“(assert($>$(str.indexOf"+]YAPKJ8b8"var3var2)(var0)))”结构的。这个在适应度评估中的表现与D基本相同（因为只交换了两个String变量名，并没有结构变体的动态执行文件之间的相似度为98.76%。因此，我们丢弃其中一个以确保我们生成框SMT实例，如群中，每代表一个SMT的测试用例。在算法的第二行到第四行是进行初始种群的的适应度评估。随后会对种群进行快速非支配。在这一步将适应度设置3.1算法一Tab. P0←GeneratePopulation(popSize) foreachind∈P0do ind.fitness←evaluate(ind) endfor fronts← Q0←selTournament(fronts, Q0←genOffspring(Q0,mutateProb,cxProb) foreachi∈[1,maxGen]do Ri←Pi-1∪Qi- foreachind∈Ri ind.fitness←evaluate(ind) endfor fronts← foreachfront∈fronts end Pi←selNSGA2(fronts, Qi←selTournamentDCD(Pi, Qi←genOffspring(Qi,mutateProb,cxProb) endfot return 定一的SMT测试用例。结基于ST-IB标准实现的。STIB理论对ST求解器输入和出准的格述在SringFuz中现了几种生成策略（被称为），它STIBSetlogiDlare、ArthektStlogicQF_S”，字串。及的在部分Dlare图1()示例的(AT)。图1()inx”描述了tr.nxbool>”运算符需要输入两个属性值为整型的节点，“.ndxfbool类型的。由于ST测试用例中可能包括多条断言语句所以采用一个列表来抽象语法树。hkt是一个固定语句，可以让求解器检查测试用例是否是可满足的。InstanceSMT3Instance的类图。我们使用三个列表来SMT测试用例的Setlogic、Assert和checksat部分。由于测试用例的变量有不同的类型，所以使用一个字典来。虽然Setlogic和checksat部分是一个固定的值，但是为了保持操作的一致性，这里依旧使用列表来表示。由于assert语整的Instace实例就生成了。Instance类包含有一些工具函数。“gen_problemInstance实例转化SMTSetlogic、Declare、Assertchecksat四个数会考虑所有断言语句中的节点来计算测试用例的复杂度，会在后续章节介绍。SMT测试用例的运行时间分数、代码覆盖率得分和测试用例的复杂SMT测试用例的运行时间分数。第一个目标函数是目标求解器和参考求解器之间有一个明确的规定。在P40分钟。时间是可以接受StringFuzz的工作中使5s作为超时时间来运行算法，这样可以减们能够最大化两SMT求解器之间的则这SMT测试用例更有可能触发目标求 𝑓𝑡(𝐼,𝑇)<𝑓𝑡(𝐼,𝑡𝑆𝑐𝑜𝑟𝑒(𝐼)={𝑓(𝐼,𝑇)+(𝑓(𝐼,𝑇)−𝑓(𝐼, 𝑓(𝐼,𝑇)>𝑓(𝐼, 我们使用$f_{t}(IT)$和$f_{t}(I,B)$IT和参考求B上被验证所需CPU运行时1展示了如SMT测试用例的运行时间分测试用I在目标T上被验证所需的时间少于参考求解B上被验证所需的时间，我们使用目标求T的运行时间作为最终分数；如果测试用I在目标求解器T上被验证所需的时间多于参考求解器B上被验证所需的时间，两者运行的验中依旧5秒作为超时时间），CVC4下运行只0.01731秒。所以这个测试用例的运行时间分数是$5+(5-0.01731)=9.98269$。SMTITB果一个测试用例在目标求解器和参考求解器上所用的时间都较长那么可能是这些测试（5秒作为时间限制难以解决的测试用例。行代码（版本号4.8.10，通过gcov测试得到的结果），而单个SMT测试用例所能覆盖因此对SMT测试用例的更改（例如对断言语句的增删查改或对断言语句点的SMT求解器代码覆因此对SMT测试用例的更改（例如对断言语句的增删查改或对断言语句点的SMT求解器代码覆过一个被广泛使用的源代码覆盖率分析和逐句分析工具Gcov来实现这一效果。c++Gcov来测量代码覆盖信息，从而计算代码Gcov通过编译选项“-fprofile-arcs”和“-ftest-coverage”应该用于目标程序以进行注释目标程序中每个语句执行次数的准确计数，“.a”文件包含了edge跳变的次数和其他的概要信息[12]；“-ftest-coverage”选项会生成“o”文件，它包含了重建基本3.1算法二Tab. covInfos←collectGcovInfo(aDir) covSocre←0 foreachfileInfos∈covInfosdo iffileInfosnotincodeInfosthen covSocre←covSocre+ foreachrow∈fileInfos ifrownotincodeInfos[fileInfos] covSocre←covSocre+100* covSocre←covSocre+10* covSocre←covSocre end end end return Gcov插桩编译求解器后，每次运行完测试用例之后都可以获得带有覆的每个语句的最大执行次数。对于每个测试用例，我们通过“*.a”文件来获1000分作为触发新代码文100来作为触发新语句的。语句出现的次数乘10来作为触发新的最大执行次数的，并且需要将这个代码语句SMT-LIB中的测试用例观察发现，影响测试用例复杂性的主要原因是其中包含的断言和节点的数量的影响，我们使用2中的方法来计算SMT实例的复杂度。𝑐𝑜𝑚𝑆𝑐𝑜𝑟𝑒(𝐼)=0−∑𝑙𝑒𝑛𝑎𝑠𝑠𝑒𝑟𝑡∑𝑑𝑒𝑒𝑝𝑎𝑠𝑠𝑒𝑟𝑡𝑖𝑗∗ 2在计算复杂性的时候，考虑所有断言语句中的节点来计算测试用例的复例如，图1(c)中的复杂度计算过程为：(1\times3+2\times1)+(1\times3+\times3+2\times1)=16，而图1(d)中的复杂度为11。由于前两个目标在优化过程算过程实现在Instance类中的“get_len”函数。遗传算[13]。在本节中会展示我们的算法中如何使用这三种算子二元竞标赛选择。在二元锦标赛选择中，从种群中随机抽取两个（注意：的每个I具有两个属性：非支配排序决定的非支配序和拥挤度。具体的比较规则如下：如果I所在的非支配序小于J，也是就I的非支配序优于J，那么就选取I；如果两个个体处在同一前沿面上，并且I有着更大的拥挤度，就选择I。这样做的目的是：一是为了保证被选择的属于较优的前沿面；其次是为了区分在同挤区域的(有较大的拥挤度)，胜出的才能进入下一阶段的操作。交叉算子。交叉操作是模仿自然界的交配过程。交配的过程会交换上的部分，从而产生新的。正如自然界中存在无性繁殖和有性繁殖一样，交叉操作也有本文的方法使用了有叉，即种群中的两个可以通过有性生殖交换彼此的基如果只进行交叉操作，可能会导致算法过早收敛。因为交叉算子只能改变的基删除变量：随机删除中的一个变量，将断言语句中出现该变量的地方替换添加断言语句：向中添加一个随机断言语句。添加断言语句时需要验证断言语更改常量：随机更改中出现的字符串或数字。替换函数类型：检查中的可修改函数，将其替换为相同类型的函数而不修改内交换同类型节点：遍历中的断言语句列表，并随机选择两个相同的节点来交换精英策现最好的（适应度评估中占优的，被称作精英）不进行配对操作直接到下携带着最优良的结构，这有利于演化算法能收敛到全局最优解。3.5精英选择策略Fig. Maintainthebestsolutionfoundovertimebeforei代产生的新种群𝑄𝑖与父代𝑃𝑖合并组成𝑅𝑖，种群的大2popSize。然后𝑅𝑖进行非支配排序，产生很多组非支配集合𝑍𝑖，并对每组非支配集合中的计算其拥挤度。子代和父代都包含在𝑅𝑖中，经过非支配排序后的非种群的大小超过了popSize，对𝑍3中的使用拥挤度比较算子，使𝑃𝑡+1数量达到本章小在本章中介绍了我们为如何解决生成SMT测试用例时的引导信息。本文设计SMT测试用例基于求解器动态文件的多样性评估方动在经典的NSGA2算法中，为了提高种群的多样性，引入了间拥挤距离和拥挤算子则是用于筛选在同一前沿面上的。通过挤距离和拥挤度的对比作为群体中之间的比较标准，使准域中的能够均匀地扩展到整个域，保证了种群中的多样性。4.1Fig. 在NSGA2算法中的拥挤距离计算方法为：首先根据适应度评估得到每个目标值的绝对差；其他目标函数采用相同的计算方法。的拥挤系数值是通过将在每例如图4.1所示，这是在有两个优化目标时形成的准前沿面。横纵坐标分别代表两个优化目标，实心的点代表其中的一个准前沿面。具体步骤如下：将每个的拥挤度𝑖𝑑置为0为无穷，即𝑂𝑑=𝐼𝑑=∞对该准前沿面的其他使用4.1计算拥挤度，其中𝑖𝑑表示点𝑖的拥挤度𝑓𝑖+1表示𝑖+1点的第𝑗个目标函数值，𝑓𝑖−1表示𝑖−1点的第𝑗 𝑖𝑑=∑𝑚(|𝑓𝑖+1− 动态日志相似测试文件的相似性的法。如图2所示，日志记录了目标程序运行时的信息Opfuzz的工作中提出图4.2C和D之间动态日志对Fig. TracelogcomparisonbetweenIndividualCandIndividual在图二的右侧展示了D被求解器验证时产生的动态文件的一部分：第30𝑠𝑖𝑚(𝐼,𝐼)=2∗ 1 ||𝐼1||+具体的计算方法如下：$\left\lVertI\right\rVert$表示日志的行数，$I_1\bigcapI_2$表示两个日志的相同部分的行数。由于动态日志记录的信息很详细，所以每次生成的文件大小在三四百MB左右，无法通过逐行遍历进行比较。我们借助了一个 进行深入比较的工具diffscope来实现。开发人员使用diffoscope来深入 使用这个方法来计算C和D的相似度：C的动态日志中包含了 个动态日志相同的行数 行。所以这两个的相似度为 ）0.374∑𝑂∈(𝑓𝑟𝑜𝑛𝑡𝑠−𝐼)𝑐𝑟𝑜𝑤𝑑𝑖𝑛𝑔𝑑𝑖𝑠𝑡(𝐼)=1−||𝑓𝑟𝑜𝑛𝑡𝑠−

作为的拥挤距离，正如4.2描述的一样。因此多样性评估的具体步骤为：本章小在本章中介绍了如何解决生成SMT测试用例时的多样性。通过使用求解器运行时的动态日志文件来度量间的相似性。我们设计了计算种群中间距离的问题1：本文基于多目标优化的算法在生成可以触发性能缺陷的SMT测试问题3：通过使用文件相似度计算拥挤距离是否可以有效的提高种群多样性？SMT测试用例方面的有效行。我们通过将本文的算法与使用单目标优化算法的StringFuzz以及我们设计的一些算法的变种进行比较来说明本文算本文中独特的拥挤距离计算方法是否有效的提高了实验设InCorei92.8GHzCPU、32GB内存的机器上运行，操作系统为Ubuntu20.04.2LTS。在运行多目标遗传算法时，我们设置种群大40，交叉概率为0.75，变异概率为0.25。个元求解器。Z3str4使用算法选择技术来完成对不可预见问题的实例求解器。每个求解直接提供使用gcov要在构建Z3求解器时时候指定“LDFLAGS、解器直接使用“--unit-testing”进行编译。除此之外，由于实验中涉及到超时的测试用例出信息信号，在执行插桩编译后的求解器时需要动态库libgcov_preload.so。SMT-LIB2.5。由于遗传算在本文的实验中，我们比较了本文中基于多目标优化的算法MulStringFuzz和基于单目标优化StringFuzz。同时本文算法设计了几种不同的变体来验证提出方法对于StringFuzz，我们设计了两种变种：Default模式和Runtime-Difference模式。异变体，即StringFuzz的默认模式。Runtime-Difference：RuntimeDifference变种以两个求解器之间的时间差为优化目标，其余部分使用StringFuzz的默认设置。对于本文算法MulStringFuzz我们设计了五种变体：DefaultOnly-Time、 试用例的动态文件的相似度计算拥挤距离。No-Coverage：该变种不使用代码覆盖率得分作为优其他策略与默认策略

实验结为了回答这个研究问题，我们比较了本文算法MulStringFuzz和采用单目标优化算StringFuzz生成的测试用例结果集。我们通过分析结果集中不同的指标来衡量结果集的效果。如表1所示，本文中使用了五个指标来对算法的运行过程和结果集进行衡量。Totlines表示算法运行中所有生成的测试用例覆盖的代码行，由每次运行算法时Avglines表示结果集中每个测试用例覆盖的平均代码行数。AvgtScore表示平均时间得5.1分栏表Tab. Resultsunderdifferent45Only-6 No-5

请注意，StringFuzzDefault变体和MulStringFuzzOnly-Time变体以单个求解器的运行时间作为优化目标，因此其平均时间得分小于5s。其他变体使用我们时间差做为优化目标，所以分数会高5s。我们还使用P所标准（以40分钟2400秒）测量结果集中测试用被求解器验证的时间。Numtimeout是2400秒超时的测试用例数。最后一个指标是plexity，它是结表一展示了算法变种的实验结果。通过totlines指标可以看到，本文基于多21188.5行代码，而单目标优化算法生成的测试用例则只能覆盖到15332.1行代码。本文MulStringFuzz在每次运行中可以多覆盖5000行代码Numtimeout的结果中可以看平均每次运行MulStringFuzz得到的结果集中比运行StringFuzz生成的结果集中多生成9个能触发求解器超时的测试用例。这一现象可以表明使用代码覆盖率信息确实有助于探索结构并生成触发5.1结果集的累积分布函数图Fig. CDFplotsofresult同时本文中的方法生成的结果集的平均复杂度仅为22.88，远低于StringFuzz的44.07。这意味着MulStringFuzz生成的测试用例可以减少两个断言语句，这点对于开发人员更快的定位到缺陷的位置十分友好。这是因为MulStringFuzz在生成的测试文件保生成的结果集数量上看，本文算法能生成触发求解器性能缺陷的测试用例。 点数赢，他只关心点数小于3的概率是多少，对于点数是1、2和3中的某一xCDF来确定取自总2400s作为超时时间来衡量结果集中的测试用中所有时间从小到大排序，绘制点(t1,1)、(t22)等，以及一般情况下(tk,k)。在不排除超时情况下，将Y轴归一化为[0,1]，就可以得到近似累积分布函数。在Satzilla的“在t秒内解决随机问题的概率是多少”。本文中则使用累积分布函数图来描述算法生在2400s的运行时间限制下，Z3str3只求解了MulStringFuzz结果集的77.5%，不到StringFuzz结果集的90%。MulStringFuzz可以找到触发求解器超时的实例。测试用例报告给Z3str3的开发人员，以帮助他们检查和解决性能缺陷。。70%1s内被求解器验证。这是因为我们的算法中包含多个现不佳。StringFuzz生成结果集中测试用例分布在5s到600s之间。由于StringFuzz运行时间限制下，Z3str3只求解了MulStringFuzz生成结果集的77.5%，与StringFuzz生成结果集的90%相比本文提出算法可以找到触发求解器超时的测试用例。实验结果表明，本文MulStringFuzz比StringFuzz生成的结果集中测试用例可以触发3.25倍的性能缺陷。MulStringFuzz生成的测试用例可以覆盖的代码语句，复杂度更低。MulStringFuzz在检测求解器性能缺陷方面优于StringFuzz。StringFuzzRuntime-differenceDefault模式生成的结果集中超时的测试用例多一个，MulStringFuzz的默认模式要比Only-Time变种多出6个超时测试用这说明无论是MulStringFuzz还是StringFuzz使间限制的（也就是我们设置的5s）。然而数测试用例在2400秒的运行时间可以看到，本文算法中Default模式和 plexity变种生成的结果集中的测试用例分别触发了求解器的13和12次超时，这远远超过了No-Coverage变种的5次，码行，并在触发超时测试用例数量上获得了优势。No-Coverage变体相当于随机选择和用例可以在相对较短的时间内被求解器验证但这些测试用例可以覆盖到求解器的代码行也就更有机会寻找到求解器的性能缺陷MulStringFuzz允许这些测试用例在种群中存活，然后参与交叉变异，可以使算法探索的结构。也就是说使用代码覆盖率分数帮助MulStringFuzz生成触发性能缺陷的测试用例，可以更好的检测求解器。最后，我们比较了使用测试用例的复杂度作为目标函数的效果。在plexity变种下生成的结果集中测试用例的平均文件复杂度为95.5，远远高于其他算法变种。也就是说使用测试用例的复杂度作为优化目标有效的限制了测试用例的膨胀。但是需要注意的是在plexity变种下，无论是算法运行期间覆盖的代码总行数，还是结果集中每覆盖情况之间存在，一个结构复杂的测试用例是可以覆盖到的代码语句。因来指导搜索过程允许MulStringFuzz找到触发性能缺陷的测试用例。我们可以清楚在本文的3.3节提出了使用求解器的动态日志来计算种群间拥挤距离的方法。为了对比本文方法与NSGA2中默认使用的拥挤距离对算法的影响，我们使01。纵坐标是拥挤距离时tscore平均值较高，可以达7-9左右，最终9左右。而使用默认拥挤距离时，平均时间score在7-8.5左右，最终收敛到8左右。不过这两种情况下两者的收敛速度并没有明显的区别，tScore的变化从45代到55代趋于平缓。这一结果说明使用求解器的动态日志来计算种群间拥挤距离并不会影响到算法的收敛速度，它只会对种群中的分布产生影响。使用本文拥挤距离计算方法有助于提高种群在目标求解器与参考求解器运行时间差上有更好的表现。从表1中的实验结果中也可以看出，本文中方法生成的结果集包含触发求解器超时 plexity变种差不多的效果， plexity变种。这证明我们使用多5.2tScoreFig. Convergencetendof5Default模式和Default-crowding变种最终生成的结果集所形成的前沿面应度值为基准，将其他的适应度标准化到区间[0,1]之间。5中两个不同算法变种产生的结果集空间分布可以看出，Default-Crowding变体在空间上更为，Default模式下产生的更为均匀的分布在解空间之中实际上我们对结果集空间分布上在一起的进行了分析，发现在其中存在着大量相似的结图5.3默认策略的前沿分Fig. ParetooptimalfrontofDefault但是对于我们想要的搜索解空间而言，如果存在大量相同的结构，他们会在适应在搜索过，如果使用默认的拥挤距离计算方法并不能提高种群多样性，这并挤距离将区分开，但是实际上这些中存在着大量相似的结构。在后续的交叉变异操作时就会产生很多相似的，导致在之后的迭代中种群多样性下降。如果使用求解器的动态日志来计算种群间拥挤距离，可以使得带有相同结构的的拥挤度较高，然后在选择操作中被丢弃掉。这样可以使新的结构可以出现在个 5.4本文中的方法Fig. 当使用相同的参数运行两种算法变体时，默认模式所花费的总体的时间是Default-crowding变种的两倍之多。交叉概率设置为0.75，将变异概率设置为0.15。接下来主要分析种群大小的设置对种群的大小是指在运行算法时种群中包含的数量，如果在种群中有包含 、、和100情况下运行了算法，左图Fig. Timeoutcasesnumberindifferentpopulation5.6Fig. Convergencetimeindifferentpopulation6060时，[40,60]。这个区间内的人口规模可以最大限度地利用计算资源本章小方法CPU和内存。也就是说我有效性CPU和更大的内存可以使求解运行内存限制为8GB，并且程序都是单线程运行的。其次在实验评估的过，我们没数，因此我们需要使用Gcov来插桩编译目标求解器，这将减少我们可以选择的求解器的数量。为了尽量减少这种，我们选择z3str3作为我们实验的目标求解器，因为它2.5语法的，它是SMT-LIB的版本之一。由于SMT-LIB各个版本的语法差异，测试容的SMT-LIB2.5。对于其他版本的SMT-LIB标准，我们只需要更改与相关的一些操关内容，并不会影响算法的其他部分，本文方法依旧时有效的。本章小 在本文中，我们提出了一种多目标进化算法MulStringFuzz，用于生成测试用例以们使用代码覆盖率分数来鼓励算法探索的解决方案空间，并在SMT实例上引入复实验结果表明，我们的算法可以生成触发求解器超时的测试用例，可以有效地检测求解器的性能缺陷。平均而言，MulStringFuzz生成的测试用例可以比StringFuzz多覆5000MulStringFuzz触发的性能缺陷是StringFuzz3.25倍。重要的是，可以有效降低生成结果集中的复杂度。同时，我们利用tracelog的相似度 王翀,吕荫润,陈力,等.SMT求解技术的发展及应用研究综述[J].计算机研究与发展,2017,54(7):1405-1425.J2018,45(6A28-SMT[J].2019,29(1):261-265.BiereA,CimattiA,ClarkeEM,etal.Boundedmodelchecking[J].YingM.Floyd--hoarelogicforquantumprograms[J].ACMTransactionsonProgrammingLanguagesandSystems(TOS),2012,33(6):1-49.MadsenM,AndreasenE.Stringysisfordynamicfieldaccess[C]//InternationalConferenceonCompilerConstruction.Springer,Berlin,Heidelberg,2014:197-217.SamimiH,SchäferM,ArtziS,etal.AutomatedrepairofHTMLgenerationerrorsinPHPapplicationsusingstringconstraintsolving[C]//201234thInternationalConferenceonSoftwareEngineering(ICSE).IEEE,2012:277-287.SamimiH,SchäferM,ArtziS,etal.AutomatedrepairofHTMLgenerationerrorsinPHPapplicationsusingstringconstraintsolving[C]//201234thInternationalConferenceonSoftwareEngineering(ICSE).IEEE,2012:277-287.ParkC,ImH,RyuS.PreciseandscalablestaticysisofjQueryusingaregularexpression[C]//Proceedingsofthe12thSymposiumonDynamicLanguages.2016:25-36.BangL,AydinA,PhanQS,etal.Stringysisforsidechannelswithsegmentedoracles[C]//Proceedingsofthe201624thACMSIGSOFTInternationalSymposiumonFoundationsofSoftwareEngineering.2016:193-204.2021,17(16):3.[J].[J械科学与技术,2013,32(3):5.MansurMN,ChristakisM,WüstholzV,etal.DetectingcriticalbugsinSMTsolversusingblackboxmutationalfuzzing[C]//Proceedingsofthe28thACMJointMeetingonEuropeanSoftwareEngineeringConferenceandSymposiumontheFoundationsofSoftwareEngineering.2020:701-712.WintererD,ZhangC,SuZ.ValidatingSMTsolversviasemanticfusion[C]//Proceedingsofthe41stACMSIGNConferenceonProgrammingLanguageDesignandImplementation.2020:718-730.WintererD,ZhangC,SuZ.Ontheunusualeffectivenessoftype-awareoperatormutationsfortestingSMTsolvers[J].ProceedingsoftheACMonProgrammingLanguages,2020,4(OOPSLA):1-25.BrummayerR,BiereA.Fuzzinganddelta-debuggingSMTsolvers[C]//Proceedingsofthe7thInternationalWorkshoponSatisfiabilityModuloTheories.2009:1-BlotskyD,MoraF,BerzishM,etal.Stringfuzz:Afuzzerforstringsolvers[C]//InternationalConferenceonComputerAidedVerification.Springer,Cham,2018:45-51.BiereA,HeuleM,vanMaarenH,etal.HandbookofSatisfiability,volume185ofFrontiersinAIandApplications[J].2009.MouraL,BjørnerN.Z3:AnefficientSMTsolver[C]//InternationalonToolsandAlgorithmsfortheConstructionandysisofSystems.Springer,Berlin,Heidelberg,2008:337-340.BarrettC,ConwayCL,DetersM,etal.Cvc4[C]//InternationalConferenceonComputerAidedVerification.Springer,Berlin,Heidelberg,2011:171-177.JinG,SongL,ShiX,etal.Understandinganddetectingreal-worldperformancebugs[J].ACMSIGNNotices,2012,47(6):77-88. p2021,”[EB/OL], p..io/2021/AccessedMay31,DebK.Multi-objectiveoptimization[M]//Searchmethodologies.Springer,Boston,MA,2014:403-449.DebK,AgrawalS,PratapA,etal.Afastelitistnon-dominatedsortinggeneticalgorithmformulti-objectiveoptimization:NSGA-II[C]//Internationalconferenceonparallelproblemsolvingfromnature.Springer,Berlin,Heidelberg,2000:849-858.BöhmeM,PhamVT,RoychoudhuryA.Coverage-basedgreyboxfuzzingasmarkovchain[J].IEEETransactionsonSoftwareEngineering,2017,45(5):489-506.ChenH,XueY,LiY,etal.Hawkeye:Towardsadesireddirectedgrey-boxfuzzer[C]//Proceedingsofthe2018ACMSIGSACConferenceonComputerandCommunicationsSecurity.2018:2095-2108.LiY,XueY,ChenH,etal.Cerebro:context-awareadaptivefuzzingforeffectivevulnerabilitydetection[C]//Proceedingsofthe201927thACMJointMeetingonEuropeanSoftwareEngineeringConferenceandSymposiumontheFoundationsofSoftwareEngineering.2019:533-544.WangJ,ChenB,WeiL,etal.Skyfire:Data-drivenseedgenerationforfuzzing[C]//2017IEEESymposiumonSecurityandPrivacy(SP).IEEE,2017:579-KhouryR,HalléS,WaldmannO.ExecutionTraceysisUsingLTL-FO[C]//InternationalSymposiumonLeveragingApplicationsofFormalMethods.Springer,Cham,2016:356-362.M,OberleitnerJ,GallH,etal.Systemevolutiontrackingthroughexecutiontraceysis[C]//13thInternationalWorkshoponProgramComprehension(IWPC'05).IEEE,2005:237-246.XuL,HutterF,Ho