Safely Detecting Cats with Crux: A Tutorial

A while back, we announced that we were open-sourcing Crux, a software verification tool.

I’d like to work through a slightly more involved example in this post than those presented in the original announcement. In particular, I’d like to give an example of how one might apply Crux to verify functional properties of a system that interacts with the real world using libraries whose source code may not be available.

A System for Detecting Cats

In my spare time, I’ve been developing a IoT for detecting cats. The system depends on a cat detector unit, which is designed to be controlled via a two-pin GPIO interface:

• One input pin for turning the sensor camera on or off, and
• One output pin indicating if a cat is currently detected or not.

While I haven’t made much progress on the cat detector unit, it’s not too early to start programming the controller.

My goal is to build a system that I can control to record whether or not a cat is detected at a given moment in time. There should be two modes of operation:

1. “Idle,” in which I can tell the controller to take a single sample; and
2. “Sampling,” in which I tell the controller to take samples periodically until instructed to stop.

There is one crucial invariant that the controller must guarantee: whenever a sample is taken and recorded, regardless of the mode, the camera must be “on!” The output of the detector, if the camera is off, is meaningless for obvious reasons.

Plan

We’ll write the controller in C, and use libgpiod to interact with the cat detector unit, and we’ll use crux-llvm to check that we’ve gotten everything right. Let’s go!

Warm Up

Setup

Because this tutorial is based around libgpiod, if you want to follow along at home, you’ll need to be using some sort of Linux distribution. Along with the normal C toolchain, you’ll also need crux-llvm (and some dependencies), which you can grab here: https://crux.galois.com/downloads.html. I’ll be trying to keep most source code in a single file – while this isn’t generally the best C development practice, it will simplify some of the presentation here without changing any of the important concepts.

A Sampling library

Before we get started programming the controller, let’s develop the API that we’ll use for recording samples. Recall that we’ll need a data structure in which we can record, for example, that sample i indicates a cat was detected, or that sample j indicates a cat was not detected.

For our purposes, a bitvector should do nicely. The interface should look something like this, where we’re using ints as booleans (ed: sigh).

void set_sample(char *samples, size_t sample, int val);
int  get_sample(char *samples, size_t sample);

That is, set_sample(samples, i, 0) records the absence of a cat at sample i, and set_sample(samples, j, 1) records the presence of a cat at sample j.

A straightforward implementation might look like:

void set_sample(char *samples, size_t sample, int val)
{
  char imask = 1 << (sample % 8);
  if (val == 0)
    samples[sample/8] &= ~imask;
  else
    samples[sample/8] |= imask;
}

int get_sample(char *samples, size_t sample)
{
  char imask = 1 << (sample % 8);
  return (samples[sample/8] & imask) == imask;
}

Testing the library

Before we proceed with the rest of the system, we want to be sure that we’ve gotten this library right. How do we know if this (or any other) implementation is correct? Well, it had better be the case that if I set sample i to b, and then retrieve the value of sample j, then I get b back when i == j, or I get the original value of sample j when i != j.

That is:

int test(char *samples, size_t i, size_t j, int val)
{
  int val_j_orig;
  int val_j;
  
  val_j_orig = get_sample(samples, j);
  set_sample(samples, i, val);
  val_j = get_sample(samples, j);
  
  return (i == j) ? (val_j == val) 
                  : (val_j == val_j_orig);
}

For all but some very small arrays, exhaustively testing all possible inputs just isn’t feasible. With traditional testing, we need to pick out (what we hope are) representative values to test. However, there is no guarantee that a selected set of inputs are actually representative in any meaningful way. Let’s see how we can instead use crux-llvm to prove that the implementation is correct for all inputs for a given array size.

Test Harness

Crux-llvm can symbolically simulate all inputs to our test function. We just need a small harness that will invoke test. Traditionally, a test case might look like the following invocation of test:

int main() 
{
  assert(test(samples, 0, 1, 1));

  return 0;
}

However, this only tells us that test succeeds for the particular values of i, j, and val. Now let’s look at how we can use some functions from the crux-llvm API to build a symbolic test harness. To tell crux-llvm to check test for arbitrary int values for i and j and so on, we use the function crucible_uint32_t() to create the values like so:

