From a084dbf424588064a97f8e687618f830c2fe283d Mon Sep 17 00:00:00 2001 From: John Wickerson Date: Mon, 14 Sep 2020 21:59:18 +0000 Subject: Update on Overleaf. --- conclusion.tex | 2 +- intro.tex | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/conclusion.tex b/conclusion.tex index 00e02aa..f073df2 100644 --- a/conclusion.tex +++ b/conclusion.tex @@ -1,7 +1,7 @@ \section{Conclusion} We have shown how existing fuzzing tools can be modified so that their outputs are compatible with HLS tools. We have used this testing framework to run 10,000 test cases \JW{check numbers} through three different HLS tools. In total, we found at least 6 individual and unique bugs in all the tools, which have been reduced, analysed, and reported to the tool vendors. These bugs include crashes as well as instances of generated designs not behaving in the same way as the original code. -One can always question how much bugs found by fuzzers really \emph{matter}, given that they are usually found by combining language features in ways that are vanishingly unlikely to happen in practice. This question is especially pertinent for our particular context of HLS tools, which are well-known to have restrictions on the language features that they handle. +One can always question how much bugs found by fuzzers really \emph{matter}, given that they are usually found by combining language features in ways that are vanishingly unlikely to happen `in the wild'. This question is especially pertinent for our particular context of HLS tools, which are well-known to have restrictions on the language features that they handle. Nevertheless, we would argue that any bugs have the potential to cause problems Further work could be done on supporting more HLS tools, especially ones that claim to prove that their output is correct before terminating. This could give an indication on how effective these proofs are, and how often they are actually able to complete their equivalence proofs during compilation in a feasible time scale. diff --git a/intro.tex b/intro.tex index 7523885..2569fe9 100644 --- a/intro.tex +++ b/intro.tex @@ -42,7 +42,7 @@ Fuzzing has been used extensively to test conventional compilers; for example, Y \paragraph{An example of a compiler bug found by fuzzing} -Figure~\ref{fig:vivado_bug1} shows a program that produces the wrong result during RTL simulation in Xilinx Vivado HLS. The bug was initially revealed by a large, randomly generated program, which we reduced to the minimal example shown in the figure. +Figure~\ref{fig:vivado_bug1} shows a program that produces the wrong result during RTL simulation in Xilinx Vivado HLS. The bug was initially revealed by a randomly generated program of around 113 lines, which we were able to reduce to the minimal example shown in the figure. The program repeatedly shifts a large integer value \code{b} right by the values stored in array \code{a}. Vivado HLS returns \code{0x006535FF}, but the result returned by GCC (and subsequently confirmed manually to be the correct one) is \code{0x046535FF}. -- cgit