Port ~50 library specifications to the new system (#1200)

* `atoi` and friends

* `htonl` and friends

* `sleep` an friends

* `strchr` and friends

* `strcasecmp` and friend

* `__builtin_strchr`

* `memcmp`

* `memchr`

* `{set,get}priority`

* `execl`

* `clock`

* `sem_init`

* `sem_wait` and `sem_trywait`

* Make `sem_wait*` consistent

* `sem_post`

* `sem_destroy`

* `sched_yield`

* `srand`

* `getpid`

* `getuid`, `geteuid`

* `getpgrp`

* `{set,get}rlimit`

* `setsid`

* `getdtablesize`

* `isatty`

* `__VERIFIER_nondet_int`

* `sigemptyset` and friends

* `sigprocmask`

* `fork`

* dynamic linking

* `inet_addr`

* `setsockopt`

* `getsockname`

* `socket`

* `gethostbyname_r`

* `gethostname`

* `getpeername`

* `uname`

* `getopt_long`

* Enable `svcomp` library functions where `racemacros.h` is included

* 36/15 activate sv-comp libraries

* Comment on `Sem*` specials that they are unused

* Move `str[n]casecmp` to Posix group

* Punctuation

* Apply suggestions from code review

Co-authored-by: Karoliine Holter <[email protected]>
Co-authored-by: Simmo Saan <[email protected]>

* Do not record accesses to `sem`

* Move `getdtablesize` to `glibc`

* Add `sema_init` back

* Remove TODO

---------

Co-authored-by: Karoliine Holter <[email protected]>
Co-authored-by: Simmo Saan <[email protected]>

Author: 3 people

src/analyses/libraryDesc.ml

@@ -58,6 +58,11 @@ type special =
   | Broadcast of Cil.exp
   | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; }
   | MutexInit of { mutex:Cil.exp; attr: Cil.exp; }
+  (* All Sem specials  are not used yet. *)
+  | SemInit of { sem: Cil.exp; pshared: Cil.exp; value: Cil.exp; }
+  | SemWait of { sem: Cil.exp; try_:bool; timeout: Cil.exp option;}
+  | SemPost of Cil.exp
+  | SemDestroy of Cil.exp
   | Wait of { cond: Cil.exp; mutex: Cil.exp; }
   | TimedWait of { cond: Cil.exp; mutex: Cil.exp; abstime: Cil.exp; (** Unused *) }
   | Math of { fun_args: math; }

src/analyses/libraryFunctions.ml

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -19,4 +20,4 @@ int main(void) {
   pthread_mutex_unlock(&mutex2);
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/01-simple_racing.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -19,4 +20,4 @@ int main(void) {
   pthread_mutex_unlock(&mutex1);
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/02-simple_racefree.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -26,4 +27,4 @@ int main(void) {
   create_threads(t1); create_threads(t2);
   join_threads(t1); join_threads(t2);
   return 0;
-}
+}

tests/regression/28-race_reach/03-munge_racing.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -26,4 +27,4 @@ int main(void) {
   create_threads(t1); create_threads(t2);
   join_threads(t1); join_threads(t2);
   return 0;
-}
+}

tests/regression/28-race_reach/04-munge_racefree.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -26,4 +27,4 @@ int main(void) {
   unlock();
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/05-lockfuns_racefree.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include<stdio.h>
 #include<pthread.h>
 
@@ -31,7 +32,3 @@ int main() {
   join_threads(t);
   return 0;
 }
-
-
-
-

tests/regression/28-race_reach/06-cond_racing1.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include<stdio.h>
 #include<pthread.h>
 #include "racemacros.h"

tests/regression/28-race_reach/07-cond_racing2.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include<stdio.h>
 #include<pthread.h>
 #include "racemacros.h"

tests/regression/28-race_reach/08-cond_racefree.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -27,4 +28,4 @@ int main(void) {
   create_threads(t1); create_threads(t2);
   join_threads(t1); join_threads(t2);
   return 0;
-}
+}

tests/regression/28-race_reach/09-ptrmunge_racing.c

@@ -1,3 +1,4 @@
+//PARAM: --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -27,4 +28,4 @@ int main(void) {
   create_threads(t1); create_threads(t2);
   join_threads(t1); join_threads(t2);
   return 0;
-}
+}

