[eacsl:runtime] Enable functions of the GMP API to support shift operations

- Add `mp_bitcnt_t` type;
- Add `__gmpz_mul_2exp()` (resp. `__gmpz_tdiv_2exp()`) to support left shift (resp. right shift);
- Add `__gmpz_fits_ulong_p()` and `__gmpz_fits_slong_p()` to guard GMP to C integer coercions.

src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h

@@ -36,10 +36,11 @@
 #include "stdlib.h"
 #include "e_acsl_alias.h"
 
-#define mpz_struct export_alias(mpz_struct)
-#define mpz_t      export_alias(mpz_t)
-#define mpq_struct export_alias(mpq_struct)
-#define mpq_t      export_alias(mpq_t)
+#define mpz_struct  export_alias(mpz_struct)
+#define mpz_t       export_alias(mpz_t)
+#define mpq_struct  export_alias(mpq_struct)
+#define mpq_t       export_alias(mpq_t)
+#define mp_bitcnt_t export_alias(mp_bitcnt_t)
 
 struct mpz_struct {
   int _mp_alloc;
@@ -58,6 +59,14 @@ struct mpq_struct {
 typedef struct mpq_struct mpq_struct;
 typedef mpq_struct (__attribute__((__FC_BUILTIN__)) mpq_t)[1];
 
+/**
+ * Counts of bits of a multi-precision number are represented in the C type
+ * mp_bitcnt_t. Currently this is always an unsigned long, but on some systems
+ * it will be an unsigned long long in the future.
+ * @see https://gmplib.org/manual/Nomenclature-and-Types#Nomenclature-and-Types
+ */
+typedef unsigned long int mp_bitcnt_t;
+
 /****************/
 /* Initializers */
 /****************/
@@ -262,6 +271,12 @@ extern void __gmpq_sub(mpq_t q1, const mpq_t q2, const mpq_t q3)
 extern void __gmpz_mul(mpz_t z1, const mpz_t z2, const mpz_t z3)
   __attribute__((FC_BUILTIN));
 
+/*@ requires \valid(z1);
+  @ requires \valid_read(z2);
+  @ assigns *z1 \from *z2, n; */
+extern void __gmpz_mul_2exp(mpz_t z1, const mpz_t z2, mp_bitcnt_t n)
+  __attribute__((FC_BUILTIN));
+
 /*@ requires \valid(q1);
   @ requires \valid_read(q2);
   @ requires \valid_read(q3);
@@ -283,6 +298,12 @@ extern void __gmpz_tdiv_q(mpz_t z1, const mpz_t z2, const mpz_t z3)
 extern void __gmpz_tdiv_r(mpz_t z1, const mpz_t z2, const mpz_t z3)
   __attribute__((FC_BUILTIN));
 
+/*@ requires \valid(z1);
+  @ requires \valid_read(z2);
+  @ assigns *z1 \from *z2, n; */
+extern void __gmpz_tdiv_q_2exp(mpz_t z1, const mpz_t z2, mp_bitcnt_t n)
+  __attribute__((FC_BUILTIN));
+
 /*@ requires \valid(q1);
   @ requires \valid_read(q2);
   @ requires \valid_read(q3);
@@ -326,6 +347,18 @@ extern int __gmpz_com(mpz_t z1, const mpz_t z2)
 /* Coercions to C types */
 /************************/
 
+/** Return non-zero iff the value of z fits in an unsigned long */
+/*@ requires \valid_read(z);
+  @ assigns \result \from *z; */
+extern int __gmpz_fits_ulong_p(const mpz_t z)
+  __attribute__((FC_BUILTIN));
+
+/** Return non-zero iff the value of z fits in a signed long */
+/*@ requires \valid_read(z);
+  @ assigns \result \from *z; */
+extern int __gmpz_fits_slong_p(const mpz_t z)
+  __attribute__((FC_BUILTIN));
+
 /*@ requires \valid_read(z);
   @ assigns \result \from *z; */
 extern long __gmpz_get_si(const mpz_t z)

src/plugins/e-acsl/src/libraries/gmp_types.ml

@@ -80,6 +80,11 @@ end
 module Z = Make(struct end)
 module Q = Make(struct end)
 
+let bitcnt_type_info_ref = mk_dummy_type_info_ref ()
+
+let set_bitcnt_t tinfo = bitcnt_type_info_ref := tinfo
+let bitcnt_t () = TNamed(!bitcnt_type_info_ref, [])
+
 (**************************************************************************)
 (******************* Initialization of mpz and mpq types ******************)
 (**************************************************************************)
@@ -89,14 +94,18 @@ let init () =
   let set_mp_t = object (self)
     inherit Cil.nopCilVisitor
 
-    (* exit after having initialized the 4 values (for Z.t and Q.t) *)
+    (* exit after having initialized the 5 values:
+       - mp_bitcnt_t
+       - 2 for Z.t
+       - 2 for Q.t *)
+    val nb_to_visit = 5
     val mutable visited = 0
     method private set f info =
       f info;
-      if visited = 3 then
+      visited <- visited + 1;
+      if visited = nb_to_visit then
         raise Exit
       else begin
-        visited <- visited + 1;
         Cil.SkipChildren
       end
 
@@ -106,6 +115,7 @@ let init () =
         else if name = "__e_acsl_mpz_struct" then self#set Z.set_t_struct info
         else if name = "__e_acsl_mpq_t" then self#set Q.set_t info
         else if name = "__e_acsl_mpq_struct" then self#set Q.set_t_struct info
+        else if name = "__e_acsl_mp_bitcnt_t" then self#set set_bitcnt_t info
         else Cil.SkipChildren
       | _ ->
         Cil.SkipChildren

src/plugins/e-acsl/src/libraries/gmp_types.mli

@@ -54,6 +54,10 @@ module Z: S
 (** Representation of the rational type at runtime *)
 module Q: S
 
+val bitcnt_t: unit -> typ
+(** @return the C Type representing the count of bits of a multi-precision
+    number at runtime *)
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."