int main() 
{
  size_t i = crucible_uint32_t("i");
  size_t j = crucible_uint32_t("j");

We also want to consider arbitrary values of val, which, if we recall, should only have the value 0 or 1. We can construct a test input as follows:

int b = crucible_uint8_t("val") != 0;

Finally, we want to perform the test in some arbitrary sample array¹. We add

#define SIZE 128

to the top of our test file and the following to main():

 char *samples = malloc(SIZE);
 for (int i = 0; i < SIZE; i++)
 {
   samples[i] = crucible_uint8_t("init");
 }

All that’s left is to actually call and check the result of our test. For that we use the check() function from the crux-llvm API. check() is a lot like the more commonly-found assert(). Operationally, if control flow reaches check(e) and e might evaluate to 0, then crux-llvm flags that as an error. If e can never evaluate to 0, then check passes.

 check(test(samples, i, j, b1 != 0));
  
 return 0;
}

Putting it all together,

In tutorial.h:

#include <stdio.h>
#include <unistd.h>

void
set_sample(char *samples, size_t sample, int val);

int
get_sample(char *samples, size_t sample);

in tutorial.c:

#include "tutorial.h"

void
set_sample(char *samples, size_t sample, int val)
{
  char imask = 1 << (sample % 8);
  if (val == 0) samples[sample/8] &= ~imask;
  else          samples[sample/8] |=  imask;
}

int
get_sample(char *samples, size_t sample)
{
  char imask = 1 << (sample % 8);
  return (samples[sample/8] & imask) == imask;
}

And in test_sample.c we have:

#include <stdlib.h>
#include "tutorial.h"
#include "crucible.h"

#define SIZE 128

int test(char *samples, size_t i, size_t j, int val)
{
    int val_j_orig;
    int val_j;

    val_j_orig = get_sample(samples, j);
    set_sample(samples, i, val);
    val_j = get_sample(samples, j);

    return (i == j) ? (val_j == val)
                    : (val_j == val_j_orig);
}

int main()
{
    uint32_t i = crucible_uint32_t("i");
    uint32_t j = crucible_uint32_t("j");
    uint32_t b = crucible_uint32_t("b") != 0;

    char *samples = malloc(SIZE);
    for (int s = 0; s < SIZE; s++)
    {
        samples[s] = crucible_uint8_t("init");
    }

    check(test(samples, i, j, b));
    
    return 0;
}

Running crux-llvm

To check our program with crux-llvm, we run:

$ crux-llvm -O0 tutorial.c test_sample.c

Oh no! Pretty quickly we get a pretty long report. We can limit some of the output by considering only the first failure using the –fail-fast option:

$ crux-llvm -O0 tutorial.c test_sample.c --fail-fast
[Crux] Using pointer width: 64 for file crux-build/crux~tutorial.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] Counterexample found, skipping remaining goals
[Crux] *** debug executable: results/tutorial/debug-15
[Crux] *** break on line: 15
[Crux] Found counterexample for verification goal
[Crux]   tutorial.c:15:11: error: in get_sample
[Crux]   Undefined behavior encountered

Crux-llvm found a counterexample, or an input to our test that causes something to go wrong at tutorial.c:15 (the line numbers may change depending on how you are following along). Reading further, the message indicates this has to do with a pointer being out of bounds, but it’s not totally clear how this came about. Crux-llvm has also built an executable that witnesses the error. We can step through it with gdb to figure out what happened:

$ gdb results/tutorial/debug-15

(gdb) run

We quickly find:

Program received signal SIGSEGV, Segmentation fault.
0x000000000040167e in get_sample (samples=0x4052a0 "", sample=2147483648)
    at sample.c:15
15    return (samples[sample/8] & imask) == imask;

So there was a segmentation fault when accessing samples. That’s odd. Let’s see why:

(gdb) p/d sample
$1 = 2147483648

