From 3f7507cfaa516a17f566947f49ac6c0649a9b7dc Mon Sep 17 00:00:00 2001 From: Camil Staps Date: Sat, 21 Aug 2021 17:04:29 +0200 Subject: Add article about Arduino and QuickCheck --- ...testing-arduino-code-with-haskell-quickcheck.md | 445 +++++++++++++++++++++ 1 file changed, 445 insertions(+) create mode 100644 resources/md/2021-09-07-testing-arduino-code-with-haskell-quickcheck.md (limited to 'resources/md/2021-09-07-testing-arduino-code-with-haskell-quickcheck.md') 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/ -- cgit v1.2.3