From bdc15d16708c9ae9bbe2dda2d7d965b73e66f2b4 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 3 Apr 2020 10:02:10 +0200
Subject: [PATCH] [Instantiate] Global_vars renamed Global_context
---
headers/header_spec.txt | 4 ++--
src/plugins/instantiate/Instantiate.mli | 13 ++++++-------
src/plugins/instantiate/Makefile.in | 2 +-
.../{global_vars.ml => global_context.ml} | 5 ++---
.../{global_vars.mli => global_context.mli} | 13 ++++++-------
src/plugins/instantiate/stdlib/basic_alloc.ml | 8 +++++++-
.../instantiate/tests/plugin/needs_globals.ml | 9 +++++++--
src/plugins/instantiate/transform.ml | 5 +++--
8 files changed, 34 insertions(+), 25 deletions(-)
rename src/plugins/instantiate/{global_vars.ml => global_context.ml} (94%)
rename src/plugins/instantiate/{global_vars.mli => global_context.mli} (81%)
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index d9acf0cdd50..91d9557fd95 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -945,8 +945,8 @@ src/plugins/occurrence/register_gui.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/occurrence/register_gui.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/basic_blocks.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/basic_blocks.mli: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/global_vars.ml: CEA_LGPL_OR_PROPRIETARY
-src/plugins/instantiate/global_vars.mli: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/global_context.ml: CEA_LGPL_OR_PROPRIETARY
+src/plugins/instantiate/global_context.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/Instantiate.mli: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/instantiator_builder.ml: CEA_LGPL_OR_PROPRIETARY
src/plugins/instantiate/instantiator_builder.mli: CEA_LGPL_OR_PROPRIETARY
diff --git a/src/plugins/instantiate/Instantiate.mli b/src/plugins/instantiate/Instantiate.mli
index aaddb8131d0..4444dd5d95b 100644
--- a/src/plugins/instantiate/Instantiate.mli
+++ b/src/plugins/instantiate/Instantiate.mli
@@ -101,13 +101,12 @@ module Transform: sig
val register: (module Instantiator_builder.Generator_sig) -> unit
end
-module Global_vars:sig
- (** [get t ghost storage name] searches for an existing variable [name]. If this
- variable does not exists, it is created with the specified type [t], [ghost]
- status and [storage].
+module Global_context:sig
+ (** [get_variable name f] searches for an existing variable [name]. If this
+ variable does not exists, it is created using [f].
- The obtained varinfo does not need to be registered, it will be done by the
- transformation.
+ The obtained varinfo does not need to be registered, nor [f] needs to
+ perform the registration, it will be done by the transformation.
*)
- val get: typ -> bool -> storage -> string -> varinfo
+ val get_variable: string -> (unit -> varinfo) -> varinfo
end
diff --git a/src/plugins/instantiate/Makefile.in b/src/plugins/instantiate/Makefile.in
index 97c0b467e45..8635d3bace9 100644
--- a/src/plugins/instantiate/Makefile.in
+++ b/src/plugins/instantiate/Makefile.in
@@ -57,7 +57,7 @@ PLUGIN_EXTRA_DIRS:=\
PLUGIN_CMI :=
PLUGIN_CMO := \
options basic_blocks \
- global_vars instantiator_builder \
+ global_context instantiator_builder \
transform register \
$(SRC_STRING) \
$(SRC_STDLIB)
diff --git a/src/plugins/instantiate/global_vars.ml b/src/plugins/instantiate/global_context.ml
similarity index 94%
rename from src/plugins/instantiate/global_vars.ml
rename to src/plugins/instantiate/global_context.ml
index 379443e789b..d28b409a52f 100644
--- a/src/plugins/instantiate/global_vars.ml
+++ b/src/plugins/instantiate/global_context.ml
@@ -23,13 +23,12 @@
module Table = Datatype.String.Hashtbl
let table = Table.create 13
-let get typ ghost storage name =
+let get_variable name make =
if Table.mem table name then Table.find table name
else begin
try Globals.Vars.find_from_astinfo name VGlobal
with Not_found ->
- let vi = Cil.makeVarinfo ~ghost true false name typ in
- vi.vstorage <- storage ;
+ let vi = make () in
Table.add table name vi ;
vi
end
diff --git a/src/plugins/instantiate/global_vars.mli b/src/plugins/instantiate/global_context.mli
similarity index 81%
rename from src/plugins/instantiate/global_vars.mli
rename to src/plugins/instantiate/global_context.mli
index 88b711593ce..66e60036195 100644
--- a/src/plugins/instantiate/global_vars.mli
+++ b/src/plugins/instantiate/global_context.mli
@@ -26,17 +26,16 @@ open Cil_types
by instantiation modules.
*)
-(** [get t ghost storage name] searches for an existing variable [name]. If this
- variable does not exists, it is created with the specified type [t], [ghost]
- status and [storage].
+(** [get_variable name f] searches for an existing variable [name]. If this
+ variable does not exists, it is created using [f].
- The obtained varinfo does not need to be registered, it will be done by the
- transformation.
+ The obtained varinfo does not need to be registered, nor [f] needs to
+ perform the registration, it will be done by the transformation.
*)
-val get: typ -> bool -> storage -> string -> varinfo
+val get_variable: string -> (unit -> varinfo) -> varinfo
(** Clears internal tables *)
val clear: unit -> unit
-(** Creates a list of global for the variables that have been created *)
+(** Creates a list of global for the elements that have been created *)
val globals: location -> global list
diff --git a/src/plugins/instantiate/stdlib/basic_alloc.ml b/src/plugins/instantiate/stdlib/basic_alloc.ml
index d2bb11bd72d..ec54907d18f 100644
--- a/src/plugins/instantiate/stdlib/basic_alloc.ml
+++ b/src/plugins/instantiate/stdlib/basic_alloc.ml
@@ -61,7 +61,13 @@ let isnt_allocable ?loc size =
new_predicate { p with pred_name = [ "allocable" ]}
let heap_status () =
- let vi = Global_vars.get Cil.intType true Extern "__fc_heap_status" in
+ let name = "__fc_heap_status" in
+ let make () =
+ let vi = Cil.makeVarinfo ~ghost:true true false name Cil.intType in
+ vi.vstorage <- Extern ;
+ vi
+ in
+ let vi = Global_context.get_variable name make in
Basic_blocks.cvar_to_tvar vi
let assigns_result ?loc typ deps =
diff --git a/src/plugins/instantiate/tests/plugin/needs_globals.ml b/src/plugins/instantiate/tests/plugin/needs_globals.ml
index c76373900f5..506da455fdb 100644
--- a/src/plugins/instantiate/tests/plugin/needs_globals.ml
+++ b/src/plugins/instantiate/tests/plugin/needs_globals.ml
@@ -27,8 +27,13 @@ let generate_prototype function_name t =
let generate_spec needed _ _ _ =
let open Cil_types in
let open Logic_const in
- let open Instantiate.Global_vars in
- let vi = get Cil.floatType true Cil_types.Extern needed in
+ let open Instantiate.Global_context in
+ let make () =
+ let vi = Cil.makeVarinfo ~ghost:true true false needed Cil.floatType in
+ vi.vstorage <- Extern ;
+ vi
+ in
+ let vi = get_variable needed make in
let t = tvar (Cil.cvar_to_lvar vi) in
let assigns =
Cil_types.Writes [ Logic_const.new_identified_term t, From [] ]
diff --git a/src/plugins/instantiate/transform.ml b/src/plugins/instantiate/transform.ml
index 7dda9a46b99..590ee506dbd 100644
--- a/src/plugins/instantiate/transform.ml
+++ b/src/plugins/instantiate/transform.ml
@@ -38,7 +38,7 @@ let get_kfs () =
Hashtbl.fold (fun k v l -> (get_kfs k v) @ l) base []
let clear () =
- Global_vars.clear () ;
+ Global_context.clear () ;
let clear _ instantiator =
let module I = (val instantiator: Instantiator) in
I.clear ()
@@ -55,7 +55,7 @@ class transformer = object(self)
method! vfile _ =
let post f =
- f.globals <- (Global_vars.globals (Cil.CurrentLoc.get())) @ f.globals ;
+ f.globals <- (Global_context.globals (Cil.CurrentLoc.get())) @ f.globals ;
Ast.mark_as_changed () ;
Ast.mark_as_grown () ;
f
@@ -163,4 +163,5 @@ let compute_statuses_all_kfs () =
let transform file =
clear () ;
Visitor.visitFramacFile (new transformer) file ;
+ File.reorder_ast () ;
compute_statuses_all_kfs ()
--
GitLab