[eacsl] Extract some translation functions

- `tapp_to_exp` is moved to `Logic_functions`, with the existing
`Logic_function.tapp_to_exp` renamed to `function_to_exp` and moved as
an internal function;
- `name_of_mpz_arith_bop` is moved to `Gmp`;
- `add_cast` and `strnum` are moved to a new `Typed_number` module.

src/plugins/e-acsl/Makefile.in

@@ -83,11 +83,12 @@ SRC_CODE_GENERATOR:= \
 	label \
 	env \
 	rational \
+	typed_number \
+	logic_functions \
 	loops \
 	quantif \
 	at_with_lscope \
 	memory_translate \
-	logic_functions \
 	logic_array \
 	translate \
 	contract \

src/plugins/e-acsl/headers/header_spec.txt

@@ -122,6 +122,8 @@ src/code_generator/translate.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/translate.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/translate_annots.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/code_generator/translate_annots.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/typed_number.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/code_generator/typed_number.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/dependencies/dep_eva.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/dependencies/dep_eva.enabled.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/dependencies/dep_eva.disabled.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL

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

@@ -35,6 +35,23 @@ let apply_on_var ~loc funname e =
   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 | IndexPI | 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
 

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

@@ -24,6 +24,10 @@
 
 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] *)
 

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

@@ -283,7 +283,9 @@ let add_generated_functions globals =
   in
   List.rev rev_globals
 
-let tapp_to_exp ~loc fname env kf t li params_ty args =
+(* Generate (and memoize) the function body and create the call to the
+   generated function. *)
+let function_to_exp ~loc fname env kf t li params_ty args =
   let ret_ty = Typing.get_typ t in
   let gen tbl =
     let vi, kf, gen_body = generate_kf fname ~loc env ret_ty params_ty li in
@@ -342,6 +344,101 @@ let tapp_to_exp ~loc fname env kf t li params_ty args =
     ret_ty
     (fun vi _ -> [ Cil.mkStmtOneInstr ~valid_sid:true (mkcall vi) ])
 
