From b2af2148d421352c9d4d0674f63f96fb0899880b Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Tue, 5 May 2020 15:29:43 +0200
Subject: [PATCH] [eacsl:codegen] Add support for left and right shift with GMP
parameters
---
.../e-acsl/src/code_generator/translate.ml | 144 +++++++++++++++++-
1 file changed, 141 insertions(+), 3 deletions(-)
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index ad1b39718cb..76d59a3eb9f 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -60,8 +60,10 @@ let name_of_mpz_arith_bop = function
| BAnd -> "__gmpz_and"
| BOr -> "__gmpz_ior"
| BXor -> "__gmpz_xor"
- | Lt | Gt | Le | Ge | Eq | Ne | LAnd | LOr | Shiftlt | Shiftrt | PlusPI
- | IndexPI | MinusPI | MinusPP -> assert false
+ | 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
@@ -399,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, ""
--
GitLab