diff --git a/.envrc b/.envrc index ac6adec59..1d953f4bd 100644 --- a/.envrc +++ b/.envrc @@ -1,3 +1 @@ -use flake - -make githooks +use nix diff --git a/flake.lock b/flake.lock deleted file mode 100644 index 2b70d8935..000000000 --- a/flake.lock +++ /dev/null @@ -1,196 +0,0 @@ -{ - "nodes": { - "flake-compat": { - "flake": false, - "locked": { - "lastModified": 1747046372, - "narHash": "sha256-CIVLLkVgvHYbgI2UpXvIIBJ12HWgX+fjA8Xf8PUmqCY=", - "owner": "edolstra", - "repo": "flake-compat", - "rev": "9100a0f413b0c601e0533d1d94ffd501ce2e7885", - "type": "github" - }, - "original": { - "owner": "edolstra", - "repo": "flake-compat", - "type": "github" - } - }, - "flake-utils": { - "inputs": { - "systems": "systems" - }, - "locked": { - "lastModified": 1731533236, - "narHash": "sha256-l0KFg5HjrsfsO/JpG+r7fRrqm12kzFHyUHqHCVpMMbI=", - "owner": "numtide", - "repo": "flake-utils", - "rev": "11707dc2f618dd54ca8739b309ec4fc024de578b", - "type": "github" - }, - "original": { - "owner": "numtide", - "repo": "flake-utils", - "type": "github" - } - }, - "mirage-opam-overlays": { - "flake": false, - "locked": { - "lastModified": 1710922379, - "narHash": "sha256-j4QREQDUf8oHOX7qg6wAOupgsNQoYlufxoPrgagD+pY=", - "owner": "dune-universe", - "repo": "mirage-opam-overlays", - "rev": "797cb363df3ff763c43c8fbec5cd44de2878757e", - "type": "github" - }, - "original": { - "owner": "dune-universe", - "repo": "mirage-opam-overlays", - "type": "github" - } - }, - "nixpkgs": { - "locked": { - "lastModified": 1751792365, - "narHash": "sha256-J1kI6oAj25IG4EdVlg2hQz8NZTBNYvIS0l4wpr9KcUo=", - "owner": "nixos", - "repo": "nixpkgs", - "rev": "1fd8bada0b6117e6c7eb54aad5813023eed37ccb", - "type": "github" - }, - "original": { - "owner": "nixos", - "ref": "nixos-unstable", - "repo": "nixpkgs", - "type": "github" - } - }, - "opam-nix": { - "inputs": { - "flake-compat": "flake-compat", - "flake-utils": "flake-utils", - "mirage-opam-overlays": "mirage-opam-overlays", - "nixpkgs": "nixpkgs", - "opam-overlays": "opam-overlays", - "opam-repository": [ - "opam-repository" - ], - "opam2json": "opam2json" - }, - "locked": { - "lastModified": 1753007101, - "narHash": "sha256-YYdS644zHwmyBY0RYdrhO05uT3xauqJ5Ww1KtN9Q3Z4=", - "owner": "tweag", - "repo": "opam-nix", - "rev": "03dd8b2577c05c42dc9e319d290f2dbfc67ab38b", - "type": "github" - }, - "original": { - "owner": "tweag", - "repo": "opam-nix", - "type": "github" - } - }, - "opam-overlays": { - "flake": false, - "locked": { - "lastModified": 1741116009, - "narHash": "sha256-Z0PIW82fHJFvAv/JYpAffnp2DaOjLhsPutqyIrORZd0=", - "owner": "dune-universe", - "repo": "opam-overlays", - "rev": "e031bb64e33bf93be963e9a38b28962e6e14381f", - "type": "github" - }, - "original": { - "owner": "dune-universe", - "repo": "opam-overlays", - "type": "github" - } - }, - "opam-repository": { - "flake": false, - "locked": { - "lastModified": 1754317519, - "narHash": "sha256-7KQkx5spZ2M4B51Ls3pRkX1SkETv/de6/XeWjDdNJ3A=", - "owner": "ocaml", - "repo": "opam-repository", - "rev": "3dab8c734b15bf2b5c1d8b99bb134f51361a6bee", - "type": "github" - }, - "original": { - "owner": "ocaml", - "repo": "opam-repository", - "type": "github" - } - }, - "opam2json": { - "inputs": { - "nixpkgs": [ - "opam-nix", - "nixpkgs" - ], - "systems": "systems_2" - }, - "locked": { - "lastModified": 1749457947, - "narHash": "sha256-+QVm+HOYikF3wUhqSIV8qJbE/feSG+p48fgxIosbHS0=", - "owner": "tweag", - "repo": "opam2json", - "rev": "0ecd66fc2bfb25d910522c990dd36412259eac1f", - "type": "github" - }, - "original": { - "owner": "tweag", - "repo": "opam2json", - "type": "github" - } - }, - "root": { - "inputs": { - "flake-utils": [ - "opam-nix", - "flake-utils" - ], - "nixpkgs": [ - "opam-nix", - "nixpkgs" - ], - "opam-nix": "opam-nix", - "opam-repository": "opam-repository" - } - }, - "systems": { - "locked": { - "lastModified": 1681028828, - "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", - "owner": "nix-systems", - "repo": "default", - "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", - "type": "github" - }, - "original": { - "owner": "nix-systems", - "repo": "default", - "type": "github" - } - }, - "systems_2": { - "locked": { - "lastModified": 1681028828, - "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=", - "owner": "nix-systems", - "repo": "default", - "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e", - "type": "github" - }, - "original": { - "owner": "nix-systems", - "repo": "default", - "type": "github" - } - } - }, - "root": "root", - "version": 7 -} diff --git a/flake.nix b/flake.nix deleted file mode 100644 index 9003d1259..000000000 --- a/flake.nix +++ /dev/null @@ -1,69 +0,0 @@ -{ - inputs = { - opam-repository = { - url = "github:ocaml/opam-repository"; - flake = false; - }; - opam-nix = { - url = "github:tweag/opam-nix"; - inputs.opam-repository.follows = "opam-repository"; - }; - flake-utils.follows = "opam-nix/flake-utils"; - nixpkgs.follows = "opam-nix/nixpkgs"; - }; - outputs = - { - flake-utils, - opam-nix, - nixpkgs, - ... - }: - flake-utils.lib.eachDefaultSystem ( - system: - let - pkgs = nixpkgs.legacyPackages.${system}; - on = opam-nix.lib.${system}; - localPackagesQuery = builtins.mapAttrs (_: pkgs.lib.last) (on.listRepo (on.makeOpamRepo ./.)); - devPackagesQuery = { - # You can add "development" packages here. They will get added to the devShell automatically. - ocaml-lsp-server = "*"; - ocamlformat = "*"; - odoc = "3.1.0"; - }; - query = devPackagesQuery // { - ## You can force versions of certain packages here, e.g: - ## - force the ocaml compiler to be taken from opam-repository: - ocaml-base-compiler = "*"; - ## - or force the compiler to be taken from nixpkgs and be a certain version: - # ocaml-system = "4.14.0"; - ## - or force ocamlfind to be a certain version: - # ocamlfind = "1.9.2"; - }; - scope = on.buildOpamProject' { } ./. query; - overlay = final: prev: { - # You can add overrides here - }; - scope' = scope.overrideScope overlay; - # Packages from devPackagesQuery - devPackages = builtins.attrValues (pkgs.lib.getAttrs (builtins.attrNames devPackagesQuery) scope'); - # Packages in this workspace - packages = pkgs.lib.getAttrs (builtins.attrNames localPackagesQuery) scope'; - in - { - legacyPackages = scope'; - - inherit packages; - - devShells.default = pkgs.mkShell { - inputsFrom = builtins.attrValues packages; - buildInputs = devPackages ++ [ - # You can add packages from nixpkgs here - pkgs.z3 - ]; - shellHook = '' - export NO_OPAM_EXEC=1 - ''; - }; - } - ); -} diff --git a/shell.nix b/shell.nix new file mode 100644 index 000000000..987a2be41 --- /dev/null +++ b/shell.nix @@ -0,0 +1,13 @@ +{ pkgs ? import {} }: + +pkgs.mkShell rec { + packages = with pkgs; [ + opam + gnumake + z3 + ]; + shellHook = '' + make githooks > /dev/null + eval $(opam env) + ''; +} diff --git a/wisl/lib/state_ex/wislSHeap.ml b/wisl/lib/state_ex/wislSHeap.ml index 6989ba291..0cea3cc4f 100644 --- a/wisl/lib/state_ex/wislSHeap.ml +++ b/wisl/lib/state_ex/wislSHeap.ml @@ -168,14 +168,16 @@ 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 @@ -183,12 +185,12 @@ let set_cell heap loc_name ofs v = | 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 diff --git a/wisl/lib/state_ex/wislSHeap.mli b/wisl/lib/state_ex/wislSHeap.mli index 63c00b01a..377cbbd8c 100644 --- a/wisl/lib/state_ex/wislSHeap.mli +++ b/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 diff --git a/wisl/lib/state_ex/wislSMemory.ml b/wisl/lib/state_ex/wislSMemory.ml index 7e0f5eda7..ad1923b44 100644 --- a/wisl/lib/state_ex/wislSMemory.ml +++ b/wisl/lib/state_ex/wislSMemory.ml @@ -19,21 +19,16 @@ let init () = WislSHeap.init () let get_init_data _ = () let clear _ = WislSHeap.init () -let resolve_loc loc = +let resolve_loc ?(alloc_if_missing = false) loc = let* loc_opt = Delayed.resolve_loc loc in - match loc_opt with - | None -> error (WislSHeap.InvalidLocation loc) - | Some loc -> ok loc - -let resolve_loc_or_alloc loc = - let* resolved_loc_opt = Delayed.resolve_loc loc in - (* If we can't find the location, we create a new location and we + match (loc_opt, alloc_if_missing) with + | Some loc, _ -> ok loc + | None, false -> error (WislSHeap.InvalidLocation loc) + | None, true -> + (* If we can't find the location, we create a new location and we add to the path condition that it is equal to the given loc *) - match resolved_loc_opt with - | Some loc_name -> Delayed.return loc_name - | None -> let al = ALoc.alloc () in - Delayed.return ~learned:[ BinOp (ALoc al, Equal, loc) ] al + ok ~learned:[ BinOp (ALoc al, Equal, loc) ] al let get_cell heap (loc : vt) (offset : vt) = let** loc = resolve_loc loc in @@ -41,9 +36,9 @@ let get_cell heap (loc : vt) (offset : vt) = let loc = Expr.loc_from_loc_name loc in (heap, [ loc; ofs; value ]) -let set_cell heap (loc : vt) (offset : vt) (value : vt) = - let* loc = resolve_loc_or_alloc loc in - let++ () = WislSHeap.set_cell heap loc offset value in +let set_cell ~alloc_if_missing heap (loc : vt) (offset : vt) (value : vt) = + let** loc = resolve_loc ~alloc_if_missing loc in + let++ () = WislSHeap.set_cell ~alloc_if_missing heap loc offset value in (heap, []) let rem_cell heap (loc : vt) (offset : vt) = @@ -58,9 +53,9 @@ let get_bound heap loc = let loc = Expr.loc_from_loc_name loc in (heap, [ loc; b ]) -let set_bound heap (loc : vt) (bound : int) = - let* loc = resolve_loc_or_alloc loc in - let++ () = WislSHeap.set_bound heap loc bound in +let set_bound ~alloc_if_missing heap (loc : vt) (bound : int) = + let** loc = resolve_loc ~alloc_if_missing loc in + let++ () = WislSHeap.set_bound ~alloc_if_missing heap loc bound in (heap, []) let rem_bound heap loc = @@ -74,10 +69,10 @@ let get_freed heap loc = let loc = Expr.loc_from_loc_name loc in (heap, [ loc ]) -let set_freed heap (loc : vt) = - let* loc = resolve_loc_or_alloc loc in - let+ () = WislSHeap.set_freed heap loc in - Ok (heap, []) +let set_freed ~alloc_if_missing heap (loc : vt) = + let** loc = resolve_loc ~alloc_if_missing loc in + let++ () = WislSHeap.set_freed ~alloc_if_missing heap loc in + (heap, []) let rem_freed heap loc = let** loc = resolve_loc loc in @@ -93,17 +88,23 @@ let dispose heap loc = let++ () = WislSHeap.dispose heap loc in (heap, []) -let execute_action ~action_name heap (args : vt list) = +let execute_action + ?(alloc_if_missing = false) + ~action_name + heap + (args : vt list) = let action = WislLActions.ac_from_str action_name in match (action, args) with | (Load | GetCell), [ loc; ofs ] -> get_cell heap loc ofs - | (Store | SetCell), [ loc; ofs; value ] -> set_cell heap loc ofs value + | (Store | SetCell), [ loc; ofs; value ] -> + set_cell ~alloc_if_missing heap loc ofs value | RemCell, [ loc; ofs ] -> rem_cell heap loc ofs | GetBound, [ loc ] -> get_bound heap loc - | SetBound, [ loc; Lit (Int b) ] -> set_bound heap loc (Z.to_int b) + | SetBound, [ loc; Lit (Int b) ] -> + set_bound ~alloc_if_missing heap loc (Z.to_int b) | RemBound, [ loc ] -> rem_bound heap loc | GetFreed, [ loc ] -> get_freed heap loc - | SetFreed, [ loc ] -> set_freed heap loc + | SetFreed, [ loc ] -> set_freed ~alloc_if_missing heap loc | RemFreed, [ loc ] -> rem_freed heap loc | Alloc, [ Lit (Int size) ] when Z.geq size Z.one -> alloc heap (Z.to_int size) @@ -146,7 +147,9 @@ let produce ~core_pred heap args = | Error _ -> Delayed.return () | Ok _ -> vanish () in - let* set_res = execute_action ~action_name:setter heap args in + let* set_res = + execute_action ~alloc_if_missing:true ~action_name:setter heap args + in match set_res with | Error _ -> (* It's ok for failing producers to vanish, no unsoundness *) @@ -214,3 +217,4 @@ let can_fix = function let get_failing_constraint _ = Expr.true_ let sure_is_nonempty t = not (WislSHeap.is_empty t) let split_further _ _ _ _ = None +let execute_action = execute_action ?alloc_if_missing:None