1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
|
\section{Technique}
Unlike the original \textsc{klee} which execute one single program at a time,
our tool performs execution on a pool of the program's revisions
at the same time.
An overview of our approach is illustrated in figure~\ref{fig:arch}.
\begin{figure}[h]\centering
\begin{tikzpicture}[mymatrix/.style={matrix of nodes,
nodes=typetag,row sep=1ex},
typetag/.style={draw,anchor=west},
title/.style={draw=none,inner sep=0pt},
line width=0.2ex]
\linespread{0.8}
\node[draw,label={[name=sched]Scheduler}] (states) {States};
\node[draw,below=0.5ex of states] (clstr) {Clusters};
\node[draw,fit={(sched) (states) (clstr)}] {};
\node[draw,right=11em of states] (symb) {Interpreter};
\draw[-angle 45] (states.north east) to[in=90,out=15]
node[sloped,above,pos=0.4]{selected state} (symb.north west);
\draw[-angle 45] (symb.south west) to[in=0,out=-90]
node[sloped,above,pos=0.6]{child state} (states.east);
\node[draw,below=6em of symb] (smt) {Theorem prover};
\draw[angle 45-angle 45] (symb) to (smt);
\node[draw,below=7em of sched,label={[name=diff]Differentiator}]
(outs) {Fruitful states};
\draw[-angle 45] (symb.south west) to[in=45,out=-90]
node[sloped,above,pos=0.6]{state with output} (outs.15);
\draw[-angle 90] (outs) to[in=90,out=0,pos=0.4]
node[sloped,below]{path conditions} (smt.north west);
\draw (outs.south east) to[in=90,out=10] (smt.north west);
\node[draw,below=0.5ex of outs] (prog) {Metaprogram};
\node[draw,fit={(diff) (outs) (prog)}] {};
\draw[-angle 45] (smt.south west) to[out=-90,in=0]
node[sloped,below]{concrete input} (prog);
\draw[-angle 45] (prog) to[out=180,in=-150]
node[left,align=center]{diff.\\test} (clstr.south west);
\node[left=4em of states.west] (bc) {bitcode};
\draw[-angle 90] (bc) to[in=180,out=60] (states.west);
\node[below=1em of bc,align=center] (tree) {decision\\tree};
\draw[-angle 45] (clstr.west) to[out=180,in=60] (tree);
\node[above=1em of bc,align=center] (seed) {seed\\input};
\draw[dotted] (seed) to[out=0,in=180] (states);
\draw[-angle 45] (bc.south west)
to[out=-135,in=-135] (prog.south west);
\end{tikzpicture}
\caption{\textsc{Psychic} overview.}\label{fig:arch}
\end{figure}
\begin{algorithm}
\caption{Overall execution}
\begin{algorithmic}[1]
\Require set of program revisions $D$
\Ensure set of differential tests $T$
\State $T \gets \varnothing$
\State $E \gets \varnothing$ \Comment{Exited states}
\State $q \gets \text{new\_searcher}(D)$
\For{$d \in D$}
\State $s \gets \text{initial\_state}(d)$
\State $\text{add\_states}(q, \{s\})$
\EndFor
\While{has\_state($q$)}
\State $s \gets \text{select\_state}(q)$
\State $i \gets \text{next\_instruction}(s)$
\Comment{$i$ is a state}
\If{$i$ is exit}
\State $E' \gets \text{head}(\text{sort}(\text{distance\_to}(i),
\text{different\_revision}(E, i)))$
\For{$e \in E'$}
\State $t \gets \text{generate\_test}(i, e)$
\If{$t$ is not null}
\State $T \gets T \cup \{t\}$
\EndIf
\EndFor
\State $E \gets E \cup \{i\}$
\Else
\State $S_+, S_- \gets \text{execute\_instruction}(i)$
\State $\text{remove\_states}\left(q, S_-\right)$
\State $\text{add\_states}\left(q, S_+\right)$
\EndIf
\EndWhile
\end{algorithmic}
\end{algorithm}
\begin{algorithm}
\caption{State selection}
\begin{algorithmic}[1]
\Require searcher $q$
\Ensure state $s$
\State $S \gets \varnothing$
\State $P \gets \text{base\_priority}(q)$
\Comment{Scheduling priority from base search algorithm}
\For{$z \in \text{states}(q)$}
\If{$z \notin S$}
\State $S' \gets \text{parallel\_states}(q, z)$
\If{$S' \ne \varnothing$}
\State $S \gets S \cup S' \cup \{z\}$
\EndIf
\EndIf
\State $l \gets \text{local\_frontier}(q, z)$
\State $g \gets \text{global\_frontier}(q, z)$
\If{$l$ is null $\land$ $g$ is not null}
\State $P_z \gets P_z + \text{distance\_bonus}(g, z)$
\Comment{Should further or nearer be prioritised?}
\EndIf
\EndFor
\For{$z \in S$}
\State $P_z \gets P_z + \text{PARALLEL\_BONUS}$
\EndFor
\State $s \gets \text{max\_priority}(P)$
\end{algorithmic}
\end{algorithm}
|