Aha – we’re trying to access a very large sample, but our array is only 128 bytes (or 1024 samples). We didn’t set up our test correctly! In this case, we need to tell crux-llvm that we want to assume test is only called with valid values i and j. For this, we use assuming() from the crux-llvm API. Unlike check(), when control flow reaches assuming(e), crux-llvm will only consider the current execution if e == 1². Thus, to restrict our test to executions where i and j are valid samples, we add:

assuming(i < 8*SIZE);
assuming(j < 8*SIZE);

before the call to check. (Recall our test array has SIZE bytes and we’re using each of the 8 bits of those bytes.)

Rerunning crux-llvm:

$ crux-llvm tutorial.c test_sample.c
[Crux] Using pointer width: 64 for file crux-build/crux~sample.bc
[Crux] Simulating function "main"
[Crux] Attempting to prove verification conditions.
[Crux] Goal status:
[Crux]   Total: 11
[Crux]   Proved: 11
[Crux]   Disproved: 0
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Valid.

This indicates that crux-llvm did not find any inputs causing the test to return 0. Our implementation is correct!

Building an I/O Library

With that out of the way, let’s turn our attention to building out the actual cat detector system.

First, we’ll write some functions to help us initialize, enable, and query the sensors and camera. Then, we’ll write the main controller logic. As before, we’ll wrap up by showing how to throw together a quick symbolic test harness to help build confidence that our implementation is correct.

Modeling GPIOD in Crux-llvm

With the exception of some built-in support for common C library functions, crux-llvm needs the source code of all of the functions that are called by the program it is analyzing. Unfortunately, our cat-detector doesn’t quite satisfy this requirement, as we plan to link against libgpiod. However, we can take a page from standard software testing techniques and create a mock implementation of libgpiod, using crux-llvm API primitives to ensure we cover interesting behaviors. First, we need to define some types – these are opaque and since we don’t care about their implementation, we can give them empty definitions:

struct gpiod_chip {};
struct gpiod_line {};

We’ll need to mock gpiod_chip_open_by_name() so that we can simulate getting a handle to our chip. The most relevant behavior is that this function can fail for a number of reasons. Instead of digging into the implementation of libgpiod to figure out what these are, we can model failure non-deterministically:

struct gpiod_chip *
gpiod_chip_open_by_name(const char *chipname)
{
  check(chipname != NULL);

  if (crucible_uint8_t("open_succeed")){
    return (struct gpiod_chip *)malloc(sizeof(struct gpiod_chip));
  } else {
    return NULL;
  }
}

There are two interesting things to note here:

1. We’ve decided to enforce the precondition that chipname is not NULL using a call to check;

2. We use crucible_uint8_t() to non-deterministically decide if the function succeeds or fails. When we call this later, crux-llvm will be forced to consider both the error and the success cases.

Another important function will be gpiod_line_get_value(), which reads the value of a GPIO pin. This function can fail (and return -1) or it can successfully read a 0 or 1. To capture all of these behaviors, we use assuming() like so:

int
gpiod_line_get_value(struct gpiod_line *line) {
  check(line != NULL);
  int v = crucible_int8_t("get_value");
  assuming(-1 <= v && v <= 1);

  return v;
}

And that’s all there is to it! The rest of the functions that we’ll need are:

struct gpiod_line *
gpiod_chip_get_line(struct gpiod_chip *chip, unsigned int offset)
{
  check(chip != NULL);
  struct gpiod_line *res = malloc(sizeof(struct gpiod_line));

  if (res && crucible_uint8_t("get_line_succeed")) {
    return res;
  } else {
    return NULL;
  }
}

void
gpiod_chip_close(struct gpiod_chip *chip)
{
  check(chip != NULL);
  free(chip);
}

void gpiod_line_release(struct gpiod_line *line)
{
  check(line != NULL);
}

int
gpiod_line_request_input(struct gpiod_line *line,
                         const char *consumer)
{
  check(line != NULL);
  check(consumer != NULL);

  if(crucible_uint8_t("request_input")) {
    return 0;
  } else {
    return -1;
  }
}


int
gpiod_line_request_output(struct gpiod_line *line,
                          const char *consumer, int default_val)

{
  check(line != NULL);
  check(consumer != NULL);

  if(crucible_uint8_t("request_output")) {
    return 0;
  } else {
    return -1;
  }
}


