arXiv 1807.091752018-07cs.LOcs.PL

用Word公式作为约束的字符串程序超编译

Supercompiling String Programs Using Word Equations as Constraints

Antonina Nepeivoda

摘要：

我们描述了一个通用的参数化方案的程序和约束分析，使我们能够指定两个程序的专业化方法称为Turchin的超级编译和Hmelevskii的算法求解二次方程。该方案是指定的两种分析和工程中的联合算法，其中这两种分析一起使用。该算法使用词方程和正则模式上的不等式作为字符串约束语言。

英文摘要：

We describe a general parameterized scheme of program and constraint analyses allowing us to specify both the program specialization method known as Turchin's supercompilation and Hmelevskii's algorithm solving the quadratic word equations. The scheme is specified for both sorts of the analysis and works in a joint algorithm in which these two sorts of the analysis are used together. The word equations and the inequalities on regular patterns are used as the string constraint language in the algorithm.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

用程序变换法解Word方程

On Solving Word Equations via Program Transformation

本文给出了一个通过特殊化配置WE（R，E）来求解文字方程的实验，其中程序WE可以被看作是一个解释器，用来测试替换R的组合是否产生文字方程E的解。这种解释器的几个变体，当专门使用基本的展开/折叠策略时，能够确定具有重叠变量的多组单词方程的可解性。

2021-06-19cs.LOcs.PL

程序特化作为求解Word方程的工具

Program Specialization as a Tool for Solving Word Equations

本文研究了词方程可满足性问题的证人的自动生成问题，通过专门化一个解释器来测试给定词方程系统的变量替换的组合是否产生它的解。我们专门聘请这样的翻译。方程系统，而替代是未知的。我们表明，这样的解释器的几个变种，专门使用基本的展开/折叠专业化方法时，能够构建整个解决方案集的某些类的字方程的左侧和右侧共享变量。我们证明了构造的解释器的专门化过程给出了所考虑的方程的可满足性的一个简单的语法标准，并表明所建议的方法可以解决Z3 str 3和CVC 4，广泛使用的SMT求解器无法解决的一些方程。

2021-09-07cs.LOcs.PL

用词方程和转换器求解字符串：分析突变的逻辑XSS（完整版）

String Solving with Word Equations and Transducers: Towards a Logic for Analysing Mutation XSS (Full Version)

我们研究了以连接和有限状态转换器作为原子操作的弦逻辑的可满足性的判定性的基本问题。虽然限制到一种类型的操作产生的可判定性，很少有人知道他们的组合理论，这是特别相关的动态网页在一个更现实的浏览器模型的安全漏洞分析时的可判定性。一方面，单词方程（带有连接的字符串逻辑）不能精确地捕获清理功能（例如htmlescape）和隐式浏览器转换（例如innerHTML突变）。另一方面，转换器遭受能够对消毒功能和浏览器转换建模，但不能对字符串连接建模的相反问题。简单地将词方程和转换器组合在一起很容易导致不可判定的逻辑。我们的主要贡献是表明，“直线片段”的逻辑是可判定的（复杂性范围从PSPACE到EXPSPACE）。该片段可以表达的程序逻辑的直线字符串操作程序的连接和转换作为原子操作，这出现在执行有界模型检验或动态符号执行。我们证明了逻辑可以自然地表达分析Web应用程序中的突变XSS所需的约束。最后，在存在长度、字母计数、正则、indexOf和不等性约束的情况下，逻辑仍然是可判定的。

2015-11-05cs.LO

结合词方程、正则表达式和长度约束的可判定逻辑

Decidable Logics Combining Word Equations, Regular Expressions and Length Constraints

在这项工作中，我们考虑的可满足性问题的逻辑，结合字方程的字符串变量表示的话的无限长度，正则语言的话属于Presburger限制的话的长度。我们提出了一种新的决策过程，在两个可决策的片段，包括二次字方程（即，每个字符串变量最多出现两次）。所提出的过程减少了问题解决的Presburger算法的可满足性。该过程结合了两个主要组成部分：（i）一个算法，以获得一个完整的一组所有的解决方案的词方程和正则表达式的连接;和（ii）两种方法，以精确计算关系约束的字符串长度所隐含的所有solutions.We已经实现了一个原型工具，并评估了一组可满足性问题的逻辑。实验结果表明，该工具是有效和高效的。

