Merge branch 'feature/thibaut/refactor-gmp-module' into 'master'

Refactor module `Gmp`

Closes e-acsl#193

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

src/plugins/e-acsl/src/code_generator/env.ml

@@ -26,6 +26,13 @@ open Analyses_types
 open Contract_types
 module Error = Translation_error
 
+
+(**************************************************************************)
+(********************** Forward references ********************************)
+(**************************************************************************)
+let gmp_clear_ref : (location -> exp -> stmt) ref =
+  Extlib.mk_fun "gmp_clear"
+
 type localized_scope =
   | LGlobal
   | LFunction of kernel_function
@@ -231,7 +238,7 @@ let do_new_var ~loc ?(scope=Varname.Block) ?(name="") env kf t ty mk_stmts =
       (*      Options.feedback "memoizing %a for term %a"
               Varinfo.pretty v (fun fmt t -> match t with None -> Format.fprintf fmt
               "NONE" | Some t -> Term.pretty fmt t) t;*)
-      { clear_stmts = Gmp.clear ~loc e :: tbl.clear_stmts;
+      { clear_stmts = !gmp_clear_ref loc e :: tbl.clear_stmts;
         new_exps = match t with
           | None -> tbl.new_exps
           | Some t -> Term.Map.add t (v, e) tbl.new_exps }
@@ -284,17 +291,6 @@ let new_var ~loc ?(scope=Varname.Block) ?name env kf t ty mk_stmts =
   | Varname.Global | Varname.Function -> memo env.global_mp_tbl
   | Varname.Block -> memo local_env.mp_tbl
 
-let new_var_and_mpz_init ~loc ?scope ?name env kf t mk_stmts =
-  new_var
-    ~loc
-    ?scope
-    ?name
-    env
-    kf
-    t
-    (Gmp_types.Z.t ())
-    (fun v e -> Gmp.init ~loc e :: mk_stmts v e)
-
 let rtl_call_to_new_var ~loc ?scope ?name env kf t ty func_name args =
   let _, exp, env =
     new_var

src/plugins/e-acsl/src/code_generator/env.mli

@@ -25,6 +25,8 @@ open Analyses_types
 open Analyses_datatype
 open Contract_types
 
+val gmp_clear_ref : (location -> exp -> stmt) ref
+
 (** Environments.
 
     Environments handle all the new C constructs (variables, statements and
@@ -54,14 +56,6 @@ val new_var:
     @return this variable as both a C variable and a C expression already
     initialized by applying it to [mk_stmts]. *)
 
-val new_var_and_mpz_init:
-  loc:location -> ?scope:Varname.scope -> ?name:string ->
-  t -> kernel_function -> term option ->
-  (varinfo -> exp (* the var as exp *) -> stmt list) ->
-  varinfo * exp * t
-(** Same as [new_var], but dedicated to mpz_t variables initialized by
-    {!Mpz.init}. *)
-
 val rtl_call_to_new_var:
   loc:location -> ?scope:Varname.scope -> ?name:string ->
   t -> kernel_function -> term option -> typ ->

src/plugins/e-acsl/src/code_generator/gmp.ml

@@ -33,29 +33,12 @@ let apply_on_var ~loc funname e =
     let ty = Cil.typeOf e in
     if Gmp_types.Z.is_t ty then "__gmpz_"
     else if Gmp_types.Q.is_t ty then "__gmpq_"
-    else assert false
+    else Options.fatal "expected GMP type instead of %a" Printer.pp_typ ty
   in
   Smart_stmt.rtl_call ~loc ~prefix funname [ e ]
 
-let name_of_mpz_arith_bop = function
-  | PlusA -> "__gmpz_add"
-  | MinusA -> "__gmpz_sub"
-  | Mult -> "__gmpz_mul"
-  | Div -> "__gmpz_tdiv_q"
-  | Mod -> "__gmpz_tdiv_r"
-  | 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 | MinusPI
-  | MinusPP as bop ->
-    Options.fatal
-      "Operation '%a' either not arithmetic or not supported on GMP integers"
-      Printer.pp_binop bop
-
 let init ~loc e = apply_on_var "init" ~loc e
-let clear ~loc e = apply_on_var "clear" ~loc e
+let clear loc e = apply_on_var "clear" ~loc e
 
 exception Longlong of ikind
 
@@ -88,17 +71,16 @@ let get_set_suffix_and_arg res_ty e =
      HOWEVER: the machdep MUST NOT be vulnerable to double rounding
      [TODO] check the statement above *)
   | C_float FLongDouble, _ -> Error.not_yet "creating gmp from long double"
-  | Gmpz, _ | Rational, _ | Real, _ | 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 =
+  | Gmpz, _ | Rational, _ | Real, _ | 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 ]
+    | _ ->
+      Options.fatal "expected char* instead of type %a" Printer.pp_typ ty
+
+let generic_assign ~loc fname lv ev e =
   let ty = Cil.typeOf ev in
   if Gmp_types.Z.is_t ty || Gmp_types.Q.is_t ty then begin
     let suf, args = get_set_suffix_and_arg ty e in
@@ -106,20 +88,20 @@ let generic_affect ~loc fname lv ev e =
   end else
     Smart_stmt.assigns ~loc:e.eloc ~result:lv e
 
-let affect ~loc lv ev e =
+let assign ~loc lv ev e =
   let fname =
     let ty = Cil.typeOf ev in
     if Gmp_types.Z.is_t ty then "__gmpz_set"
     else if Gmp_types.Q.is_t ty then "__gmpq_set"
     else ""
   in
