From bd124c027ac27cfd81238961efef7e215c390f9c Mon Sep 17 00:00:00 2001 From: Alistair Michael Date: Thu, 12 Oct 2023 16:59:11 +1000 Subject: [PATCH] add example with quantified specs --- .../simplified_http_parse_basic/example.c | 35 ++++++++ .../simplified_http_parse_basic/example.spec | 57 +++++++++++++ .../simplified_http_parse_basic/malloc.md | 26 ++++++ .../string-specs.md | 84 +++++++++++++++++++ 4 files changed, 202 insertions(+) create mode 100644 examples/simplified_http_parse_basic/example.c create mode 100644 examples/simplified_http_parse_basic/example.spec create mode 100644 examples/simplified_http_parse_basic/malloc.md create mode 100644 examples/simplified_http_parse_basic/string-specs.md diff --git a/examples/simplified_http_parse_basic/example.c b/examples/simplified_http_parse_basic/example.c new file mode 100644 index 000000000..69ba0603c --- /dev/null +++ b/examples/simplified_http_parse_basic/example.c @@ -0,0 +1,35 @@ +#include +#include +#include + +#define MALLOC_SIZE 10 + + +// cntlm 22 + +char *buf; +char password = 7; // secret value; has to be a variable so that we get a Gamma_password variable +char stext[11] = "sometext"; + + + +int main() { + char *pos = NULL, *dom = NULL; + + + stext[5] = password; + buf = malloc(strlen(stext) + 1); + memcpy(buf, stext, strlen(stext) + 1); // inlined by -O2 + + puts(buf); + + // find the split between username and password ("username:password") + pos = buf + 2; + + *pos = 0; + + memset(buf, 0, strlen(buf)); + free(buf); // requires secret[i] == true + +} + diff --git a/examples/simplified_http_parse_basic/example.spec b/examples/simplified_http_parse_basic/example.spec new file mode 100644 index 000000000..a17b48513 --- /dev/null +++ b/examples/simplified_http_parse_basic/example.spec @@ -0,0 +1,57 @@ +Globals: +password: char +buf: long +stext: char[11] + + +DIRECT functions: gamma_load64, gamma_load8, memory_load8_le, bvult64, bvule64, bvsub64 + + +Subroutine: #free +Requires DIRECT: "gamma_load64(Gamma_mem, R0)" +Ensures DIRECT: "Gamma_R0 == true" + + +Subroutine: main +Requires: Gamma_password == false + + +Subroutine: malloc +Modifies: R0 +Ensures: buf == old(buf) && password == old(password) +// modifies R0, Gamma_R0; +Ensures DIRECT: "R0 == 990000bv64" +Ensures DIRECT: "Gamma_R0 == true" + + +Subroutine: memcpy +Modifies: mem +Ensures: buf == old(buf) && password == old(password) && stext==old(stext) + Ensures DIRECT: "((memory_load64_le(mem, $buf_addr) == old(memory_load64_le(mem, $buf_addr))) && (memory_load8_le(mem, $password_addr) == old(memory_load8_le(mem, $password_addr))))" + // Works + //ensures (forall i: bv64 :: {mem[i]} (memory_load8_le(mem, i) == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then memory_load8_le(old(mem), bvadd64(bvsub64(i, R0), R1)) else old(memory_load8_le(mem, i)))); + // Faster + Ensures DIRECT: "(forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then memory_load8_le(old(mem), bvadd64(bvsub64(i, R0), R1)) else old(memory_load8_le(mem, i))))" + // Does not verify with removed \0 write + // ensures (forall i: bv64 :: (memory_load8_le(mem, i) == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then memory_load8_le(old(mem), bvadd64(bvsub64(i, R0), R1)) else old(memory_load8_le(mem, i)))); + +// forall i <= n, Gamma_mem[R0] low +Subroutine: memset + Modifies: mem + Ensures DIRECT: "(forall i: bv64 :: (Gamma_mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then Gamma_R1 else old(Gamma_mem[i])))" + // Works + //ensures (forall i: bv64 :: {mem[i]} (memory_load8_le(mem, i) == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then R1[8:0] else old(memory_load8_le(mem, i)))); + // Faster + Ensures DIRECT: "(forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then R1[8:0] else old(memory_load8_le(mem, i))))" + // Does not verify with removed \0 write + // ensures (forall i: bv64 :: (memory_load8_le(mem, i) == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then R1[8:0] else old(memory_load8_le(mem, i)))); + + +Subroutine: strlen + Ensures: buf == old(buf) && password == old(password) + Ensures DIRECT: "Gamma_R0 == true" + Ensures DIRECT: "(forall i: bv64 :: (((bvule64(0bv64, i)) && (bvult64(i, R0)) ==> (mem[bvadd64(old(R0), i)] != 0bv8))))" + Ensures DIRECT: "(mem[bvadd64(old(R0), R0)] == 0bv8)" + Ensures DIRECT: "(bvule64(old(R0), bvadd64(old(R0), R0)))" // doesnt overflow + + diff --git a/examples/simplified_http_parse_basic/malloc.md b/examples/simplified_http_parse_basic/malloc.md new file mode 100644 index 000000000..6d62aedb8 --- /dev/null +++ b/examples/simplified_http_parse_basic/malloc.md @@ -0,0 +1,26 @@ + +This has been tested with minimal examples + +Allocator gives a new pointer to a region disjoint from all other regions on each call. + +Todo: Representation compatible with reusing allocated regions that have been freed. + +```bpl +var malloc_count: int; +var malloc_base: [int]bv64; +var malloc_end: [int]bv64; + +procedure malloc(); +modifies mem, Gamma_mem, malloc_count, malloc_base, malloc_end, R0, Gamma_R0; +requires Gamma_R0 == true; +ensures Gamma_R0 == true; +ensures malloc_count == old(malloc_count) + 1; +ensures bvuge64(malloc_end[malloc_count], malloc_base[malloc_count]); +ensures R0 == malloc_base[malloc_count]; +ensures malloc_end[malloc_count] == bvadd64(R0, old(R0)); +ensures (forall i: int :: i != malloc_count ==> bvugt64(malloc_base[malloc_count], malloc_end[i]) || bvult64(malloc_end[malloc_count], malloc_base[i])); +ensures (forall i: int :: i != malloc_count ==> malloc_base[i] == old(malloc_base[i]) && malloc_end[i] == old(malloc_end[i])); +ensures bvuge64(R0, 100000000bv64); // above the got +``` + + diff --git a/examples/simplified_http_parse_basic/string-specs.md b/examples/simplified_http_parse_basic/string-specs.md new file mode 100644 index 000000000..826586373 --- /dev/null +++ b/examples/simplified_http_parse_basic/string-specs.md @@ -0,0 +1,84 @@ +We want general specs for standard library functions and with this example +we made some progress on that front. + +Generalising specifications often requires quantification to summarise loops, +and this requires dealing with the challenges of triggers. + +### Triggers + +In short quantifications are not instantiated in Z3 unless they are 'triggered' +by some existing facts pattern-matching against a chosen subexpression of the +quantification. Normally boogie and Z3 try to choose triggers, but can +struggle if the quantification is not in a "nice" form. Without a good trigger +Z3 responds as if the quantification does not exist, appearing to give "incorrect" +counterexamples. + +In short quantifications which have simple sub-expressions in the left-hand-side +(i.e. the facts we begin with and try to deduce from) to trigger instantiation on +work better. + +Quantification instantiation can also be less reliable when you would +want to trigger on expressions hidden behind a function call, +so it is more reliable to write `mem[i]` than `memory_load8_le(mem, i)`. + + +For example, for the `memset` function the following **does** work: + +```bpl +procedure memset(); + modifies mem, Gamma_mem; + ensures (forall i: bv64 :: (Gamma_mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then Gamma_R1 else old(Gamma_mem[i]))); + // Works + //ensures (forall i: bv64 :: {mem[i]} (memory_load8_le(mem, i) == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then R1[8:0] else old(memory_load8_le(mem, i)))); + // Faster + ensures (forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then R1[8:0] else old(memory_load8_le(mem, i)))); + // Does not verify + // ensures (forall i: bv64 :: (memory_load8_le(mem, i) == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then R1[8:0] else old(memory_load8_le(mem, i)))); +``` + +Similarly for `memcpy` + + +```bpl +procedure memcpy(); + modifies mem, Gamma_mem; + // Works + //ensures (forall i: bv64 :: {mem[i]} (memory_load8_le(mem, i) == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then memory_load8_le(old(mem), bvadd64(bvsub64(i, R0), R1)) else old(memory_load8_le(mem, i)))); + // Faster + ensures (forall i: bv64 :: (mem[i] == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then memory_load8_le(old(mem), bvadd64(bvsub64(i, R0), R1)) else old(memory_load8_le(mem, i)))); + // Does not verify + // ensures (forall i: bv64 :: (memory_load8_le(mem, i) == if (bvule64(R0, i) && bvult64(i,bvadd64(R0, R2))) then memory_load8_le(old(mem), bvadd64(bvsub64(i, R0), R1)) else old(memory_load8_le(mem, i)))); +``` + +(Thank you to Nick for these examples) + +Similarly `strlen()` works in this form, + +```bpl +procedure strlen(); + modifies R0, Gamma_R0; + ensures Gamma_R0 == true; + ensures (forall i: bv64 :: (bvule64(old(R0), i)) && (bvult64(i, bvadd64(old(R0), R0))) ==> mem[i] != 0bv8); + ensures (memory_load8_le(mem, bvadd64(old(R0), R0)) == 0bv8); + ensures (bvule64(old(R0), bvadd64(old(R0), R0))); +``` + +But **does not** work when we do the address calculation in the load. + +```bpl +procedure strlen(); + // does not work + modifies R0, Gamma_R0; + ensures Gamma_R0 == true; + ensures (forall i: bv64 :: (bvule64(0bv64, i)) && (bvult64(i, R0)) ==> mem[bvadd64(old(R0), i)] != 0bv8); + ensures (memory_load8_le(mem, bvadd64(old(R0), R0)) == 0bv8); + ensures (bvule64(old(R0), bvadd64(old(R0), R0))); +``` + +### Dafny inferred triggers + +Dafny can also infer triggers, which may be worth comparing. To get Dafny to emit its +generated boogie code run it with `dafny -print:a.bpl b.dfy`. + +- https://leino.science/papers/krml253.pdf +- https://github.com/dafny-lang/dafny/wiki/FAQ#how-does-dafny-handle-quantifiers-ive-heard-about-triggers-what-are-those