diff options
author | Yann Herklotz <ymh15@ic.ac.uk> | 2020-09-12 09:52:07 +0000 |
---|---|---|
committer | overleaf <overleaf@localhost> | 2020-09-12 10:03:11 +0000 |
commit | 47ffe25ba969f577e1829d136aae541b9eeceeb5 (patch) | |
tree | c465b3f4115929522efbe7e7dda5278d36f0018f /intro.tex | |
parent | 639377a488e3d079bf95d9ee53cb748a3d3bedba (diff) | |
download | fccm21_esrhls-47ffe25ba969f577e1829d136aae541b9eeceeb5.tar.gz fccm21_esrhls-47ffe25ba969f577e1829d136aae541b9eeceeb5.zip |
Update on Overleaf.
Diffstat (limited to 'intro.tex')
-rw-r--r-- | intro.tex | 40 |
1 files changed, 24 insertions, 16 deletions
@@ -6,36 +6,44 @@ It is even being used in high-assurance settings, such as financial services~\ci Our method is brought over from the compiler testing literature. We use a tool called Csmith~\cite{yang11_findin_under_bugs_c_compil} to generate well-formed C programs from the subset of the C language that is supported by all the HLS tools we test, and then augment each program with randomly chosen HLS-specific directives. We synthesise each C program to RTL, and use a Verilog simulator to calculate its return value. If synthesis crashes, or if this return value differs from the return value obtained by executing a binary compiled from the C program by gcc, then we have found a candidate bug. We then use trial-and-error to reduce the C program to a minimal version that still triggers a bug. + + +We have tested three widely used HLS tools: LegUp~\cite{canis13_legup}, Xilinx Vivado HLS~\cite{xilinx20_vivad_high_synth}, and the Intel HLS Compiler~\cite{?}. For all three tools, we were able to find valid C programs that cause crashes while compiling and valid C programs that cause wrong RTL to be generated. We have submitted a total of \ref{?} bug reports to the developers, \ref{?} of which have been confirmed and \ref{?} of which have now been fixed at the time of writing. + \begin{figure} \centering \begin{minted}{c} unsigned int b = 0x1194D7FF; int a[6] = {1, 1, 1, 1, 1, 1}; -int result() { +int main() { int c; for (c = 0; c < 2; c++) b = b >> a[c]; return b; } \end{minted} - \caption{Miscompilation bug found in Vivado 2018.3 and 2019.2 which returns \texttt{6535FF} instead of \texttt{46535FF} which is the correct result.}\label{fig:vivado_bug1} + \caption{Miscompilation bug found in Vivado 2018.3 and 2019.2 which returns \code{0x006535FF} instead of \code{0x046535FF} which is the correct result.}\label{fig:vivado_bug1} \end{figure} -\NR{ -Notes on program: -\begin{itemize} - \item result is main - \item array a needs to be at least 6 elements - \item magic number as well - \item for loop at least two. - \item constant replacement fixes it too. - \item all three versions of Vivado. - \item -\end{itemize} -} - -We have tested three widely used HLS tools: LegUp~\cite{canis13_legup}, Xilinx Vivado HLS~\cite{xilinx20_vivad_high_synth}, and the Intel HLS Compiler~\cite{?}. For all three tools, we were able to find valid C programs that cause crashes while compiling and valid C programs that cause wrong RTL to be generated. We have submitted a total of \ref{?} bug reports to the developers, \ref{?} of which have been confirmed and \ref{?} of which have now been fixed at the time of writing. +\paragraph{An example of a fuzzed buggy program} +Figure~\ref{fig:vivado_bug1} shows a minimal example that produces the wrong result during RTL simulation in all three versions of VivadoHLS, compared to GCC execution. +In this example, we right shift a large integer value \code{b} by values of array elements, in array \code{a}, within iterations of a \code{for}-loop. +VivadoHLS returns \code{0x006535FF} instead of \code{0x046535FF} as in GCC. +The circumstances in which we found this right shift bug shows the challenge of testing current HLS tools. + +For instance, the for-loop was also necessary to ensure that a bug was detected. +Also, the shift value needs to be accessed from an array. +Replacing the array accesses within the loop with constants result in the bug not surfacing. +Additionally, the array \code{a} needed to be at least six elements in size although the for-loop only has two iterations. +Any array smaller than that did not surface this bug. +Finally, the value of \code{b} is an oracle that could not be changed without masking the bug. +Producing such circumstances within C code for HLS testing is both arduous and counter-intuitive to human testers. +In contrast, producing non-intuitive, complex but valid C programs is the cornerstone of fuzzing tools. +Thus, it was natural to adopt program fuzzing for our HLS testing campaign. +\NR{Yann, please double check my claims about the bug. I hope I accurately described what we discussed. }\YH{Yes I agree with all that, I think that is a good description of it} + +\paragraph{Our contribution} We hope that our work serves to stimulate efforts to improve the quality of HLS tools. |