2018-05-23cs.LO

并行超边替换字符串语言

Parallel Hyperedge Replacement String Languages

有许多悬而未决的问题，围绕着群体的特点与上下文敏感的文字问题。直到2018年，才发现所有由双曲群生成的几乎阿贝尔群都有多个上下文无关的词问题，而双曲群的词问题在形式语言层次结构中的位置是一个长期存在的开放问题。在本文中，我们介绍了一个新的语言类称为并行超边替换字符串语言，它包含所有多个上下文无关和ET0L语言，并奠定了基础，为未来的工作，可能能够放置在这个类的字的问题，许多双曲群。

2021-02-04cs.FLcs.LO

Word Equations in Synergy with Regular Constraints（技术报告）

Word Equations in Synergy with Regular Constraints (Technical Report)

吃意大利面时，要把酱汁和面条混在一起吃，不要分开吃。我们认为，也在字符串求解，字方程和定期约束更好地混合在一起，而不是单独接近，在目前的字符串求解。我们提出了一个快速算法，完全的无链约束的片段，其中字方程和正则约束是紧密集成和交换信息，有效地修剪彼此产生的情况下，限制可能的组合爆炸。该算法是基于一种新的语言为基础的字符的可满足性的文字方程与定期约束。我们的实验表明，我们的原型实现是最好的字符串求解器的竞争力，甚至更优越，因为它是最快的困难的例子，并具有最少的超时。

2022-12-05cs.FLcs.LO

更多相关论文收起更多论文

带长度约束的二次字方程、计数器系统和带整除性的Presburger算术

Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility

词方程是弦上约束求解理论基础中的一个重要组成部分，近年来受到了广泛的关注。一个词等式将两个词与字符串变量和常量联系起来。它的解决方案相当于一个函数，将变量映射到常量字符串，使等式的左侧和右侧相等。虽然求解词方程的问题是可判定的，但是求解具有长度约束的词方程的问题的可判定性（即，与词等式中的词的长度相关的约束）仍然是一个长期存在的公开问题。在本文中，我们专注于二次字方程的子类，即，其中每个变量最多出现两次。我们首先表明，二次字方程的解决方案的长度抽象一般不Presburger定义。然后，我们描述了一类计数器系统的Presburger转换关系，捕获的长度抽象的二次词方程与定期约束。我们提供了存在性普雷斯伯格整除算术（PAD）理论中计数器系统简单循环效果的编码。由于PAD是可判定的，我们得到了具有长度约束的二次字方程的判定过程，其中相关的计数器系统是\emph{flat}（即，所有节点属于至多一个循环）。我们展示了一个可判定性的结果（事实上，也是一个NP算法与PAD甲骨文）最近提出的NP-完整片段的字方程称为定期面向字方程，连同长度限制。当约束被额外扩展为具有1-弱控制结构的常规约束时，判定性成立。

2018-05-17cs.LO

字符串中朴素模式匹配程序模型的特殊化（扩展抽象）

On Specialization of a Program Model of Naive Pattern Matching in Strings (Extended Abstract)

我们证明了对于任何模式p，朴素模式匹配的尾递归程序模型可以自动地特化为w.r.t.模式p到所谓的KMP算法的专门版本，使用控制展开/折叠的Higman-Kruskal关系。给定一个输入字符串，相应的残差程序在线性时间内找到字符串中第一次出现的p。基于展开/折叠的自动化程序专业化技术的当前状态太弱，以便能够再现手工完成的上述统一属性的证明，而在此之前已知程序专业化有时能够为一些具体的静态模式产生KMP算法。

2021-08-23cs.DScs.LOcs.PL

