[Libc] Fix specs in wchar.h

share/libc/__fc_string_axiomatic.h

@@ -171,6 +171,21 @@ __BEGIN_DECLS
   @ }
   @*/
 
+/*@ axiomatic WMemChr {
+  @ logic 𝔹 wmemchr{L}(wchar_t *s, wchar_t c, ℤ n)
+  @   reads s[0..n - 1];
+  @ // Returns [true] iff wide char array [s] contains wide character [c]
+  @
+  @ logic ℤ wmemchr_off{L}(wchar_t *s, wchar_t c, ℤ n)
+  @   reads s[0..n - 1];
+  @ // Returns the offset at which [c] appears in [s].
+  @
+  @ axiom wmemchr_def{L}:
+  @   \forall wchar_t *s; \forall wchar_t c; \forall ℤ n;
+  @      wmemchr(s,c,n) <==> \exists int i; 0 <= i < n && s[i] == c;
+  @ }
+  @*/
+
 /*@ axiomatic WcsLen {
   @ logic ℤ wcslen{L}(wchar_t *s)
   @   reads s[0..];

share/libc/wchar.h

@@ -41,6 +41,8 @@ __PUSH_FC_STDLIB
 // ISO C requires the tag 'struct tm' (as declared in <time.h>) to be declared.
 #include "time.h"
 
+#include "string.h"
+
 __BEGIN_DECLS
 
 #ifndef WEOF
@@ -48,16 +50,35 @@ __BEGIN_DECLS
 #endif
 
 /*@
+  requires valid:
+    valid_read_or_empty((char*)s, (size_t)(sizeof(wchar_t)*n))
+    || \valid_read(((unsigned char*)s)+(0..wmemchr_off(s,c,n)));
+  @ requires initialization:
+        \initialized(s+(0..n - 1))
+     || \initialized(s+(0..wmemchr_off(s,c,n)));
+  @ requires danglingness:
+        non_escaping(s, (size_t)(sizeof(wchar_t)*n))
+     || non_escaping(s, (size_t)(sizeof(wchar_t)*(wmemchr_off(s,c,n)+1)));
   assigns \result \from s, indirect:s[0 .. n-1], indirect:c, indirect:n;
   ensures result_null_or_inside_s:
     \result == \null || \subset (\result, s+(0 .. n-1));
  */
 extern wchar_t * wmemchr(const wchar_t *s, wchar_t c, size_t n);
 
-/*@ assigns \result \from indirect:s1[0 .. n-1], indirect:s2[0 .. n-1], indirect:n; */
+/*@
+  requires valid_s1: valid_read_or_empty(s1, (size_t)(sizeof(wchar_t)*n));
+  requires valid_s2: valid_read_or_empty(s2, (size_t)(sizeof(wchar_t)*n));
+  requires initialization:s1: \initialized(s1+(0..n-1));
+  requires initialization:s2: \initialized(s2+(0..n-1));
+  requires danglingness:s1: non_escaping(s1, (size_t)(sizeof(wchar_t)*n));
+  requires danglingness:s2: non_escaping(s2, (size_t)(sizeof(wchar_t)*n));
+  assigns \result \from indirect:s1[0 .. n-1], indirect:s2[0 .. n-1], indirect:n;
+*/
 extern int wmemcmp(const wchar_t *s1, const wchar_t *s2, size_t n);
 
 /*@
+  requires valid_dest: valid_or_empty(dest, (size_t)(sizeof(wchar_t)*n));
+  requires valid_src: valid_read_or_empty(src, (size_t)(sizeof(wchar_t)*n));
   requires separation:dest:src: \separated(dest+(0 .. n-1), src+(0 .. n-1));
   assigns dest[0 .. n-1] \from src[0 .. n-1], indirect:src, indirect:n;
   assigns \result \from dest;
@@ -66,6 +87,8 @@ extern int wmemcmp(const wchar_t *s1, const wchar_t *s2, size_t n);
 extern wchar_t * wmemcpy(wchar_t *restrict dest, const wchar_t *restrict src, size_t n);
 
 /*@
+  requires valid_src: \valid_read(src+(0..n-1));
+  requires valid_dest: \valid(dest+(0..n-1));
   assigns dest[0 .. n-1] \from src[0 .. n-1], indirect:src, indirect:n;
   assigns \result \from dest;
   ensures result_ptr: \result == dest;
@@ -73,6 +96,7 @@ extern wchar_t * wmemcpy(wchar_t *restrict dest, const wchar_t *restrict src, si
 extern wchar_t * wmemmove(wchar_t *dest, const wchar_t *src, size_t n);
 
 /*@
+  requires valid_wcs: \valid(wcs+(0..n-1));
   assigns wcs[0 .. n-1] \from wc, indirect:n;
   assigns \result \from wcs;
   ensures result_ptr: \result == wcs;
@@ -82,6 +106,10 @@ extern wchar_t * wmemmove(wchar_t *dest, const wchar_t *src, size_t n);
 extern wchar_t * wmemset(wchar_t *wcs, wchar_t wc, size_t n);
 
 /*@
+  requires valid_wstring_src: valid_read_wstring(src);
+  requires valid_wstring_dest: valid_wstring(dest);
+  requires room_for_concatenation: \valid(dest+(wcslen(dest)..wcslen(dest)+wcslen(src)));
+  requires separation:\separated(dest+(0..wcslen(dest)+wcslen(src)),src+(0..wcslen(src)));
   assigns dest[0 .. ] \from dest[0 .. ], indirect:dest, src[0 .. ], indirect:src;
   assigns \result \from dest;
   ensures result_ptr: \result == dest;
@@ -96,21 +124,36 @@ extern wchar_t * wcscat(wchar_t *restrict dest, const wchar_t *restrict src);
 */
 extern wchar_t * wcschr(const wchar_t *wcs, wchar_t wc);
 