int
gpiod_line_set_value(struct gpiod_line *line, int value)
{
  check(line != NULL);

  if(crucible_uint8_t("request_output")) {
    return 0;
  } else {
    return -1;
  }
}

I’ve decided to put all of these functions in a file called crux_gpiod.c.

Managing GPIO state

Armed with the mocked library, we can proceed to building our slightly-higher level implementation.

Initialization

Recall that our plan is to use libgpiod to interface with the sensor and camera. We’ll use some global variables for the GPIO state. Let’s add these to the tutorial.c:

// GPIO State
#define CHIP_NAME "gpiochip0"
#define CONSUMER "cat_sensor"
#define CAMERA_ENABLE_LINE 0
#define SENSOR_IN_LINE 1
struct gpiod_chip *chip;
struct gpiod_line *sensor_in_line;
struct gpiod_line *camera_enable_line;

We’ll need a function for initializing all of this state:

int
initialize_sensors()
{
    int req_err;
    struct gpiod_chip *chip = gpiod_chip_open_by_name(CHIP_NAME);
    if (!chip) return -1;

    sensor_in_line = gpiod_chip_get_line(chip, SENSOR_IN_LINE);
    camera_enable_line = gpiod_chip_get_line(chip, CAMERA_ENABLE_LINE);
    if (!sensor_in_line || !camera_enable_line) return -1;

    req_ok  = gpiod_line_request_input(sensor_in_line, CONSUMER);
    req_ok |= gpiod_line_request_output(camera_enable_line, CONSUMER, 0);

    return req_err;
}

The details here aren’t super important. All this function does is call out to libgpiod to actually find the chip, and then gives us handles to the cat sensor and camera enable lines. The important thing is that these operations can fail: hence initialize_sensors fails if any of these operations fail themselves.

Manipulating Sensors

Next, we need a function for manipulating the camera. We’ll use a global variable to remember the state of the camera:

int camera_enabled;

And we’ll use that to help implement switch_camera, which we use to turn on/off the camera.

int
switch_camera(int enable)
{
    if (0 == gpiod_line_set_value(camera_enable_line, enable)) {
      camera_enabled = enable;
      return 0;
    }

    return -1;
}

Finally, we’ll use a global buffer for sample storage

// Sample buffer
#define SAMPLE_BUFFER_SIZE 256
#define NUM_SAMPLES (8*SAMPLE_BUFFER_SIZE)
char samples[SAMPLE_BUFFER_SIZE];

and use that in the implementation of collect_sample(), which we’ll use for, well, collecting samples. Recall that a functional requirement of the system is that the camera is on before collecting a sample. We add a call to check() to check the precondition that the camera is enabled whenever we try to collect a sample.

int
collect_sample(size_t i)
{
    check(camera_enabled);

    int is_cat = gpiod_line_get_value(sensor_in_line);
    if (is_cat >= 0){
        set_sample(&samples[0], i, is_cat);

        return is_cat;
    }

    return -1;
}

Testing our library

Let’s build a little test harness for what we have so far. The main capabilities we have at the moment are the ability to initialize the system, the ability to turn the camera on, and finally the ability to record a sample. Let’s try to verify that these pieces all fit together in the expected way, using the following test (which I’ve dumped into test_initialize.c):

#include "tutorial.h"
#include "crucible.h" 

int main()
{
    if (0 == initialize_sensors())
    {
        if (0 == switch_camera(1))
        {
            size_t i = crucible_uint32_t("i");
            collect_sample(i);
        }
    }
}

Let’s try running crux-llvm on this test:

$ crux-llvm -O0 crux_gpiod.c tutorial.c test_initialize.c --fail-fast
[Crux] Using pointer width: 64 for file crux-build/crux~crux_gpiod.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] Counterexample found, skipping remaining goals
[Crux] *** debug executable: results/crux_gpiod/debug-9
[Crux] *** break on line: 9
[Crux] Found counterexample for verification goal
[Crux]   tutorial.c:9:17: error: in set_sample
[Crux]   Undefined behavior encountered
[Crux]   Details:
...

