From e0e11b119f38a318df88128865366254356dd09b Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sun, 1 Oct 2023 14:46:13 +0200
Subject: [PATCH] Make `sem_wait*` consistent

---
 src/analyses/libraryDesc.ml      | 2 +-
 src/analyses/libraryFunctions.ml | 9 ++++-----
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml
index fde24ac77e..a0cf133eb8 100644
--- a/src/analyses/libraryDesc.ml
+++ b/src/analyses/libraryDesc.ml
@@ -58,7 +58,7 @@ type special =
   | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; }
   | MutexInit of { mutex:Cil.exp; attr: Cil.exp; }
   | SemInit of { sem: Cil.exp; pshared: Cil.exp; value: Cil.exp; }
-  | SemWait of { sem: Cil.exp; try_:bool}
+  | SemWait of { sem: Cil.exp; try_:bool; timeout: Cil.exp option;}
   | 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; }
diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 08ec2e2b3e..fa87810b74 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -404,13 +404,12 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("pthread_condattr_setclock", unknown [drop "attr" [w]; drop "clock_id" []]);
     ("pthread_mutexattr_destroy", unknown [drop "attr" [f]]);
     ("pthread_attr_setschedparam", unknown [drop "attr" [r; w]; drop "param" [r]]);
-    ("sem_timedwait", unknown [drop "sem" [r]; drop "abs_timeout" [r]]); (* no write accesses to sem because sync primitive itself has no race *)
     ("pthread_setaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [r]]);
     ("pthread_getaffinity_np", unknown [drop "thread" []; drop "cpusetsize" []; drop "cpuset" [w]]);
-    (* TODO: Remove w as soon as we have proper support for semaphores *)
-    ("sem_init", special [__ "sem" [w]; __ "pshared" []; __ "value" []] @@ fun sem pshared value -> SemInit {sem; pshared; value});
-    ("sem_wait", special [__ "sem" [w]] @@ fun sem -> SemWait {sem; try_ = false});
-    ("sem_trywait", special [__ "sem" [w]] @@ fun sem -> SemWait {sem; try_ = true});
+    ("sem_init", special [__ "sem" [r]; __ "pshared" []; __ "value" []] @@ fun sem pshared value -> SemInit {sem; pshared; value});
+    ("sem_wait", special [__ "sem" [r]] @@ fun sem -> SemWait {sem; try_ = false; timeout = None});
+    ("sem_trywait", special [__ "sem" [r]] @@ fun sem -> SemWait {sem; try_ = true; timeout = None});
+    ("sem_timedwait", special [__ "sem" [r]; __ "abs_timeout" [r]] @@ fun sem abs_timeout-> SemWait {sem; try_ = true; timeout = Some abs_timeout}); (* no write accesses to sem because sync primitive itself has no race *)
   ]
 
 (** GCC builtin functions.