-  try generic_affect ~loc fname lv ev e
+  try generic_assign ~loc fname lv ev e
   with Longlong _ ->
     Error.not_yet "quantification over long long and requiring GMP"
 
 let init_set ~loc lv ev e =
   let mpz_init_set fname =
-    try generic_affect ~loc fname lv ev e
+    try generic_assign ~loc fname lv ev e
     with
     | Longlong IULongLong ->
       (match e.enode with
@@ -148,12 +130,316 @@ let init_set ~loc lv ev e =
     mpz_init_set "__gmpz_init_set"
   else if Gmp_types.Q.is_t ty then
     Smart_stmt.block_stmt
-      (Cil.mkBlock
-         [ init ~loc ev ;
-           affect ~loc lv ev e ])
+      (Cil.mkBlock [ init ~loc ev; assign ~loc lv ev e ])
   else
     mpz_init_set ""
 
+module Z = struct
+
+  let name_arith_bop = function
+    | PlusA -> "__gmpz_add"
+    | MinusA -> "__gmpz_sub"
+    | Mult -> "__gmpz_mul"
+    | Div -> "__gmpz_tdiv_q"
+    | Mod -> "__gmpz_tdiv_r"
+    | 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 | MinusPI
+    | MinusPP as bop ->
+      Options.fatal
+        "Operation '%a' not supported on GMP integers"
+        Printer.pp_binop bop
+
+  let new_var ~loc ?scope ?name env kf t mk_stmts =
+    Env.new_var
+      ~loc
+      ?scope
+      ?name
+      env
+      kf
+      t
+      (Gmp_types.Z.t ())
+      (fun v e -> init ~loc e :: mk_stmts v e)
+
+  let create ~loc ?name t_opt env kf e =
+    let _, e, env =
+      Env.new_var
+        ~loc
+        ?name
+        env
+        kf
+        t_opt
+        (Gmp_types.Z.t ())
+        (fun vi vi_e -> [ init_set ~loc (Cil.var vi) vi_e e ])
+    in
+    e, env
+
+  let add_cast ~loc ?name env kf ty e =
+    let fname, new_ty =
+      if Cil.isSignedInteger ty then "__gmpz_get_si", Cil.longType
+      else "__gmpz_get_ui", Cil.ulongType
+    in
+    let _, e, env =
+      Env.new_var
+        ~loc
+        ?name
+        env
+        kf
+        None
+        new_ty
+        (fun v _ ->
+           [ Smart_stmt.rtl_call ~loc
+               ~result:(Cil.var v)
+               ~prefix:""
+               fname
+               [ e ] ])
+    in
+    e, env
+
+  let binop ~loc t_opt bop env kf e1 e2 =
+    let name = name_arith_bop bop in
+    let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
+                           ~prefix:""
+                           name
+                           [ e; e1; e2 ] ] in
+    let name = Misc.name_of_binop bop in
+    let _, e, env = new_var ~loc ~name env kf t_opt mk_stmts in
+    e,env
+
+  let cmp ~loc name t_opt bop env kf e1 e2 =
+    let _, e, env = Env.new_var
+        ~loc
+        env
+        kf
+        t_opt
+        ~name
+        Cil.intType
+        (fun v _ ->
+           [ Smart_stmt.rtl_call ~loc
+               ~result:(Cil.var v)
+               ~prefix:""
+               "__gmpz_cmp"
+               [ e1; e2 ] ])
+    in
+    Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
+
+end
+
+module Q = struct
+  let name_arith_bop = function
+    | PlusA -> "__gmpq_add"
+    | MinusA -> "__gmpq_sub"
+    | Mult -> "__gmpq_mul"
+    | Div -> "__gmpq_div"
+    | Mod | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
+    | Shiftlt | Shiftrt | PlusPI | MinusPI | MinusPP as bop ->
+      Options.fatal
+        "Operation '%a' not supported on GMP rationals"
+        Printer.pp_binop bop
+
+  exception Not_a_decimal of string
+  exception Is_a_float
+
+  (* The possible float suffixes (ISO C 6.4.4.2) are lLfF.
+     dD is a GNU extension accepted by Frama-C (only!) in the logic *)
+  let float_suffixes = [ 'f'; 'F'; 'l'; 'L'; 'd'; 'D' ]
+
+  (* Computes the fractional representation of a decimal number.
+     Does NOT perform reduction.
+     Example: [dec_to_frac "43.567"] evaluates to ["43567/1000"]
+     Complexity: Linear
+     Original Author: Frédéric Recoules
+
+     It iterates **once** over [str] during which three cases are distinguished,
+     example for "43.567":
+     Case1: pre: no '.' has been found yet ==> copy current char into buf
+      buf: | 4 |   |   |   |   |   |   |   |   |   |   |   |
+           | 4 | 3 |   |   |   |   |   |   |   |   |   |   |
+     Case2: mid: current char is '.' ==> put "/1" into buf at [(length str) - 1]
+      buf: | 4 | 3 |   |   |   | / | 1 |   |   |   |   |   |
+     Case3: post: a '.' was found ==> put current char in numerator AND '0' in den
+      buf: | 4 | 3 | 5 |   |   | / | 1 | 0 |   |   |   |   |
+           | 4 | 3 | 5 | 6 |   | / | 1 | 0 | 0 |   |   |   |
+           | 4 | 3 | 5 | 6 | 7 | / | 1 | 0 | 0 | 0 |   |   | *)
+  let decimal_to_fractional str =
+    let rec post str len buf len' i =
+      if i = len then
+        Bytes.sub_string buf 0 len'
+      else
+        match String.unsafe_get str i with
+        | c when '0' <= c && c <= '9' ->
+          Bytes.unsafe_set buf (i - 1) c;
+          Bytes.unsafe_set buf len' '0';
+          post str len buf (len' + 1) (i + 1)
+        | c when List.mem c float_suffixes ->
+          (* [JS] a suffix denoting a C type is possible *)
+          assert (i = len - 1);
+          raise Is_a_float
+        | _ ->
+          raise (Not_a_decimal str)
+    in
+    let mid buf len =
+      Bytes.unsafe_set buf (len - 1) '/';
+      Bytes.unsafe_set buf len '1'
+    in
+    let rec pre str len buf i =
+      if i = len then
+        str
+      else
+        match String.unsafe_get str i with
+        | '.' ->
+          mid buf len;
+          post str len buf (len + 1) (i + 1)
+        | c when '0' <= c && c <= '9' ->
+          Bytes.unsafe_set buf i c;
+          pre str len buf (i + 1)
+        | c when List.mem c float_suffixes ->
+          (* [JS] a suffix denoting a C type is possible *)
+          assert (i = len - 1);
+          raise Is_a_float
+        | _ ->
+          raise (Not_a_decimal str)
+    in
+    let strlen = String.length str in
+    let buflen =
+      (* The fractional representation is at most twice as lengthy
+         as the decimal one. *)
+      2 * strlen
+    in
+    try pre str strlen (Bytes.create buflen) 0
+    with Is_a_float -> str (* just left it unchanged *)
+
+  (* ACSL considers strings written in decimal expansion to be reals.
+     Yet GMPQ considers them to be double:
+     they MUST be converted into fractional representation. *)
+  let normalize_str str =
+    try
+      decimal_to_fractional str
+    with Invalid_argument _ ->
+      Error.not_yet "number not written in decimal expansion"
+
+  let create ~loc ?name t_opt env kf e =
+    let ty = Cil.typeOf e in
+    if Gmp_types.Q.is_t ty then
+      e, env
+    else
+      let _, e, env =
+        Env.new_var
+          ~loc
+          ?name
+          env
+          kf
+          t_opt
+          (Gmp_types.Q.t ())
+          (fun vi vi_e -> [ init_set ~loc (Cil.var vi) vi_e e ])
+      in
+      e, env
+
+  let cast_to_z ~loc:_ ?name:_ _env e =
+    assert (Gmp_types.Q.is_t (Cil.typeOf e));
+    Error.not_yet "reals: cast from R to Z"
+
+  let add_cast ~loc ?name env kf ty e =
+    (* TODO: The best solution would actually be to directly write all the
+       needed functions as C builtins then just call them here depending on the
+       situation at hand. *)
+    assert (Gmp_types.Q.is_t (Cil.typeOf e));
+    let get_double e env =
+      let _, e, env =
+        Env.new_var
+          ~loc
+          ?name
+          env
+          kf
+          None
+          Cil.doubleType
+          (fun v _ ->
+             [ Smart_stmt.rtl_call ~loc
+                 ~result:(Cil.var v)
+                 ~prefix:""
+                 "__gmpq_get_d"
+                 [ e ] ])
+      in
+      e, env
+    in
+    match Cil.unrollType ty with
+    | TFloat(FLongDouble, _) ->
+      (* The biggest floating-point type we can extract from GMPQ is double *)
+      Error.not_yet "R to long double"
+    | TFloat(FDouble, _) ->
+      get_double e env
+    | TFloat(FFloat, _) ->
+      (* No "get_float" in GMPQ, but fortunately, [float] \subset [double].
+         HOWEVER: going through double as intermediate step might be unsound
+         since it could cause double rounding. See: [Boldo2013, Sec 2.2]
+         https://hal.inria.fr/hal-00777639/document *)
+      let e, env = get_double e env in
+      Options.warning
+        ~once:true "R to float: double rounding might cause unsoundness";
+      Cil.mkCastT ~force:false ~oldt:Cil.doubleType ~newt:ty e, env
+    | TInt(IULongLong, _) ->
+      (* The biggest C integer type we can extract from GMP is ulong *)
+      Error.not_yet "R to unsigned long long"
+    | TInt _ ->
+      (* 1) Cast R to Z using cast_to_z
+         2) Extract ulong from Z
+         3) Potentially cast ulong to ty *)
+      Error.not_yet "R to Int"
+    | _ ->
+      Error.not_yet "R to <typ>"
+
+  let new_var ~loc ?scope ?name env kf t_opt mk_stmts =
+    Env.new_var
+      ~loc
+      ?scope
+      ?name
+      env
+      kf
+      t_opt
+      (Gmp_types.Q.t ())
+      (fun v e -> init ~loc e :: mk_stmts v e)
+
+  let binop ~loc t_opt bop env kf e1 e2 =
+    let name = name_arith_bop bop in
+    let e1, env = create ~loc None env kf e1 in
+    let e2, env = create ~loc None env kf e2 in
+    let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
+                           ~prefix:""
+                           name
+                           [ e; e1; e2 ] ] in
+    let name = Misc.name_of_binop bop in
+    let _, e, env = new_var ~loc ~name env kf t_opt mk_stmts in
+    e, env
+
+  let cmp ~loc name t_opt bop env kf e1 e2 =
+    let fname = "__gmpq_cmp" in
+    let e1, env = create ~loc None env kf e1 in
+    let e2, env = create ~loc None env kf e2 in
+    let _, e, env =
+      Env.new_var
+        ~loc
+        env
+        kf
+        t_opt
+        ~name
+        Cil.intType
+        (fun v _ ->
+           [ Smart_stmt.rtl_call ~loc
+               ~result:(Cil.var v)
+               ~prefix:""
+               fname
+               [ e1; e2 ] ])
+    in
+    Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
+
+end
+
+let () =
+  Env.gmp_clear_ref := clear
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

