[eacsl] Move analyses types and datatypes into their own modules

src/plugins/e-acsl/Makefile.in

@@ -56,7 +56,12 @@ SRC_PROJECT_INITIALIZER:=\
   $(addprefix src/project_initializer/, $(SRC_PROJECT_INITIALIZER))
 
 # analyses
+ANALYSES_CMI:= \
+	analyses_types
+ANALYSES_CMI:=$(addprefix src/analyses/, $(ANALYSES_CMI))
+
 SRC_ANALYSES:= \
+	analyses_datatype \
 	rte \
 	lscope \
 	e_acsl_visitor \
@@ -128,6 +133,7 @@ PLUGIN_CMO:= src/local_config \
 	src/main
 PLUGIN_CMI:= \
 	$(LIBRARIES_CMI) \
+	$(ANALYSES_CMI) \
 	$(CODE_GENERATOR_CMI)
 PLUGIN_HAS_MLI:=yes
 PLUGIN_DISTRIBUTED:=yes

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

@@ -79,6 +79,9 @@ share/e-acsl/observation_model/e_acsl_observation_model.c: CEA_LGPL_OR_PROPRIETA
 share/e-acsl/observation_model/e_acsl_observation_model.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 share/e-acsl/e_acsl.h: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 share/e-acsl/e_acsl_rtl.c: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/analyses_datatype.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/analyses_datatype.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
+src/analyses/analyses_types.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/bound_variables.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/bound_variables.mli: CEA_LGPL_OR_PROPRIETARY.E_ACSL
 src/analyses/e_acsl_visitor.ml: CEA_LGPL_OR_PROPRIETARY.E_ACSL

src/plugins/e-acsl/src/analyses/analyses_datatype.ml

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2021                                               *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Datatypes for analyses types *)
+
+open Cil_datatype
+open Analyses_types
+
+module PredOrTerm =
+  Datatype.Make_with_collections
+    (struct
+      type t = pred_or_term
+
+      let name = "E_ACSL.PredOrTerm"
+
+      let reprs =
+        let reprs =
+          List.fold_left
+            (fun reprs t -> PoT_term t :: reprs)
+            []
+            Term.reprs
+        in
+        List.fold_left
+          (fun reprs p -> PoT_pred p :: reprs)
+          reprs
+          Predicate.reprs
+
+      include Datatype.Undefined
+
+      let compare pot1 pot2 =
+        match pot1, pot2 with
+        | PoT_pred _, PoT_term _ -> -1
+        | PoT_term _, PoT_pred _ -> 1
+        | PoT_pred p1, PoT_pred p2 -> PredicateStructEq.compare p1 p2
+        | PoT_term t1, PoT_term t2 -> Term.compare t1 t2
+
+      let equal = Datatype.from_compare
+
+      let hash = function
+        | PoT_pred p -> 7 * PredicateStructEq.hash p
+        | PoT_term t -> 97 * Term.hash t
+
+      let pretty fmt = function
+        | PoT_pred p -> Printer.pp_predicate fmt p
+        | PoT_term t -> Printer.pp_term fmt t
+
+      let varname _ = "pred_or_term"
+    end)

src/plugins/e-acsl/src/analyses/analyses_datatype.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2021                                               *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Datatypes for analyses types *)
+
+open Analyses_types
+
+module PredOrTerm: Datatype.S_with_collections with type t = pred_or_term

src/plugins/e-acsl/src/analyses/analyses_types.mli

+(**************************************************************************)
+(*                                                                        *)
+(*  This file is part of the Frama-C's E-ACSL plug-in.                    *)
+(*                                                                        *)
+(*  Copyright (C) 2012-2021                                               *)
+(*    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).            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(** Types used by E-ACSL analyses *)
+
+open Cil_types
+
+type lscope_var =
+  | Lvs_let of logic_var * term (* the expression to which the lv is binded *)
+  | Lvs_quantif of term * relation * logic_var * relation * term
+  | Lvs_formal of logic_var * logic_info (* the logic definition *)
+  | Lvs_global of logic_var * term (* same as Lvs_let *)
+
+type lscope = lscope_var list
+
+type pred_or_term =
+  | PoT_pred of predicate
+  | PoT_term of term

src/plugins/e-acsl/src/analyses/logic_normalizer.ml

@@ -21,8 +21,7 @@
 (**************************************************************************)
 
 open Cil_types
-
-type pred_or_term = Lscope.pred_or_term
+open Analyses_types
 
 module Id_predicate =
   Datatype.Make_with_collections
@@ -53,7 +52,7 @@ end = struct
 
   let get_pred p =
     try Id_predicate.Hashtbl.find tbl_pred p
-    with Not_found -> Lscope.PoT_pred p
+    with Not_found -> PoT_pred p
 
   let memo_pred process p =
     try ignore (Id_predicate.Hashtbl.find tbl_pred p) with
@@ -98,7 +97,7 @@ let preprocess_pred ~loc p =
           | Pvalid _ -> Logic_const.pvalid ~loc (llabel, t)
           | _ -> assert false
         in
-        Some (Lscope.PoT_pred (Logic_const.pand ~loc (init, p_copy)))
+        Some (PoT_pred (Logic_const.pand ~loc (init, p_copy)))
       | _ -> None
     end
   | _ -> None

src/plugins/e-acsl/src/analyses/logic_normalizer.mli

@@ -30,6 +30,7 @@
 *)
 
 open Cil_types