具有长度和正则表达式约束的字方程的（Un）可判定性结果

(Un)Decidability Results for Word Equations with Length and Regular Expression Constraints

我们证明了几个可判定性和不可判定性结果的可满足性和有效性问题的语言，可以表示解决方案的字方程的长度约束。这种语言上的原子公式是字符串项上的等式（单词等式）、长度函数上的线性不等式（长度约束）和正则集中的成员资格。这些问题在逻辑、程序分析和形式化验证中很重要。这些问题的变体已经被数学家研究了几十年。最近，这些公式的实际可满足性程序（又名SMT求解器）在字符串操作程序（如Web应用程序）的安全分析中变得越来越重要。我们证明了三个主要定理。首先，我们给出了一个新的证明不可判定的有效性问题的一组句子写为一个forall-exists量词交替应用于正字方程。这个不可判定性结果的一个推论是，这个集合是不可判定的，即使句子中最多出现两次字符串变量。第二，我们考虑布尔组合的量词自由公式构建的词方程和长度约束。我们表明，如果字方程可以转换为一个解决的形式，在实践中相关的形式，然后满足性问题的布尔组合的字方程和长度约束是可判定的。第三，我们证明了无量词公式在正则解形式、长度约束和正则表达式上的成员谓词上的可满足性问题也是可判定的。

2013-06-25cs.LO

一个符号算法的情况下分裂规则在解决词的约束与扩展（技术报告）

A Symbolic Algorithm for the Case-Split Rule in Solving Word Constraints with Extensions (Technical Report)

案例分割是当前字符串约束理论决策过程中的一个核心证明规则。它的使用是字符串约束求解中状态空间爆炸的主要原因，因为它是在证明树中创建分支的唯一规则。此外，显式处理的情况下分裂规则可能会导致重新计算相同的任务在多个分支的证明树。在本文中，我们提出了一个符号算法，显着减少这样的冗余。特别是，我们将字符串约束编码为正则语言，并将证明规则编码为理性转换器。这允许我们在证明树中只执行一次类似的步骤，从而缓解状态空间爆炸。我们还扩展了编码，以处理字符串约束，长度约束和常规约束的任意布尔组合。在我们的实验结果中，我们验证了我们的技术在许多其他最先进的求解器无法提供答案的实际情况下有效;我们的Python原型实现解决了超过50%的其他工具无法解决的字符串约束。

2023-03-02cs.LO

一种判定具有非数据类型的字符串操作程序路径可行性的方法

A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type

字符串广泛用于程序中，特别是Web应用程序中。字符串数据类型自然出现在字符串操作程序中，并且经常用于引用字符串的长度或位置。字符串操作程序的分析和测试可以表述为路径可行性问题：给定一个符号执行路径，是否存在对输入的赋值，从而产生实现该路径的具体执行？这样的问题可以自然地重新表述为字符串约束求解问题。虽然最先进的字符串约束求解器通常提供对字符串和整数数据类型的支持，但它们主要采用没有完整性保证的解析法。在本文中，我们提出了一类字符串操作程序，其中不仅包括广泛的字符串操作，如串联，replaceAll，反向，有限的转换器，但也涉及整数数据类型，如长度，indexof，和子串的决策过程。据我们所知，这是目前已知的最具表现力的字符串约束语言之一。我们的决策过程是基于一个变种的成本寄存器自动机。我们实施的决策过程，从而产生一个新的解决方案OSTRICH+。我们在广泛的现有和新的基准上评估OSTRICH+的性能。实验结果表明，OSTRICH+是第一个字符串决策程序能够处理有限的传感器和整数约束，而其整体性能是最先进的字符串约束求解器相媲美。

2020-07-14cs.FLcs.LO

面向测试数据生成的字符串约束逻辑程序设计

Towards Constraint Logic Programming over Strings for Test Data Generation

