论文分享_08_10

复杂字符串约束的化简规则

          今天分享的论文是发表在CAV2019的一篇文章High-Level Abstractions for Simplifying Extended String Constraints in SMT,作者是Andrew Reynolds等人。

摘     要

       含字符串理论的SMT求解器是分析字符串操作相关程序的有力工具,它们的求解能力受制于复杂的字符串操作如substring和contains等。本文作者为了提高SMT求解器对于字符串理论的求解能力,从输入的字符串约束中生成线性算术公式、多重集抽象(multiset abstraction)和字符串包含(contains),并基于这三种生成关系对输入的字符串约束进行化简,使其更容易被求解。

本文的贡献有四点

  1. 从输入的字符串约束中生成线性算术公式,并基于线性算术公式进行化简;
  2. 从输入的字符串约束中生成字符串包含,并基于字符串包含进行化简;
  3. 从输入的字符串约束中生成多重集抽象,并基于多重集抽象进行化简;
  4. 在相同的测试用例上和目前最好的求解工具进行对比,证明了化简规则的有效性。

记号

一、要化简的字符串理论

         本文要化简的字符串理论主要包含了字符串和整数两种类型,并囊括了contains、substring、indexof等复杂的字符串函数,具体的形式化定义如下图:

1、基于线性算数公式的化简规则

2、基于字符串包含的化简规则

3、基于多重集抽象的化简规则

二、实验结果

        并分别对比了-arith、-contain、-msets三种化简策略和-all化简策略在相同测试集上使用的时间,发现-all化简策略的测试时间在unsat的例子上远远低于其他三种策略,说明了这三种化简规则都是必不可少的。