diff --git a/seahorn/leftpad.c b/seahorn/leftpad.c new file mode 100644 index 0000000..659f1b4 --- /dev/null +++ b/seahorn/leftpad.c @@ -0,0 +1,78 @@ +/* Leftpad, proved with SeaHorn: https://seahorn.github.io/ + * + * Verify with: sea pf leftpad.c + * "unsat" means the verification conditions are unsatisfiable, + * i.e. no execution can violate an assertion: leftpad is correct. + */ +#include "seahorn/seahorn.h" +#include + +/* External functions with no definition are treated by SeaHorn as + * returning an arbitrary (nondeterministic) value. */ +extern int nd_int(void); +extern char nd_char(void); + +/* SeaHorn built-in: marks `size` bytes at `ptr` as holding arbitrary + * values. */ +extern void memhavoc(void *ptr, size_t size); + +static int max(int a, int b) { return a > b ? a : b; } + +/* The code under verification. Pads string `s` of length `len` on the + * left with `c` up to length `n`, writing into `out`. Returns the + * number of characters written. */ +int leftpad(char c, int n, const char *s, int len, char *out) { + int pad = n - len; + if (pad < 0) + pad = 0; + for (int i = 0; i < pad; ++i) + out[i] = c; + for (int i = 0; i < len; ++i) + out[pad + i] = s[i]; + return pad + len; +} + +/* The verification harness. Every value is arbitrary, so proving the + * assertions here proves them for ALL inputs. */ +int main(void) { + char c = nd_char(); + int n = nd_int(); + int len = nd_int(); + assume(len >= 0); /* a string's length is non-negative */ + + int expected = max(n, len); + int pad = expected - len; + + /* Specs 2 and 3 are universally quantified over positions, so we + * check them at an arbitrary symbolic index j. Since j is arbitrary, + * proving the assertion proves it for every position at once. We + * pick j *before* the loops run, so that the loop invariants Spacer + * must infer only concern the single cell out[j] and stay + * quantifier-free. j is only constrained to be non-negative: the + * guards below decide whether it falls in the prefix, the suffix, + * or (when j >= expected) outside the output, where there is + * nothing to assert. Additionally assuming j < expected (i.e. + * assume(j >= 0 && j < expected)) would make the combined + * assumption unsatisfiable when expected == 0, silently pruning + * those inputs and leaving Spec 1 unverified for them. */ + int j = nd_int(); + assume(j >= 0); + + /* An arbitrary string: `len` nondeterministic characters. */ + char *s = malloc(len); + memhavoc(s, len); + char *out = malloc(expected); + + int outlen = leftpad(c, n, s, len, out); + + /* Spec 1: the length of the output is max(n, len). */ + sassert(outlen == expected); + if (j < pad) + /* Spec 2: the prefix is padding characters, and nothing else. */ + sassert(out[j] == c); + else if (j < expected) + /* Spec 3: the suffix is the original string. */ + sassert(out[j] == s[j - pad]); + + return 0; +} diff --git a/seahorn/readme.md b/seahorn/readme.md new file mode 100644 index 0000000..78e8cd4 --- /dev/null +++ b/seahorn/readme.md @@ -0,0 +1,72 @@ +# [SeaHorn](https://seahorn.github.io/) + +## About SeaHorn + +SeaHorn is an automated verification framework for LLVM-based +languages. It takes a C program with assertions, compiles it to LLVM +bitcode, translates the bitcode into Constrained Horn Clauses (CHCs), +and hands those to the [Spacer](https://spacer.bitbucket.io/) solver +built into Z3. Spacer searches for an inductive invariant that proves +every assertion, or for a concrete execution that violates one. + +The proof here, `leftpad.c`, contains no loop invariants, lemmas, or +proof hints, only the implementation and the specification (as +assertions); the invariants needed to prove the loops correct are +inferred by the solver. The +[Dafny](../dafny/Leftpad.dfy) and [Frama-C](../frama-c/leftpad.c) +proofs verify similar imperative code but annotate their loops with +explicit invariants; the [smtlib](../smtlib/leftpad.smt) and +[z3py](../z3py/leftpad.py) proofs are equally automatic but prove a +declarative definition of leftpad rather than loop code. The trade-off +for the automation is less control: if the solver diverges, you cannot +supply the missing invariant annotation; you have to reshape the +problem instead. + +## About the proof + +The code under verification is an ordinary imperative `leftpad`: two +loops writing into an output buffer. The proof lives in `main`, a +verification harness in which every input (the pad character, the +target length, the string contents and its length) is nondeterministic, +so proving the assertions proves them for all inputs. There are no +upper bounds on the string length or the padding. + +The three properties of leftpad are checked as follows: + +1. The length of the output is `max(n, len(str))`: asserted directly + on the length returned by `leftpad`. + +2 & 3. The prefix is all padding and the suffix is the original + string. These properties are universally quantified over every + position of the output. Instead of a quantified assertion, the + harness picks a + single symbolic index `j`, constrained only to be non-negative, and + asserts the property at `out[j]` whenever `j` falls inside the + output. Since `j` is arbitrary, SeaHorn must prove the assertion + for every value of `j`, which is the universally quantified + property. This keeps the invariants Spacer needs quantifier-free. + +The only assumption on the inputs is `len >= 0`, which says the input +string has a non-negative length. + +One caveat: SeaHorn's default encoding models signed integer +arithmetic as exact mathematical arithmetic, so this proof does not +account for overflow of `n - len`. + +## Running it + +With [Docker](https://hub.docker.com/r/seahorn/seahorn-llvm14): + +``` +docker run --rm -v $(pwd):/host -it seahorn/seahorn-llvm14:nightly \ + sea pf /host/leftpad.c +``` + +SeaHorn prints `unsat`, meaning the verification conditions are +unsatisfiable: no execution of `leftpad` can violate the specification. + +## About me + +I'm [John Lu](https://johnlyu2.github.io/), a PhD student at +UWaterloo. My research interests are at the intersection of formal +methods and machine learning.