src/plugins/e-acsl/src/code_generator/gmp.mli

@@ -24,10 +24,6 @@
 
 open Cil_types
 
-val name_of_mpz_arith_bop: binop -> string
-(** [name_of_mpz_arith_bop bop] returns the name of the GMP function on integer
-    corresponding to the [bop] arithmetic operation. *)
-
 val init: loc:location -> exp -> stmt
 (** build stmt [mpz_init(v)] or [mpq_init(v)] depending on typ of [v] *)
 
@@ -36,14 +32,96 @@ val init_set: loc:location -> lval -> exp -> exp -> stmt
     or [mpq_init_set*(v, e)] with the good function 'set'
     according to the type of [e] *)
 
-val clear: loc:location -> exp -> stmt
+val clear: location -> exp -> stmt
 (** build stmt [mpz_clear(v)] or [mpq_clear(v)] depending on typ of [v] *)
 
-val affect: loc:location -> lval -> exp -> exp -> stmt
-(** [affect x_as_lv x_as_exp e] builds stmt [x = e] or [mpz_set*(e)]
+val assign: loc:location -> lval -> exp -> exp -> stmt
+(** [assign x_as_lv x_as_exp e] builds stmt [x = e] or [mpz_set*(e)]
     or [mpq_set*(e)] with the good function 'set'
     according to the type of [e] *)
 
+module Z : sig
+
+  val name_arith_bop: binop -> string
+  (** [name_of_mpz_arith_bop bop] returns the name of the GMP integer function
+      corresponding to the [bop] arithmetic operation. *)
+
+  val new_var:
+    loc:location -> ?scope:Varname.scope -> ?name:string ->
+    Env.t -> kernel_function -> term option ->
+    (varinfo -> exp (* the var as exp *) -> stmt list) ->
+    varinfo * exp * Env.t
+  (** Same as [Env.new_var], but dedicated to mpz_t variables initialized by
+      {!Mpz.init}. *)
+
+  val create:
+    loc:location -> ?name:string -> term option ->  Env.t -> kernel_function ->
+    exp -> exp * Env.t
+  (** Create an integer number. *)
+
+  val add_cast:
+    loc:location -> ?name:string -> Env.t -> kernel_function -> typ -> exp ->
+    exp * Env.t
+  (** Assumes that the given exp is of integer type and casts it into
+      the given typ *)
+
+  val binop:
+    loc:location -> term option -> binop -> Env.t -> kernel_function ->
+    exp -> exp -> exp * Env.t
+  (** Applies [binop] to the given expressions. The optional term
+      indicates whether the comparison has a correspondance in the logic. *)
+
+  val cmp:
+    loc:location -> string -> term option -> binop ->  Env.t ->
+    kernel_function -> exp -> exp -> exp * Env.t
+    (** Compares two expressions according to the given [binop]. The optional
+        term indicates whether the comparison has a correspondance in the
+        logic. *)
+
+end
+
+module Q : sig
+
+  val name_arith_bop: binop -> string
+  (** [name_of_mpz_arith_bop bop] returns the name of the GMP rational function
+      corresponding to the [bop] arithmetic operation. *)
+
+  val normalize_str: string -> string
+  (** Normalize the string so that it fits the representation used by the
+      underlying real library. For example, "0.1" is a real number in ACSL
+      whereas it is considered as a double by [libgmp] because it is written in
+      decimal expansion. In order to make [libgmp] consider it to be a rational,
+      it must be converted into "1/10". *)
+
+  val create:
+    loc:location -> ?name:string -> term option ->  Env.t -> kernel_function ->
+    exp -> exp * Env.t
+  (** Create a rational number. *)
+
+  val cast_to_z: loc:location -> ?name:string -> Env.t -> exp -> exp * Env.t
+  (** Assumes that the given exp is of real type and casts it into Z *)
+
+  val add_cast:
+    loc:location -> ?name:string -> Env.t -> kernel_function -> typ -> exp ->
+    exp * Env.t
+  (** Assumes that the given exp is of real type and casts it into
+      the given typ *)
+
+  val binop:
+    loc:location -> term option -> binop -> Env.t -> kernel_function ->
+    exp -> exp -> exp * Env.t
+  (** Applies [binop] to the given expressions. The optional term
+      indicates whether the comparison has a correspondance in the logic. *)
+
+  val cmp:
+    loc:location -> string -> term option -> binop ->  Env.t ->
+    kernel_function -> exp -> exp -> exp * Env.t
+    (** Compares two expressions according to the given [binop]. The optional
+        term indicates whether the comparison has a correspondance in the
+        logic. *)
+
+end
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."

src/plugins/e-acsl/src/code_generator/loops.ml

@@ -321,7 +321,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     let e1, _, env = term_to_exp kf (Env.push env) t1 in
     let init_blk, env = Env.pop_and_get
         env
-        (Gmp.affect ~loc:e1.eloc lv_x x e1)
+        (Gmp.assign ~loc:e1.eloc lv_x x e1)
         ~global_clear:false
         Env.Middle
     in
@@ -342,7 +342,10 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
           (TBinOp(Lt, tlv, t2))
           Linteger
     in
-    Typing.preprocess_term ~use_gmp_opt:false ~ctx:Typing.c_int ~logic_env guard;
+    Typing.preprocess_term
+      ~use_gmp_opt:false
+      ~ctx:Typing.c_int
+      ~logic_env guard;
     let guard_exp, _, env = term_to_exp kf (Env.push env) guard in
     let break_stmt = Smart_stmt.break ~loc:guard_exp.eloc in
     let guard_blk, env = Env.pop_and_get
@@ -362,13 +365,15 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     let incr, _, env = term_to_exp kf (Env.push env) tlv_one in
     let next_blk, env = Env.pop_and_get
         env
-        (Gmp.affect ~loc:incr.eloc lv_x x incr)
+        (Gmp.assign ~loc:incr.eloc lv_x x incr)
         ~global_clear:false
         Env.Middle
     in
     (* generate the whole loop *)
     let next = block_to_stmt next_blk in
-    let guard_for_small_type_opt = Bound_variables.get_guard_for_small_type logic_x in
+    let guard_for_small_type_opt =
+      Bound_variables.get_guard_for_small_type logic_x
+    in
     let stmts, env = match guard_for_small_type_opt with
       | None ->
         guard :: body @ [ next ], env
@@ -429,6 +434,6 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
 
 (*
 Local Variables:
-compile-command: "make -C ../.."
+compile-command: "make -C ../../../../.."
 End:
 *)

src/plugins/e-acsl/src/code_generator/rational.ml

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
-(*                                                                        *)
-(*  Copyright (C) 2012-2022                                               *)
-(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
-(*         alternatives)                                                  *)
-(*                                                                        *)
-(*  you can redistribute it and/or modify it under the terms of the GNU   *)
-(*  Lesser General Public License as published by the Free Software       *)
-(*  Foundation, version 2.1.                                              *)
-(*                                                                        *)
-(*  It is distributed in the hope that it will be useful,                 *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
-(*  GNU Lesser General Public License for more details.                   *)
-(*                                                                        *)
-(*  See the GNU Lesser General Public License version 2.1                 *)
-(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-open Cil_types
-
-let create ~loc ?name e env kf t_opt =
-  let ty = Cil.typeOf e in
-  if Gmp_types.Q.is_t ty then
-    e, env
-  else
-    let _, e, env =
-      Env.new_var
-        ~loc
-        ?name
-        env
-        kf
-        t_opt
-        (Gmp_types.Q.t ())
-        (fun vi vi_e ->
-           [ Gmp.init ~loc vi_e ;
-             Gmp.affect ~loc (Cil.var vi) vi_e e ])
-    in
-    e, env
-
-exception Not_a_decimal of string
-exception Is_a_float
-
-(* The possible float suffixes (ISO C 6.4.4.2) are lLfF.
-   dD is a GNU extension accepted by Frama-C (only!) in the logic *)
-let float_suffixes = [ 'f'; 'F'; 'l'; 'L'; 'd'; 'D' ]
-
-(* Computes the fractional representation of a decimal number.
-   Does NOT perform reduction.
-   Example: [dec_to_frac "43.567"] evaluates to ["43567/1000"]
-   Complexity: Linear
-   Original Author: Frédéric Recoules
-
-   It iterates **once** over [str] during which three cases are distinguished,
-   example for "43.567":
-   Case1: pre: no '.' has been found yet ==> copy current char into buf
-    buf: | 4 |   |   |   |   |   |   |   |   |   |   |   |
-         | 4 | 3 |   |   |   |   |   |   |   |   |   |   |
-   Case2: mid: current char is '.' ==> put "/1" into buf at [(length str) - 1]
-    buf: | 4 | 3 |   |   |   | / | 1 |   |   |   |   |   |
-   Case3: post: a '.' was found ==> put current char in numerator AND '0' in den
-    buf: | 4 | 3 | 5 |   |   | / | 1 | 0 |   |   |   |   |
-         | 4 | 3 | 5 | 6 |   | / | 1 | 0 | 0 |   |   |   |
-         | 4 | 3 | 5 | 6 | 7 | / | 1 | 0 | 0 | 0 |   |   | *)
-let decimal_to_fractional str =
-  let rec post str len buf len' i =
-    if i = len then
-      Bytes.sub_string buf 0 len'
-    else
-      match String.unsafe_get str i with
-      | c when '0' <= c && c <= '9' ->
-        Bytes.unsafe_set buf (i - 1) c;
-        Bytes.unsafe_set buf len' '0';
-        post str len buf (len' + 1) (i + 1)
-      | c when List.mem c float_suffixes ->
-        (* [JS] a suffix denoting a C type is possible *)
-        assert (i = len - 1);
-        raise Is_a_float
-      | _ ->
-        raise (Not_a_decimal str)
-  in
-  let mid buf len =
-    Bytes.unsafe_set buf (len - 1) '/';
-    Bytes.unsafe_set buf len '1'
-  in
-  let rec pre str len buf i =
-    if i = len then
-      str
-    else
-      match String.unsafe_get str i with
-      | '.' ->
-        mid buf len;
-        post str len buf (len + 1) (i + 1)
-      | c when '0' <= c && c <= '9' ->
-        Bytes.unsafe_set buf i c;
-        pre str len buf (i + 1)
-      | c when List.mem c float_suffixes ->
-        (* [JS] a suffix denoting a C type is possible *)
-        assert (i = len - 1);
-        raise Is_a_float
-      | _ ->
-        raise (Not_a_decimal str)
-  in
-  let strlen = String.length str in
-  let buflen =
-    (* The fractional representation is at most twice as lengthy
-       as the decimal one. *)
-    2 * strlen
-  in
-  try pre str strlen (Bytes.create buflen) 0
-  with Is_a_float -> str (* just left it unchanged *)
-
-(* ACSL considers strings written in decimal expansion to be reals.
-   Yet GMPQ considers them to be double:
-   they MUST be converted into fractional representation. *)
-let normalize_str str =
-  try
-    decimal_to_fractional str
-  with Invalid_argument _ ->
-    Error.not_yet "number not written in decimal expansion"
-
-let cast_to_z ~loc:_ ?name:_ e _env =
-  assert (Gmp_types.Q.is_t (Cil.typeOf e));
-  Error.not_yet "reals: cast from R to Z"
-
-let add_cast ~loc ?name e env kf ty =
-  (* TODO: The best solution would actually be to directly write all the needed
-     functions as C builtins then just call them here depending on the situation
-     at hand. *)
-  assert (Gmp_types.Q.is_t (Cil.typeOf e));
-  let get_double e env =
-    let _, e, env =
-      Env.new_var
-        ~loc
-        ?name
-        env
-        kf
-        None
-        Cil.doubleType
-        (fun v _ ->
-           [ Smart_stmt.rtl_call ~loc
-               ~result:(Cil.var v)
-               ~prefix:""
-               "__gmpq_get_d"
-               [ e ] ])
-    in
-    e, env
-  in
-  match Cil.unrollType ty with
-  | TFloat(FLongDouble, _) ->
-    (* The biggest floating-point type we can extract from GMPQ is double *)
-    Error.not_yet "R to long double"
-  | TFloat(FDouble, _) ->
-    get_double e env
-  | TFloat(FFloat, _) ->
-    (* No "get_float" in GMPQ, but fortunately, [float] \subset [double].
-       HOWEVER: going through double as intermediate step might be unsound since
-       it could cause double rounding. See: [Boldo2013, Sec 2.2]
-       https://hal.inria.fr/hal-00777639/document *)
-    let e, env = get_double e env in
-    Options.warning
-      ~once:true "R to float: double rounding might cause unsoundness";
-    Cil.mkCastT ~force:false ~oldt:Cil.doubleType ~newt:ty e, env
-  | TInt(IULongLong, _) ->
-    (* The biggest C integer type we can extract from GMP is ulong *)
-    Error.not_yet "R to unsigned long long"
-  | TInt _ ->
-    (* 1) Cast R to Z using cast_to_z
-       2) Extract ulong from Z
-       3) Potentially cast ulong to ty *)
-    Error.not_yet "R to Int"
-  | _ ->
-    Error.not_yet "R to <typ>"
-
-let cmp ~loc bop e1 e2 env kf t_opt =
-  let fname = "__gmpq_cmp" in
-  let name = Misc.name_of_binop bop in
-  (* TODO: [t1_opt] and [t2_opt] could be provided when creating [e1] and
-     [e2] *)
-  let e1, env = create ~loc e1 env kf None in
-  let e2, env = create ~loc e2 env kf None in
-  let _, e, env =
-    Env.new_var
-      ~loc
-      env
-      kf
-      t_opt
-      ~name
-      Cil.intType
-      (fun v _ ->
-         [ Smart_stmt.rtl_call ~loc
-             ~result:(Cil.var v)
-             ~prefix:""
-             fname
-             [ e1; e2 ] ])
-  in
-  Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
-
-let new_var_and_init ~loc ?scope ?name env kf t_opt mk_stmts =
-  Env.new_var
-    ~loc
-    ?scope
-    ?name
-    env
-    kf
-    t_opt
-    (Gmp_types.Q.t ())
-    (fun v e -> Gmp.init ~loc e :: mk_stmts v e)
-
-let name_arith_bop = function
-  | PlusA -> "__gmpq_add"
-  | MinusA -> "__gmpq_sub"
-  | Mult -> "__gmpq_mul"
-  | Div -> "__gmpq_div"
-  | Mod | Lt | Gt | Le | Ge | Eq | Ne | BAnd | BXor | BOr | LAnd | LOr
-  | Shiftlt | Shiftrt | PlusPI | MinusPI | MinusPP -> assert false
-
-let binop ~loc bop e1 e2 env kf t_opt =
-  let name = name_arith_bop bop in
-  (* TODO: [t1_opt] and [t2_opt] could be provided when creating [e1] and
-     [e2] *)
-  let e1, env = create ~loc e1 env kf None in
-  let e2, env = create ~loc e2 env kf None in
-  let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
-                         ~prefix:""
-                         name
-                         [ e; e1; e2 ] ] in
-  let name = Misc.name_of_binop bop in
-  let _, e, env = new_var_and_init ~loc ~name env kf t_opt mk_stmts in
-  e, env
-
-(*
-Local Variables:
-compile-command: "make -C ../.."
-End:
-*)

src/plugins/e-acsl/src/code_generator/rational.mli

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
-(*                                                                        *)
-(*  Copyright (C) 2012-2022                                               *)
-(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
-(*         alternatives)                                                  *)
-(*                                                                        *)
-(*  you can redistribute it and/or modify it under the terms of the GNU   *)
-(*  Lesser General Public License as published by the Free Software       *)
-(*  Foundation, version 2.1.                                              *)
-(*                                                                        *)
-(*  It is distributed in the hope that it will be useful,                 *)
-(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
-(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
-(*  GNU Lesser General Public License for more details.                   *)
-(*                                                                        *)
-(*  See the GNU Lesser General Public License version 2.1                 *)
-(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-(** Generation of rational numbers. *)
-
-(* [TODO ARCHI]: change the call convention in the whole module *)
-
-open Cil_types
-
-(* TODO: change the call convention *)
-val create:
-  loc:location -> ?name:string -> exp -> Env.t -> kernel_function ->
-  term option ->
-  exp * Env.t
-(** Create a real *)
-
-val normalize_str: string -> string
-(** Normalize the string so that it fits the representation used by the
-    underlying real library. For example, "0.1" is a real number in ACSL
-    whereas it is considered as a double by [libgmp] because it is written in
-    decimal expansion. In order to make [libgmp] consider it to be a rational,
-    it must be converted into "1/10". *)
-
-(* TODO: change the call convention *)
-val cast_to_z: loc:location -> ?name:string -> exp -> Env.t -> exp * Env.t
-(** Assumes that the given exp is of real type and casts it into Z *)
-
-(* TODO: change the call convention *)
-val add_cast:
-  loc:location -> ?name:string -> exp -> Env.t -> kernel_function -> typ ->
-  exp * Env.t
-(** Assumes that the given exp is of real type and casts it into
-    the given typ *)
-
-(* TODO: change the call convention --> exp at the end *)
-val binop:
-  loc:location -> binop -> exp -> exp -> Env.t -> kernel_function ->
-  term option ->
-  exp * Env.t
-(** Applies [binop] to the given expressions. The optional term
-    indicates whether the comparison has a correspondance in the logic. *)
-
-(* TODO: change the call convention --> exp at the end *)
-val cmp:
-  loc:location -> binop -> exp -> exp -> Env.t -> kernel_function ->
-  term option ->
-  exp * Env.t
-(** Compares two expressions according to the given [binop]. The optional term
-    indicates whether the comparison has a correspondance in the logic. *)
-
-(*
-Local Variables:
-compile-command: "make -C ../.."
-End:
-*)

src/plugins/e-acsl/src/code_generator/translate_terms.ml

@@ -47,7 +47,7 @@ let translate_rte_exp_ref
 
 let constant_to_exp ~loc env t c =
   let mk_real s =
-    let s = Rational.normalize_str s in
+    let s = Gmp.Q.normalize_str s in
     Cil.mkString ~loc s, Typed_number.Str_R
   in
   match c with
@@ -115,9 +115,8 @@ let affect_binop ~loc var_as_varinfo var_as_exp binop exp_type exp1 exp2 =
          "__gmpz_cmp"
          [exp1; exp2]
      | Some e ->
-       let name = Gmp.name_of_mpz_arith_bop binop in
-       Smart_stmt.rtl_call
-         ~loc ~prefix:"" name [e; exp1; exp2])
+       let name = Gmp.Z.name_arith_bop binop in
+       Smart_stmt.rtl_call ~loc ~prefix:"" name [e; exp1; exp2])
   else if Gmp_types.Q.is_t exp_type then
     Error.not_yet "rational in affect_binop"
   else
@@ -201,7 +200,7 @@ and extended_quantifier_to_exp ~adata ~loc kf env t t_min t_max lambda name =
     let e_lbd, _, env = to_exp ~adata:Assert.no_data kf env lt in
     let lbd_stmt,env =
       Env.pop_and_get env
-        (Gmp.affect ~loc (Cil.var lbd_as_varinfo) lbd_as_exp e_lbd)
+        (Gmp.assign ~loc (Cil.var lbd_as_varinfo) lbd_as_exp e_lbd)
         ~global_clear:false Env.Middle
     in
     (* statement construction *)
@@ -304,7 +303,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
         | LNot -> assert false
       in
       let _, e, env =
-        Env.new_var_and_mpz_init
+        Gmp.Z.new_var
           ~loc
           env
           kf
@@ -350,18 +349,10 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
     let e1, adata, env = to_exp ~adata kf env t1 in
     let e2, adata, env = to_exp ~adata kf env t2 in
     if Gmp_types.Z.is_t ty then
-      let name = Gmp.name_of_mpz_arith_bop bop in
-      let mk_stmts _ e = [ Smart_stmt.rtl_call ~loc
-                             ~prefix:""
-                             name
-                             [ e; e1; e2 ] ] in
-      let name = Misc.name_of_binop bop in
-      let _, e, env =
-        Env.new_var_and_mpz_init ~loc ~name env kf (Some t) mk_stmts
-      in
+      let e, env = Gmp.Z.binop ~loc (Some t) bop env kf e1 e2 in
       e, adata, env, Typed_number.C_number, ""
     else if Gmp_types.Q.is_t ty then
-      let e, env = Rational.binop ~loc bop e1 e2 env kf (Some t) in
+      let e, env = Gmp.Q.binop ~loc (Some t) bop env kf e1 e2 in
       e, adata, env, Typed_number.C_number, ""
     else begin
       assert (Logic_typing.is_integral_type t.term_type);
@@ -384,7 +375,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
          RTE should do this automatically. *)
       let ctx = Typing.get_number_ty ~logic_env t in
       let t = Some t in
-      let name = Gmp.name_of_mpz_arith_bop bop in
+      let name = Gmp.Z.name_arith_bop bop in
       (* [TODO] can now do better since the type system got some info about
          possible values of [t2] *)
       (* guarding divisions and modulos *)
@@ -424,11 +415,11 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
         [ cond; instr ]
       in
       let name = Misc.name_of_binop bop in
-      let _, e, env = Env.new_var_and_mpz_init ~loc ~name env kf t mk_stmts in
+      let _, e, env = Gmp.Z.new_var ~loc ~name env kf t mk_stmts in
       e, adata, env, Typed_number.C_number, ""
     else if Gmp_types.Q.is_t ty then
       let e2, adata, env = t2_to_exp adata env in
-      let e, env = Rational.binop ~loc bop e1 e2 env kf (Some t) in
+      let e, env = Gmp.Q.binop ~loc (Some t) bop env kf e1 e2 in
       e, adata, env, Typed_number.C_number, ""
     else begin
       assert (Logic_typing.is_integral_type t.term_type);
@@ -560,7 +551,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
 
       (* Create the shift instruction *)
       let mk_shift_instr result_e =
-        let name = Gmp.name_of_mpz_arith_bop bop in
+        let name = Gmp.Z.name_arith_bop bop in
         Smart_stmt.rtl_call ~loc
           ~prefix:""
           name
@@ -568,7 +559,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
       in
 
       (* Put t in an option to use with Translate_utils.comparison_to_exp and
-         Env.new_var_and_mpz_init *)
+         Gmp.Z.new_var *)
       let t = Some t in
 
       (* TODO: let RTE generate the undef behaviors assertions *)
