diff options
Diffstat (limited to 'technique.tex')
| -rw-r--r-- | technique.tex | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/technique.tex b/technique.tex index af1fa92..63b7ea1 100644 --- a/technique.tex +++ b/technique.tex @@ -13,7 +13,7 @@ to generate \glspl{difftest}. Third, the new conditions the combined are assertions on the distinction of corresponding values across revisions, so we offer multiple options to capture such \emph{\glspl{symout}}. -Next, we introduces concrete execution to reduce the theorem proving load, +Next, we introduce concrete execution to reduce the theorem proving load, and produce \glspl{difftest} for clustering the patches and finally produce a decision tree. One may observe that the clustering information can help with selecting more ``promising'' states, although such scheduling @@ -161,7 +161,7 @@ used for shadow symbolic execution. Unlike \textsc{Shadow} which tests only one patch~\cite{shadow} to reveal its regressions, though, the goal of \psychic{} is to find the difference in behavior between multiple patches. Therefore, the former's annotation -at level of expressions does not meet our expectation on expressivity. +at the level of expressions does not meet our expectation on expressivity. Instead, we implement higher-order branching. Annotating patches at block level simplifies the generation process and improves the readability of the meta program. @@ -195,7 +195,7 @@ and improves the readability of the meta program. For instance, given the two unified diffs~\cite{unidiff} of a bug fix from upstream \texttt{grep}, and a patch in \textsc{DBGBench}~\cite{dbgbench} -in figure~\ref{grep-8f08d8e2},\footnote{The snippets have been outdented +in figure~\ref{grep-8f08d8e2},\footnote{These snippets have been outdented to fit within the width of this page.} one can construct the relevant part of the meta program in figure~\ref{grep-8f08d8e2-meta}, where \verb|__klee_meta| parses the environment for the choice of revision when executed @@ -227,7 +227,7 @@ if (__klee_meta(3) == \textcolor{purple}{0}) \verb|{| One may notice that the meta program may have any level of granularity. \psychic{} utilizes the meta program to maximize instructions -and path constraints sharing, which effectively means to defer +and path constraints that are shared, which effectively means to defer the divergence point deep into the control flow. For its intended use on automatically generated patches whose hunks are commonly short, optimizing the meta program construction is not a major issue. @@ -237,7 +237,7 @@ higher-order branching patch identifier, via basic tree pattern matching% ~\cite{tree-pattern} and skip adding its condition to the children states. Instead, those states carry the revision number outside of their path constraints for constant-time access when pruning paths -going though multiple patches in algorithm~\ref{apply-meta}. +going through multiple patches in algorithm~\ref{apply-meta}. \begin{algorithm} \caption{Construction of possible states after a patch location} @@ -247,7 +247,7 @@ going though multiple patches in algorithm~\ref{apply-meta}. \State $n' \gets \Call{RevisionNumber}{\varphi}$ \State $s_a = (i_a, e, \varPhi, n)$ \Comment{assume the lack of meta branch nesting - and always follow alternative path} + and always follow alternative paths} \If{$n = 0$} \Return $\{(i_c, e, \varPhi, n'), s_a\}$ \Comment{$i_c$ enters patch $n'$ } @@ -288,7 +288,7 @@ or automatically~\cite{fl-eval}, output annotation has limited exhaustiveness. To balance between manual annotation and computational scalability, methods \ref{ret} and \ref{parg} are introduced to automatically capture output more precisely at the end of every interested function. Debugging information -forwarded from compiler frontend are kept in bitcodes, and they are used +forwarded from compiler frontend are kept in bitcodes. They are used to limit the subroutines to be monitored, for example in algorithm~\ref{fnout}, the file that is patched by an \gls{apr} tool. @@ -314,7 +314,7 @@ the file that is patched by an \gls{apr} tool. \end{algorithmic} \end{algorithm} -Each \gls{symout} then is given an unique name for later comparison. +Each \gls{symout} then is given a unique name for later comparison. For the sake of simplicity, we name them after the capturing method and associated identifier, i.e.~variable or subroutine. @@ -328,7 +328,7 @@ and the conjunction of their path conditions is satisfiable. Currently \psychic{} only compare halt states to minimize memory usage 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. +then for the common ones assert for a possible distinction between two paths. If the path constraints of both states are \gls{sat} with at least one difference in outputs, a \gls{difftest} can be generated from the \gls{smt} model. @@ -384,4 +384,4 @@ 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 by searching through the subsets -of set of clustering sets. +of the set of clustering sets. |