From 754a4b95bb451dbdb6aabcfc700e7bb9a92143b1 Mon Sep 17 00:00:00 2001
From: Pierre Villemot <pierre.villemot@ocamlpro.com>
Date: Thu, 22 Aug 2024 16:54:15 +0200
Subject: [PATCH] Remove some polymorphic hashtables

We should not use polymorphic equality on expressions because they may
contain recursive terms producing by Dolmen. This PR removes these
dangerous hashtables.
---
 src/lib/reasoners/uf.ml     | 51 ++++++++++++++++++-------------------
 src/lib/structures/expr.ml  |  7 +++++
 src/lib/structures/expr.mli |  2 +-
 3 files changed, 33 insertions(+), 27 deletions(-)

diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml
index eefe70e82..4049634cf 100644
--- a/src/lib/reasoners/uf.ml
+++ b/src/lib/reasoners/uf.ml
@@ -1137,31 +1137,30 @@ let terms env =
 
 (* Helper functions used by the caches during the computation of the model. *)
 module Cache = struct
-  let store_array_get arrays_cache (t : Expr.t) (i : Expr.t) (v : Expr.t) =
-    match Hashtbl.find_opt arrays_cache t with
-    | Some values ->
-      Hashtbl.replace values i v
-    | None ->
-      let values = Hashtbl.create 17 in
-      Hashtbl.add values i v;
-      Hashtbl.add arrays_cache t values
-
-  let get_abstract_for abstracts_cache env (t : Expr.t) =
+  let store_array_get arrays_cache (t : E.t) (i : E.t) (v : E.t) =
+    match E.Table.find arrays_cache t with
+    | exception Not_found ->
+      let values = E.Table.create 17 in
+      E.Table.add values i v;
+      E.Table.add arrays_cache t values
+    | values ->
+      E.Table.replace values i v
+
+  let get_abstract_for abstracts_cache env (t : E.t) =
     let r, _ = find env t in
-    match Hashtbl.find_opt abstracts_cache r with
-    | Some abstract -> abstract
-    | None ->
-      let abstract = Expr.mk_abstract (Expr.type_info t) in
-      Hashtbl.add abstracts_cache r abstract;
+    match Shostak.HX.find abstracts_cache r with
+    | exception Not_found ->
+      let abstract = E.mk_abstract (E.type_info t) in
+      Shostak.HX.add abstracts_cache r abstract;
       abstract
+    | abstract -> abstract
 end
 
 type cache = {
-  array_selects: (Expr.t, (Expr.t, Expr.t) Hashtbl.t)
-      Hashtbl.t;
+  array_selects: Expr.t E.Table.t E.Table.t;
   (** Stores all the get accesses to arrays. *)
 
-  abstracts: (r, Expr.t) Hashtbl.t;
+  abstracts: Expr.t Shostak.HX.t;
   (** Stores all the abstract values generated. This cache is necessary
       to ensure we don't generate twice an abstract value for a given symbol. *)
 }
@@ -1212,13 +1211,13 @@ let compute_concrete_model_of_val cache =
         match f, arg_vals, ty with
         | Sy.Name _, [], Ty.Tfarray _ ->
           begin
-            match Hashtbl.find_opt cache.array_selects t with
-            | Some _ -> acc
-            | None ->
+            match E.Table.find cache.array_selects t with
+            | exception Not_found ->
               (* We have to add an abstract array in case there is no
                  constraint on its values. *)
-              Hashtbl.add cache.array_selects t (Hashtbl.create 17);
+              E.Table.add cache.array_selects t (E.Table.create 17);
               acc
+            | _ -> acc
           end
 
         | Sy.Op Sy.Set, _, _ -> acc
@@ -1258,13 +1257,13 @@ let extract_concrete_model cache =
         terms (ModelMap.empty ~suspicious declared_ids, ME.empty)
     in
     let model =
-      Hashtbl.fold (fun t vals mdl ->
+      E.Table.fold (fun t vals mdl ->
           (* We produce a fresh identifiant for abstract value in order to
              prevent any capture. *)
           let abstract = get_abstract_for env t in
           let ty = Expr.type_info t in
           let arr_val =
-            Hashtbl.fold (fun i v arr_val ->
+            E.Table.fold (fun i v arr_val ->
                 Expr.ArraysEx.store arr_val i v
               ) vals abstract
           in
@@ -1299,7 +1298,7 @@ let extract_concrete_model cache =
 
 let extract_concrete_model ~prop_model ~declared_ids =
   let cache : cache = {
-    array_selects = Hashtbl.create 17;
-    abstracts = Hashtbl.create 17;
+    array_selects = E.Table.create 17;
+    abstracts = Shostak.HX.create 17;
   }
   in fun env -> extract_concrete_model cache ~prop_model ~declared_ids env
diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml
index b9bd5fc46..7fec2a89e 100644
--- a/src/lib/structures/expr.ml
+++ b/src/lib/structures/expr.ml
@@ -3267,3 +3267,10 @@ module ArraysEx = struct
   let store a i v =
     mk_term Sy.(Op Set) [a; i; v] (type_info a)
 end
+
+module Table =
+  Hashtbl.Make (struct
+    type nonrec t = t
+    let hash = hash
+    let equal = equal
+  end)
diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli
index 8c639480c..7b30236e4 100644
--- a/src/lib/structures/expr.mli
+++ b/src/lib/structures/expr.mli
@@ -155,8 +155,8 @@ and trigger = private {
   from_user : bool;
 }
 
+module Table : Hashtbl.S with type key = t
 module Set : Set.S with type elt = t
-
 module Map : Map.S with type key = t
 
 type subst = t Var.Map.t * Ty.subst