-/*@ assigns \result \from indirect:s1[0 .. ], indirect:s2[0 .. ]; */
+/*@
+  requires valid_wstring_s1: valid_read_wstring(s1); // over-strong
+  requires valid_wstring_s2: valid_read_wstring(s2); // over-strong
+  assigns \result \from indirect:s1[0 .. ], indirect:s2[0 .. ];
+*/
 extern int wcscmp(const wchar_t *s1, const wchar_t *s2);
 
 /*@
-  assigns dest[0 .. ] \from src[0 .. ], indirect:src, dest[0 .. ], indirect:dest;
+  requires valid_wstring_src: valid_read_wstring(src);
+  requires room_wstring: \valid(dest+(0 .. wcslen(src)));
+  requires separation:\separated(dest+(0..wcslen(src)),src+(0..wcslen(src)));
+  assigns dest[0 .. wcslen(src)] \from src[0 .. wcslen(src)], indirect:src;
   assigns \result \from dest;
   ensures result_ptr: \result == dest;
  */
 extern wchar_t * wcscpy(wchar_t *restrict dest, const wchar_t *restrict src);
 
-/*@ assigns \result \from indirect:wcs[0 .. ], indirect:accept[0 .. ]; */
+/*@
+  requires valid_wstring_wcs: valid_read_wstring(wcs);
+  requires valid_wstring_accept: valid_read_wstring(accept);
+  assigns \result \from indirect:wcs[0 .. ], indirect:accept[0 .. ];
+ */
 extern size_t wcscspn(const wchar_t *wcs, const wchar_t *accept);
 
 // wcslcat is a BSD extension (non-C99, non-POSIX)
 /*@
+  requires valid_nwstring_src: valid_read_nwstring(src, n);
+  requires valid_wstring_dest: valid_wstring(dest);
+  requires room_for_concatenation: \valid(dest+(wcslen(dest)..wcslen(dest)+\min(wcslen(src), n)));
+  requires separation:\separated(dest+(0..wcslen(dest)+wcslen(src)),src+(0..wcslen(src)));
   assigns dest[0 .. ] \from dest[0 .. ], indirect:dest, src[0 .. n-1], indirect:src, indirect:n;
   assigns \result \from indirect:dest[0 .. ], indirect:src[0 .. n-1], indirect:n;
 */
