From 48356f3732fca021d9a4732f859d0f0c73b2cb92 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 25 Mar 2020 17:13:14 +0100
Subject: [PATCH] [Instantiate] Simplifies internal tables management
---
.../instantiate/instantiator_builder.ml | 19 ++++++++++---------
.../instantiate/instantiator_builder.mli | 5 ++---
.../instantiate/tests/plugin/ast_clear.c | 9 +++++++++
.../tests/plugin/oracle/ast_clear.res.oracle | 2 ++
src/plugins/instantiate/transform.ml | 15 ++++++++-------
5 files changed, 31 insertions(+), 19 deletions(-)
create mode 100644 src/plugins/instantiate/tests/plugin/ast_clear.c
create mode 100644 src/plugins/instantiate/tests/plugin/oracle/ast_clear.res.oracle
diff --git a/src/plugins/instantiate/instantiator_builder.ml b/src/plugins/instantiate/instantiator_builder.ml
index df9028d122d..6b98b3ad9d2 100644
--- a/src/plugins/instantiate/instantiator_builder.ml
+++ b/src/plugins/instantiate/instantiator_builder.ml
@@ -46,10 +46,9 @@ module type Instantiator = sig
val retype_args: override_key -> exp list -> exp list
val get_override: override_key -> fundec
val get_kfs: unit -> kernel_function list
- val mark_as_computed: ?project:Project.t -> unit -> unit
+ val clear: unit -> unit
end
-
let build_body caller callee args_generator =
let open Extlib in
let loc = Cil_datatype.Location.unknown in
@@ -68,12 +67,13 @@ let build_body caller callee args_generator =
module Make_instantiator (G: Generator_sig) = struct
include G
module Enabled = Options.NewInstantiator (G)
- module Cache = State_builder.Hashtbl (G.Hashtbl) (Cil_datatype.Fundec)
- (struct
- let size = 5
- let dependencies = []
- let name = "Instantiator." ^ G.function_name
- end)
+ module Cache = struct
+ let tbl = G.Hashtbl.create 13
+ let find = G.Hashtbl.find tbl
+ let add = G.Hashtbl.add tbl
+ let fold f = G.Hashtbl.fold f tbl
+ let clear () = G.Hashtbl.clear tbl
+ end
let make_fundec key =
let open Globals.Functions in
@@ -113,5 +113,6 @@ module Make_instantiator (G: Generator_sig) = struct
let get_kfs () =
Cache.fold (fun _ fd l -> Globals.Functions.get fd.svar :: l) []
- let mark_as_computed = Cache.mark_as_computed
+ let clear () =
+ Cache.clear ()
end
diff --git a/src/plugins/instantiate/instantiator_builder.mli b/src/plugins/instantiate/instantiator_builder.mli
index e2432608275..87c268d2d49 100644
--- a/src/plugins/instantiate/instantiator_builder.mli
+++ b/src/plugins/instantiate/instantiator_builder.mli
@@ -123,10 +123,9 @@ module type Instantiator = sig
*)
val get_kfs: unit -> kernel_function list
- (** [mark_as_computed ?project ()] applies the [mark_as_computed] on the
- internal table.
+ (** [clear ()] clears the internal table of the instantiator.
*)
- val mark_as_computed: ?project:Project.t -> unit -> unit
+ val clear: unit -> unit
end
(** Generates a [Instantiator] from a [Generator_sig] adding all necessary stuff for
diff --git a/src/plugins/instantiate/tests/plugin/ast_clear.c b/src/plugins/instantiate/tests/plugin/ast_clear.c
new file mode 100644
index 00000000000..d3dfbb6ad2a
--- /dev/null
+++ b/src/plugins/instantiate/tests/plugin/ast_clear.c
@@ -0,0 +1,9 @@
+/* run.config
+ OPT: -instantiate -then -pp-annot
+*/
+
+#include <string.h>
+
+int foo(char* s1, char* s2, size_t len){
+ return memcmp(s1, s2, len) ;
+}
\ No newline at end of file
diff --git a/src/plugins/instantiate/tests/plugin/oracle/ast_clear.res.oracle b/src/plugins/instantiate/tests/plugin/oracle/ast_clear.res.oracle
new file mode 100644
index 00000000000..1a8c67bb4f4
--- /dev/null
+++ b/src/plugins/instantiate/tests/plugin/oracle/ast_clear.res.oracle
@@ -0,0 +1,2 @@
+[kernel] Parsing tests/plugin/ast_clear.c (with preprocessing)
+[kernel] Parsing tests/plugin/ast_clear.c (with preprocessing)
diff --git a/src/plugins/instantiate/transform.ml b/src/plugins/instantiate/transform.ml
index 28f7a1ca811..c1f0f29d170 100644
--- a/src/plugins/instantiate/transform.ml
+++ b/src/plugins/instantiate/transform.ml
@@ -29,12 +29,6 @@ let register (module G: Generator_sig) =
let module Instantiator = Make_instantiator(G) in
Hashtbl.add base G.function_name (module Instantiator)
-let mark_as_computed () =
- let mark_as_computed _ instantiator =
- let module I = (val instantiator: Instantiator) in I.mark_as_computed ()
- in
- Hashtbl.iter mark_as_computed base
-
let get_kfs () =
let get_kfs _ instantiator =
let module I = (val instantiator: Instantiator) in
@@ -43,6 +37,13 @@ let get_kfs () =
in
Hashtbl.fold (fun k v l -> (get_kfs k v) @ l) base []
+let clear () =
+ let clear _ instantiator =
+ let module I = (val instantiator: Instantiator) in
+ I.clear ()
+ in
+ Hashtbl.iter clear base
+
module VISet = Cil_datatype.Varinfo.Hptset
class transformer = object(self)
@@ -55,7 +56,6 @@ class transformer = object(self)
let post f =
Ast.mark_as_changed () ;
Ast.mark_as_grown () ;
- mark_as_computed () ;
f
in
Cil.DoChildrenPost post
@@ -158,5 +158,6 @@ let compute_statuses_all_kfs () =
List.iter compute_comp_disj_statuses kfs
let transform file =
+ clear () ;
Visitor.visitFramacFile (new transformer) file ;
compute_statuses_all_kfs ()
--
GitLab