Update on Overleaf.

1 files changed, 7 insertions, 5 deletions

diff --git a/method.tex b/method.tex
index d27f22b..b9356ec 100644
--- a/method.tex
+++ b/method.tex
@@ -89,13 +89,15 @@ More importantly, we disable the generation of several language features to enab
 First, we ensure that all mathematical expressions are safe and unsigned, to ensure no undefined behaviour. 
 We also disallow assignments being embedded within expressions, since HLS generally does not support them.
 We eliminate any floating-point numbers since they typically involve external libraries or use of hard IPs on FPGAs, which in turn make it hard to reduce bugs to their minimal form.
-We also disable the generation of pointers for HLS testing, since pointer support in HLS tools is either absent or immature~\cite{xilinx20_vivad_high_synth}.\YH{I've looked at the documentation and even pointer to pointer is supported, but maybe not pointer to pointer to pointer.  I think there was some other pointer assignment that didn't quite work, but I don't remember now.  Immature might be a good description though.}
-We also disable void functions, since we are not supporting pointers.\YH{Figure \ref{fig:eval:vivado:mismatch} actually has void functions...} \JW{Hm, true. Perhaps these were introduced during reduction.}
+We also disable the generation of pointers for HLS testing, since pointer support in HLS tools is either absent or immature~\cite{xilinx20_vivad_high_synth}.
+%\YH{I've looked at the documentation and even pointer to pointer is supported, but maybe not pointer to pointer to pointer.  I think there was some other pointer assignment that didn't quite work, but I don't remember now.  Immature might be a good description though.}
+We also disable void functions, since we are not supporting pointers.
+%\YH{Figure \ref{fig:eval:vivado:mismatch} actually has void functions...} \JW{Hm, true. Perhaps these were introduced during reduction.}
 We disable the generation of unions as these were not supported by some of the tools such as LegUp 4.0.
 
 To decide whether a problematic feature should be disabled or reported as a bug, the tool in question is taken into account.  Unfortunately there is no standard subset of C that is supported by HLS tools; every tool chooses a slightly different subset.  It is therefore important to choose the right subset in order to maximise the number of real bugs found in each tool, while avoiding generating code that the tool does not support.  Therefore, we disable a feature if it fails gracefully (i.e. with an error message stating the issue) in one of the tools.  If the HLS tool fails in a different way though, such as generating a wrong design or crashing during synthesis, the feature is kept in our test suite.
 
-Use a volatile pointer for any pointer that is accessed multiple times within a single transaction (one execution of the C function). If you do not use a volatile pointer, everything except the first read and last write is optimized out to adhere to the C standard.
+%Use a volatile pointer for any pointer that is accessed multiple times within a single transaction (one execution of the C function). If you do not use a volatile pointer, everything except the first read and last write is optimized out to adhere to the C standard.
 
 We enforce that the main function of each generated program must not have any input arguments to allow for HLS synthesis. 
 We disable structure packing within Csmith since the ``\code{\#pragma pack(1)}'' directive involved causes conflicts in HLS tools because it is interpreted as an unsupported pragma. 
@@ -198,7 +200,7 @@ We first perform a custom reduction in which we iteratively remove the HLS direc
 %Although, our custom reduction gives us the freedom and control of how to reduce buggy programs, it is arduous and requires a lot of manual effort.
 We then use the \creduce{} tool~\cite{creduce} to automatically reduce the remaining C program.
 \creduce{} is effective because it reduces the input while preserving semantic validity and avoiding undefined behaviour.
-It has various reduction strategies, such as delta debugging passes and function inlining, that help it converge rapidly to a test case that is small enough to understand and step through.
+It has various reduction strategies, such as delta debugging passes and function inlining, that help it converge rapidly to a test-case that is small enough to understand and step through.
 
 However, the downside of using \creduce{} with HLS tools is that we are not in control of which lines and features are prioritised for removal.
 As a consequence, we can easily end up with \creduce{} producing programs that are not synthesisable, despite being valid C.
@@ -206,7 +208,7 @@ As a consequence, we can easily end up with \creduce{} producing programs that a
 Even though \creduce{} does not normally introduce undefined behaviour, it can introduce behaviour that is unsupported in the HLS tools.
 An example is the reduction of a function call, where the reducer realises that a mismatch is still observed when the function call's arguments are removed, and the function pointer is assigned a constant instead.
 This is however often unsupported in HLS tools, since a function pointer does not have a concrete interpretation in hardware, because in the absence of instructions, functions are not associated with a particular memory location.
-Once unhandled behaviour is introduced at any point in the reduction, the test cases will often zero in on that unhandled behaviour, even though it does not actually represent an interesting bug.
+Once unhandled behaviour is introduced at any point in the reduction, the test-cases will often zero in on that unhandled behaviour, even though it does not actually represent an interesting bug.
 To prevent this, we use a script to guide \creduce{} away from introducing these unhandled behaviours as much as possible. 
 This script involves adding \texttt{-fsanitize=undefined} to the GCC options in order to abort when undefined behaviour is detected at runtime, and erroring out whenever any warning is encountered while running the HLS tool (except common warnings that are known to be harmless).