Repository navigation
Conversation
AstraVer (Jessie) has had no release since frama-c.astraver.v20.0 and no longer builds against a current Frama-C. Drop the plugin-specific build and proof machinery so the project targets stock Frama-C/WP: - delete the 30 sessions/*.av why3 proof protocols and the CI workflow - drop the verify/replay/sprove Makefile targets and the why3 'verker' strategy - drop acsl_syntax_extension.h; expand AENO/AENOC to nothing and FRAMAC_VTAB_BUG to a literal '\v', which vanilla Frama-C 33 handles - collapse the ctype string-literal model and its global invariant - park the lemma functions behind #undef LEMMA_FUNCTIONS; they stay in the headers until ported to vanilla ACSL ghost functions - README: keep the AstraVer status as history, add an empty WP column
Frama-C 33 rejected eight files. All fixes are syntactic; no contract
changes semantics.
- drop 'requires \typeof(x) <: \type(T)' (13 clauses): WP has no
\typeof/<:, and the neighbouring \valid_read cast already says it
- cast the recursive logic bodies of match_string, real_len, strncmp and
sysfs_strlen to their declared return type, not integer
- ghost code is C and cannot call a logic function: replace the four
'ghost size_t n = strlen(...)' bindings with strlen{Pre}(...)
- strlcat: 'ghost Mid:' is a label without a statement
- expand __visible to nothing under Frama-C, which does not know
__externally_visible__
All 44 src/*.c now typecheck with no warnings.
Replaces the removed AstraVer targets. -c11 no longer exists in Frama-C 33 and aborted every run; the language level moves to -std c11. - wp, wp-<fn>, wp-proved, wp-status, wp-smoke, wp-gui-<fn> - wp-replay replays from the committed cache with -wp-cache offline and never invokes a solver; wp-rebuild regenerates after a toolchain bump - wp-report writes per-function -wp-report-json baselines with paths relative to the source root - wp-prune rebuilds the committed cache from the functions marked proved in the README WP column, keeping only entries that record a proof, so neither cached timeouts nor goals of unproved functions are committed - eva replaces the deprecated -val and is restricted to the files that actually define a libFuzzer harness; it is kept out of the WP run so a harness-specific verdict cannot suppress a WP goal - rte likewise restricted to the fuzz-harness files Some goals are out of reach for the SMT provers but fall to a WP tactic, so 'script' comes first in the prover list: an ordinary run replays a saved script before calling a prover, and the search cost is paid once. wp-auto-<fn> runs the search and writes the script to sessions/script/, and -wp-script batch keeps runs from silently rewriting saved scripts. Note that raising TIMEOUT does nothing to a goal whose timeout is already cached; that needs wp-rebuild. Both -warn-unsigned-overflow and -warn-unsigned-downcast are left off. Unsigned wraparound is defined behaviour in C, and this corpus is built out of two kernel idioms that rely on it: 'while (count--)', where RTE asserts '0 <= count - 1' before the decrement and is false on the last iteration, and the byte comparison 'c = (unsigned char) *s++', where converting a negative char is the entire point of the expression. With either check on, RTE asks these functions to prove they never do the thing they exist to do, and it made 19 goals across 11 functions unprovable by construction. AENO and AENOC suppressed exactly this under AstraVer. Baseline: 2092/2579 goals proved across 44 files.
Without them Frama-C generated default clauses for every ctype callee, so any proof that calls isxdigit or _tolower rested on invented specifications. The functions are pure, so the clauses are exact. Also drop the duplicate tolower/toupper contracts from ctype.c; the header is the single source of truth and Frama-C was merging the two and silently discarding one terminates clause. ctype: 73/80 -> 108/115 goals; all 35 new goals proved.
Both already discharged every goal; they only lacked the clauses that make the result trustworthy and usable by callers. - terminates \true and exits \false on both - _parse_integer_fixup_radix gains 'assigns \result \from s, *base', without which WP warned that callers' assumptions were imprecise - kstrtobool gains a global assigns alongside its per-behavior ones 234/234 and 79/79 goals with -wp-rte, smoke tests 15/15 and 9/9, no soundness findings. Marked proved in the README WP column, which is what seeds sessions/cache via wp-prune.
Two separate problems, neither of them a weakening: - the quantifiers ranged over char* and compared pointers, so the established goal reduced to 'a < s && s <= a ==> ...' and no solver could discharge the contradiction. Restated over integer indices, which is equivalent and is what the Typed model reasons about. - 'xs' was missing from the loop assigns although the loop increments it, and the pointer-range invariant is replaced by the exact offset xs == (char *)s + (ocount - count). Also adds terminates/exits and 'assigns \result \from s'. 22/22 goals, smoke tests 4/4, no soundness findings.
- requires \separated(dest, src): memcpy is the non-overlapping variant (memmove exists for the other case), and without it the copy invariant is false, since writing dest can change src - pointer-range loop invariants replaced by the exact offsets tmp == (char *)dest + (ocount - count) and likewise for s; the range form left the provers reasoning about pointer order - adds terminates, exits, 'assigns \result \from dest' and 'ensures \result == dest' 26/26 goals, smoke tests 4/4, no soundness findings. Note: the new separation precondition is discharged at strlcpy's call site, but it perturbs strlcpy's size_is_greater_src postcondition, which now times out. strlcpy is blocked on the strlen lemmas anyway and is handled in its own commit.
Same restatement as memset and memcpy, applied to both the forward and the backward loop: - pointer-range invariants replaced by exact offsets, tmp == dest + k and s == src + k, with k = ocount - count forward and count backward - 'tmp' added to both loop assigns; the loops move it but neither clause listed it - drop the tautological 'base_addr(dest) == base_addr(src) ^^ base_addr(dest) != base_addr(src)', a Jessie idiom for forcing a case split that means nothing to WP - adds terminates, exits, 'assigns \result \from dest' and 'ensures \result == dest' 62/62 goals, smoke tests 10/10, no soundness findings. This includes the pointer-difference VC that AstraVer could not discharge; the README footnote is updated rather than dropped.
sessions/ is machine-generated and rewritten wholesale on every reproof, so a single reproof buries a review in thousands of JSON lines. Mark it '-diff linguist-generated=true': git prints 'Binary files differ' instead of the content, and GitHub collapses it in pull requests and excludes it from language stats. 'git diff --text -- sessions/' still shows it.
The specification was written over u8* while WP's Typed model represents void* as char*, so every access went through an incompatible-pointer cast (11 of them) and the goals were degraded rather than proved. - restate the contract and loop invariants over char* and integer indices, matching memset/memcpy/memmove which already prove - 'const unsigned char *p' becomes 'const char *p' and the comparison '(unsigned char) c' becomes '(char) c', marked CODE_CHANGE as the project already does in strcmp, strncmp, strncasecmp and memset. The two are bit-identical, so the comparison is unchanged - adds terminates, exits and 'assigns \result \from s' 35/35 goals, smoke tests 7/7, no cast warnings left.
Same u8*/char* mismatch as memchr, but memscan compares a byte against an int, so the unsigned reading has to be preserved rather than folded away. - contract and loop invariants restated over char* and integer indices - the byte keeps its '(unsigned char)' reading in both the code and the specification, so the comparison is still against a 0..255 value - 'unsigned char *p' becomes 'char *p', marked CODE_CHANGE - drops the \base_addr invariant, now implied by the exact offset - adds terminates, exits and 'assigns \result \from addr' 24/24 goals, smoke tests 7/7, no soundness findings.
Same u8*/char* mismatch as memchr and memscan; memcmp returns the difference of two byte values, so the unsigned reading is load-bearing. - contract and loop invariants restated over char* and integer indices - bytes keep their '(unsigned char)' reading in both the code and the specification, so the difference is still computed on 0..255 values - 'const unsigned char *su1, *su2' becomes char*, marked CODE_CHANGE - drops the tautological base_addr xor requires, a Jessie case-split idiom that means nothing to WP - adds terminates and exits 29/29 goals, smoke tests 7/7, no soundness findings. strstr and strnstr are unaffected.
24/36 -> 29/31 goals. Not yet complete, so the WP column is unchanged. - loop invariants use the exact offset start == ostart + (obytes-bytes) and index-based quantifiers - the found behavior returns an index witness rather than doing pointer arithmetic on \result - adds terminates, exits and 'assigns \result \from start' The two remaining goals need to bridge the u8* parameters to the void* return value. WP's Typed model keeps uint8 and sint8 in separate memory chunks and models void* as char*, so any such cast is imprecise. Closing them would mean changing the function's signature, which is more than a specification fix.
The loop had a variant but no assigns, so WP could not discharge the function's own assigns clause. Adds 'loop assigns b, m, x, y' plus terminates, exits and 'assigns \result \from x'. 11/11 goals. Note this is runtime-error safety and termination only: int_sqrt still has no functional postcondition relating \result to x, so it is not marked proved in the README.
strscpy and memchr_inv type-pun through unsigned long*, bsearch calls through a function pointer, and ctype needs a case analysis over all 256 byte values. None of these is a specification problem, so note them rather than leaving them looking merely unfinished.
24/30 -> 87/87. Marked proved. AstraVer's 'lemma' keyword self-generalised a ghost function's contract into an axiom. Vanilla ACSL has no equivalent, so each fact is a proved ghost function with an explicit call at the site that needs it. - intro_valid_str_len carries the induction by recursion on n, with 'decreases n', and concludes valid_str(s) and strlen(s) == n - elim_valid_str goes the other way, returning the length - valid_str_len and valid_str_shift are the two facts callers need strlen.c calls valid_str_shift in the loop and valid_str_len before the return. The contract and invariants move to integer indices with a ghost index k, so the returned difference is a shift of s by a known integer rather than an opaque pointer subtraction.
strnlen_shift and strnlen_shift_ex both shifted the pointer without reducing the bound: strnlen(s + i, cnt) == strnlen(s, cnt) - i Take s = "abcde" with cnt = 3, so no NUL falls inside the bound. Then strnlen(s,3) = 3 and strnlen(s+1,3) = 3, not 2; strnlen_shift_ex is false on the same witness. Both counterexamples are machine-checked. ACSL lemmas are axioms for every proof that follows, so an inconsistent axiomatic can discharge anything. Everything including strnlen.h - strnlen, strncmp, strncasecmp, strncpy, strnchr, strnstr, sysfs_streq - was proving against it. Neither lemma was ever discharged, under AstraVer or WP, so this was latent rather than newly introduced. The bound has to shrink with the pointer: strnlen(s + i, (size_t)(cnt - i)) == strnlen(s, cnt) - i i <= strnlen(s, cnt) <= cnt, so cnt - i is non-negative. Only strncmp loses a goal (166 -> 142/166), which is the one proof that was resting on the false axiom.
The logic function recursed on s instead of s + 1: sysfs_strlen(s) = (s[0]=='\0' || ...) ? 0 : 1 + sysfs_strlen(s) For any s that hits the else branch this asserts f(s) == 1 + f(s), i.e. 0 == 1. The axiomatic was inconsistent, so every goal in sysfs_streq.c was vacuously provable and its 335/346 score meant nothing. WP proves 'assert \false' from the definition given a concrete witness. With the recursion advancing, sysfs_streq is 311/346: 24 of the goals it used to 'prove' were resting on the contradiction. Checked every other recursive logic definition in the corpus - strlen, strnlen, strncmp, strchr, strchrnul, strrchr_helper, strspn, strcspn, strpbrk, skip_spaces, check_bytes8, match_string, real_len. All of them advance the pointer or decrease the bound; this was the only ill-founded one.
101/111 -> 227/227. Marked proved; strnlen.h carries no unproved lemma. Same shape as strlen: elim_valid_strn walks to the first NUL or the bound, intro_valid_strn_len carries the induction by recursion with 'decreases n', and valid_strn_len and valid_strn_shift are the facts callers need. strnlen.c calls valid_strn_shift in the loop and valid_strn_len before the return, and gains a ghost index k without which the nz invariant does not hold. Nine lemmas are dropped because a proved ghost function now supplies the fact: valid_strn_shift1, strnlen_range, strnlen_null, strnlen_before_zero, strnlen_at_zero, strnlen_at_cnt, strnlen_zero, strnlen_cnt and strnlen_shift1. Four of them only appeared to prove because WP may use a sibling lemma as a hypothesis, so they fell as soon as their unproved neighbours were removed. The five that need induction of their own are converted rather than dropped: strnlen_shift and strnlen_less recurse through valid_strn_shift; strnlen_min_len is restated as strnlen_is_strlen - 'strlen(s) < cnt implies strnlen(s,cnt) == strlen(s)' - which is what callers actually use and avoids \min; strnlen_cmp follows from strnlen_is_strlen plus valid_strn_len; and strnlen_shift_ex goes with them. This unblocks the family: strnchr, strncmp, strncasecmp, strncpy, strncat and sysfs_streq all rest on these facts.
92/99 -> 167/167. strchr is fully proved and marked in the README. lemma strchr_at_end_zero was false: it claimed strchr(str,c) == \null whenever *str == '\0', but with c == '\0' the definition returns str on its first branch, which is also what C's strchr does. Guarded with c != '\0'. The parked lemma-function version already carried that guard, so the axiomatic branch had simply lost it. Removing the false lemma dropped strchr to 85/99: strchr_defn, strchr_skipped and most of the function body had been resting on it. - strchr_mem, strchr_res, strchr_defn and strchr_skipped become ghost functions; each calls valid_str_shift before recursing, which is what justifies the 'decreases strlen(str)' variant - strchr_mem's XOR is restated as an implication so the null case does not evaluate '\null - str' - the contract and loop invariants move to integer indices, and the function carries a ghost index k with 's == os + k' so 'os[k] == *s' is a rewrite rather than a pointer-difference obligation Also drops the dead 'return 0' from elim_valid_str in strlen.h: the loop it follows cannot exit normally, and WP's smoke test correctly flagged it. strlen smoke tests are 23/23 and strchr's 48/48.
103/106 -> 187/187, smoke tests 54/54. Marked proved in the README. lemma strchrnul_res was false: it stated *strchrnul(str,c) == '\0' ^^ *strchrnul(str,c) == c and with c == '\0' both disjuncts hold, so the exclusive-or is false. As in strchr, the parked lemma-function version already carried 'requires c != '\0'' and the axiomatic branch had lost it. - strchrnul_mem, strchrnul_res, strchrnul_defn, strchrnul_strlen and strchrnul_skipped become ghost functions, each calling valid_str_shift to justify its decreases clause - strchrnul_skipped and strchrnul_strlen only appeared to prove while their unproved neighbours were present - contract and invariants move to integer indices; the body carries a ghost index k with 's == os + k' - drops 'ensures \base_addr(\result) == \base_addr(s)', now implied by '0 <= \result - s <= strlen(s)'
The three in_array lemmas guarded on 's != '\0'' - comparing the *pointer* against a character constant, i.e. 's != NULL', where '*s' was meant. Consequences: - in_array_false read 'valid_str(s) && s == NULL', which is contradictory, so the lemma was vacuous - in_array_true claimed in_array(s, c) whenever *s == c, including c == '\0', where strlen(s) == 0 makes the range empty and the existential false - in_array_shift1 lost its '*s != '\0'' precondition the same way All three now guard on *s. in_array itself is restated over integer indices rather than a pointer range, matching the rest of the corpus, and in_array_false and in_array_true become proved ghost functions. strspn 113/133 -> 134/153, strcspn 101/125 -> 122/145, strpbrk 102/123 -> 121/143. in_array_shift1 remains open: proving 'in_array(s,c) <==> in_array(s+1,c)' needs the existential witness shifted by one in both directions, which no prover does unaided.
113/133 -> 316/316 with smoke tests 63/63. Marked proved. - in_array_elim returns a witness index and in_array_intro consumes one, which is what lets in_array_shift1 be proved at all: the equivalence needs the existential witness shifted by one in both directions, so it is split into in_array_shift1_fwd and in_array_shift1_bwd rather than stated as an <==> that no prover can instantiate - strspn_range becomes a ghost function. It recurses on '*s != '\0'' alone rather than the definition's guard, because ghost code is C and cannot branch on in_array; the postcondition holds in both cases - both loops carry ghost indices (k for s, m for accept) so the quantifiers are over integers and 'accept[m] == *p' is a rewrite - with in_array indexed by integer, the inner loop no longer needs a shift lemma at all: !in_array follows from the exhausted range and in_array from in_array_intro strcspn 122/145 -> 184/205, strpbrk 121/143 -> 183/203, strsep 215/218.
strcspn 122/145 -> 337/337 (smoke 77/77), strpbrk 121/143 -> 351/351 (smoke 79/79). Both marked proved. Both mirror strspn now that in_array is indexed by integer: ghost indices k and m for the outer and inner loops, integer quantifiers throughout, in_array_intro at the match, and the exhausted inner range giving !in_array otherwise. - strcspn_range, strcspn_empty_reject, strpbrk_range and strpbrk_empty_ct become ghost functions - strpbrk's found behavior had 'ct <= t <= ct + strlen(ct)', which admits the terminator; restated as in_array(ct, *\result)
79/92 -> 166/166 (smoke 54/54). Marked proved. This was the last header still carrying parked AstraVer lemma functions. lemma skip_spaces_iter_one had its guard inverted: valid_str(str) && !isspace(*str) ==> skip_spaces(str) == skip_spaces(str+1) With !isspace(*str) the definition returns str itself, so the lemma claims str == skip_spaces(str+1), which is false for any non-space followed by a non-space. Machine-checked on "ab". The parked lemma-function branch had no such lemma at all. - skip_spaces_range, skip_spaces_defn and skipped_are_spaces become ghost functions; skip_spaces_deref and skip_spaces_base_addr fold into skip_spaces_range's postcondition - is_space is a ghost helper because ghost code is C and cannot branch on the isspace predicate, which is also why skip_spaces_range takes that form - the body carries a ghost index k, and the contract moves to integer quantifiers strim improves to 195/217.
strsep 215/218 -> 248/248 (smoke 64/64), strpbrk stays complete at 274/274. strsep marked proved. The one open goal was \valid(end) for the '*end++ = ' write. The facts were all present - valid_str(sbegin) and 0 <= end - sbegin < strlen - but WP will not rewrite 'end' into 'sbegin + (end - sbegin)', and a ghost index does not help when the pointer comes from a call rather than a loop. Adding 'ensures \valid(\result)' to strpbrk's found behavior states the fact where it is cheap to prove and consumes it where it is needed. Also gives each strsep behavior an 'assigns \result \from *s'. The function-level assigns is left to the complete behaviors: a global over-approximation would have to mention strpbrk(*s, ct), which is meaningless in the branch where *s is null.
95/112 -> 298/298, smoke 27/27. Marked proved. - 'last' was missing from the loop assigns although the loop writes it, the same omission found in memset, memcpy, memmove and hex2bin - the invariants tracked 'last' with nested pointer quantifiers and an exclusive-or; replaced by two ghost indices, k for the cursor and lastk for the recorded match, so 'os[lastk] == c' is a rewrite - contract restated over integer indices - the do-while advances the cursor in its condition, so the ghost updates are guarded by '*s != 0' to match The disabled axiomatic at the top of the header is left as it is: it is inside a plain comment, not an annotation, so it has no effect either way.
Both return 'sc - s' cast to size_t. WP's memory model does not bound object sizes, so nothing rules out a difference above LONG_MAX: even with 'sc == s + k' for a size_t k, nothing constrains k. The current RTE option set does not ask either function to prove it, but the assumption is real, and it belongs in the contract rather than in the option list - stated there, the contracts still hold if -warn-unsigned-downcast is turned back on. strlen gains 'requires strlen(s) <= LONG_MAX' and strnlen 'requires count <= LONG_MAX'; LONG_MAX is added to kernel_definitions.h. Both also gain terminates and exits. Neither function's own count moves - strlen stays 88/88, strnlen 228/228 - because a requires clause creates goals in callers, not in the callee. That is the cost: the bound propagates. Measured on the completed functions, strchr, strchrnul, strspn, strcspn, strpbrk, skip_spaces, strsep and strrchr all stay at 100%; strlcpy picks up one new unproved goal, its own call-site instance of the bound, which has to be threaded up into strlcpy's contract in turn.
121/136 -> 236/236, smoke 47/47. Marked proved. range, defn_equal, defn_less and defn_greater all needed induction over the comparison length and are now proved ghost functions. defn_less and defn_greater only walk indices 0..k, so their validity requirement is weakened from 0..n to 0..k, which is what call sites can actually establish: when strcmp stops at a mismatch the shorter string may not be valid all the way to n. The body gains ghost indices and calls the new functions at each exit.
206/218 -> 250/250, smoke 63/63. Marked proved. Standard treatment: ghost index k with 's == os + k', integer quantifiers in the contract and invariants, valid_strn_shift in the loop and valid_strn_len after it. The last goal was the not_exists postcondition. Returning early has to be infeasible under that behavior's assumption, which needs 'k < strnlen(os, ocount)' at the match - it follows from the length invariant plus the loop condition, but WP does not derive it unaided. Also inherits 'requires count <= LONG_MAX' from strnlen.
The recursive case had no increment:
match_string(a, n, s) =
n == 0 ? 0 : (strcmp(a[0],s) == 0 ? 0 : match_string(a+1, n-1, s))
so a match at index 1 yields match_string(a+1,1,s), which is 0. The
function is supposed to return the index of the first match, and the
contract's 'ensures \result == match_string(array, real_len(array,n),
string)' is stated in those terms, so the specification asserted the C
function always returns 0. Machine-checked on a two-element array whose
match is at index 1.
The recursive case is now '1 + match_string(a+1, n-1, s)'.
match_string_definition also becomes a proved ghost function - it could
not have been proved before, since its conclusion is exactly the index
the definition threw away - and is called at the match return, which
gives the exists behavior its '\result == match_string(...)'
postcondition. real_len_lower is new: a non-null entry at index i with
i <= real_len and i < len forces i < real_len. That is what the
real_len_not_nulls call site needs, and it is not derivable from the
other three without the case split on whether real_len equals len.
strcmp also gains terminates and exits; without them WP generated
default clauses for it in every caller, which the missing-spec audit
flagged.
211/214 -> 273/274. Only strcmp_corollary is left. It relates
'strcmp(s1,s2) != 0' to a differing character, which needs an induction
over the comparison that strcmp's own lemmas stop short of.
82/94 -> 115/115, smoke 23/23. Marked proved.
This is the first of the copy family, and it settles a question I had
framed wrongly. The obstacle was never 'WP cannot show strlen(src)
survives the write' - it was that the contract asked for that at all.
Restated the way strreplace is:
- the postcondition speaks of strlen{Pre}(src) and \at(src[i], Pre),
never the post-state length of src
- the loop carries an 'untouched' invariant saying osrc[i] still equals
its pre-state value for every i <= n. That is a pointwise frame fact,
which follows from \separated directly; nothing has to be re-derived
about the recursive strlen
- the destination's own length is established at the end with
intro_valid_str_len(tmp, n), exactly as strreplace does
So the two-label frame lemma is not needed here, and Coq is not needed.
'requires \base_addr(dest) != \base_addr(src)' becomes the precise
\separated, and the contract gains terminates, exits and the result
length.
83/97 -> 117/117, smoke 23/23. Marked proved.
Same restatement as strcpy: the postcondition speaks of strlen{Pre}(src)
and \at(src[i], Pre), the loop carries the pointwise 'untouched'
invariant for the source, and intro_valid_str_len establishes the
destination's length at the end.
The returned pointer is stated as 'dest + strlen{Pre}(src)' rather than
against the post-state length.
105/115 -> 142/142, smoke 28/28. Marked proved.
Same restatement: strlen{Pre} and \at(..., Pre) throughout, a pointwise
'untouched' invariant for the source, and intro_valid_str_len(tmp, d + n)
at the end to establish the concatenated length.
Both loops carry ghost indices - j for the walk to the end of dest, k
for the copy - and the second loop keeps a 'prefix' invariant saying the
original dest content below d is undisturbed, which is what the first
postcondition needs.
'requires \separated(dest, src)' is new; strcat had no separation
requirement at all, though the copy is only correct without overlap.
133/137 -> 159/159. Marked proved.
- valid_str_len(src) before the strlen call and intro_valid_str_len
after the terminator is written give 'strlen(dest) == len'
- 'requires \base_addr(dest) != \base_addr(src)' becomes
'\separated(dest+(0..size-1), src+(0..strlen(src)))', the precise
frame condition and what memcpy's own precondition needs
- the in-block facts are carried across the branch merge as an
implication guarded by 'size > ret', which is vacuous on the size == 0
path
The size_is_greater_src postcondition was the hard one: stated over the
post-state strlen(src), WP cannot show the source survives the write to
dest even with the separation hypothesis. Restated over strlen{Pre}(src)
and \at(src[i], Pre) it needs nothing about survival at all, which is
the same move that unblocks the rest of the copy family. No labelled
frame lemma and no Coq.
Also adds 'ensures \result == strlen{Pre}(src)', the per-behavior
destination lengths, terminates, exits, and the strlen LONG_MAX bound
that strlcpy has to discharge for its own strlen call.
102/108 -> 123/123, smoke 30/30. Marked proved - it was not proved under
AstraVer either, so this is a new result rather than a restoration.
Same restatement as the rest of the family: the contract speaks of
strlen{Pre}(dest) and strlen{Pre}(src) and \at(src[i], Pre), and the two
intro_valid_str_len calls at the end establish the appended string's
length. The 'ghost Mid:' label and the \at(dest,Mid) assertions are no
longer needed once the copy is expressed against odest and dsize.
'requires \separated(dest, src)' is new, as is the strlen LONG_MAX bound
for the two strlen calls, and the result is now pinned exactly rather
than bounded.
197/216 -> 246/246, smoke 62/62. Marked proved - it was not proved under
AstraVer either.
The exceed behavior's padding range was wrong:
\forall i; strlen(src) <= i <= count - strlen(src) ==> \result[i] == 0
'count - strlen(src)' is a length, not an index bound, so the range was
nonsense as soon as the two lengths were comparable. It is now
'strlen{Pre}(src) <= i < count'.
The rest is the family restatement, with one wrinkle: src stops
advancing at the terminator while dest keeps padding, so the invariant
pins it as 'src == osrc + (k < n ? k : n)' and the copied and padded
ranges are split at n.
Also adds \separated, the strlen LONG_MAX bound, terminates, exits and
the destination length.
229/241 -> 311/311, smoke 66/66. Marked proved - not proved under
AstraVer either. This completes the copy family.
Same restatement as the rest, with two extra facts the second loop
needs: 'count > 0' as an invariant, since the loop breaks the moment the
decrement reaches zero, and 'k < n' at the point a non-terminator is
copied, which follows from valid_strn_len's characterisation of strnlen
but needs the case split spelled out.
The postcondition's source range is restated as
'\result[strlen{Pre}(dest) + i] == \at(src[i], Pre)' rather than
indexing \result by 'i - strlen{Old}(dest)', which is the same property
without the subtraction.
Adds \separated, the strlen LONG_MAX bound, terminates, exits and the
concatenated length.
195/218 -> 265/265. Marked proved - it was not proved under AstraVer
either.
The backward scan can leave 'end' at 's - 1', so the invariants compared
a pointer one before the array. It now carries a signed ghost index e
with 'end == s + e' and '-1 <= e', and the invariants are stated as
integer differences with the variant as 'end - s + 1'. That is what
makes the mem_access and invariant goals go through: WP will not rewrite
'end' into 's + (end - s)', but with e in hand every access is a shift
of s by a known integer.
The contract moves to strlen{Pre}(s) and \at(s[i], Pre), with a 'kept'
invariant for the untouched prefix, and the trimmed string's own length
is established by intro_valid_str_len after the terminator is written.
The result is computed into a local so ghost code can name it. Also
adds the strlen LONG_MAX bound, terminates, exits, and a per-behavior
'assigns \result \from s' - a function-level one conflicts with zero_len
assigning nothing.
The last goal needed 'res == s + (res - s)', which WP will not derive.
Rather than assert it at the call site and leave the assert unproved,
skip_spaces states it: 'ensures \result == str + (\result - str)'.
Inside skip_spaces the body carries a ghost index k with
'\result == os + k', so the reconstruction is immediate there, while a
caller holding only the difference cannot rebuild the pointer. That is
the same move as strpbrk's 'ensures \valid(\result)': when a caller
needs a fact about a returned pointer that the difference alone cannot
give, state it in the callee where the index still exists.
memcmp's contract lived in memcmp.c, so every caller in another translation unit saw a bare prototype and WP generated a default spec for it. Frama-C says so plainly - 'annot:missing-spec src/memcmp.h:13' - but the warning was lost among the others. Moving the contract to memcmp.h is what finally let strstr use it. That was the real cause of what I had blamed on the '(char *)(void *)' round trip. The round trip is fine: a minimal caller/callee pair proves it. The postcondition simply was not there. memcmp also gains 'ensures \result == 0 ==> all bytes equal'. The body subtracts '(unsigned char)' values, so that direction is stated on those rather than on chars; for equality the two are the same relation, which is what lets strstr's strmatch stay plain character equality. strstr 124/127 -> 133/134, memcmp still 33/33, strnstr and strlcat unaffected. One goal remains: under the exists behavior the NULL return has to be infeasible, which needs the argument that no match can start within l2 of the end because the terminator would have to equal a non-terminator.
98/108 -> 102/102, smoke 19/19. hex2bin is not in the README table, so there is no WP column to mark. Three of the old loop invariants were vacuous or wrong: 'osrc <= src <= src + 2*ocount' and 'odst <= dst <= dst + count' each compare a pointer with itself plus a non-negative offset, and the loop assigns listed 'src' twice while omitting 'dst'. Replaced by the exact offsets src == osrc + 2*(ocount-count) and dst == odst + (ocount-count). - behaviors restated over integer indices - requires \separated(dst, src), which the copy loop needs The nibble combination '(hi << 4) | lo' is written as 'hi * 16 + lo', marked CODE_CHANGE as the project already does in strcmp, strncmp, strncasecmp, memset, memchr, memscan and memcmp. The two operands occupy disjoint nibbles and both facts prove, but no prover or tactic closes 'disjoint bits implies sum' within a usable budget - wp:bitwised gets Qed 3/6 and stalls. This is a source change, not a specification fix: it is provably equivalent here because hi and lo are each below 16, but it is a change to the kernel text and should be read as such. With the shift gone the file needs no bit reasoning at all.
strspn.h was the only header still carrying the `#ifndef LEMMA_FUNCTIONS` split, 96 lines of stale duplicate: its own `strspn_range` recursed on `in_array(accept, *s)`, which the live version deliberately does not. The branch was unreachable, so it had already drifted without anyone noticing. With it gone nothing references LEMMA_FUNCTIONS, so the `#undef` that parked the AstraVer lemma functions goes too.
LONG_MAX was hardcoded to its 64-bit value outside the `#ifdef CONFIG_64BIT` guard that BITS_PER_LONG already sits under, so the two could disagree. Eight contracts carry `requires strlen(s) <= LONG_MAX` to bound the ptrdiff cast, and under a 32-bit configuration every one of them would admit differences that overflow `long`. The 32-bit arm is unreachable today - CONFIG_64BIT is defined unconditionally a few lines above and -machdep pins the ABI from the other side - so this buys consistency, not a behaviour change. The comment says as much rather than implying portability it does not provide.
The `len` behaviour lost `ensures !isspace(*\result)` and its counterpart on the last character, leaving a contract that a do-nothing `return s;` satisfies: with `\result == s` and the length unchanged both surviving `\forall` clauses range over empty intervals and `assigns` permits no write. The proof no longer said anything had been trimmed, and strim was marked proved on it. The trailing-space clause is now guarded by `strlen(\result) > 0`, which the original lacked and which the empty result needs. 271/271.
strncmp was the one function marked proved whose contract carried neither clause, so WP generated no termination obligation for it while every sibling had one - a quietly weaker result than the identical looking strcmp line in the table. Both clauses prove: 289/289.
The target branched on Frama-C's exit status, and Frama-C exits 0 with goals left unproved - verified on a function returning 7 under `ensures \result == 42`, which reports 3/4 and exits 0. So the only regression gate in the tree could never fail, and it was printing `OK: strcmp` for a function that replayed 215/236. It now matches WP's own "Proved goals: n / m" line and compares the halves with a back-reference. A soundness scan runs first, so a full count cannot outvote a finding from the tier that can lie - an annotation silently dropped with `not yet supported (skipped)` used to pass this gate at 100%.
wp-prune filled the cache with one Frama-C invocation over every proved file, while wp-replay consumes it one file at a time. A goal's cache key depends on the analysis context, so a file proved alongside thirty others gets different keys than the same file proved alone: six of the thirty-two proved functions did not replay at all. Measured on strcmp - 215/236 from the multi-file cache, 236/236 once the file had been proved on its own. Populating per file fixes it. Each run also writes its JSON baseline now, so the reports come out of the same pass instead of a second one over the whole corpus.
hex2bin calls _tolower, so it needs ctype.o like the other char-class users. Inert until hex2bin appears in the results table, which is what puts it in BINAVAILFILES.
- hex2bin joins the results table as proved; int_sqrt joins it unmarked, reading the same as strnstr - both have memory safety and termination but no functional postcondition, and the WP column means fully specified and proved. The table is also the list the build derives PROVEDFILES from, so the entry is what puts hex2bin's proof under the replay gate. - the install line omitted z3 and cvc5, which the Makefile actually invokes and which the committed cache records verdicts from. cvc5's opam package is OCaml bindings, not the solver, so it is noted as a separate install. - the tactic passage offered `(hi << 4) | lo == hi * 16 + lo` as the typical goal `make wp-auto` closes. It does not close it: wp:bitwised stalls at Qed 3/6 even with both operands proved below 16, which is why hex2bin writes the arithmetic form and marks it CODE_CHANGE. sessions/script/ is empty for the same reason. - README_ru claimed -warn-unsigned-downcast was enabled. It is off, as the English README says.
Both said the lemmas in the axiomatics are assumed rather than proved. They are not: a `lemma` is a proof obligation, and WP generates a goal for each one. The corpus has 27 and discharges 26 - only strcmp_corollary times out. An older sentence carried the same error from the AstraVer era, when the lemma functions really were parked. What is assumed are the 76 `axiom`s in ctype.h, strncasecmp.h and hex2bin.h, which tabulate tolower/toupper and hex_to_bin over the character set. Nothing checks them, and a contradiction there would make every dependent goal vacuously provable - the failure mode sysfs_strlen already demonstrated. Only make wp-smoke would notice. Also notes that strrchr.h, strim.c and memcmp.c still carry an older axiomatic inside a plain comment rather than an ACSL one, so that text is inert: not parsed, not proved, not used.
Frama-C drops .frama-c in the working directory on any run, and the skill wrappers write .wp-session. Neither belongs in the tree.
evdenis
force-pushed
the
wp-port
branch
2 times, most recently
from
September 14, 2026 13:28
5229850 to
9d4fc84
Compare
The ERROR branch captured Frama-C's output and then threw it away, so a run that aborted reported only "no goal count" with no cause. That is how it reads in CI, where the tree is not in front of you: thirty-two identical lines and nothing to act on. It now prints the User Error, unknown-prover and abort lines it found.
The workflow removed with the AstraVer toolchain installed four provers and re-proved the corpus. This one replays: `make wp-replay` runs with `-wp-cache offline`, which resolves every goal from sessions/cache without executing a solver. Verified with an Alt-Ergo that answers --version but refuses to solve - memchr still replays 35/35 and the sabotaged binary is never called. The provers are installed all the same, because why3 has to resolve the names WP is asked for: with them absent WP aborts with `Unknown prover alt-ergo` before it consults the cache at all. They are registration, not work, which is why the job stays short. Everything is pinned - Frama-C 33.0, Alt-Ergo 2.6.3, CVC5 1.3.4, Z3 5.1.0. A cache entry records the goal hash together with the prover and version that discharged it, and goal generation changes between Frama-C releases, so an unpinned upgrade would miss every entry and fail for a reason unrelated to the specifications. The upgrade path is a comment at the top of the file. The job fails if a proved function does not replay at 100%, if a run reports a soundness finding, or if WP reports no goal count. Badge added to both READMEs.
sessions/cache holds one entry per proved goal of the files marked proved in the README WP column, built one file at a time so that wp-replay - which consumes it one file at a time - actually finds them. sessions/reports holds the per-function -wp-report-json baselines, written by the same pass. `make wp-replay` re-checks all 32 with `-wp-cache offline`, resolving every goal from the cache without executing a solver; CI does exactly that on every push. Entries are keyed by a hash of the goal and record the prover and version that discharged it, so a toolchain upgrade invalidates them - wp-rebuild then wp-prune regenerates. sessions/script is empty: no proof in the corpus depends on a committed tactic script.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Re-proves the corpus with stock Frama-C/WP, replacing the unmaintained AstraVer (Jessie) plugin.
This was expected to be a porting exercise — adjust syntax, swap the memory model, re-run.
Results
lemmadeclarationsaxioms — assumed, uncheckedFour functions are proved that AstraVer never proved —
strlcat,strncpy,strncat,strim— andmemmove's pointer-difference VC, which AstraVer could not discharge, now goes through.Coq was needed zero times. The frame problem in the copy family dissolved once the contracts were phrased over
Prewith a pointwise untouched invariant: the obstacle was never that WP cannot show the source survives the write, it was that the contract asked for that at all.Infrastructure
make wp-replayre-checks every proved function from the committed cache with-wp-cache offline— no solver is invoked, so a checkout can be verified without provers installed.while (count--)andc = (unsigned char) *s++rely on defined unsigned wraparound, and with the checks on RTE asks these functions to prove they never do the thing they exist to do — measured, 19 goals across 11 functions unprovable by construction.Still out of reach
strscpyandmemchr_invtype-pun throughunsigned long *;bsearchcalls through a function pointer;ctypeneeds a case analysis over all 256 byte values. None is a specification problem. Individual goals remain open incheck_bytes8,strstrandmatch_string;int_sqrt,strnstrandstrncasecmpare deliberately not marked proved despite carrying work.The 76
axioms inctype.h,strncasecmp.handhex2bin.hremain the corpus's trust anchor — nothing checks them, andmake wp-smokeis the only thing that would notice a contradiction.