[libc] add prototypes and spec for gcc __atomic_* specialized operations

share/libc/__fc_gcc_builtins.h

@@ -27,6 +27,7 @@
 #define __FC_GCC_BUILTINS
 #include "features.h"
 #include "__fc_machdep.h"
+#include "__fc_define_size_t.h"
 
 __PUSH_FC_STDLIB
 
@@ -254,6 +255,398 @@ int __builtin_popcountl (unsigned long x);
  */
 int __builtin_popcountll (unsigned long long x);
 
+// GCC specialized __atomic_* functions.
+// TODO: add generic counterpart with some help from cabs2cil for typing
+// NB: __atomic_* operations do not seem to make a distinction between
+// signed and unsigned: this may lead to some warnings by Frama-C
+
+/*@
+  requires validity: \valid_read(mem);
+  assigns \result \from *mem, indirect:model;
+*/
+__INT8_T __atomic_load_1(__INT8_T* mem, int model);
+
+/*@
+  requires validity: \valid_read(mem);
+  assigns \result \from *mem, indirect: model;
+*/
+__INT16_T __atomic_load_2(__INT16_T* mem, int model);
+
+/*@
+  requires validity: \valid_read(mem);
+  assigns \result \from *mem, indirect:model;
+*/
+__INT32_T __atomic_load_4(__INT32_T* mem, int model);
+
+/*@
+  requires validity: \valid_read(mem);
+  assigns \result \from *mem, indirect:model;
+*/
+__INT64_T __atomic_load_8(__INT64_T* mem, int model);
+
+/*@
+  requires validity: \valid(mem);
+  assigns *mem \from val, indirect: model;
+*/
+void __atomic_store_1(__INT8_T* mem, __INT8_T val, int model);
+
+/*@
+  requires validity: \valid(mem);
+  assigns *mem \from val, indirect: model;
+*/
+void __atomic_store_2(__INT16_T* mem, __INT16_T val, int model);
+
+/*@
+  requires validity: \valid(mem);
+  assigns *mem \from val, indirect: model;
+*/
+void __atomic_store_4(__INT32_T* mem, __INT32_T val, int model);
+
+/*@
+  requires validity: \valid(mem);
+  assigns *mem \from val, indirect: model;
+*/
+void __atomic_store_8(__INT64_T* mem, __INT64_T val, int model);
+
+/*@ requires validity: \valid(mem);
+    assigns *mem \from val, indirect:model;
+    assigns \result \from *mem, indirect:model;
+ */
+__INT8_T __atomic_exchange_1(__INT8_T* mem, __INT8_T val, int model);
+
+/*@ requires validity: \valid(mem);
+    assigns *mem \from val, indirect:model;
+    assigns \result \from *mem, indirect:model;
+ */
+__INT16_T __atomic_exchange_2(__INT16_T* mem, __INT16_T val, int model);
+
+/*@ requires validity: \valid(mem);
+    assigns *mem \from val, indirect:model;
+    assigns \result \from *mem, indirect:model;
+ */
+__INT32_T __atomic_exchange_4(__INT32_T* mem, __INT32_T val, int model);
+
+/*@ requires validity: \valid(mem);
+    assigns *mem \from val, indirect:model;
+    assigns \result \from *mem, indirect:model;
+ */
+__INT64_T __atomic_exchange_8(__INT64_T* mem, __INT64_T val, int model);
+
+/*@ requires validity: \valid(mem) && \valid_read(expected);
+  assigns *mem \from *mem, indirect: *expected, desired,
+          indirect: success_model, indirect: weak;
+  assigns *expected \from *expected, indirect: *mem, desired,
+          indirect: failure_model, indirect: weak;
+  assigns \result \from indirect: *mem, indirect: *expected;
+*/
+_Bool __atomic_compare_exchange_1(
+  __INT8_T* mem,
+  __INT8_T* expected,
+  __INT8_T desired,
+  _Bool weak, int success_model, int failure_model);
+
+/*@ requires validity: \valid(mem) && \valid_read(expected);
+  assigns *mem \from *mem, indirect: *expected, desired,
+          indirect: success_model, indirect: weak;
+  assigns *expected \from *expected, indirect: *mem, desired,
+          indirect: failure_model, indirect: weak;
+  assigns \result \from indirect: *mem, indirect: *expected;
+*/
+_Bool __atomic_compare_exchange_2(
+  __INT16_T* mem,
+  __INT16_T* expected,
+  __INT16_T desired,
+  _Bool weak, int success_model, int failure_model);
+
+/*@ requires validity: \valid(mem) && \valid_read(expected);
+  assigns *mem \from *mem, indirect: *expected, desired,
+          indirect: success_model, indirect: weak;
+  assigns *expected \from *expected, indirect: *mem, desired,
+          indirect: failure_model, indirect: weak;
+  assigns \result \from indirect: *mem, indirect: *expected;
+*/
+_Bool __atomic_compare_exchange_4(
+  __INT32_T* mem,
+  __INT32_T* expected,
+  __INT32_T desired,
+  _Bool weak, int success_model, int failure_model);
+
+/*@ requires validity: \valid(mem) && \valid_read(expected);
+  assigns *mem \from *mem, indirect: *expected, desired,
+          indirect: success_model, indirect: weak;
+  assigns *expected \from *expected, indirect: *mem, desired,
+          indirect: failure_model, indirect: weak;
+  assigns \result \from indirect: *mem, indirect: *expected;
+*/
+_Bool __atomic_compare_exchange_8(
+  __INT64_T* mem,
+  __INT64_T* expected,
+  __INT64_T desired,
+  _Bool weak, int success_model, int failure_model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT8_T __atomic_add_fetch_1 (__INT8_T *ptr, __INT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT8_T __atomic_sub_fetch_1 (__INT8_T *ptr, __INT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT8_T __atomic_and_fetch_1 (__INT8_T *ptr, __INT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT8_T __atomic_xor_fetch_1 (__INT8_T *ptr, __INT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT8_T __atomic_or_fetch_1 (__INT8_T *ptr, __INT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT8_T __atomic_nand_fetch_1 (__INT8_T *ptr, __INT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT16_T __atomic_add_fetch_2 (__INT16_T *ptr, __INT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT16_T __atomic_sub_fetch_2 (__INT16_T *ptr, __INT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT16_T __atomic_and_fetch_2 (__INT16_T *ptr, __INT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT16_T __atomic_xor_fetch_2 (__INT16_T *ptr, __INT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT16_T __atomic_or_fetch_2 (__INT16_T *ptr, __INT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT16_T __atomic_nand_fetch_2 (__INT16_T *ptr, __INT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT32_T __atomic_add_fetch_4 (__INT32_T *ptr, __INT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT32_T __atomic_sub_fetch_4 (__INT32_T *ptr, __INT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT32_T __atomic_and_fetch_4 (__INT32_T *ptr, __INT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT32_T __atomic_xor_fetch_4 (__INT32_T *ptr, __INT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT32_T __atomic_or_fetch_4 (__INT32_T *ptr, __INT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT32_T __atomic_nand_fetch_4 (__INT32_T *ptr, __INT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT64_T __atomic_add_fetch_8 (__INT64_T *ptr, __INT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT64_T __atomic_sub_fetch_8 (__INT64_T *ptr, __INT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT64_T __atomic_and_fetch_8 (__INT64_T *ptr, __INT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT64_T __atomic_xor_fetch_8 (__INT64_T *ptr, __INT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT64_T __atomic_or_fetch_8 (__INT64_T *ptr, __INT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT64_T __atomic_nand_fetch_8(__INT64_T* ptr, __INT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT8_T __atomic_fetch_add_1 (__INT8_T *ptr, __INT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT8_T __atomic_fetch_sub_1 (__INT8_T *ptr, __INT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT8_T __atomic_fetch_and_1 (__INT8_T *ptr, __INT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT8_T __atomic_fetch_xor_1 (__INT8_T *ptr, __INT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT8_T __atomic_fetch_or_1 (__INT8_T *ptr, __INT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT8_T __atomic_fetch_nand_1 (__INT8_T *ptr, __INT8_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT16_T __atomic_fetch_add_2 (__INT16_T *ptr, __INT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT16_T __atomic_fetch_sub_2 (__INT16_T *ptr, __INT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT16_T __atomic_fetch_and_2 (__INT16_T *ptr, __INT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT16_T __atomic_fetch_xor_2 (__INT16_T *ptr, __INT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT16_T __atomic_fetch_or_2 (__INT16_T *ptr, __INT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT16_T __atomic_fetch_nand_2 (__INT16_T *ptr, __INT16_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT32_T __atomic_fetch_add_4 (__INT32_T *ptr, __INT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT32_T __atomic_fetch_sub_4 (__INT32_T *ptr, __INT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT32_T __atomic_fetch_and_4 (__INT32_T *ptr, __INT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT32_T __atomic_fetch_xor_4 (__INT32_T *ptr, __INT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT32_T __atomic_fetch_or_4 (__INT32_T *ptr, __INT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT32_T __atomic_fetch_nand_4 (__INT32_T *ptr, __INT32_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT64_T __atomic_fetch_add_8 (__INT64_T *ptr, __INT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT64_T __atomic_fetch_sub__8 (__INT64_T *ptr, __INT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT64_T __atomic_fetch_and_8 (__INT64_T *ptr, __INT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT64_T __atomic_fetch_xor_8 (__INT64_T *ptr, __INT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT64_T __atomic_fetch_or_8 (__INT64_T *ptr, __INT64_T val, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns \result, *ptr \from *ptr, val, indirect: model;
+*/
+__INT64_T __atomic_fetch_nand_8(__INT64_T* ptr, __INT64_T val, int model);
+
+/*@ requires validity: \valid((char*)ptr);
+    assigns \result \from *((char*)ptr);
+    assigns *((char*)ptr) \from \nothing;
+*/
+_Bool __atomic_test_and_set (void *ptr, int model);
+
+/*@ requires validity: \valid(ptr);
+    assigns *ptr \from \nothing;
+*/
+void __atomic_clear(_Bool* ptr, int model);
+
+/*@ assigns \nothing; */
+void __atomic_thread_fence(int model);
+
+/*@ assigns \nothing; */
+void __atomic_signal_fence(int model);
+
+/*@ assigns \result \from indirect: size, indirect: ptr; */
+_Bool __atomic_always_lock_free (size_t size, void *ptr);
+
+/*@ assigns \result \from indirect: size, indirect: ptr; */
+_Bool __atomic_lock_free (size_t size, void *ptr);
+
 // According to the GCC docs
 // (https://gcc.gnu.org/onlinedocs/gcc/_005f_005fsync-Builtins.html),
 // this creates a 'full memory barrier'; we do not model the concurrency