From 94e508874dcab68de1f3320f44fcf71de8afa2ba Mon Sep 17 00:00:00 2001 From: N1ark Date: Fri, 19 Dec 2025 11:29:07 +0000 Subject: [PATCH 1/9] Use `Bimap` in `Fun_ctx` --- soteria-c/lib/fun_ctx.ml | 18 ++++-------------- soteria-rust/lib/state.ml | 2 +- soteria/lib/soteria_std/bimap.ml | 20 +++++++++++++++++--- 3 files changed, 22 insertions(+), 18 deletions(-) diff --git a/soteria-c/lib/fun_ctx.ml b/soteria-c/lib/fun_ctx.ml index 1887436b1..9ec122bf7 100644 --- a/soteria-c/lib/fun_ctx.ml +++ b/soteria-c/lib/fun_ctx.ml @@ -1,19 +1,9 @@ module Bidirectional_map = struct - module SMap = Symbol_std.Map - module IMap = Map.Make (Z) + include Bimap.Make (Symbol_std) (Z) - type t = { s_to_i : Z.t SMap.t; i_to_s : Symbol_std.t IMap.t } - - let empty = { s_to_i = SMap.empty; i_to_s = IMap.empty } - let has_sym s map = SMap.mem s map.s_to_i - - let add s i map = - let s_to_i = SMap.add s i map.s_to_i in - let i_to_s = IMap.add i s map.i_to_s in - { s_to_i; i_to_s } - - let get_loc_id s map = SMap.find_opt s map.s_to_i - let get_sym i map = IMap.find_opt i map.i_to_s + let has_sym = mem_l + let get_loc_id = find_l + let get_sym = find_r end (* FIXME: This is slightly off because we could have a location that is already assigned. diff --git a/soteria-rust/lib/state.ml b/soteria-rust/lib/state.ml index 4398c9e0d..5eebbd5a8 100644 --- a/soteria-rust/lib/state.ml +++ b/soteria-rust/lib/state.ml @@ -85,7 +85,7 @@ end) module FunBiMap = struct include - Bimap.Make + Bimap.MakePp (struct type t = T.sloc Typed.t diff --git a/soteria/lib/soteria_std/bimap.ml b/soteria/lib/soteria_std/bimap.ml index e69b4dacb..20509a363 100644 --- a/soteria/lib/soteria_std/bimap.ml +++ b/soteria/lib/soteria_std/bimap.ml @@ -4,8 +4,9 @@ correspondence between keys of type [KeyL] (left) and [KeyR] (right). It allows efficient lookup in both directions by internally maintaining two synchronized maps. *) -module Make (KeyL : Ordered_type.S) (KeyR : Ordered_type.S) = struct - module M = Map.MakePp (KeyL) +module Make (KeyL : Stdlib.Map.OrderedType) (KeyR : Stdlib.Map.OrderedType) = +struct + module M = Map.Make (KeyL) module M_rev = Map.Make (KeyR) type t = KeyR.t M.t * KeyL.t M_rev.t @@ -40,12 +41,25 @@ module Make (KeyL : Ordered_type.S) (KeyR : Ordered_type.S) = struct | None -> (m, m_rev) | Some k1 -> (M.remove k1 m, M_rev.remove k2 m_rev) + (** Whether the map contains a binding for the given left key. *) + let mem_l k1 (m, _) = M.mem k1 m + + (** Whether the map contains a binding for the given right key. *) + let mem_r k2 (_, m_rev) = M_rev.mem k2 m_rev + (** Find the right key associated with the given left key. *) let find_l k1 (m, _) = M.find_opt k1 m (** Find the left key associated with the given right key. *) let find_r k2 (_, m_rev) = M_rev.find_opt k2 m_rev +end + +(** Equivalent to [Make], but with pretty-printing. *) +module MakePp (KeyL : Ordered_type.S) (KeyR : Ordered_type.S) = struct + include Make (KeyL) (KeyR) (** Pretty-printer for the map. *) - let pp ft (m, _) = M.pp KeyR.pp ft m + let pp ft (m, _) = + let pp_pair = Fmt.pair ~sep:(Fmt.any " -> ") KeyL.pp KeyR.pp in + Fmt.iter_bindings ~sep:Fmt.cut M.iter pp_pair ft m end From eb105ba3a65420a48d3749883254aa2dcaeee6bc Mon Sep 17 00:00:00 2001 From: N1ark Date: Fri, 19 Dec 2025 11:35:30 +0000 Subject: [PATCH 2/9] Use Patricia trees where possible --- dune-project | 2 ++ soteria-rust.opam | 1 + soteria-rust/lib/dune | 13 +++++++------ soteria-rust/lib/tree_borrow.ml | 10 +++++----- soteria.opam | 1 + soteria/lib/bv_values/analyses.ml | 6 +++--- soteria/lib/c_values/analyses.ml | 4 ++-- soteria/lib/dune | 1 + soteria/lib/soteria_std/int.ml | 3 +++ soteria/lib/symex/var.ml | 4 ++-- soteria/lib/symex/var.mli | 4 ++-- 11 files changed, 29 insertions(+), 20 deletions(-) diff --git a/dune-project b/dune-project index 0dfb78a99..151fdb2a6 100644 --- a/dune-project +++ b/dune-project @@ -35,6 +35,7 @@ eio_main simple_smt iter + patricia-tree (ppx_expect (>= 0.17.0)) ppx_deriving @@ -142,6 +143,7 @@ soteria dune-site zarith + patricia-tree ppx_deriving cmdliner fmt diff --git a/soteria-rust.opam b/soteria-rust.opam index 41c43a235..c830e9bc7 100644 --- a/soteria-rust.opam +++ b/soteria-rust.opam @@ -19,6 +19,7 @@ depends: [ "soteria" "dune-site" "zarith" + "patricia-tree" "ppx_deriving" "cmdliner" "fmt" diff --git a/soteria-rust/lib/dune b/soteria-rust/lib/dune index eebd00fae..8ada99f66 100644 --- a/soteria-rust/lib/dune +++ b/soteria-rust/lib/dune @@ -4,18 +4,19 @@ (package soteria-rust) (name soteria_rust_lib) (libraries - soteria + charon cmdliner + dune-site fmt fmt.tty - iter - zarith grace grace.ansi_renderer + iter simple_smt - charon - dune-site - str) + soteria + str + patricia-tree + zarith) (flags :standard -open Soteria.Soteria_std -open Soteria.Bv_values) (preprocess (pps ppx_deriving.std ppx_subliner soteria.ppx)) diff --git a/soteria-rust/lib/tree_borrow.ml b/soteria-rust/lib/tree_borrow.ml index eec010d6d..4a836ccc4 100644 --- a/soteria-rust/lib/tree_borrow.ml +++ b/soteria-rust/lib/tree_borrow.ml @@ -11,10 +11,10 @@ let fresh_tag () = let zero = 0 let pp_tag fmt tag = Fmt.pf fmt "‖%d‖" tag -module TagMap = Map.Make (struct +module TagMap = PatriciaTree.MakeMap (struct type t = tag - let compare = compare + let to_int = Fun.id end) type access = Read | Write @@ -41,7 +41,7 @@ let pp_state fmt = function | Disabled -> Fmt.string fmt "Dis " | UB -> Fmt.string fmt "UB " -let meet st1 st2 = +let[@inline] meet st1 st2 = match (st1, st2) with | UB, _ | _, UB -> UB | Disabled, _ | _, Disabled -> Disabled @@ -52,7 +52,7 @@ let meet st1 st2 = | Reserved _, ReservedIM | ReservedIM, Reserved _ -> failwith "Can't compare Reserved and ReservedIM" -let meet' (p1, st1) (p2, st2) = (p1 || p2, meet st1 st2) +let[@inline] meet' (p1, st1) (p2, st2) = (p1 || p2, meet st1 st2) let transition = let transition st e = @@ -185,4 +185,4 @@ let access accessed e (root : t) st = in if !ub_happened then Result.error `AliasingError else Result.ok st' -let merge = TagMap.merge @@ fun _ -> Option.merge meet' +let merge = TagMap.idempotent_union @@ fun _ -> meet' diff --git a/soteria.opam b/soteria.opam index fb66b5335..7e27abb3b 100644 --- a/soteria.opam +++ b/soteria.opam @@ -19,6 +19,7 @@ depends: [ "eio_main" "simple_smt" "iter" + "patricia-tree" "ppx_expect" {>= "0.17.0"} "ppx_deriving" "fmt" diff --git a/soteria/lib/bv_values/analyses.ml b/soteria/lib/bv_values/analyses.ml index a9139ecbd..5bd7e71a1 100644 --- a/soteria/lib/bv_values/analyses.ml +++ b/soteria/lib/bv_values/analyses.ml @@ -243,8 +243,8 @@ module Interval : S = struct let get n v st = match Var.Map.find_opt v st with Some r -> r | None -> Data.mk n - let st_equal = Var.Map.equal Data.equal - let merge_states = Var.Map.merge (fun _ -> Option.merge Data.union) + let st_equal = Var.Map.reflexive_equal Data.equal + let merge_states = Var.Map.idempotent_inter (fun _ -> Data.union) let pp ft st = Fmt.(iter_bindings Var.Map.iter (pair ~sep:(any " -> ") Var.pp Data.pp)) @@ -503,7 +503,7 @@ end module Equality : S = struct module UnionFind = UnionFind.Make (UnionFind.StoreMap) - module IMap = Map.Make (Int) + module IMap = PatriciaTree.MakeMap (Int) include Reversible.Make_mutable (struct type t = Svalue.t UnionFind.store * Svalue.t UnionFind.rref IMap.t diff --git a/soteria/lib/c_values/analyses.ml b/soteria/lib/c_values/analyses.ml index b95e13447..84581128e 100644 --- a/soteria/lib/c_values/analyses.ml +++ b/soteria/lib/c_values/analyses.ml @@ -123,7 +123,7 @@ module Interval : S = struct end) (** Union of two interval mappings, doing the union of the intervals *) - let st_union = Var.Map.merge (fun _ -> Option.map2 Range.union) + let st_inter = Var.Map.idempotent_inter (fun _ -> Range.union) let get v st = Var.Map.find_opt v st |> Option.value ~default:(None, None) @@ -276,7 +276,7 @@ module Interval : S = struct log (fun m -> m "%a || %a => %a || %a" Svalue.pp v1 Svalue.pp v2 Svalue.pp v1' Svalue.pp v2'); - ((v1' ||@ v2', Var.Set.union vars1 vars2), st_union st1 st2) + ((v1' ||@ v2', Var.Set.union vars1 vars2), st_inter st1 st2) | _ -> ((v, Var.Set.empty), st) (** Simplifies a constraints using the current knowledge base, without diff --git a/soteria/lib/dune b/soteria/lib/dune index edb451d9f..6933b4d94 100644 --- a/soteria/lib/dune +++ b/soteria/lib/dune @@ -11,6 +11,7 @@ hc htmlit iter + patricia-tree printbox-text progress simple_smt diff --git a/soteria/lib/soteria_std/int.ml b/soteria/lib/soteria_std/int.ml index 3af11c79f..70911245f 100644 --- a/soteria/lib/soteria_std/int.ml +++ b/soteria/lib/soteria_std/int.ml @@ -10,3 +10,6 @@ let of_string s = match int_of_string_opt s with | Some i -> Ok i | None -> Error ("Invalid integer: " ^ s) + +(** No-op, used for [PatriciaTree] functors. *) +let to_int = Fun.id diff --git a/soteria/lib/symex/var.ml b/soteria/lib/symex/var.ml index c2d1a4ba1..d306e580f 100644 --- a/soteria/lib/symex/var.ml +++ b/soteria/lib/symex/var.ml @@ -12,9 +12,9 @@ let pp = Fmt.of_to_string to_string let equal = Int.equal let compare = Int.compare -module Set = Set.Make (Int) +module Set = PatriciaTree.MakeSet (Int) module Hashset = Hashset.Hint -module Map = Map.Make (Int) +module Map = PatriciaTree.MakeMap (Int) module Hashtbl = Hashtbl.Make (Int) module Counter (Start_at : sig diff --git a/soteria/lib/symex/var.mli b/soteria/lib/symex/var.mli index 5f73b7e1a..001e63e71 100644 --- a/soteria/lib/symex/var.mli +++ b/soteria/lib/symex/var.mli @@ -38,6 +38,6 @@ module Incr_counter_mut : (_ : sig end module Hashset : Hashset.S with type elt = t -module Set : Set.S with type elt = t +module Set : PatriciaTree.SET with type elt = t module Hashtbl : Hashtbl.S with type key = t -module Map : Map.S with type key = t +module Map : PatriciaTree.MAP with type key = t From bf3c3907eb6c6f71a05e4f206f2c0416d9f00c44 Mon Sep 17 00:00:00 2001 From: N1ark Date: Fri, 19 Dec 2025 11:38:00 +0000 Subject: [PATCH 3/9] Ignore failures in soteria-c `--benchmark` --- soteria-c/scripts/experiments.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/soteria-c/scripts/experiments.py b/soteria-c/scripts/experiments.py index b938108cf..34ebdc492 100755 --- a/soteria-c/scripts/experiments.py +++ b/soteria-c/scripts/experiments.py @@ -249,7 +249,7 @@ def run_soteria_c(self): "Hyperfine is required for benchmarking but was not found in PATH. Install it and try again." ) exit(4) - cmd = f"hyperfine '{cmd}' --warmup 1 --runs 10" + cmd = f"hyperfine '{cmd}' --warmup 1 --runs 10 -i" self.run_command(cmd) def run(self): From c1218b3bb76839c067081a582196ff577e4f3dca Mon Sep 17 00:00:00 2001 From: N1ark Date: Fri, 19 Dec 2025 13:06:13 +0000 Subject: [PATCH 4/9] Update shell.nix --- shell.nix | 1 + 1 file changed, 1 insertion(+) diff --git a/shell.nix b/shell.nix index 4799160fb..34cf67b82 100644 --- a/shell.nix +++ b/shell.nix @@ -135,6 +135,7 @@ let hc htmlit iter + patricia-tree ppxlib ppx_blob ppx_deriving From 80a117823e3bce6a28802b17579e2820ce021198 Mon Sep 17 00:00:00 2001 From: N1ark Date: Fri, 19 Dec 2025 18:10:38 +0000 Subject: [PATCH 5/9] Patricia trees of values --- soteria/lib/bv_values/analyses.ml | 28 ++++++++++++++++------------ soteria/lib/bv_values/svalue.ml | 3 +++ 2 files changed, 19 insertions(+), 12 deletions(-) diff --git a/soteria/lib/bv_values/analyses.ml b/soteria/lib/bv_values/analyses.ml index 5bd7e71a1..106bd18da 100644 --- a/soteria/lib/bv_values/analyses.ml +++ b/soteria/lib/bv_values/analyses.ml @@ -503,12 +503,12 @@ end module Equality : S = struct module UnionFind = UnionFind.Make (UnionFind.StoreMap) - module IMap = PatriciaTree.MakeMap (Int) + module VMap = PatriciaTree.MakeMap (Svalue) include Reversible.Make_mutable (struct - type t = Svalue.t UnionFind.store * Svalue.t UnionFind.rref IMap.t + type t = Svalue.t UnionFind.store * Svalue.t UnionFind.rref VMap.t - let default = (UnionFind.new_store (), IMap.empty) + let default = (UnionFind.new_store (), VMap.empty) end) (* override to account for UnionFind *) @@ -538,11 +538,11 @@ module Equality : S = struct | BvOfFloat _ | FloatOfBv _ -> 4 | _ -> 1 - let get_or_make (v : Svalue.t) ((uf, refs) as st) = - match IMap.find_opt v.tag refs with + let get_or_make v ((uf, refs) as st) = + match VMap.find_opt v refs with | None -> let ref = UnionFind.make uf v in - let refs = IMap.add v.tag ref refs in + let refs = VMap.add v ref refs in (ref, (uf, refs)) | Some ref -> (ref, st) @@ -552,18 +552,18 @@ module Equality : S = struct (fun v1 v2 -> if cost v1 > cost v2 then v2 else v1) v1 v2 - let find_cheaper_opt (v : Svalue.t) (uf, refs) = - Option.bind (IMap.find_opt v.tag refs) @@ fun r -> + let find_cheaper_opt v (uf, refs) = + Option.bind (VMap.find_opt v refs) @@ fun r -> let v_repr = UnionFind.get uf r in if Svalue.equal v v_repr then None else Some v_repr - let known_eq (v1 : Svalue.t) (v2 : Svalue.t) (uf, refs) : bool = - match (IMap.find_opt v1.tag refs, IMap.find_opt v2.tag refs) with + let known_eq v1 v2 (uf, refs) : bool = + match (VMap.find_opt v1 refs, VMap.find_opt v2 refs) with | Some r1, Some r2 -> UnionFind.eq uf r1 r2 | _ -> false - let eval_var (uf, refs) (var : Svalue.t) _ _ = - IMap.find_opt var.tag refs |> Option.fold ~none:var ~some:(UnionFind.get uf) + let eval_var (uf, refs) var _ _ = + VMap.find_opt var refs |> Option.fold ~none:var ~some:(UnionFind.get uf) let simplify (v : Svalue.t) st = let rec simplify ~fuel v = @@ -595,6 +595,10 @@ module Equality : S = struct let v1, st = get_or_make v1 st in let v2, st = get_or_make v2 st in merge v1 v2 st; + (* Here we choose to pass down the equality (rather than simplifying to true), + so that the underlying solver can do trivial SAT checks using these equalities. + This also means this analysis is exempt from implementing [encode], since it + doesn't store anything. *) ((v, Var.Set.empty), st) | _ -> ((v, Var.Set.empty), st) diff --git a/soteria/lib/bv_values/svalue.ml b/soteria/lib/bv_values/svalue.ml index 2d691a3ee..231287aa4 100644 --- a/soteria/lib/bv_values/svalue.ml +++ b/soteria/lib/bv_values/svalue.ml @@ -208,6 +208,9 @@ and t = t_node hash_consed [@@deriving show { with_path = false }, eq, ord] let hash t = t.tag let kind t = t.node.kind +(** Used for [PatriciaTree] *) +let to_int t = t.tag + let iter = let rec aux (f : t -> unit) (sv : t) : unit = f sv; From f83778d2c213b5010c47819ada5bad5a9b6b51ba Mon Sep 17 00:00:00 2001 From: N1ark Date: Sat, 27 Dec 2025 22:33:01 +0100 Subject: [PATCH 6/9] Tentative: add `Patricia_tree` to `pmap` --- soteria-c/lib/csymex.ml | 7 +- soteria-c/lib/state.ml | 1 + soteria-rust/lib/sptr.ml | 3 +- soteria-rust/lib/state.ml | 5 +- soteria/lib/bv_values/svalue.ml | 2 +- soteria/lib/bv_values/typed.mli | 3 + soteria/lib/sym_states/pmap.ml | 172 +++++++++++++++++++++++++++++--- soteria/lib/sym_states/pmap.mli | 137 +++++++++++++++++++++++++ 8 files changed, 309 insertions(+), 21 deletions(-) create mode 100644 soteria/lib/sym_states/pmap.mli diff --git a/soteria-c/lib/csymex.ml b/soteria-c/lib/csymex.ml index d756fc5c3..5991fb7d9 100644 --- a/soteria-c/lib/csymex.ml +++ b/soteria-c/lib/csymex.ml @@ -62,8 +62,11 @@ module With_origin = end) module Freeable = Soteria.Sym_states.Freeable.Make (SYMEX) -module Pmap_direct_access = Soteria.Sym_states.Pmap.Direct_access (SYMEX) -module Pmap = Soteria.Sym_states.Pmap.Make (SYMEX) + +module Pmap_direct_access = + Soteria.Sym_states.Pmap.Direct_access_patricia_tree (SYMEX) + +module Pmap = Soteria.Sym_states.Pmap.Make_patricia_tree (SYMEX) module Tree_block = Soteria.Sym_states.Tree_block.Make (SYMEX) module Concrete_map = Soteria.Sym_states.Pmap.Concrete (SYMEX) module Bi = Soteria.Sym_states.Bi_abd.Make (SYMEX) diff --git a/soteria-c/lib/state.ml b/soteria-c/lib/state.ml index 9af9a415d..fea355f79 100644 --- a/soteria-c/lib/state.ml +++ b/soteria-c/lib/state.ml @@ -21,6 +21,7 @@ module SPmap = Pmap_direct_access (struct let pp = ppa let fresh () = Csymex.nondet Typed.t_loc let simplify = Csymex.simplify + let to_int = Typed.to_int end) type t = (Block.t SPmap.t option, Globs.t) State_intf.Template.t diff --git a/soteria-rust/lib/sptr.ml b/soteria-rust/lib/sptr.ml index 08fff5793..21f14a42e 100644 --- a/soteria-rust/lib/sptr.ml +++ b/soteria-rust/lib/sptr.ml @@ -51,7 +51,8 @@ module DecayMap : DecayMapS = struct let fresh () = failwith "Allocation is not valid for the decay map!" end - module SPmap = Soteria.Sym_states.Pmap.Make (Rustsymex) (StateKey) + module SPmap = + Soteria.Sym_states.Pmap.Make_patricia_tree (Rustsymex) (StateKey) type data = { address : T.sint Typed.t; exposed : bool } [@@deriving show { with_path = false }] diff --git a/soteria-rust/lib/state.ml b/soteria-rust/lib/state.ml index 082c83711..223dc9b0d 100644 --- a/soteria-rust/lib/state.ml +++ b/soteria-rust/lib/state.ml @@ -59,7 +59,10 @@ module StateKey = struct end module Freeable = Soteria.Sym_states.Freeable.Make (DecayMapMonad) -module SPmap = Soteria.Sym_states.Pmap.Direct_access (DecayMapMonad) (StateKey) + +module SPmap = + Soteria.Sym_states.Pmap.Direct_access_patricia_tree (DecayMapMonad) (StateKey) + module Bi = Soteria.Sym_states.Bi_abd.Make (DecayMapMonad) module Tree_block = Rtree_block.Make (Sptr) diff --git a/soteria/lib/bv_values/svalue.ml b/soteria/lib/bv_values/svalue.ml index 18389e796..055798987 100644 --- a/soteria/lib/bv_values/svalue.ml +++ b/soteria/lib/bv_values/svalue.ml @@ -209,7 +209,7 @@ let hash t = t.tag let kind t = t.node.kind (** Used for [PatriciaTree] *) -let to_int t = t.tag +let to_int = hash let iter = let rec aux (f : t -> unit) (sv : t) : unit = diff --git a/soteria/lib/bv_values/typed.mli b/soteria/lib/bv_values/typed.mli index 874139afb..fc579f5d2 100644 --- a/soteria/lib/bv_values/typed.mli +++ b/soteria/lib/bv_values/typed.mli @@ -90,6 +90,9 @@ val equal : ([< any ] as 'a) t -> 'a t -> bool val compare : ([< any ] as 'a) t -> 'a t -> int val hash : [< any ] t -> int +(** Same as [hash] *) +val to_int : [< any ] t -> int + (** Typed constructors *) val sem_eq : 'a t -> 'a t -> sbool t diff --git a/soteria/lib/sym_states/pmap.ml b/soteria/lib/sym_states/pmap.ml index 649980009..55a804098 100644 --- a/soteria/lib/sym_states/pmap.ml +++ b/soteria/lib/sym_states/pmap.ml @@ -16,6 +16,107 @@ module KeyS (Symex : Symex.Base) = struct val subst : (Var.t -> Var.t) -> t -> t val iter_vars : t -> 'a Symex.Value.ty Var.iter_vars end + + module type S_PatriciaTree = sig + include S + + val to_int : t -> int + end +end + +module type MapS = sig + type key + type 'a t + + val empty : 'a t + val is_empty : 'a t -> bool + val add : key -> 'a -> 'a t -> 'a t + val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t + val update : key -> ('a option -> 'a option) -> 'a t -> 'a t + val mem : key -> 'a t -> bool + val find_opt : key -> 'a t -> 'a option + val iter : (key -> 'a -> unit) -> 'a t -> unit + val to_seq : 'a t -> (key * 'a) Seq.t + val bindings : 'a t -> (key * 'a) list +end + +module S (Symex : Symex.Base) = struct + module type S = sig + module M : MapS + + type 'a t = 'a M.t + type 'a serialized = (M.key * 'a) list + + val pp : + ?ignore:(M.key * 'a -> bool) -> + (Format.formatter -> 'a -> unit) -> + Format.formatter -> + 'a t -> + unit + + val pp_serialized : + (Format.formatter -> 'a -> unit) -> + Format.formatter -> + 'a serialized -> + unit + + val serialize : ('a -> 'b) -> 'a t -> (M.key * 'b) list + + val subst_serialized : + ((Var.t -> Var.t) -> 'a -> 'b) -> + (Var.t -> Var.t) -> + 'a serialized -> + 'b serialized + + val iter_vars_serialized : + ('a -> (Var.t * 'b Symex.Value.ty -> unit) -> unit) -> + 'a serialized -> + (Var.t * 'b Symex.Value.ty -> unit) -> + unit + + val of_opt : 'a t option -> 'a t + val to_opt : 'a t -> 'a t option + + val alloc : + new_codom:'a -> + 'a t option -> + (M.key * 'a t option, 'err, 'fix list) Symex.Result.t + + val allocs : + fn:('b -> M.key -> ('a * 'k) Symex.t) -> + els:'b list -> + 'a t option -> + ('k list * 'a t option, 'err, 'fix list) Symex.Result.t + + val wrap : + ('a option -> ('b * 'a option, 'err, 'fix) Symex.Result.t) -> + M.key -> + 'a t option -> + ('b * 'a t option, 'err, 'fix serialized) Symex.Result.t + + val fold : + ('acc -> M.key * 'a -> ('acc, 'err, 'fix serialized) Symex.Result.t) -> + 'acc -> + 'a t option -> + ('acc, 'err, 'fix serialized) Symex.Result.t + + val produce : + ('inner_serialized -> 'inner_st option -> 'inner_st option Symex.t) -> + 'inner_serialized serialized -> + 'inner_st t option -> + 'inner_st t option Symex.t + + val consume : + ('inner_serialized -> + 'inner_st option -> + ( 'inner_st option, + ([> Symex.lfail ] as 'a), + 'inner_serialized ) + Symex.Result.t) -> + 'inner_serialized serialized -> + 'inner_st t option -> + ('inner_st t option, 'a, 'inner_serialized serialized) Symex.Result.t + end end module Mk_concrete_key (Symex : Symex.Base) (Key : Soteria_std.Ordered_type.S) : @@ -30,16 +131,27 @@ module Mk_concrete_key (Symex : Symex.Base) (Key : Soteria_std.Ordered_type.S) : let iter_vars _ = fun _ -> () end +module PatriciaTreeMakeMap (K : sig + type t + + val to_int : t -> int +end) : MapS with type key = K.t = struct + include PatriciaTree.MakeMap (K) + + let bindings m = to_seq m |> List.of_seq +end + module Build_from_find_opt_sym (Symex : Symex.Base) (Key : KeyS(Symex).S) + (Map : MapS with type key = Key.t) (Find_opt_sym : sig - val f : Key.t -> 'a Stdlib.Map.Make(Key).t -> (Key.t * 'a option) Symex.t + val f : Key.t -> 'a Map.t -> (Key.t * 'a option) Symex.t end) = struct open Symex.Syntax open Symex - module M = Stdlib.Map.Make (Key) + module M = Map type 'a t = 'a M.t type 'a serialized = (Key.t * 'a) list @@ -151,12 +263,15 @@ struct Result.fold_seq (M.to_seq st) ~init ~f end -module Make (Symex : Symex.Base) (Key : KeyS(Symex).S) = struct +module Build_base + (Symex : Symex.Base) + (Key : KeyS(Symex).S) + (M : MapS with type key = Key.t) = +struct open Symex.Syntax - module M' = Stdlib.Map.Make (Key) (* Symbolic process that under-approximates Map.find_opt *) - let find_opt_sym (key : Key.t) (st : 'a M'.t) = + let find_opt_sym (key : Key.t) (st : 'a M.t) = let rec find_bindings = function | [] -> Symex.return (key, None) | (k, v) :: tl -> @@ -164,22 +279,35 @@ module Make (Symex : Symex.Base) (Key : KeyS(Symex).S) = struct else find_bindings tl (* TODO: Investigate: this is not a tailcall, because if%sat is not an if. *) in - match M'.find_opt key st with + match M.find_opt key st with | Some v -> Symex.return (key, Some v) - | None -> find_bindings (M'.bindings st) + | None -> find_bindings (M.bindings st) include - Build_from_find_opt_sym (Symex) (Key) + Build_from_find_opt_sym (Symex) (Key) (M) (struct let f = find_opt_sym end) end -module Direct_access (Symex : Symex.Base) (Key : KeyS(Symex).S) = struct +module Make (Symex : Symex.Base) (Key : KeyS(Symex).S) = + Build_base (Symex) (Key) (Stdlib.Map.Make (Key)) + +module Make_patricia_tree + (Symex : Symex.Base) + (Key : KeyS(Symex).S_PatriciaTree) = + Build_base (Symex) (Key) (PatriciaTreeMakeMap (Key)) + +(** Sound to use when the keys of the map may depend on symbolic variables *) + +module Build_direct_access + (Symex : Symex.Base) + (Key : KeyS(Symex).S) + (M : MapS with type key = Key.t) = +struct open Symex.Syntax - module M' = Stdlib.Map.Make (Key) - let find_opt_sym (key : Key.t) (st : 'a M'.t) = + let find_opt_sym (key : Key.t) (st : 'a M.t) = let rec find_bindings = function | [] -> Symex.vanish () | (k, v) :: tl -> @@ -187,22 +315,34 @@ module Direct_access (Symex : Symex.Base) (Key : KeyS(Symex).S) = struct else find_bindings tl in let* key = Key.simplify key in - match M'.find_opt key st with + match M.find_opt key st with | Some v -> Symex.return (key, Some v) | None -> let not_in_map = - M'.to_seq st |> Seq.map fst |> List.of_seq |> Key.distinct + M.to_seq st |> Seq.map fst |> List.of_seq |> Key.distinct in if%sat1 not_in_map then Symex.return (key, None) - else find_bindings (M'.bindings st) + else find_bindings (M.bindings st) include - Build_from_find_opt_sym (Symex) (Key) + Build_from_find_opt_sym (Symex) (Key) (M) (struct let f = find_opt_sym end) end +module Direct_access (Symex : Symex.Base) (Key : KeyS(Symex).S) = struct + include Build_direct_access (Symex) (Key) (Stdlib.Map.Make (Key)) +end + +module Direct_access_patricia_tree + (Symex : Symex.Base) + (Key : KeyS(Symex).S_PatriciaTree) = +struct + module M' = PatriciaTreeMakeMap (Key) + include Build_direct_access (Symex) (Key) (M') +end + (** Only sound to use if the keys of the map are invariant under interpretations of the symbolic variables *) module Concrete (Symex : Symex.Base) (Key : Soteria_std.Ordered_type.S) = struct @@ -213,7 +353,7 @@ module Concrete (Symex : Symex.Base) (Key : Soteria_std.Ordered_type.S) = struct Symex.return (key, M'.find_opt key st) include - Build_from_find_opt_sym (Symex) (Key) + Build_from_find_opt_sym (Symex) (Key) (M') (struct let f = find_opt_sym end) diff --git a/soteria/lib/sym_states/pmap.mli b/soteria/lib/sym_states/pmap.mli new file mode 100644 index 000000000..d19e21b0f --- /dev/null +++ b/soteria/lib/sym_states/pmap.mli @@ -0,0 +1,137 @@ +open Symex + +module KeyS (Symex : Symex.Base) : sig + module type S = sig + type t + + include Stdlib.Map.OrderedType with type t := t + + type sbool_v := Symex.Value.sbool Symex.Value.t + + val pp : Format.formatter -> t -> unit + val sem_eq : t -> t -> sbool_v + val fresh : unit -> t Symex.t + val simplify : t -> t Symex.t + val distinct : t list -> sbool_v + val subst : (Var.t -> Var.t) -> t -> t + val iter_vars : t -> 'a Symex.Value.ty Var.iter_vars + end + + module type S_PatriciaTree = sig + include S + + val to_int : t -> int + end +end + +module type MapS = sig + type key + type 'a t + + val empty : 'a t + val is_empty : 'a t -> bool + val add : key -> 'a -> 'a t -> 'a t + val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t + val update : key -> ('a option -> 'a option) -> 'a t -> 'a t + val mem : key -> 'a t -> bool + val find_opt : key -> 'a t -> 'a option + val iter : (key -> 'a -> unit) -> 'a t -> unit + val to_seq : 'a t -> (key * 'a) Seq.t + val bindings : 'a t -> (key * 'a) list +end + +module S (Symex : Symex.Base) : sig + module type S = sig + module M : MapS + + type 'a t = 'a M.t + type 'a serialized = (M.key * 'a) list + + val pp : + ?ignore:(M.key * 'a -> bool) -> + (Format.formatter -> 'a -> unit) -> + Format.formatter -> + 'a t -> + unit + + val pp_serialized : + (Format.formatter -> 'a -> unit) -> + Format.formatter -> + 'a serialized -> + unit + + val serialize : ('a -> 'b) -> 'a t -> (M.key * 'b) list + + val subst_serialized : + ((Var.t -> Var.t) -> 'a -> 'b) -> + (Var.t -> Var.t) -> + 'a serialized -> + 'b serialized + + val iter_vars_serialized : + ('a -> (Var.t * 'b Symex.Value.ty -> unit) -> unit) -> + 'a serialized -> + (Var.t * 'b Symex.Value.ty -> unit) -> + unit + + val of_opt : 'a t option -> 'a t + val to_opt : 'a t -> 'a t option + + val alloc : + new_codom:'a -> + 'a t option -> + (M.key * 'a t option, 'err, 'fix list) Symex.Result.t + + val allocs : + fn:('b -> M.key -> ('a * 'k) Symex.t) -> + els:'b list -> + 'a t option -> + ('k list * 'a t option, 'err, 'fix list) Symex.Result.t + + val wrap : + ('a option -> ('b * 'a option, 'err, 'fix) Symex.Result.t) -> + M.key -> + 'a t option -> + ('b * 'a t option, 'err, 'fix serialized) Symex.Result.t + + val fold : + ('acc -> M.key * 'a -> ('acc, 'err, 'fix serialized) Symex.Result.t) -> + 'acc -> + 'a t option -> + ('acc, 'err, 'fix serialized) Symex.Result.t + + val produce : + ('inner_serialized -> 'inner_st option -> 'inner_st option Symex.t) -> + 'inner_serialized serialized -> + 'inner_st t option -> + 'inner_st t option Symex.t + + val consume : + ('inner_serialized -> + 'inner_st option -> + ( 'inner_st option, + ([> Symex.lfail ] as 'a), + 'inner_serialized ) + Symex.Result.t) -> + 'inner_serialized serialized -> + 'inner_st t option -> + ('inner_st t option, 'a, 'inner_serialized serialized) Symex.Result.t + end +end + +module Make (Symex : Symex.Base) (Key : KeyS(Symex).S) : + S(Symex).S with type M.key = Key.t + +module Make_patricia_tree + (Symex : Symex.Base) + (Key : KeyS(Symex).S_PatriciaTree) : S(Symex).S with type M.key = Key.t + +module Direct_access (Symex : Symex.Base) (Key : KeyS(Symex).S) : + S(Symex).S with type M.key = Key.t + +module Direct_access_patricia_tree + (Symex : Symex.Base) + (Key : KeyS(Symex).S_PatriciaTree) : S(Symex).S with type M.key = Key.t + +module Concrete (Symex : Symex.Base) (Key : Soteria_std.Ordered_type.S) : + S(Symex).S with type M.key = Key.t From 4cc1513af64abab015d750030896ba56c928599f Mon Sep 17 00:00:00 2001 From: N1ark Date: Sat, 27 Dec 2025 23:16:15 +0100 Subject: [PATCH 7/9] `Typo_in_module_name` :P --- soteria/lib/sym_states/pmap.ml | 6 +++--- soteria/lib/sym_states/pmap.mli | 6 +++--- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/soteria/lib/sym_states/pmap.ml b/soteria/lib/sym_states/pmap.ml index 55a804098..327d852ed 100644 --- a/soteria/lib/sym_states/pmap.ml +++ b/soteria/lib/sym_states/pmap.ml @@ -17,7 +17,7 @@ module KeyS (Symex : Symex.Base) = struct val iter_vars : t -> 'a Symex.Value.ty Var.iter_vars end - module type S_PatriciaTree = sig + module type S_patricia_tree = sig include S val to_int : t -> int @@ -295,7 +295,7 @@ module Make (Symex : Symex.Base) (Key : KeyS(Symex).S) = module Make_patricia_tree (Symex : Symex.Base) - (Key : KeyS(Symex).S_PatriciaTree) = + (Key : KeyS(Symex).S_patricia_tree) = Build_base (Symex) (Key) (PatriciaTreeMakeMap (Key)) (** Sound to use when the keys of the map may depend on symbolic variables *) @@ -337,7 +337,7 @@ end module Direct_access_patricia_tree (Symex : Symex.Base) - (Key : KeyS(Symex).S_PatriciaTree) = + (Key : KeyS(Symex).S_patricia_tree) = struct module M' = PatriciaTreeMakeMap (Key) include Build_direct_access (Symex) (Key) (M') diff --git a/soteria/lib/sym_states/pmap.mli b/soteria/lib/sym_states/pmap.mli index d19e21b0f..89564ecae 100644 --- a/soteria/lib/sym_states/pmap.mli +++ b/soteria/lib/sym_states/pmap.mli @@ -17,7 +17,7 @@ module KeyS (Symex : Symex.Base) : sig val iter_vars : t -> 'a Symex.Value.ty Var.iter_vars end - module type S_PatriciaTree = sig + module type S_patricia_tree = sig include S val to_int : t -> int @@ -124,14 +124,14 @@ module Make (Symex : Symex.Base) (Key : KeyS(Symex).S) : module Make_patricia_tree (Symex : Symex.Base) - (Key : KeyS(Symex).S_PatriciaTree) : S(Symex).S with type M.key = Key.t + (Key : KeyS(Symex).S_patricia_tree) : S(Symex).S with type M.key = Key.t module Direct_access (Symex : Symex.Base) (Key : KeyS(Symex).S) : S(Symex).S with type M.key = Key.t module Direct_access_patricia_tree (Symex : Symex.Base) - (Key : KeyS(Symex).S_PatriciaTree) : S(Symex).S with type M.key = Key.t + (Key : KeyS(Symex).S_patricia_tree) : S(Symex).S with type M.key = Key.t module Concrete (Symex : Symex.Base) (Key : Soteria_std.Ordered_type.S) : S(Symex).S with type M.key = Key.t From 10d7834118600741b6b10719f092733913500db6 Mon Sep 17 00:00:00 2001 From: N1ark Date: Mon, 29 Dec 2025 19:11:47 +0100 Subject: [PATCH 8/9] drive-by: Nicer frontend error message --- soteria-rust/lib/config.ml | 4 +++- soteria-rust/lib/frontend.ml | 13 +++++++++---- 2 files changed, 12 insertions(+), 5 deletions(-) diff --git a/soteria-rust/lib/config.ml b/soteria-rust/lib/config.ml index c6ecd36e5..2445c542c 100644 --- a/soteria-rust/lib/config.ml +++ b/soteria-rust/lib/config.ml @@ -2,7 +2,9 @@ We ignore the warning here. *) [@@@warning "-unused-open"] -type frontend = Charon | Obol [@@deriving subliner_enum] +type frontend = Charon | Obol +[@@deriving subliner_enum, show { with_path = false }] + type provenance = Strict | Permissive [@@deriving subliner_enum] type t = { diff --git a/soteria-rust/lib/frontend.ml b/soteria-rust/lib/frontend.ml index 9ddfc4218..ec3c565e6 100644 --- a/soteria-rust/lib/frontend.ml +++ b/soteria-rust/lib/frontend.ml @@ -427,13 +427,18 @@ let parse_ullbc ~mode ~plugin ?input ~output ~pwd () = err; Cleaner.touched output); let crate = - try + match output |> Yojson.Basic.from_file |> Charon.UllbcOfJson.crate_of_json with - | Sys_error _ -> frontend_err "File doesn't exist" - | _ -> frontend_err "Failed to parse ULLBC" + | Ok crate -> crate + | Error _ -> + Fmt.kstr frontend_err + "Failed to parse ULLBC. Do you have the right version of %a \ + installed?" + Config.pp_frontend !Config.current.frontend + | exception Sys_error _ -> frontend_err "File doesn't exist" + | exception _ -> frontend_err "Unexpected error" in - let crate = Result.get_or_raise frontend_err crate in if !Config.current.output_crate then ( (* save pretty-printed crate to local file *) let crate_file = Printf.sprintf "%s.crate" output in From d5cf8e01e2a1f1247efd9b7577587ef28b6e5ddc Mon Sep 17 00:00:00 2001 From: N1ark Date: Mon, 29 Dec 2025 19:11:57 +0100 Subject: [PATCH 9/9] Unexpose some `PMap` stuff --- soteria-c/lib/globs.ml | 32 ++++++++----------- soteria-c/lib/state.ml | 2 +- soteria-rust/lib/sptr.ml | 5 +-- soteria-rust/lib/state.ml | 1 + soteria/lib/bv_values/analyses.ml | 7 +++- soteria/lib/bv_values/svalue.ml | 4 +-- soteria/lib/bv_values/typed.mli | 4 +-- soteria/lib/sym_states/pmap.ml | 31 ++++++++++++------ soteria/lib/sym_states/pmap.mli | 53 ++++++++++++------------------- 9 files changed, 69 insertions(+), 70 deletions(-) diff --git a/soteria-c/lib/globs.ml b/soteria-c/lib/globs.ml index b1ba4b908..fb53a8594 100644 --- a/soteria-c/lib/globs.ml +++ b/soteria-c/lib/globs.ml @@ -42,24 +42,22 @@ let get sym st = It'd be nice to enforce this modularly, but right now we do it as a wrapper. Unless one has hundreds of globals, the cost is negligeable, but still. *) let open Csymex.Syntax in - let existed = Option.fold ~none:false ~some:(Sym_map.M.mem sym) st in + let existed = Option.fold ~none:false ~some:(Sym_map.syntactic_mem sym) st in let* res = (Sym_map.wrap GlobFn.load) sym st in let loc, st = Soteria.Symex.Compo_res.get_ok res in let+ () = if existed then (* We haven't created a new location *) return () else (* We learn that the new location is distinct from all other global locations *) - let to_assume = - Sym_map.M.to_seq (Option.value ~default:Sym_map.M.empty st) - |> Seq.filter_map (fun (k, v) -> - let open Typed.Infix in - if Cerb_frontend.Symbol.equal_sym k sym then None - else - let neq = Typed.not (v ==@ loc) in - Some neq) - |> List.of_seq - in - assume to_assume + Sym_map.syntactic_bindings (Option.value ~default:Sym_map.empty st) + |> Seq.filter_map (fun (k, v) -> + let open Typed.Infix in + if Cerb_frontend.Symbol.equal_sym k sym then None + else + let neq = Typed.not (v ==@ loc) in + Some neq) + |> List.of_seq + |> assume in (loc, st) @@ -69,14 +67,12 @@ let produce serialized st = let+ () = (* Bit heavy-handed but we just massively assume the well-formedness *) let to_assume = - Sym_map.M.to_seq (Option.value ~default:Sym_map.M.empty st') - |> Seq.self_cross_product - |> Seq.map (fun ((_, loca), (_, locb)) -> - let open Typed.Infix in - Typed.not (loca ==@ locb)) + Sym_map.syntactic_bindings (Option.value ~default:Sym_map.empty st') + |> Seq.map snd |> List.of_seq + |> Typed.distinct in - assume to_assume + assume [ to_assume ] in st' diff --git a/soteria-c/lib/state.ml b/soteria-c/lib/state.ml index fea355f79..7ecfbfe08 100644 --- a/soteria-c/lib/state.ml +++ b/soteria-c/lib/state.ml @@ -21,7 +21,7 @@ module SPmap = Pmap_direct_access (struct let pp = ppa let fresh () = Csymex.nondet Typed.t_loc let simplify = Csymex.simplify - let to_int = Typed.to_int + let to_int = unique_tag end) type t = (Block.t SPmap.t option, Globs.t) State_intf.Template.t diff --git a/soteria-rust/lib/sptr.ml b/soteria-rust/lib/sptr.ml index 21f14a42e..6e2a3f573 100644 --- a/soteria-rust/lib/sptr.ml +++ b/soteria-rust/lib/sptr.ml @@ -46,6 +46,7 @@ module DecayMap : DecayMapS = struct type t = T.sloc Typed.t + let to_int = unique_tag let pp = ppa let simplify = Rustsymex.simplify let fresh () = failwith "Allocation is not valid for the decay map!" @@ -96,13 +97,13 @@ module DecayMap : DecayMapS = struct See https://doc.rust-lang.org/nightly/std/ptr/fn.with_exposed_provenance.html *) let usize_ty = Typed.t_usize () in - let bindings = SPmap.M.bindings (SPmap.of_opt st) in + let bindings = SPmap.syntactic_bindings (SPmap.of_opt st) in let binding = Typed.iter_vars loc_int |> Iter.filter (fun (_, ty) -> Typed.equal_ty usize_ty ty) |> Iter.filter_map (fun (var, ty) -> let v = Typed.mk_var var ty in - List.find_opt + Seq.find (fun (_, { address; exposed }) -> exposed && Typed.equal v address) bindings) diff --git a/soteria-rust/lib/state.ml b/soteria-rust/lib/state.ml index 223dc9b0d..f79634366 100644 --- a/soteria-rust/lib/state.ml +++ b/soteria-rust/lib/state.ml @@ -44,6 +44,7 @@ module StateKey = struct type t = T.sloc Typed.t let pp = ppa + let to_int = unique_tag let i = ref 0 let fresh_rsym () = diff --git a/soteria/lib/bv_values/analyses.ml b/soteria/lib/bv_values/analyses.ml index 106bd18da..83eec600e 100644 --- a/soteria/lib/bv_values/analyses.ml +++ b/soteria/lib/bv_values/analyses.ml @@ -503,7 +503,12 @@ end module Equality : S = struct module UnionFind = UnionFind.Make (UnionFind.StoreMap) - module VMap = PatriciaTree.MakeMap (Svalue) + + module VMap = PatriciaTree.MakeMap (struct + type t = Svalue.t + + let to_int = Svalue.unique_tag + end) include Reversible.Make_mutable (struct type t = Svalue.t UnionFind.store * Svalue.t UnionFind.rref VMap.t diff --git a/soteria/lib/bv_values/svalue.ml b/soteria/lib/bv_values/svalue.ml index 055798987..4ca99b63e 100644 --- a/soteria/lib/bv_values/svalue.ml +++ b/soteria/lib/bv_values/svalue.ml @@ -207,9 +207,7 @@ and t = t_node hash_consed [@@deriving show { with_path = false }, eq, ord] let hash t = t.tag let kind t = t.node.kind - -(** Used for [PatriciaTree] *) -let to_int = hash +let unique_tag t = t.tag let iter = let rec aux (f : t -> unit) (sv : t) : unit = diff --git a/soteria/lib/bv_values/typed.mli b/soteria/lib/bv_values/typed.mli index fc579f5d2..d6c478995 100644 --- a/soteria/lib/bv_values/typed.mli +++ b/soteria/lib/bv_values/typed.mli @@ -89,9 +89,7 @@ val ppa : Format.formatter -> 'a t -> unit val equal : ([< any ] as 'a) t -> 'a t -> bool val compare : ([< any ] as 'a) t -> 'a t -> int val hash : [< any ] t -> int - -(** Same as [hash] *) -val to_int : [< any ] t -> int +val unique_tag : [< any ] t -> int (** Typed constructors *) diff --git a/soteria/lib/sym_states/pmap.ml b/soteria/lib/sym_states/pmap.ml index 327d852ed..9b40c997d 100644 --- a/soteria/lib/sym_states/pmap.ml +++ b/soteria/lib/sym_states/pmap.ml @@ -40,15 +40,22 @@ module type MapS = sig val bindings : 'a t -> (key * 'a) list end -module S (Symex : Symex.Base) = struct +module S + (Symex : Symex.Base) + (Key : sig + type t + end) = +struct module type S = sig - module M : MapS + type 'a t + type 'a serialized = (Key.t * 'a) list - type 'a t = 'a M.t - type 'a serialized = (M.key * 'a) list + val empty : 'a t + val syntactic_bindings : 'a t -> (Key.t * 'a) Seq.t + val syntactic_mem : Key.t -> 'a t -> bool val pp : - ?ignore:(M.key * 'a -> bool) -> + ?ignore:(Key.t * 'a -> bool) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> @@ -60,7 +67,7 @@ module S (Symex : Symex.Base) = struct 'a serialized -> unit - val serialize : ('a -> 'b) -> 'a t -> (M.key * 'b) list + val serialize : ('a -> 'b) -> 'a t -> (Key.t * 'b) list val subst_serialized : ((Var.t -> Var.t) -> 'a -> 'b) -> @@ -80,22 +87,22 @@ module S (Symex : Symex.Base) = struct val alloc : new_codom:'a -> 'a t option -> - (M.key * 'a t option, 'err, 'fix list) Symex.Result.t + (Key.t * 'a t option, 'err, 'fix list) Symex.Result.t val allocs : - fn:('b -> M.key -> ('a * 'k) Symex.t) -> + fn:('b -> Key.t -> ('a * 'k) Symex.t) -> els:'b list -> 'a t option -> ('k list * 'a t option, 'err, 'fix list) Symex.Result.t val wrap : ('a option -> ('b * 'a option, 'err, 'fix) Symex.Result.t) -> - M.key -> + Key.t -> 'a t option -> ('b * 'a t option, 'err, 'fix serialized) Symex.Result.t val fold : - ('acc -> M.key * 'a -> ('acc, 'err, 'fix serialized) Symex.Result.t) -> + ('acc -> Key.t * 'a -> ('acc, 'err, 'fix serialized) Symex.Result.t) -> 'acc -> 'a t option -> ('acc, 'err, 'fix serialized) Symex.Result.t @@ -156,6 +163,10 @@ struct type 'a t = 'a M.t type 'a serialized = (Key.t * 'a) list + let empty = M.empty + let syntactic_bindings = M.to_seq + let syntactic_mem = M.mem + let lift_fix_s ~key res = let+? fix = res in [ (key, fix) ] diff --git a/soteria/lib/sym_states/pmap.mli b/soteria/lib/sym_states/pmap.mli index 89564ecae..bd6576532 100644 --- a/soteria/lib/sym_states/pmap.mli +++ b/soteria/lib/sym_states/pmap.mli @@ -24,31 +24,21 @@ module KeyS (Symex : Symex.Base) : sig end end -module type MapS = sig - type key - type 'a t - - val empty : 'a t - val is_empty : 'a t -> bool - val add : key -> 'a -> 'a t -> 'a t - val add_seq : (key * 'a) Seq.t -> 'a t -> 'a t - val update : key -> ('a option -> 'a option) -> 'a t -> 'a t - val mem : key -> 'a t -> bool - val find_opt : key -> 'a t -> 'a option - val iter : (key -> 'a -> unit) -> 'a t -> unit - val to_seq : 'a t -> (key * 'a) Seq.t - val bindings : 'a t -> (key * 'a) list -end - -module S (Symex : Symex.Base) : sig +module S + (Symex : Symex.Base) + (Key : sig + type t + end) : sig module type S = sig - module M : MapS + type 'a t + type 'a serialized = (Key.t * 'a) list - type 'a t = 'a M.t - type 'a serialized = (M.key * 'a) list + val empty : 'a t + val syntactic_bindings : 'a t -> (Key.t * 'a) Seq.t + val syntactic_mem : Key.t -> 'a t -> bool val pp : - ?ignore:(M.key * 'a -> bool) -> + ?ignore:(Key.t * 'a -> bool) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> @@ -60,7 +50,7 @@ module S (Symex : Symex.Base) : sig 'a serialized -> unit - val serialize : ('a -> 'b) -> 'a t -> (M.key * 'b) list + val serialize : ('a -> 'b) -> 'a t -> (Key.t * 'b) list val subst_serialized : ((Var.t -> Var.t) -> 'a -> 'b) -> @@ -80,22 +70,22 @@ module S (Symex : Symex.Base) : sig val alloc : new_codom:'a -> 'a t option -> - (M.key * 'a t option, 'err, 'fix list) Symex.Result.t + (Key.t * 'a t option, 'err, 'fix list) Symex.Result.t val allocs : - fn:('b -> M.key -> ('a * 'k) Symex.t) -> + fn:('b -> Key.t -> ('a * 'k) Symex.t) -> els:'b list -> 'a t option -> ('k list * 'a t option, 'err, 'fix list) Symex.Result.t val wrap : ('a option -> ('b * 'a option, 'err, 'fix) Symex.Result.t) -> - M.key -> + Key.t -> 'a t option -> ('b * 'a t option, 'err, 'fix serialized) Symex.Result.t val fold : - ('acc -> M.key * 'a -> ('acc, 'err, 'fix serialized) Symex.Result.t) -> + ('acc -> Key.t * 'a -> ('acc, 'err, 'fix serialized) Symex.Result.t) -> 'acc -> 'a t option -> ('acc, 'err, 'fix serialized) Symex.Result.t @@ -119,19 +109,18 @@ module S (Symex : Symex.Base) : sig end end -module Make (Symex : Symex.Base) (Key : KeyS(Symex).S) : - S(Symex).S with type M.key = Key.t +module Make (Symex : Symex.Base) (Key : KeyS(Symex).S) : S(Symex)(Key).S module Make_patricia_tree (Symex : Symex.Base) - (Key : KeyS(Symex).S_patricia_tree) : S(Symex).S with type M.key = Key.t + (Key : KeyS(Symex).S_patricia_tree) : S(Symex)(Key).S module Direct_access (Symex : Symex.Base) (Key : KeyS(Symex).S) : - S(Symex).S with type M.key = Key.t + S(Symex)(Key).S module Direct_access_patricia_tree (Symex : Symex.Base) - (Key : KeyS(Symex).S_patricia_tree) : S(Symex).S with type M.key = Key.t + (Key : KeyS(Symex).S_patricia_tree) : S(Symex)(Key).S module Concrete (Symex : Symex.Base) (Key : Soteria_std.Ordered_type.S) : - S(Symex).S with type M.key = Key.t + S(Symex)(Key).S