trying to produce "interesting examples"...

LiveVerif/src/LiveVerifExamples/bsearch.v

@@ -0,0 +1,75 @@
+(* -*- eval: (load-file "../LiveVerif/live_verif_setup.el"); -*- *)
+Require Import LiveVerif.LiveVerifLib.
+
+Load LiveVerif.
+
+Definition sorted(vs: list word): Prop :=
+  forall i j, 0 <= i -> i < j -> j < len vs -> \[vs[i]] <= \[vs[j]].
+
+#[export] Instance spec_of_bsearch: fnspec :=                                   .**/
+
+uintptr_t bsearch(uintptr_t a, uintptr_t n, uintptr_t v, uintptr_t idxp) /**#
+  ghost_args := vs (R: mem -> Prop);
+  requires t m := <{ * array uintptr \[n] vs a
+                     * uintptr ? idxp
+                     * R }> m /\
+                  sorted vs;
+  ensures t' m' r := t' = t /\ exists i,
+      ((r = /[1] /\ vs[\[i]] = v) \/ (r = /[0] /\ ~ List.In v vs)) /\
+       <{ * array uintptr \[n] vs a
+          * uintptr i idxp
+          * R }> m' #**/                                                   /**.
+Derive bsearch SuchThat (fun_correct! bsearch) As bsearch_ok.                   .**/
+{                                                                          /**.
+  unfold anyval in *. repeat heapletwise_step. rename v0 into i0.               .**/
+  if (n == 0) /* split */ {                                                /**. .**/
+    return 0;                                                              /**. .**/
+  }                                                                        /**.
+    right. step. step. destruct vs. 2: discriminate. intro C. inversion C.      .**/
+  else {                                                                   /**. .**/
+  uintptr_t lo = 0;                                                        /**. .**/
+  uintptr_t hi = n - 1;                                                    /**. .**/
+  uintptr_t ret = 0;                                                       /**.
+
+  prove (0 <= \[lo] /\ \[lo] <= \[hi] /\ \[hi] < \[n]).
+  delete #(ret = ??).
+  delete #(lo = ??).
+  delete #(hi = ??).
+  delete #(n <> /[0]).
+  loop invariant above lo.
+  (* TODO why are these moves needed if we don't want old memory predicates
+     to be visible in loop body? *)
+  move H0 after Scope4. move H2 after H0. move H3 after H2. move D after H2.
+
+                                                                                .**/
+  while (lo < hi) /* decreases (hi^-lo) */ {                               /**. .**/
+    uintptr_t mid = (lo + hi)/2;                                           /**. .**/
+    uintptr_t midv = load(a + mid * sizeof(uintptr_t));                    /**.
+
+    assert (subrange (a ^+ mid ^* /[4]) 4 a (\[n] * 4)). {
+      clear Error.
+      unfold subrange.
+      subst mid.
+      bottom_up_simpl_in_goal.
+      (* if we use indices, there's actually no risk for overflow because they
+         are at least 4x smaller than 2^32 *)
+(*
+    if (mid == v) /* split */ {                                            /**. .**/
+      ret = 1;                                                             /**. .**/
+    }                                                                      /**. .**/
+
+
+else {                                                               /**. .**/
+      if (v < mid) /* split */ {                                           /**. .**/
+        hi = mid;                                                          /**. .**/
+      } else {                                                             /**. .**/
+        lo = mid;                                                          /**. .**/
+      }                                                                    /**. .**/
+    }                                                                      /**. .**/
+  }                                                                        /**. .**/
+
+  return ret;
+*)
+Abort.
+
+End LiveVerif. Comments .**/ //.

LiveVerif/src/LiveVerifExamples/mini_stagefright.v

@@ -0,0 +1,91 @@
+(* -*- eval: (load-file "../LiveVerif/live_verif_setup.el"); -*- *)
+Require Import LiveVerif.LiveVerifLib.
+
+Load LiveVerif.
+
+(* src consists of length-type-value chunks:
+struct TLV { uint32_t length; uint32_t typ; uint32_t data[length]; }; *)
+
+#[export] Instance spec_of_parse_chunk_of_type_or_skip: fnspec :=                .**/
+
+uintptr_t parse_chunk_of_type_or_skip(
+  uintptr_t src, uintptr_t pSrcOfs, uintptr_t srcLen,
+  uintptr_t expected_typ,
+  uintptr_t dst, uintptr_t pDstOfs, uintptr_t dstLen
+) /**#
+  ghost_args := srcOfs dstOfs srcData dstData dstUninit (R: mem -> Prop);
+  requires t m :=
+    <{ * uintptr srcOfs pSrcOfs
+       * uintptr dstOfs pDstOfs
+       * array (uint 32) \[srcLen] srcData src
+       * array (uint 32) \[dstLen] (dstData ++ dstUninit) dst
+       * R }> m /\
+    \[srcOfs] + 2 <= \[srcLen] /\
+    len dstData = \[dstOfs];
+  ensures t' m' r := t' = t /\ exists newSrcOfs newDstOfs newData,
+    <{ * uintptr newSrcOfs pSrcOfs
+       * uintptr newDstOfs pDstOfs
+       * array (uint 32) \[srcLen] srcData src
+       * array (uint 32) \[dstLen] (dstData ++ newData ++ dstUninit[len newData :]) dst
+       * R }> m' /\
+    \[newSrcOfs] = \[srcOfs] + len newData /\
+    \[newDstOfs] = \[dstOfs] + len newData /\
+    ((r = /[0] /\ newData = nil) \/
+     (r = /[1] /\ newData = srcData[\[srcOfs]+2:][:len newData])) #**/        /**.
+Derive parse_chunk_of_type_or_skip SuchThat (fun_correct! parse_chunk_of_type_or_skip)
+  As parse_chunk_of_type_or_skip_ok.                                            .**/
+{                                                                          /**. .**/
+  uintptr_t srcOfs = deref(pSrcOfs);                                       /**. .**/
+  uintptr_t dstOfs = deref(pDstOfs);                                       /**. .**/
+  uintptr_t actual_typ = deref32(src + srcOfs * 4 + 4);                    /**. .**/
+  if (actual_typ == expected_typ) /* split */ {                            /**. .**/
+    uintptr_t n = deref32(src + srcOfs * 4);                               /**. .**/
+    if (srcOfs + n <= srcLen && dstOfs + n <= dstLen) /* split */ {        /**. .**/
+
+(* use bytes and more-parsed src? *)
+(* memcpy or uint32arrayCpy? *)
+
+    }                                                                      /**.
+
+Abort.
+
+
+(* TODO would be more interesting with byte arrays: *)
+
+#[export] Instance spec_of_parse_chunk_of_type_bytearr: fnspec :=                .**/
+
+uintptr_t parse_chunk_of_type_bytearr(
+  uintptr_t src, uintptr_t pSrcOfs, uintptr_t srcLen,
+  uintptr_t expected_typ,
+  uintptr_t dst, uintptr_t pDstOfs, uintptr_t dstLen
+) /**#
+  ghost_args := srcOfs dstOfs srcData dstData dstUninit (R: mem -> Prop);
+  requires t m :=
+    <{ * uintptr srcOfs pSrcOfs
+       * uintptr dstOfs pDstOfs
+       * array (uint 8) \[srcLen] srcData src
+       * array (uint 8) \[dstLen] (dstData ++ dstUninit) dst
+       * R }> m /\
+    \[srcOfs] + 8 <= \[srcLen] /\
+    len dstData = \[dstOfs];
+  ensures t' m' r := t' = t /\ exists newSrcOfs newDstOfs newData,
+    <{ * uintptr newSrcOfs pSrcOfs
+       * uintptr newDstOfs pDstOfs
+       * array (uint 8) \[srcLen] srcData src
+       * array (uint 8) \[dstLen] (dstData ++ newData ++ dstUninit[len newData :]) dst
+       * R }> m' /\
+    \[newSrcOfs] = \[srcOfs] + len newData /\
+    \[newDstOfs] = \[dstOfs] + len newData /\
+    ((r = /[0] /\ newData = nil) \/
+     (r = /[1] /\ newData = srcData[\[srcOfs]+8:][:len newData])) #**/        /**.
+Derive parse_chunk_of_type_bytearr SuchThat (fun_correct! parse_chunk_of_type_bytearr)
+  As parse_chunk_of_type_bytearr_ok.                                            .**/
+{                                                                          /**. .**/
+  uintptr_t srcOfs = load(pSrcOfs);                                        /**. .**/
+  uintptr_t dstOfs = load(pDstOfs);                                        /**. .**/
+  uintptr_t actual_typ = load32(src + srcOfs + 4);                         /**.
+
+  2: {
+Abort.
+
+End LiveVerif. Comments .**/ //.