diff options
| -rw-r--r-- | src/Identifiers.ml | 12 | ||||
| -rw-r--r-- | src/Values.ml | 47 |
2 files changed, 57 insertions, 2 deletions
diff --git a/src/Identifiers.ml b/src/Identifiers.ml index 28ed1909..7d440f4d 100644 --- a/src/Identifiers.ml +++ b/src/Identifiers.ml @@ -17,7 +17,9 @@ module type Id = sig val to_string : id -> string - val empty : 'a vector + val empty_vector : 'a vector + + module Set : Set.S with type elt = id val id_of_json : Yojson.Basic.t -> (id, string) result @@ -47,7 +49,13 @@ module IdGen () : Id = struct let to_string = string_of_int - let empty = [] + let empty_vector = [] + + module Set = Set.Make (struct + type t = id + + let compare = compare + end) let id_of_json js = match js with diff --git a/src/Values.ml b/src/Values.ml index e1205efc..051949fc 100644 --- a/src/Values.ml +++ b/src/Values.ml @@ -3,6 +3,8 @@ open Types module VarId = IdGen () +module BorrowId = IdGen () + type var = { index : VarId.id; (** Unique variable identifier *) name : string option; @@ -42,8 +44,53 @@ type scalar_value = | U64 of big_int | U128 of big_int +(** A constant value *) type constant_value = | Scalar of scalar_value | Bool of bool | Char of char | String of string + +type symbolic_value = unit +(** Symbolic value - TODO *) + +(** An untyped value, used in the environments *) +type value = + | Adt of adt_value (** Enumerations and structures *) + | Symbolic of symbolic_value (** Unknown value *) + | Concrete of constant_value (** Concrete (non-symbolic) value *) + | Tuple of value FieldId.vector + (** Tuple - note that units are encoded as 0-tuples *) + | Borrow of borrow_content (** A borrowed value *) + | Loan of loan_content (** A loaned value *) + | Bottom (** No value (uninitialized or moved value) *) + | Assumed of assumed_value (** Assumed types (Box, Vec, Cell...) *) + +and adt_value = { + def_id : TypeDefId.id; + variant_id : VariantId.id option; + regions : erased_region list; + types : rty list; + field_values : value FieldId.vector; +} + +and borrow_content = + | SharedBorrow of BorrowId.id (** A shared value *) + | MutBorrow of BorrowId.id * value (** A mutably borrowed value *) + | InactivatedMutBorrow of BorrowId.id + (** An inactivated mut borrow. + + This is used to model two-phase borrows. When evaluating a two-phase + mutable borrow, we first introduce an inactivated borrow which behaves + like a shared borrow, until the moment we actually *use* the borrow: + at this point, we end all the other shared borrows (or inactivated borrows + - though there shouldn't be any other inactivated borrows if the program + is well typed) of this value and replace the inactivated borrow with a + mutable borrow. + *) + +and loan_content = + | SharedLoan of BorrowId.Set.t * value + | MutLoan of BorrowId.id + +and assumed_value = Box of value |