From a488c2ac51285cf1151452005249e79dd21dfc25 Mon Sep 17 00:00:00 2001
From: Virgile Robles <virgile.robles@protonmail.ch>
Date: Tue, 20 Oct 2020 06:10:59 +0200
Subject: [PATCH] Reorganize utils and specialize more tables

---
 meta_annotate.ml  |  1 +
 meta_bindings.ml  | 26 +++++++++++---------------
 meta_bindings.mli |  7 ++++---
 meta_deduce.ml    |  1 +
 meta_dispatch.ml  |  1 +
 meta_dispatch.mli |  1 +
 meta_options.ml   | 11 -----------
 meta_parse.ml     | 15 ++++++---------
 meta_parse.mli    |  6 +-----
 meta_utils.ml     | 15 +++++++++++++++
 10 files changed, 41 insertions(+), 43 deletions(-)
 create mode 100644 meta_utils.ml

diff --git a/meta_annotate.ml b/meta_annotate.ml
index 451ef6d..3037da9 100644
--- a/meta_annotate.ml
+++ b/meta_annotate.ml
@@ -19,6 +19,7 @@
 (*  for more details (enclosed in the file LICENSE)                       *)
 (**************************************************************************)
 
+open Meta_utils
 open Meta_options
 open Meta_parse
 open Meta_dispatch
diff --git a/meta_bindings.ml b/meta_bindings.ml
index 741af90..a4a6edf 100644
--- a/meta_bindings.ml
+++ b/meta_bindings.ml
@@ -20,15 +20,14 @@
 (**************************************************************************)
 
 open Meta_options
+open Meta_utils
 open Logic_ptree
 open Logic_typing
 open Cil_types
 
-module Stmt_Hashtbl = Cil_datatype.Stmt.Hashtbl
-
 (* Gathered bindings *)
 let gathered_bindings = ref []
-let types = Hashtbl.create 5
+let types = Str_Hashtbl.create 5
 
 let setname base = base ^ "_set"
 let sizename base = base ^ "_size"
@@ -40,16 +39,16 @@ let capname base = base ^ "_capacity"
 *)
 let parse_bound tc loc quantifiers bn = match bn.lexpr_node with
   | PLvar bname ->
-    let content_type = begin match Hashtbl.find_opt types bname with
+    let content_type = begin match Str_Hashtbl.find_opt types bname with
       | Some x -> x
       | None -> tc.error loc "The name '%s' is used but not bound anywhere" bname
     end in
     let tabvar = tc.find_var (setname bname) in
-    let quantvar = begin match Hashtbl.find_opt quantifiers bname with
+    let quantvar = begin match Str_Hashtbl.find_opt quantifiers bname with
       | Some x -> x
       | None ->
         let res = Cil_const.make_logic_var_quant (bname ^ "_i") Linteger
-        in Hashtbl.add quantifiers bname res; res
+        in Str_Hashtbl.add quantifiers bname res; res
     end in
     let tlv = (TVar tabvar, TIndex (Logic_const.tvar quantvar, TNoOffset)) in
     Logic_const.term (TLval tlv) content_type
@@ -64,8 +63,8 @@ let parse_bind tc loc cvar_name gvar_name =
     | Ctype _ as lt -> lt
     | _ -> tc.error loc "Only C variables can be bound to names"
   end in
-  begin match Hashtbl.find_opt types gvar_name with
-    | None -> Hashtbl.add types gvar_name bdg_type
+  begin match Str_Hashtbl.find_opt types gvar_name with
+    | None -> Str_Hashtbl.add types gvar_name bdg_type
     | Some old_type ->
       if not @@ Logic_utils.is_same_type bdg_type old_type then
         tc.error loc
@@ -91,8 +90,8 @@ let from_id id =
 *)
 let after_parse tc pred quanthash =
   let open Logic_const in