+open Analyses_types
 
 val preprocess : file -> unit
 (** Preprocess all the predicates of the ast and store the results *)
@@ -41,7 +42,7 @@ val preprocess_annot : code_annotation -> unit
 val preprocess_predicate : predicate -> unit
 (** Preprocess a predicate and its children and store the results  *)
 
-val get_pred : predicate -> Lscope.pred_or_term
+val get_pred : predicate -> pred_or_term
 (** Retrieve the preprocessed form of a predicate *)
 val get_term : term -> term
 (** Retrieve the preprocessed form of a term *)

src/plugins/e-acsl/src/analyses/lscope.ml

@@ -21,14 +21,9 @@
 (**************************************************************************)
 
 open Cil_types
+open Analyses_types
 
-type lscope_var =
-  | Lvs_let of logic_var * term
-  | Lvs_quantif of term * relation * logic_var * relation * term
-  | Lvs_formal of logic_var * logic_info
-  | Lvs_global of logic_var * term
-
-type t = lscope_var list
+type t = lscope
 (* The logic scope is usually small, so a list is fine instead of a Map *)
 
 let empty = []
@@ -47,8 +42,6 @@ let exists lv t =
   in
   List.exists is_lv t
 
-type pred_or_term = PoT_pred of predicate | PoT_term of term
-
 exception Lscope_used
 let is_used lscope pot =
   let o = object inherit Visitor.frama_c_inplace

src/plugins/e-acsl/src/analyses/lscope.mli

@@ -20,19 +20,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-open Cil_types
+open Analyses_types
 
 (* Handle the logic scope of a term.
    We define the logic scope of a term [t] to be the set of PURELY logic
    variables that are bound in [t] in case of use. *)
 
-type lscope_var =
-  | Lvs_let of logic_var * term (* the expression to which the lv is binded *)
-  | Lvs_quantif of term * relation * logic_var * relation * term
-  | Lvs_formal of logic_var * logic_info (* the logic definition *)
-  | Lvs_global of logic_var * term (* same as Lvs_let *)
-
-type t
+type t = lscope
 
 val empty: t
 (* Create an empty logic scope. *)
@@ -48,7 +42,6 @@ val get_all: t -> lscope_var list
    The first element is the first [lscope_var] that was added to [t], the
    second element is the second [lscope_var] that was added to [t], an so on. *)
 
-type pred_or_term = PoT_pred of predicate | PoT_term of term
 val is_used: t -> pred_or_term -> bool
 (* [is_used lscope pot] returns [true] iff [pot] uses a variable from
    [lscope]. *)

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

@@ -21,6 +21,7 @@
 (**************************************************************************)
 
 open Cil_types
+open Analyses_types
 
 (**************************************************************************)
 (********************** Forward references ********************************)
@@ -85,10 +86,10 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
   match lscope with
   | [] ->
     sizes_and_shifts
-  | Lscope.Lvs_quantif(tmin, _, _,  _, tmax) ::_
+  | Lvs_quantif(tmin, _, _,  _, tmax) ::_
     when Misc.term_has_lv_from_vi tmin || Misc.term_has_lv_from_vi tmax ->
     Error.not_yet "\\at with logic variable linked to C variable"
-  | Lscope.Lvs_quantif(tmin, rel1, lv, rel2, tmax) :: lscope' ->
+  | Lvs_quantif(tmin, rel1, lv, rel2, tmax) :: lscope' ->
     let t_size = Logic_const.term ~loc (TBinOp(MinusA, tmax, tmin)) Linteger in
     let t_size = match rel1, rel2 with
       | Rle, Rle ->
@@ -146,14 +147,14 @@ let rec sizes_and_shifts_from_quantifs ~loc kf lscope sizes_and_shifts =
     (* Returning *)
     let sizes_and_shifts = (t_size, t_shifted) :: sizes_and_shifts in
     sizes_and_shifts_from_quantifs ~loc kf lscope' sizes_and_shifts
