summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-11-23 09:35:12 +0100
committerSon Ho2021-11-23 09:35:12 +0100
commitd145f46b141a8d7cc66372693bc68691af34c8cf (patch)
treeacc1f8612df6793cf6f7ab599025cc1d1760cdb4
parent7ff59a3ff5daae9e88e9ff15f8a3452536c94628 (diff)
Start implementing update_env_along_read_place
-rw-r--r--src/Interpreter.ml29
1 files changed, 29 insertions, 0 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 8ed1a68c..5cba4908 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -709,3 +709,32 @@ let write_place (config : config) (nv : typed_value) (p : place) (env0 : env) :
| res -> res)
in
write_in_env env0
+
+(** Update the environment to be able to read a place.
+
+ When reading a place, we may be stuck along the way because some value
+ is borrowed, we reach a symbolic value, etc. In this situation [read_place]
+ fails while returning precise information about the failure. This function
+ uses this information to update the environment (by ending borrows,
+ expanding symbolic values) until we manage to fully read the place.
+ *)
+let rec update_env_along_read_place (config : config) (access : path_access)
+ (p : place) (env : env) : typed_value * env =
+ (* Attempt to read the place: if it fails, update the environment and retry *)
+ match read_place config access p env with
+ | Ok v -> (v, env)
+ | Error err ->
+ let env' =
+ match err with
+ | FailSharedLoan bids -> end_borrows config bids env
+ | FailMutLoan bid -> end_borrow config bid env
+ | FailInactivatedMutBorrow bid ->
+ activate_inactivated_mut_borrow config bid env
+ | FailSymbolic (pe, sp) ->
+ (* Expand the symbolic value *)
+ raise Unimplemented
+ | FailBottom (remaining_pes, pe, ty) ->
+ (* Expand the "bottom" value, if possible *)
+ raise Unimplemented
+ in
+ update_env_along_read_place config access p env'