summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-22 09:57:23 +0100
committerSon Ho2021-11-22 09:57:23 +0100
commitc1f628b7fde13df56bc7e71f1619f4427ed157dc (patch)
tree9eb3eeca18662b2b0da9ed62148e1cbcfe5ee279
parent6d21462223fe26a92ee565deb56e48670a74f16a (diff)
Start working on printing for avalues
-rw-r--r--src/Identifiers.ml6
-rw-r--r--src/Print.ml34
-rw-r--r--src/Values.ml46
3 files changed, 54 insertions, 32 deletions
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index be6a3c58..51a22072 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -23,6 +23,8 @@ module type Id = sig
module Set : Set.S with type elt = id
+ val set_to_string : Set.t -> string
+
val id_of_json : Yojson.Basic.t -> (id, string) result
val vector_of_json :
@@ -63,6 +65,10 @@ module IdGen () : Id = struct
let compare = compare
end)
+ let set_to_string ids =
+ let ids = Set.fold (fun id ids -> to_string id :: ids) ids [] in
+ "{" ^ String.concat ", " (List.rev ids) ^ "}"
+
let id_of_json js =
match js with
| `Int i -> Ok i
diff --git a/src/Print.ml b/src/Print.ml
index 1ad2f5cb..47350324 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -211,15 +211,8 @@ module Values = struct
let symbolic_proj_comp_to_string (fmt : rtype_formatter)
(sp : symbolic_proj_comp) : string =
- let regions =
- RegionId.Set.fold
- (fun id ids -> region_id_to_string id :: ids)
- sp.rset_ended []
- in
- let regions = String.concat "," (List.rev regions) in
- "proj_comp {" ^ regions ^ "} ("
- ^ symbolic_value_to_string fmt sp.svalue
- ^ ")"
+ let regions = RegionId.set_to_string sp.rset_ended in
+ "proj_comp " ^ regions ^ " (" ^ symbolic_value_to_string fmt sp.svalue ^ ")"
let rec typed_value_to_string (fmt : value_formatter) (v : typed_value) :
string =
@@ -268,12 +261,23 @@ module Values = struct
string =
match lc with
| SharedLoan (loans, v) ->
- let loans =
- BorrowId.Set.fold
- (fun lid loans -> BorrowId.to_string lid :: loans)
- loans []
- in
- let loans = String.concat ", " (List.rev loans) in
+ let loans = BorrowId.set_to_string loans in
"@shared_loan({" ^ loans ^ "}, " ^ typed_value_to_string fmt v ^ ")"
| MutLoan bid -> "⌊mut@" ^ BorrowId.to_string bid ^ "⌋"
+
+ let rec abstract_shared_borrows_to_string (fmt : value_formatter)
+ (abs : abstract_shared_borrows) : string =
+ match abs with
+ | AsbSet bs -> BorrowId.set_to_string bs
+ | AsbProjReborrows (sv, rty) ->
+ "{"
+ ^ symbolic_value_id_to_string sv.sv_id
+ ^ " : "
+ ^ ty_to_string (value_to_rtype_formatter fmt) sv.sv_ty
+ ^ " <: "
+ ^ ty_to_string (value_to_rtype_formatter fmt) rty
+ | AsbUnion (asb1, asb2) ->
+ abstract_shared_borrows_to_string fmt asb1
+ ^ " U "
+ ^ abstract_shared_borrows_to_string fmt asb2
end
diff --git a/src/Values.ml b/src/Values.ml
index 0fe928fa..5ebc97b0 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -114,10 +114,10 @@ and assumed_value = Box of typed_value
and typed_value = { value : value; ty : ety }
-type abstract_shared_borrow =
- | AsvSet of BorrowId.Set.t
- | AsvProjReborrows of symbolic_value * rty
- | AsvUntion of abstract_shared_borrow * abstract_shared_borrow
+type abstract_shared_borrows =
+ | AsbSet of BorrowId.Set.t
+ | AsbProjReborrows of symbolic_value * rty
+ | AsbUnion of abstract_shared_borrows * abstract_shared_borrows
(** TODO: explanations *)
(** Abstraction values are used inside of abstractions to properly model
@@ -131,20 +131,10 @@ type avalue =
| AAdt of aadt_value
| ATuple of typed_avalue FieldId.vector
| ABottom
+ | ALoan of aloan_content
+ | ABorrow of aborrow_content
| AAssumed of aassumed_value
- | AMutBorrow of BorrowId.id * typed_avalue
- | ASharedBorrow of BorrowId.id
- | AMutLoan of BorrowId.id * typed_avalue
- | ASharedLoan of BorrowId.Set.t * value * typed_avalue
- | AEndedMutLoan of value * typed_avalue (* TODO: given_back, child *)
- | AEndedSharedLoan of value * typed_avalue
- | AIgnoredMutLoan of BorrowId.id * typed_avalue
- | AIgnoredMutBorrow of typed_avalue
- | AEndedIgnoredMutLoan of typed_avalue * typed_avalue (* TODO: given back, child *)
- | AIgnoredSharedBorrow of abstract_shared_borrow
- | AIgnoredSharedLoan of abstract_shared_borrow
- | AProjLoans of symbolic_value
- | AProjBorrows of symbolic_value * rty
+ | AProj of aproj
and aadt_value = {
adef_id : TypeDefId.id;
@@ -154,8 +144,30 @@ and aadt_value = {
afield_values : typed_avalue FieldId.vector;
}
+and aloan_content =
+ | AMutLoan of BorrowId.id * typed_avalue
+ | ASharedLoan of BorrowId.Set.t * value * typed_avalue
+ | AEndedMutLoan of value * typed_avalue (* TODO: given_back, child *)
+ | AEndedSharedLoan of value * typed_avalue
+ | AIgnoredMutLoan of BorrowId.id * typed_avalue
+ | AIgnoredSharedLoan of abstract_shared_borrows
+
+(** 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
+ children values) *)
+and aborrow_content =
+ | AMutBorrow of BorrowId.id * typed_avalue
+ | ASharedBorrow of BorrowId.id
+ | AIgnoredMutBorrow of typed_avalue
+ | AEndedIgnoredMutLoan of typed_avalue * typed_avalue (* TODO: given back, child *)
+ | AIgnoredSharedBorrow of abstract_shared_borrows
+
and aassumed_value = ABox of typed_avalue
+and aproj =
+ | AProjLoans of symbolic_value
+ | AProjBorrows of symbolic_value * rty
+
and typed_avalue = { avalue : avalue; aty : rty }
type abs = {