-  | (Lscope.Lvs_let(_, t) | Lscope.Lvs_global(_, t)) :: _
+  | (Lvs_let(_, t) | Lvs_global(_, t)) :: _
     when Misc.term_has_lv_from_vi t ->
     Error.not_yet "\\at with logic variable linked to C variable"
-  | Lscope.Lvs_let _ :: lscope' ->
+  | Lvs_let _ :: lscope' ->
     sizes_and_shifts_from_quantifs ~loc kf lscope' sizes_and_shifts
-  | Lscope.Lvs_formal _ :: _ ->
+  | Lvs_formal _ :: _ ->
     Error.not_yet "\\at using formal variable of a logic function"
-  | Lscope.Lvs_global _ :: _ ->
+  | Lvs_global _ :: _ ->
     Error.not_yet "\\at using global logic variable"
 
 let size_from_sizes_and_shifts ~loc = function
@@ -240,9 +241,9 @@ let to_exp ~loc kf env pot label =
   in
   (* Creating the pointer *)
   let ty = match pot with
-    | Lscope.PoT_pred _ ->
+    | PoT_pred _ ->
       Cil.intType
-    | Lscope.PoT_term t ->
+    | PoT_term t ->
       let lenv = (Env.Local_vars.get env) in
       begin match Typing.get_number_ty ~lenv t with
         | Typing.(C_integer _ | C_float _ | Nan) ->
@@ -310,7 +311,7 @@ let to_exp ~loc kf env pot label =
     let term_to_exp = !term_to_exp_ref ~adata:Assert.no_data in
     let named_predicate_to_exp = !predicate_to_exp_ref ~adata:Assert.no_data in
     match pot with
-    | Lscope.PoT_pred p ->
+    | PoT_pred p ->
       let env = Env.push env in
       let lval, env = lval_at_index ~loc kf env (e_at, vi_at, t_index) in
       let e, _, env = named_predicate_to_exp kf env p in
@@ -324,7 +325,7 @@ let to_exp ~loc kf env pot label =
       (* We CANNOT return [block.bstmts] because it does NOT contain
          variable declarations. *)
       [ Smart_stmt.block_stmt block ], env
-    | Lscope.PoT_term t ->
+    | PoT_term t ->
       begin match Typing.get_number_ty ~lenv:(Env.Local_vars.get env) t with
         | Typing.(C_integer _ | C_float _ | Nan) ->
           let env = Env.push env in

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

@@ -22,6 +22,7 @@
 
 open Cil_types
 open Cil_datatype
+open Analyses_types
 
 (* Convert \at on terms or predicates in which we can find purely
    logic variable. *)
@@ -32,7 +33,7 @@ open Cil_datatype
 
 val to_exp:
   loc:Location.t -> kernel_function -> Env.t ->
-  Lscope.pred_or_term -> logic_label -> exp * Env.t
+  pred_or_term -> logic_label -> exp * Env.t
 
 (*****************************************************************************)
 (**************************** Handling memory ********************************)

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

@@ -21,6 +21,7 @@
 (**************************************************************************)
 
 open Cil_types