What’s happened here? Using gdb as before, we see that we’ve called collect_sample() with too large a value. Since collect_sample() ought to know the size of the array it is indexing (e.g., that it has NUM_SAMPLES samples), it should really perform some bounds checking. We add the following guard to the body of collect_sample():

int
collect_sample(size_t i)
{
  if (i < NUM_SAMPLES) {
    // Original body goes here...
  }
  
  return -1;
}

Rerunning crux-llvm confirms the fix:

crux-llvm -O0 crux_gpiod.c tutorial.c test_initialize.c --fail-fast
[Crux] Using pointer width: 64 for file crux-build/crux~crux_gpiod.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] Goal status:
[Crux]   Total: 16
[Crux]   Proved: 16
[Crux]   Disproved: 0
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Valid.

Controller Logic

Let’s put everything together and build the main controller logic.

Recall that we want to support two modes of operation: an “idle” mode that allows the user to collect individual samples, and a “sampling” mode that automatically collects samples at some rate.

We’ll implement the main logic of a controller as a procedure, take_step, that responds to different external events:

1. A TAKE_ONE_SAMPLE event, indicating that the user has asked the system to record a sample. This should only have an effect in the “idle” mode.

2. BEGIN_SAMPLING/END_SAMPLING events, indicating that the user has asked the system to start or stop sample recording. This event will be accompanied by the amount of time to wait between samples.

3. A TICK event, denoting the passage of some fixed time interval. We’ll use this to implement the “sampling” mode.

Into tutorial.h we throw:

typedef enum mode {
  IDLE=0,
  SAMPLING=1,
  NUM_MODES=2
} mode_t;

typedef enum event {
  TAKE_ONE_SAMPLE=0,
  BEGIN_SAMPLING=1,
  END_SAMPLING=2,
  TICK=3,
  NUM_OPS=4
} event_t;

// Current mode
sample_mode_t mode;

int 
take_step(event_t cmd, void *arg)
{
  int err = 0;
  size_t i;
  switch(cmd) 
  {
    case TAKE_ONE_SAMPLE:
      // handle sample request ...
    case BEGIN_SAMPLING:
      // start sampling
    case END_SAMPLING:
      // end sampling
    case TICK:
      // update timer
    default: break; 
  }
  
  return err;
}

Let’s take a look at implementing the handlers for each of these commands:

TAKE_ONE_SAMPLE

This case is pretty straightforward. We get the index of the sample the user is requesting, and call our collect_sample() procedure:

case TAKE_ONE_SAMPLE:
  if (mode != IDLE)
    break;

  i = *(size_t *)arg;
  if ((err = switch_camera(1)))
    break;

  err |= (collect_sample(i) < 0);
  err |= switch_camera(0);
  break;

We turn the camera on before collecting the sample, and to save power we turn the camera back off.

TICK

Next we’ll implement the logic that updates the timer that BEGIN_SAMPLING/END_SAMPLING depend on. Since we’ll be sampling at some frequency, we need some sort of timer to tell us when to take the next sample, and we need to know what the index of the next sample is. We’ll implement these as globals.

unsigned int sample_reload;
unsigned int sample_timer;
size_t current_sample;

I don’t know what a good sample period is, and maybe we’ll want the user to be able to configure this, so we’ll make this a global value that gets initialized by adding a parameter to initialize:

int
initialize(unsigned int sample_reload_value)
{
   ...
   sample_reload = sample_reload_value;
   ...
}

Next we’ll need a procedure tick_sample() that updates the timer, collects a sample when the timer reaches 0, and resets the timer when it expires.

int
tick_sample()
{
    if (mode == SAMPLING && sample_timer > 0) {
        sample_timer--;

        if(sample_timer == 0) {
            int err = collect_sample(current_sample);
            sample_timer = sample_reload;
            current_sample++;
            return err;
        }
    }

    return 0;
}

We’ll just call this in take_step:

case TICK:
  err = tick_sample();
  break;

BEGIN_SAMPLING/END_SAMPLING

To implement these commands, we’ll build a simple timer out of a global variable that we’ll then update every TICK. We’ll also grab the starting sample and store that in a global:On BEGIN_SAMPLING, we’ll load this timer and change our mode to SAMPLING. On END_SAMPLING we will change the mode back to IDLE, and set the timer to 0 out of politeness.