为了正确地测试软件，需要一定质量的测试数据。然而，有用的测试数据通常是不可用的：现有的或手工制作的数据可能不够多样化，无法实现所需的测试用例。此外，由于安全或隐私问题或其他法规，可能会禁止使用生产数据。同时，用于测试数据生成的现有工具通常是有限的。在本文中，我们评估在何种程度上约束逻辑编程可以用来生成测试数据，特别是字符串集中。要做到这一点，我们介绍了一个原型CLP求解器字符串约束。作为案例研究，我们使用它来生成IBAN号码和日期。

2019-08-27cs.LOcs.SE

带长度约束的二次词方程、计数器系统与带可除性的普雷斯堡算术

Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility

本文研究带长度约束的二次词方程的可判定性，通过计数器系统与带可除性的普雷斯堡算术编码，证明了平坦情形下可判定，并扩展至正则定向词方程。

2021-10-28cs.FLcs.LO

部分弦的并发Kleene代数

Concurrent Kleene Algebra of Partial Strings

并发Kleene代数（CKA）是Hoare等人最近提出的一种代数结构，它统一了并发编程的规律。CKA的统一力量主要依赖于所谓的交换定律，该定律描述了并发和顺序组合操作符如何互换。本文在前人对真并发性理论研究的基础上，利用最小不动点算子扩展了Gischer的pomset模型，并利用Ésik的单调双射态射形式化了程序精化关系，构造了CKA的偏序模型.当我们想证明和反驳带有循环的并发程序的性质时，这种模型的存在是相关的。特别是，它提供了一个基础的分析程序，同时访问放松的内存中所示的后续工作。

2014-10-17cs.LO

活性验证与综合：递归程序的新算法

Liveness Verification and Synthesis: New Algorithms for Recursive Programs

我们考虑递归程序的活性验证和活性合成问题。活性验证问题（LVP）是判定给定的omega-正则语言是否包含给定的omega-上下文无关语言。活性合成问题（LSP）是计算一个策略，使得当沿着该策略进行给定的omega-上下文无关游戏时，保证导出给定omega-正则语言中的单词。这两个问题分别是EXPTIME完全问题和EXPTIME完全问题。我们的贡献是新的算法具有最佳的时间复杂度。对于LVP，我们概括了最近的拉索发现算法（也称为拉姆齐算法）从有限递归程序。对于LSP，我们概括了最近的摘要为基础的算法从有限到无限的话。Lasso查找和摘要已被证明在有限状态和有限字设置的许多实现中是有效的。

2017-01-11cs.FLcs.LO

复杂操作字符串操作程序路径可行性的判定方法

Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations

字符串操作程序中路径可行性检测决策过程的设计与实现是一个重要的问题，其应用包括符号执行和跨站脚本（XSS）漏洞的自动检测。（符号）路径是赋值和断言的有限序列（即没有循环），并且检查其可行性相当于确定产生成功执行的输入的存在。我们给出了两个一般的语义条件，共同确保路径可行性的可判定性：（1）每个断言承认定期一元分解，（2）每个分配使用（可能是不确定的）函数，其逆关系保持规律性。我们表明，这些条件是表达，因为他们是由众多的字符串操作满足。他们也严格地支持现有的可判定弦理论和大多数现有的基准（例如卡鲁扎的大部分，以及所有的Slove，Stranger和Sloth）。我们给出了一个简单的决策过程和一个可扩展的体系结构的字符串求解器中，用户可以很容易地将他/她自己的字符串函数。我们发现一般的片段有一个紧密的，但高的复杂性。为了解决这个问题，我们建议只允许部分字符串函数（即，禁止非确定性）在条件（2）中。当需要非确定性函数时，我们还提供了一个语法片段，它提供了对非确定性函数的支持，但可以简化为现有的求解器SLOTH。我们提供了一个有效的实现我们的决定过程中确定性的部分字符串函数在一个新的字符串求解器OSTRICH。它提供了对串联、反向、函数转换器和replaceall的内置支持，并提供了一个可扩展的框架，以支持更多的字符串函数。我们证明了我们的新求解器对其他竞争对手的求解器的功效。

2018-11-07cs.FLcs.LO