diff options
Diffstat (limited to '')
| -rw-r--r-- | src/Interpreter.ml | 62 |
1 files changed, 49 insertions, 13 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml index ecb38757..52e744ac 100644 --- a/src/Interpreter.ml +++ b/src/Interpreter.ml @@ -547,7 +547,11 @@ let activate_inactivated_mut_borrow (config : config) (io : inner_outer) (** Paths *) -type access_kind = Read | Write +type access_kind = + | Read (** Read a value *) + | Write + (** Update a value (but don't replace it with [Bottom] or values containing [Bottom] *) + | Move (** Replace a value with [Bottom] *) (** 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 @@ -625,7 +629,8 @@ let rec read_projection (config : config) (access : access_kind) (env : env) 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) + | (Write | Move), SharedLoan (bids, _) -> + Error (FailSharedLoan bids) (* We always have to end mutable loans *) | _, MutLoan bid -> Error (FailMutLoan bid)) | _ -> Ok v @@ -666,8 +671,11 @@ let rec read_projection (config : config) (access : access_kind) (env : env) | Read, SharedBorrow bid -> let sv = lookup_shared_value_from_borrow_id bid env in read_projection config access env p' sv - | Write, SharedBorrow _ -> failwith "Unreachable" - | _, MutBorrow (_, bv) -> read_projection config access env p' bv + | Write, SharedBorrow _ -> + failwith "Can't write to a shared borrow" + | (Read | Write), MutBorrow (_, bv) -> + read_projection config access env p' bv + | Move, _ -> failwith "Can't move out of a borrow" (* We need to activate inactivated mutable borrows *) | _, InactivatedMutBorrow bid -> Error (FailInactivatedMutBorrow bid)) @@ -692,7 +700,7 @@ let read_place (config : config) (access : access_kind) (p : place) (env0 : env) in read_in_env env0 -(** Update the value at the end of a projection *) +(** Update the value at the end of a projection. *) let rec write_projection (config : config) (new_value : typed_value) (p : projection) (v : typed_value) : typed_value path_access_result = match p with @@ -766,7 +774,11 @@ let rec write_projection (config : config) (new_value : typed_value) | _, (Concrete _ | Adt _ | Tuple _ | Bottom | Assumed _ | Borrow _) -> failwith "Unreachable") -(** Update the value at the end of a place *) +(** Update the value at the end of a place. + + We don't specify the access kind, because it should have been specified in + a prior access check with [read_place]. + *) let write_place (config : config) (nv : typed_value) (p : place) (env0 : env) : env path_access_result = let rec write_in_env env : env path_access_result = @@ -884,10 +896,10 @@ let expand_bottom_value (config : config) (tyctx : type_def TypeDefId.vector) expanding symbolic values) until we manage to fully read the place. *) let rec update_env_along_read_place (config : config) (access : access_kind) - (p : place) (env : env) : env * typed_value = + (p : place) (env : env) : env = (* Attempt to read the place: if it fails, update the environment and retry *) match read_place config access p env with - | Ok v -> (env, v) + | Ok _ -> env | Error err -> let env' = match err with @@ -1219,12 +1231,36 @@ let constant_value_to_typed_value (ctx : eval_ctx) (ty : ety) (*let eval_operand (config : config) (ctx : eval_ctx) (op : operand) : eval_ctx * typed_value = match op with - | Constant (ty, cv) -> + | Expressions.Constant (ty, cv) -> let v = constant_value_to_typed_value ctx ty cv in (ctx, v) - | Copy p -> - let ctx' = - | Move p -> () - + | Expressions.Copy p -> ( + (* Access the value *) + let access = Read in + let env1 = update_env_along_read_place config access p ctx.env in + let env2 = collect_borrows_at_place config access p env1 in + match read_place config access p env2 with + | Err _ -> failwith "Unreachable" + | Ok v -> + (* Copy the value *) + assert (not (bottom_in_value v)); + let ctx2 = { ctx with env = env2 } in + copy_value config ctx2 v) + | Expressions.Move p -> ( + (* Access the value *) + let access = Move in + let env1 = update_env_along_read_place config access p ctx.env in + let env2 = collect_borrows_at_place config access p env1 in + match read_place config access p env2 with + | Err _ -> failwith "Unreachable" + | Ok v -> + (* Move the value *) + assert (not (bottom_in_value v)); + let bottom = { value = Bottom; ty = v.ty } in + let env3 = write_place config bottom p env2 in + let ctx3 = { ctx with env = env3 } in + (ctx3, v))*) + +(* let rec update_env_along_read_place (config : config) (access : access_kind) (p : place) (env : env) : typed_value * env =*) |