Agolic

How Agolic tests your program

Even a simple program
can hide a bug.

This example checks a four-character input and one input crashes it. Find it, then see how Agolic looks for it with each technique.

Your program

The program

/* rows[1] to rows[40] hold the rows */
const char *lookup(const char *input) {
    if (strlen(input) != 4)
        return "invalid input";
    if (input[0] != 'A' || input[1] != '7')
        return "invalid input";
    if (input[2] < '0' || input[2] > '9' ||
        input[3] < '0' || input[3] > '9')
        return "invalid input";
    int n = (input[2] - '0') * 10
          + (input[3] - '0');
    if (n > 40)
        return "out of range";
    return rows[n]->text;
}

Try an input

····

Type a four-character input.

The program says which check stopped you.

The try box needs JavaScript. A712 returns row 12.

Four checks, then a lookup.

The techniques

The technique

Symbolic execution

Tool KLEE

Leave the input open and follow every path at once.

A solver works out A700. Row 0 is not in the table, so it crashes.

Coverage-guided fuzzing

Tool AFL++

Change inputs at random and keep the ones that reach new lines.

A700 reaches the last line and it crashes.

Concolic execution

Tool SymCC

Run a seed, then go back and flip one branch at a time.

On the second round the solver picked 00 and A700 crashed.

Hybrid fuzzing

Tool AFL++ with SymCC

The fuzzer explores and a solver writes inputs that pass the checks.

The solver wrote A712 and the fuzzer found A700.

Bounded model checking

Tool CBMC

Cover every input with one formula, then ask the solver.

Can the lookup ever crash? Yes, A700 does.

Property-based testing

Tool theft

Write a rule and a generator, then look for a counterexample.

A700 breaks the rule.

Generated tests

Tool Agolic (built in)

Read the source and docs, then write the test.

The docs say rows 1 to 40. The test expects out of range and gets a crash, so the test fails.

Your own

Build your own tool with Agolic.

Every technique here began as someone's idea. Agolic runs yours beside them.

Which way is best?

This example is simple enough to fit on a page, so they can all get there. Agolic is built for real programs, large ones included, where no technique today wins every time. Each one trades a strength for another and our paper measures some of those trade-offs. Maybe you will build the tool that beats them all.

Read the paper