From ac25bb7230a3165d11b7d4ae9d4bf6a729b7ab34 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 28 Feb 2023 11:25:27 +0100
Subject: [PATCH] [server] Removes cache between some localizables.
This cache required parsing C expressions and lvalues as terms, which would
sometimes fail and prevent the creation of otherwise fine markers.
Also, this cache was only used for terms manually provided by the user,
which should not happen too frequently.
---
src/plugins/server/kernel_ast.ml | 47 ++++----------------------------
1 file changed, 6 insertions(+), 41 deletions(-)
diff --git a/src/plugins/server/kernel_ast.ml b/src/plugins/server/kernel_ast.ml
index 873e9e181d0..0411f40ff33 100644
--- a/src/plugins/server/kernel_ast.ml
+++ b/src/plugins/server/kernel_ast.ml
@@ -28,37 +28,6 @@ open Cil_types
let package = Pkg.package ~title:"Ast Services" ~name:"ast" ~readme:"ast.md" ()
-(* -------------------------------------------------------------------------- *)
-(* --- Marker Cache System --- *)
-(* -------------------------------------------------------------------------- *)
-
-let logic_environment () =
- let open Logic_typing in
- Lenv.empty () |> append_pre_label |> append_init_label |> append_here_label
-
-module Key = Datatype.Pair(Cil_datatype.Stmt)(Cil_datatype.Term)
-module Cache = Hashtbl.Make(Key)
-
-let get_term kf term =
- let env = logic_environment () in
- try Some (Logic_parse_string.term ~env kf term)
- with Logic_parse_string.Error _ | Parsing.Parse_error -> None
-
-let key_of_localizable =
- let open Printer_tag in
- function
- | PStmt _ | PStmtStart _ | PTermLval _ | PVDecl _ | PGlobal _ | PIP _
- | PType _ | PLval (_, Kglobal, _) | PExp (_, Kglobal, _)
- -> None
- | PLval (kf, Kstmt stmt, lval) ->
- let str = Format.asprintf "%a" Cil_datatype.Lval.pretty lval in
- Option.(bind kf (fun kf -> get_term kf str) |> map (fun t -> (stmt, t)))
- | PExp (kf, Kstmt stmt, exp) ->
- let str = Format.asprintf "%a" Cil_datatype.Exp.pretty exp in
- Option.(bind kf (fun kf -> get_term kf str) |> map (fun t -> (stmt, t)))
-
-let cache = Cache.create 10
-
(* -------------------------------------------------------------------------- *)
(* --- Compute Ast --- *)
(* -------------------------------------------------------------------------- *)
@@ -320,8 +289,6 @@ struct
| PType _ -> Printf.sprintf "#y%d" (incr kid ; !kid)
let create loc =
- let add_cache key = Cache.add cache key loc in
- key_of_localizable loc |> Option.iter add_cache;
let { tags ; locs } = STATE.get () in
try Localizable.Hashtbl.find tags loc
with Not_found ->
@@ -882,16 +849,14 @@ module MarkerTermOutput = Data.Joption (Marker)
let build_marker =
Option.map @@ fun input ->
- let env = logic_environment () in
+ let env =
+ let open Logic_typing in
+ Lenv.empty () |> append_pre_label |> append_init_label |> append_here_label
+ in
let kf = Kernel_function.find_englobing_kf input.atStmt in
let term = Logic_parse_string.term ~env kf input.term in
- let key = (input.atStmt, term) in
- match Cache.find_opt cache key with
- | Some tag -> tag
- | None ->
- let exp = Logic_to_c.term_to_exp term in
- let tag = Printer_tag.PExp (Some kf, Kstmt input.atStmt, exp) in
- Cache.add cache key tag ; tag
+ let exp = Logic_to_c.term_to_exp term in
+ Printer_tag.PExp (Some kf, Kstmt input.atStmt, exp)
let descr = "Build a marker from an ACSL term."
--
GitLab