From bea4906b85bd0664ab52bbe871e07d75b13e7f9b Mon Sep 17 00:00:00 2001
From: Jan Rochel <jan.rochel@cea.fr>
Date: Wed, 18 Sep 2024 01:56:58 +0200
Subject: [PATCH] [e-acsl] Logic_normalizer: rework memoization
Render the memoization tables for predicates and terms bidirectional.
This will help improve user feedback messages in the subsequent commits.
We do not want to confront to the user with feedback messages that
contain transformed code, so we need bidirectional memoization tables in
order to determine the original code that we then can show to the user.
---
.../e-acsl/src/analyses/logic_normalizer.ml | 87 ++++++++++---------
.../e-acsl/src/analyses/logic_normalizer.mli | 6 ++
2 files changed, 54 insertions(+), 39 deletions(-)
diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
index 8e370f5f25c..a6fd74c101f 100644
--- a/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
+++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.ml
@@ -39,46 +39,50 @@ module Id_predicate =
let mem_project = Datatype.never_any_project
end)
-(* Memoization module which retrieves the preprocessed form of predicates *)
-module Memo: sig
- val memo_pred: (predicate -> predicate option) -> predicate -> unit
- val get_pred: predicate -> predicate
- val memo_term : (term -> term option) -> term -> unit
- val get_term : term -> term
- val clear: unit -> unit
-end = struct
-
- let tbl_term = Misc.Id_term.Hashtbl.create 97
- let tbl_pred = Id_predicate.Hashtbl.create 97
-
- let get_pred p =
- try Id_predicate.Hashtbl.find tbl_pred p
- with Not_found -> p
-
- let memo_pred process p =
- try ignore (Id_predicate.Hashtbl.find tbl_pred p) with
- | Not_found ->
- match process p with
- | Some pot -> Id_predicate.Hashtbl.add tbl_pred p pot
- | None -> ()
+module BiMap (H : Hashtbl.S) = struct
+ let from_tbl = H.create 7
+ let dest_tbl = H.create 7
- let get_term t =
- try Misc.Id_term.Hashtbl.find tbl_term t
- with Not_found -> t
+ let clear () =
+ H.clear from_tbl;
+ H.clear dest_tbl
- let memo_term process t =
- try ignore (Misc.Id_term.Hashtbl.find tbl_term t) with
- | Not_found ->
- match process t with
- | Some term -> Misc.Id_term.Hashtbl.add tbl_term t term
- | None -> ()
+ let add from dest =
+ H.add from_tbl from dest;
+ H.add dest_tbl dest from
- let clear () =
- Misc.Id_term.Hashtbl.clear tbl_term;
- Id_predicate.Hashtbl.clear tbl_pred
+ let dest from = H.find from_tbl from
+ let dest_opt from = H.find_opt from_tbl from
+ let from dest = H.find dest_tbl dest
+ let from_opt dest = H.find_opt dest_tbl dest
+
+ let dest_or_self from = try dest from with Not_found -> from
+ let from_or_self dest = try from dest with Not_found -> dest
+end
+(* Memoization modules for retrieving the preprocessed and original form of
+ predicates and terms *)
+module Memo (H : Hashtbl.S) = struct
+ module M = BiMap (H)
+
+ let clear = M.clear
+
+ let normalized x = M.dest_or_self x
+ let normalized_opt x = M.dest_opt x
+ let original x = M.from_or_self x
+ let original_opt x = M.from_opt x
+
+ let memoize process x =
+ try Some (M.dest x) with
+ | Not_found ->
+ match process x with
+ | Some y -> M.add x y; Some y
+ | None -> None
end
+module Predicates = Memo (Id_predicate.Hashtbl)
+module Terms = Memo (Misc.Id_term.Hashtbl)
+
let preprocess_pred ~loc p =
match p.pred_content with
| Pvalid_read(BuiltinLabel Here as llabel, t)
@@ -134,12 +138,12 @@ let preprocessor = object
method !vpredicate p =
let loc = p.pred_loc in
- Memo.memo_pred (preprocess_pred ~loc) p;
+ ignore @@ Predicates.memoize (preprocess_pred ~loc) p;
Cil.DoChildren
method !vterm t =
let loc = t.term_loc in
- Memo.memo_term (preprocess_term ~loc) t;
+ ignore @@ Terms.memoize (preprocess_term ~loc) t;
Cil.DoChildren
end
@@ -152,6 +156,11 @@ let preprocess_annot annot =
let preprocess_predicate p =
ignore @@ preprocessor#visit_predicate p
-let get_pred = Memo.get_pred
-let get_term = Memo.get_term
-let clear = Memo.clear
+let get_pred = Predicates.normalized
+let get_orig_pred = Predicates.original
+let get_term = Terms.normalized
+let get_orig_term = Terms.original
+
+let clear () =
+ Terms.clear ();
+ Predicates.clear ()
diff --git a/src/plugins/e-acsl/src/analyses/logic_normalizer.mli b/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
index 521d23380fd..e081f4da949 100644
--- a/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
+++ b/src/plugins/e-acsl/src/analyses/logic_normalizer.mli
@@ -44,8 +44,14 @@ val preprocess_predicate : predicate -> unit
val get_pred : predicate -> predicate
(** Retrieve the preprocessed form of a predicate *)
+val get_orig_pred : predicate -> predicate
+(** Retrieve the original form of the given predicate *)
+
val get_term : term -> term
(** Retrieve the preprocessed form of a term *)
+val get_orig_term : term -> term
+(** Retrieve the original form of the given term *)
+
val clear: unit -> unit
(** clear the table of normalized predicates *)
--
GitLab