summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Identifiers.ml12
-rw-r--r--src/Values.ml47
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