Make progress on {read,write}_path

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
+ *)