Fix WISL cell creation bug

.envrc

@@ -1,3 +1 @@
-use flake
-
-make githooks
+use nix

shell.nix

@@ -0,0 +1,13 @@
+{ pkgs ? import <nixpkgs> {} }:
+
+pkgs.mkShell rec {
+  packages = with pkgs; [
+    opam
+    gnumake
+    z3
+  ];
+  shellHook = ''
+    make githooks > /dev/null
+    eval $(opam env)
+  '';
+}

wisl/lib/state_ex/wislSHeap.ml

@@ -168,27 +168,29 @@ let get_cell heap loc ofs =
             | Some (o, v) -> ok (loc, o, v)
             | None -> error (MissingResource (Cell, loc, Some ofs))))
 
-let set_cell heap loc_name ofs v =
-  match Hashtbl.find_opt heap loc_name with
+let set_cell ~alloc_if_missing heap loc ofs v =
+  match Hashtbl.find_opt heap loc with
   | None ->
-      let data = SFVL.add ofs v SFVL.empty in
-      let bound = None in
-      let () = Hashtbl.replace heap loc_name (Allocated { data; bound }) in
-      ok ()
-  | Some Block.Freed -> error (UseAfterFree loc_name)
+      if alloc_if_missing then
+        let data = SFVL.add ofs v SFVL.empty in
+        let bound = None in
+        let () = Hashtbl.replace heap loc (Allocated { data; bound }) in
+        ok ()
+      else error (MissingResource (Cell, loc, Some ofs))
+  | Some Block.Freed -> error (UseAfterFree loc)
   | Some (Allocated { data; bound }) ->
       let** () =
         match bound with
         | None -> ok ()
         | Some n ->
             let n = Expr.int n in
             let open Expr.Infix in
-            if%sat n <= ofs then error (UseAfterFree loc_name) else ok ()
+            if%sat n <= ofs then error (UseAfterFree loc) else ok ()
       in
       let* { pfs; gamma; matching } = Delayed.leak_pc_copy () in
       let equality_test = Solver.is_equal ~matching ~pfs ~gamma in
       let data = SFVL.add_with_test ~equality_test ofs v data in
-      let () = Hashtbl.replace heap loc_name (Allocated { data; bound }) in
+      let () = Hashtbl.replace heap loc (Allocated { data; bound }) in
       ok ()
 
 let rem_cell heap loc offset =
@@ -210,8 +212,13 @@ let get_bound heap loc =
       error (MissingResource (Bound, loc, None))
   | Some (Allocated { bound = Some bound; _ }) -> ok bound
 
-let set_bound heap loc bound =
-  let prev = Option.value ~default:Block.empty (Hashtbl.find_opt heap loc) in
+let set_bound ~alloc_if_missing heap loc bound =
+  let** prev =
+    match (Hashtbl.find_opt heap loc, alloc_if_missing) with
+    | Some b, _ -> ok b
+    | None, true -> ok Block.empty
+    | None, false -> error (MissingResource (Cell, loc, None))
+  in
   match prev with
   | Freed -> error (UseAfterFree loc)
   | Allocated { data; _ } ->
@@ -235,9 +242,12 @@ let get_freed heap loc =
   | Some _ -> error MemoryLeak
   | None -> error (MissingResource (Freed, loc, None))
 
-let set_freed heap loc =
-  set_freed_with_logging heap loc;
-  Delayed.return ()
+let set_freed ~alloc_if_missing heap loc =
+  match (Hashtbl.find_opt heap loc, alloc_if_missing) with
+  | Some _, _ | None, true ->
+      set_freed_with_logging heap loc;
+      ok ()
+  | None, false -> error (MissingResource (Cell, loc, None))
 
 let rem_freed heap loc =
   match Hashtbl.find_opt heap loc with

wisl/lib/state_ex/wislSHeap.mli

@@ -21,13 +21,26 @@ val is_empty : t -> bool
 val get_cell :
   t -> string -> Expr.t -> (string * Expr.t * Expr.t, err) Delayed_result.t
 
-val set_cell : t -> string -> Expr.t -> Expr.t -> (unit, err) Delayed_result.t
+val set_cell :
+  alloc_if_missing:bool ->
+  t ->
+  string ->
+  Expr.t ->
+  Expr.t ->
+  (unit, err) Delayed_result.t
+
 val rem_cell : t -> string -> Expr.t -> (unit, err) Delayed_result.t
 val get_bound : t -> string -> (int, err) Delayed_result.t
-val set_bound : t -> string -> int -> (unit, err) Delayed_result.t
+
+val set_bound :
+  alloc_if_missing:bool -> t -> string -> int -> (unit, err) Delayed_result.t
+
 val rem_bound : t -> string -> (unit, err) Delayed_result.t
 val get_freed : t -> string -> (unit, err) Delayed_result.t
-val set_freed : t -> string -> unit Delayed.t
+
+val set_freed :
+  alloc_if_missing:bool -> t -> string -> (unit, err) Delayed_result.t
+
 val rem_freed : t -> string -> (unit, err) Delayed_result.t
 val pp : t Fmt.t
 val copy : t -> t