Skip to content
This repository has been archived by the owner on Feb 24, 2023. It is now read-only.

lemma functions for match_string #14

Open
wants to merge 15 commits into
base: master
Choose a base branch
from
Open

lemma functions for match_string #14

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
25d2856
[+] match_string proved
Jul 5, 2019
56546da
[fix] requirements for NULL terminated arrays, logic functions from s…
Jul 5, 2019
ca8d329
[fix] correct -1 casting
Jul 5, 2019
ab9fcfd
[wip]
Jul 5, 2019
baa74c1
[wip]
Jul 8, 2019
8dbb5dd
[+] match_string for null-terminated arrays proved
Jul 23, 2019
4f70635
match_string: regenerate session
evdenis Jul 25, 2019
3b93699
match_string: restore original main
evdenis Jul 25, 2019
777541d
match_string: reindend
evdenis Jul 25, 2019
d25b3f1
match_string: simplify specification
evdenis Jul 25, 2019
87faa30
strcmp: add logic function
evdenis Jul 28, 2019
8345738
strncmp: move contract to the header
evdenis Jul 28, 2019
bbde78d
strnlen: session update
evdenis Jul 28, 2019
8e420ba
Merge branch 'master' of github.com:evdenis/verker
Aug 21, 2019
38ab80d
[+] lemma functions
Aug 21, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
91 changes: 62 additions & 29 deletions sessions/match_string.av/whole_program/why3session.xml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,42 +2,51 @@
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="CVC4" version="1.6" alternative="noBV" timelimit="2" steplimit="0" memlimit="2000"/>
<prover id="1" name="Alt-Ergo" version="2.3.0" timelimit="2" steplimit="0" memlimit="2000"/>
<file name="../whole_program.mlw" expanded="true">
<theory name="Function_match_string_0_safety" sum="1f8cc5c24984d52512517b21ae5a2b91" expanded="true">
<prover id="0" name="CVC4" version="1.6" timelimit="5" steplimit="0" memlimit="1000"/>
<file name="../match_string_c.mlw" expanded="true">
<theory name="Function_match_string_0_safety" sum="3b002289067cc2e04884e4456f785076" expanded="true">
<goal name="WP_parameter match_string_0" expl="Function match_string, safety" expanded="true">
<proof prover="0"><result status="valid" time="0.14"/></proof>
<proof prover="0"><result status="valid" time="0.94" steps="224269"/></proof>
</goal>
</theory>
<theory name="Function_match_string_0_behaviors" sum="2f161d4328733cc19f2abd76a447ae37" expanded="true">
<goal name="WP_parameter match_string_ensures_default" expl="Function match_string, default behavior" expanded="true">
<transf name="split_goal_wp" expanded="true">
<theory name="Function_match_string_0_behaviors" sum="e25eb01a76d367c7275a2b285cb2e34b" expanded="true">
<goal name="WP_parameter match_string_ensures_default" expl="Function match_string, default behavior">
<transf name="split_goal_wp">
<goal name="WP_parameter match_string_ensures_default.1" expl="Behavior disjointness check">
<proof prover="1"><result status="valid" time="0.04" steps="151"/></proof>
<proof prover="0"><result status="valid" time="0.19" steps="40246"/></proof>
</goal>
<goal name="WP_parameter match_string_ensures_default.2" expl="Behavior completeness check">
<proof prover="1"><result status="valid" time="0.04" steps="149"/></proof>
<proof prover="0"><result status="valid" time="0.19" steps="40250"/></proof>
</goal>
<goal name="WP_parameter match_string_ensures_default.3" expl="loop invariant init">
<proof prover="0"><result status="valid" time="0.19"/></proof>
<proof prover="0"><result status="valid" time="0.43" steps="113464"/></proof>
</goal>
<goal name="WP_parameter match_string_ensures_default.4" expl="Assertion in line 21">
<proof prover="1"><result status="valid" time="0.11" steps="912"/></proof>
<proof prover="0"><result status="valid" time="0.39" steps="68706"/></proof>
</goal>
<goal name="WP_parameter match_string_ensures_default.5" expl="Assertion in line 25">
<proof prover="1"><result status="valid" time="1.34" steps="9983"/></proof>
<proof prover="0"><result status="valid" time="0.31" steps="58709"/></proof>
</goal>
<goal name="WP_parameter match_string_ensures_default.6" expl="loop invariant preservation">
<proof prover="1"><result status="valid" time="0.31" steps="2523"/></proof>
<proof prover="0"><result status="valid" time="0.70" steps="117333"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter match_string_ensures_exists" expl="Function match_string, behavior exists" expanded="true">
<proof prover="1"><result status="valid" time="1.44" steps="6473"/></proof>
<goal name="WP_parameter match_string_ensures_exists" expl="Function match_string, behavior exists">
<transf name="split_goal_wp">
<goal name="WP_parameter match_string_ensures_exists.1" expl="Postcondition (Ensures clause)">
<proof prover="0"><result status="valid" time="0.22" steps="57428"/></proof>
</goal>
<goal name="WP_parameter match_string_ensures_exists.2" expl="Postcondition (Ensures clause)">
<proof prover="0"><result status="valid" time="1.26" steps="206471"/></proof>
</goal>
<goal name="WP_parameter match_string_ensures_exists.3" expl="Postcondition (Ensures clause)">
<proof prover="0"><result status="valid" time="0.17" steps="44607"/></proof>
</goal>
</transf>
</goal>
<goal name="WP_parameter match_string_ensures_missing" expl="Function match_string, behavior missing" expanded="true">
<proof prover="1"><result status="valid" time="0.32" steps="2393"/></proof>
<goal name="WP_parameter match_string_ensures_missing" expl="Function match_string, behavior missing">
<proof prover="0"><result status="valid" time="1.25" steps="229496"/></proof>
</goal>
</theory>
<theory name="Axiomatic_Padding" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
Expand Down Expand Up @@ -366,17 +375,17 @@
<goal name="At_end" expl="Lemma at_end" expanded="true">
</goal>
</theory>
<theory name="Axiomatic_MatchString" sum="d8754ca9cc049dbbfef27b01ad97e44c" expanded="true">
<goal name="Real_len_not_nulls" expl="Lemma real_len_not_nulls" expanded="true">
</goal>
<goal name="Real_len_terminate" expl="Lemma real_len_terminate" expanded="true">
</goal>
<goal name="Real_len_maximum" expl="Lemma real_len_maximum" expanded="true">
</goal>
<goal name="Match_string_definition" expl="Lemma match_string_definition" expanded="true">
</goal>
<goal name="Strcmp_corollary" expl="Lemma strcmp_corollary" expanded="true">
</goal>
<theory name="Axiomatic_Strchrnul" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Axiomatic_LF__Axiomatic__real_len_iteration_1" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Axiomatic_LF__Axiomatic__real_len_iteration_2" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Axiomatic_LF__Axiomatic__real_len_iteration_4" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Axiomatic_LF__Axiomatic__real_len_iteration_5" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Axiomatic_LF__Axiomatic__real_len_iteration_6" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Safe_uint64_of_Safe_int32" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
Expand Down Expand Up @@ -878,6 +887,30 @@
</theory>
<theory name="Function_strlen_0_safe" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_real_len_iteration_1" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_real_len_iteration_1_safe" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_real_len_iteration_2" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_real_len_iteration_2_safe" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_real_len_iteration_4" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_real_len_iteration_4_safe" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_srrcmp" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_srrcmp_safe" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_real_len_iteration_5" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_real_len_iteration_5_safe" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_real_len_iteration_6" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_real_len_iteration_6_safe" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_match_string_0" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Function_match_string_0_safe" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
Expand Down
94 changes: 94 additions & 0 deletions src/match_string.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,8 @@
* be overflowed
*/

#ifndef LEMMA_FUNCTIONS

/*@ axiomatic MatchString {

logic size_t match_string(char **a, size_t n, char *s) =
Expand Down Expand Up @@ -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)));
Expand Down