@@ -633,7 +624,7 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
         | 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
+      let _, e, env = Gmp.Z.new_var ~loc ~name env kf t mk_stmts in
       e, adata, env, Typed_number.C_number, ""
     else begin
       assert (Logic_typing.is_integral_type t.term_type);
@@ -691,13 +682,13 @@ and context_insensitive_term_to_exp ~adata ?(inplace=false) kf env t =
     let e2, adata, env = to_exp ~adata kf env t2 in
     if Gmp_types.Z.is_t ty then
       let mk_stmts _v e =
-        let name = Gmp.name_of_mpz_arith_bop bop in
+        let name = Gmp.Z.name_arith_bop bop in
         let instr = Smart_stmt.rtl_call ~loc ~prefix:"" 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
+      let _, e, env = Gmp.Z.new_var ~loc ~name env kf t mk_stmts in
       e, adata, env, Typed_number.C_number, ""
     else begin
       assert (Logic_typing.is_integral_type t.term_type);

src/plugins/e-acsl/src/code_generator/translate_utils.ml

@@ -205,23 +205,8 @@ let comparison_to_exp
         match ity with
         | C_integer _ | C_float _ | Nan ->
           Cil.mkBinOp ~loc bop e1 e2, env
-        | Gmpz ->
-          let _, e, env = Env.new_var
-              ~loc
-              env
-              kf
-              t_opt
-              ~name
-              Cil.intType
-              (fun v _ ->
-                 [ Smart_stmt.rtl_call ~loc
-                     ~result:(Cil.var v)
-                     ~prefix:""
-                     "__gmpz_cmp"
-                     [ e1; e2 ] ])
-          in
-          Cil.new_exp ~loc (BinOp(bop, e, Cil.zero ~loc, Cil.intType)), env
-        | Rational -> Rational.cmp ~loc bop e1 e2 env kf t_opt
+        | Gmpz -> Gmp.Z.cmp ~loc name t_opt bop env kf e1 e2
+        | Rational -> Gmp.Q.cmp ~loc name t_opt bop env kf e1 e2
         | Real -> Error.not_yet "comparison involving real numbers"
       end
     | _, _ ->

