diff options
Diffstat (limited to 'technique.tex')
| -rw-r--r-- | technique.tex | 118 |
1 files changed, 118 insertions, 0 deletions
diff --git a/technique.tex b/technique.tex new file mode 100644 index 0000000..d4a576c --- /dev/null +++ b/technique.tex @@ -0,0 +1,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} |