软件分析第二次大作业

算法一

算法概述

实现了类似EUSolver的基于多标签决策树的枚举算法，并且对于当前任务做了一些优化。算法可以在很多数据集(如 array_search 系列)上迅速求出简洁的程序，但在一些程序上效率较低。由于算法二已经完成通过 open_test 中的所有测试用例的目标，目前未尝试继续优化。

在 array_search_15 数据上，只需要 8s 即可得到下面的程序：

(define-fun findIdx ((y1 Int) (y2 Int) (y3 Int) (y4 Int) (y5 Int) (y6 Int) (y7 Int) (y8 Int) (y9 Int) (y10 Int) (y11 Int) (y12 Int) (y13 Int) (y14 Int) (y15 Int) (k1 Int)) Int
    (ite (< k1 y8)
        (ite (< k1 y4)
            (ite (< k1 y2)
                (ite (< k1 y1) 0 1)
                (ite (< k1 y3) 2 3))
            (ite (< k1 y6)
                (ite (< k1 y5) 4 5)
                (ite (< k1 y7) 6 7)))
        (ite (< y12 k1)
            (ite (< k1 y14)
                (ite (< k1 y13) 12 13)
                (ite (< k1 y15) 14 15))
            (ite (< k1 y10)
                (ite (< k1 y9) 8 9)
                (ite (< k1 y11) 10 11)))))

可以注意到它找到的解采用了优雅的二分查找的算法，并且在后面的讨论中我们可以看到，算法的搜索过程会迅速收敛到合适的解上。

算法过程

算法主要分为预处理，枚举，和决策树学习三个步骤：

1. 预处理阶段对约束进行预处理，简化条件，并转化为易于处理的形式，同时求出算法的所有可能输出作为标签，以便决策树算法进行分类。
2. 算法通过标准的枚举算法生成决策树判断条件
3. 计算每个样例点对应的标签，通过ML-DT决策树算法学习一棵决策树。该决策树即是生成的程序，若该程序存在不满足约束的反例，则加入新的样例点，重复进行3直到学习到一棵不存在反例的决策树。

目前此算法只能处理对于每个反例点，约束中的所有函数调用共享输入的情形，如果不能变换到该情形则无法处理。

预处理

注意到输入的约束的形式实际上是多个子句的合取，但由于子句可以任意复杂，可能存在冗余，且可能含有大量不同运算符影响算法进行，故算法第一步是将约束化为标准形式。算法会将输入的约束首先化为合取范式，这就可以保证每个子句中的逻辑运算符只含有或和非，然后算法会通过 SMT Solver 求解约束间的等价性，去除相同的或平凡的约束，从而达到约束的简化。

在简化后的约束中依然会存在一些如下的约束影响决策树学习中的标签计算：

(declare-var x Int)
(constraint (= (f 1) 1))
(constraint (= (f 2) 2))
....

对于样例点 x = 1，f(x) = 1 应当是其标签，但是当我们将该函数和样例点直接代入时会发现该式为加，因此应将输入变换为 "Guarded" 形式如下：

(constraint (or (= (f x) 1) (not (= x 1))))
(constraint (or (= (f x) 2) (not (= x 2))))

这时就可以直接代入求解了。同时代换过程中可以判断是否存在不能处理的输入，若存在则放弃用此算法计算。

下面是 s1.sl 经过预处理后得到的约束

(constraint (or (= (f x) 0) (not (= x 0))))
(constraint (or (= (f x) 10) (not (= x 1))))
(constraint (or (= (f x) 20) (not (= x 2))))
(constraint (or (= (f x) 30) (not (= x 3))))
(constraint (or (= (f x) 40) (not (= x 4))))
(constraint (or (= (f x) 50) (not (= x 5))))
(constraint (or (= (f x) x) (<= x 5)))

可以看到所有的函数调用共享参数，并且多余的 $x > 5$ 的条件已经被去除。

