summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-15 21:15:20 +0100
committerSon Ho2022-01-15 21:15:20 +0100
commit231c65c04c511db3c8f7f68cd5d37cdeeedfe809 (patch)
treefbf656ae97d6a00c21f344c6de9fc50e444d9089
parent9711789ae50ddcf2d2f4181044ba4f5eeb139ec8 (diff)
Use the new collections
Diffstat (limited to '')
-rw-r--r--src/Contexts.ml4
-rw-r--r--src/Identifiers.ml124
-rw-r--r--src/InterpreterBorrows.ml6
-rw-r--r--src/InterpreterBorrowsCore.ml6
-rw-r--r--src/InterpreterProjectors.ml14
-rw-r--r--src/InterpreterStatements.ml2
-rw-r--r--src/InterpreterUtils.ml4
-rw-r--r--src/Invariants.ml17
-rw-r--r--src/Print.ml10
-rw-r--r--src/TypesUtils.ml6
-rw-r--r--src/Values.ml10
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 *)