summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Identifiers.ml4
-rw-r--r--src/Interpreter.ml146
2 files changed, 80 insertions, 70 deletions
diff --git a/src/Identifiers.ml b/src/Identifiers.ml
index e75099d6..9b125161 100644
--- a/src/Identifiers.ml
+++ b/src/Identifiers.ml
@@ -23,6 +23,8 @@ module type Id = sig
val vector_of_list : 'a list -> 'a vector
+ val nth : 'a vector -> id -> 'a
+
val nth_opt : 'a vector -> id -> 'a option
val update_nth : 'a vector -> id -> 'a -> 'a vector
@@ -65,6 +67,8 @@ module IdGen () : Id = struct
let vector_of_list v = v
+ let nth v id = List.nth v id
+
let nth_opt v id = List.nth_opt v id
let rec update_nth vec id v =
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 5cba4908..062c8214 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -117,14 +117,9 @@ let rec end_borrow_get_borrow_in_env (config : config) l env0 :
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 _ :: _ -> (
- match config.mode with
- | ConcreteMode ->
- (* There can't be abstractions if we run in concrete mode *)
- failwith "Unreachable"
- | SymbolicMode ->
- (* TODO *)
- raise Unimplemented)
+ | Abs _ :: _ ->
+ assert (config.mode = SymbolicMode);
+ raise Unimplemented
let rec give_back_value_to_value config bid (v : typed_value)
(destv : typed_value) : typed_value =
@@ -173,10 +168,9 @@ let give_back_value_to_abs (_config : config) _bid _v _abs : abs =
let give_back_value_to_env_value config bid v ev : env_value =
match ev with
| Var (vid, destv) -> Var (vid, give_back_value_to_value config bid v destv)
- | Abs abs -> (
- match config.mode with
- | ConcreteMode -> failwith "Unreachable"
- | SymbolicMode -> Abs (give_back_value_to_abs config bid v abs))
+ | Abs abs ->
+ assert (config.mode = SymbolicMode);
+ Abs (give_back_value_to_abs config bid v abs)
let rec give_back_shared_to_value (config : config) bid (destv : typed_value) :
typed_value =
@@ -237,13 +231,13 @@ let give_back_shared_to_abs _config _bid _abs : abs =
(* TODO *)
raise Unimplemented
+(* TODO: merge this in the other functions *)
let give_back_shared_to_env_value (config : config) bid ev : env_value =
match ev with
| Var (vid, destv) -> Var (vid, give_back_shared_to_value config bid destv)
- | Abs abs -> (
- match config.mode with
- | ConcreteMode -> failwith "Unreachable"
- | SymbolicMode -> Abs (give_back_shared_to_abs config bid abs))
+ | Abs abs ->
+ assert (config.mode = SymbolicMode);
+ Abs (give_back_shared_to_abs config bid abs)
let give_back_value (config : config) (bid : BorrowId.id) (v : typed_value)
(env : env) : env =
@@ -262,10 +256,9 @@ let rec end_borrow (config : config) (l : BorrowId.id) (env0 : env) : env =
match end_borrow_get_borrow_in_env config l env0 with
(* It is possible that we can't find a borrow in symbolic mode (ending
* an abstraction may end several borrows at once *)
- | NotFound, env -> (
- match config.mode with
- | ConcreteMode -> failwith "Unreachable"
- | SymbolicMode -> env)
+ | NotFound, env ->
+ assert (config.mode = SymbolicMode);
+ env
(* If we found outer borrows: end those borrows first *)
| Outer outer_borrows, env ->
let env' =
@@ -309,10 +302,9 @@ let lookup_loan_in_env_value (config : config) (l : BorrowId.id)
(ev : env_value) : loan_content option =
match ev with
| Var (_, v) -> lookup_loan_in_value config l v
- | Abs _ -> (
- match config.mode with
- | ConcreteMode -> failwith "Unreachable"
- | SymbolicMode -> None)
+ | Abs _ ->
+ assert (config.mode = SymbolicMode);
+ None
(** Lookup a loan content from a borrow id.
Note that we never lookup loans in the abstractions.
@@ -393,10 +385,9 @@ let promote_shared_loan_to_mut_loan (config : config) (l : BorrowId.id)
| Some (borrowed, new_v) -> (borrowed, Var (vid, new_v) :: env))
| Abs abs :: env ->
(* We don't promote inside abstractions *)
- if config.mode = ConcreteMode then failwith "Unreachable"
- else
- let borrowed, env' = promote_in_env env in
- (borrowed, Abs abs :: env')
+ assert (config.mode = SymbolicMode);
+ let borrowed, env' = promote_in_env env in
+ (borrowed, Abs abs :: env')
in
(* Apply *)
promote_in_env env0
@@ -432,7 +423,8 @@ let promote_inactivated_borrow_to_mut_borrow (config : config) (l : BorrowId.id)
match ev with
| Var (name, v) -> Var (name, promote_in_value v)
| Abs abs ->
- if config.mode = ConcreteMode then failwith "Unreachable" else Abs abs
+ assert (config.mode = SymbolicMode);
+ Abs abs
in
List.map promote_in_env_value env0
@@ -546,7 +538,7 @@ let rec read_projection (config : config) (access : path_access) (env : env)
(* 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 -> (
+ | 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 -> ()
@@ -554,18 +546,14 @@ let rec read_projection (config : config) (access : path_access) (env : env)
if vid <> vid' then failwith "Unreachable"
| _ -> failwith "Unreachable");
(* Actually project *)
- match FieldId.nth_opt adt.field_values field_id with
- | None -> failwith "Unreachable"
- | Some fv -> read_projection config access env p fv)
+ let fv = FieldId.nth adt.field_values field_id in
+ read_projection config access env p fv
(* Tuples *)
- | Field (ProjTuple _, field_id), Tuple values -> (
- match FieldId.nth_opt values field_id with
- | None -> failwith "Unreachable"
- | Some fv -> read_projection config access env p fv)
- (* 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))
+ | Field (ProjTuple _, field_id), Tuple values ->
+ let fv = FieldId.nth values field_id in
+ read_projection config access env p fv
+ (* We can expand [Bottom] values only while *writing* to places *)
+ | _, Bottom -> failwith "Unreachable"
(* Symbolic value: needs to be expanded *)
| _, Symbolic sp ->
assert (config.mode = SymbolicMode);
@@ -588,9 +576,7 @@ let rec read_projection (config : config) (access : path_access) (env : env)
(* Remaining cases: error. We enumerate all the value variants
* on purpose, to make sure we statically catch errors if we
* modify the [value] definition. *)
- | ( _,
- ( Concrete _ | Adt _ | Tuple _ | Bottom | Assumed _ | Borrow _
- | Loan _ ) ) ->
+ | _, (Concrete _ | Adt _ | Tuple _ | Assumed _ | Borrow _ | Loan _) ->
failwith "Unreachable")
(* Entering loans failed *)
| res -> res)
@@ -624,33 +610,27 @@ let rec write_projection (config : config) (new_value : typed_value)
| Some vid, Some vid' -> if vid <> vid' then failwith "Unreachable"
| _ -> failwith "Unreachable");
(* Actually project *)
- match FieldId.nth_opt adt.field_values field_id with
- | None -> failwith "Unreachable"
- | Some fv -> (
- (* Update the field value *)
- match write_projection config new_value p fv with
- | Error err -> Error err
- | Ok nfv ->
- (* Reinsert the field value *)
- let nvalues =
- FieldId.update_nth adt.field_values field_id nfv
- in
- let nadt = Adt { adt with field_values = nvalues } in
- Ok { v with value = nadt }))
+ let fv = FieldId.nth adt.field_values field_id in
+ (* Update the field value *)
+ match write_projection config new_value p fv with
+ | Error err -> Error err
+ | Ok nfv ->
+ (* Reinsert the field value *)
+ let nvalues = FieldId.update_nth adt.field_values field_id nfv in
+ let nadt = Adt { adt with field_values = nvalues } in
+ Ok { v with value = nadt })
(* Tuples *)
| Field (ProjTuple _, field_id), Tuple values -> (
(* Project *)
- match FieldId.nth_opt values field_id with
- | None -> failwith "Unreachable"
- | Some fv -> (
- (* Update the field value *)
- match write_projection config new_value p fv with
- | Error err -> Error err
- | Ok nfv ->
- (* Reinsert the field value *)
- let nvalues = FieldId.update_nth values field_id nfv in
- let ntuple = Tuple nvalues in
- Ok { v with value = ntuple }))
+ let fv = FieldId.nth values field_id in
+ (* Update the field value *)
+ match write_projection config new_value p fv with
+ | Error err -> Error err
+ | Ok nfv ->
+ (* Reinsert the field value *)
+ let nvalues = FieldId.update_nth values field_id nfv in
+ let ntuple = Tuple nvalues in
+ Ok { v with value = ntuple })
(* If we reach Bottom, it may mean we need to expand an uninitialized
* enumeration value *)
| Field (ProjAdt (_, Some _variant_id), _), Bottom ->
@@ -710,6 +690,32 @@ let write_place (config : config) (nv : typed_value) (p : place) (env0 : env) :
in
write_in_env env0
+(** Auxiliary function to expand [Bottom] values
+
+ During compilation, rustc desaggregates the ADT initializations. The
+ consequence is that the following rust code:
+ ```
+ let x = Cons a b;
+ ```
+
+ Looks like this in MIR:
+ ```
+ (x as Cons).0 = a;
+ (x as Cons).1 = b;
+ set_discriminant(x, 0); // If `Cons` is the variant of index 0
+ ```
+
+ The consequence is that we may sometimes need to write fields to values
+ which are currently [Bottom]. When doing this, we first expand the value
+ to, say, [Cons Bottom Bottom] (note that field projection contains information
+ about which variant we should project to, which is why we *can* set the
+ variant index when writing one of its fields).
+*)
+(*let expand_bottom_value (config : config) (tyctx : type_def TypeDefId.vector)
+ (p : place) (env : env) (remaining_pes : int) (pe : projection_elem)
+ (ty : ety) : env =
+ let *)
+
(** Update the environment to be able to read a place.
When reading a place, we may be stuck along the way because some value
@@ -734,7 +740,7 @@ let rec update_env_along_read_place (config : config) (access : path_access)
(* Expand the symbolic value *)
raise Unimplemented
| FailBottom (remaining_pes, pe, ty) ->
- (* Expand the "bottom" value, if possible *)
- raise Unimplemented
+ (* We can't expand [Bottom] values while reading them *)
+ failwith "Unreachable"
in
update_env_along_read_place config access p env'