case BEGIN_SAMPLING:
    if (mode != IDLE)
        break;
    mode = SAMPLING;
    sample_timer = SAMPLE_RATE;
    current_sample = *(size_t *)arg;
    break;

case END_SAMPLING:
    if (mode != SAMPLING)
        break;
    mode = IDLE;
    sample_timer = 0;
    break;

Have we forgotten anything? Not sure, but let’s press on.

Initialization

We’ve introduced a lot of global state here. We need to initialize that, plus the GPIO devices.

int
initialize(unsigned int sample_reload_value)
{
    current_sample = 0; // for timer
    camera_enabled = 0;
    mode = IDLE;
    sample_reload  = sample_reload_value;

    return initialize_sensors();
}

Testing

OK let’s check our implementation so far. I put the following in test_take_step.c:

#include "crucible.h"
#include "tutorial.h"

int main()
{
    unsigned char sample_reload = crucible_uint8_t("sample");
    assuming(sample_reload > 0);

    int init_ok = initialize(sample_reload);
    assuming(!init_ok);

    int steps = 5;
    op_t op;
    size_t arg;
    int err = 0;
    while(steps --> 0) {
        op = crucible_uint8_t("op");
        assuming (op < NUM_OPS);
        arg = crucible_uint32_t("arg");
        assuming (arg < NUM_SAMPLES);
        switch (op)
        {
            case END_SAMPLING:
            case TICK:
                take_step(op, NULL);
                break;
            default:
                take_step(op, &arg);
                break;
        }
    }

    return 0;
}

This program runs a sequence of five steps³. Each time, we make a non-deterministic choice of operation via op = crucible_uint8_t("op") and argument via arg = crucible_uint32_t("arg"). I’m using assuming() to ensure that these values are valid. The switch simply invokes take_step() with or without a value for arg.

Let’s give this a spin with crux-llvm (but by now you probably have an idea of where this is going):

crux-llvm tutorial.c crux_gpiod.c test_take_step.c -O0 --fail-fast
[Crux] Using pointer width: 64 for file crux-build/crux~tutorial.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] Counterexample found, skipping remaining goals
[Crux] *** debug executable: results/tutorial/debug-77
[Crux] *** break on line: 77
[Crux] Found counterexample for verification goal
[Crux]   tutorial.c:77:0: error: in collect_sample
[Crux]   crucible_assert
[Crux] Goal status:
[Crux]   Total: 37
[Crux]   Proved: 36
[Crux]   Disproved: 1
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.

What happened this time? You know the drill:

$ gdb results/tutorial/debug-77...
(gdb) break take_step
Breakpoint 1 at 0x40195f: file tutorial.c, line 124.
(gdb) run
Starting program: /home/abakst/tutorial/results/tutorial/debug-77

Breakpoint 1, take_step (cmd=BEGIN_SAMPLING, arg=0x7fffffffe2a0) at tutorial.c:124
124   int err = 0;
(gdb) c
Continuing.

Breakpoint 1, take_step (cmd=TICK, arg=0x0) at tutorial.c:124
124   int err = 0;
(gdb) c
Continuing.
tutorial.c:77: Assertion failed.

We run BEGIN_SAMPLING then TICK, and then, we hit fail the assert in collect_sample(). Of course, we forgot to turn the camera on in the handler for BEGIN_SAMPLING. We need:

...
    case BEGIN_SAMPLING:
      if (mode != IDLE)
          break;
      mode = SAMPLING;
      sample_timer = sample_reload;
      current_sample = *(size_t *)arg;
      if ((err = switch_camera(1)))
        break;
      break;

    case END_SAMPLING:
      if (mode != SAMPLING)
        break;
      mode = IDLE;
      sample_timer = 0;
      err = switch_camera(0);
      break;
...

Let’s try again:

