summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/Errors.ml4
-rw-r--r--src/Identifiers.ml8
-rw-r--r--src/Interpreter.ml112
-rw-r--r--src/Values.ml38
-rw-r--r--src/main.ml1
5 files changed, 145 insertions, 18 deletions
diff --git a/src/Errors.ml b/src/Errors.ml
index dcdc9102..b9263d5a 100644
--- a/src/Errors.ml
+++ b/src/Errors.ml
@@ -3,3 +3,7 @@ exception IntegerOverflow of unit
exception Unimplemented of string
let unimplemented msg = raise (Unimplemented ("unimplemented: " ^ msg))
+
+exception Unreachable of string
+
+let unreachable msg = raise (Unreachable ("unreachable: " ^ msg))
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 07d9c8a5..be6a3c58 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -17,6 +17,10 @@ module type Id = sig
val empty_vector : 'a vector
+ val vector_to_list : 'a vector -> 'a list
+
+ val vector_of_list : 'a list -> 'a vector
+
module Set : Set.S with type elt = id
val id_of_json : Yojson.Basic.t -> (id, string) result
@@ -49,6 +53,10 @@ module IdGen () : Id = struct
let empty_vector = []
+ let vector_to_list v = v
+
+ let vector_of_list v = v
+
module Set = Set.Make (struct
type t = id
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
new file mode 100644
index 00000000..b8daf38d
--- /dev/null
+++ b/src/Interpreter.ml
@@ -0,0 +1,112 @@
+open Types
+open Values
+
+type env_value = Var of string * typed_value | Abs of abs
+
+type env = env_value list
+
+type 'a result = Stuck | Panic | Res of 'a
+
+type interpreter_mode = ConcreteMode | SymbolicMode
+
+type config = { mode : interpreter_mode; check_invariants : bool }
+
+type outer_borrows = Borrows of BorrowId.Set.t | Borrow of BorrowId.id
+
+(** Borrow lookup result *)
+type borrow_lres =
+ | Outer of outer_borrows
+ | FoundMut of typed_value
+ | FoundShared
+ | NotFound
+
+let update_if_none opt x = match opt with None -> Some x | _ -> opt
+
+let unwrap_res_to_outer_or opt default =
+ match opt with Some x -> Outer x | None -> default
+
+let rec end_borrow_get_borrow_in_value config l outer_borrows v0 :
+ borrow_lres * typed_value =
+ match v0.value with
+ | Concrete _ | Bottom | Symbolic _ -> (NotFound, v0)
+ | Assumed (Box bv) ->
+ let res, bv' = end_borrow_get_borrow_in_value config l outer_borrows bv in
+ (* Note that we allow boxes to outlive the inner borrows.
+ * Also note that when using the symbolic mode, boxes will never
+ * be "opened" and will be manipulated solely through functions
+ * like new, deref, etc. which will enforce that we destroy
+ * boxes upon ending inner borrows *)
+ (res, { v0 with value = Assumed (Box bv') })
+ | Adt adt ->
+ let values = FieldId.vector_to_list adt.field_values in
+ let res, values' =
+ end_borrow_get_borrow_in_values config l outer_borrows values
+ in
+ let values' = FieldId.vector_of_list values' in
+ (res, { v0 with value = Adt { adt with field_values = values' } })
+ | Tuple values ->
+ let values = FieldId.vector_to_list values in
+ let res, values' =
+ end_borrow_get_borrow_in_values config l outer_borrows values
+ in
+ let values' = FieldId.vector_of_list values' in
+ (res, { v0 with value = Tuple values' })
+ | Loan (MutLoan _) -> (NotFound, v0)
+ | Loan (SharedLoan (borrows, v)) ->
+ let outer_borrows = update_if_none outer_borrows (Borrows borrows) in
+ let res, v' = end_borrow_get_borrow_in_value config l outer_borrows v in
+ (res, { value = Loan (SharedLoan (borrows, v')); ty = v0.ty })
+ | Borrow (SharedBorrow l') ->
+ if l = l' then
+ ( unwrap_res_to_outer_or outer_borrows FoundShared,
+ { v0 with value = Bottom } )
+ else (NotFound, v0)
+ | Borrow (InactivatedMutBorrow l') ->
+ if l = l' then
+ ( unwrap_res_to_outer_or outer_borrows FoundShared,
+ { v0 with value = Bottom } )
+ else (NotFound, v0)
+ | Borrow (MutBorrow (l', bv)) ->
+ if l = l' then
+ ( unwrap_res_to_outer_or outer_borrows (FoundMut bv),
+ { v0 with value = Bottom } )
+ else
+ let outer_borrows = update_if_none outer_borrows (Borrow l') in
+ let res, bv' =
+ end_borrow_get_borrow_in_value config l outer_borrows bv
+ in
+ (res, { v0 with value = Borrow (MutBorrow (l', bv')) })
+
+and end_borrow_get_borrow_in_values config l outer_borrows vl0 :
+ borrow_lres * typed_value list =
+ match vl0 with
+ | [] -> (NotFound, vl0)
+ | v :: vl -> (
+ let res, v' = end_borrow_get_borrow_in_value config l outer_borrows v in
+ match res with
+ | NotFound ->
+ let res, vl' =
+ end_borrow_get_borrow_in_values config l outer_borrows vl
+ in
+ (res, v' :: vl')
+ | _ -> (res, v' :: vl))
+
+(*let rec end_borrow_get_borrow_in_env config l env : borrow_lres * env =
+ match env with
+ | [] -> NotFound
+ | Var (x, v) :: env' -> (
+ match end_borrow_get_borrow_in_value config None l v with
+ | NotFound, v' ->
+ let res, env'' = end_borrow_get_borrow_in_env config l env' in
+ (res, Var (x, v') :: env'')
+ | res, v' -> (res, Var (x, v') :: env'))
+ | Abs _ :: _ -> unimplemented __LOC__*)
+
+(*let rec end_borrow config (env0 : env) (env : env) (l : BorrowId.id) =
+ match env with
+ | [] -> []
+ | Var (x, v) :: env' -> unimplemented __LOC__
+ | Abs _ :: _ -> (
+ match config.mode with
+ | Concrete -> unreachable __LOC__
+ | Symbolic -> unimplemented __LOC__)*)
diff --git a/src/Values.ml b/src/Values.ml
index bab7c9a1..df8ed27d 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -75,7 +75,7 @@ type symbolic_proj_comp = {
type value =
| Concrete of constant_value (** Concrete (non-symbolic) value *)
| Adt of adt_value (** Enumerations and structures *)
- | Tuple of value FieldId.vector
+ | Tuple of typed_value FieldId.vector
(** Tuple - note that units are encoded as 0-tuples *)
| Bottom (** No value (uninitialized or moved value) *)
| Assumed of assumed_value (** Assumed types (Box, Vec, Cell...) *)
@@ -88,12 +88,12 @@ and adt_value = {
variant_id : VariantId.id option;
regions : erased_region list;
types : ety list;
- field_values : value FieldId.vector;
+ field_values : typed_value FieldId.vector;
}
and borrow_content =
| SharedBorrow of BorrowId.id (** A shared value *)
- | MutBorrow of BorrowId.id * value (** A mutably borrowed value *)
+ | MutBorrow of BorrowId.id * typed_value (** A mutably borrowed value *)
| InactivatedMutBorrow of BorrowId.id
(** An inactivated mut borrow.
@@ -107,12 +107,12 @@ and borrow_content =
*)
and loan_content =
- | SharedLoan of BorrowId.Set.t * value
+ | SharedLoan of BorrowId.Set.t * typed_value
| MutLoan of BorrowId.id
-and assumed_value = Box of value
+and assumed_value = Box of typed_value
-type typed_value = { value : value; ty : ety }
+and typed_value = { value : value; ty : ety }
type abstract_shared_borrow =
| AsvSet of BorrowId.Set.t
@@ -129,18 +129,18 @@ type abstract_shared_borrow =
type avalue =
| AConcrete of constant_value
| AAdt of aadt_value
- | ATuple of avalue FieldId.vector
+ | ATuple of typed_avalue FieldId.vector
| ABottom
| AAssumed of aassumed_value
- | AMutBorrow of BorrowId.id * avalue
+ | AMutBorrow of BorrowId.id * typed_avalue
| ASharedBorrow of BorrowId.id
- | AMutLoan of BorrowId.id * avalue
- | ASharedLoan of BorrowId.Set.t * value * avalue
- | AEndedMutLoan of value * avalue (* TODO: given_back, child *)
- | AEndedSharedLoan of value * avalue
- | AIgnoredMutLoan of BorrowId.id * avalue
- | AIgnoredMutBorrow of avalue
- | AEndedIgnoredMutLoan of avalue * avalue (* TODO: given back, child *)
+ | 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
@@ -151,10 +151,12 @@ and aadt_value = {
avariant_id : VariantId.id option;
aregions : erased_region list;
atypes : rty list;
- afield_values : avalue FieldId.vector;
+ afield_values : typed_avalue FieldId.vector;
}
-and aassumed_value = ABox of avalue
+and aassumed_value = ABox of typed_avalue
+
+and typed_avalue = { avalue : avalue; aty : rty }
type abs = {
parents : AbstractionId.Set.t; (** The parent abstraction *)
@@ -162,7 +164,7 @@ type abs = {
(** Union of the regions owned by the (transitive) parent abstractions and
by the current abstraction *)
regions : RegionId.Set.t; (** Regions owned by this abstraction *)
- values : avalue list; (** The values in this abstraction *)
+ values : typed_avalue list; (** The values in this abstraction *)
}
(** Abstractions model the parts in the borrow graph where the borrowing relations
have been abstracted because of a function call.
diff --git a/src/main.ml b/src/main.ml
index b82485b2..9ba76a18 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -1,4 +1,5 @@
open CfimOfJson
+(*open Interpreter*)
let () =
let json = Yojson.Basic.from_file "../charon/charon/tests/test1.cfim" in
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 08:40:22 +0000