tests/regression/28-race_reach/10-ptrmunge_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -20,4 +21,4 @@ int main(void) {
   pthread_mutex_unlock(&mutex2);
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/11-ptr_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -16,8 +17,8 @@ void *t_fun(void *arg) {
 int main(void) {
   create_threads(t);
   pthread_mutex_lock(&mutex1);
-  assert_racefree(global); 
+  assert_racefree(global);
   pthread_mutex_unlock(&mutex1);
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/12-ptr_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 extern int __VERIFIER_nondet_int();
 
 #include<pthread.h>

tests/regression/28-race_reach/19-callback_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 extern int __VERIFIER_nondet_int();
 
 #include<pthread.h>

tests/regression/28-race_reach/20-callback_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/21-deref_read_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/22-deref_read_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/23-sound_unlock_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/24-sound_lock_racing.c

@@ -1,15 +1,16 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include <stdio.h>
 #include "racemacros.h"
 
 int global;
 pthread_mutex_t gm = PTHREAD_MUTEX_INITIALIZER;
 
-void bad() { 
+void bad() {
   access(global);
 }
 
-void good() { 
+void good() {
   pthread_mutex_lock(&gm);
   access(global);
   pthread_mutex_unlock(&gm);
@@ -42,4 +43,4 @@ int main() {
 
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/27-funptr_racing.c

@@ -1,14 +1,15 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include <stdio.h>
 #include "racemacros.h"
 
 int global = 0;
 pthread_mutex_t gm = PTHREAD_MUTEX_INITIALIZER;
 
-void bad() { 
+void bad() {
   access(global);
-} 
-void good() { 
+}
+void good() {
   pthread_mutex_lock(&gm);
   access(global);
   pthread_mutex_unlock(&gm);
@@ -41,4 +42,4 @@ int main() {
 
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/28-funptr_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/36-indirect_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/37-indirect_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -25,4 +26,4 @@ int main(void) {
   pthread_mutex_unlock(&mutex); // no UB because ERRORCHECK
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/40-trylock_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -22,4 +23,4 @@ int main(void) {
   pthread_mutex_unlock(&mutex);
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/41-trylock_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 
@@ -35,4 +36,4 @@ int main(void) {
 
   join_threads(t);
   return 0;
-}
+}

tests/regression/28-race_reach/42-trylock2_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/45-escape_racing.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/46-escape_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include <pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/51-mutexptr_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/60-invariant_racefree.c

@@ -1,3 +1,4 @@
+// PARAM:  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/61-invariant_racing.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include<stdio.h>
 #include "racemacros.h"

tests/regression/28-race_reach/70-funloop_racefree.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include<stdio.h>
 #include "racemacros.h"

tests/regression/28-race_reach/71-funloop_racing.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include<stdio.h>
 #include "racemacros.h"

tests/regression/28-race_reach/72-funloop_hard_racing.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include<stdio.h>
 #include "racemacros.h"

tests/regression/28-race_reach/73-funloop_hard_racefree.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include<stdio.h>
 #include "racemacros.h"

tests/regression/28-race_reach/74-tricky_address1_racefree.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include<stdio.h>
 #include "racemacros.h"

tests/regression/28-race_reach/75-tricky_address2_racefree.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include<stdio.h>
 #include "racemacros.h"

tests/regression/28-race_reach/76-tricky_address3_racefree.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include<stdio.h>
 #include "racemacros.h"

tests/regression/28-race_reach/77-tricky_address4_racing.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include<stdlib.h>
 #include "racemacros.h"

tests/regression/28-race_reach/78-equ_racing.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"
+// PARAM: --enable ana.race.direct-arithmetic --set ana.activated[+] "'var_eq'"  --set ana.activated[+] "'symb_locks'"  --set lib.activated[+] sv-comp
 #include<pthread.h>
 #include<stdlib.h>
 #include "racemacros.h"

tests/regression/28-race_reach/79-equ_racefree.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] "'region'"
+// PARAM: --set ana.activated[+] "'region'"  --set lib.activated[+] sv-comp
 #include<stdlib.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/81-list_racing.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] "'region'"
+// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp
 #include<stdlib.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/82-list_racefree.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] "'region'"
+// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp
 #include<stdlib.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/83-list2_racing1.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] "'region'"
+// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp
 #include<stdlib.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/84-list2_racing2.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] "'region'"
+// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp
 #include<stdlib.h>
 #include "racemacros.h"
 

tests/regression/28-race_reach/85-list2_racefree.c

@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] "'region'"
+// PARAM: --set ana.activated[+] "'region'" --set lib.activated[+] sv-comp
 #include<stdlib.h>
 #include "racemacros.h"