-  let quantifiers = Hashtbl.fold (fun _ -> List.cons) quanthash [] in
-  let conditions = Hashtbl.fold (fun name var conds ->
+  let quantifiers = Str_Hashtbl.fold (fun _ -> List.cons) quanthash [] in
+  let conditions = Str_Hashtbl.fold (fun name var conds ->
       let mainterm = tvar var in
       let sizeterm = tc.find_var (sizename name) |> tvar in
       let supzero = prel (Rle, tinteger 0, mainterm) in
@@ -141,7 +140,7 @@ let add_ghost_code flags =
         Globals.Vars.add cvar sinit;
         GVar (cvar, sinit, unkloc) :: pre
   in
-  let globs = Hashtbl.fold (fun a b c -> (make_global a b) @ c) types [] in
+  let globs = Str_Hashtbl.fold (fun a b c -> (make_global a b) @ c) types [] in
   f.globals <- globs @ f.globals;
   (* Visit the file, resetting to_add when encoutering a function (since sids
    * are unique only within a function) and inserting values of to_add in
@@ -211,10 +210,7 @@ let gf () =
 let process_imeta vis = if !visit_inline then function
     | Ext_id id ->
       let lvar, name = from_id id in
-      let s = begin match vis#current_kinstr with
-        | Kglobal -> assert false
-        | Kstmt s -> s
-      end in
+      let s = Extlib.the vis#current_stmt in
       let gf = gf () in
       List.iter (fun (v : stmt) ->
           add_to_hash_list Stmt_Hashtbl.(find_opt, replace) to_add s v
diff --git a/meta_bindings.mli b/meta_bindings.mli
index 15eccb7..d079ec2 100644
--- a/meta_bindings.mli
+++ b/meta_bindings.mli
@@ -21,14 +21,15 @@
 
 open Cil_types
 open Logic_typing
+open Meta_utils
 
-val types : (string, Cil_types.logic_type) Hashtbl.t
+val types : Cil_types.logic_type Str_Hashtbl.t
 val parse_bound : typing_context -> location ->
-  (string, logic_var) Hashtbl.t -> Logic_ptree.lexpr -> term
+  logic_var Str_Hashtbl.t -> Logic_ptree.lexpr -> term
 val parse_bind : typing_context -> location -> string -> string ->
   acsl_extension_kind
 val after_parse : typing_context -> predicate ->
-  (string, logic_var) Hashtbl.t -> predicate
+  logic_var Str_Hashtbl.t -> predicate
 val add_ghost_code : Meta_options.meta_flags -> unit
 
 val process_imeta: Acsl_extension.extension_visitor
diff --git a/meta_deduce.ml b/meta_deduce.ml
index 4b0a0e7..e49b569 100644
--- a/meta_deduce.ml
+++ b/meta_deduce.ml
@@ -1,4 +1,5 @@
 open Cil_types
+open Meta_utils
 open Meta_options
 open Meta_parse
 
diff --git a/meta_dispatch.ml b/meta_dispatch.ml
index 7d68eb6..020c04a 100644
--- a/meta_dispatch.ml
+++ b/meta_dispatch.ml
@@ -20,6 +20,7 @@
 (**************************************************************************)
 
 open Cil_types
+open Meta_utils
 open Meta_parse
 open Meta_options
 
diff --git a/meta_dispatch.mli b/meta_dispatch.mli
index b70d07b..3232d36 100644
--- a/meta_dispatch.mli
+++ b/meta_dispatch.mli
@@ -20,6 +20,7 @@
 (**************************************************************************)
 
 open Cil_types
+open Meta_utils
 open Meta_parse
 open Meta_options
 
diff --git a/meta_options.ml b/meta_options.ml
index 09ab601..937e8b6 100644
--- a/meta_options.ml
+++ b/meta_options.ml
@@ -107,14 +107,3 @@ type meta_flags = {
   keep_proof_files : bool;
   default_to_assert : bool;
 }
-
-let find_hash_list find_opt table key =
-  match find_opt table key with
-    | Some l -> l
-    | None -> []
-
-(* In a hashtable mapping key to lists of values, adds v to that list *)
-let add_to_hash_list (find_opt, replace) table key v =
-  let old_list = find_hash_list find_opt table key in
-  replace table key (v :: old_list)
-
diff --git a/meta_parse.ml b/meta_parse.ml
index 618d634..f5688bb 100644
--- a/meta_parse.ml
+++ b/meta_parse.ml
@@ -23,6 +23,7 @@ open Logic_ptree
 open Logic_typing
 open Cil_types
 open Meta_options
+open Meta_utils
 
 (* Define builtins *)
 type context =
@@ -34,11 +35,6 @@ type context =
   | Postcond
   | Precond
 
-module StrSet = Datatype.String.Set
-module Str_Hashtbl = Datatype.String.Hashtbl
-module Stmt_Hashtbl = Cil_datatype.Stmt.Hashtbl
-module Fundec_Hashtbl = Cil_datatype.Fundec.Hashtbl
-
 type target =
   | TgAll
   | TgSet of StrSet.t
@@ -154,7 +150,7 @@ let meta_type_term termassoc quantifiers kf loc orig_ctxt meta_ctxt env expr =
  * a full custom predicate
 *)
 let process_meta_termassoc typing_context loc expr kf termassoc =
-  let quantifiers = Hashtbl.create 5 in
+  let quantifiers = Str_Hashtbl.create 5 in
   let meta_tc =
     {typing_context with
        type_predicate = (meta_type_predicate loc typing_context);
@@ -463,8 +459,9 @@ let metaproperties () =
       !gathered_props in
   begin match check_for_duplicates sorted_props with
     | None -> ()
-    | Some (m1, m2) -> Self.abort "The meta-property named %s is defined at \
-                                   least twice :@,Here: %a@,and here: %a" m1.mp_name Printer.pp_location m1.mp_loc
-                         Printer.pp_location m2.mp_loc
+    | Some (m1, m2) ->
+      Self.abort "The meta-property named %s is defined at \
+                  least twice :@,Here: %a@,and here: %a"
+        m1.mp_name Printer.pp_location m1.mp_loc Printer.pp_location m2.mp_loc
   end ;
   List.rev !gathered_props
diff --git a/meta_parse.mli b/meta_parse.mli
index a8d26d7..cc62307 100644
--- a/meta_parse.mli
+++ b/meta_parse.mli
@@ -20,6 +20,7 @@
 (**************************************************************************)
 
 open Cil_types
+open Meta_utils
 
 type context =
   | Weak_invariant
@@ -30,11 +31,6 @@ type context =
   | Postcond
   | Precond
 
-module StrSet = Datatype.String.Set
-module Str_Hashtbl = Datatype.String.Hashtbl
-module Stmt_Hashtbl = Cil_datatype.Stmt.Hashtbl
-module Fundec_Hashtbl = Cil_datatype.Fundec.Hashtbl
-
 type target =
   | TgAll
   | TgSet of StrSet.t
diff --git a/meta_utils.ml b/meta_utils.ml
new file mode 100644
index 0000000..41e812e
--- /dev/null
+++ b/meta_utils.ml
@@ -0,0 +1,15 @@
+module StrSet = Datatype.String.Set
+module Str_Hashtbl = Datatype.String.Hashtbl
+module Stmt_Hashtbl = Cil_datatype.Stmt.Hashtbl
+module Fundec_Hashtbl = Cil_datatype.Fundec.Hashtbl
+
+let find_hash_list find_opt table key =
+  match find_opt table key with
+    | Some l -> l
+    | None -> []
+
+(* In a hashtable mapping key to lists of values, adds v to that list *)
+let add_to_hash_list (find_opt, replace) table key v =
+  let old_list = find_hash_list find_opt table key in
+  replace table key (v :: old_list)
+
-- 
GitLab