crux-llvm tutorial.c crux_gpiod.c test_take_step.c -O0 --fail-fast
[Crux] Using pointer width: 64 for file crux-build/crux~tutorial.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] Counterexample found, skipping remaining goals
[Crux] *** debug executable: results/tutorial/debug-77
[Crux] *** break on line: 77
[Crux] Found counterexample for verification goal
[Crux]   tutorial.c:77:0: error: in collect_sample
[Crux]   crucible_assert
[Crux] Goal status:
[Crux]   Total: 36
[Crux]   Proved: 35
[Crux]   Disproved: 1
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.

What? The same error? Let’s use gdb figure it out:

(gdb) break take_step
Breakpoint 1 at 0x40195f: file tutorial.c, line 124.
(gdb) run
Starting program: /home/abakst/tutorial/results/tutorial/debug-77

Breakpoint 1, take_step (cmd=BEGIN_SAMPLING, arg=0x7fffffffe2a0) at tutorial.c:124
124   int err = 0;
(gdb) n
127   switch(cmd)
(gdb) n
142       if (mode != IDLE)
(gdb) n
144       mode = SAMPLING;
(gdb) n
145       sample_timer = sample_reload;
(gdb) n
146       current_sample = *(size_t *)arg;
(gdb) n
147       if ((err = switch_camera(1)))
(gdb) n
148         break;

Interestingly, switch_camera() returned an error! But it turns out we don’t actually do anything with this error aside from returning it – that’s our problem! Even though we failed to turn the camera on, we continued like nothing happened.

An ABORT mode

A good idea is to have the controller probably enter an ABORT state when it hits a problem. We can add this to the sample_mode_t type:

typedef enum mode {
  IDLE=0,
  SAMPLING=1,
  ABORT=2,
  NUM_MODES=3,
} sample_mode_t;

And then at the beginning of take_step(), simply return if we’ve aborted. At the end of take_step(), we change the mode to ABORT if we encountered an error.

int
take_step(event_t cmd, void *arg)
{
  int err = 0;
  size_t i;

  if (mode == ABORT)
    return;
    
  switch (cmd) {
    // ...
  }
  
  if (err)
    mode = ABORT;
    
  return err;
}

If we re-run crux-llvm, we should see the verification succeed.

Testing Redux

Actually, now that we’ve exposed an ABORT state denoting that some application-specific invariant has been broken, a good property to check would be that in the absence of hardware (libgpiod) failures, we never actually hit the ABORT state. While there are a number of ways we might specify this, let’s take a look at the following simple approach.

First, we need a way to disable (libgpiod) failures. For this, we add

unsigned int crux_gpiod_no_failure;

#define FAIL() assuming(crux_gpiod_no_failure == 0);

in our mock gpiod implementation, and then add FAIL() before returning an error in the various gpiod_* functions. When crux_gpiod_no_failure is 0 (false), then FAIL() is equivalent to assuming(0 == 0), or assuming(1), which has no effect on the symbolic execution.

Otherwise FAIL() is equivalent to assuming(1 == 0) or assuming(0), which has the effect of blocking crux-llvm from considering paths through it. 

For example, our mock implementation of gpiod_chip_open_by_name() now looks like:

struct gpiod_chip *
gpiod_chip_open_by_name(const char *chipname)
{
  check(chipname != NULL);

  if (crucible_uint8_t("open_succeed")){
    return (struct gpiod_chip *)malloc(sizeof(struct gpiod_chip));
  } else {
    FAIL();
    return NULL;
  }
}

When FAIL() expands to assuming(0), all executions of our program that pass through the else branch of gpiod_chip_open_by_name() will be ignored, thus ignoring the case where gpiod_chip_open_by_name() fails. 

Now let’s add an assertion to take_step() that we never actually reach an ABORT state. To do so, we add

extern unsigned int crux_gpiod_no_failure;

to our tutorial.h header file, and add

if (crux_gpiod_no_failure)
  check(mode != ABORT);

to the end of the body of take_step(), and that’s it.

Let’s give this a spin. In the body of main of test_take_step.c, add the assignment:

crux_gpiod_no_failure = crucible_uint8_t("hw_failure") == 0;

This will simultaneously test both cases: when hardware failures are enabled and when they are ignored.