+open Analyses_types
 open Contract_types
 
 (** Environments.
@@ -129,7 +130,7 @@ module Logic_scope: sig
   val get: t -> Lscope.t
   (** Return the logic scope associated to the environment. *)
 
-  val extend: t -> Lscope.lscope_var -> t
+  val extend: t -> lscope_var -> t
   (** Add a new logic variable with its associated information in the
       logic scope of the environment. *)
 

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

@@ -22,6 +22,7 @@
 
 open Cil
 open Cil_types
+open Analyses_types
 
 (**************************************************************************)
 (********************** Forward references ********************************)
@@ -291,7 +292,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
   match lscope_vars with
   | [] ->
     mk_innermost_block env
-  | Lscope.Lvs_quantif(t1, rel1, logic_x, rel2, t2) :: lscope_vars' ->
+  | Lvs_quantif(t1, rel1, logic_x, rel2, t2) :: lscope_vars' ->
     assert (rel1 == Rle && rel2 == Rlt);
     Typing.type_term ~use_gmp_opt:false ~lenv t1;
     Typing.type_term ~use_gmp_opt:false ~lenv t2;
@@ -418,7 +419,7 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     (* remove logic binding before returning *)
     Env.Logic_binding.remove env logic_x;
     [ start ;  stmt ], env
-  | Lscope.Lvs_let(lv, t) :: lscope_vars' ->
+  | Lvs_let(lv, t) :: lscope_vars' ->
     let ty = Typing.get_typ ~lenv t in
     let vi_of_lv, exp_of_lv, env = Env.Logic_binding.add ~ty env kf lv in
     let e, _, env = term_to_exp kf env t in
@@ -434,10 +435,10 @@ let rec mk_nested_loops ~loc mk_innermost_block kf env lscope_vars =
     Env.Logic_binding.remove env lv;
     (* return *)
     let_stmt :: stmts, env
-  | Lscope.Lvs_formal _ :: _ ->
+  | Lvs_formal _ :: _ ->
     Error.not_yet
       "creating nested loops from formal variable of a logic function"
-  | Lscope.Lvs_global _ :: _ ->
+  | Lvs_global _ :: _ ->
     Error.not_yet
       "creating nested loops from global logic variable"
 

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

@@ -23,6 +23,7 @@
 (** Loop specific actions. *)
 
 open Cil_types
+open Analyses_types
 
 (**************************************************************************)
 (************************* Loop annotations *******************************)
@@ -40,7 +41,7 @@ val handle_annotations:
 
 val mk_nested_loops:
   loc:location -> (Env.t -> stmt list * Env.t) -> kernel_function -> Env.t ->
-  Lscope.lscope_var list -> stmt list * Env.t
+  lscope_var list -> stmt list * Env.t
 (** [mk_nested_loops ~loc mk_innermost_block kf env lvars] creates nested
     loops (with the proper statements for initializing the loop counters)
     from the list of logic variables [lvars]. Quantified variables create

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

@@ -22,6 +22,7 @@
 
 open Cil_types
 open Cil
+open Analyses_types
 
 (** Forward reference for [Translate_predicates.to_exp]. *)
 let predicate_to_exp_ref
@@ -92,7 +93,7 @@ let convert kf env loc ~is_forall quantif =
          and update logic scope in the process *)
       let lvs_guards, env = List.fold_right
           (fun (t1, lv, t2) (lvs_guards, env) ->
-             let lvs = Lscope.Lvs_quantif (t1, Rle, lv, Rlt, t2) in
+             let lvs = Lvs_quantif (t1, Rle, lv, Rlt, t2) in
              let env = Env.Logic_scope.extend env lvs in
              lvs :: lvs_guards, env)
           bound_vars

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

@@ -24,6 +24,7 @@
 
 open Cil_types
 open Cil_datatype
+open Analyses_types
 let dkey = Options.Dkey.translation
 
 (**************************************************************************)
@@ -180,7 +181,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
                (Translate_utils.conditional_to_exp ~loc kf None e1 res2 res3)
            ))
   | Plet(li, p) ->
-    let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
+    let lvs = Lvs_let(li.l_var_info, Misc.term_of_li li) in
     let env = Env.Logic_scope.extend env lvs in
     let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
     let e, adata, env = to_exp ~adata kf env p in
@@ -194,7 +195,7 @@ let rec predicate_content_to_exp ~adata ?name kf env p =
     to_exp ~adata kf env p
   | Pat(p', label) ->
     let lscope = Env.Logic_scope.get env in
-    let pot = Lscope.PoT_pred p' in
+    let pot = PoT_pred p' in
     if Lscope.is_used lscope pot then
       let e, env = At_with_lscope.to_exp ~loc kf env pot label in
       let adata, env = Assert.register_pred ~loc kf env p e adata in

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

@@ -23,6 +23,7 @@
 (** Generate C implementations of E-ACSL terms. *)
 
 open Cil_types
+open Analyses_types
 let dkey = Options.Dkey.translation
 
 (**************************************************************************)
@@ -797,7 +798,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
     e, adata, env, Typed_number.C_number, ""
   | Tat(t', label) ->
     let lscope = Env.Logic_scope.get env in
-    let pot = Lscope.PoT_term t' in
+    let pot = PoT_term t' in
     if Lscope.is_used lscope pot then
       let e, env = At_with_lscope.to_exp ~loc kf env pot label in
       let adata, env = Assert.register_term ~loc kf env t e adata in
@@ -854,7 +855,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
   | Tcomprehension _ -> Env.not_yet env "tset comprehension"
   | Trange _ -> Env.not_yet env "range"
   | Tlet(li, t) ->
-    let lvs = Lscope.Lvs_let(li.l_var_info, Misc.term_of_li li) in
+    let lvs = Lvs_let(li.l_var_info, Misc.term_of_li li) in
     let env = Env.Logic_scope.extend env lvs in
     let adata, env = Translate_utils.env_of_li ~adata ~loc kf env li in
     let e, adata, env = to_exp ~adata kf env t in