From 638dca648dba9c79e2bd52869645b756f58311d5 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Fri, 27 Mar 2020 16:41:28 +0100
Subject: [PATCH] [Instantiate] Introduces globals variables table
---
src/plugins/instantiate/Instantiate.mli | 11 +++
src/plugins/instantiate/Makefile.in | 4 +-
src/plugins/instantiate/global_vars.ml | 40 ++++++++++
src/plugins/instantiate/global_vars.mli | 42 +++++++++++
src/plugins/instantiate/stdlib/basic_alloc.ml | 4 +-
.../instantiate/tests/plugin/needs_global.i | 14 ++++
.../instantiate/tests/plugin/needs_globals.ml | 75 +++++++++++++++++++
.../plugin/oracle/needs_global.res.oracle | 34 +++++++++
src/plugins/instantiate/transform.ml | 2 +
9 files changed, 223 insertions(+), 3 deletions(-)
create mode 100644 src/plugins/instantiate/global_vars.ml
create mode 100644 src/plugins/instantiate/global_vars.mli
create mode 100644 src/plugins/instantiate/tests/plugin/needs_global.i
create mode 100644 src/plugins/instantiate/tests/plugin/needs_globals.ml
create mode 100644 src/plugins/instantiate/tests/plugin/oracle/needs_global.res.oracle
diff --git a/src/plugins/instantiate/Instantiate.mli b/src/plugins/instantiate/Instantiate.mli
index d47de410b8f..4af9d03fc53 100644
--- a/src/plugins/instantiate/Instantiate.mli
+++ b/src/plugins/instantiate/Instantiate.mli
@@ -100,3 +100,14 @@ 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].
+
+ The obtained varinfo does not need to be registered, it will be done by the
+ transformation.
+ *)
+ val get: typ -> bool -> storage -> string -> varinfo
+end
\ No newline at end of file
diff --git a/src/plugins/instantiate/Makefile.in b/src/plugins/instantiate/Makefile.in
index a8fc2764589..97c0b467e45 100644
--- a/src/plugins/instantiate/Makefile.in
+++ b/src/plugins/instantiate/Makefile.in
@@ -56,7 +56,9 @@ PLUGIN_EXTRA_DIRS:=\
stdlib
PLUGIN_CMI :=
PLUGIN_CMO := \
- options basic_blocks instantiator_builder transform register \
+ options basic_blocks \
+ global_vars instantiator_builder \
+ transform register \
$(SRC_STRING) \
$(SRC_STDLIB)
diff --git a/src/plugins/instantiate/global_vars.ml b/src/plugins/instantiate/global_vars.ml
new file mode 100644
index 00000000000..379443e789b
--- /dev/null
+++ b/src/plugins/instantiate/global_vars.ml
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+module Table = Datatype.String.Hashtbl
+let table = Table.create 13
+
+let get typ ghost storage name =
+ 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 ;
+ Table.add table name vi ;
+ vi
+ end
+
+let clear () = Table.clear table
+
+let globals loc =
+ Table.fold (fun _ x l -> Cil_types.GVarDecl(x, loc) :: l) table []
diff --git a/src/plugins/instantiate/global_vars.mli b/src/plugins/instantiate/global_vars.mli
new file mode 100644
index 00000000000..88b711593ce
--- /dev/null
+++ b/src/plugins/instantiate/global_vars.mli
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+
+(** The purpose of this module is to create global variables when it is needed
+ 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].
+
+ The obtained varinfo does not need to be registered, it will be done by the
+ transformation.
+*)
+val get: typ -> bool -> storage -> string -> varinfo
+
+(** Clears internal tables *)
+val clear: unit -> unit
+
+(** Creates a list of global for the variables 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 41679ef1d11..d2bb11bd72d 100644
--- a/src/plugins/instantiate/stdlib/basic_alloc.ml
+++ b/src/plugins/instantiate/stdlib/basic_alloc.ml
@@ -61,8 +61,8 @@ let isnt_allocable ?loc size =
new_predicate { p with pred_name = [ "allocable" ]}
let heap_status () =
- let heap_status = Globals.Vars.find_from_astinfo "__fc_heap_status" VGlobal in
- Basic_blocks.cvar_to_tvar (heap_status)
+ let vi = Global_vars.get Cil.intType true Extern "__fc_heap_status" in
+ Basic_blocks.cvar_to_tvar vi
let assigns_result ?loc typ deps =
let heap_status = new_identified_term (heap_status ()) in
diff --git a/src/plugins/instantiate/tests/plugin/needs_global.i b/src/plugins/instantiate/tests/plugin/needs_global.i
new file mode 100644
index 00000000000..dfd53797477
--- /dev/null
+++ b/src/plugins/instantiate/tests/plugin/needs_global.i
@@ -0,0 +1,14 @@
+/* run.config
+ OPT: -load-script tests/plugin/needs_globals.ml -instantiate -check -print
+*/
+
+int i ; // needed for already_one specifciation
+void already_one(void* parameter) ;
+
+void needs_new(void* parameter) ;
+
+void foo(void){
+ int *i ;
+ already_one(i);
+ needs_new(i);
+}
diff --git a/src/plugins/instantiate/tests/plugin/needs_globals.ml b/src/plugins/instantiate/tests/plugin/needs_globals.ml
new file mode 100644
index 00000000000..c76373900f5
--- /dev/null
+++ b/src/plugins/instantiate/tests/plugin/needs_globals.ml
@@ -0,0 +1,75 @@
+let well_typed_call _ _ = function
+ | [ e ] ->
+ let t = Cil.typeOf(Cil.stripCasts e) in
+ not (Cil.isVoidPtrType t) && Cil.isPointerType t
+ | _ -> false
+
+let key_from_call _ _ = function
+ | [ e ] -> Cil.typeOf_pointed (Cil.typeOf(Cil.stripCasts e))
+ | _ -> assert false
+
+let retype_args _ = function
+ | [ e ] -> [ Cil.stripCasts e ]
+ | _ -> assert false
+
+let generate_function_type t =
+ let params = [("x", Cil_types.TPtr(t, []), [])] in
+ Cil_types.TFun(Cil.voidType, Some params, false, [])
+
+let generate_prototype function_name t =
+ let fun_type = generate_function_type t in
+ let name = function_name ^ "_" ^ match t with
+ | Cil_types.TInt(_) -> "int"
+ | _ -> assert false (* nothing else in our test *)
+ in
+ name, fun_type
+
+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 t = tvar (Cil.cvar_to_lvar vi) in
+ let assigns =
+ Cil_types.Writes [ Logic_const.new_identified_term t, From [] ]
+ in {
+ spec_behavior = [ {
+ b_name = Cil.default_behavior_name ;
+ b_requires = [] ;
+ b_assumes = [] ;
+ b_post_cond = [] ;
+ b_assigns = assigns ;
+ b_allocation = FreeAllocAny ;
+ b_extended = []
+ } ] ;
+ spec_variant = None ;
+ spec_terminates = None ;
+ spec_complete_behaviors = [] ;
+ spec_disjoint_behaviors = [] ;
+ }
+
+let () = Instantiate.Transform.register (module struct
+ module Hashtbl = Cil_datatype.Typ.Hashtbl
+ type override_key = Hashtbl.key
+
+ let function_name = "already_one"
+ let well_typed_call = well_typed_call
+ let key_from_call = key_from_call
+ let retype_args = retype_args
+ let generate_prototype = generate_prototype function_name
+ let generate_spec = generate_spec "i"
+ let args_for_original _ = Extlib.id
+ end)
+
+let () = Instantiate.Transform.register (module struct
+ module Hashtbl = Cil_datatype.Typ.Hashtbl
+ type override_key = Hashtbl.key
+
+ let function_name = "needs_new"
+ let well_typed_call = well_typed_call
+ let key_from_call = key_from_call
+ let retype_args = retype_args
+ let generate_prototype = generate_prototype function_name
+ let generate_spec = generate_spec "j"
+ let args_for_original _ = Extlib.id
+ end)
diff --git a/src/plugins/instantiate/tests/plugin/oracle/needs_global.res.oracle b/src/plugins/instantiate/tests/plugin/oracle/needs_global.res.oracle
new file mode 100644
index 00000000000..0b7e5b4ccb7
--- /dev/null
+++ b/src/plugins/instantiate/tests/plugin/oracle/needs_global.res.oracle
@@ -0,0 +1,34 @@
+[kernel] Parsing tests/plugin/needs_global.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ ghost extern float j; */
+
+int i;
+void already_one(void *parameter);
+
+void needs_new(void *parameter);
+
+/*@ assigns j;
+ assigns j \from \nothing; */
+void needs_new_int(int *x)
+{
+ needs_new((void *)x);
+ return;
+}
+
+/*@ assigns i;
+ assigns i \from \nothing; */
+void already_one_int(int *x)
+{
+ already_one((void *)x);
+ return;
+}
+
+void foo(void)
+{
+ int *i_0;
+ already_one_int(i_0);
+ needs_new_int(i_0);
+ return;
+}
+
+
diff --git a/src/plugins/instantiate/transform.ml b/src/plugins/instantiate/transform.ml
index 4970a5913e2..8b0f9ece40e 100644
--- a/src/plugins/instantiate/transform.ml
+++ b/src/plugins/instantiate/transform.ml
@@ -38,6 +38,7 @@ let get_kfs () =
Hashtbl.fold (fun k v l -> (get_kfs k v) @ l) base []
let clear () =
+ Global_vars.clear () ;
let clear _ instantiator =
let module I = (val instantiator: Instantiator) in
I.clear ()
@@ -54,6 +55,7 @@ class transformer = object(self)
method! vfile _ =
let post f =
+ f.globals <- (Global_vars.globals (Cil.CurrentLoc.get())) @ f.globals ;
Ast.mark_as_changed () ;
Ast.mark_as_grown () ;
f
--
GitLab