在约束经过预处理后，算法会计算出所有可能作为返回值的表达式集合，该过程与算法二中的第一部分相同。若不进行此计算，算法也可以通过标准的枚举算法来枚举返回值，但这会带来很大的效率下降。

枚举条件

采用标准的枚举算法对条件进行枚举，注意到用 ite 语句的嵌套组合可以表达所有的 and 和 or 条件，因此只需要生成由比较运算符连接的简单条件即可，但在实际计算过程中，由于含有 and 和 or 的条件的表达式比较大，因此会在算法后期才会被枚举出来，因此不需要特殊处理。

决策树学习

给定当前样例集合和条件语句集合，算法会利用通用的多标签决策树算法进行学习。

在该学习任务中，标签集合是所有可能返回语句，被分类集合为样例集合。对于每一个样例，我们求出满足约束的所有返回语句集合，这个过程可以通过对 LIA 文法的解释执行完成。

以下定义 $T$ 为标签集合，$C$ 为样例集合，$\mathrm{label}(c)$ 表示样例 $c$ 的标签，$\mathrm{cover}(t)$ 表示标签 $t$ 覆盖的样例。

决策树的内部节点由条件语句组成，条件语句 $p$ 将样例集合 $C$ 划分为两个集合 $C_t$， $C_f$，按照标准的 ML-DT 算法这个过程中的信息量提升由下式给出 $$ G(p) = \frac{|C_t|}{|C|}\cdot H(C_t) + \frac{|C_f|}{|C|}\cdot H(C_f) $$ 其中 $H(\cdot)$ 为某个样例集合对应的信息熵，由下式给出 $$ H(C_0) = -\sum_{t\in T}\mathbb{P}{C_0}(\mathrm{label}(c) = t)\cdot\log_2\mathrm{P}{C_0}(\mathrm{label}(c)=t) $$ 其中概率可以在均匀标记的假设下利用全概率公式推出 $$ \mathbb{P}{C_0}(\mathrm{label}(c)=t\mid c) = \left{\begin{array}{ll} 0&\mathrm{if}, c\not\in \mathrm{cover}(t)\ \displaystyle\frac{|\mathrm{cover}[t]\cap C_0|}{\displaystyle\sum{t', c\in\mathrm{cover}(t')}|\mathrm{cover}[t']\cap C_0|} & \mathrm{if}, c\in \mathrm{cover}(t) \end{array} \right. $$

$$ \mathbb{P}{C_0}(\mathrm{label(c) = t}) = \frac{1}{|C|}\cdot\sum{c\in C_0}\mathbb{P}_{C_0}(\mathrm{label}(c) = t\mid c) $$

决策树算法通过最大化信息增量来选取每一步的分支策略，从而实现学习，并且可以达到良好的泛化性能，从而不需要进行太多步的穷举就能得到满足约束的解。

SMT Solver 生成反例的质量控制

决策树算法作为数据驱动的机器学习算法，其泛化性能与数据集质量关系非常大，如果不对数据集质量进行控制，算法会在 $x>0$ 等分支条件上浪费太多时间，因此需要控制 SMT Solver 给出的数据集质量。在本次任务中由于限定文法在 LIA 上，我们可以采用如下的简单而有效的算法来控制生成反例的质量：在最开始的时候求出所有可能取的常量的最大值和最小值，生成额外约束要求生成的反例的每个输入变量均大于这个最大值，或者小于最小值，这样就能有效的避免过度与常数比较而过拟合。

如果发现在额外约束条件下，无法生成反例，那么就将额外约束逐个放松，然后判断是否有反例。如果所有的额外约束均已放松，仍然不能找到反例，那么算法结束，输出解。

算法二

算法概述

设计了一个较为高效的 Example Based Synthesis 算法，具有如下的特点：

1. 效率高，可以在时间限制能正确生成本次大作业 open_tests 中的所有测试用例。

2. 结果简洁，下面是本算法生成的两个例子：

   (define-fun max6 ((x1 Int) (x2 Int) (x3 Int) (x4 Int) (x5 Int) (x6 Int)) Int (ite (and (and (and (and (<= x2 x1) (<= x3 x1)) (<= x4 x1)) (<= x5 x1)) (<= x6 x1)) x1 (ite (and (and (and (<= x3 x2) (<= x4 x2)) (<= x5 x2)) (<= x6 x2)) x2 (ite (and (and (<= x4 x3) (<= x5 x3)) (<= x6 x3)) x3 (ite (and (<= x5 x4) (<= x6 x4)) x4 (ite (<= x6 x5) x5 x6))))))

   (define-fun findIdx ((y1 Int) (y2 Int) (y3 Int) (k1 Int)) Int (ite (or (or (or (or (<= y2 y1) (<= y3 y2)) (<= k1 y1)) (= y3 k1)) (= y2 k1)) 0 (ite (<= k1 y2) 1 (ite (<= k1 y3) 2 3))))

   其中第一个程序是 max6 的答案，第二个程序是 array_search_3。值得注意的是，在 array_serach_3 中，并没有对序列无序或者 $k1$ 和数列中某一个元素值相同的情况进行约束，可以发现在我们的算法把这个约束准确地求出了。

算法过程

算法主要分成三部分：

1. 求出可能作为返回值的表达式集合（不含 ite） $R$。
2. 求出可能出现在 if 条件里的比较表达式（形如 $x \leq, <, = y$）集合 $C$。
3. 对 $R$ 中的每一个元素生成一个它作为返回值的条件（以析取范式的形式）。

目前本算法只能处理在输入中，所有输入均以 $(f\ x\ y\ z)$ 形式出现的情况。因此在读入输入的时候，算法会先尝试把所有 $f$ 的调用变换成相同的形式，碰到不能变换的情况（例如一个等号两端出现了参数不同的两次调用）会转而用更加暴力的方法求解。

这儿定义 $\phi_t(I)$ 为把输入约束中的所有 $(f\ x\ y\ z)$ 都替换成表达式 $t$ 后的约束，其中 $I$ 为输入变量。

第一部分

可以判断一个表达式集合 $R$ 是否覆盖了 $f$ 的所有返回值，即下列布尔表达式不可满足： $$ \neg (\phi_\text{value}(I)) \wedge \bigvee_{t \in R} [\text{value} = t]) $$ 因为在测试集中，返回值的形式都非常简单，因此这儿使用最暴力的方法，令 $R(k)$ 为包含 $k$ 个运算符（不含 ite）的所有表达式集合，直接找到最小的 $k$ 使得 $R(k)$ 满足条件。

因为这样找到的 $R(k)$ 非常大，因此使用了简单的二分来去重，找到一个极小的满足条件集合作为 $R$ 返回。因为在 Int 范围内，很难出现两个不同的表达式集合 $A,B$ 对应的取值集合是完全相同的情况，因此该算法能非常精确的找到 $R$。

当返回值形式比较复杂的时候，也可以用一个 example based synthesis 来生成表达式（每次找到一个反例再生成一个表达式覆盖它）。

第二部分

因为测试集中，条件判断的形式都非常简单，因此这儿令 $C(k)$ 为包含 $k$ 个运算符的比较表达式。从小到大依次尝试用 $C(k)$ 进行生成，直到正确的生成出程序为止。

第三部分

我们以析取范式的形式来生成答案，即对每一个返回值，生成一系列的集合 $P_i \subseteq C$，对应的布尔表达式为: $\bigvee_{P_i} \bigwedge_{t \in P_i} t$.

设 $R$ 中的元素为 $t_1$ 至 $t_n$，当前正在生成 $t_k$，设 $t_1$ 至 $t_k$ 目前已有的条件为 $f_i(I)$。则可以从如下约束来生成一个返回值应该是 $t_k$ 且不能被当前表示的 example: $$ \phi_{\text{value}}(I) \wedge \bigwedge {i=1}^k (\neg f{i}(I)) \wedge \bigwedge _{i=k+1}^n [\text{value} \neq t_i] \wedge [\text{value} = t_k] $$ 如果这个表达式 unsat，则说明 $f_k$ 的生成已经完成，可以继续生成接下来的变量，否则它的 model 就是一个范反例$e$。

为了通过这个 example，需要扩大 $f_k$，即在 $f_k$ 中加入一个新的集合 $P$，使得 $P$ 在 $e$ 上为真。可以从 $C$ 中找到所有在 $e$ 下为真的集合 $S$，则真实的 $P$ 一定是 $S$ 的子集。

我们可以用如下的约数来判断一个集合 $P$ 能不能被加入答案，设 $P$ 对应的布尔表达式为 $P(I)$ $$ (\neg \phi_{\text{value}}(I)) \wedge \bigwedge _{i=1}^k(\neg f_i(I)) \wedge P(I) \wedge [\text{value} = t_k] $$ 如果这个表达式 sat，说明集合 $P$ 太容易被满足，把不满足答案的解加进来了，否则说明加入集合 $P$ 程序还是正确的。

可以先检查 $S$ 能不能别加入答案，如果不能，说明当前无法继续生成了，原因是集合 $C$ 不够大，算法会返回第二部分生成一个更大的集合 $C$ 来生成。

直接加入 $S$ 会产生较为严重的过拟合，因此同样采用了二分的方法来取得 $S$ 的一个极小子集来作为 $P$。

第三部分对过拟合的处理

上述的算法在 max 中仍然会产生严重的过拟合，max10 里会产生 $173K$ 长度的代码。

考虑在析取范式中不存在 or 的情况，即可以用一个 $P$ 集合来表出条件。在这种情况下，上述算法相当于在取值为 $t_k$ 的空间中，每次选择一个包含某个点的子空间加入答案，直到当前选择的点不能被更小的子空间表示了，才能产生正确的结果。

在已知真实答案中不存在 or 的前提下，可以采用更高效的做法：每一次用之前产生过的所有测试数据来筛选集合 $S$，使得 $S$ 中的每一个判断表达式，在之前每一个测试用例下均为真。

采用这样的策略，算法可以在非常快的速度内生成 max15。直观上来说，这个算法寻找 $P$ 的过程相当于每次扩张一个维度，而不是扩展一个子空间。（实际上，这个算法在 $|C|$ 次 SMT 求解后一定能找到答案，而之前的算法是指数级的）

但是在实际生成的时候，并不知道答案中有几个 or。因为我们采用了如下的扩展方法：

1. 维护若干个 example 集合 $S_i$，每产生一个新的 example，就对每一个已有的 $S_i$ 尝试把 $e$ 加入这个集合中。如果 $e$ 的加入使得集合 $S_i$ 不能被任何一个正确的条件集合 $P$ 表出，那么就制止这次加入。
2. 如果 $e$ 无法被加入任何已有的集合中，那么就加入一个新的集合，集合的元素只有 $e$ 本身。如果这个集合也不能被任何一个正确的条件集合 $P$ 表出，那么说明 $C$ 集合不够大，回到第二步。

实验结果

数据点	算法一(s)	算法二(s)	数据点	算法一(s)	算法二(s)
max2	0.31	0.34	array2	0.38	0.50
max3	0.39	0.44	array3	0.52	0.80
max4	0.84	0.65	array4	0.65	1.31
max5	4.88	0.93	array5	0.85	2.14
max6	230.47	1.37	array6	1.09	3.11
max7	TLE	2.01	array7	1.57	6.12
max8	TLE	3.18	array8	1.85	10.19
max9	TLE	4.43	array9	2.50	15.29
max10	TLE	7.72	array10	2.85	15.83
max11	TLE	9.29	array11	4.64	22.58
max12	TLE	12.19	array12	4.63	37.58
max13	TLE	18.34	array13	5.63	38.13
max14	TLE	26.80	array14	6.56	50.03
max15	TLE	29.08	array15	7.97	112.21
s1	TLE	1.12	tutorial	69.43	64.13
s2	0.59	0.68	three	WA	41.27
s3	2.33	2.46	mytest	TLE	32.45