simplify store + tiny bug in the engine (#262)

* fix a tiny bug first Signed-off-by: Sacha Ayoun <[email protected]> * simplify the store Signed-off-by: Sacha Ayoun <[email protected]> --------- Signed-off-by: Sacha Ayoun <[email protected]>
GillianPlatform · Sep 18, 2023 · 5e15c33 · 5e15c33
1 parent 8306c3c
commit 5e15c33
Show file tree

Hide file tree

Showing 7 changed files with 31 additions and 80 deletions.
diff --git a/GillianCore/engine/Abstraction/Verifier.ml b/GillianCore/engine/Abstraction/Verifier.ml
@@ -500,7 +500,7 @@ struct
           L.Parent.with_id parent_id (fun () ->
               let store = SPState.get_store final_state in
               let () =
-                SStore.filter store (fun x v ->
+                SStore.filter_map_inplace store (fun x v ->
                     if x = Names.return_variable then Some v else None)
               in
               let subst = make_post_subst test final_state in

diff --git a/GillianCore/engine/BiAbduction/Abductor.ml b/GillianCore/engine/BiAbduction/Abductor.ml
@@ -86,7 +86,7 @@ module Make
             params SPState.pp state_af SPState.pp state_f);
       (* Drop all pvars except ret/err from the state *)
       let () =
-        SStore.filter (SPState.get_store state_f) (fun x v ->
+        SStore.filter_map_inplace (SPState.get_store state_f) (fun x v ->
             if x = Names.return_variable then Some v else None)
       in
       let* post =

diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml
@@ -864,7 +864,7 @@ struct
                       process_ret true ret_state fl b_counter (Some others)
                         spec_name
                       :: others
-                  | _ -> failwith "unreachable"
+                  | [] -> []
                 in
                 let error_confs =
                   match errors with

diff --git a/GillianCore/engine/general_semantics/store.ml b/GillianCore/engine/general_semantics/store.ml
@@ -22,7 +22,7 @@ module type S = sig
   val domain : t -> Var.Set.t
 
   (** Store filtering *)
-  val filter : t -> (Var.t -> vt -> vt option) -> unit
+  val filter_map_inplace : t -> (Var.t -> vt -> vt option) -> unit
 
   (** Store fold *)
   val fold : t -> (Var.t -> vt -> 'a -> 'a) -> 'a -> 'a
@@ -63,9 +63,6 @@ module type S = sig
   (** Converts the store into an ssubst *)
   val to_ssubst : t -> SESubst.t
 
-  (** Symbolic indices *)
-  val symbolics : t -> Var.Set.t
-
   (** Logical variables *)
   val lvars : t -> Var.Set.t
 end
@@ -78,8 +75,7 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
   type vt = Val.t [@@deriving yojson]
 
   (** Actual type of GIL Stores *)
-  type t = { conc : (Var.t, vt) Hashtbl.t; symb : (Var.t, vt) Hashtbl.t }
-  [@@deriving yojson]
+  type t = (Var.t, vt) Hashtbl.t [@@deriving yojson]
 
   (**
     Store initialisation
@@ -88,27 +84,15 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
     @return Newly constructed and initialised store
   *)
   let init (vars_and_vals : (Var.t * vt) list) : t =
-    let new_store =
-      {
-        conc = Hashtbl.create Config.big_tbl_size;
-        symb = Hashtbl.create Config.big_tbl_size;
-      }
-    in
-    List.iter
-      (fun (x, v) ->
-        if Val.is_concrete v then Hashtbl.replace new_store.conc x v
-        else Hashtbl.replace new_store.symb x v)
-      vars_and_vals;
-    new_store
+    Hashtbl.of_seq (List.to_seq vars_and_vals)
 
   (**
     Store copy
 
     @param store Target store
     @return Copy of the given store
   *)
-  let copy (store : t) : t =
-    { conc = Hashtbl.copy store.conc; symb = Hashtbl.copy store.symb }
+  let copy (store : t) : t = Hashtbl.copy store
 
   (**
     Store lookup
@@ -117,9 +101,7 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
     @param x Target variable
     @return Optional value of the variable in the store
   *)
-  let get (store : t) (x : Var.t) : vt option =
-    let result = Hashtbl.find_opt store.conc x in
-    if result = None then Hashtbl.find_opt store.symb x else result
+  let get (store : t) (x : Var.t) : vt option = Hashtbl.find_opt store x
 
   (**
     Store get with throw
@@ -132,11 +114,7 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
   let get_unsafe (store : t) (v : Var.t) : vt =
     match get store v with
     | Some result -> result
-    | None ->
-        raise
-          (Failure
-             (Printf.sprintf "Store.get_unsafe: variable %s not found in store"
-                v))
+    | None -> Fmt.failwith "Store.get_unsafe: variable %s not found in store" v
 
   (**
     Store update (in-place)
@@ -145,23 +123,15 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
     @param x Target variable
     @param v Value to be put
   *)
-  let put (store : t) (x : Var.t) (v : vt) : unit =
-    let add, rem =
-      if Val.is_concrete v then (store.conc, store.symb)
-      else (store.symb, store.conc)
-    in
-    Hashtbl.replace add x v;
-    Hashtbl.remove rem x
+  let put (store : t) (x : Var.t) (v : vt) : unit = Hashtbl.replace store x v
 
   (**
     Store removal (in-place)
 
     @param store Target store
     @param x Target variable
   *)
-  let remove (store : t) (x : Var.t) : unit =
-    Hashtbl.remove store.conc x;
-    Hashtbl.remove store.symb x
+  let remove (store : t) (x : Var.t) : unit = Hashtbl.remove store x
 
   (**
     Store membership check
@@ -170,18 +140,15 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
     @param x Target variable
     @return true if the variable is in the store, false otherwise
   *)
-  let mem (store : t) (x : Var.t) : bool =
-    Hashtbl.mem store.conc x || Hashtbl.mem store.symb x
+  let mem (store : t) (x : Var.t) : bool = Hashtbl.mem store x
 
   (**
     Store iterator
 
     @param store Target store
     @param f Iterator function
   *)
-  let iter (store : t) (f : Var.t -> vt -> unit) : unit =
-    Hashtbl.iter f store.conc;
-    Hashtbl.iter f store.symb
+  let iter (store : t) (f : Var.t -> vt -> unit) : unit = Hashtbl.iter f store
 
   (**
     Store fold
@@ -191,7 +158,7 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
     @param ac Accumulator
   *)
   let fold (store : t) (f : Var.t -> vt -> 'a -> 'a) (ac : 'a) : 'a =
-    Hashtbl.fold f store.symb (Hashtbl.fold f store.conc ac)
+    Hashtbl.fold f store ac
 
   (**
     Store bindings
@@ -200,7 +167,7 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
     @return Bindings of the store formatted as (variable, value)
   *)
   let bindings (store : t) : (Var.t * vt) list =
-    fold store (fun x le ac -> (x, le) :: ac) []
+    Hashtbl.to_seq store |> List.of_seq
 
   (**
     Store domain
@@ -209,17 +176,16 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
     @return Set of variables that are in the domain of the store
   *)
   let domain (store : t) : Var.Set.t =
-    Var.Set.of_list (fold store (fun x _ ac -> x :: ac) [])
+    Hashtbl.to_seq_keys store |> Var.Set.of_seq
 
   (**
     Store filtering (in-place)
 
     @param store Target store
     @param f The filtering function
   *)
-  let filter (store : t) (f : Var.t -> vt -> vt option) : unit =
-    Hashtbl.filter_map_inplace f store.conc;
-    Hashtbl.filter_map_inplace f store.symb
+  let filter_map_inplace (store : t) (f : Var.t -> vt -> vt option) : unit =
+    Hashtbl.filter_map_inplace f store
 
   (**
     Store partition
@@ -242,10 +208,13 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
     @param xs List of variables to be projected
     @return New store that only contains the projected variables
   *)
-  let projection (store : t) (xs : Var.t list) : t =
-    let y = init [] in
-    List.iter (fun v -> if mem store v then put y v (get_unsafe store v)) xs;
-    y
+  let projection (store : t) (vars : Var.t list) : t =
+    let projected = Hashtbl.create (List.length vars) in
+    List.iter
+      (fun var ->
+        get store var |> Option.iter (fun value -> put projected var value))
+      vars;
+    projected
 
   (**
     Store printer
@@ -288,17 +257,8 @@ module Make (Val : Val.S) : S with type vt = Val.t = struct
     iter store (fun x v -> SESubst.put subst (Expr.PVar x) (Val.to_expr v));
     subst
 
-  (**
-    Variables that can be affected by substitution
-
-    @param target store
-    @return Set of variables that can be affected by substitution
-  *)
-  let symbolics (store : t) : Var.Set.t =
-    Hashtbl.fold (fun v _ ac -> Var.Set.add v ac) store.symb Var.Set.empty
-
   let lvars (store : t) : Var.Set.t =
     Hashtbl.fold
       (fun _ v ac -> Var.Set.union ac (Expr.lvars (Val.to_expr v)))
-      store.symb Var.Set.empty
+      store Var.Set.empty
 end
diff --git a/GillianCore/engine/general_semantics/store.mli b/GillianCore/engine/general_semantics/store.mli
@@ -22,7 +22,7 @@ module type S = sig
   val domain : t -> Var.Set.t
 
   (** Store filtering *)
-  val filter : t -> (Var.t -> vt -> vt option) -> unit
+  val filter_map_inplace : t -> (Var.t -> vt -> vt option) -> unit
 
   (** Store fold *)
   val fold : t -> (Var.t -> vt -> 'a -> 'a) -> 'a -> 'a
@@ -63,9 +63,6 @@ module type S = sig
   (** Converts the store into an ssubst *)
   val to_ssubst : t -> SVal.SESubst.t
 
-  (** Symbolic indices *)
-  val symbolics : t -> Var.Set.t
-
   (** Logical variables *)
   val lvars : t -> Var.Set.t
 end

diff --git a/GillianCore/engine/symbolic_semantics/SStore.ml b/GillianCore/engine/symbolic_semantics/SStore.ml
@@ -15,14 +15,9 @@ let substitution_in_place ?(subst_all = false) (subst : SESubst.t) (x : t) :
             Some (LVar x)
         | _ -> Some le);
 
-    let symbolics = symbolics x in
-    Var.Set.iter
-      (fun v ->
-        let le = Option.get (get x v) in
-        let s_le = SESubst.subst_in_expr store_subst ~partial:true le in
-        let s_le = if le <> s_le then Reduction.reduce_lexpr s_le else s_le in
-        if le <> s_le then put x v s_le)
-      symbolics)
+    filter_map_inplace x (fun _ value ->
+        let substed = SESubst.subst_in_expr store_subst ~partial:true value in
+        Some (Reduction.reduce_lexpr substed)))
 
 (** Returns the set containing all the vars occurring in --x-- *)
 let vars (x : t) : SS.t =

diff --git a/GillianCore/engine/symbolic_semantics/SStore.mli b/GillianCore/engine/symbolic_semantics/SStore.mli
@@ -19,7 +19,7 @@ val pp : Format.formatter -> t -> unit
 val pp_by_need : Containers.SS.t -> Format.formatter -> t -> unit
 val iter : t -> (Var.t -> Expr.t -> unit) -> unit
 val fold : t -> (Var.t -> Expr.t -> 'a -> 'a) -> 'a -> 'a
-val filter : t -> (Var.t -> Expr.t -> Expr.t option) -> unit
+val filter_map_inplace : t -> (Var.t -> Expr.t -> Expr.t option) -> unit
 val vars : t -> Var.Set.t
 val lvars : t -> Var.Set.t
 val clocs : t -> Var.Set.t
@@ -29,5 +29,4 @@ val substitution_in_place : ?subst_all:bool -> SVal.SESubst.t -> t -> unit
 val is_well_formed : t -> bool
 val bindings : t -> (Var.t * vt) list
 val to_ssubst : t -> SVal.SESubst.t
-val symbolics : t -> Var.Set.t
 val is_in : t -> Expr.t -> bool