Merge branch 'feature/basile/eacsl-33-bitwise-ops-gmp' into 'master'

[eacsl] Add support for bitwise operators when using GMP integer types

Closes e-acsl#33

See merge request frama-c/frama-c!2641

src/plugins/e-acsl/doc/Changelog

@@ -25,13 +25,16 @@
 Plugin E-ACSL <next-release>
 ############################
 
+-  E-ACSL       [2020-07-28] Add support of bitwise operators.
+                (frama-c/e-acsl#33)
 -* E-ACSL       [2020-07-20] Fix unstable order of generated globals.
                 (frama-c/e-acsl#124)
 -* E-ACSL       [2020-07-10] Fix translation of trange (incorrect length).
 -* E-ACSL       [2020-07-09] Decrease the number of allocated blocks when one
                 block is freed.
--  E-ACSL       [2020-06-19] Add support of bitwise operators for C integers.
-                (frama-c/e-acsl#33)
+-* E-ACSL       [2020-07-10] Fix translation of trange (incorrect length).
+-* E-ACSL       [2020-07-09] Decrease the number of allocated blocks when one
+                block is freed.
 -  E-ACSL       [2020-06-19] Add support to create GMP rational from GMP
                 integer. (frama-c/e-acsl#120)
 -* E-ACSL       [2020-06-18] Fix support of VLA memory tracking.

src/plugins/e-acsl/doc/refman/changes_modern.tex

@@ -126,6 +126,12 @@ in \lstinline|\\at|}
 
 \subsection*{Version \eacslpluginversion}
 
+\begin{itemize}
+\item \changeinsection{expressions}{support of bitwise operations}
+\end{itemize}
+
+\subsection*{Version Scandium-21}
+
 \begin{itemize}
 \item \changeinsection{reals}{support of rational numbers and operations}
 \item \changeinsection{fn-behavior}{remove abrupt clauses from the list of

src/plugins/e-acsl/doc/refman/intro_modern.tex

@@ -48,7 +48,6 @@ currently implemented into the \framac's \eacsl plug-in.
       \hline
       terms
       & \lstinline|\\true| and \lstinline|\\false| \\
-      & bitwise operators \\
       & let binding \\
       & t-sets \\
       \hline

src/plugins/e-acsl/doc/refman/term.tex

@@ -4,11 +4,11 @@
        | real ; real constants
        | string ; string constants
        | character ; character constants
-       \ 
-  bin-op ::= "+" | "-" | "*" | [ "/" ] | [ "%" ] | { "<<" } | { ">>" };
+       \
+  bin-op ::= "+" | "-" | "*" | [ "/" ] | [ "%" ] | "<<" | ">>";
        | "==" | "!=" | "<=" | ">=" | ">" | "<" ;
        | [ "&&" ] | [ "||" ] | [ "^^" ] ; boolean operations
-       | { "&" } | { "|" } | { "-->" } | { "<-->" } | "^" ; bitwise operations
+       | "&" | "|" | "-->" | "<-->" | "^" ; bitwise operations
        \
   unary-op ::= "+" | "-" ; unary plus and minus
        | "!" ; boolean negation

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);
@@ -294,6 +315,27 @@ extern void __gmpq_div(mpq_t q1, const mpq_t q2, const mpq_t q3)
 /* Bitwise operators */
 /*********************/
 
+/*@ requires \valid(z1);
+  @ requires \valid_read(z2);
+  @ requires \valid_read(z3);
+  @ assigns *z1 \from *z2, *z3; */
+extern void __gmpz_and(mpz_t z1, const mpz_t z2, const mpz_t z3)
+  __attribute__((FC_BUILTIN));
+
+/*@ requires \valid(z1);
+  @ requires \valid_read(z2);
+  @ requires \valid_read(z3);
+  @ assigns *z1 \from *z2, *z3; */
+extern void __gmpz_ior(mpz_t z1, const mpz_t z2, const mpz_t z3)
+  __attribute__((FC_BUILTIN));
+
+/*@ requires \valid(z1);
+  @ requires \valid_read(z2);
+  @ requires \valid_read(z3);
+  @ assigns *z1 \from *z2, *z3; */
+extern void __gmpz_xor(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;
@@ -305,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/code_generator/translate.ml

@@ -57,8 +57,13 @@ let name_of_mpz_arith_bop = function
   | Mult -> "__gmpz_mul"
   | Div -> "__gmpz_tdiv_q"
   | Mod -> "__gmpz_tdiv_r"
-  | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
-  | Shiftlt | Shiftrt | PlusPI | IndexPI | MinusPI | MinusPP -> assert false
+  | BAnd -> "__gmpz_and"
+  | BOr -> "__gmpz_ior"
+  | BXor -> "__gmpz_xor"
+  | Shiftlt -> "__gmpz_mul_2exp"
+  | Shiftrt -> "__gmpz_tdiv_q_2exp"
+  | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr | PlusPI | IndexPI | MinusPI
+  | MinusPP -> assert false
 
 (* Type of a string that represents a number.
    Used when a string is required to encode a constant number because it is not
@@ -396,7 +401,143 @@ and context_insensitive_term_to_exp kf env t =
     let e1, env = term_to_exp kf env t1 in
     let e2, env = term_to_exp kf env t2 in
     if Gmp_types.Z.is_t ty then
-      not_yet env "left/right shift on arbitrary precision"
+      (* If the given term is an lvalue variable or a cast from an lvalue
+         variable, retrieve the name of this variable. Otherwise return
+         default *)
+      let rec term_to_name t =
+        match t.term_node with
+        | TConst _ -> "cst_"
+        | TLval (TVar { lv_name }, _) -> lv_name ^ "_"
+        | TCastE (_, t) -> term_to_name t
+        | TLogic_coerce (_, t) -> term_to_name t
+        | _ -> ""
+      in
+      let ctx = Typing.get_number_ty t in
+      let bop_name = Misc.name_of_binop bop in
+      let e1_name = term_to_name t1 in
+      let e2_name = term_to_name t2 in
+      let zero = Logic_const.tinteger 0 in
+      Typing.type_term ~use_gmp_opt:true ~ctx zero;
+
+      (* Check that e2 is representable in mp_bitcnt_t *)
+      let coerce_guard, env =
+        let name = e2_name ^ bop_name ^ "_guard" in
+        let _vi, e, env =
+          Env.new_var
+            ~loc
+            ~scope:Varname.Block
+            ~name
+            env
+            kf
+            None
+            Cil.intType
+            (fun vi _e ->
+               let result = Cil.var vi in
+               let fname = "__gmpz_fits_ulong_p" in
+               [ Constructor.mk_lib_call ~loc ~result fname [ e2 ] ])
+        in
+        e, env
+      in
+      (* Coerce e2 to mp_bitcnt_t *)
+      let mk_coerce_stmts vi _e =
+        let coerce_guard_cond =
+          let max_bitcnt =
+            Cil.max_unsigned_number (Cil.bitsSizeOf (Gmp_types.bitcnt_t ()))
+          in
+          let max_bitcnt_term = Cil.lconstant ~loc max_bitcnt in
+          let pred =
+            Logic_const.pand
+              ~loc
+              (Logic_const.prel ~loc (Rle, zero, t2),
+               Logic_const.prel ~loc (Rle, t2, max_bitcnt_term))
+          in
+          let pname = bop_name ^ "_rhs_fits_in_mp_bitcnt_t" in
+          let pred = { pred with pred_name = pname :: pred.pred_name } in
+          let cond = Constructor.mk_runtime_check
+              ~reverse:true
+              Constructor.RTE
+              kf
+              coerce_guard
+              pred
+          in
+          Env.add_assert kf cond pred;
+          cond
+        in
+        let result = Cil.var vi in
+        let name = "__gmpz_get_ui" in
+        let instr = Constructor.mk_lib_call ~loc ~result name [ e2 ] in
+        [ coerce_guard_cond; instr ]
+      in
+      let name = e2_name ^ bop_name ^ "_coerced" in
+      let _e2_as_bitcnt_vi, e2_as_bitcnt_e, env =
+        Env.new_var
+          ~loc
+          ~scope:Varname.Block
+          ~name
+          env
+          kf
+          None
+          (Gmp_types.bitcnt_t ())
+          mk_coerce_stmts
+      in
+
+      (* Create the shift instruction *)
+      let mk_shift_instr result_e =
+        let name = name_of_mpz_arith_bop bop in
+        Constructor.mk_lib_call ~loc name [ result_e; e1; e2_as_bitcnt_e ]
+      in
+
+      (* Put t in an option to use with comparison_to_exp and
+         Env.new_var_and_mpz_init *)
+      let t = Some t in
+
+      (* TODO: let RTE generate the undef behaviors assertions *)
+
+      (* Boolean to choose whether the guard [e1 >= 0] should be added *)
+      let should_guard_e1 =
+        match bop with
+        | Shiftlt -> Kernel.LeftShiftNegative.get ()
+        | Shiftrt -> Kernel.RightShiftNegative.get ()
+        | _ -> assert false
+      in
+
+      (* Create the statements to initialize [e1 shift e2] *)
+      let e1_guard_opt, env =
+        if should_guard_e1 then
+          (* Future RTE:
+             if (warn left shift negative and left shift)
+                or (warn right shift negative and right shift)
+             then check e1 >= 0 *)
+          let e1_guard, env =
+            let name = e1_name ^ bop_name ^ "_guard" in
+            comparison_to_exp
+              ~loc kf env Typing.gmpz ~e1 ~name Ge t1 zero t
+          in
+          let e1_guard_cond =
+            let pred = Logic_const.prel ~loc (Rge, t1, zero) in
+            let cond = Constructor.mk_runtime_check
+                ~reverse:true
+                Constructor.RTE
+                kf
+                e1_guard
+                pred
+            in
+            Env.add_assert kf cond pred;
+            cond
+          in
+          Some e1_guard_cond, env
+        else
+          None, env
+      in
+      let mk_stmts _ e =
+        let shift_instr = mk_shift_instr e in
+        match e1_guard_opt with
+        | None -> [ shift_instr ]
+        | Some e1_guard -> [ e1_guard; shift_instr ]
+      in
+      let name = bop_name in
+      let _, e, env = Env.new_var_and_mpz_init ~loc ~name env kf t mk_stmts in
+      e, env, C_number, ""
     else begin
       assert (Logic_typing.is_integral_type t.term_type);
       Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""
@@ -426,7 +567,15 @@ and context_insensitive_term_to_exp kf env t =
     let e1, env = term_to_exp kf env t1 in
     let e2, env = term_to_exp kf env t2 in
     if Gmp_types.Z.is_t ty then
-      not_yet env "bitwise operator on arbitrary precision"
+      let mk_stmts _v e =
+        let name = name_of_mpz_arith_bop bop in
+        let instr = Constructor.mk_lib_call ~loc name [ e; e1; e2 ] in
+        [ instr ]
+      in
+      let name = Misc.name_of_binop bop in
+      let t = Some t in
+      let _, e, env = Env.new_var_and_mpz_init ~loc ~name env kf t mk_stmts in
+      e, env, C_number, ""
     else begin
       assert (Logic_typing.is_integral_type t.term_type);
       Cil.new_exp ~loc (BinOp(bop, e1, e2, ty)), env, C_number, ""

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 ../../../../.."

src/plugins/e-acsl/tests/arith/bitwise.c

 /* run.config_ci, run.config_dev
    COMMENT: Support of bitwise operations
    STDOPT: #"-warn-right-shift-negative -warn-left-shift-negative"
+   MACRO: ROOT_EACSL_GCC_FC_EXTRA_EXT -warn-right-shift-negative -warn-left-shift-negative
 */
 
 #include <limits.h>
@@ -42,8 +43,6 @@ void g_signed(int a, int b) {
 
     /*@ assert ((ULLONG_MAX + 1) << 1) != 0; */
     /*@ assert ((ULLONG_MAX + 1) >> 1) != 0; */
-    /*@ assert ((LLONG_MIN - 1) << 1) != 0; */
-    /*@ assert ((LLONG_MIN - 1) >> 1) != 0; */
     /*@ assert (1 << 65) != 0; */
     /*@ assert ((ULLONG_MAX + 1) | (LLONG_MIN - 1)) != 0; */
     /*@ assert ((ULLONG_MAX + 1) & (LLONG_MIN - 1)) !=

src/plugins/e-acsl/tests/arith/oracle_ci/bitwise.res.oracle

 [e-acsl] beginning translation.
-[e-acsl] tests/arith/bitwise.c:39: Warning: 
-  E-ACSL construct `left/right shift on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:41: Warning: 
-  E-ACSL construct `left/right shift on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:43: Warning: 
-  E-ACSL construct `left/right shift on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:44: Warning: 
-  E-ACSL construct `left/right shift on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:45: Warning: 
-  E-ACSL construct `left/right shift on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:46: Warning: 
-  E-ACSL construct `left/right shift on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:47: Warning: 
-  E-ACSL construct `left/right shift on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:48: Warning: 
-  E-ACSL construct `bitwise operator on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:49: Warning: 
-  E-ACSL construct `bitwise operator on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:56: Warning: 
-  E-ACSL construct `left/right shift on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:58: Warning: 
-  E-ACSL construct `left/right shift on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:60: Warning: 
-  E-ACSL construct `left/right shift on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:61: Warning: 
-  E-ACSL construct `left/right shift on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:62: Warning: 
-  E-ACSL construct `left/right shift on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:63: Warning: 
-  E-ACSL construct `bitwise operator on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
-[e-acsl] tests/arith/bitwise.c:64: Warning: 
-  E-ACSL construct `bitwise operator on arbitrary precision'
-  is not yet supported.
-  Ignoring annotation.
 [e-acsl] translation done in project "e-acsl".
+[eva:alarm] tests/arith/bitwise.c:40: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:40: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:42: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:42: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:44: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:45: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:46: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:47: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:48: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:55: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:55: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:57: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:57: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:59: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:60: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:61: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:62: Warning: 
+  function __e_acsl_assert: precondition got status unknown.
+[eva:alarm] tests/arith/bitwise.c:63: Warning: 
+  function __e_acsl_assert: precondition got status unknown.