Add article about Arduino and QuickCheck

5 files changed, 474 insertions, 0 deletions

diff --git a/resources/img/dual-lever-paddle.jpg b/resources/img/dual-lever-paddle.jpg
new file mode 100644
index 0000000..978f38a
--- /dev/null
+++ b/resources/img/dual-lever-paddle.jpg
diff --git a/resources/md/2021-09-07-testing-arduino-code-with-haskell-quickcheck.md b/resources/md/2021-09-07-testing-arduino-code-with-haskell-quickcheck.md
new file mode 100644
index 0000000..647da97
--- /dev/null
+++ b/resources/md/2021-09-07-testing-arduino-code-with-haskell-quickcheck.md
@@ -0,0 +1,445 @@
+*An [Arduino][] program of mine showed a weird bug, but I couldn't reliably
+reproduce it. I isolated the relevant C code so that I could run it on a
+computer, and used [Haskell][] [QuickCheck][] to run automated property tests
+against it. With that set up, fixing the bug was a matter of minutes. This
+article assumes basic knowledge of both Arduino and Haskell.*
+
+[[toc]]
+
+# Background
+
+A friend of mine (Rick PA5NN) built a morse code transceiver, the [ATSAMF][],
+and I wrote the Arduino software for it. Part of the software is the keyer
+routine, which translates the input of a [dual-lever paddle][] to a stream of
+dots and dashes:
+
+![Electronic dual paddle keyer (public domain; from the Wikipedia page).](/assets/img/dual-lever-paddle.jpg)
+
+One of the levers is for the dot; the other for the dash. The controller does
+the timing: the dash is three times as long as the dot, and the time between
+dots and dashes is the same as the time for the dot.
+
+But there is a trick: when you squeeze both levers simultaneously, dots and
+dashes will alternate. With some practise, this allows you to send a number of
+characters much more easily. For example, the `C` is `-.-.`. With this *iambic
+keying mode*, you squeeze the dash lever first, hold both until the second dash
+is keyed, and release the dot lever when the second dot is keyed:
+
+```text
+Output:  ------------------      ......      ------------------      ......
+Normal:  toggle dash             toggle dot  toggle dash             toggle dot
+Iambic:  press dash, press dot                     release dash        release dot
+```
+
+The algorithm should be pretty straightforward, but nevertheless a bug got in.
+Occasionally, an extra dash would be keyed, but we were unable to reliably
+reproduce it and I couldn't see any obvious problems in the code that could
+explain this behaviour.
+
+At this point I could have tried some things, upload new code, and see if the
+bug was still present. But without a sure-fire way to reproduce the bug, I
+would never be 100% sure it was fixed (or which of the changes did the trick).
+So, I set out to do some proper testing.
+
+I wanted to test on my computer rather than the Arduino to be able to run a
+large amount of test cases. I also wanted to be able to specify the tests in a
+higher-level language than C or C++, to avoid the problem that the test would
+be as complex as the code itself. [Haskell][] was the obvious choice given my
+personal expertise, although there are probably lots of other valid options out
+there. I won't claim to be an expert on Arduino, nor on testing with Haskell,
+but I wanted to share some experiences in the hope they are useful to somebody.
+
+# Compiling the C code for x86
+
+First, I needed to be able to compile the Arduino code for my own computer, an
+x86 architecture. Fortunately, the code was already pretty compartmentalized,
+so that the keying routines rarely used Arduino-specific functions.
+
+However, my code was not completely independent from the rest of the sketch. In
+many real libraries, you see that a C++ class is parametrized in the pins they
+use. For example, the `LiquidCrystal` constructor takes the pin numbers of the
+lines that are used to communicate with an LCD display:
+
+```arduino
+LiquidCrystal lcd(12, 11, 10, 5, 4, 3, 2);
+```
+
+That means that internally these pin numbers are stored, and when the LCD
+library writes to one of these lines it needs to retrieve the value of the pin
+number from memory. That's a bit inefficient (though I don't know how much), so
+instead I define the pins I use in a central header file and use them
+throughout the code:
+
+```arduino
+/* main.h */
+#define INPUT_DASH A3
+
+/* key.ino */
+if (digitalRead(INPUT_DASH)) {
+  /* .. */
+}
+```
+
+Also, I wanted that `key.ino` (the 'library') only took care of the timing, not
+of the actual handling of dashes and dots. This is because the keyer is not
+only used to transmit dashes and dots, but also in the radio's menus. This
+logic does not belong in the keying library.
+
+To overcome this problem, in the main file I define some functions that act as
+an interface for the keying library. They react to events like "Start dash",
+"Start dot", and "End keying". The library in `key.ino` only needs to do timing
+and call the handlers for these events:
+
+```arduino
+/* main.ino */
+void key_handle_dash(void) {
+  /* transmit a dash, do something in the menu, ... depending on the state */
+}
+
+/* key.ino */
+if (digitalRead(INPUT_DASH)) {
+  key_handle_dash();
+  /* timing logic... */
+}
+```
+
+Finally, my code also needed to read from some pins (`digitalRead`) and do some
+`delay`s. Furthermore, it had an interrupt service routine (ISR) for the timer.
+Put simply, this is a function that is executed every time an internal timer
+changes value, and it was needed to get the timing of the dots and dashes
+right. These three features (`digitalRead`, `delay`, and the ISR) are
+Arduino-specific.
+
+All this made that I could not use `key.ino` as a stand-alone library without
+significant refactoring.
+
+What I did instead was create a small wrapper program, `test_key.c`. This file
+would provide the handler functions like `key_handle_dash`, the
+Arduino-specific functions like `delay`, and call the ISR in `key.ino`.
+
+But because `INPUT_DASH` is defined as `A3`, I still needed the Arduino header
+files in which pin `A3` is defined. I came up with the following Makefile:
+
+```make
+SRC_DIR:=../ATSAMF
+
+CC:=gcc
+CFLAGS:=\
+	-D__AVR_ATmega328P__\
+	-DARDUINO=105\
+	-DF_CPU=16000000L\
+	-I/opt/arduino/hardware/arduino/avr/cores/arduino\
+	-I/opt/arduino/hardware/tools/avr/avr/include\
+	-I/opt/arduino/hardware/arduino/avr/variants/standard\
+	-I$(SRC_DIR)\
+	-Wno-attributes\
+	-O
+
+key.o: $(SRC_DIR)/key.ino .FORCE
+	$(CC) $(CFLAGS) -x c++ -c $<
+
+test_key.o: test_key.c .FORCE
+	$(CC) $(CFLAGS) -c $<
+
+.FORCE:
+.PHONY: .FORCE
+```
+
+The three `-D` defines and the three include paths from `/opt/arduino` are
+needed for the Arduino header files. `key.o` needs to be compiled as C++ (hence
+`-x c++`), but `test_key.c` is a pure C program. This is possible because the
+code in `key.ino` is wrapped in `extern "C" { .. }` so that the C calling
+convention is used:
+
+```arduino
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/* actual code... */
+
+#ifdef __cplusplus
+}
+#endif
+```
+
+# Mocking the keying library
+
+To test the keying library, I needed to provide it with input and check its
+output. It read input with `digitalRead`, then ran some code depending on the
+interrupt service routine, and produced output through handler functions like
+`key_handle_dash`.
+
+To provide input, I defined my own `digitalRead` in `test_key.c`:
+
+```c
+static char *character;
+
+int digitalRead(uint8_t pin) {
+	int enabled = 0;
+
+	if (pin == DASHin)
+		enabled = *character == '-' || *character == 'B';
+	else if (pin == DOTin)
+		enabled = *character == '.' || *character == 'B';
+
+	return enabled ? LOW : HIGH;
+}
+```
+
+Here, `character` is used for the current test case—the input that we are
+providing to the library. This is a simple string where `-` and `.` are used
+for dashes and dots, and `B` for the state that both levers are squeezed. When
+no levers are squeezed, a space (` `) is used.
+
+To run the ISR every now and then, I provided my own `delay`. It does not
+actually delay, it just calls the ISR repeatedly:
+
+```c
+void delay(unsigned long ms) {
+	for (; ms; ms--)
+		key_isr();
+}
+```
+
+Finally, I keep a global buffer `result` in which I store the dots and dashes
+provided by the keying library through the handlers:
+
+```c
+static char result[BUFFER_SIZE];
+static char *result_ptr = result;
+
+void key_handle_dash(void) { /* and similarly for key_handle_dot */
+	*result_ptr++ = '-';
+	*result_ptr = '\0';
+}
+```
+
+This allowed me to write a function `run_test` which, given a test case (i.e. a
+sequence of characters from `-`, `.`, `B`, and space), runs the keying
+function, and retrieves the result:
+
+```c
+char *run_test(char *_character) {
+	character = _character; /* Set global character, used in digitalRead */
+
+	result_ptr = result; /* Reset result */
+	*result_ptr = '\0';
+
+	iambic_key(); /* The function from key.ino that we are testing */
+
+	return result;
+}
+```
+
+However, nowhere do we move the `character` pointer, so we only provide the
+first dash or dot in the string as input. Where can we do this? I chose to do
+this in `delay`. Using a global timer, I could move the pointer with the same
+interval as that dots are keyed:
+
+```c
+void delay(unsigned long ms) {
+	for (; ms; ms--) {
+		if (state.key.timer % DOT_TIME == DOT_TIME / 2) {
+			if (*character)
+				character++;
+		}
+
+		key_isr();
+	}
+}
+```
+
+I use `timer % DOT_TIME == DOT_TIME / 2` because dots and dashes are sent when
+the `timer` is 0. With this conditional, the `character` pointer will move when
+they keyer state is not changing. This makes it easier to reason about the
+semantics. Schematically, it looks like this, assuming `DOT_TIME = 100`:
+
+```text
+Time:    0      50    100    150    200    250    300    350    400    450    500
+Input:   | Dash |     Both    |     Both    |     Dot     |     None    |     None..
+Output:  |     Dash    |     Dash    |     Dash    |   Silence   |     Dot     | ..
+```
+
+As you can see, the input changes on *t* = 50 mod 100 but the output changes on
+*t* = 0 mod 100.
+
+# The Haskell interface
+
+With this set up, I wanted to be able to use `run_test` from Haskell. I defined
+a type `Input` to represent the input at a given moment (both levers can be
+squeezed independent from each other, so two booleans in a record). With this
+type I could define an `InputSequence` as a non-empty list of
+`Input`s.[^NonEmptyList] The result is simply a `String`, which contains `-`,
+`.`, and spaces.
+
+[^NonEmptyList]: `NonEmptyList` is provided by [QuickCheck][]. Values of this
+  type are guaranteed to contain at least one element when generated
+  automatically by the library.
+
+```haskell
+data Input = Input
+  { dashSqueezed :: Bool,
+    dotSqueezed :: Bool
+  }
+
+newtype InputSequence = InputSequence { getInputSequence :: NonEmptyList Input }
+
+type Result = String
+
+-- This uses the same representation as `digitalRead` assumes.
+instance Show Input where
+  show input
+    | dashSqueezed input = if dotSqueezed input then "B" else "-"
+    | dotSqueezed input = "."
+    | otherwise = " "
+
+instance Show InputSequence where show = concatMap show . getNonEmpty . getInputSequence
+
+-- To generate random values for testing.
+instance Arbitrary Input where arbitrary = Input <$> arbitrary <*> arbitrary
+instance Arbitrary InputSequence where arbitrary = InputSequence <$> arbitrary
+```
+
+Using the foreign function interface I could define `iambicKey` which runs the
+C function `run_test` on a given `InputSequence` and returns the `Result`:
+
+```haskell
+iambicKey :: InputSequence -> IO Result
+iambicKey input =
+  withCString (packInputSequence input) $
+  run_test >=> peekCString >>^ fmap (unwords . words)
+  where
+	packInputSequence = concatMap show . getNonEmpty . getInputSequence
+
+foreign import ccall "test_key.h run_test" run_test :: CString -> IO CString
+```
+
+To get this to compile, I needed to link the C object files as well. I added
+`ld-options: key.o test_key.o` to my Cabal file, but I'm not sure if that is
+the best way to do this.
+
+This allowed me to do things like:
+
+```haskell
+main = do
+  result <- iambicKey {- some input sequence -}
+  putStrLn result
+```
+
+# The QuickCheck tests
+
+To actually test the implementation, I had to either write some properties or
+write a specification. I chose the latter: I defined the behaviour of the
+`iambic_key` routine as a function `expectedResult :: InputSequence -> Result`,
+and wrote a single property to test the implementation against the spec:
+
+```haskell
+testAgainstSpecification :: InputSequence -> Property
+testAgainstSpecification input = monadicIO $ do
+  output <- run (iambicKey input)
+  stop $ output === expectedResult input :: PropertyM IO ()
+```
+
+Finally there is the implementation of `expectedResult`. I wrote this as a
+shallowly embedded state machine. The functions (`start`, `playDot`, etc.) are
+states and their parameters are memory. The states consume the input sequence
+and produce an output sequence:
+
+```haskell
+expectedResult :: InputSequence -> Result
+expectedResult = unwords . words . start . getNonEmpty . getInputSequence
+  where
+    -- The initial state, when no dashes and dots are queud.
+    -- When we are in this state for 7+ iterations, a new character is begun.
+    start = start' 0
+
+    start' 6 input = ' ' : start' 7 input
+    start' i [] = []
+    start' i (input : rest)
+      | dashSqueezed input = playDash (dotSqueezed input) rest
+      | dotSqueezed input = playDot False rest
+      | otherwise = start' (i + 1) rest
+
+    -- Produce a '.'; check the dash lever.
+    playDot dashQueued input = '.' : playDot' dashQueued input
+
+    playDot' dashQueued [] = ['-' | dashQueued]
+    playDot' dashQueued (input : rest) =
+      waitAfterDot (dashQueued || dashSqueezed input) rest
+
+    -- After playing a '.', we are quiet for one dot time and check the dash lever.
+    waitAfterDot dashQueued [] = ['-' | dashQueued]
+    waitAfterDot dashQueued (input : rest)
+      | dashQueued || dashSqueezed input = playDash (dotSqueezed input) rest
+      | dotSqueezed input = playDot False rest
+      | otherwise = start rest
+
+    -- Poduce a '-'; check the dot lever. Dashes are 3x longer than dots.
+    playDash dotQueued input = '-' : playDash' 2 dotQueued input
+
+    playDash' _ dotQueued [] = ['.' | dotQueued]
+    playDash' 0 dotQueued (input : rest) =
+      waitAfterDash (dotQueued || dotSqueezed input) rest
+    playDash' i dotQueued (input : rest) =
+      playDash' (i - 1) (dotQueued || dotSqueezed input) rest
+
+    -- After playing a '-', we are quiet for one dot time and check the dot lever.
+    waitAfterDash dotQueued [] = ['.' | dotQueued]
+    waitAfterDash dotQueued (input : rest)
+      | dotQueued || dotSqueezed input = playDot (dashSqueezed input) rest
+      | dashSqueezed input = playDash False rest
+      | otherwise = start rest
+```
+
+Finally we can write a `main` function that performs the actual tests:
+
+```haskell
+main :: IO ()
+main = quickCheckWith args testAgainstSpecification
+  where
+    args = stdArgs
+      { replay = Just (mkQCGen 0, 0), -- Fix the random seed for reproducibility
+        maxSuccess = 100000 -- Larger test suite by default
+      }
+```
+
+# Conclusion
+
+Having set all this up QuickCheck immediately found a counter-example:
+
+```text
+*** Failed! Falsified (after 18 tests):
+  -B--BB-B B -.
+"-.-..-" /= "-.-.-."
+```
+
+The input sequence is `-B--BB-B B -.`. The first result is that of the C
+implementation; the second result that of the Haskell specification. The bug
+was easily found and solved, and now no bugs can be found in 100000 test
+cases—with a reasonable amount of certainty, the implementation is correct with
+respect to the specification.
+
+It took some effort to mock the Arduino code and simulate the interrupt service
+routine. Also, with my setup I compile using Arduino headers but link with
+libc. This can give problems. I noticed I could not use `stderr`, for example,
+because the implementation in the Arduino headers is different than the one in
+libc, leading to linking errors. In my case, I could work around this
+reasonably easily.
+
+All of this is less of a problem when the Arduino code is more
+compartmentalized and you can readily compile it with GCC, of course. This does
+incur some overhead during runtime on the Arduino, however (though I don't know
+how much).
+
+All in all, I would certainly consider this approach again with another hard to
+reproduce bug. However, it is clearly most usable when the code you want to
+test is not very Arduino-specific. It remains to be seen at what point you hit
+the limit of how much you can mock.
+
+[Arduino]: https://www.arduino.cc/
+[ATSAMF]: https://a03.veron.nl/projectvoorstel-pa5nn-zelfbouw-qrp-hf-cw-transceiver/
+[ATSAMF-source]: https://github.com/camilstaps/ATSAMF-source/
+[dual-lever paddle]: https://en.wikipedia.org/wiki/Telegraph_key#Dual-lever_paddles
+[Haskell]: https://haskell.org/
+[QuickCheck]: https://hackage.haskell.org/package/QuickCheck/
diff --git a/resources/pug/finals/articles/2021-09-07-testing-arduino-code-with-haskell-quickcheck.pug b/resources/pug/finals/articles/2021-09-07-testing-arduino-code-with-haskell-quickcheck.pug
new file mode 100644
index 0000000..b1e77d5
--- /dev/null
+++ b/resources/pug/finals/articles/2021-09-07-testing-arduino-code-with-haskell-quickcheck.pug
@@ -0,0 +1,18 @@
+extends /layout-articles.pug
+
+block prepend title
+	| Testing Arduino code with QuickCheck - 
+
+block prepend menu
+	- var page = '2021-09-07-testing-arduino-code-with-haskell-quickcheck'
+
+block append breadcrumbs
+	+breadcrumb('Testing Arduino code with Haskell QuickCheck')
+
+block subtitle
+	| Testing Arduino code with Haskell QuickCheck
+block subtitleDate
+	| 7 September 2021
+
+block page
+	include:markdown ../../../md/2021-09-07-testing-arduino-code-with-haskell-quickcheck.md
diff --git a/resources/pug/finals/articles/index.pug b/resources/pug/finals/articles/index.pug
index b9fcfff..9edea4e 100644
--- a/resources/pug/finals/articles/index.pug
+++ b/resources/pug/finals/articles/index.pug
@@ -15,6 +15,14 @@ block page
 		| You can also go back to my #[a(href='/') home page].
 
 	h1
+		a(href='2021-09-07-testing-arduino-code-with-haskell-quickcheck.html').
+			7 September 2021: Testing Arduino code with Haskell QuickCheck
+	blockquote.
+		An Arduino program of mine showed a weird bug, but I couldn't reliably reproduce it.
+		I isolated the relevant C code so that I could run it on a computer, and used Haskell QuickCheck to run automated property tests	against it.
+		With that set up, fixing the bug was a matter of minutes.
+
+	h1
 		a(href='2021-08-02-cloogle-search-overview.html').
 			2 August 2021: Cloogle search overview
 	blockquote.
diff --git a/resources/pug/include/layout-articles.pug b/resources/pug/include/layout-articles.pug
index 2aeaa1c..7b63cca 100644
--- a/resources/pug/include/layout-articles.pug
+++ b/resources/pug/include/layout-articles.pug
@@ -8,6 +8,9 @@ block append menu
 	+menu(
 		{name: 'Home', link: ''},
 		{name: 2021, menu: [
+			{ name: 'Testing Arduino code with Haskell QuickCheck',
+				year: 2021, month: 9, day: 7
+			},
 			{ name: 'Cloogle search overview',
 				year: 2021, month: 8, day: 2
 			},