diff options
| -rw-r--r-- | src/Errors.ml | 4 | ||||
| -rw-r--r-- | src/Identifiers.ml | 8 | ||||
| -rw-r--r-- | src/Interpreter.ml | 112 | ||||
| -rw-r--r-- | src/Values.ml | 38 | ||||
| -rw-r--r-- | src/main.ml | 1 |
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 |