diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Identifiers.ml | 6 | ||||
| -rw-r--r-- | src/Print.ml | 34 | ||||
| -rw-r--r-- | src/Values.ml | 46 |
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 = { |