From 02a4b536b8db456703632bf906c391d1f6860ad1 Mon Sep 17 00:00:00 2001
From: Thibaut Benjamin <thibaut.benjamin@cea.fr>
Date: Wed, 8 Sep 2021 10:11:17 +0200
Subject: [PATCH] [e-acsl] delete separate files for typing phase
---
src/plugins/e-acsl/Makefile.in | 1 -
.../e-acsl/src/analyses/memory_tracking.ml | 2 +-
.../e-acsl/src/analyses/preprocess_typing.ml | 131 ------------------
.../e-acsl/src/analyses/preprocess_typing.mli | 33 -----
src/plugins/e-acsl/src/analyses/typing.ml | 58 ++++++++
src/plugins/e-acsl/src/analyses/typing.mli | 22 ++-
.../e-acsl/src/code_generator/contract.ml | 8 +-
.../e-acsl/src/code_generator/injector.ml | 4 +-
.../e-acsl/src/code_generator/logic_array.ml | 2 +-
.../src/code_generator/memory_translate.ml | 2 +-
.../e-acsl/src/code_generator/translate.ml | 6 +-
11 files changed, 90 insertions(+), 179 deletions(-)
delete mode 100644 src/plugins/e-acsl/src/analyses/preprocess_typing.ml
delete mode 100644 src/plugins/e-acsl/src/analyses/preprocess_typing.mli
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 914074b0c6b..bd124212bf6 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -63,7 +63,6 @@ SRC_ANALYSES:= \
bound_variables \
interval \
typing \
- preprocess_typing \
literal_strings \
memory_tracking \
exit_points
diff --git a/src/plugins/e-acsl/src/analyses/memory_tracking.ml b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
index 6b8f0a27c88..ba85781275c 100644
--- a/src/plugins/e-acsl/src/analyses/memory_tracking.ml
+++ b/src/plugins/e-acsl/src/analyses/memory_tracking.ml
@@ -491,7 +491,7 @@ module rec Transfer
in
if stmt.ghost then
let rtes = Rte.stmt kf stmt in
- List.iter (Preprocess_typing.preprocess_rte ~lenv:[]) rtes;
+ List.iter (Typing.preprocess_rte ~lenv:[]) rtes;
List.fold_left
(fun state a -> register_code_annot kf a state) state rtes
else
diff --git a/src/plugins/e-acsl/src/analyses/preprocess_typing.ml b/src/plugins/e-acsl/src/analyses/preprocess_typing.ml
deleted file mode 100644
index bd15a8bf308..00000000000
--- a/src/plugins/e-acsl/src/analyses/preprocess_typing.ml
+++ /dev/null
@@ -1,131 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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
-
-let typer_visitor lenv = object
- inherit Visitor.frama_c_inplace
-
- (* Only type the globals that do not come from the Rtl *)
- method !vglob_aux =
- function
- (* library functions and built-ins *)
- | GFun({ svar = vi }, _) when Builtins.mem vi.vname ->
- Cil.SkipChildren
-
- | GFun({ svar = vi }, _)
- when Misc.is_fc_or_compiler_builtin vi ->
- Cil.SkipChildren
-
- | g when Rtl.Symbols.mem_global g ->
- Cil.SkipChildren
-
- | GFun({svar = vi}, _) ->
- let kf = try Globals.Functions.get vi with Not_found -> assert false in
- if Functions.check kf then Cil.DoChildren else Cil.SkipChildren
-
- (* other globals: nothing to do *)
- | GFunDecl _
- | GVarDecl _
- | GVar _
- | GType _
- | GCompTag _
- | GCompTagDecl _
- | GEnumTag _
- | GEnumTagDecl _
- | GAsm _
- | GPragma _
- | GText _
- | GAnnot _
- -> Cil.SkipChildren
-
-<<<<<<< HEAD
-<<<<<<< variant A
- | _ -> Cil.DoChildren
->>>>>>> variant B
- method !vpredicate p =
- Error.generic_handle (Typing.type_named_predicate ~lenv) () p;
- Cil.SkipChildren
- method !vpredicate p =
- Error.generic_handle (Typing.type_named_predicate ~lenv) () p; Cil.SkipChildren
-
- method !vspec spec =
- List.iter (fun b -> (List.iter (fun p -> ignore (Visitor.visitFramacIdPredicate self p)) b.b_assumes)) spec.spec_behavior;
- List.iter (type_requires self (Option.get self#current_kf) (self#current_kinstr)) spec.spec_behavior;
- List.iter (type_post_conditions self (Option.get self#current_kf) self#current_kinstr) spec.spec_behavior;
- Cil.SkipChildren
-
- method !vcode_annot annot =
- match annot.annot_content with
- | AAssert(_, _) | AVariant(_, _) ->
- let translate = try
- !must_translate_ref
- (Property.ip_of_code_annot_single
- (Option.get self#current_kf)
- (Option.get self#current_stmt)
- annot)
- with Invalid_argument _ -> true
- in
- if translate then
- Cil.DoChildren
- else
- Cil.SkipChildren
- | AStmtSpec(l, _) ->
- if l <> [] then Cil.SkipChildren
- else Cil.DoChildren
- | AInvariant(l, _, _) ->
- let translate =
- try !must_translate_ref
- (Property.ip_of_code_annot_single
- (Option.get self#current_kf)
- (Option.get self#current_stmt)
- annot)
- with Invalid_argument _ -> true
- in if translate then
- if l <> [] then
- Cil.SkipChildren
- else Cil.DoChildren
- else Cil.SkipChildren
- | AAssigns _ -> Cil.SkipChildren
- | AAllocation _ -> Cil.SkipChildren
- | APragma _ -> Cil.SkipChildren
- | AExtended _ -> Cil.SkipChildren
-
-=======
->>>>>>> e54ebd15af9... [e-acsl] simplify typing visitor
-end
-
-let type_program ast =
- Visitor.visitFramacFileSameGlobals (typer_visitor []) ast
-
-let type_code_annot lenv annot =
- ignore (Visitor.visitFramacCodeAnnotation (typer_visitor lenv) annot)
-
-let preprocess_predicate lenv p =
- Predicate_normalizer.preprocess_predicate p;
- Bound_variables.preprocess_predicate p;
- ignore (Visitor.visitFramacPredicate (typer_visitor lenv) p)
-
-let preprocess_rte ~lenv rte =
- Predicate_normalizer.preprocess_annot rte;
- Bound_variables.preprocess_annot rte;
- type_code_annot lenv rte
diff --git a/src/plugins/e-acsl/src/analyses/preprocess_typing.mli b/src/plugins/e-acsl/src/analyses/preprocess_typing.mli
deleted file mode 100644
index 6b9b6dd1205..00000000000
--- a/src/plugins/e-acsl/src/analyses/preprocess_typing.mli
+++ /dev/null
@@ -1,33 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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
-
-val type_program : file -> unit
-(** compute and store the type of all the terms that will be translated
- in a program *)
-
-val preprocess_predicate : Typing.Function_params_ty.t -> predicate -> unit
-(** compute and store the types of all the terms in a given predicate *)
-
-val preprocess_rte : lenv:Typing.Function_params_ty.t -> code_annotation -> unit
-(** compute and store the type of all the terms in a code annotation *)
diff --git a/src/plugins/e-acsl/src/analyses/typing.ml b/src/plugins/e-acsl/src/analyses/typing.ml
index bbde25130c9..798600441b0 100644
--- a/src/plugins/e-acsl/src/analyses/typing.ml
+++ b/src/plugins/e-acsl/src/analyses/typing.ml
@@ -956,6 +956,64 @@ let get_cast_of_predicate ~lenv p =
let clear = Memo.clear
+open Cil_types
+
+let typer_visitor lenv = object
+ inherit Visitor.frama_c_inplace
+
+ method !vglob_aux =
+ function
+ (* library functions and built-ins *)
+ | GFun({ svar = vi }, _) when Builtins.mem vi.vname ->
+ Cil.SkipChildren
+
+ | GFun({ svar = vi }, _)
+ when Misc.is_fc_or_compiler_builtin vi ->
+ Cil.SkipChildren
+
+ | g when Rtl.Symbols.mem_global g ->
+ Cil.SkipChildren
+
+ | GFun({svar = vi}, _) ->
+ let kf = try Globals.Functions.get vi with Not_found -> assert false in
+ if Functions.check kf then Cil.DoChildren else Cil.SkipChildren
+
+ (* other globals: nothing to do *)
+ | GFunDecl _
+ | GVarDecl _
+ | GVar _
+ | GType _
+ | GCompTag _
+ | GCompTagDecl _
+ | GEnumTag _
+ | GEnumTagDecl _
+ | GAsm _
+ | GPragma _
+ | GText _
+ | GAnnot _
+ -> Cil.SkipChildren
+
+ method !vpredicate p =
+ Error.generic_handle (type_named_predicate ~lenv) () p;
+ Cil.SkipChildren
+end
+
+let type_program ast =
+ Visitor.visitFramacFileSameGlobals (typer_visitor []) ast
+
+let type_code_annot lenv annot =
+ ignore (Visitor.visitFramacCodeAnnotation (typer_visitor lenv) annot)
+
+let preprocess_predicate lenv p =
+ Predicate_normalizer.preprocess_predicate p;
+ Bound_variables.preprocess_predicate p;
+ ignore (Visitor.visitFramacPredicate (typer_visitor lenv) p)
+
+let preprocess_rte ~lenv rte =
+ Predicate_normalizer.preprocess_annot rte;
+ Bound_variables.preprocess_annot rte;
+ type_code_annot lenv rte
+
(*
Local Variables:
compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/analyses/typing.mli b/src/plugins/e-acsl/src/analyses/typing.mli
index e56f54b73e9..5bf1e0c9349 100644
--- a/src/plugins/e-acsl/src/analyses/typing.mli
+++ b/src/plugins/e-acsl/src/analyses/typing.mli
@@ -60,7 +60,8 @@ type number_ty = private
| Real
| Nan
-module Function_params_ty: Datatype.S_with_collections with type t = number_ty list
+module Function_params_ty:
+ Datatype.S_with_collections with type t = number_ty list
(** {3 Smart constructors} *)
@@ -96,7 +97,12 @@ val join: number_ty -> number_ty -> number_ty
(** {2 Typing} *)
(******************************************************************************)
-val type_term: use_gmp_opt:bool -> ?ctx:number_ty -> ?lenv:Function_params_ty.t -> term -> unit
+val type_term:
+ use_gmp_opt:bool ->
+ ?ctx:number_ty ->
+ ?lenv:Function_params_ty.t ->
+ term ->
+ unit
(** Compute the type of each subterm of the given term in the given context. If
[use_gmp_opt] is false, then the conversion to the given context is done
even if -e-acsl-gmp-only is set. *)
@@ -125,7 +131,8 @@ val get_integer_op: lenv:Function_params_ty.t -> term -> number_ty
It is meaningless to call this function over a non-arithmetical/logical
operator. *)
-val get_integer_op_of_predicate: lenv:Function_params_ty.t -> predicate -> number_ty
+val get_integer_op_of_predicate:
+ lenv:Function_params_ty.t -> predicate -> number_ty
(** @return the infered type for the top operation of the given predicate. *)
val get_typ: lenv:Function_params_ty.t -> term -> typ
@@ -156,6 +163,15 @@ val ty_of_interv: ?ctx:number_ty -> Interval.t -> number_ty
val typ_of_lty: logic_type -> typ
(** @return the C type that correponds to the given logic type. *)
+val type_program : file -> unit
+(** compute and store the type of all the terms that will be translated
+ in a program *)
+
+val preprocess_predicate : Function_params_ty.t -> predicate -> unit
+(** compute and store the types of all the terms in a given predicate *)
+
+val preprocess_rte : lenv:Function_params_ty.t -> code_annotation -> unit
+(** compute and store the type of all the terms in a code annotation *)
(*
Local Variables:
diff --git a/src/plugins/e-acsl/src/code_generator/contract.ml b/src/plugins/e-acsl/src/code_generator/contract.ml
index 5b4947fcf7f..126fa5a0c6b 100644
--- a/src/plugins/e-acsl/src/code_generator/contract.ml
+++ b/src/plugins/e-acsl/src/code_generator/contract.ml
@@ -178,7 +178,7 @@ let assumes_predicate env assumes =
Logic_const.ptrue
assumes
in
- Preprocess_typing.preprocess_predicate (Env.Local_vars.get env) p;
+ Typing.preprocess_predicate (Env.Local_vars.get env) p;
p
let create ~loc spec =
@@ -364,7 +364,7 @@ let check_requires kf kinstr env contract =
let requires =
{ requires with pred_name = b.b_name :: requires.pred_name }
in
- Preprocess_typing.preprocess_predicate (Env.Local_vars.get env) requires;
+ Typing.preprocess_predicate (Env.Local_vars.get env) requires;
(* Create runtime check *)
let adata, env = Assert.empty ~loc kf env in
let requires_e, adata, env =
@@ -686,7 +686,9 @@ let check_post_conds kf kinstr env contract =
{ post_cond with
pred_name = b.b_name :: post_cond.pred_name }
in
- Preprocess_typing.preprocess_predicate (Env.Local_vars.get env) post_cond;
+ Typing.preprocess_predicate
+ (Env.Local_vars.get env)
+ post_cond;
(* Create runtime check *)
let adata, env = Assert.empty ~loc kf env in
let post_cond_e, adata, env =
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index be5660c79af..23e1965ce62 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -213,7 +213,7 @@ let add_new_block_in_stmt env kf stmt =
(* translate potential RTEs of ghost code *)
let rtes = Rte.stmt ~warn:false kf stmt in
List.iter
- (Preprocess_typing.preprocess_rte ~lenv:(Env.Local_vars.get env))
+ (Typing.preprocess_rte ~lenv:(Env.Local_vars.get env))
rtes;
Translate.translate_rte_annots Printer.pp_stmt stmt kf env rtes
end else
@@ -877,7 +877,7 @@ let inject () =
Options.feedback ~level:2
"typing annotations in project %a"
Project.pretty current_project;
- Preprocess_typing.type_program ast;
+ Typing.type_program ast;
Options.feedback ~level:2
"injecting annotations as code in project %a"
Project.pretty current_project;
diff --git a/src/plugins/e-acsl/src/code_generator/logic_array.ml b/src/plugins/e-acsl/src/code_generator/logic_array.ml
index 3b6999e95d3..adf0734cc3d 100644
--- a/src/plugins/e-acsl/src/code_generator/logic_array.ml
+++ b/src/plugins/e-acsl/src/code_generator/logic_array.ml
@@ -240,7 +240,7 @@ let comparison_to_exp ~loc kf env ~name bop array1 array2 =
(Rle, Logic_utils.expr_to_term len, Logic_utils.expr_to_term len_orig)
in
let p = { p with pred_name = "array_coercion" :: p.pred_name } in
- Preprocess_typing.preprocess_predicate (Env.Local_vars.get env) p;
+ Typing.preprocess_predicate (Env.Local_vars.get env) p;
let adata, env = Assert.empty ~loc kf env in
let adata, env =
Assert.register ~loc kf env "destination length" len adata
diff --git a/src/plugins/e-acsl/src/code_generator/memory_translate.ml b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
index efa66fcbe4e..d92926c8163 100644
--- a/src/plugins/e-acsl/src/code_generator/memory_translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/memory_translate.ml
@@ -469,7 +469,7 @@ let call_with_tset
in
(* There's no more quantifiers in the arguments now, we can call back
[predicate_to_exp] to translate the predicate as usual *)
- Preprocess_typing.preprocess_predicate (Env.Local_vars.get env) p_quantified;
+ Typing.preprocess_predicate (Env.Local_vars.get env) p_quantified;
!predicate_to_exp_ref ~adata kf env p_quantified
| [] ->
(* No arguments require quantifiers, so we can directly translate the
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index ad07712f4dc..a56fc42a945 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -604,7 +604,7 @@ and context_insensitive_term_to_exp ~adata kf env t =
in
let e1_guard_cond, env =
let pred = Logic_const.prel ~loc (Rge, t1, zero) in
- Preprocess_typing.preprocess_predicate (Env.Local_vars.get env) pred;
+ Typing.preprocess_predicate (Env.Local_vars.get env) pred;
let cond, env =
Assert.runtime_check
~adata:adata1
@@ -1167,7 +1167,7 @@ and predicate_content_to_exp ~adata ?name kf env p =
let p = { p with pred_name = name :: p.pred_name } in
let tp = Logic_const.toplevel_predicate ~kind:Assert p in
let annot = Logic_const.new_code_annotation (AAssert ([],tp)) in
- Preprocess_typing.preprocess_rte (Env.Local_vars.get env) annot;
+ Typing.preprocess_rte (Env.Local_vars.get env) annot;
translate_rte_annots Printer.pp_code_annotation annot kf env [annot]
)
env
@@ -1303,7 +1303,7 @@ and translate_rte ?filter kf env e =
| Some f -> List.filter f l
| None -> l
in
- List.iter (Preprocess_typing.preprocess_rte ~lenv:(Env.Local_vars.get env)) l;
+ List.iter (Typing.preprocess_rte ~lenv:(Env.Local_vars.get env)) l;
translate_rte_annots Printer.pp_exp e kf env l
and translate_predicate ?pred_to_print kf env p =
--
GitLab