From 9357fe5443b9333aabf19ddd9c2284c62a400f02 Mon Sep 17 00:00:00 2001
From: thibautbenjamin <thibaut.benjamin@polytechnique.edu>
Date: Mon, 19 Jul 2021 15:22:53 +0200
Subject: [PATCH] [e-acsl] preprocessing phase for \valid predicates
---
src/plugins/e-acsl/Makefile.in | 7 +-
.../src/analyses/preprocess_predicates.ml | 135 ++++++++++++++++++
.../src/analyses/preprocess_predicates.mli | 9 ++
.../e-acsl/src/code_generator/injector.ml | 1 +
.../e-acsl/src/code_generator/translate.ml | 24 ----
5 files changed, 149 insertions(+), 27 deletions(-)
create mode 100644 src/plugins/e-acsl/src/analyses/preprocess_predicates.ml
create mode 100644 src/plugins/e-acsl/src/analyses/preprocess_predicates.mli
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 0d9786c27d7..4009f65874b 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -58,14 +58,15 @@ SRC_PROJECT_INITIALIZER:=\
# analyses
SRC_ANALYSES:= \
rte \
- bound_variables \
+ lscope \
+ preprocess_predicates \
+ bound_variables \
interval \
typing \
preprocess_typing \
literal_strings \
memory_tracking \
- exit_points \
- lscope
+ exit_points
SRC_ANALYSES:=$(addprefix src/analyses/, $(SRC_ANALYSES))
# code generator
diff --git a/src/plugins/e-acsl/src/analyses/preprocess_predicates.ml b/src/plugins/e-acsl/src/analyses/preprocess_predicates.ml
new file mode 100644
index 00000000000..7a68bf55f1f
--- /dev/null
+++ b/src/plugins/e-acsl/src/analyses/preprocess_predicates.ml
@@ -0,0 +1,135 @@
+open Cil_types
+open Lscope
+
+module Id_predicate =
+ Datatype.Make_with_collections
+ (struct
+ include Cil_datatype.Predicate
+ let name = "E_ACSL.Id_predicate"
+ (* The function compare should never be used since we only use this
+ datatype for hashtables *)
+ let compare _ _ = assert false
+ let equal (p1:predicate) p2 = p1 == p2
+ let structural_descr = Structural_descr.t_abstract
+ let hash = Logic_utils.hash_predicate
+ let rehash = Datatype.identity
+ let mem_project = Datatype.never_any_project
+ end)
+
+(* Memoization module which retrieves the preprocessed form of predicates *)
+module Memo: sig
+ val memo: (predicate -> pred_or_term option) -> predicate -> unit
+ val get: predicate -> pred_or_term
+ val clear: unit -> unit
+end = struct
+
+ let tbl = Id_predicate.Hashtbl.create 97
+
+ let get p =
+ try Id_predicate.Hashtbl.find tbl p
+ with Not_found -> PoT_pred p
+
+ let memo process p =
+ try ignore (Id_predicate.Hashtbl.find tbl p) with
+ | Not_found ->
+ match process p with
+ | Some pot -> Id_predicate.Hashtbl.add tbl p (pot)
+ | None -> ()
+
+ let clear () = Id_predicate.Hashtbl.clear tbl
+
+end
+
+let preprocess ~loc p =
+ match p.pred_content with
+ | Pvalid_read(BuiltinLabel Here as llabel, t)
+ | Pvalid(BuiltinLabel Here as llabel, t) -> begin
+ match t.term_node, t.term_type with
+ | TLval tlv, lty ->
+ let init =
+ Logic_const.pinitialized ~loc (llabel, Logic_utils.mk_logic_AddrOf ~loc tlv lty)
+ in
+ (* need to store a copy, to avoid p to appear in its own preprocessed form (otherwise it loops) *)
+ let p_copy =
+ match p.pred_content with
+ | Pvalid_read _ -> Logic_const.pvalid_read ~loc (llabel, t)
+ | Pvalid _ -> Logic_const.pvalid ~loc (llabel, t)
+ | _ -> assert false
+ in
+ Some (PoT_pred (Logic_const.pand ~loc (init, p_copy)))
+ | _ -> None
+ end
+ | Papp(li, labels, args) ->
+ (* Simply use the implementation of Tapp(li, labels, args).
+ To achieve this, we create a clone of [li] for which the type is
+ transformed from [None] (type of predicates) to
+ [Some int] (type as a term). *)
+ let prj = Project.current () in
+ let o = object inherit Visitor.frama_c_copy prj end in
+ let li = Visitor.visitFramacLogicInfo o li in
+ let lty = Ctype Cil.intType in
+ li.l_type <- Some lty;
+ let tapp = Logic_const.term ~loc (Tapp(li, labels, args)) lty in
+ Some (PoT_term tapp)
+ | _ -> None
+
+let preprocessor = object
+ inherit Visitor.frama_c_inplace
+
+ (* Only logic functions and logic predicates are handled.
+ E-acsl simply ignores all the other global annotations *)
+ method !vannotation annot =
+ match annot with
+ | Dfun_or_pred _ -> Cil.DoChildren
+ | _ -> Cil.SkipChildren
+
+ (* Ignore the annotations attached to statements from the RTL *)
+ method !vglob_aux =
+ function
+ | g when Rtl.Symbols.mem_global g ->
+ Cil.SkipChildren
+
+ | GFun({ svar = vi }, _) when Builtins.mem vi.vname ->
+ Cil.SkipChildren
+
+ | GFun({ svar = vi }, _)
+ when Misc.is_fc_or_compiler_builtin vi ->
+ 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
+
+ | GAnnot _ -> Cil.DoChildren
+
+ (* other globals: nothing to do *)
+ | GFunDecl _
+ | GVarDecl _
+ | GVar _
+ | GType _
+ | GCompTag _
+ | GCompTagDecl _
+ | GEnumTag _
+ | GEnumTagDecl _
+ | GAsm _
+ | GPragma _
+ | GText _
+ -> Cil.SkipChildren
+
+ method !vpredicate p =
+ let loc = p.pred_loc in
+ Memo.memo (preprocess ~loc) p;
+ Cil.DoChildren
+
+end
+
+let preprocess ast =
+ Visitor.visitFramacFileSameGlobals preprocessor ast
+
+let preprocess_annot annot =
+ ignore (Visitor.visitFramacCodeAnnotation preprocessor annot)
+
+let preprocess_predicate p =
+ ignore (Visitor.visitFramacPredicate preprocessor p)
+
+let get_preprocessed_form p = Memo.get p
diff --git a/src/plugins/e-acsl/src/analyses/preprocess_predicates.mli b/src/plugins/e-acsl/src/analyses/preprocess_predicates.mli
new file mode 100644
index 00000000000..c573a2a93c1
--- /dev/null
+++ b/src/plugins/e-acsl/src/analyses/preprocess_predicates.mli
@@ -0,0 +1,9 @@
+open Cil_types
+
+val preprocess : file -> unit
+
+val preprocess_annot : code_annotation -> unit
+
+val preprocess_predicate : predicate -> unit
+
+val get_preprocessed_form : predicate -> Lscope.pred_or_term
diff --git a/src/plugins/e-acsl/src/code_generator/injector.ml b/src/plugins/e-acsl/src/code_generator/injector.ml
index e865ccb14bb..92af80f37c7 100644
--- a/src/plugins/e-acsl/src/code_generator/injector.ml
+++ b/src/plugins/e-acsl/src/code_generator/injector.ml
@@ -864,6 +864,7 @@ let inject () =
Project.pretty (Project.current ());
Gmp_types.init ();
let ast = Ast.get () in
+ Preprocess_predicates.preprocess ast;
Bound_variables.preprocess ast;
Preprocess_typing.type_program ast;
inject_in_file ast;
diff --git a/src/plugins/e-acsl/src/code_generator/translate.ml b/src/plugins/e-acsl/src/code_generator/translate.ml
index 2521e4ee81f..9c790beab41 100644
--- a/src/plugins/e-acsl/src/code_generator/translate.ml
+++ b/src/plugins/e-acsl/src/code_generator/translate.ml
@@ -27,11 +27,6 @@ open Cil_types
open Cil_datatype
let dkey = Options.dkey_translation
-(* internal to [predicate_to_exp] but put it outside in order to not add
- extra tedious parameter.
- It is [true] iff we are currently visiting \valid. *)
-let is_visiting_valid = ref false
-
(* ************************************************************************** *)
(* Transforming terms and predicates into C expressions (if any) *)
(* ************************************************************************** *)
@@ -1160,26 +1155,9 @@ and predicate_content_to_exp ~adata ?name kf env p =
let adata, env = Assert.register_pred ~loc kf env p e adata in
e, adata, env
in
- if !is_visiting_valid then begin
(* we already transformed \valid(t) into \initialized(&t) && \valid(t):
now convert this right-most valid. *)
- is_visiting_valid := false;
call_valid ~adata t p
- end else begin
- match t.term_node, t.term_type with
- | TLval tlv, lty ->
- let init =
- Logic_const.pinitialized
- ~loc
- (llabel, Logic_utils.mk_logic_AddrOf ~loc tlv lty)
- in
- Typing.type_named_predicate ~must_clear:false init;
- let p = Logic_const.pand ~loc (init, p) in
- is_visiting_valid := true;
- predicate_to_exp ~adata kf env p
- | _ ->
- call_valid ~adata t p
- end
| Pvalid _ -> Env.not_yet env "labeled \\valid"
| Pvalid_read _ -> Env.not_yet env "labeled \\valid_read"
| Pseparated tlist ->
@@ -1294,7 +1272,6 @@ and translate_rte_annots:
'a. (Format.formatter -> 'a -> unit) -> 'a ->
kernel_function -> Env.t -> code_annotation list -> Env.t =
fun pp elt kf env l ->
- let old_valid = !is_visiting_valid in
let old_kind = Env.annotation_kind env in
let env = Env.set_annotation_kind env Smart_stmt.RTE in
let env =
@@ -1320,7 +1297,6 @@ and translate_rte_annots:
env
l
in
- is_visiting_valid := old_valid;
Env.set_annotation_kind env old_kind
and translate_rte ?filter kf env e =
--
GitLab