summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-29 23:46:20 +0100
committerSon Ho2021-11-29 23:46:20 +0100
commitac0bc7e011a93d955b5078e27f890e5a6916b412 (patch)
treecc50b9253c6d8623a67b71e03f1eee637f861213
parent2c7e19de3465c2ead68a4c851f2cc140d1542969 (diff)
Derive more debugging facilities
-rw-r--r--src/Identifiers.ml17
-rw-r--r--src/Values.ml43
2 files changed, 47 insertions, 13 deletions
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index e1684f2c..931ec97b 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -12,6 +12,8 @@ module type Id = sig
type 'a vector
+ type set_t
+
val zero : id
val generator_zero : generator
@@ -68,9 +70,13 @@ module type Id = sig
val exists : ('a -> bool) -> 'a vector -> bool
+ val pp_set_t : Format.formatter -> set_t -> unit
+
+ val show_set_t : set_t -> string
+
module Ord : Map.OrderedType with type t = id
- module Set : Set.S with type elt = id
+ module Set : Set.S with type elt = id with type t = set_t
val set_to_string : Set.t -> string
@@ -157,6 +163,15 @@ module IdGen () : Id = struct
module Set = Set.Make (Ord)
module Map = Map.Make (Ord)
+ type set_t = Set.t
+
+ 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 = Format.pp_print_string fmt (show_set_t s)
+
let set_to_string ids =
let ids = Set.fold (fun id ids -> to_string id :: ids) ids [] in
"{" ^ String.concat ", " (List.rev ids) ^ "}"
diff --git a/src/Values.ml b/src/Values.ml
index e549846d..07dfb618 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -35,7 +35,12 @@ let big_int_of_yojson (json : Yojson.Safe.t) : (big_int, string) result =
let big_int_to_yojson (i : big_int) = `Intlit (Z.to_string i)
-type scalar_value = { value : big_int; int_ty : integer_type }
+let pp_big_int (fmt : Format.formatter) (bi : big_int) : unit =
+ Format.pp_print_string fmt (Z.to_string bi)
+
+let show_big_int (bi : big_int) : string = Z.to_string bi
+
+type scalar_value = { value : big_int; int_ty : integer_type } [@@deriving show]
(** A scalar value
Note that we use unbounded integers everywhere.
@@ -48,15 +53,18 @@ type constant_value =
| Bool of bool
| Char of char
| String of string
+[@@deriving show]
type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty }
+[@@deriving show]
(** Symbolic value *)
type symbolic_proj_comp = {
svalue : symbolic_value; (** The symbolic value itself *)
- rset_ended : RegionId.Set.t;
+ rset_ended : RegionId.set_t;
(** The regions used in the symbolic value which have already ended *)
}
+[@@deriving show]
(** A complementary projector over a symbolic value.
"Complementary" stands for the fact that it is a projector over all the
@@ -74,6 +82,7 @@ type value =
| Borrow of borrow_content (** A borrowed value *)
| Loan of loan_content (** A loaned value *)
| Symbolic of symbolic_proj_comp (** Unknown value *)
+[@@deriving show]
and adt_value = {
def_id : TypeDefId.id;
@@ -82,6 +91,7 @@ and adt_value = {
types : ety list;
field_values : typed_value FieldId.vector;
}
+[@@deriving show]
and borrow_content =
| SharedBorrow of BorrowId.id (** A shared value *)
@@ -97,20 +107,23 @@ and borrow_content =
is well typed) of this value and replace the inactivated borrow with a
mutable borrow.
*)
+[@@deriving show]
and loan_content =
- | SharedLoan of BorrowId.Set.t * typed_value
+ | SharedLoan of BorrowId.set_t * typed_value
| MutLoan of BorrowId.id
+[@@deriving show]
-and assumed_value = Box of typed_value
+and assumed_value = Box of typed_value [@@deriving show]
-and typed_value = { value : value; ty : ety }
+and typed_value = { value : value; ty : ety } [@@deriving show]
type abstract_shared_borrows =
- | AsbSet of BorrowId.Set.t
+ | AsbSet of BorrowId.set_t
| AsbProjReborrows of symbolic_value * rty
| AsbUnion of abstract_shared_borrows * abstract_shared_borrows
(** TODO: explanations *)
+[@@deriving show]
(** Abstraction values are used inside of abstractions to properly model
borrowing relations introduced by function calls.
@@ -127,6 +140,7 @@ type avalue =
| ABorrow of aborrow_content
| AAssumed of aassumed_value
| AProj of aproj
+[@@deriving show]
and aadt_value = {
adef_id : TypeDefId.id;
@@ -135,14 +149,16 @@ and aadt_value = {
atypes : rty list;
afield_values : typed_avalue FieldId.vector;
}
+[@@deriving show]
and aloan_content =
| AMutLoan of BorrowId.id * typed_avalue
- | ASharedLoan of BorrowId.Set.t * typed_value * typed_avalue
+ | ASharedLoan of BorrowId.set_t * typed_value * typed_avalue
| AEndedMutLoan of { given_back : typed_value; child : typed_avalue }
| AEndedSharedLoan of typed_value * typed_avalue
| AIgnoredMutLoan of BorrowId.id * typed_avalue
| AIgnoredSharedLoan of abstract_shared_borrows
+[@@deriving show]
(** Note that when a borrow content is ended, it is replaced by Bottom (while
we need to track ended loans more precisely, especially because of their
@@ -153,24 +169,27 @@ and aborrow_content =
| AIgnoredMutBorrow of typed_avalue
| AEndedIgnoredMutLoan of { given_back : typed_avalue; child : typed_avalue }
| AIgnoredSharedBorrow of abstract_shared_borrows
+[@@deriving show]
-and aassumed_value = ABox of typed_avalue
+and aassumed_value = ABox of typed_avalue [@@deriving show]
and aproj =
| AProjLoans of symbolic_value
| AProjBorrows of symbolic_value * rty
+[@@deriving show]
-and typed_avalue = { avalue : avalue; aty : rty }
+and typed_avalue = { avalue : avalue; aty : rty } [@@deriving show]
type abs = {
abs_id : AbstractionId.id;
- parents : AbstractionId.Set.t; (** The parent abstractions *)
- acc_regions : RegionId.Set.t;
+ parents : AbstractionId.set_t; (** The parent abstractions *)
+ acc_regions : RegionId.set_t;
(** Union of the regions owned by the (transitive) parent abstractions and
by the current abstraction *)
- regions : RegionId.Set.t; (** Regions owned by this abstraction *)
+ regions : RegionId.set_t; (** Regions owned by this abstraction *)
avalues : typed_avalue list; (** The values in this abstraction *)
}
+[@@deriving show]
(** Abstractions model the parts in the borrow graph where the borrowing relations
have been abstracted because of a function call.