From 29ec67340c03fb15dce465381737b96e12ef764b Mon Sep 17 00:00:00 2001
From: Nguyễn Gia Phong <cnx@loang.net>
Date: Sat, 28 Oct 2023 15:57:52 +0900
Subject: Draft skeleton

---
 technique.tex | 118 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 118 insertions(+)
 create mode 100644 technique.tex

(limited to 'technique.tex')

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}
-- 
cgit 1.4.1