diff options
Diffstat (limited to 'technique.tex')
| -rw-r--r-- | technique.tex | 42 |
1 files changed, 26 insertions, 16 deletions
diff --git a/technique.tex b/technique.tex index 58e9348..470449f 100644 --- a/technique.tex +++ b/technique.tex @@ -111,6 +111,7 @@ is denoted in algorithm~\ref{overall}. \Require Meta program $P$ \Ensure Set of differential tests $T$ \State $T \gets \varnothing$ + \State $D \gets \varnothing$ \Comment{Distinguished revision pairs} \State $H \gets \varnothing$ \Comment{Halt states} \State $S \gets \Call{InitialState}{P}$ \While{$S \neq \varnothing$} @@ -121,14 +122,12 @@ is denoted in algorithm~\ref{overall}. \State $(i', e') \gets \Call{Execute}{i, e}$ \If{$\Call{IsHalt}{i}$} \For{$(\varPhi', n') \in H$} - \If{$n \ne n'$} - \State $t \gets \Call{DiffTest}{\varPhi, n, \varPhi', n'}$ - \If{$t \ne \bot$} - $T \gets T \cup \{t\}$ - \EndIf + \State $t \gets \Call{DiffTest}{D, \varPhi, n, \varPhi', n'}$ + \If{$t \ne \bot$} + \State $T \gets T \cup \{t\}$ + \State $D \gets D \cup \Call{DistinguishPairs}{t}$ \EndIf \EndFor - \State TODO: describe clustering \State $H \gets H \cup \{(\varPhi, n)\}$ \ElsIf{$\Call{IsBranch}{i}$} \State $(\varphi, i_c', i_a') \gets i'$ @@ -269,7 +268,6 @@ for calling \klee{} intrinsics and a compiler using LLVM as a backend. One kind of LLVM instruction may be used for difference purposes, so for better applicability we try to accommodate for a range of usages. For capturing output values, \psychic{} offers the following methods. -\pagebreak \begin{enumerate}[noitemsep] \item Source code annotation\label{annote} \item Output files (including standard output)\label{stdout} @@ -332,25 +330,28 @@ and \gls{smt} solving cost. Such \gls{smt} formula is constructed in algorithm~\ref{diffgen} by first append a suffix to each output name, then for the common ones assert for possible distinction between two paths. If the path constraints of both states are \gls{sat} with at least -one difference in output, a \gls{difftest} can be generated +one difference in outputs, a \gls{difftest} can be generated from the \gls{smt} model. \begin{algorithm} \caption{\Gls{difftest} generation}\label{diffgen} \begin{algorithmic}[1] - \Procedure{DiffTest}{$\varPhi, n, \varPhi', n'$} + \Procedure{DiffTest}{$D, \varPhi, n, \varPhi', n'$} + \If{$n \ne n' \lor \{n, n'\} \in D$} + \Return $\bot$ + \EndIf \State $\varPsi, N \gets \Call{RenameOutputs}{\varPhi, n}$ \State $\varPsi', N' \gets \Call{RenameOutputs}{\varPhi', n'}$ - \For{$a \in N \cap N'$} - \State $\varPsi_\text{diff} - \gets \varPsi_\text{diff} \lor \Call{Distinct}{a, n, n'}$ - \EndFor + \State $\varPsi_\text{diff} + \gets \bigvee_{a \in N \cap N'}\Call{Distinct}{a, n, n'}$ \If{$\lnot\Call{sat}{\varPsi \land \varPsi' \land \varPsi_\text{diff}}$} - \State \Return $\bot$ + \Return $\bot$ \EndIf - \State TODO: describe concrete execution - \State \Return $\Call{Model}{\varPsi \land \varPsi' + \State $m \gets \Call{Model}{\varPsi \land \varPsi' \land \varPsi_\text{diff}}$ + \State $I \gets \Call{InputValues}{m}$ + \State \Return $(m, + \{\Call{Execute}{I, r} \mid r \in \textsc{revisions}\})$ \EndProcedure \Procedure{RenameOutputs}{$x, n$} \State $X, k \gets x$ \Comment{subexpressions and kind} @@ -374,3 +375,12 @@ from the \gls{smt} model. \EndProcedure \end{algorithmic} \end{algorithm} + +\subsection{Decision tree construction} +From each \gls{difftest}, a set of clusters of revisions with the same output +is constructed. We then superimpose these clustering sets to create +hierarchical clusterings or a decision tree. A minimal tree, i.e~a tree +with the shortest height, is found through exhaustively search though +all subsets of set of clustering sets. + +TODO: analyse complexity |