From ad52adcc6960693b407af5981f873be16e60f497 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 25 Jan 2022 23:22:56 +0100
Subject: Make good progress on typed_avalue_to_consumed

---
 src/SymbolicToPure.ml | 70 +++++++++++++++++++++++++++++++++++----------------
 1 file changed, 49 insertions(+), 21 deletions(-)

diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 4dfe00c7..42214c8c 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -552,6 +552,8 @@ let get_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
     
     TODO: we have a problem with shared borrows. I think the shared borrows
     should carry the shared value as a meta-value.
+    
+    TODO: rename: remove the "translate_" prefix
  *)
 let rec translate_typed_value_to_rvalue (ctx : bs_ctx) (v : V.typed_value) :
     typed_rvalue =
@@ -592,13 +594,51 @@ let rec typed_avalue_to_consumed (ctx : bs_ctx) (av : V.typed_avalue) :
     | AConcrete _ -> failwith "Unreachable"
     | AAdt av -> raise Unimplemented
     | ABottom -> raise Unimplemented
-    | ALoan lc -> raise Unimplemented
-    | ABorrow bc -> raise Unimplemented
-    | ASymbolic aproj -> raise Unimplemented
+    | ALoan lc -> aloan_content_to_consumed ctx lc
+    | ABorrow bc -> aborrow_content_to_consumed ctx bc
+    | ASymbolic aproj -> aproj_to_consumed ctx aproj
     | AIgnored -> None
   in
   raise Unimplemented
 
+and aloan_content_to_consumed (ctx : bs_ctx) (lc : V.aloan_content) :
+    typed_rvalue option =
+  match lc with
+  | AMutLoan (_, _) | ASharedLoan (_, _, _) -> failwith "Unreachable"
+  | AEndedMutLoan { child = _; given_back = _; given_back_meta } ->
+      (* Return the meta-value *)
+      Some (translate_typed_value_to_rvalue ctx given_back_meta)
+  | AEndedSharedLoan (_, _) ->
+      (* We don't dive into shared loans: there is nothing to give back
+       * inside (note that there could be a mutable borrow in the shared
+       * value, pointing to a mutable loan in the child avalue, but this
+       * borrow is in practice immutable) *)
+      None
+  | AIgnoredMutLoan (_, _) ->
+      (* There can be *inner* mutable loans, but not outer ones *)
+      failwith "Unreachable"
+  | AEndedIgnoredMutLoan _ ->
+      (* This happens with nested borrows: we need to dive in *)
+      raise Unimplemented
+  | AIgnoredSharedLoan _ ->
+      (* Ignore *)
+      None
+
+and aborrow_content_to_consumed (ctx : bs_ctx) (bc : V.aborrow_content) :
+    typed_rvalue option =
+  match bc with
+  | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) ->
+      failwith "Unreachable"
+  | AEndedMutBorrow (mv, _) ->
+      (* Return the meta-value *)
+      Some (translate_typed_value_to_rvalue ctx mv)
+  | AEndedIgnoredMutBorrow _ ->
+      (* This happens with nested borrows: we need to dive in *)
+      raise Unimplemented
+  | AProjSharedBorrow _ ->
+      (* Ignore *)
+      None
+
 and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : typed_rvalue option =
   let translate = aproj_to_consumed ctx in
   match aproj with
@@ -606,30 +646,18 @@ and aproj_to_consumed (ctx : bs_ctx) (aproj : V.aproj) : typed_rvalue option =
       (* The symbolic value was left unchanged *)
       let var = get_var_for_symbolic_value msv ctx in
       Some (mk_typed_rvalue_from_var var)
-  | V.AEndedProjLoans (_, [ (mnv, AIgnoredProjBorrows) ]) ->
+  | V.AEndedProjLoans (_, [ (mnv, child_aproj) ]) ->
+      assert (child_aproj = AIgnoredProjBorrows);
       (* The symbolic value was updated *)
       let var = get_var_for_symbolic_value mnv ctx in
       Some (mk_typed_rvalue_from_var var)
-  | AEndedProjBorrows _ -> (* We consider consumed values *) None
-  | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
-      failwith "Unreachable"
-
-(*
   | V.AEndedProjLoans (_, _) ->
-      (* The symbolic value was through values given back by several abstractions *)
+      (* The symbolic value was updated, and the given back values come from sevearl
+       * abstractions *)
       raise Unimplemented
-  | V.AEndedSharedLoan (_, _) ->
-      (* Shared loans don't consume anything *)
-      None
-  | AIgnoredMutLoan (_, _) ->
-      (* There can be *inner* mutable loans, but not outer ones *)
+  | AEndedProjBorrows _ -> (* We consider consumed values *) None
+  | AIgnoredProjBorrows | AProjLoans (_, _) | AProjBorrows (_, _) ->
       failwith "Unreachable"
-  | AEndedIgnoredMutLoan { child = _; given_back = _; given_back_meta = _ } ->
-      (* No nested borrows for now *)
-      raise Unimplemented
-  | AIgnoredSharedLoan _ ->
-      (* Ignore *)
-None*)
 
 let abs_to_consumed (ctx : bs_ctx) (abs : V.abs) : typed_rvalue list =
   List.filter_map (typed_avalue_to_consumed ctx) abs.avalues
-- 
cgit v1.2.3