add example with quantified specs

examples/simplified_http_parse_basic/example.c

@@ -0,0 +1,35 @@
+#include <stdlib.h>
+#include <string.h>
+#include <stdio.h>
+
+#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
+
+}
+

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
+
+

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
+```
+
+

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