diff options
author | Son Ho | 2022-01-15 21:15:20 +0100 |
---|---|---|
committer | Son Ho | 2022-01-15 21:15:20 +0100 |
commit | 231c65c04c511db3c8f7f68cd5d37cdeeedfe809 (patch) | |
tree | fbf656ae97d6a00c21f344c6de9fc50e444d9089 | |
parent | 9711789ae50ddcf2d2f4181044ba4f5eeb139ec8 (diff) |
Use the new collections
-rw-r--r-- | src/Contexts.ml | 4 | ||||
-rw-r--r-- | src/Identifiers.ml | 124 | ||||
-rw-r--r-- | src/InterpreterBorrows.ml | 6 | ||||
-rw-r--r-- | src/InterpreterBorrowsCore.ml | 6 | ||||
-rw-r--r-- | src/InterpreterProjectors.ml | 14 | ||||
-rw-r--r-- | src/InterpreterStatements.ml | 2 | ||||
-rw-r--r-- | src/InterpreterUtils.ml | 4 | ||||
-rw-r--r-- | src/Invariants.ml | 17 | ||||
-rw-r--r-- | src/Print.ml | 10 | ||||
-rw-r--r-- | src/TypesUtils.ml | 6 | ||||
-rw-r--r-- | src/Values.ml | 10 |
11 files changed, 65 insertions, 138 deletions
diff --git a/src/Contexts.ml b/src/Contexts.ml index 8a9c4857..1a9dcfc8 100644 --- a/src/Contexts.ml +++ b/src/Contexts.ml @@ -137,7 +137,7 @@ let config_of_partial (mode : interpreter_mode) (config : partial_config) : } type type_context = { - type_defs_groups : M.types_decl_group TypeDefId.map_t; + type_defs_groups : M.types_decl_group TypeDefId.Map.t; type_defs : type_def list; } [@@deriving show] @@ -147,7 +147,7 @@ type eval_ctx = { fun_context : fun_def list; type_vars : type_var list; env : env; - ended_regions : RegionId.set_t; + ended_regions : RegionId.Set.t; } [@@deriving show] (** Evaluation context *) diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 4ec5aab7..fd07b7b6 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -1,4 +1,4 @@ -open Collections +module C = Collections (** Signature for a module describing an identifier. @@ -12,19 +12,18 @@ module type Id = sig type generator (** Id generator - simply a counter *) - type set_t - - type +!'a map_t - val zero : id val generator_zero : generator val fresh_stateful_generator : unit -> generator ref * (unit -> id) - (* TODO: this is stateful! - but we may want to be able to duplicate contexts... *) + (* TODO: this should be stateful! - but we may want to be able to duplicate + contexts... + Maybe we could have a `fresh` and a `global_fresh` + TODO: change the order of the returned types + *) val fresh : generator -> id * generator - (* TODO: change the order of the returned types *) val to_string : id -> string @@ -32,6 +31,8 @@ module type Id = sig val show_id : id -> string + val id_of_json : Yojson.Basic.t -> (id, string) result + val pp_generator : Format.formatter -> generator -> unit val show_generator : generator -> string @@ -53,38 +54,16 @@ module type Id = sig val mapi : (id -> 'a -> 'b) -> 'a list -> 'b list val mapi_from1 : (id -> 'a -> 'b) -> 'a list -> 'b list - (** Same as [mapi], but where the indices start with 1 *) - - val pp_set_t : Format.formatter -> set_t -> unit - - val show_set_t : set_t -> string - - val pp_map_t : - (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a map_t -> unit - - val show_map_t : ('a -> string) -> 'a map_t -> string - - module Ord : Map.OrderedType with type t = id - - module Set : Set.S with type elt = id with type t = set_t - - val set_to_string : string option -> Set.t -> string - (** Convert a set to a string. - - Takes an indentation as parameter, in case you want to insert a breakline - for every binding. + (** Same as [mapi], but where the indices start with 1. + + TODO: generalize to `map_from_i` *) - module Map : Map.S with type key = id with type 'a t = 'a map_t + module Ord : C.OrderedType with type t = id - val map_to_string : string option -> ('a -> string) -> 'a map_t -> string - (** Convert a map to a string. - - Takes an indentation as parameter, in case you want to insert a breakline - for every binding. - *) + module Set : C.Set with type elt = id - val id_of_json : Yojson.Basic.t -> (id, string) result + module Map : C.Map with type key = id end (** Generative functor for identifiers. @@ -124,6 +103,12 @@ module IdGen () : Id = struct let of_int x = x + let id_of_json js = + (* TODO: check boundaries ? *) + match js with + | `Int i -> Ok i + | _ -> Error ("id_of_json: failed on " ^ Yojson.Basic.show js) + let nth v id = List.nth v id let nth_opt v id = List.nth_opt v id @@ -146,73 +131,16 @@ module IdGen () : Id = struct type t = id let compare = compare - end - - module Set = Set.Make (Ord) - module Map = Map.Make (Ord) - type set_t = Set.t + let to_string = to_string - type +!'a map_t = 'a Map.t + let pp_t = pp_id - let show_set_t s = - let ids = Set.fold (fun id s -> to_string id :: s) s [] in - let ids = List.rev ids in - "{" ^ String.concat "," ids ^ "}" - - let pp_set_t fmt s = - let pp_string = Format.pp_print_string fmt in - pp_string "{"; - Set.iter (fun id -> pp_string (to_string id ^ ",")) s; - pp_string "}" - - let show_map_t show_a s = - let ids = - Map.fold (fun id x s -> (to_string id ^ " -> " ^ show_a x) :: s) s [] - in - let ids = List.rev ids in - "{" ^ String.concat "," ids ^ "}" - - let pp_map_t (pp_a : Format.formatter -> 'a -> unit) (fmt : Format.formatter) - (m : 'a map_t) : unit = - let pp_string = Format.pp_print_string fmt in - pp_string "{"; - Map.iter - (fun id x -> - pp_string (to_string id ^ " -> "); - pp_a fmt x; - pp_string ",") - m; - pp_string "}" - - let set_to_string indent_opt ids = - let indent, sep = - match indent_opt with Some indent -> (indent, ",\n") | None -> ("", ",") - in - let ids = Set.fold (fun id ids -> (indent ^ to_string id) :: ids) ids [] in - match ids with - | [] -> "{}" - | _ -> "{\n" ^ String.concat sep (List.rev ids) ^ "\n}" - - let map_to_string indent_opt a_to_string ids = - let indent, sep = - match indent_opt with Some indent -> (indent, ",\n") | None -> ("", ",") - in - let ids = - Map.fold - (fun id v ids -> - (indent ^ to_string id ^ " -> " ^ a_to_string v) :: ids) - ids [] - in - match ids with - | [] -> "{}" - | _ -> "{\n" ^ String.concat sep (List.rev ids) ^ "\n}" + let show_t = show_id + end - let id_of_json js = - (* TODO: check boundaries ? *) - match js with - | `Int i -> Ok i - | _ -> Error ("id_of_json: failed on " ^ Yojson.Basic.show js) + module Set = C.MakeSet (Ord) + module Map = C.MakeMap (Ord) end type name = string list [@@deriving show] diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml index cde799d8..faa63c0a 100644 --- a/src/InterpreterBorrows.ml +++ b/src/InterpreterBorrows.ml @@ -430,7 +430,7 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id) it was left unchanged. *) let give_back_symbolic_value (_config : C.config) - (proj_regions : T.RegionId.set_t) (proj_ty : T.rty) (sv : V.symbolic_value) + (proj_regions : T.RegionId.Set.t) (proj_ty : T.rty) (sv : V.symbolic_value) (nsv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = let subst local_regions local_ty = let child_proj = @@ -971,7 +971,7 @@ and end_abstraction (config : C.config) (chain : borrow_or_abs_ids) ctx and end_abstractions (config : C.config) (chain : borrow_or_abs_ids) - (abs_ids : V.AbstractionId.set_t) (ctx : C.eval_ctx) : C.eval_ctx = + (abs_ids : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx = V.AbstractionId.Set.fold (fun id ctx -> end_abstraction config chain id ctx) abs_ids ctx @@ -1185,7 +1185,7 @@ and end_abstraction_remove_from_context (_config : C.config) abstraction *) and end_proj_loans_symbolic (config : C.config) (chain : borrow_or_abs_ids) - (abs_id : V.AbstractionId.id) (regions : T.RegionId.set_t) + (abs_id : V.AbstractionId.id) (regions : T.RegionId.Set.t) (sv : V.symbolic_value) (ctx : C.eval_ctx) : C.eval_ctx = (* Find the first proj_borrows which intersects the proj_loans *) let explore_shared = true in diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml index 6bc31d63..455d62c3 100644 --- a/src/InterpreterBorrowsCore.ml +++ b/src/InterpreterBorrowsCore.ml @@ -31,7 +31,7 @@ type exploration_kind = { let ek_all : exploration_kind = { enter_shared_loans = true; enter_mut_borrows = true; enter_abs = true } -type borrow_ids = Borrows of V.BorrowId.set_t | Borrow of V.BorrowId.id +type borrow_ids = Borrows of V.BorrowId.Set.t | Borrow of V.BorrowId.id [@@deriving show] exception FoundBorrowIds of borrow_ids @@ -84,8 +84,8 @@ let add_borrow_or_abs_id_to_chain (msg : string) (id : borrow_or_abs_id) Note that the two abstractions have different views (in terms of regions) of the symbolic value (hence the two region types). *) -let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.set_t) - (ty2 : T.rty) (rset2 : T.RegionId.set_t) : bool = +let rec projections_intersect (ty1 : T.rty) (rset1 : T.RegionId.Set.t) + (ty2 : T.rty) (rset2 : T.RegionId.Set.t) : bool = match (ty1, ty2) with | T.Bool, T.Bool | T.Char, T.Char | T.Str, T.Str -> false | T.Integer int_ty1, T.Integer int_ty2 -> diff --git a/src/InterpreterProjectors.ml b/src/InterpreterProjectors.ml index d2d10670..7c648563 100644 --- a/src/InterpreterProjectors.ml +++ b/src/InterpreterProjectors.ml @@ -13,7 +13,7 @@ type symbolic_expansion = | SeConcrete of V.constant_value | SeAdt of (T.VariantId.id option * V.symbolic_value list) | SeMutRef of V.BorrowId.id * V.symbolic_value - | SeSharedRef of V.BorrowId.set_t * V.symbolic_value + | SeSharedRef of V.BorrowId.Set.t * V.symbolic_value (** Auxiliary function. @@ -23,7 +23,7 @@ type symbolic_expansion = *) let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id) - (regions : T.RegionId.set_t) (v : V.typed_value) (ty : T.rty) : + (regions : T.RegionId.Set.t) (v : V.typed_value) (ty : T.rty) : V.abstract_shared_borrows = (* Sanity check - TODO: move this elsewhere (here we perform the check at every * recursive call which is a bit overkill...) *) @@ -132,7 +132,7 @@ let rec apply_proj_borrows_on_shared_borrow (ctx : C.eval_ctx) *) let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) (fresh_reborrow : V.BorrowId.id -> V.BorrowId.id) - (regions : T.RegionId.set_t) (ancestors_regions : T.RegionId.set_t) + (regions : T.RegionId.Set.t) (ancestors_regions : T.RegionId.Set.t) (v : V.typed_value) (ty : T.rty) : V.typed_avalue = (* Sanity check - TODO: move this elsewhere (here we perform the check at every * recursive call which is a bit overkill...) *) @@ -235,9 +235,9 @@ let rec apply_proj_borrows (check_symbolic_no_ended : bool) (ctx : C.eval_ctx) (lazy ("projections_intersect:" ^ "\n- ty1: " ^ rty_to_string ctx ty1 ^ "\n- rset1: " - ^ T.RegionId.set_to_string None rset1 + ^ T.RegionId.Set.to_string None rset1 ^ "\n- ty2: " ^ rty_to_string ctx ty2 ^ "\n- rset2: " - ^ T.RegionId.set_to_string None rset2 + ^ T.RegionId.Set.to_string None rset2 ^ "\n")); assert (not (projections_intersect ty1 rset1 ty2 rset2))); V.ASymbolic (V.AProjBorrows (s, ty)) @@ -290,7 +290,7 @@ let symbolic_expansion_non_shared_borrow_to_value (sv : V.symbolic_value) TODO: detailed comments. See [apply_proj_borrows] *) -let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.set_t) +let apply_proj_loans_on_symbolic_expansion (regions : T.RegionId.Set.t) (see : symbolic_expansion) (original_sv_ty : T.rty) : V.typed_avalue = (* Sanity check: if we have a proj_loans over a symbolic value, it should * contain regions which we will project *) @@ -528,7 +528,7 @@ let prepare_reborrows (config : C.config) (allow_reborrows : bool) : (fresh_reborrow, apply_registered_reborrows) let apply_proj_borrows_on_input_value (config : C.config) (ctx : C.eval_ctx) - (regions : T.RegionId.set_t) (ancestors_regions : T.RegionId.set_t) + (regions : T.RegionId.Set.t) (ancestors_regions : T.RegionId.Set.t) (v : V.typed_value) (ty : T.rty) : C.eval_ctx * V.typed_avalue = let check_symbolic_no_ended = true in let allow_reborrows = true in diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml index 1b06dd7f..8b29bac9 100644 --- a/src/InterpreterStatements.ml +++ b/src/InterpreterStatements.ml @@ -554,7 +554,7 @@ let create_empty_abstractions_from_abs_region_groups * - the regions of the ancestors of abs_id * - the regions of abs_id *) - let abs_to_ancestors_regions : T.RegionId.set_t V.AbstractionId.Map.t ref = + let abs_to_ancestors_regions : T.RegionId.Set.t V.AbstractionId.Map.t ref = ref V.AbstractionId.Map.empty in (* Auxiliary function to create one abstraction *) diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml index fc86f1f5..971dc801 100644 --- a/src/InterpreterUtils.ml +++ b/src/InterpreterUtils.ml @@ -192,7 +192,7 @@ let symbolic_value_id_in_ctx (sv_id : V.SymbolicValueId.id) (ctx : C.eval_ctx) : check that the set of ended regions doesn't intersect the set of regions used in the type (this is more general). *) -let symbolic_value_has_ended_regions (ended_regions : T.RegionId.set_t) +let symbolic_value_has_ended_regions (ended_regions : T.RegionId.Set.t) (s : V.symbolic_value) : bool = let regions = rty_regions s.V.sv_ty in not (T.RegionId.Set.disjoint regions ended_regions) @@ -202,7 +202,7 @@ let symbolic_value_has_ended_regions (ended_regions : T.RegionId.set_t) Note that this function is very general: it also checks wether symbolic values contain already ended regions. *) -let bottom_in_value (ended_regions : T.RegionId.set_t) (v : V.typed_value) : +let bottom_in_value (ended_regions : T.RegionId.Set.t) (v : V.typed_value) : bool = let obj = object diff --git a/src/Invariants.ml b/src/Invariants.ml index 66a5e5ac..77b11136 100644 --- a/src/Invariants.ml +++ b/src/Invariants.ml @@ -19,8 +19,8 @@ type borrow_info = { loan_kind : T.ref_kind; loan_in_abs : bool; (* true if the loan was found in an abstraction *) - loan_ids : V.BorrowId.set_t; - borrow_ids : V.BorrowId.set_t; + loan_ids : V.BorrowId.Set.t; + borrow_ids : V.BorrowId.Set.t; } [@@deriving show] @@ -36,14 +36,13 @@ let set_outer_mut (info : outer_borrow_info) : outer_borrow_info = let set_outer_shared (_info : outer_borrow_info) : outer_borrow_info = { outer_borrow = true; outer_shared = true } -(* TODO: we need to factorize print functions for sets *) let ids_reprs_to_string (indent : string) (reprs : V.BorrowId.id V.BorrowId.Map.t) : string = - V.BorrowId.map_to_string (Some indent) V.BorrowId.to_string reprs + V.BorrowId.Map.to_string (Some indent) V.BorrowId.to_string reprs let borrows_infos_to_string (indent : string) (infos : borrow_info V.BorrowId.Map.t) : string = - V.BorrowId.map_to_string (Some indent) show_borrow_info infos + V.BorrowId.Map.to_string (Some indent) show_borrow_info infos type borrow_kind = Mut | Shared | Inactivated @@ -79,7 +78,7 @@ let check_loans_borrows_relation_invariant (ctx : C.eval_ctx) : unit = ignored_loans := (rkind, bid) :: !ignored_loans in - let register_shared_loan (loan_in_abs : bool) (bids : V.BorrowId.set_t) : unit + let register_shared_loan (loan_in_abs : bool) (bids : V.BorrowId.Set.t) : unit = let reprs = !ids_reprs in let infos = !borrows_infos in @@ -612,7 +611,7 @@ let check_typing_invariant (ctx : C.eval_ctx) : unit = type proj_borrows_info = { abs_id : V.AbstractionId.id; - regions : T.RegionId.set_t; + regions : T.RegionId.Set.t; proj_ty : T.rty; as_shared_value : bool; (** True if the value is below a shared borrow *) } @@ -620,7 +619,7 @@ type proj_borrows_info = { type proj_loans_info = { abs_id : V.AbstractionId.id; - regions : T.RegionId.set_t; + regions : T.RegionId.Set.t; } [@@deriving show] @@ -704,7 +703,7 @@ let check_symbolic_values (_config : C.config) (ctx : C.eval_ctx) : unit = log#ldebug (lazy ("check_symbolic_values: collected information:\n" - ^ V.SymbolicValueId.map_to_string (Some " ") show_sv_info !infos)); + ^ V.SymbolicValueId.Map.to_string (Some " ") show_sv_info !infos)); (* Check *) let check_info _id info = assert (info.env_count = 0 || info.aproj_borrows = []); diff --git a/src/Print.ml b/src/Print.ml index 000874fe..282b2860 100644 --- a/src/Print.ml +++ b/src/Print.ml @@ -290,7 +290,7 @@ module Values = struct string = match lc with | SharedLoan (loans, v) -> - let loans = V.BorrowId.set_to_string None loans in + let loans = V.BorrowId.Set.to_string None loans in "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string fmt v ^ ")" | MutLoan bid -> "⌊mut@" ^ V.BorrowId.to_string bid ^ "⌋" @@ -375,7 +375,7 @@ module Values = struct ^ typed_avalue_to_string fmt av ^ "⌋" | ASharedLoan (loans, v, av) -> - let loans = V.BorrowId.set_to_string None loans in + let loans = V.BorrowId.Set.to_string None loans in "@shared_loan(" ^ loans ^ ", " ^ typed_value_to_string fmt v ^ ", " @@ -441,9 +441,9 @@ module Values = struct indent ^ "abs@" ^ V.AbstractionId.to_string abs.abs_id ^ "{parents=" - ^ V.AbstractionId.set_to_string None abs.parents + ^ V.AbstractionId.Set.to_string None abs.parents ^ "}" ^ "{regions=" - ^ T.RegionId.set_to_string None abs.regions + ^ T.RegionId.Set.to_string None abs.regions ^ "}" ^ " {\n" ^ avs ^ "\n" ^ indent ^ "}" end @@ -552,7 +552,7 @@ module Contexts = struct let eval_ctx_to_string (ctx : C.eval_ctx) : string = let fmt = eval_ctx_to_ctx_formatter ctx in - let ended_regions = T.RegionId.set_to_string None ctx.ended_regions in + let ended_regions = T.RegionId.Set.to_string None ctx.ended_regions in let frames = split_env_according_to_frames ctx.env in let num_frames = List.length frames in let frames = diff --git a/src/TypesUtils.ml b/src/TypesUtils.ml index 38560894..3accb9c5 100644 --- a/src/TypesUtils.ml +++ b/src/TypesUtils.ml @@ -44,11 +44,11 @@ let mk_ref_ty (r : 'r) (ty : 'r ty) (ref_kind : ref_kind) : 'r ty = let mk_box_ty (ty : 'r ty) : 'r ty = Adt (Assumed Box, [], [ ty ]) (** Check if a region is in a set of regions *) -let region_in_set (r : RegionId.id region) (rset : RegionId.set_t) : bool = +let region_in_set (r : RegionId.id region) (rset : RegionId.Set.t) : bool = match r with Static -> false | Var id -> RegionId.Set.mem id rset (** Return the set of regions in an rty *) -let rty_regions (ty : rty) : RegionId.set_t = +let rty_regions (ty : rty) : RegionId.Set.t = let s = ref RegionId.Set.empty in let add_region (r : RegionId.id region) = match r with Static -> () | Var rid -> s := RegionId.Set.add rid !s @@ -65,7 +65,7 @@ let rty_regions (ty : rty) : RegionId.set_t = (* Return the set of accumulated regions *) !s -let rty_regions_intersect (ty : rty) (regions : RegionId.set_t) : bool = +let rty_regions_intersect (ty : rty) (regions : RegionId.Set.t) : bool = let ty_regions = rty_regions ty in not (RegionId.Set.disjoint ty_regions regions) diff --git a/src/Values.ml b/src/Values.ml index 31f47709..59cfbdca 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -132,7 +132,7 @@ and borrow_content = *) and loan_content = - | SharedLoan of (BorrowId.set_t[@opaque]) * typed_value + | SharedLoan of (BorrowId.Set.t[@opaque]) * typed_value | MutLoan of (BorrowId.id[@opaque]) (** TODO: we might want to add a set of borrow ids (useful for inactivated borrows, and extremely useful when giving shared values to abstractions). @@ -322,7 +322,7 @@ and aloan_content = px -> mut_borrow l0 (mut_borrow @s1) ``` *) - | ASharedLoan of (BorrowId.set_t[@opaque]) * typed_value * typed_avalue + | ASharedLoan of (BorrowId.Set.t[@opaque]) * typed_value * typed_avalue (** A shared loan owned by an abstraction. Example: @@ -599,9 +599,9 @@ and typed_avalue = { value : avalue; ty : rty } type abs = { abs_id : (AbstractionId.id[@opaque]); - parents : (AbstractionId.set_t[@opaque]); (** The parent abstractions *) - regions : (RegionId.set_t[@opaque]); (** Regions owned by this abstraction *) - ancestors_regions : (RegionId.set_t[@opaque]); + parents : (AbstractionId.Set.t[@opaque]); (** The parent abstractions *) + regions : (RegionId.Set.t[@opaque]); (** Regions owned by this abstraction *) + ancestors_regions : (RegionId.Set.t[@opaque]); (** Union of the regions owned by this abstraction's ancestors (not including the regions of this abstraction itself) *) avalues : typed_avalue list; (** The values in this abstraction *) |