From 25d2856af3283c2d9ae3d6daf2325c59a68dc8c1 Mon Sep 17 00:00:00 2001 From: Igor Tarakanov Date: Fri, 5 Jul 2019 15:50:19 +0300 Subject: [PATCH 01/14] [+] match_string proved --- .../whole_program/why3session.xml | 847 ++++++++++++++++++ src/match_string.c | 60 +- src/match_string.h | 36 +- 3 files changed, 891 insertions(+), 52 deletions(-) create mode 100644 sessions/match_string.c.av/whole_program/why3session.xml diff --git a/sessions/match_string.c.av/whole_program/why3session.xml b/sessions/match_string.c.av/whole_program/why3session.xml new file mode 100644 index 0000000..9ed1dba --- /dev/null +++ b/sessions/match_string.c.av/whole_program/why3session.xml @@ -0,0 +1,847 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/match_string.c b/src/match_string.c index beaf577..6e2bdc9 100644 --- a/src/match_string.c +++ b/src/match_string.c @@ -1,39 +1,23 @@ #include "match_string.h" -/*@ predicate null_terminator(char **array) = - \exists integer i; - 0 <= i && - array[i] == \null && - (\forall integer j; 0 <= j < i ==> array[j] != \null); - logic integer null_at(char **array) = - *array == \null ? 1 : 1 + null_at(array + 1); - */ -/*@ requires valid_str(string); - requires n <= INT_MAX; - requires (null_terminator(array) && - null_at(array) <= n && - \valid_read(array + (0 .. null_at(array))) && - (\forall integer i; 0 <= i < null_at(array) ==> valid_str(array[i]))) - || - (\valid_read(array + (0 .. n - 1)) && - (\forall integer i; 0 <= i < n ==> valid_str(array[i]))); - assigns \nothing; - */ int match_string(const char * const *array, size_t n, const char *string) { int index; const char *item; - /*@ loop invariant 0 <= index; - loop invariant null_terminator(array) ==> index <= null_at(array); - loop invariant !null_terminator(array) ==> index <= n; - loop assigns index; - loop variant n - index; - */ + /*@ + loop invariant 0 <= index <= n; + loop invariant \forall integer k; 0 <= k < index ==> + strcmp(array[k], string) != 0; + loop invariant \forall integer k; 0 <= k < index ==> + array[k] != NULL; + loop assigns index; + loop assigns item; + loop variant n - index; + */ for (index = 0; index < n; index++) { item = array[index]; - //@ assert item == \null || valid_str(item); if (!item) break; if (!strcmp(item, string)) @@ -41,26 +25,4 @@ int match_string(const char * const *array, size_t n, const char *string) } return -EINVAL; -} - - -#ifdef DUMMY_MAIN - -int main(int argc, char *argv[]) -{ - const char *str = "12345"; - const char *list[] = { - "TEST", - "TST", - "TS", - "T", - "12345", - NULL - }; - - match_string(list, -1, str); - match_string(list, 3, str); - - return 0; -} -#endif +} \ No newline at end of file diff --git a/src/match_string.h b/src/match_string.h index e4de8f8..ecdf53b 100644 --- a/src/match_string.h +++ b/src/match_string.h @@ -1,10 +1,8 @@ #ifndef __MATCH_STRING_H__ #define __MATCH_STRING_H__ -#include "kernel_definitions.h" #include "strcmp.h" - /** * match_string - matches given string in an array * @array: array of strings @@ -15,6 +13,38 @@ * index of a @string in the @array if matches, or %-EINVAL otherwise. */ +/*@ + logic integer cmp(unsigned char a, unsigned char b) = + a == b ? 0 : a < b ? -1 : 1; + + logic integer strncmp(char *cs, char *ct, integer n) = + n == -1 ? 0 : (cs[n] == ct[n] ? strncmp(cs+1, ct+1, n-1) : cmp((u8 AENO)cs[n], (u8 AENO)ct[n])); + logic integer strcmp(char *cs, char *ct) = strncmp(cs, ct, strlen(cs)); +*/ + +/*@ + requires \valid_read(array + (0..n-1)); + requires valid_str(string); + requires n <= INT_MAX; + requires \forall integer i; 0 <= i < n && valid_str(array[i]); + + assigns \nothing; + + behavior exists: + assumes \exists integer i; 0 <= i < n && strcmp(array[i], string) == 0; + ensures 0 <= \result < n; + ensures strcmp(array[\result], string) == 0; + ensures \forall integer i; 0 <= i < \result ==> + strcmp(array[\result], string) != 0; + + behavior missing: + assumes \forall integer i; 0 <= i < n ==> + strcmp(array[i], string) != 0; + ensures \result == -EINVAL; + + complete behaviors; + disjoint behaviors; +*/ int match_string(const char * const *array, size_t n, const char *string); -#endif // __MATCH_STRING_H__ \ No newline at end of file +#endif // __MATCH_STRING_H__ From 56546dad8b9164516ce0f433037f22570ea87eaa Mon Sep 17 00:00:00 2001 From: Igor Tarakanov Date: Fri, 5 Jul 2019 18:13:45 +0300 Subject: [PATCH 02/14] [fix] requirements for NULL terminated arrays, logic functions from strcmp.h --- README.md | 2 +- .../whole_program/why3session.xml | 15 ++++---- src/match_string.c | 23 +++++++++++- src/match_string.h | 36 +++++++++++++------ src/strcmp.h | 3 +- 5 files changed, 57 insertions(+), 22 deletions(-) diff --git a/README.md b/README.md index b8b2105..c585b96 100644 --- a/README.md +++ b/README.md @@ -16,7 +16,7 @@ The repository contains ACSL specifications for the Linux kernel functions. The | ID | Function | Status | Logic function | libfuzzer | Comment | |----|---------------|--------|----------------|-----------|---------| | 1 | check\_bytes8 | proved | proved | yes | | -| 2 | match\_string | | not required | | | +| 2 | match\_string | proved | not required | | | | 3 | memchr | proved | | yes | | | 4 | memcmp | proved | | yes | | | 5 | memscan | proved | not required | yes | | diff --git a/sessions/match_string.c.av/whole_program/why3session.xml b/sessions/match_string.c.av/whole_program/why3session.xml index 9ed1dba..2411659 100644 --- a/sessions/match_string.c.av/whole_program/why3session.xml +++ b/sessions/match_string.c.av/whole_program/why3session.xml @@ -2,23 +2,22 @@ - - + - + - + - + - + - + - + diff --git a/src/match_string.c b/src/match_string.c index 6e2bdc9..4ca0a52 100644 --- a/src/match_string.c +++ b/src/match_string.c @@ -25,4 +25,25 @@ int match_string(const char * const *array, size_t n, const char *string) } return -EINVAL; -} \ No newline at end of file +} + +#ifdef DUMMY_MAIN + + int main(int argc, char *argv[]) +{ + const char *str = "12345"; + const char *list[] = { + "TEST", + "TST", + "TS", + "T", + "12345", + NULL + }; + + match_string(list, -1, str); + match_string(list, 3, str); + + return 0; +} +#endif \ No newline at end of file diff --git a/src/match_string.h b/src/match_string.h index ecdf53b..cceccfb 100644 --- a/src/match_string.h +++ b/src/match_string.h @@ -1,6 +1,7 @@ #ifndef __MATCH_STRING_H__ #define __MATCH_STRING_H__ +#include "kernel_definitions.h" #include "strcmp.h" /** @@ -13,25 +14,38 @@ * index of a @string in the @array if matches, or %-EINVAL otherwise. */ -/*@ - logic integer cmp(unsigned char a, unsigned char b) = - a == b ? 0 : a < b ? -1 : 1; - - logic integer strncmp(char *cs, char *ct, integer n) = - n == -1 ? 0 : (cs[n] == ct[n] ? strncmp(cs+1, ct+1, n-1) : cmp((u8 AENO)cs[n], (u8 AENO)ct[n])); - logic integer strcmp(char *cs, char *ct) = strncmp(cs, ct, strlen(cs)); -*/ - /*@ requires \valid_read(array + (0..n-1)); requires valid_str(string); requires n <= INT_MAX; - requires \forall integer i; 0 <= i < n && valid_str(array[i]); + requires + ( + n == -1 && ( + \exists integer end; + array[end] == NULL && + ( + \forall integer k; + 0 < k < end && array[k] != NULL + ) && + ( + \forall integer k; + 0 < k < end && valid_str(array[k]) + ) + ) + + ) || + ( + n >= 0 && ( + \forall integer i; + 0 <= i < n && valid_str(array[i]) + ) + ); assigns \nothing; behavior exists: - assumes \exists integer i; 0 <= i < n && strcmp(array[i], string) == 0; + assumes \exists integer i; + 0 <= i < n && strcmp(array[i], string) == 0; ensures 0 <= \result < n; ensures strcmp(array[\result], string) == 0; ensures \forall integer i; 0 <= i < \result ==> diff --git a/src/strcmp.h b/src/strcmp.h index 2337d8d..ac7141b 100644 --- a/src/strcmp.h +++ b/src/strcmp.h @@ -3,7 +3,8 @@ #include "strlen.h" -/* axiomatic StrCmp { + +/*@ axiomatic StrCmp { logic integer cmp(unsigned char a, unsigned char b) = a == b ? 0 : a < b ? -1 : 1; From ca8d329b686039d9f77d8a19839fd8ba01c48549 Mon Sep 17 00:00:00 2001 From: Igor Tarakanov Date: Fri, 5 Jul 2019 18:18:34 +0300 Subject: [PATCH 03/14] [fix] correct -1 casting --- .../whole_program/why3session.xml | 42 +++++++++++-------- src/match_string.h | 2 +- 2 files changed, 26 insertions(+), 18 deletions(-) diff --git a/sessions/match_string.c.av/whole_program/why3session.xml b/sessions/match_string.c.av/whole_program/why3session.xml index 2411659..0533341 100644 --- a/sessions/match_string.c.av/whole_program/why3session.xml +++ b/sessions/match_string.c.av/whole_program/why3session.xml @@ -4,20 +4,20 @@ - + - + - + - + - + - + @@ -332,21 +332,29 @@ - - - - - + + + + + + + + + + + + + - + - + - + - + @@ -678,9 +686,9 @@ - + - + diff --git a/src/match_string.h b/src/match_string.h index cceccfb..f8608a5 100644 --- a/src/match_string.h +++ b/src/match_string.h @@ -20,7 +20,7 @@ requires n <= INT_MAX; requires ( - n == -1 && ( + n == (size_t AENO)(-1) && ( \exists integer end; array[end] == NULL && ( From ab9fcfd2b4bf98a8b226b3d4c29b10500c56417a Mon Sep 17 00:00:00 2001 From: Igor Tarakanov Date: Fri, 5 Jul 2019 21:41:45 +0300 Subject: [PATCH 04/14] [wip] --- src/match_string.c | 2 ++ src/match_string.h | 62 ++++++++++++++++++++++------------------------ 2 files changed, 32 insertions(+), 32 deletions(-) diff --git a/src/match_string.c b/src/match_string.c index 4ca0a52..a0c6f97 100644 --- a/src/match_string.c +++ b/src/match_string.c @@ -6,6 +6,8 @@ int match_string(const char * const *array, size_t n, const char *string) int index; const char *item; + /*@ assert 0 == 1; */ + /*@ loop invariant 0 <= index <= n; loop invariant \forall integer k; 0 <= k < index ==> diff --git a/src/match_string.h b/src/match_string.h index f8608a5..011cad3 100644 --- a/src/match_string.h +++ b/src/match_string.h @@ -15,46 +15,44 @@ */ /*@ - requires \valid_read(array + (0..n-1)); - requires valid_str(string); - requires n <= INT_MAX; - requires - ( - n == (size_t AENO)(-1) && ( - \exists integer end; - array[end] == NULL && - ( - \forall integer k; - 0 < k < end && array[k] != NULL - ) && - ( - \forall integer k; - 0 < k < end && valid_str(array[k]) - ) - ) - - ) || - ( - n >= 0 && ( - \forall integer i; - 0 <= i < n && valid_str(array[i]) - ) + logic size_t _real_len(char **array, size_t n) = + array[0] == NULL + ? (size_t) 0 + : ( + n > 0 + ? (size_t) (1 + _real_len(array + 1, (size_t)(n - 1))) + : 0 ); +*/ - assigns \nothing; +/*@ + requires _real_len(array, n) <= SIZE_MAX; + requires \valid_read(array + (0.._real_len(array, n)-1)); + requires valid_str(string); + + requires \forall integer i; + 0 <= i < _real_len(array, n) && + valid_str(array[i]); + + assigns \nothing; behavior exists: - assumes \exists integer i; - 0 <= i < n && strcmp(array[i], string) == 0; - ensures 0 <= \result < n; - ensures strcmp(array[\result], string) == 0; - ensures \forall integer i; 0 <= i < \result ==> + assumes \exists integer i; + 0 <= i < _real_len(array, n) && + strcmp(array[i], string) == 0; + + ensures 0 <= \result < _real_len(array, n); + ensures strcmp(array[\result], string) == 0; + ensures \forall integer k; + 0 <= k < \result && strcmp(array[\result], string) != 0; behavior missing: - assumes \forall integer i; 0 <= i < n ==> + assumes \forall integer i; + 0 <= i < _real_len(array, n) && strcmp(array[i], string) != 0; - ensures \result == -EINVAL; + + ensures \result == -EINVAL; complete behaviors; disjoint behaviors; From baa74c107106556708dd2ee97c235bac1c969082 Mon Sep 17 00:00:00 2001 From: Igor Tarakanov Date: Mon, 8 Jul 2019 14:10:07 +0300 Subject: [PATCH 05/14] [wip] --- src/match_string.c | 19 ++++--- src/match_string.h | 125 +++++++++++++++++++++++++++++++++++++-------- 2 files changed, 115 insertions(+), 29 deletions(-) diff --git a/src/match_string.c b/src/match_string.c index a0c6f97..3dc8299 100644 --- a/src/match_string.c +++ b/src/match_string.c @@ -6,26 +6,31 @@ int match_string(const char * const *array, size_t n, const char *string) int index; const char *item; - /*@ assert 0 == 1; */ /*@ - loop invariant 0 <= index <= n; - loop invariant \forall integer k; 0 <= k < index ==> - strcmp(array[k], string) != 0; - loop invariant \forall integer k; 0 <= k < index ==> - array[k] != NULL; + loop invariant 0 <= index < real_len(array, n); + loop invariant \forall integer k; 0 <= k < index ==> ( + array[k] != NULL && + strcmp(array[k], string) != 0 + ); loop assigns index; loop assigns item; - loop variant n - index; + loop variant real_len(array, n) - index; */ + for (index = 0; index < n; index++) { item = array[index]; if (!item) break; + //@ assert array[index] != NULL; if (!strcmp(item, string)) return index; + //@ assert strcmp(array[index], string) != 0; + //@ assert checked_head(array, string, index); } + //@ assert checked_head(array, string, n); + return -EINVAL; } diff --git a/src/match_string.h b/src/match_string.h index 011cad3..57e12ef 100644 --- a/src/match_string.h +++ b/src/match_string.h @@ -14,49 +14,130 @@ * index of a @string in the @array if matches, or %-EINVAL otherwise. */ + /*@ - logic size_t _real_len(char **array, size_t n) = - array[0] == NULL - ? (size_t) 0 - : ( - n > 0 - ? (size_t) (1 + _real_len(array + 1, (size_t)(n - 1))) - : 0 - ); + axiomatic MatchString { + logic integer real_len(char **array, integer n) = + ((n <= 0) || (array[0] == NULL)) + ? 0 + : 1 + real_len(array + 1, n - 1); + + predicate checked_head(char** array, char* string, integer tail) = + \forall integer k; + (0 <= k < tail) ==> ( + array[k] != NULL && + strcmp(array[k], string) != 0 + ); + + lemma zero_len_a: + \forall char** array; + \valid_read(array) ==> + real_len(array, 0) == 0; + + lemma zero_len_b: + \forall char** array, integer n; + ( + \valid_read(array) && + array[0] == NULL && + n > 0 + ) ==> + real_len(array, n) == 0; + + lemma one_element: + \forall char** array; + ( + \valid_read(array) && + array[0] != NULL + ) ==> + real_len(array, 1) == 1; + + lemma basic: + \forall char** array, integer n; + ( + n > 0 && + \valid_read(array+(0..n)) && + array[0] != NULL + ) ==> + (real_len(array, n) == + 1 + real_len(array + 1, n - 1)); + + lemma one_element_or_more: + \forall char** array, integer n; + ( + n > 0 && + \valid_read(array + (0..n)) && + array[0] != NULL + ) ==> + real_len(array, n + 1) > 0; + + lemma not_null_terminated: + \forall char** array, integer n; + ( + \valid_read(array+(0..n)) && + (\forall integer k; k <= n ==> array[k] != NULL) + ) ==> + real_len(array, n + 1) == n + 1; + + lemma lower_bound: + \forall char** array, integer n, char* string; + ( + valid_str(string) && + n > 0 && + \valid_read(array+(0..n)) + ) ==> ( + \forall integer k; + 0 <= k <= n && + checked_head(array, string, k) ==> + real_len(array, n + 1) >= k + ); + + lemma upper_bound: + \forall char** array, integer n; + ( + n >= 0 && + \valid_read(array + (0..n)) + ) ==> + (0 <= real_len(array, n + 1) <= n + 1); + + } */ /*@ - requires _real_len(array, n) <= SIZE_MAX; - requires \valid_read(array + (0.._real_len(array, n)-1)); + requires real_len(array, n) <= SIZE_MAX; + requires \valid_read(array + (0..real_len(array, n)-1)); requires valid_str(string); - requires \forall integer i; - 0 <= i < _real_len(array, n) && - valid_str(array[i]); + requires \forall integer k; + (0 <= k < real_len(array, n)) ==> + valid_str(array[k]); assigns \nothing; behavior exists: - assumes \exists integer i; - 0 <= i < _real_len(array, n) && - strcmp(array[i], string) == 0; + assumes \exists integer k; + (0 <= k < real_len(array, n)) ==> + strcmp(array[k], string) == 0; - ensures 0 <= \result < _real_len(array, n); + ensures 0 <= \result < real_len(array, n); ensures strcmp(array[\result], string) == 0; ensures \forall integer k; - 0 <= k < \result && - strcmp(array[\result], string) != 0; + (0 <= k < \result) ==> + ( + array[k] != NULL && + strcmp(array[\result], string) != 0 + ); behavior missing: - assumes \forall integer i; - 0 <= i < _real_len(array, n) && - strcmp(array[i], string) != 0; + assumes \forall integer k; + (0 <= k < real_len(array, n)) ==> + strcmp(array[k], string) != 0; ensures \result == -EINVAL; complete behaviors; disjoint behaviors; */ + int match_string(const char * const *array, size_t n, const char *string); #endif // __MATCH_STRING_H__ From 8dbb5dd7f4bc3ce8b9435cab3b7b471923e37dc7 Mon Sep 17 00:00:00 2001 From: Igor Tarakanov Date: Tue, 23 Jul 2019 20:07:19 +0300 Subject: [PATCH 06/14] [+] match_string for null-terminated arrays proved --- .../whole_program/why3session.xml | 71 +++++- src/match_string.c | 55 +++-- src/match_string.h | 217 ++++++++---------- src/strcmp.h | 5 +- 4 files changed, 195 insertions(+), 153 deletions(-) rename sessions/{match_string.c.av => match_string.av}/whole_program/why3session.xml (93%) diff --git a/sessions/match_string.c.av/whole_program/why3session.xml b/sessions/match_string.av/whole_program/why3session.xml similarity index 93% rename from sessions/match_string.c.av/whole_program/why3session.xml rename to sessions/match_string.av/whole_program/why3session.xml index 0533341..07e6212 100644 --- a/sessions/match_string.c.av/whole_program/why3session.xml +++ b/sessions/match_string.av/whole_program/why3session.xml @@ -2,22 +2,57 @@ - + + - + - + - + - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + @@ -332,7 +367,7 @@ - + @@ -346,13 +381,25 @@ - + + + + + + + + + + + + + - + @@ -686,9 +733,9 @@ - + - + diff --git a/src/match_string.c b/src/match_string.c index 3dc8299..10d77ad 100644 --- a/src/match_string.c +++ b/src/match_string.c @@ -5,31 +5,54 @@ int match_string(const char * const *array, size_t n, const char *string) { int index; const char *item; - - - /*@ - loop invariant 0 <= index < real_len(array, n); - loop invariant \forall integer k; 0 <= k < index ==> ( - array[k] != NULL && - strcmp(array[k], string) != 0 - ); - loop assigns index; + + /*@ + loop invariant 0 <= index <= real_len(array, n) <= n; + loop invariant + \forall size_t k; + 0 <= k < index ==> + strcmp(array[k], string) != 0; + loop invariant + \forall size_t k; + 0 <= k < index ==> + array[k] != NULL; + loop invariant + \forall size_t k; + 0 <= k < index ==> + valid_str(array[k]); + loop assigns index; loop assigns item; - loop variant real_len(array, n) - index; - */ - + loop variant real_len(array, n) - index; + */ for (index = 0; index < n; index++) { item = array[index]; if (!item) break; - //@ assert array[index] != NULL; + //@ assert valid_str(array[index]); if (!strcmp(item, string)) + //@ assert strlen(item) == strlen(string); + /*@ + assert \forall size_t i; + 0 < i <= strlen(item) ==> item[i] == string[i]; + */ return index; - //@ assert strcmp(array[index], string) != 0; - //@ assert checked_head(array, string, index); + + /*@ + assert + \exists size_t i; + ( + 0 <= i <= \min(strlen(item), strlen(string)) && + item[i] != string[i] + ); + */ + /*@ assert \forall size_t i; + 0 <= i <= index ==> strcmp(array[i], string) != 0; + */ } - //@ assert checked_head(array, string, n); + /*@ assert \forall size_t i; + 0 <= i < real_len(array, n) ==> strcmp(array[i], string) != 0; + */ return -EINVAL; } diff --git a/src/match_string.h b/src/match_string.h index 57e12ef..72e3ad2 100644 --- a/src/match_string.h +++ b/src/match_string.h @@ -5,7 +5,7 @@ #include "strcmp.h" /** - * match_string - matches given string in an array + * match_stringn - matches given string in an array * @array: array of strings * @n: number of strings in the array or -1 for NULL terminated arrays * @string: string to match with @@ -14,130 +14,103 @@ * index of a @string in the @array if matches, or %-EINVAL otherwise. */ +/* + * In fact this function searches in a subarray ending NULL + * If n > INT_MAX and in array[0..INT_MAX] there are not NULL int index will + * be overflowed + */ -/*@ - axiomatic MatchString { - logic integer real_len(char **array, integer n) = - ((n <= 0) || (array[0] == NULL)) - ? 0 - : 1 + real_len(array + 1, n - 1); - - predicate checked_head(char** array, char* string, integer tail) = - \forall integer k; - (0 <= k < tail) ==> ( - array[k] != NULL && - strcmp(array[k], string) != 0 - ); - - lemma zero_len_a: - \forall char** array; - \valid_read(array) ==> - real_len(array, 0) == 0; - - lemma zero_len_b: - \forall char** array, integer n; - ( - \valid_read(array) && - array[0] == NULL && - n > 0 - ) ==> - real_len(array, n) == 0; - - lemma one_element: - \forall char** array; - ( - \valid_read(array) && - array[0] != NULL - ) ==> - real_len(array, 1) == 1; - - lemma basic: - \forall char** array, integer n; - ( - n > 0 && - \valid_read(array+(0..n)) && - array[0] != NULL - ) ==> - (real_len(array, n) == - 1 + real_len(array + 1, n - 1)); - - lemma one_element_or_more: - \forall char** array, integer n; - ( - n > 0 && - \valid_read(array + (0..n)) && - array[0] != NULL - ) ==> - real_len(array, n + 1) > 0; - - lemma not_null_terminated: - \forall char** array, integer n; - ( - \valid_read(array+(0..n)) && - (\forall integer k; k <= n ==> array[k] != NULL) - ) ==> - real_len(array, n + 1) == n + 1; - - lemma lower_bound: - \forall char** array, integer n, char* string; - ( - valid_str(string) && - n > 0 && - \valid_read(array+(0..n)) - ) ==> ( - \forall integer k; - 0 <= k <= n && - checked_head(array, string, k) ==> - real_len(array, n + 1) >= k - ); - - lemma upper_bound: - \forall char** array, integer n; - ( - n >= 0 && - \valid_read(array + (0..n)) - ) ==> - (0 <= real_len(array, n + 1) <= n + 1); - - } -*/ + +/*@ axiomatic MatchString { + + logic size_t match_stringn(char** array, size_t n, char* string) = + n == 0 + ? 0 + : ( + strcmp(array[0], string) == 0 + ? 0 + : match_stringn(array + 1, (size_t)(n - 1), string) + ); + + logic size_t real_len(char** array, size_t n) = + ((array[0] == NULL) || (n == 0)) + ? 0 + : (size_t)((size_t)1 + real_len(array + 1, (size_t)(n - 1))); + + lemma real_len_not_nulls: + \forall char** array, size_t i, len; + 0 <= i < real_len(array, len) ==> array[i] != NULL; + + lemma real_len_terminate: + \forall char** array, size_t i, len; + i == real_len(array, len) ==> + array[i] == NULL || i == len; + + lemma real_len_maximum: + \forall char** array, size_t len; + (\forall size_t i; i < len ==> array[i] != NULL) ==> + real_len(array, len) == len; + + lemma match_string_definition: + \forall char** array, char* string, size_t i, len; + ( + 0 <= i < real_len(array, len) && + ( + \forall size_t j; + 0 <= j < i ==> strcmp(array[j], string) != 0 + ) && + strcmp(array[i], string) == 0 + ) ==> + match_stringn(array, real_len(array, len), string) == i; + + lemma strcmp_corollary: + \forall char* string1, char* string2; + ( + valid_str(string1) && + valid_str(string2) && + strcmp(string1, string2) != 0 + ) ==> ( + \exists size_t i; + 0 <= i <= \min(strlen(string1), strlen(string2)) && + string1[i] != string2[i] + ); +} + */ /*@ - requires real_len(array, n) <= SIZE_MAX; - requires \valid_read(array + (0..real_len(array, n)-1)); - requires valid_str(string); - - requires \forall integer k; - (0 <= k < real_len(array, n)) ==> - valid_str(array[k]); - - assigns \nothing; - - behavior exists: - assumes \exists integer k; - (0 <= k < real_len(array, n)) ==> - strcmp(array[k], string) == 0; - - ensures 0 <= \result < real_len(array, n); - ensures strcmp(array[\result], string) == 0; - ensures \forall integer k; - (0 <= k < \result) ==> - ( - array[k] != NULL && - strcmp(array[\result], string) != 0 - ); - - behavior missing: - assumes \forall integer k; - (0 <= k < real_len(array, n)) ==> - strcmp(array[k], string) != 0; - - ensures \result == -EINVAL; - - complete behaviors; - disjoint behaviors; + requires n <= INT_MAX; + requires (real_len(array, n) == n) ==> \valid(array+(0..n-1)); + requires (real_len(array, n) < n) ==> \valid(array+(0..real_len(array, n))); + requires valid_str(string); + requires \forall size_t i; + 0 <= i < real_len(array, n) ==> valid_str(array[i]); + + assigns \nothing; + + behavior exists: + assumes \exists size_t k; + (0 <= k < real_len(array, n)) && + strcmp(array[k], string) == 0; + + ensures \result == match_stringn(array, real_len(array, n), string); + ensures 0 <= \result < real_len(array, n); + ensures strcmp(array[\result], string) == 0; + ensures \forall size_t k; + (0 <= k < \result) ==> ( + strcmp(array[k], string) != 0 + ); + + behavior missing: + assumes \forall size_t k; + (0 <= k < real_len(array, n)) ==> ( + strcmp(array[k], string) != 0 + ); + + ensures \result == -EINVAL; + + complete behaviors; + disjoint behaviors; */ - -int match_string(const char * const *array, size_t n, const char *string); +int match_string(const char* const* array, size_t n, const char* string); #endif // __MATCH_STRING_H__ diff --git a/src/strcmp.h b/src/strcmp.h index ac7141b..61d69c9 100644 --- a/src/strcmp.h +++ b/src/strcmp.h @@ -3,13 +3,12 @@ #include "strlen.h" - /*@ axiomatic StrCmp { logic integer cmp(unsigned char a, unsigned char b) = a == b ? 0 : a < b ? -1 : 1; logic integer strncmp(char *cs, char *ct, integer n) = - n == -1 ? 0 : (cs[n] == ct[n] ? strncmp(cs+1, ct+1, n-1) : cmp((u8 AENO)cs[n], (u8 AENO)ct[n])); + n == -1 ? 0 : (cs[0] == ct[0] ? strncmp(cs+1, ct+1, n-1) : cmp((u8 AENO)cs[0], (u8 AENO)ct[0])); logic integer strcmp(char *cs, char *ct) = strncmp(cs, ct, strlen(cs)); predicate equaln(char *cs, char *ct, size_t n) = strncmp(cs, ct, n) == 0; predicate equal(char *cs, char *ct) = strcmp(cs, ct) == 0; @@ -58,7 +57,7 @@ /*@ requires valid_str(cs); requires valid_str(ct); assigns \nothing; - //ensures \result == strcmp(cs, ct); + ensures \result == strcmp(cs, ct); behavior equal: assumes \forall integer i; 0 <= i <= strlen(cs) ==> cs[i] == ct[i]; ensures \result == 0; From 4f7063525ca40a53e45dadc928f43c413eef560a Mon Sep 17 00:00:00 2001 From: Denis Efremov Date: Thu, 25 Jul 2019 15:35:43 +0300 Subject: [PATCH 07/14] match_string: regenerate session --- .../whole_program/why3session.xml | 34 +++++++++---------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/sessions/match_string.av/whole_program/why3session.xml b/sessions/match_string.av/whole_program/why3session.xml index 07e6212..4e7b613 100644 --- a/sessions/match_string.av/whole_program/why3session.xml +++ b/sessions/match_string.av/whole_program/why3session.xml @@ -2,57 +2,57 @@ - - - + + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + From 3b93699373747d931345c448f57ad1649257bac7 Mon Sep 17 00:00:00 2001 From: Denis Efremov Date: Thu, 25 Jul 2019 15:35:58 +0300 Subject: [PATCH 08/14] match_string: restore original main --- src/match_string.c | 35 ++++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/src/match_string.c b/src/match_string.c index 10d77ad..20c4fe9 100644 --- a/src/match_string.c +++ b/src/match_string.c @@ -57,23 +57,24 @@ int match_string(const char * const *array, size_t n, const char *string) return -EINVAL; } -#ifdef DUMMY_MAIN - int main(int argc, char *argv[]) -{ - const char *str = "12345"; - const char *list[] = { - "TEST", - "TST", - "TS", - "T", - "12345", - NULL - }; +#ifdef DUMMY_MAIN - match_string(list, -1, str); - match_string(list, 3, str); +int main(int argc, char *argv[]) +{ + const char *str = "12345"; + const char *list[] = { + "TEST", + "TST", + "TS", + "T", + "12345", + NULL + }; + + match_string(list, -1, str); + match_string(list, 3, str); - return 0; -} -#endif \ No newline at end of file + return 0; +} +#endif From 777541d36065f55d24ad4601866e683798a0786f Mon Sep 17 00:00:00 2001 From: Denis Efremov Date: Thu, 25 Jul 2019 23:54:40 +0300 Subject: [PATCH 09/14] match_string: reindend --- .../whole_program/why3session.xml | 48 +++--- src/match_string.c | 56 +++---- src/match_string.h | 149 ++++++++---------- 3 files changed, 111 insertions(+), 142 deletions(-) diff --git a/sessions/match_string.av/whole_program/why3session.xml b/sessions/match_string.av/whole_program/why3session.xml index 4e7b613..76a639d 100644 --- a/sessions/match_string.av/whole_program/why3session.xml +++ b/sessions/match_string.av/whole_program/why3session.xml @@ -5,12 +5,12 @@ - - - + + + - + @@ -20,39 +20,39 @@ - + - - + + - - + + - - + + - - + + - + - - + + - - + + - - + + - + - + @@ -893,9 +893,9 @@ - + - + diff --git a/src/match_string.c b/src/match_string.c index 20c4fe9..19c3aed 100644 --- a/src/match_string.c +++ b/src/match_string.c @@ -5,25 +5,18 @@ int match_string(const char * const *array, size_t n, const char *string) { int index; const char *item; - - /*@ - loop invariant 0 <= index <= real_len(array, n) <= n; - loop invariant - \forall size_t k; - 0 <= k < index ==> - strcmp(array[k], string) != 0; - loop invariant - \forall size_t k; - 0 <= k < index ==> - array[k] != NULL; - loop invariant - \forall size_t k; - 0 <= k < index ==> - valid_str(array[k]); - loop assigns index; - loop assigns item; - loop variant real_len(array, n) - index; - */ + + /*@ loop invariant 0 <= index <= real_len(array, n) <= n; + loop invariant \forall size_t k; + 0 <= k < index ==> strcmp(array[k], string) != 0; + loop invariant \forall size_t k; + 0 <= k < index ==> array[k] != NULL; + loop invariant \forall size_t k; + 0 <= k < index ==> valid_str(array[k]); + loop assigns index; + loop assigns item; + loop variant real_len(array, n) - index; + */ for (index = 0; index < n; index++) { item = array[index]; if (!item) @@ -31,28 +24,23 @@ int match_string(const char * const *array, size_t n, const char *string) //@ assert valid_str(array[index]); if (!strcmp(item, string)) //@ assert strlen(item) == strlen(string); - /*@ - assert \forall size_t i; - 0 < i <= strlen(item) ==> item[i] == string[i]; + /*@ assert \forall size_t i; + 0 < i <= strlen(item) ==> item[i] == string[i]; */ return index; - /*@ - assert - \exists size_t i; - ( - 0 <= i <= \min(strlen(item), strlen(string)) && - item[i] != string[i] - ); - */ + /*@ assert \exists size_t i; + 0 <= i <= \min(strlen(item), strlen(string)) && + item[i] != string[i]; + */ /*@ assert \forall size_t i; - 0 <= i <= index ==> strcmp(array[i], string) != 0; - */ + 0 <= i <= index ==> strcmp(array[i], string) != 0; + */ } /*@ assert \forall size_t i; - 0 <= i < real_len(array, n) ==> strcmp(array[i], string) != 0; - */ + 0 <= i < real_len(array, n) ==> strcmp(array[i], string) != 0; + */ return -EINVAL; } diff --git a/src/match_string.h b/src/match_string.h index 72e3ad2..49c4e1d 100644 --- a/src/match_string.h +++ b/src/match_string.h @@ -5,7 +5,7 @@ #include "strcmp.h" /** - * match_stringn - matches given string in an array + * match_string - matches given string in an array * @array: array of strings * @n: number of strings in the array or -1 for NULL terminated arrays * @string: string to match with @@ -20,93 +20,74 @@ * be overflowed */ - /*@ axiomatic MatchString { - logic size_t match_stringn(char** array, size_t n, char* string) = - n == 0 - ? 0 - : ( - strcmp(array[0], string) == 0 - ? 0 - : match_stringn(array + 1, (size_t)(n - 1), string) - ); - - logic size_t real_len(char** array, size_t n) = - ((array[0] == NULL) || (n == 0)) - ? 0 - : (size_t)((size_t)1 + real_len(array + 1, (size_t)(n - 1))); - - lemma real_len_not_nulls: - \forall char** array, size_t i, len; - 0 <= i < real_len(array, len) ==> array[i] != NULL; - - lemma real_len_terminate: - \forall char** array, size_t i, len; - i == real_len(array, len) ==> - array[i] == NULL || i == len; - - lemma real_len_maximum: - \forall char** array, size_t len; - (\forall size_t i; i < len ==> array[i] != NULL) ==> - real_len(array, len) == len; - - lemma match_string_definition: - \forall char** array, char* string, size_t i, len; - ( - 0 <= i < real_len(array, len) && - ( - \forall size_t j; - 0 <= j < i ==> strcmp(array[j], string) != 0 - ) && - strcmp(array[i], string) == 0 - ) ==> - match_stringn(array, real_len(array, len), string) == i; - - lemma strcmp_corollary: - \forall char* string1, char* string2; - ( - valid_str(string1) && - valid_str(string2) && - strcmp(string1, string2) != 0 - ) ==> ( - \exists size_t i; - 0 <= i <= \min(strlen(string1), strlen(string2)) && - string1[i] != string2[i] - ); -} + logic size_t match_string(char **a, size_t n, char *s) = + n == 0 ? + 0 + : + (strcmp(a[0], s) == 0 ? 0 : match_string(a + 1, (size_t)(n - 1), s)); + + logic size_t real_len(char **a, size_t n) = + ((a[0] == NULL) || (n == 0)) ? + 0 + : + (size_t)(1 + real_len(a + 1, (size_t)(n - 1))); + + lemma real_len_not_nulls: + \forall char **a, size_t i, len; + 0 <= i < real_len(a, len) ==> a[i] != NULL; + + lemma real_len_terminate: + \forall char **a, size_t i, len; + i == real_len(a, len) ==> a[i] == NULL || i == len; + + lemma real_len_maximum: + \forall char** array, size_t len; + (\forall size_t i; i < len ==> array[i] != NULL) ==> + real_len(array, len) == len; + + lemma match_string_definition: + \forall char** array, char* string, size_t i, len; + 0 <= i < real_len(array, len) && + (\forall size_t j; 0 <= j < i ==> strcmp(array[j], string) != 0) && + strcmp(array[i], string) == 0 ==> + match_string(array, real_len(array, len), string) == i; + + lemma strcmp_corollary: + \forall char* string1, char* string2; + valid_str(string1) && + valid_str(string2) && + strcmp(string1, string2) != 0 ==> + (\exists size_t i; + 0 <= i <= \min(strlen(string1), strlen(string2)) && + string1[i] != string2[i]); + } */ -/*@ - requires n <= INT_MAX; - requires (real_len(array, n) == n) ==> \valid(array+(0..n-1)); - requires (real_len(array, n) < n) ==> \valid(array+(0..real_len(array, n))); - requires valid_str(string); - requires \forall size_t i; - 0 <= i < real_len(array, n) ==> valid_str(array[i]); - - assigns \nothing; - - behavior exists: - assumes \exists size_t k; - (0 <= k < real_len(array, n)) && - strcmp(array[k], string) == 0; - - ensures \result == match_stringn(array, real_len(array, n), string); - ensures 0 <= \result < real_len(array, n); - ensures strcmp(array[\result], string) == 0; - ensures \forall size_t k; - (0 <= k < \result) ==> ( - strcmp(array[k], string) != 0 - ); - - behavior missing: - assumes \forall size_t k; - (0 <= k < real_len(array, n)) ==> ( - strcmp(array[k], string) != 0 - ); - - ensures \result == -EINVAL; +/*@ requires n <= INT_MAX; + requires (real_len(array, n) == n) ==> \valid(array+(0..n-1)); + requires (real_len(array, n) < n) ==> \valid(array+(0..real_len(array, n))); + requires valid_str(string); + requires \forall size_t i; + 0 <= i < real_len(array, n) ==> valid_str(array[i]); + + assigns \nothing; + + behavior exists: + assumes \exists size_t k; + (0 <= k < real_len(array, n)) && + strcmp(array[k], string) == 0; + ensures \result == match_string(array, real_len(array, n), string); + ensures 0 <= \result < real_len(array, n); + ensures strcmp(array[\result], string) == 0; + ensures \forall size_t k; + 0 <= k < \result ==> strcmp(array[k], string) != 0; + + behavior missing: + assumes \forall size_t k; + 0 <= k < real_len(array, n) ==> strcmp(array[k], string) != 0; + ensures \result == -EINVAL; complete behaviors; disjoint behaviors; From d25b3f1aedf6c52cf4affb6dc8a808df0db53740 Mon Sep 17 00:00:00 2001 From: Denis Efremov Date: Fri, 26 Jul 2019 00:11:38 +0300 Subject: [PATCH 10/14] match_string: simplify specification --- .../whole_program/why3session.xml | 43 ++++++------------- src/match_string.c | 18 +------- src/match_string.h | 6 +-- 3 files changed, 19 insertions(+), 48 deletions(-) diff --git a/sessions/match_string.av/whole_program/why3session.xml b/sessions/match_string.av/whole_program/why3session.xml index 76a639d..13e45d9 100644 --- a/sessions/match_string.av/whole_program/why3session.xml +++ b/sessions/match_string.av/whole_program/why3session.xml @@ -5,54 +5,39 @@ - + - + - + - + - + - + - - + + - - + + - - - - - - - - - - - - - - - - - + + - + - + diff --git a/src/match_string.c b/src/match_string.c index 19c3aed..a43e6c3 100644 --- a/src/match_string.c +++ b/src/match_string.c @@ -9,13 +9,10 @@ int match_string(const char * const *array, size_t n, const char *string) /*@ loop invariant 0 <= index <= real_len(array, n) <= n; loop invariant \forall size_t k; 0 <= k < index ==> strcmp(array[k], string) != 0; - loop invariant \forall size_t k; - 0 <= k < index ==> array[k] != NULL; loop invariant \forall size_t k; 0 <= k < index ==> valid_str(array[k]); - loop assigns index; - loop assigns item; - loop variant real_len(array, n) - index; + loop assigns index, item; + loop variant INT_MAX - index; */ for (index = 0; index < n; index++) { item = array[index]; @@ -23,25 +20,14 @@ int match_string(const char * const *array, size_t n, const char *string) break; //@ assert valid_str(array[index]); if (!strcmp(item, string)) - //@ assert strlen(item) == strlen(string); - /*@ assert \forall size_t i; - 0 < i <= strlen(item) ==> item[i] == string[i]; - */ return index; /*@ assert \exists size_t i; 0 <= i <= \min(strlen(item), strlen(string)) && item[i] != string[i]; */ - /*@ assert \forall size_t i; - 0 <= i <= index ==> strcmp(array[i], string) != 0; - */ } - /*@ assert \forall size_t i; - 0 <= i < real_len(array, n) ==> strcmp(array[i], string) != 0; - */ - return -EINVAL; } diff --git a/src/match_string.h b/src/match_string.h index 49c4e1d..d021c01 100644 --- a/src/match_string.h +++ b/src/match_string.h @@ -89,9 +89,9 @@ 0 <= k < real_len(array, n) ==> strcmp(array[k], string) != 0; ensures \result == -EINVAL; - complete behaviors; - disjoint behaviors; + complete behaviors; + disjoint behaviors; */ -int match_string(const char* const* array, size_t n, const char* string); +int match_string(const char * const *array, size_t n, const char *string); #endif // __MATCH_STRING_H__ From 87faa30d781cec1e2117a4d114c410ecbdfdcad4 Mon Sep 17 00:00:00 2001 From: Denis Efremov Date: Sun, 28 Jul 2019 18:46:48 +0300 Subject: [PATCH 11/14] strcmp: add logic function --- .../strcmp.av/whole_program/why3session.xml | 112 ++++++++++++++---- src/strcmp.c | 2 +- 2 files changed, 93 insertions(+), 21 deletions(-) diff --git a/sessions/strcmp.av/whole_program/why3session.xml b/sessions/strcmp.av/whole_program/why3session.xml index aef36a2..53ff32f 100644 --- a/sessions/strcmp.av/whole_program/why3session.xml +++ b/sessions/strcmp.av/whole_program/why3session.xml @@ -5,46 +5,104 @@ - - - - + + + + - + - + - + - + - + - + - - + + - - + + - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + - + - + @@ -351,6 +409,20 @@ + + + + + + + + + + + + + + @@ -843,9 +915,9 @@ - + - + diff --git a/src/strcmp.c b/src/strcmp.c index 266f99d..0b0775b 100644 --- a/src/strcmp.c +++ b/src/strcmp.c @@ -15,7 +15,7 @@ int strcmp(const char *cs, const char *ct) loop invariant \forall integer i; 0 <= i < cs - \at(cs,Pre) ==> \at(cs,Pre)[i] == \at(ct,Pre)[i]; loop invariant strlen(cs) == strlen(\at(cs,Pre)) - (cs - \at(cs,Pre)); - //loop invariant strcmp(\at(cs,Pre), \at(ct,Pre)) == strcmp(cs, ct); + loop invariant strcmp(\at(cs,Pre), \at(ct,Pre)) == strcmp(cs, ct); loop assigns cs, ct; loop variant strlen(\at(cs,Pre)) - (cs - \at(cs,Pre)); */ From 8345738083588a1438c2f96b4a48b2dea0f71d32 Mon Sep 17 00:00:00 2001 From: Denis Efremov Date: Sun, 28 Jul 2019 18:48:12 +0300 Subject: [PATCH 12/14] strncmp: move contract to the header --- README.md | 2 +- src/strncmp.c | 26 -------------------------- src/strncmp.h | 26 ++++++++++++++++++++++++++ 3 files changed, 27 insertions(+), 27 deletions(-) diff --git a/README.md b/README.md index c585b96..0c16a67 100644 --- a/README.md +++ b/README.md @@ -25,7 +25,7 @@ The repository contains ACSL specifications for the Linux kernel functions. The | 8 | strcat | proved | not required | | usr strcmp in ensures | | 9 | strchr | proved | proved | yes | | | 10 | strchrnul | proved | proved | yes | | -| 11 | strcmp | proved | | yes | | +| 11 | strcmp | proved | proved | yes | | | 12 | strcpy | proved | not required | | use strcmp logic function | | 13 | strcspn | proved | proved | yes | | | 14 | strim | | not required | !const | | diff --git a/src/strncmp.c b/src/strncmp.c index fbd183e..e74d398 100644 --- a/src/strncmp.c +++ b/src/strncmp.c @@ -1,31 +1,5 @@ #include "strncmp.h" -/*@ requires valid_strn(cs, count); - requires valid_strn(ct, count); - assigns \nothing; - ensures \result == -1 || \result == 0 || \result == 1; - behavior equal: - assumes count == 0 || - count > 0 && - (\forall integer i; 0 <= i < strnlen(cs, count) ==> (cs[i] == ct[i])) && - strnlen(cs, count) == strnlen(ct, count); - ensures \result == 0; - behavior len_diff: - assumes count > 0; - assumes \forall integer i; 0 <= i < strnlen(cs, count) ==> (cs[i] == ct[i]); - assumes strnlen(cs, count) != strnlen(ct, count); - ensures strnlen(cs, count) < strnlen(ct, count) ==> \result == -1; - ensures strnlen(cs, count) > strnlen(ct, count) ==> \result == 1; - behavior not_equal: - assumes count > 0; - assumes \exists integer i; 0 <= i < strnlen(cs, count) && cs[i] != ct[i]; - ensures \exists integer i; 0 <= i < strnlen(cs, count) && - (\forall integer j; 0 <= j < i ==> cs[j] == ct[j]) && - (cs[i] != ct[i]) && - ((u8 AENO)cs[i] < (u8 AENO)ct[i] ? \result == -1 : \result == 1); - complete behaviors; - disjoint behaviors; - */ int strncmp(const char *cs, const char *ct, size_t count) { unsigned char c1, c2; diff --git a/src/strncmp.h b/src/strncmp.h index 34cd370..49c3fdb 100644 --- a/src/strncmp.h +++ b/src/strncmp.h @@ -41,6 +41,32 @@ } */ +/*@ requires valid_strn(cs, count); + requires valid_strn(ct, count); + assigns \nothing; + ensures \result == -1 || \result == 0 || \result == 1; + behavior equal: + assumes count == 0 || + count > 0 && + (\forall integer i; 0 <= i < strnlen(cs, count) ==> (cs[i] == ct[i])) && + strnlen(cs, count) == strnlen(ct, count); + ensures \result == 0; + behavior len_diff: + assumes count > 0; + assumes \forall integer i; 0 <= i < strnlen(cs, count) ==> (cs[i] == ct[i]); + assumes strnlen(cs, count) != strnlen(ct, count); + ensures strnlen(cs, count) < strnlen(ct, count) ==> \result == -1; + ensures strnlen(cs, count) > strnlen(ct, count) ==> \result == 1; + behavior not_equal: + assumes count > 0; + assumes \exists integer i; 0 <= i < strnlen(cs, count) && cs[i] != ct[i]; + ensures \exists integer i; 0 <= i < strnlen(cs, count) && + (\forall integer j; 0 <= j < i ==> cs[j] == ct[j]) && + (cs[i] != ct[i]) && + ((u8 AENO)cs[i] < (u8 AENO)ct[i] ? \result == -1 : \result == 1); + complete behaviors; + disjoint behaviors; + */ int strncmp(const char *cs, const char *ct, size_t count); #endif // __STRNCMP_H__ From bbde78dfcde2efb006adc1a5939972d61add2a09 Mon Sep 17 00:00:00 2001 From: Denis Efremov Date: Sun, 28 Jul 2019 19:14:49 +0300 Subject: [PATCH 13/14] strnlen: session update --- .../strnlen.av/whole_program/why3session.xml | 978 +++++++++--------- 1 file changed, 489 insertions(+), 489 deletions(-) diff --git a/sessions/strnlen.av/whole_program/why3session.xml b/sessions/strnlen.av/whole_program/why3session.xml index 6c23402..a4eeb75 100644 --- a/sessions/strnlen.av/whole_program/why3session.xml +++ b/sessions/strnlen.av/whole_program/why3session.xml @@ -4,18 +4,18 @@ - - - + + + - - - + + + - - + + @@ -23,43 +23,43 @@ - + - + - + - + - - + + - - - + + + - - - + + + - - - + + + - - - + + + - + @@ -71,933 +71,933 @@ - + - + - - - + + + - - + + - - + + - - - + + + - - + + - - - + + + - - + + - - - + + + - - - + + + - - - + + + - - + + - - - + + + - - + + - - + + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + - + From 38ab80d0e82e9b545c977ec4d1fa34a75a7a3a07 Mon Sep 17 00:00:00 2001 From: Igor Tarakanov Date: Wed, 21 Aug 2019 19:37:59 +0300 Subject: [PATCH 14/14] [+] lemma functions --- .../whole_program/why3session.xml | 91 ++++++++++++------ src/match_string.h | 94 +++++++++++++++++++ 2 files changed, 156 insertions(+), 29 deletions(-) diff --git a/sessions/match_string.av/whole_program/why3session.xml b/sessions/match_string.av/whole_program/why3session.xml index 13e45d9..4f30d7b 100644 --- a/sessions/match_string.av/whole_program/why3session.xml +++ b/sessions/match_string.av/whole_program/why3session.xml @@ -2,42 +2,51 @@ - - - - + + + - + - - - + + + - + - + - + - + - + - + - - + + + + + + + + + + + + - - + + @@ -366,17 +375,17 @@ - - - - - - - - - - - + + + + + + + + + + + @@ -878,6 +887,30 @@ + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/match_string.h b/src/match_string.h index d021c01..9783cbe 100644 --- a/src/match_string.h +++ b/src/match_string.h @@ -20,6 +20,8 @@ * be overflowed */ +#ifndef LEMMA_FUNCTIONS + /*@ axiomatic MatchString { logic size_t match_string(char **a, size_t n, char *s) = @@ -65,6 +67,98 @@ } */ +#else + +/*@ axiomatic Strchrnul { + logic size_t match_string(char **a, size_t n, char *s) = + n == 0 ? + 0 + : + (strcmp(a[0], s) == 0 ? 0 : match_string(a + 1, (size_t)(n - 1), s)); + + logic size_t real_len(char **a, size_t n) = + ((a[0] == NULL) || (n == 0)) ? + 0 + : + (size_t)(1 + real_len(a + 1, (size_t)(n - 1))); + } + */ + +/*@ ghost + @ /@ lemma + @ @ requires 0 <= i < real_len(a, len); + @ @ decreases i; + @ @ ensures a[i] != NULL; + @ @/ + @ void real_len_iteration_1(char **a, size_t i, size_t len) + @ { + @ if (a[i] != NULL && len > 0) + @ real_len_iteration_1(a + 1, i + 1, len - 1); + @ } + @*/ + +/*@ ghost + @ /@ lemma + @ @ requires i == real_len(a, len); + @ @ decreases i; + @ @ ensures a[i] == NULL || i == len; + @ @/ + @ void real_len_iteration_2(char **a, size_t i, size_t len) + @ { + @ if (a[i] != NULL && len > 0) + @ real_len_iteration_2(a + 1, i + 1, len - 1); + @ } + @*/ + +/*@ ghost + @ /@ lemma + @ @ requires (\forall size_t i; i < len ==> a[i] != NULL); + @ @ decreases len; + @ @ ensures real_len(a, len) == len; + @ @/ + @ void real_len_iteration_4(char** a, size_t len) + @ { + @ if (*a != NULL && len > 0) + @ real_len_iteration_4(a + 1, len - 1); + @ } + @*/ + +/*@ ghost + @ /@ lemma + @ @ requires 0 <= i < real_len(array, len) && + @ (\forall size_t j; 0 <= j < i ==> strcmp(array[j], string) != 0) && + @ strcmp(array[i], string) == 0; + @ @ decreases len; + @ @ ensures match_string(array, real_len(array, len), string) == i; + @ @/ + @ void real_len_iteration_5(char** array, char* string, size_t i, size_t len) + @ { + @ if (srrcmp(array[i], string) != 0 && len > 0) + @ real_len_iteration_5(array, string, i + 1, len - 1); + @ } + @*/ + +/*@ ghost + @ /@ lemma + @ @ requires valid_str(string1) && + @ valid_str(string2) && + @ strcmp(string1, string2) != 0; + @ @ decreases strlen(string1); + @ @ ensures (\exists size_t i; + @ 0 <= i <= \min(strlen(string1), strlen(string2)) && + @ string1[i] != string2[i]); + @ @/ + @ void real_len_iteration_6(char* string1, char* string2) + @ { + @ if (*string1 != *string2 && *string1 != '\0' && *string2 != '\0') + @ real_len_iteration_6(string1 + 1, string2 + 1); + @ } + @*/ + + + +#endif /* LEMMA_FUNCTIONS */ + /*@ requires n <= INT_MAX; requires (real_len(array, n) == n) ==> \valid(array+(0..n-1)); requires (real_len(array, n) < n) ==> \valid(array+(0..real_len(array, n)));