+let tapp_to_exp kf env ?eargs tapp =
+  match tapp.term_node with
+  | Tapp(li, [], targs) ->
+    let loc = tapp.term_loc in
+    let fname = li.l_var_info.lv_name in
+    (* build the varinfo (as an expression) which stores the result of the
+       function call. *)
+    let _, e, env =
+      if Builtins.mem li.l_var_info.lv_name then
+        (* E-ACSL built-in function call *)
+        let args, env =
+          match eargs with
+          | None ->
+            List.fold_right
+              (fun targ (l, env) ->
+                 let e, env = !term_to_exp_ref kf env targ in
+                 e :: l, env)
+              targs
+              ([], env)
+          | Some eargs ->
+            if List.compare_lengths targs eargs != 0 then
+              Options.fatal
+                "[Tapp] unexpected number of arguments when calling %s"
+                fname;
+            eargs, env
+        in
+        Env.new_var
+          ~loc
+          ~name:(fname ^ "_app")
+          env
+          kf
+          (Some tapp)
+          (Misc.cty (Option.get li.l_type))
+          (fun vi _ ->
+             [ Smart_stmt.rtl_call ~loc
+                 ~result:(Cil.var vi)
+                 ~prefix:""
+                 fname
+                 args ])
+      else
+        (* build the arguments and compute the integer_ty of the parameters *)
+        let params_ty, args, env =
+          let eargs, env =
+            match eargs with
+            | None ->
+              List.fold_right
+                (fun targ (eargs, env) ->
+                   let e, env = !term_to_exp_ref kf env targ in
+                   e :: eargs, env)
+                targs
+                ([], env)
+            | Some eargs ->
+              if List.compare_lengths targs eargs != 0 then
+                Options.fatal
+                  "[Tapp] unexpected number of arguments when calling %s"
+                  fname;
+              eargs, env
+          in
+          try
+            List.fold_right2
+              (fun targ earg (params_ty, args, env) ->
+                 let param_ty = Typing.get_number_ty targ in
+                 let e, env =
+                   try
+                     let ty = Typing.typ_of_number_ty param_ty in
+                     Typed_number.add_cast
+                       ~loc
+                       env
+                       kf
+                       (Some ty)
+                       Typed_number.C_number
+                       (Some targ)
+                       earg
+                   with Typing.Not_a_number ->
+                     earg, env
+                 in
+                 param_ty :: params_ty, e :: args, env)
+              targs eargs
+              ([], [], env)
+          with Invalid_argument _ ->
+            Options.fatal
+              "[Tapp] unexpected number of arguments when calling %s"
+              fname
+        in
+        let gen_fname =
+          Varname.get ~scope:Varname.Global (Functions.RTL.mk_gen_name fname)
+        in
+        function_to_exp ~loc gen_fname env kf tapp li params_ty args
+    in
+    e, env
+  | _ ->
+    Options.fatal
+      "tapp_to_exp called with '%a' instead of Tapp term"
+      Printer.pp_term tapp
+
 (*
 Local Variables:
 compile-command: "make -C ../.."

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

@@ -37,10 +37,9 @@ open Cil_types
 val reset: unit -> unit
 
 val tapp_to_exp:
-  loc:location ->
-  string -> Env.t -> kernel_function ->
-  term -> logic_info -> Typing.number_ty list -> exp list ->
-  varinfo * exp * Env.t
+  kernel_function -> Env.t -> ?eargs:exp list -> term -> exp * Env.t
+(** Translate a Tapp term to an expression. If the optional argument [eargs] is
+    provided, then these expressions are used as arguments of the fonction. *)
 
 val add_generated_functions: global list -> global list
 (* @return the input list of globals in which the generated functions have been

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

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2020                                               *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Manipulate the type of numbers. *)
+
+type strnum =
+  | Str_Z         (* integers *)
+  | Str_R         (* reals *)
+  | 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
+    | C_number -> e, env
+  in
+  match ctx with
+  | None ->
+    e, env
+  | Some ctx ->
+    let ty = Cil.typeOf e in
+    match Gmp_types.Z.is_t ty, Gmp_types.Z.is_t ctx with
+    | true, true ->
+      (* Z --> Z *)
+      e, env
+    | false, true ->
+      if Gmp_types.Q.is_t ty then
+        (* R --> Z *)
+        Rational.cast_to_z ~loc ?name e env
+      else
+        (* C integer --> Z *)
+        let e =
+          if not (Cil.isIntegralType ty) && strnum = C_number then
+            (* special case for \null that must be casted to long: it is the
+               only non integral value that can be seen as an integer, while the
+               type system infers that it is C-representable (see
+               tests/runtime/null.i) *)
+            Cil.mkCast Cil.longType e (* \null *)
+          else
+            e
+        in
+        mk_mpz 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
+      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
+      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
+      else
+        (* C type --> another C type *)
+        Cil.mkCastT ~force:false ~oldt:ty ~newt:ctx e, env

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

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2020                                               *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Manipulate the type of numbers. *)
+
+open Cil_types
+
+(** Type of a string that represents a number.
+    Used when a string is required to encode a constant number because it is not
+    representable in any C type  *)
+type strnum =
+  | Str_Z         (* integers *)
+  | Str_R         (* reals *)
+  | C_number      (* integers and floats included *)
+
+(** [add_cast ~loc ?name env kf ctx sty t_opt e] convert number expression [e]
+    in a way that it is compatible with the given typing context [ctx].
+    [sty] indicates if the expression is a string representing a number (integer
+    or real) or directly a C number type.
+    [t_opt] is the term that is represented by the expression [e]. *)
+val add_cast:
+  loc:location ->
+  ?name:string ->
+  Env.t ->
+  kernel_function ->
+  typ option ->
+  strnum ->
+  term option ->
+  exp ->
+  exp * Env.t