diff --git a/docs/getting-started/case-studies/strings.md b/docs/getting-started/case-studies/strings.md new file mode 100644 index 00000000..1d90e037 --- /dev/null +++ b/docs/getting-started/case-studies/strings.md @@ -0,0 +1,125 @@ +# Null-terminated strings + +A null-terminated string is an array of characters where the 0 character, +`'\0'`, signals the end of the string. (Note that there is no "null" in the +usual pointer sense, just the byte consisting of all zeros. Note also that this +is distinct from `'0'`.) + +To ensure safety for operations like in-place concatenation, we need to keep +track of not just the string up to `'\0'`, but the entire buffer allocated for +the string. This means our logical representation of strings looks like this: + +```c title="exercises/string/cn_types.h" +--8<-- +exercises/string/cn_types.h +--8<-- +``` + +In order to facilitate proofs, we define logical string buffers inductively. A +string buffer represents either the empty string, in which case we have a +64-bit integer indicating how many unused bytes the buffer has (counting the +null byte as unused), or a nonempty string, in which case we have a (non-null) +character followed by another string buffer. + +Due to CN restrictions on top-level `if`, we have two mutually-recursive +predicates. `String_Buf_At(p, buf_len)` asserts that at the input pointer `p`, +there is a buffer of total size `buf_len` (including the string, the `'\0'` +terminator, and any extra empty bytes), represented by the logical string that +`String_Buf_At` returns. (Note that `buf_len` must be at least 1, to have space +for at least `'\0'`.) `String_Buf_At` reads the first character and, via +`String_Buf_Aux`, checks if it is `'\0'`. If so, it blocks the rest of the +bytes, using `W` instead of `RW` because these bytes have no meaningful data +for us to read yet. If the first byte is not `'\0'`, we recursively call +`String_Buf_At` on the rest of the buffer. + +`spec_funs.h` contains CN functions on the logical representation of string +buffers. Specifically: +* `buf_len` gets the length of the entire allocated buffer for the string +* `string_length` gets the length of the conceptual string, i.e., all the +characters before `'\0'` +* `empty_buf_len` gets the number of bytes after the conceptual string, i.e., +the number of bytes in the buffer starting with the first `'\0'` +* `string_buf_concat` performs in-place concatenation of two strings. It +assumes the destination string has sufficient space +* `string_buf_nth` returns the (0-indexed) nth character of a string, +defaulting to `'\0'` if n is greater than or equal to the length of the +conceptual string +* `is_nil_string_buf` checks if a string buffer represents the empty string +* `string_equal` checks if two string buffers contain equal conceptual strings, +i.e., the buffers may have different total size, but they should contain the +same characters up to and including the first `'\0'` + +`string_buf.c` contains specifications for string functions in the C standard +library. The functions we would like to have available are `malloc`, `free`, +`strlen`, `strcpy`, `strcmp`, and `strcat`. However, to work with our +`String_Buf` type and ensure memory safety, we add additional arguments to +keep track of the lengths of all of the strings' buffers. + +`trusted.h` and `lemmas.c` both contain lemmas about the functions in +`spec_funs.h` and `string_buf.c`. The lemmas in `trusted.h` are trusted, +i.e., not proven in CN, while the ones in `lemmas.c` are proven in CN. +These will be useful for the example function in `example.c`. + +`example.c` contains a toy function designed to use every function in +`string_buf.c` together. It takes a pointer to an input string, the length of +the buffer containing that string, the number of bytes we will allocate for +a second string, and two characters. To make the later copies and comparisons +interesting, we require the input string to be nonempty and the characters +distinct and non-null. We will also later concatenate the strings, so we want +enough space in the buffer we will allocate to fit the input string twice (with +room for a terminating `'\0'` also). We specify this with the constraint +`string_len(sIn) + string_len(sIn) < n2`, and we require the input string to be +sufficiently small that this statement is meaningful, i.e., the `+` is not +wrapping around. + +In the body of our function, we first allocate the second string using +`malloc_str`. Like `malloc`, this does not initialize the bytes in the string to +any specific value. + +Next, we copy the input string into the second string's buffer. Thanks to our +preconditions, we know we have enough space for this. + +After that, we compare the two strings. Because we just copied the first into +the second, the result should be 0; we confirm with `assert` that it is. + +We would now like to edit the first character of each string. We have a safe +wrapper for array edits, `edit_array_at`. This ensures not only that we do +not write beyond the bounds of our array, but also that our edit is meaningful: +we must edit a character within the current defined string, not the empty +buffer space. (If we wanted to extend the string, we would use +`string_buf_cat`.) However, in order to do this, we need to switch from our +`String_Buf` representation of strings to an array representation of strings. + +Luckily, we have a lemma for this, `string_buf_to_array`. When we go to edit +the first array, however, we will need to know that the index at which we are +writing is less than the string length. We are writing at index `0`, so the +lemma that tells us this is `nonempty_string_len`, which asserts that nonempty +strings have positive length. This lemma is stated in terms of our +`String_Buf_At` predicate, so we need to apply it before applying +`string_buf_to_array`. + +This allows us to edit the array, but when we go to convert it back to a +`String_Buf`, we will need additional information. In order for an array to +be a valid string buffer, it must start with some number (potentially 0) of +non-null characters, in this case `s1Len - 1` of them, followed by the null +character, followed by 0 or more write-only bytes. We have a lemma stating +that the first `s1Len - 1` characters of the array are non-null, +`nonzero_up_to_len`, but again, it is stated in terms of `String_Buf` and +`String_Buf_At`, so we must apply it before `string_buf_to_array`. + +We now wish to edit the first character of the second string. Again, we will +need `nonzero_up_to_len` for the conversion back to a `String_Buf`. Before +that, though, how do we know that the length of this second string is positive? +We previously compared it to the first string and got `0`, so we know the two +strings were equal at that point, and we showed that the first string has +nonzero length. That means we can apply `string_equal_impl_equal_len` before +editing the first string to assert that the second string has nonzero length +as well. + +Next, we concatenate the two strings. We know from the lemmas we just applied +and the precondition that the sum of the two strings' lengths is less than +the number of bytes in the second string's buffer, so the in-place +concatenation will not write beyond the end of the buffer. + +Finally, we free the two strings. The only precondition for this is ownership, +so there is nothing to prove. \ No newline at end of file diff --git a/src/exercises/string/cn_types.h b/src/exercises/string/cn_types.h new file mode 100644 index 00000000..ba386b4f --- /dev/null +++ b/src/exercises/string/cn_types.h @@ -0,0 +1,42 @@ +/* +CN string buffer type and predicate. +*/ + +/*@ +// null-terminated strings with (potentially) extra buffer space + +datatype String_Buf { + String_Buf_Nil { + u64 empty_buf // empty buffer space remaining, including null char + }, + String_Buf_Cons { + u8 head, // should not be 0u8 + datatype String_Buf tail + } +} + +// p: pointer to string buffer +// buf_len: length of *entire* buffer, including string +predicate (datatype String_Buf) String_Buf_At(pointer p, u64 buf_len) { + take h = RW(p); + take s = String_Buf_Aux(p, buf_len, h); + assert (buf_len >= 1u64); // there must be space for at least the null char + return s; +} + +// p: pointer to h +// buf_len: length of buffer *including* h +// h: first character of string pointed to by p +predicate (datatype String_Buf) String_Buf_Aux(pointer p, u64 buf_len, u8 h) { + if (h == 0u8) { + // everything after h can be write-only + take rem = each (u64 i; 0u64 < i && i < buf_len) { + W( array_shift(p, i)) }; + return String_Buf_Nil { empty_buf : buf_len }; + } else { + take tl_buf = String_Buf_At(array_shift(p, 1u64), buf_len - 1u64); + return String_Buf_Cons {head : h, tail : tl_buf}; + } +} + +@*/ diff --git a/src/exercises/string/example.c b/src/exercises/string/example.c new file mode 100644 index 00000000..d9208632 --- /dev/null +++ b/src/exercises/string/example.c @@ -0,0 +1,51 @@ +#include "util.c" + +/* +Example using string library functions. +*/ + +void simple_ex(char *s1, size_t n1, size_t n2, char c1, char c2) +/*@ + requires + take sIn = String_Buf_At(s1, n1); + !is_nil_string_buf(sIn); + (u128) string_len(sIn) + (u128) string_len(sIn) < (u128) n2; // so it fits in allocated buffer twice + c1 != c2; + c1 != 0u8; + c2 != 0u8; + ensures + true; +@*/ +{ + // allocate second string + char *s2 = malloc_str(n2); + + // copy s1 into s2 + s2 = str_buf_cpy(s2, s1, n2, n1); + + // compare s1 and s2 + int j = str_buf_cmp(s1, s2, n1, n2); + /*@ assert (j == 0i32); @*/ + + // edit s1 + size_t s1Len = str_buf_len(s1, n1); + size_t s2Len = str_buf_len(s2, n2); + nonzero_up_to_len(s1, n1); + nonempty_string_len(s1, n1); + string_equal_impl_equal_len(s1, n1, s2, n2); + /*@ apply string_buf_to_array(s1, n1, s1Len); @*/ + edit_array_at(s1, s1Len, 0, c1); + /*@ apply array_to_string_buf(s1, n1, s1Len); @*/ + + // edit s2 differently + s2Len = str_buf_len(s2, n2); + nonzero_up_to_len(s2, n2); + /*@ apply string_buf_to_array(s2, n2, s2Len); @*/ + edit_array_at(s2, s2Len, 0, c2); + /*@ apply array_to_string_buf(s2, n2, s2Len); @*/ + + s2 = str_buf_cat(s2, s1, n2, n1); + + free_str(s1, n1); + free_str(s2, n2); +} \ No newline at end of file diff --git a/src/exercises/string/lemmas.c b/src/exercises/string/lemmas.c new file mode 100644 index 00000000..1d20d992 --- /dev/null +++ b/src/exercises/string/lemmas.c @@ -0,0 +1,204 @@ +#include +#include "trusted.h" + +/* +String lemmas proven in CN. +*/ + +// string length is less than buffer size +void len_lt_buf_size(char *s, size_t n) +/*@ +requires + take sIn = String_Buf_At(s, n); +ensures + take sOut = String_Buf_At(s, n); + sIn == sOut; + string_len(sOut) < n; +@*/ +{ + char c = s[0]; + + if (c == '\0') + { + /*@ unfold string_len(sIn); @*/ + } + else + { + len_lt_buf_size(&s[1], n - (size_t)1); + /*@ unfold string_len(sIn);@*/ + } +} + +// nonempty string's length is 1 + its tail's length +void one_plus_string_len(char *s, size_t n) +/*@ +requires + n > 1u64; + take hIn = RW(s); + hIn != 0u8; + take tlIn = String_Buf_At(array_shift(s, 1u64), n - 1u64); +ensures + take hOut = RW(s); + hOut != 0u8; + take tlOut = String_Buf_At(array_shift(s, 1u64), n - 1u64); + hIn == hOut; + tlIn == tlOut; + string_len(String_Buf_Cons { head : hIn, tail : tlIn }) == 1u64 + string_len(tlIn); +@*/ +{ + /*@ split_case (hIn == 0u8); @*/ + /*@ unfold string_len(String_Buf_Cons { head : hIn, tail : tlIn }); @*/ +} + +// string length is less than max u64 +void string_len_not_max(char *s, size_t n) +/*@ +requires + take sIn = String_Buf_At(s, n); +ensures + take sOut = String_Buf_At(s, n); + sIn == sOut; + string_len(sIn) < MAXu64(); +@*/ +{ + len_lt_buf_size(s, n); +} + +// adding one to less than max u64 does not wrap around +void plus_one_gt_zero(size_t n) +/*@ +requires + n < MAXu64(); +ensures + 1u64 + n > 0u64; +@*/ +{ +} + +// length of nonempty string is > 0 +void nonempty_string_len(char *s, size_t n) +/*@ +requires + take sIn = String_Buf_At(s, n); + !is_nil_string_buf(sIn); +ensures + take sOut = String_Buf_At(s, n); + sIn == sOut; + string_len(sIn) > 0u64; +@*/ +{ + char c = s[0]; + /*@ split_case (c == 0u8); @*/ + string_len_not_max(&s[1], n - (size_t)1); + len_lt_buf_size(&s[1], n - (size_t)1); + plus_one_gt_zero(str_buf_len(&s[1], n - (size_t)1)); + one_plus_string_len(s, n); +} + +// equal strings have the same length +void string_equal_impl_equal_len(char *s1, size_t n1, char *s2, size_t n2) +/*@ +requires + take s1In = String_Buf_At(s1, n1); + take s2In = String_Buf_At(s2, n2); + string_equal(s1In, s2In); +ensures + take s1Out = String_Buf_At(s1, n1); + take s2Out = String_Buf_At(s2, n2); + s1In == s1Out; + s2In == s2Out; + string_len(s1In) == string_len(s2In); +@*/ +{ + char c1 = s1[0]; + char c2 = s2[0]; + if (c1 == '\0') + { + /*@ unfold string_equal(s1In, s2In); @*/ + /*@ unfold string_len(s1In); @*/ + /*@ unfold string_len(s2In); @*/ + } + else + { + /*@ unfold string_equal(s1In, s2In); @*/ + /*@ unfold string_len(s1In); @*/ + /*@ unfold string_len(s2In); @*/ + /*@ split_case (c2 == 0u8); @*/ + string_equal_impl_equal_len(&s1[1], n1 - (size_t)1, &s2[1], n2 - (size_t)1); + } +} + +// all elements of a string are nonzero up to (excluding) string_len +void nonzero_up_to_len(char *s, size_t n) +/*@ +requires + take sIn = String_Buf_At(s, n); +ensures + take sOut = String_Buf_At(s, n); + sIn == sOut; + each (u64 i; i < string_len(sIn)) { + string_buf_nth(sIn, i) != 0u8 }; +@*/ +{ + char c = s[0]; + if (c == '\0') + { + /*@ unfold string_len(sIn); @*/ + } + else + { + /*@ unfold string_buf_nth(sIn, 0u64); @*/ + nonzero_up_to_len(&s[1], n - (size_t)1); + /*@ apply nonzero_up_to_len_step(s, n); @*/ + } +} + +void update_empty_buf_preserves_string(char *s, size_t n, size_t new_empty_buf) +/*@ +requires + take sIn = String_Buf_At(s, n); +ensures + take sOut = String_Buf_At(s, n); + sIn == sOut; + string_equal(sIn, update_empty_buf(sIn, new_empty_buf)); +@*/ +{ + char c = s[0]; + if (c == '\0') + { + /*@ unfold update_empty_buf(sIn, new_empty_buf); @*/ + /*@ unfold string_equal(sIn, update_empty_buf(sIn, new_empty_buf)); @*/ + } + else + { + update_empty_buf_preserves_string(&s[1], n - (size_t)1, new_empty_buf); + /*@ unfold update_empty_buf(sIn, new_empty_buf); @*/ + /*@ unfold string_equal(sIn, update_empty_buf(sIn, new_empty_buf)); @*/ + } +} + +void update_empty_buf_preserves_len(char *s, size_t n, size_t new_empty_buf) +/*@ +requires + take sIn = String_Buf_At(s, n); +ensures + take sOut = String_Buf_At(s, n); + sIn == sOut; + string_len(sIn) == string_len(update_empty_buf(sIn, new_empty_buf)); +@*/ +{ + char c = s[0]; + if (c == '\0') + { + /*@ unfold update_empty_buf(sIn, new_empty_buf); @*/ + /*@ unfold string_len(update_empty_buf(sIn, new_empty_buf)); @*/ + /*@ unfold string_len(sIn); @*/ + } + else + { + update_empty_buf_preserves_len(&s[1], n - (size_t)1, new_empty_buf); + /*@ unfold update_empty_buf(sIn, new_empty_buf); @*/ + /*@ unfold string_len(update_empty_buf(sIn, new_empty_buf)); @*/ + /*@ unfold string_len(sIn); @*/ + } +} \ No newline at end of file diff --git a/src/exercises/string/more_lemmas.broken.c b/src/exercises/string/more_lemmas.broken.c new file mode 100644 index 00000000..7fbdf971 --- /dev/null +++ b/src/exercises/string/more_lemmas.broken.c @@ -0,0 +1,185 @@ +#include +#include "lemmas.c" + +/* +In progress CN versions of trusted lemmas. +*/ + +void array_to_string_buf_c(char *s, size_t string_len, size_t n) +/*@ +requires + take sArray = each(u64 i; i < string_len) { + RW( array_shift(s, i) ) }; + take sRem = each(u64 i; string_len < i && i < n) { + W( array_shift(s, i)) }; + n >= 1u64; + string_len < n; + take sNull = RW(array_shift(s, string_len)); + sNull == 0u8; + // we need some "fix arbitrary i" tactic for the below + each (u64 i; i < string_len) { + sArray[i] != 0u8 + }; +ensures + take sBuf = String_Buf_At(s, n); + string_len == string_len(sBuf); + each (u64 i; i < string_len(sBuf)) { + string_buf_nth(sBuf, i) == sArray[i] + }; +@*/ +{ + /*@ split_case (string_len == 0u64); @*/ + /*@ focus RW, 0u64; @*/ + char c = s[0]; + /*@split_case (c == 0u8); @*/ + if (string_len == (size_t)0) + { + if (c == '\0') + { + /*@ unfold string_len(String_Buf_Nil { empty_buf : n }); @*/ + } + else + { + // impossible + /*@ instantiate 0u64; @*/ + /*@ assert (false); @*/ + } + } + else + { + /*@ apply array_shift_one_r(s, string_len - 1u64, n - 1u64); @*/ + array_to_string_buf_c(&s[1], string_len - (size_t)1, n - (size_t)1); + one_plus_string_len(s, n); + } +} + +void string_buf_to_array_c(char *s, size_t n) +/*@ +requires + take sBuf = String_Buf_At(s, n); +ensures + string_len(sBuf) < n; + n >= 1u64; + take sArray = each (u64 i; i < string_len(sBuf)) { + RW( array_shift(s, i) ) }; + take sRem = each (u64 i; string_len(sBuf) < i && i < n) { + W( array_shift(s, i) ) }; + take sNull = RW(array_shift(s, string_len(sBuf))); + sNull == 0u8; + // we need some "fix arbitrary i" tactic for the below + each (u64 i; i < string_len(sBuf)) { + string_buf_nth(sBuf, i) == sArray[i] + }; +@*/ +{ + char c = s[0]; + if (c == '\0') + { + /*@ unfold string_len(sBuf); @*/ + } + else + { + char c1 = s[1]; + string_buf_to_array_c(&s[1], n - (size_t)1); + /*@ unfold string_len(sBuf); @*/ + /*@ apply array_owned_shift_one_l(s, string_len(sBuf) - 1u64); @*/ + /*@ apply array_blocked_shift_one_l(s, string_len(sBuf) - 1u64, n - 1u64); @*/ + } +} + +void nonzero_up_to_len_step(char *s, size_t n) +/*@ +requires + n > 1u64; + take sHead = RW(s); + take sTail = String_Buf_At(array_shift(s, 1u64), n - 1u64); + each (u64 i; i < string_len(sTail)) { + string_buf_nth(sTail, i) != 0u8 }; +ensures + take sOut = String_Buf_At(s, n); + sOut == String_Buf_Cons { head : sHead, tail : sTail }; + each (u64 i; i < string_len(sOut)) { + string_buf_nth(sOut, i) != 0u8 }; +@*/ +{ +} + +/* +In progress potentially-useful functions. +*/ + +// edit any character in the initial string to a non-null character +void edit_at(char *s, size_t buf_len, size_t index, char c) +/*@ +requires + take sIn = String_Buf_At(s, buf_len); + index < string_len(sIn); + c != 0u8; +ensures + take sOut = String_Buf_At(s, buf_len); + // we need some "fix arbitrary i" tactic for the below + each (u64 i; i < string_len(sOut)) { + i == index + ? string_buf_nth(sOut, i) == c + : string_buf_nth(sOut, i) == string_buf_nth(sIn, i) + }; +@*/ +{ + size_t sLen = str_buf_len(s, buf_len); + /*@ apply string_buf_to_array(s, buf_len, string_len(sIn)); @*/ + edit_array_at(s, sLen, index, c); + /*@ instantiate index; @*/ + /*@ apply array_to_string_buf(s, buf_len, sLen); @*/ +} + +// allocate a string of size n and set the first byte to '\0' +char *init_string(size_t n) +/*@ +requires + 1u64 <= n; // 1 byte is required for null termination +ensures + take sOut = String_Buf_At(return, n); + sOut == String_Buf_Nil { empty_buf : n }; +@*/ +{ + char *s = malloc_str(n); + /*@ apply string_buf_to@*/ + s[0] = '\0'; + return s; +} + +void concat_len(char *dest, char *src, size_t dest_size, size_t src_size) +/*@ +requires + take srcIn = String_Buf_At(src, src_size); + take destIn = String_Buf_At(dest, dest_size); + (u128) string_len(srcIn) + (u128) string_len(destIn) < (u128) dest_size; +ensures + take srcOut = String_Buf_At(src, src_size); + take destOut = String_Buf_At(dest, dest_size); + srcIn == srcOut; + destIn == destOut; + string_len(string_buf_concat(destIn, srcIn)) == string_len(srcIn) + string_len(destIn); +@*/ +{ + char c = dest[0]; + if (c == '\0') + { + update_empty_buf_preserves_len(src, src_size, dest_size - str_buf_len(src, src_size)); + /*@ unfold string_len(srcIn); @*/ + /*@ unfold string_len(destIn); @*/ + /*@ unfold string_buf_concat(destIn, srcIn); @*/ + /*@ unfold string_len(string_buf_concat(destIn, srcIn)); @*/ + } + else + { + /*@ split_case (c == 0u8); @*/ + /*@ unfold string_len(destIn); @*/ + /*@ assert (string_len(destIn) > 0u64); @*/ + one_plus_string_len(dest, dest_size); + concat_len(&dest[1], src, dest_size - (size_t)1, src_size); + /*@ unfold string_len(srcIn); @*/ + /*@ unfold string_buf_concat(destIn, srcIn); @*/ + /*@ unfold string_len(string_buf_concat(destIn, srcIn)); @*/ + } +} \ No newline at end of file diff --git a/src/exercises/string/spec_funs.h b/src/exercises/string/spec_funs.h new file mode 100644 index 00000000..462e5494 --- /dev/null +++ b/src/exercises/string/spec_funs.h @@ -0,0 +1,95 @@ +#include "cn_types.h" + +/* +Logical string functions for use in specifications. +*/ + +/*@ +// the length of the *entire* buffer, including the string +function [rec] (u64) buf_len(String_Buf s) { + match s { + String_Buf_Nil { empty_buf : n } => { n } + String_Buf_Cons { head : h, tail : tl } => { 1u64 + buf_len(tl) } + } +} + +// the length of just the string +function [rec] (u64) string_len(String_Buf s) { + match s { + String_Buf_Nil { empty_buf : n } => { 0u64 } + String_Buf_Cons { head : h , tail : tl } => { 1u64 + string_len(tl) } + } +} + +// the length of the buffer space *after* the string, including the null +function [rec] (u64) empty_buf_len(String_Buf s) { + match s { + String_Buf_Nil { empty_buf : n } => { n } + String_Buf_Cons { head : h, tail : tl } => { empty_buf_len(tl) } + } +} + +// updates the number of empty bytes +function [rec] (datatype String_Buf) update_empty_buf(String_Buf s, u64 new_empty_buf) +{ + match s { + String_Buf_Nil { empty_buf : nDest } => { String_Buf_Nil { empty_buf : new_empty_buf } } + String_Buf_Cons { head : h, tail : tl } => { + String_Buf_Cons { head : h, tail : update_empty_buf(tl, new_empty_buf) } + } + } +} + +// in-place string concat +// assumes destination buffer has enough space for source string +function [rec] (datatype String_Buf) string_buf_concat(String_Buf dest, String_Buf src) { + match dest { + String_Buf_Nil { empty_buf : nDest } => { + // string_len(src) should be strictly less than nDest + update_empty_buf(src, nDest - string_len(src)) + } + String_Buf_Cons { head : h , tail : tl } => { + String_Buf_Cons { head : h, tail : string_buf_concat(tl, src) } + } + } +} + +// defaults to \0 +function [rec] (u8) string_buf_nth(String_Buf s, u64 n) { + match s { + String_Buf_Nil { empty_buf : nS } => { 0u8 } + String_Buf_Cons { head : h , tail : tl } => { + n == 0u64 ? h : string_buf_nth(tl, n - 1u64) + } + } +} + +// checks if input buffer represents the empty string +function (boolean) is_nil_string_buf(String_Buf s) { + match s { + String_Buf_Nil {empty_buf : n } => { true } + String_Buf_Cons { head : h , tail : tl } => { false } + } +} + +// compares strings contained in two buffers; does not compare buffer size +function [rec] (boolean) string_equal(String_Buf s1, String_Buf s2) { + match s1 { + String_Buf_Nil { empty_buf : n1 } => { + match s2 { + String_Buf_Nil { empty_buf : n2 } => { true } + String_Buf_Cons { head : h2, tail : tl2 } => { false } + } + } + String_Buf_Cons { head : h1, tail : tl1 } => { + match s2 { + String_Buf_Nil { empty_buf : n2 } => { false } + String_Buf_Cons { head : h2, tail : tl2 } => { + h1 == h2 && string_equal(tl1, tl2) + } + } + } + } +} + +@*/ \ No newline at end of file diff --git a/src/exercises/string/string_buf.c b/src/exercises/string/string_buf.c new file mode 100644 index 00000000..47ca9e2c --- /dev/null +++ b/src/exercises/string/string_buf.c @@ -0,0 +1,78 @@ +#include +#include "spec_funs.h" + +/* +Specifications for external standard library functions for null-terminated strings. +*/ + +extern char *malloc_str(size_t n); +/*@ spec malloc_str(u64 n); + requires + 1u64 <= n; // 1 byte is required for null termination + ensures + take s = String_Buf_At(return, n); +@*/ + +extern void free_str(char *p, size_t n); +/*@ spec free_str(pointer p, u64 n); + requires + take s = String_Buf_At(p, n); + ensures + true; +@*/ + +// buffer version of strlen +extern size_t str_buf_len(const char *s, size_t n); +/*@ spec str_buf_len(pointer s, u64 n); + requires + take sIn = String_Buf_At(s, n); + ensures + take sOut = String_Buf_At(s, n); + sIn == sOut; + return == string_len(sIn); +@*/ + +// buffer version of strcpy +extern char *str_buf_cpy(char *dest, const char *src, size_t dest_size, size_t src_size); +/*@ spec str_buf_cpy(pointer dest, pointer src, u64 dest_size, u64 src_size); + requires + take srcIn = String_Buf_At(src, src_size); + take destIn = String_Buf_At(dest, dest_size); + string_len(srcIn) < dest_size; // < to leave room for the null + ensures + take srcOut = String_Buf_At(src, src_size); + take destOut = String_Buf_At(dest, dest_size); + srcIn == srcOut; + string_equal(srcOut, destOut); + buf_len(destIn) == buf_len(destOut); + ptr_eq(return, dest); +@*/ + +// buffer version of strcmp; does not compare buffer size +extern int str_buf_cmp(char *s1, char *s2, size_t n1, size_t n2); +/*@ spec str_buf_cmp(pointer s1, pointer s2, u64 n1, u64 n2); + requires + take s1In = String_Buf_At(s1, n1); + take s2In = String_Buf_At(s2, n2); + ensures + take s1Out = String_Buf_At(s1, n1); + take s2Out = String_Buf_At(s2, n2); + s1In == s1Out; + s2In == s2Out; + (return == 0i32) == string_equal(s1In, s2In); +@*/ + +// buffer version of strcat +extern char *str_buf_cat(char *dest, const char *src, size_t dest_size, size_t src_size); +/*@ spec str_buf_cat(pointer dest, pointer src, u64 dest_size, u64 src_size); + requires + take srcIn = String_Buf_At(src, src_size); + take destIn = String_Buf_At(dest, dest_size); + (u128) string_len(srcIn) + (u128) string_len(destIn) < (u128) dest_size; // < to leave room for the null + ensures + take srcOut = String_Buf_At(src, src_size); + take destOut = String_Buf_At(dest, dest_size); + srcIn == srcOut; + destOut == string_buf_concat(destIn, srcIn); + ptr_eq(return, dest); +@*/ diff --git a/src/exercises/string/trusted.h b/src/exercises/string/trusted.h new file mode 100644 index 00000000..e9af0986 --- /dev/null +++ b/src/exercises/string/trusted.h @@ -0,0 +1,62 @@ +#include "string_buf.c" + +/* +Trusted string lemmas. +*/ + +/*@ +lemma array_to_string_buf(pointer s, u64 n, u64 string_len) +requires + take sArray = each(u64 i; i < string_len) { + RW( array_shift(s, i) ) }; + take sRem = each(u64 i; string_len < i && i < n) { + W( array_shift(s, i)) }; + n >= 1u64; + string_len < n; + take sNull = RW(array_shift(s, string_len)); + sNull == 0u8; + each (u64 i; i < string_len) { + sArray[i] != 0u8 + }; +ensures + take sBuf = String_Buf_At(s, n); + string_len == string_len(sBuf); + each (u64 i; i < string_len(sBuf)) { + string_buf_nth(sBuf, i) == sArray[i] + }; +@*/ + +/*@ +lemma string_buf_to_array(pointer s, u64 n, u64 string_len) //TODO +requires + take sBuf = String_Buf_At(s, n); + string_len(sBuf) == string_len; +ensures + string_len < n; + n >= 1u64; + take sArray = each (u64 i; i < string_len) { + RW( array_shift(s, i) ) }; + take sRem = each (u64 i; string_len < i && i < n) { + W( array_shift(s, i) ) }; + each (u64 i; i < string_len) { + string_buf_nth(sBuf, i) == sArray[i] + }; + take sNull = RW(array_shift(s, string_len)); + sNull == 0u8; +@*/ + +/*@ +lemma nonzero_up_to_len_step(pointer s, u64 n) + +requires + n > 1u64; + take sHead = RW(s); + take sTail = String_Buf_At(array_shift(s, 1u64), n - 1u64); + each (u64 i; i < string_len(sTail)) { + string_buf_nth(sTail, i) != 0u8 }; +ensures + take sOut = String_Buf_At(s, n); + sOut == String_Buf_Cons { head : sHead, tail : sTail }; + each (u64 i; i < string_len(sOut)) { + string_buf_nth(sOut, i) != 0u8 }; +@*/ \ No newline at end of file diff --git a/src/exercises/string/unused.c b/src/exercises/string/unused.c new file mode 100644 index 00000000..505b04c7 --- /dev/null +++ b/src/exercises/string/unused.c @@ -0,0 +1,181 @@ +#include +#include "string_buf.c" + +/* +Not used for current example, but potentially useful, including for `more_lemmas.broken.c`. +*/ + +/* CN lemmas */ + +// buffer size for a nonempty string is > 1 +void nonempty_buf_size(char *s, size_t n) +/*@ +requires + take sIn = String_Buf_At(s, n); + !is_nil_string_buf(sIn); +ensures + take sOut = String_Buf_At(s, n); + sIn == sOut; + n > 1u64; +@*/ +{ + char c = s[0]; + /*@ split_case (c == 0u8); @*/ +} + +// empty string has length 0 +void nil_string_len(char *s, size_t n) +/*@ +requires + take sIn = String_Buf_At(s, n); + is_nil_string_buf(sIn); +ensures + take sOut = String_Buf_At(s, n); + sIn == sOut; + string_len(sOut) == 0u64; +@*/ +{ + /*@ unfold string_len(sIn); @*/ +} + +void sum_string_parts(char *s, size_t n) +/*@ +requires + take sIn = String_Buf_At(s, n); +ensures + take sOut = String_Buf_At(s, n); + sIn == sOut; + string_len(sIn) + empty_buf_len(sIn) == buf_len(sIn); +@*/ +{ + char c = s[0]; + if (c == '\0') + { + /*@ unfold string_len(sIn); @*/ + /*@ unfold empty_buf_len(sIn); @*/ + /*@ unfold buf_len(sIn); @*/ + } + else + { + sum_string_parts(&s[1], n - (size_t)1); + /*@ unfold string_len(sIn); @*/ + /*@ unfold empty_buf_len(sIn); @*/ + /*@ unfold buf_len(sIn); @*/ + } +} + +/* Trusted lemmas */ + +/*@ +lemma array_owned_shift_one_r(pointer s, u64 tail_owned_len) //TODO + +requires + take all = each (u64 i; i < 1u64 + tail_owned_len) { + RW(array_shift(s, i))}; + tail_owned_len < MAXu64(); +ensures + take first = RW(s); + take rest = each (u64 i; i < tail_owned_len) { + RW(array_shift(array_shift(s, 1u64), i))}; +@*/ + +/*@ +lemma array_blocked_shift_one_r(pointer s, u64 tail_low, u64 tail_high) //TODO + +requires + take blockedIn = each (u64 i; tail_low + 1u64 < i && i < 1u64 + tail_high) { + W(array_shift(s, i))}; + tail_high < MAXu64(); +ensures + take blockedOut = each (u64 i; tail_low < i && i < tail_high) { + W(array_shift(array_shift(s, 1u64), i))}; +@*/ + +/*@ +lemma nonzero_shift_one_r(pointer s, size_t tail_len) + +requires + take sIn = each (u64 i; i < 1u64 + tail_len) { + RW(array_shift(s, i))}; + each (u64 i; i < 1u64 + tail_len) { + sIn[i] != 0u8 + }; +ensures + take sOut = each (u64 i; i < 1u64 + tail_len) { + RW(array_shift(s, i))}; + each (u64 i; i < tail_len) { + sOut[1u64 + i] != 0u8 + }; +@*/ + +/*@ +lemma array_owned_shift_one_l(pointer s, u64 tail_owned_len) + +requires + take first = RW(s); + take rest = each (u64 i; i < tail_owned_len) { + RW(array_shift(array_shift(s, 1u64), i))}; + tail_owned_len < MAXu64(); +ensures + take all = each (u64 i; i < 1u64 + tail_owned_len) { + RW(array_shift(s, i))}; +@*/ + +/*@ +lemma array_blocked_shift_one_l(pointer s, u64 tail_low, u64 tail_high) //TODO + +requires + take blockedIn = each (u64 i; tail_low < i && i < tail_high) { + W(array_shift(array_shift(s, 1u64), i))}; + tail_high < MAXu64(); +ensures + take blockedOut = each (u64 i; tail_low + 1u64 < i && i < 1u64 + tail_high) { + W(array_shift(s, i))}; +@*/ + +/*@ +lemma array_shift_one_r(pointer s, size_t tail_string_len, size_t tail_buf_len) + +requires + take ownedIn = each (u64 i; i < 1u64 + tail_string_len) { + RW(array_shift(s, i))}; + take blockedIn = each (u64 i; tail_string_len + 1u64 < i && i < 1u64 + tail_buf_len) { + W(array_shift(s, i))}; + tail_string_len < tail_buf_len; + tail_buf_len < MAXu64(); + take nullIn = RW(array_shift(s, 1u64 + tail_string_len)); + nullIn == 0u8; + each (u64 i; i < 1u64 + tail_string_len) { + ownedIn[i] != 0u8 + }; +ensures + take first = RW(s); + first != 0u8; + take ownedOut = each (u64 i; i < tail_string_len) { + RW(array_shift(array_shift(s, 1u64), i))}; + take blockedOut = each (u64 i; tail_string_len < i && i < tail_buf_len) { + W(array_shift(array_shift(s, 1u64), i))}; + take nullOut = RW(array_shift(array_shift(s, 1u64), tail_string_len)); + nullOut == 0u8; + each (u64 i; i < tail_string_len) { + ownedOut[i] != 0u8 + }; +@*/ + +/*@ +lemma convert_to_write_only(pointer s, size_t n, size_t string_len, size_t index) + +requires + n >= 1u64; + string_len < n; + index <= string_len; + take rwIn = each (u64 i; i <= string_len) { + RW(array_shift(s, i)) }; + take wIn = each (u64 i; string_len < i && i < n) { + W(array_shift(s, i)) }; +ensures + take rwOut = each (u64 i; i < index) { + RW(array_shift(s, i)) }; + take wOut = each (u64 i; index <= i && i < n) { + W(array_shift(s, i)) }; +@*/ \ No newline at end of file diff --git a/src/exercises/string/util.c b/src/exercises/string/util.c new file mode 100644 index 00000000..77cdc73b --- /dev/null +++ b/src/exercises/string/util.c @@ -0,0 +1,32 @@ +#include +#include "lemmas.c" + +/* +Library functions for null-terminated strings. +*/ + +// edit any character up to (not including) string_len +void edit_array_at(char *s, size_t string_len, size_t index, char c) +/*@ +requires + take sIn = each (u64 i; i < string_len) { + RW(array_shift(s, i)) + }; + take sNullIn = RW(array_shift(s, string_len)); + index < string_len; +ensures + take sOut = each (u64 i; i < string_len) { + RW(array_shift(s, i)) + }; + each (u64 i; i < string_len) { + i == index + ? sOut[i] == c + : sOut[i] == sIn[i] + }; + take sNullOut = RW(array_shift(s, string_len)); + sNullOut == sNullIn; +@*/ +{ + /*@ focus RW, index; @*/ + s[index] = c; +} \ No newline at end of file