From 133dc3d4cbae6682eb45407c7e7798b9f73b24c3 Mon Sep 17 00:00:00 2001 From: Pavel Ivanov Date: Thu, 8 Aug 2019 20:13:29 +0300 Subject: [PATCH 1/3] strnstr: specifications added --- src/strnstr.c | 60 +++++++++++++++++++++++++++++++++++++++++++++++++++ src/strnstr.h | 2 +- 2 files changed, 61 insertions(+), 1 deletion(-) diff --git a/src/strnstr.c b/src/strnstr.c index 49c4d3c..1f1f1d2 100644 --- a/src/strnstr.c +++ b/src/strnstr.c @@ -1,18 +1,78 @@ #include "strnstr.h" +/*@ predicate eqstr{L1, L2}(char *str1, char *str2, integer n) = + \forall integer i; 0 <= i < n ==> \at(str1[i], L1) == \at(str2[i], L2); +*/ + +/*@ requires valid_str(s1); + requires valid_str(s2); + requires len <= strlen(s1); + assigns \nothing; + + behavior empty: + assumes strlen(s2) == 0; + ensures \result == s1; + behavior len_l_l2: + assumes strlen(s2) != 0; + assumes len < strlen(s2); + ensures \result == NULL; + behavior not_found: + assumes strlen(s2) != 0; + assumes len >= strlen(s2); + assumes \forall integer j; 0 <= j <= len - strlen(s2) ==> !eqstr{Pre, Pre}(s1 + j, s2, strlen(s2)); + ensures \result == NULL; + behavior found: + assumes strlen(s2) != 0; + assumes len >= strlen(s2); + assumes \exists integer j; 0 <= j <= len - strlen(s2) && eqstr{Pre, Pre}(s1 + j, s2, strlen(s2)); + ensures eqstr{Post, Pre}(\result, s2, strlen(s2)); + disjoint behaviors; + complete behaviors; +*/ + char *strnstr(const char *s1, const char *s2, size_t len) { size_t l2; + //@ ghost char* os1 = s1; + //@ ghost size_t olen = len; + //@ ghost bool t = false; l2 = strlen(s2); + //@ assert strlen(s2) == l2; if (!l2) return (char *)s1; + /*@ + //loop invariant valid_str(os1); + //loop invariant s1 - olen >= os1 - len; + //loop invariant s1 - os1 == olen - len; + loop invariant os1 <= s1 <= os1 + strlen(os1); + loop invariant s1 + len == os1 + olen; + loop invariant len <= strlen(s1); + loop invariant valid_str(s1); + loop invariant valid_str(s2); + loop assigns len, s1; + //loop invariant eqstr{Pre, Pre}(\at(s1, Pre), s2, l2) ^^ !eqstr{Pre, Pre}(\at(s1, Pre), s2, l2); + //loop invariant s1 == os1 || !eqstr{Here, Pre}(s1 - 1, s2, l2); + //loop invariant eqstr{Pre, Pre}(\at(s1, Pre), s2, l2) ^^ (\forall integer j; 0 <= j <= s1 - os1 ==> !eqstr{Here, Pre}(\at(s1, Pre) + j, s2, l2)); + //loop invariant (s1 != os1) ==> (\forall integer j; 0 <= j <= s1 - os1 ==> !eqstr{Pre, Pre}(os1 + j, s2, l2)); + loop invariant \forall integer j; 0 <= j < s1 - os1 ==> !eqstr{Pre, Pre}(os1 + j, s2, l2); + loop variant len; + */ while (len >= l2) { + //@ ghost t = false; + //@ assert \at(len, Pre) >= strlen(s2); len--; if (!memcmp(s1, s2, l2)) + //@ assert eqstr{Here, Pre}(s1, s2, l2); + //@ assert strlen(os1) == strlen{Pre}(\at(s1, Pre)); + //@ assert \forall integer i; 0 <= i < strlen{Pre}(\at(s1, Pre)) ==> \at(os1[i], Here) == \at(s1[i], Pre); + //@ assert eqstr{Here, Pre}(os1, \at(s1, Pre), strlen{Pre}(\at(s1, Pre))); + //@ assert \exists integer j; eqstr{Here, Pre}(os1 + j, s2, l2) && j == s1 - os1; return (char *)s1; s1++; } + //@ assert len < strlen(s2); + //@ assert \forall integer j; 0 <= j <= len - l2 ==> !eqstr{Pre, Pre}(\at(s1, Pre) + j, s2, l2); return NULL; } diff --git a/src/strnstr.h b/src/strnstr.h index 1411cd5..ba978cb 100644 --- a/src/strnstr.h +++ b/src/strnstr.h @@ -2,7 +2,7 @@ #define __STRNSTR_H__ #include "kernel_definitions.h" -#include "memcmp.h" +//#include "memcmp.h" #include "strlen.h" /** From 03bdb993e45ca15ead2d9475efd616d53b813a67 Mon Sep 17 00:00:00 2001 From: Pavel Ivanov Date: Thu, 8 Aug 2019 20:14:01 +0300 Subject: [PATCH 2/3] strnstr: session added --- ...WP_parameter_strnstr_ensures_default_1.why | 114 ++ .../strnstr.av/whole_program/why3session.xml | 1191 +++++++++++++++++ 2 files changed, 1305 insertions(+) create mode 100644 sessions/strnstr.av/whole_program/whole_program-Function_strnstr_behaviors-WP_parameter_strnstr_ensures_default_1.why create mode 100644 sessions/strnstr.av/whole_program/why3session.xml diff --git a/sessions/strnstr.av/whole_program/whole_program-Function_strnstr_behaviors-WP_parameter_strnstr_ensures_default_1.why b/sessions/strnstr.av/whole_program/whole_program-Function_strnstr_behaviors-WP_parameter_strnstr_ensures_default_1.why new file mode 100644 index 0000000..008f227 --- /dev/null +++ b/sessions/strnstr.av/whole_program/whole_program-Function_strnstr_behaviors-WP_parameter_strnstr_ensures_default_1.why @@ -0,0 +1,114 @@ +(* this is the prelude for Alt-Ergo, version >= 0.95.2 *) +(* this is a prelude for Alt-Ergo integer arithmetic *) +logic comp_div: int, int -> int +axiom comp_div_def: forall x, y:int. x >= 0 and y > 0 -> comp_div(x,y) = x / y +logic comp_mod: int, int -> int +axiom comp_mod_def: forall x, y:int. x >= 0 and y > 0 -> comp_mod(x,y) = x % y +logic match_bool : bool, 'a, 'a -> 'a + +axiom match_bool_True : + (forall z:'a. forall z1:'a. (match_bool(true, z, z1) = z)) + +axiom match_bool_False : + (forall z:'a. forall z1:'a. (match_bool(false, z, z1) = z1)) + +type 't pointer + +logic null : 't pointer + +logic sub_pointer : 't pointer, 't pointer -> int + +logic shift : 't pointer, int -> 't pointer + +logic same_block : 't pointer, 't pointer -> prop + +type 't tag_id + +logic int_of_tag : 't tag_id -> int + +type voidP + +type t + +logic to_int : t -> int + +logic of_int : int -> t + +predicate infix_ls(a: t, b: t) = (to_int(a) < to_int(b)) + +predicate infix_gt(a: t, b: t) = (to_int(b) < to_int(a)) + +type t1 + +logic to_int1 : t1 -> int + +logic of_int1 : int -> t1 + +type t2 + +logic to_int2 : t2 -> int + +logic of_int2 : int -> t2 + +type 't3 alloc_table + +logic offset_min : 't3 alloc_table, 't3 pointer -> int + +logic offset_max : 't3 alloc_table, 't3 pointer -> int + +logic strlen : voidP pointer, (voidP pointer,t2) farray -> t + +axiom strlen_def : + (forall s_0:voidP pointer. + forall charP_charM_s_0_3_at_L:(voidP pointer,t2) farray. + (((charP_charM_s_0_3_at_L[shift(s_0, 0)]) = of_int2(0)) -> (strlen(s_0, + charP_charM_s_0_3_at_L) = of_int(0)))) + +axiom strlen_def1 : + (forall s_0:voidP pointer. + forall charP_charM_s_0_3_at_L:(voidP pointer,t2) farray. + ((not ((charP_charM_s_0_3_at_L[shift(s_0, 0)]) = of_int2(0))) -> + (strlen(s_0, charP_charM_s_0_3_at_L) = of_int((1 + to_int(strlen(shift(s_0, + 1), charP_charM_s_0_3_at_L))))))) + +predicate valid_str(s: voidP pointer, + voidP_s_2_alloc_table_at_L: voidP alloc_table, + charP_charM_s_2_at_L: (voidP pointer,t2) farray) = + (exists n_1_0:t. (((charP_charM_s_2_at_L[shift(s, + to_int(n_1_0))]) = of_int2(0)) and ((0 <= to_int(n_1_0)) -> + ((offset_min(voidP_s_2_alloc_table_at_L, s) <= 0) and + (offset_max(voidP_s_2_alloc_table_at_L, s) >= to_int(n_1_0)))))) + +logic parenttag : 't3 tag_id, 't3 tag_id -> prop + +logic subtag : 't3 tag_id, 't3 tag_id -> prop + +logic bottom_tag : 'a tag_id + +logic voidP_tag : voidP tag_id + +logic downcast : ('t3 pointer,'t3 tag_id) farray, 't3 pointer, + 't3 tag_id -> 't3 pointer + +logic charP_tag : voidP tag_id + +predicate allocated(a: 't3 alloc_table, p: 't3 pointer) = (offset_min(a, + p) <= offset_max(a, p)) + +goal WP_parameter_strnstr_ensures_default : + (forall s1:voidP pointer. forall s2:voidP pointer. forall len:t. + forall voidP_s1_19_alloc_table:voidP alloc_table. + forall voidP_s2_20_alloc_table:voidP alloc_table. + forall voidP_s1_19_tag_table:(voidP pointer,voidP tag_id) farray. + forall charP_charM_s1_19:(voidP pointer,t2) farray. + forall charP_charM_s2_20:(voidP pointer,t2) farray. + (((allocated(voidP_s1_19_alloc_table, s1) -> + (((voidP_s1_19_tag_table[s1]) = charP_tag) and + (forall i:int. (((offset_min(voidP_s1_19_alloc_table, s1) <= i) and + (i < offset_max(voidP_s1_19_alloc_table, s1))) -> + ((voidP_s1_19_tag_table[shift(s1, i)]) = charP_tag))))) and (valid_str(s1, + voidP_s1_19_alloc_table, charP_charM_s1_19) and (valid_str(s2, + voidP_s2_20_alloc_table, charP_charM_s2_20) and (infix_ls(len, + of_int(18446744073709551615)) and ((strlen(s2, + charP_charM_s2_20) = of_int(0)) and infix_gt(strlen(s2, charP_charM_s2_20), + of_int(0))))))) -> (0 = 1))) diff --git a/sessions/strnstr.av/whole_program/why3session.xml b/sessions/strnstr.av/whole_program/why3session.xml new file mode 100644 index 0000000..b86d8a4 --- /dev/null +++ b/sessions/strnstr.av/whole_program/why3session.xml @@ -0,0 +1,1191 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + From ccb2a3c350590071ab75876e7e8ab7605f01c2e9 Mon Sep 17 00:00:00 2001 From: Pavel Ivanov Date: Thu, 8 Aug 2019 20:15:15 +0300 Subject: [PATCH 3/3] README: mark strnstr as proved --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index 0c16a67..9f2ed6f 100644 --- a/README.md +++ b/README.md @@ -36,7 +36,7 @@ The repository contains ACSL specifications for the Linux kernel functions. The | 19 | strncmp | proved | | yes | | | 20 | strncpy | | not required | | | | 21 | strnlen | proved | proved | yes | | -| 22 | strnstr | | | yes | | +| 22 | strnstr | proved | | yes | | | 23 | strpbrk | proved | proved | yes | | | 24 | strrchr | proved | | yes | | | 25 | strreplace | | not required | !const | |