From 96f265f5b20254eb6eafb7e151db44f218324f28 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Mon, 15 Jun 2020 17:41:19 +0200
Subject: [PATCH] [eacsl:codegen] Add support to create GMP rational from GMP
integer
---
.../e-acsl/share/e-acsl/e_acsl_gmp_api.h | 12 +++
src/plugins/e-acsl/src/code_generator/gmp.ml | 75 +++++++++++--------
.../e-acsl/src/code_generator/rational.ml | 7 +-
3 files changed, 56 insertions(+), 38 deletions(-)
diff --git a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
index 625d41ea3e4..39946e50b14 100644
--- a/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
+++ b/src/plugins/e-acsl/share/e-acsl/e_acsl_gmp_api.h
@@ -154,6 +154,12 @@ extern void __gmpq_set_ui(mpq_t q, unsigned long int n, unsigned long int d)
extern void __gmpq_set_si(mpq_t q, signed long int n, unsigned long int d)
__attribute__((FC_BUILTIN));
+/*@ requires \valid_read(z_orig);
+ @ requires \valid(q);
+ @ assigns *q \from *z_orig; */
+extern void __gmpq_set_z(mpq_t q, const mpz_t z_orig)
+ __attribute__((FC_BUILTIN));
+
/*@ allocates q;
@ ensures \valid(q);
@ ensures \initialized(q);
@@ -173,6 +179,12 @@ extern void __gmpz_set_ui(mpz_t z, unsigned long int n)
extern void __gmpz_set_si(mpz_t z, signed long int n)
__attribute__((FC_BUILTIN));
+/*@ requires \valid_read(q_orig);
+ @ requires \valid(z);
+ @ assigns *z \from *q_orig; */
+extern void __gmpz_set_q(mpz_t z, const mpq_t q_orig)
+ __attribute__((FC_BUILTIN));
+
/*************/
/* Finalizer */
/*************/
diff --git a/src/plugins/e-acsl/src/code_generator/gmp.ml b/src/plugins/e-acsl/src/code_generator/gmp.ml
index 89ea82b0bdf..b35afd1163c 100644
--- a/src/plugins/e-acsl/src/code_generator/gmp.ml
+++ b/src/plugins/e-acsl/src/code_generator/gmp.ml
@@ -42,38 +42,49 @@ exception Longlong of ikind
let get_set_suffix_and_arg res_ty e =
let ty = Cil.typeOf e in
- if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then "", [ e ]
- else
- let args_uisi e =
- if Gmp_types.Z.is_t res_ty then [ e ]
- else begin
- assert (Gmp_types.Q.is_t res_ty);
- [ e; Cil.one ~loc:e.eloc ]
- end
- in
- match Cil.unrollType ty with
- | TInt(IChar, _) ->
- (if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
- else "_si"),
- args_uisi e
- | TInt((IBool | IUChar | IUInt | IUShort | IULong), _) ->
- "_ui", args_uisi e
- | TInt((ISChar | IShort | IInt | ILong), _) -> "_si", args_uisi e
- | TInt((ILongLong | IULongLong as ikind), _) -> raise (Longlong ikind)
- | TPtr(TInt(IChar, _), _) ->
- "_str",
- (* decimal base for the number given as string *)
- [ e; Cil.integer ~loc:e.eloc 10 ]
- | TFloat((FDouble | FFloat), _) ->
- (* FFloat is a strict subset of FDouble (modulo exceptional numbers)
- Hence, calling [set_d] for both of them is sound.
- HOWEVER: the machdep MUST NOT be vulnerable to double rounding
- [TODO] check the statement above *)
- "_d", [ e ]
- | TFloat(FLongDouble, _) ->
- Error.not_yet "creating gmp from long double"
- | _ ->
- assert false
+ let exp_number_ty = Typing.number_ty_of_typ ~post:true ty in
+ let res_number_ty = Typing.number_ty_of_typ ~post:true res_ty in
+ let args_uisi e =
+ if Gmp_types.Z.is_t res_ty then [ e ]
+ else begin
+ assert (Gmp_types.Q.is_t res_ty);
+ [ e; Cil.one ~loc:e.eloc ]
+ end
+ in
+ match (exp_number_ty, res_number_ty) with
+ | Typing.Gmpz, Typing.Gmpz | Typing.Rational, Typing.Rational ->
+ "", [ e ]
+ | Typing.Gmpz, Typing.Rational ->
+ "_z", [ e ]
+ | Typing.Rational, Typing.Gmpz ->
+ "_q", [ e ]
+ | Typing.C_integer IChar, _ ->
+ (if Cil.theMachine.Cil.theMachine.char_is_unsigned then "_ui"
+ else "_si"),
+ args_uisi e
+ | Typing.C_integer (IBool | IUChar | IUInt | IUShort | IULong), _ ->
+ "_ui", args_uisi e
+ | Typing.C_integer (ISChar | IShort | IInt | ILong), _ ->
+ "_si", args_uisi e
+ | Typing.C_integer (ILongLong | IULongLong as ikind), _ ->
+ raise (Longlong ikind)
+ | Typing.C_float (FDouble | FFloat), _ ->
+ (* FFloat is a strict subset of FDouble (modulo exceptional numbers)
+ Hence, calling [set_d] for both of them is sound.
+ HOWEVER: the machdep MUST NOT be vulnerable to double rounding
+ [TODO] check the statement above *)
+ "_d", [ e ]
+ | Typing.C_float FLongDouble, _ ->
+ Error.not_yet "creating gmp from long double"
+ | Typing.Gmpz, _ | Typing.Rational, _ | Typing.Real, _ | Typing.Nan, _ -> (
+ match Cil.unrollType ty with
+ | TPtr(TInt(IChar, _), _) ->
+ "_str",
+ (* decimal base for the number given as string *)
+ [ e; Cil.integer ~loc:e.eloc 10 ]
+ | _ ->
+ assert false
+ )
let generic_affect ~loc fname lv ev e =
let ty = Cil.typeOf ev in
diff --git a/src/plugins/e-acsl/src/code_generator/rational.ml b/src/plugins/e-acsl/src/code_generator/rational.ml
index 172206f198a..4c0ae922b43 100644
--- a/src/plugins/e-acsl/src/code_generator/rational.ml
+++ b/src/plugins/e-acsl/src/code_generator/rational.ml
@@ -32,12 +32,7 @@ let init_set ~loc lval vi_e e =
let create ~loc ?name e env kf t_opt =
let ty = Cil.typeOf e in
- if Gmp_types.Z.is_t ty then
- (* GMPQ has no builtin for creating Q from Z. Hence:
- 1) Get the MPZ as a string: gmZ_get_str
- 2) Set the MPQ with that string: gmpQ_set_str *)
- Error.not_yet "reals: creating Q from Z"
- else if Gmp_types.Q.is_t ty then
+ if Gmp_types.Q.is_t ty then
e, env
else
let _, e, env =
--
GitLab