summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-22 19:52:49 +0100
committerSon Ho2021-11-22 19:52:49 +0100
commit115960297c2f9cf839d51232dd2961e0d4817657 (patch)
treea1d05c1f1692e5c8230cca18c49641e297dbbbc6
parent402a5405f5e622cd09b6dafbe630bc4348ebe681 (diff)
Make progress on {read,write}_path
Diffstat (limited to '')
-rw-r--r--src/CfimOfJson.ml3
-rw-r--r--src/Errors.ml1
-rw-r--r--src/Expressions.ml1
-rw-r--r--src/Identifiers.ml4
-rw-r--r--src/Interpreter.ml174
5 files changed, 148 insertions, 35 deletions
diff --git a/src/CfimOfJson.ml b/src/CfimOfJson.ml
index 5455c487..cc7b5603 100644
--- a/src/CfimOfJson.ml
+++ b/src/CfimOfJson.ml
@@ -273,9 +273,6 @@ let projection_elem_of_json (js : json) : (projection_elem, string) result =
let* proj_kind = field_proj_kind_of_json proj_kind in
let* field_id = FieldId.id_of_json field_id in
Ok (Field (proj_kind, field_id))
- | `Assoc [ ("Downcast", variant_id) ] ->
- let* variant_id = VariantId.id_of_json variant_id in
- Ok (Downcast variant_id)
| _ -> Error ("projection_elem_of_json failed on:" ^ show js))
let projection_of_json (js : json) : (projection, string) result =
diff --git a/src/Errors.ml b/src/Errors.ml
index b9263d5a..d732e1f3 100644
--- a/src/Errors.ml
+++ b/src/Errors.ml
@@ -1,5 +1,6 @@
exception IntegerOverflow of unit
+(* TODO: remove those *)
exception Unimplemented of string
let unimplemented msg = raise (Unimplemented ("unimplemented: " ^ msg))
diff --git a/src/Expressions.ml b/src/Expressions.ml
index 66cf5197..c0ee90a9 100644
--- a/src/Expressions.ml
+++ b/src/Expressions.ml
@@ -9,7 +9,6 @@ type projection_elem =
| Deref
| DerefBox
| Field of field_proj_kind * FieldId.id
- | Downcast of VariantId.id
type projection = projection_elem list
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index 51a22072..04c5427b 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -21,6 +21,8 @@ module type Id = sig
val vector_of_list : 'a list -> 'a vector
+ val nth_opt : 'a vector -> id -> 'a option
+
module Set : Set.S with type elt = id
val set_to_string : Set.t -> string
@@ -59,6 +61,8 @@ module IdGen () : Id = struct
let vector_of_list v = v
+ let nth_opt v id = List.nth_opt v id
+
module Set = Set.Make (struct
type t = id
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 5675a4f0..ff19b3f6 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -20,7 +20,7 @@ let env_to_string (fmt : value_formatter) (env : env) : string =
(List.map (fun ev -> " " ^ env_value_to_string fmt ev) env)
^ "\n}"
-type 'a result = Stuck | Panic | Res of 'a
+type 'a eval_result = Stuck | Panic | Res of 'a
type interpreter_mode = ConcreteMode | SymbolicMode
@@ -460,18 +460,33 @@ let activate_inactivated_mut_borrow (config : config) (l : BorrowId.id)
type path_access = Read | Write
-(** The result of reading from/writing to a place *)
-type 'a path_access_result =
- | Success of 'a (** Success *)
- | SharedLoan of BorrowId.Set.t
+(** When we fail reading from or writing to a path, it might be because we
+ ** need to update the environment by ending borrows, expanding symbolic
+ ** values, etc. *)
+type path_fail_kind =
+ | FailSharedLoan of BorrowId.Set.t
(** Failure because we couldn't go inside a shared loan *)
- | MutLoan of BorrowId.id
+ | FailMutLoan of BorrowId.id
(** Failure because we couldn't go inside a mutable loan *)
- | InactivatedMutBorrow of BorrowId.id
+ | FailInactivatedMutBorrow of BorrowId.id
(** Failure because we couldn't go inside an inactivated mutable borrow
(which should get activated) *)
- | Failed
- (** Failure for another reason (ex.: couldn't go inside a shared borrow... *)
+ | FailSymbolic of (projection_elem * symbolic_proj_comp)
+ (** Failure because we need to enter a symbolic value (and thus need to expand it) *)
+ | FailBottom of (int * projection_elem * ety)
+ (** Failure because we need to enter an any value - we can expand Bottom
+ values if they are left values. We return the number of elements which
+ were remaining in the path when we reached the error - this allows to
+ properly update the Bottom value, if needs be.
+ *)
+
+(** Result of evaluating a path (reading from a path/writing to a path)
+
+ Note that when we fail, we return information used to update the
+ environment, as well as the
+*)
+type 'a path_access_result = ('a, path_fail_kind) result
+(** The result of reading from/writing to a place *)
let lookup_shared_value_from_borrow_id (bid : BorrowId.id) (env : env) :
typed_value =
@@ -510,6 +525,90 @@ let lookup_shared_value_from_borrow_id (bid : BorrowId.id) (env : env) :
let rec read_projection (config : config) (access : path_access) (env : env)
(p : projection) (v : typed_value) : typed_value path_access_result =
match p with
+ | [] -> Ok v
+ | pe :: p' -> (
+ (* The projection is non-empty: we need to enter all the loans we find,
+ * if we are allowed to do so *)
+ let rec enter_loans (v : typed_value) : typed_value path_access_result =
+ match v.value with
+ | Loan lc -> (
+ match (access, lc) with
+ (* We can enter shared loans only if we are in "read" mode *)
+ | Read, SharedLoan (_, sv) -> enter_loans sv
+ | Write, SharedLoan (bids, _) -> Error (FailSharedLoan bids)
+ (* We can always enter mutable loans *)
+ | _, MutLoan bid -> Error (FailMutLoan bid))
+ | _ -> Ok v
+ in
+ (* Enter inside the loans and match on the resulting value *)
+ match enter_loans v with
+ | Ok v -> (
+ (* Match on the projection element and the value *)
+ match (pe, v.value) with
+ (* Field projection *)
+ | Field (ProjAdt (_def_id, opt_variant_id), field_id), Adt adt -> (
+ (* Check that the projection is consistent with the current value *)
+ (match (opt_variant_id, adt.variant_id) with
+ | None, None -> ()
+ | Some vid, Some vid' -> if vid <> vid' then unreachable __LOC__
+ | _ -> unreachable __LOC__);
+ (* Actually project *)
+ match FieldId.nth_opt adt.field_values field_id with
+ | None -> unreachable __LOC__
+ | Some fv -> read_projection config access env p fv)
+ | _, Adt _ -> unreachable __LOC__
+ (* Tuples *)
+ | Field (ProjTuple _, field_id), Tuple values -> (
+ match FieldId.nth_opt values field_id with
+ | None -> unreachable __LOC__
+ | Some fv -> read_projection config access env p fv)
+ | _, Tuple _ -> unreachable __LOC__
+ (* If we reach Bottom, it may mean we need to expand an uninitialized
+ * enumeration value *)
+ | Field (ProjAdt (_, Some _variant_id), _), Bottom ->
+ Error (FailBottom (1 + List.length p', pe, v.ty))
+ | _, Bottom -> unreachable __LOC__
+ (* Symbolic value: needs to be expanded *)
+ | _, Symbolic sp ->
+ assert (config.mode = SymbolicMode);
+ (* Expand the symbolic value *)
+ Error (FailSymbolic (pe, sp))
+ (* Box dereferencement *)
+ | DerefBox, Assumed (Box bv) ->
+ read_projection config access env p' bv
+ (* Borrow dereferencement *)
+ | Deref, Borrow bc -> (
+ match (access, bc) with
+ | Read, SharedBorrow bid ->
+ let sv = lookup_shared_value_from_borrow_id bid env in
+ read_projection config access env p' sv
+ | Write, SharedBorrow _ -> unreachable __LOC__
+ | _, MutBorrow (_, bv) -> read_projection config access env p' bv
+ | _, InactivatedMutBorrow bid ->
+ Error (FailInactivatedMutBorrow bid))
+ | _, (Concrete _ | Assumed _ | Borrow _ | Loan _) ->
+ unreachable __LOC__)
+ (* Entering loans failed *)
+ | res -> res)
+
+(*
+(** Read the value at the end of a place *)
+let read_place (config : config) (access : path_access) (p : place) (env0 : env)
+ : typed_value path_access_result =
+ let rec read_in_env env : typed_value path_access_result =
+ match env with
+ | [] -> unreachable __LOC__
+ | Var (vid, v) :: env' ->
+ if vid = p.var_id then read_projection config access env0 p.projection v
+ else read_in_env env'
+ | Abs _ :: env' -> read_in_env env'
+ in
+ read_in_env env0
+
+(** Update the value at the end of a projection *)
+let rec write_projection (config : config) (nv : typed_value) (p : projection)
+ (v : typed_value) : typed_value path_access_result =
+ match p with
| [] -> Success v
| pe :: p' -> (
match (pe, v.value) with
@@ -521,32 +620,45 @@ let rec read_projection (config : config) (access : path_access) (env : env)
(* Expand the symbolic value *)
(* TODO *)
unimplemented __LOC__)
- | DerefBox, Assumed (Box bv) -> read_projection config access env p' bv
+ | DerefBox, Assumed (Box bv) -> (
+ match write_projection config p' bv with
+ | Success bv' ->
+ Success
+ { v with value = Assumed (Box (write_projection config p' bv)) }
+ | res -> res)
| Deref, Borrow bc -> (
- match (access, bc) with
- | Read, SharedBorrow bid ->
- let sv = lookup_shared_value_from_borrow_id bid env in
- read_projection config access env p' sv
- | Write, SharedBorrow _ -> Failed
- | _, MutBorrow (_, bv) -> read_projection config access env p' bv
- | _, InactivatedMutBorrow bid -> InactivatedMutBorrow bid)
+ match bc with
+ | SharedBorrow _ -> Failed
+ | MutBorrow (bid, bv) -> (
+ match write_projection config p' bv with
+ | Success bv' -> Success (Borrow (MutBorrow (bid, bv')))
+ | res -> res)
+ | InactivatedMutBorrow bid -> InactivatedMutBorrow bid)
| _, Loan lc -> (
- match (access, lc) with
- | Read, SharedLoan (_, sv) ->
- read_projection config access env (pe :: p') sv
- | Write, SharedLoan (bids, _) -> SharedLoan bids
- | _, MutLoan bid -> MutLoan bid)
+ match lc with
+ | SharedLoan (bids, _) -> SharedLoan bids
+ | MutLoan bid -> MutLoan bid)
| _ -> unreachable __LOC__)
-(** Read the value at the end of a place *)
-let read_place (config : config) (access : path_access) (p : place) (env0 : env)
- : typed_value path_access_result =
- let rec read_in_env env : typed_value path_access_result =
+(** Update the value at the end of a place *)
+let write_place (config : config) (p : place) (env0 : env) :
+ env path_access_result =
+ let rec write_in_env env : env path_access_result =
match env with
| [] -> unreachable __LOC__
- | Var (vid, v) :: env' ->
- if vid = p.var_id then read_projection config access env0 p.projection v
- else read_in_env env'
- | Abs _ :: env' -> read_in_env env'
+ | Var (vid, v) :: env' -> (
+ if vid = p.var_id then
+ match write_projection config access p.projection v with
+ | Success nv -> Var (vid, nv) :: env'
+ | res -> res
+ else
+ match write_in_env env' with
+ | Success env'' -> Success (Var (vid v) :: env'')
+ | res -> res)
+ | Abs abs :: env' -> (
+ match write_in_env env' with
+ | Success env'' -> Success (Abs abs :: env'')
+ | res -> res)
in
- read_in_env env0
+ write_in_env env0
+ *)