From 48142bf8e3acc717d2cb519ea3a0f6e7a344330b Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Wed, 8 Sep 2021 10:10:30 +0200
Subject: [PATCH] [e-acsl] separate files for assigns clause generation
---
src/plugins/e-acsl/Makefile.in | 1 +
.../e-acsl/src/code_generator/genassigns.ml | 90 +++++++++++++++++++
.../e-acsl/src/code_generator/genassigns.mli | 37 ++++++++
.../src/code_generator/logic_functions.ml | 73 +--------------
4 files changed, 131 insertions(+), 70 deletions(-)
create mode 100644 src/plugins/e-acsl/src/code_generator/genassigns.ml
create mode 100644 src/plugins/e-acsl/src/code_generator/genassigns.mli
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 18869a85f29..914074b0c6b 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -83,6 +83,7 @@ SRC_CODE_GENERATOR:= \
assert \
rational \
typed_number \
+ genassigns \
logic_functions \
loops \
quantif \
diff --git a/src/plugins/e-acsl/src/code_generator/genassigns.ml b/src/plugins/e-acsl/src/code_generator/genassigns.ml
new file mode 100644
index 00000000000..630786709a2
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/genassigns.ml
@@ -0,0 +1,90 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+exception NoAssigns
+
+(*****************************************************************************)
+(****************** Generation of function assigns ***************************)
+(*****************************************************************************)
+
+(* If an argument contains a pointer type, then it is undecidable which assigns
+ clause should be generated, so skip the assigns generation in this case *)
+let rec is_ptr_free typ = match Cil.unrollType typ with
+ | TVoid _
+ | TInt (_, _)
+ | TFloat (_, _) -> true
+ | TPtr (_, _) -> false
+ | TArray (ty, _, _, _) -> is_ptr_free ty
+ | TFun (_, _, _, _) ->
+ (* a function cannot be an argument of a function *)
+ assert false
+ | TNamed (_, _) ->
+ (* The named types are unfolded with [Cil.unrolltype] *)
+ assert false
+ | TEnum (_, _)
+ | TBuiltin_va_list _ -> true
+ | TComp (cinfo, _, _) ->
+ match cinfo.cfields with
+ | None -> raise NoAssigns
+ | Some fields ->
+ List.for_all
+ (fun fi -> fi.fbitfield <> None || is_ptr_free fi.ftype)
+ fields
+
+(* For a GMP argument of a function, we generate an assigns from its address,
+ since these are the only semantically valid operations on integers.
+ For the argument [__e_acsl_mpz_struct * x], this function generates the
+ expression [*(( __e_acsl_mpz_struct * )x)] *)
+let deref_gmp_arg ~loc var =
+ Smart_exp.lval ~loc
+ (Mem (Cil.mkAddrOrStartOf ~loc (Var var , NoOffset)), NoOffset)
+
+let rec get_assigns_from ~loc env lprofile lv =
+ match lprofile with
+ | [] -> []
+ | lvar :: lvars ->
+ let var = Env.Logic_binding.get env lvar in
+ if is_ptr_free var.vtype then
+ Smart_exp.lval ~loc (Cil.var var) :: get_assigns_from ~loc env lvars lv
+ (* If the argument contains a pointer, but is an integer, then it is
+ necessarily a GMP type *)
+ else if lvar.lv_type = Linteger then
+ (deref_gmp_arg ~loc var) :: (get_assigns_from ~loc env lvars lv)
+ else begin
+ Options.warning ~current:true "skipping function %a when generating\
+ assigns because pointers as arguments\
+ is not yet supported"
+ Printer.pp_logic_var lv;
+ raise NoAssigns
+ end
+
+(* Special case when the function takes an extra argument as its result:
+ For the argument [__e_acsl_mpz_t *__retres_arg], this function generates the
+ expression [( *__retres_arg )[0]] *)
+let get_gmp_integer ~loc vi =
+ Smart_exp.lval
+ ~loc
+ (Mem
+ (Smart_exp.lval ~loc (Var vi, NoOffset)),
+ (Index (Cil.zero ~loc, NoOffset)))
diff --git a/src/plugins/e-acsl/src/code_generator/genassigns.mli b/src/plugins/e-acsl/src/code_generator/genassigns.mli
new file mode 100644
index 00000000000..a770607bd2c
--- /dev/null
+++ b/src/plugins/e-acsl/src/code_generator/genassigns.mli
@@ -0,0 +1,37 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+exception NoAssigns
+
+val get_assigns_from :
+ loc:Cil_types.location ->
+ Env.t ->
+ Cil_types.logic_var list ->
+ Cil_types.logic_var ->
+ Cil_types.exp list
+(* @returns the list of expressions that are allowed to be used to assign the
+ the result of a logic function *)
+
+val get_gmp_integer :
+ loc:Cil_types.location -> Cil_types.varinfo -> Cil_types.exp
+(* @returns the expression that gets assigned when the result of the function is
+ a pointer on a GMP type *)
diff --git a/src/plugins/e-acsl/src/code_generator/logic_functions.ml b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
index f442c14ec6c..dfb58431806 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_functions.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_functions.ml
@@ -23,8 +23,6 @@
open Cil_types
open Cil_datatype
-exception NoAssigns
-
(**************************************************************************)
(********************** Forward references ********************************)
(**************************************************************************)
@@ -58,71 +56,6 @@ let result_as_extra_argument = Gmp_types.Z.is_t
(* TODO: to be extended to any compound type? E.g. returning a struct is not
good practice... *)
-(*****************************************************************************)
-(****************** Generation of function assigns ***************************)
-(*****************************************************************************)
-
-(* If an argument contains a pointer type, then it is undecidable which assigns
- clause should be generated, so skip the assigns generation in this case *)
-let rec is_ptr_free typ = match Cil.unrollType typ with
- | TVoid _
- | TInt (_, _)
- | TFloat (_, _) -> true
- | TPtr (_, _) -> false
- | TArray (ty, _, _, _) -> is_ptr_free ty
- | TFun (_, _, _, _) ->
- (* a function cannot be an argument of a function *)
- assert false
- | TNamed (_, _) ->
- (* The named types are unfolded with [Cil.unrolltype] *)
- assert false
- | TEnum (_, _)
- | TBuiltin_va_list _ -> true
- | TComp (cinfo, _, _) ->
- match cinfo.cfields with
- | None -> raise NoAssigns
- | Some fields ->
- List.for_all
- (fun fi -> fi.fbitfield <> None || is_ptr_free fi.ftype)
- fields
-
-(* For a GMP argument of a function, we generate an assigns from its address,
- since these are the only semantically valid operations on integers.
- For the argument [__e_acsl_mpz_struct * x], this function generates the
- expression [*(( __e_acsl_mpz_struct * )x)] *)
-let deref_gmp_arg ~loc var =
- Smart_exp.lval ~loc
- (Mem (Cil.mkAddrOrStartOf ~loc (Var var , NoOffset)), NoOffset)
-
-let rec get_assigns_from ~loc env lprofile lv =
- match lprofile with
- | [] -> []
- | lvar :: lvars ->
- let var = Env.Logic_binding.get env lvar in
- if is_ptr_free var.vtype then
- Smart_exp.lval ~loc (Cil.var var) :: get_assigns_from ~loc env lvars lv
- (* If the argument contains a pointer, but is an integer, then it is
- necessarily a GMP type *)
- else if lvar.lv_type = Linteger then
- (deref_gmp_arg ~loc var) :: (get_assigns_from ~loc env lvars lv)
- else begin
- Options.warning ~current:true "skipping function %a when generating\
- assigns because pointers as arguments\
- is not yet supported"
- Printer.pp_logic_var lv;
- raise NoAssigns
- end
-
-(* Special case when the function takes an extra argument as its result:
- For the argument [__e_acsl_mpz_t *__retres_arg], this function generates the
- expression [( *__retres_arg )[0]] *)
-let get_gmp_integer ~loc vi =
- Smart_exp.lval
- ~loc
- (Mem
- (Smart_exp.lval ~loc (Var vi, NoOffset)),
- (Index (Cil.zero ~loc, NoOffset)))
-
(*****************************************************************************)
(****************** Generation of function bodies ****************************)
(*****************************************************************************)
@@ -281,13 +214,13 @@ let generate_kf ~loc fname env ret_ty params_ty li =
List.fold_left2 add env li.l_profile params
in
let assigns_from =
- try Some (get_assigns_from ~loc env li.l_profile li.l_var_info)
- with NoAssigns -> None
+ try Some (Genassigns.get_assigns_from ~loc env li.l_profile li.l_var_info)
+ with Genassigns.NoAssigns -> None
in
let assigned_var =
Logic_const.new_identified_term
(if res_as_extra_arg then
- Logic_utils.expr_to_term (get_gmp_integer ~loc ret_vi)
+ Logic_utils.expr_to_term (Genassigns.get_gmp_integer ~loc ret_vi)
else
Logic_const.tresult fundec.svar.vtype)
in
--
GitLab