diff --git a/LiveVerif/src/LiveVerifExamples/bsearch.v b/LiveVerif/src/LiveVerifExamples/bsearch.v new file mode 100644 index 000000000..21e988592 --- /dev/null +++ b/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 .**/ //. diff --git a/LiveVerif/src/LiveVerifExamples/mini_stagefright.v b/LiveVerif/src/LiveVerifExamples/mini_stagefright.v new file mode 100644 index 000000000..7e632bf24 --- /dev/null +++ b/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 .**/ //.