src/plugins/e-acsl/src/code_generator/typed_number.ml

@@ -28,22 +28,9 @@ type strnum =
   | C_number      (* integers and floats included *)
 
 let add_cast ~loc ?name env kf ctx strnum t_opt e =
-  let mk_mpz e =
-    let _, e, env =
-      Env.new_var
-        ~loc
-        ?name
-        env
-        kf
-        t_opt
-        (Gmp_types.Z.t ())
-        (fun lv v -> [ Gmp.init_set ~loc (Cil.var lv) v e ])
-    in
-    e, env
-  in
   let e, env = match strnum with
-    | Str_Z -> mk_mpz e
-    | Str_R -> Rational.create ~loc ?name e env kf t_opt
+    | Str_Z -> Gmp.Z.create ~loc ?name t_opt env kf e
+    | Str_R -> Gmp.Q.create ~loc ?name t_opt env kf e
     | C_number -> e, env
   in
   match ctx with
@@ -58,7 +45,7 @@ let add_cast ~loc ?name env kf ctx strnum t_opt e =
     | false, true ->
       if Gmp_types.Q.is_t ty then
         (* R --> Z *)
-        Rational.cast_to_z ~loc ?name e env
+        Gmp.Q.cast_to_z ~loc ?name env e
       else
         (* C integer --> Z *)
         let e =