@@ -118,6 +161,8 @@ extern size_t wcslcat(wchar_t *restrict dest, const wchar_t *restrict src, size_
 
 // wcslcpy is a BSD extension (non-C99, non-POSIX)
 /*@
+  requires valid_wstring_src: valid_read_wstring(src);
+  requires room_nwstring: \valid(dest+(0 .. n));
   requires separation:dest:src: \separated(dest+(0 .. n-1), src+(0 .. n-1));
   assigns dest[0 .. n-1] \from src[0 .. n-1], indirect:src, indirect:n;
   assigns \result \from indirect:dest[0 .. n-1], indirect:dest,
@@ -125,29 +170,45 @@ extern size_t wcslcat(wchar_t *restrict dest, const wchar_t *restrict src, size_
  */
 extern size_t wcslcpy(wchar_t *dest, const wchar_t *src, size_t n);
 
-/*@ requires valid_string_s: valid_read_wstring(s);
-  assigns \result \from indirect:s[0 .. ]; */
+/*@
+  requires valid_string_s: valid_read_wstring(s);
+  assigns \result \from indirect:s[0 .. wcslen(s)];
+  ensures result_is_length: \result == wcslen(s);
+ */
 extern size_t wcslen(const wchar_t *s);
 
 /*@
+  requires valid_nwstring_src: valid_read_nwstring(src, n);
+  requires valid_wstring_dest: valid_wstring(dest);
+  requires room_for_concatenation: \valid(dest+(wcslen(dest)..wcslen(dest)+\min(wcslen(src), n)));
+  requires separation:\separated(dest+(0..wcslen(dest)+wcslen(src)),src+(0..wcslen(src)));
   assigns dest[0 .. ] \from dest[0 .. ], indirect:dest, src[0 .. n-1], indirect:src, indirect:n;
   assigns \result \from dest;
   ensures result_ptr: \result == dest;
 */
 extern wchar_t * wcsncat(wchar_t *restrict dest, const wchar_t *restrict src, size_t n);
 
-/*@ assigns \result \from indirect:s1[0 .. n-1], indirect:s2[0 .. n-1], indirect:n; */
+/*@
+  requires valid_wstring_s1: valid_read_wstring(s1); // over-strong
+  requires valid_wstring_s2: valid_read_wstring(s2); // over-strong
+  assigns \result \from indirect:s1[0 .. n-1], indirect:s2[0 .. n-1], indirect:n;
+*/
 extern int wcsncmp(const wchar_t *s1, const wchar_t *s2, size_t n);
 
 /*@
+  requires valid_wstring_src: valid_read_wstring(src);
+  requires room_nwstring: \valid(dest+(0 .. n-1));
   requires separation:dest:src: \separated(dest+(0 .. n-1), src+(0 .. n-1));
   assigns dest[0 .. n-1] \from src[0 .. n-1], indirect:src, indirect:n;
   assigns \result \from dest;
   ensures result_ptr: \result == dest;
+  ensures initialization: \initialized(dest+(0 .. n-1));
  */
 extern wchar_t * wcsncpy(wchar_t *restrict dest, const wchar_t *restrict src, size_t n);
 
 /*@
+  requires valid_wstring_wcs: valid_read_wstring(wcs);
+  requires valid_wstring_accept: valid_read_wstring(accept);
   assigns \result \from wcs, indirect:wcs[0 .. ], indirect:accept[0 .. ];
   ensures result_null_or_inside_wcs:
     \result == \null || \subset (\result, wcs+(0 .. ));
@@ -155,16 +216,24 @@ extern wchar_t * wcsncpy(wchar_t *restrict dest, const wchar_t *restrict src, si
 extern wchar_t * wcspbrk(const wchar_t *wcs, const wchar_t *accept);
 
 /*@
-  assigns \result \from wcs, indirect:wcs[0 .. ], indirect:wc;
+  requires valid_wstring_wcs: valid_read_wstring(wcs);
+  assigns \result \from wcs, indirect:wcs[0 .. wcslen(wcs)], indirect:wc;
   ensures result_null_or_inside_wcs:
     \result == \null || \subset (\result, wcs+(0 .. ));
  */
 extern wchar_t * wcsrchr(const wchar_t *wcs, wchar_t wc);
 
-/*@ assigns \result \from indirect:wcs[0 .. ], indirect:accept[0 .. ]; */
+/*@
+  requires valid_wstring_wcs: valid_read_wstring(wcs);
+  requires valid_wstring_accept: valid_read_wstring(accept);
+  assigns \result \from indirect:wcs[0 .. wcslen(wcs)],
+                        indirect:accept[0 .. wcslen(accept)];
+*/
 extern size_t wcsspn(const wchar_t *wcs, const wchar_t *accept);
 
 /*@
+  requires valid_wstring_haystack: valid_read_wstring(haystack);
+  requires valid_wstring_needle: valid_read_wstring(needle);
   assigns \result \from haystack, indirect:haystack[0 .. ], indirect:needle[0 .. ];
   ensures result_null_or_inside_haystack:
     \result == \null || \subset (\result, haystack+(0 .. ));
@@ -172,8 +241,9 @@ extern size_t wcsspn(const wchar_t *wcs, const wchar_t *accept);
 extern wchar_t * wcsstr(const wchar_t *haystack, const wchar_t *needle);
 
 /*@
+  requires room_nwstring: \valid(ws+(0..n-1));
   requires valid_stream: \valid(stream);
-  assigns ws[0..n] \from indirect:n, indirect:*stream;
+  assigns ws[0..n-1] \from indirect:n, indirect:*stream;
   assigns \result \from ws, indirect:n, indirect:*stream;
   ensures result_null_or_same: \result == \null || \result == ws;
   ensures terminated_string_on_success:

tests/libc/wchar_h.c

 #include <stdio.h>
 #include <wchar.h>
-
+volatile int v;
 int main() {
   FILE *fd = fopen("bla", "r");
   if (!fd) return 1;
@@ -8,5 +8,63 @@ int main() {
   wchar_t *res = fgetws(buf, 29, fd);
   if (!res) return 1;
   //@ assert res == buf;
+  wchar_t buf2[2];
+  buf2[0] = L'a';
+  wchar_t *r = wmemchr(buf2, L'a', 2); // no warning
+  //@ check ok: r != \null;
+  r = wmemchr(0, 0, 0); // should be ok
+  //@ check ok: r == \null;
+  if (v) {
+    r = wmemchr(buf2, 0, 2); // red alarm (uninit)
+    //@ assert unreachable:\false;
+  }
+  r = wmemchr(buf2, L'a', 3); // no warning
+  //@ check ok: r != \null;
+  if (v) buf2[1] = L'b';
+  r = wmemchr(buf2, L'a', 3); // no warning
+  //@ check ok: r != \null;
+  r = wmemchr(buf2, L'b', 3); // warning: buf2[1] maybe uninit
+  //@ check ok: r != \null;
+  buf2[1] = L'b';
+  r = wmemchr(buf2, L'b', 3); // no warning
+  //@ check ok: r != \null;
+  wchar_t *wsrc = L"wide thing";
+  wchar_t wdst[10];
+  r = wcsncpy(wdst, wsrc, 10); // no warning
+  //@ check ok: r == wdst;
+  //@ check ok: \initialized(&wdst[9]);
+  if (v) {
+    r = wcsncpy(wdst, wsrc, wcslen(wsrc)+1); // error: not enough room
+    //@ assert unreachable:\false;
+  }
+  if (v) {
+    wcsncpy(wdst, wdst, 10); // error: no separation
+    //@ assert unreachable:\false;
+  }
+  if (v) {
+    wcsncpy(0, wsrc, 10); // error: invalid dest
+    //@ assert unreachable:\false;
+  }
+  if (v) {
+    wcsncpy(wdst, 0, 10); // error: invalid src
+    //@ assert unreachable:\false;
+  }
+  if (v) {
+    wcsncpy(wsrc, wdst, 10); // error: non-writable dest
+    //@ assert unreachable:\false;
+  }
+  wcsncmp(wsrc, wsrc, 11); // no warning
+  wcsncmp(wsrc, wdst, 11); // warning: wdst possibly invalid
+  wchar_t wdst2[20] = {0};
+  wcsncat(wdst2, wsrc, 11); // no warning
+  wcsncat(wdst2, wsrc, 10); // no warning (if wdst2 is precise)
+  //@ loop unroll 10;
+  for (int i = 0; i < 10; i++)
+    wdst2[i] = L'A';
+  wdst2[10] = L'\0'; // wdst2 now has length 10
+  if (v) {
+    wcsncat(wdst2+10, wdst2, 10); // error: no separation
+    //@ assert unreachable:\false;
+  }
   return 0;
 }