$ crux-llvm tutorial.c crux_gpiod.c test_take_step.c -O0 --fail-fast
[Crux] Using pointer width: 64 for file crux-build/crux~tutorial.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] Counterexample found, skipping remaining goals
[Crux] *** debug executable: results/tutorial/debug-174
[Crux] *** break on line: 174
[Crux] Found counterexample for verification goal
[Crux]   tutorial.c:174:0: error: in take_step
[Crux]   crucible_assert
[Crux] Goal status:
[Crux]   Total: 94
[Crux]   Proved: 93
[Crux]   Disproved: 1
[Crux]   Incomplete: 0
[Crux]   Unknown: 0
[Crux] Overall status: Invalid.

Predictable at this point, but, yes, this reveals another failure. Firing up gdb and stepping through take_step(), we see that mode is assigned ABORT after a TICK command. Inspecting tick_sample(), we can see that this will only happen if collect_sample() returns an error, and since hardware errors are disabled, this will only happen if the requested sample is out of bounds – which means current_sample() must have gone out of bounds!

Staring at the implementation of tick_sample(), the expression current_sample++ looks rather fishy: given a large enough starting value and enough TICKs, we’ll eventually exceed the number of samples. Let’s replace that with:

current_sample = (current_sample + 1) % NUM_SAMPLES;

Let’s check our work with crux-llvm:

$ crux-llvm tutorial.c crux_gpiod.c test_take_step.c -O0 --fail-fast
[Crux] Using pointer width: 64 for file crux-build/crux~tutorial.bc
[Crux] Simulating function main
[Crux] Attempting to prove verification conditions.
[Crux] Goal status:
[Crux]   Total: 205
[Crux]   Proved: 205
[Crux]   Disproved: 0
[Crux]   Incomplete: 0
[Crux]   Unknown: 0

Awesome!

What have we done?

Now let us take a step back and evaluate our work, and interpret what it tells us about the system we have built. While crux-llvm now reports our tests are Valid, we need to be precise about what this actually means.

libgpiod Stubs: To analyze code that uses a third-party I/O library, I wrote a mock implementation using crux-llvm primitives to model, for example, failure as non-deterministic choice. These mock implementations are intended to be approximations of the actual behavior of libgpiod. However, it is crucial to make sure this is actually the case: if I had forgotten a failure case in one of the stub implementations, for example, then that could invalidate the results of the analysis.

Fixed array sizes: in our tests, we have fixed the sizes of our sample arrays⁴. Thus, whatever results we report about the correctness of the system are limited to the concrete sizes tested.

Fixed step sizes: the test in test_next_step is restricted to a bounded number of executions. It is possible that there are bugs waiting to be discovered by increasing the bound. We can gain confidence by increasing this bound and letting crux-llvm run longer.

Nevertheless, because we consider all executions (up to some fixed size), we can be reasonably confident that we have not forgotten to test some obscure corner case.

Wrapping up

In this brief introduction, we have touched on a few concepts:

• Setting up a symbolic test harness and executing the test with crux-llvm
• Modeling a third party I/O library
• Debugging failed tests, both when the test is incorrect and when there are real bugs

We’d love feedback on these tools: feel free to file issues here or contact us at crux@galois.com!

Footnotes

[1] We use a fixed size here. Generally, crux-llvm should only be used with fixed-size data structures. The reasons are a bit technical, but in this case, if we wanted to run our test for arbitrary array sizes, crux-llvm would effectively try for arrays of size 0, then 1, then 2,… etc. and hence fail to terminate in a reasonable time.

[2] As a consequence, for example, check(0); assuming(0); will be flagged by crux-llvm as an assertion failure, whereas assuming(0); check(0) will not. The following example adds some intuition for the relationship between assuming() and check():

cond = crucible_uint8_t("cond");

assuming(!cond);

if(cond)
  check(0);

Crux-llvm will not flag the check(0) call above, because assuming(!cond) restricts the analysis to only those executions where cond is false.

[3] As with arrays, we test over a fixed number of iterations. In general, crux-llvm requires all loops to terminate after a bounded number of iterations. The interested reader might try using crucible_uint8_t() and assuming() to check a range of iterations. Crux-llvm also allows bounding loop iterations at the command line via the -i/–iteration-bound flag.