@@ -71,39 +58,20 @@ let add_cast ~loc ?name env kf ctx strnum t_opt e =
           else
             e
         in
-        mk_mpz e
+        Gmp.Z.create ~loc ?name t_opt env kf e
     | _, false ->
       if Gmp_types.Q.is_t ctx then
         if Gmp_types.Q.is_t (Cil.typeOf e) then (* R --> R *)
           e, env
         else (* C integer or Z --> R *)
-          Rational.create ~loc ?name e env kf t_opt
+          Gmp.Q.create ~loc ?name t_opt env kf e
       else if Gmp_types.Z.is_t ty || strnum = Str_Z then
         (* Z --> C type or the integer is represented by a string:
            anyway, it fits into a C integer: convert it *)
-        let fname, new_ty =
-          if Cil.isSignedInteger ctx then "__gmpz_get_si", Cil.longType
-          else "__gmpz_get_ui", Cil.ulongType
-        in
-        let _, e, env =
-          Env.new_var
-            ~loc
-            ?name
-            env
-            kf
-            None
-            new_ty
-            (fun v _ ->
-               [ Smart_stmt.rtl_call ~loc
-                   ~result:(Cil.var v)
-                   ~prefix:""
-                   fname
-                   [ e ] ])
-        in
-        e, env
+        Gmp.Z.add_cast ~loc ?name env kf ctx e
       else if Gmp_types.Q.is_t ty || strnum = Str_R then
         (* R --> C type or the real is represented by a string *)
-        Rational.add_cast ~loc ?name e env kf ctx
+        Gmp.Q.add_cast ~loc ?name env kf ctx e
       else
         (* C type --> another C type *)
         Cil.mkCastT ~force:false ~oldt:ty ~newt:ctx e, env