From 7372a2fb529df9750b06ccefdbb3f716f9823846 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 26 Jan 2022 09:02:22 +0100
Subject: Replace other occurrences of mvalue with msymbolic_value

---
 src/InterpreterBorrows.ml | 11 +++++++----
 src/SymbolicAstUtils.ml   |  2 +-
 src/Values.ml             | 10 ++++++++--
 3 files changed, 16 insertions(+), 7 deletions(-)

(limited to 'src')

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 6cf2c88f..f87d053c 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -314,8 +314,10 @@ let give_back_value (config : C.config) (bid : V.BorrowId.id)
               match nv.V.value with
               | V.Symbolic sv ->
                   let abs = Option.get opt_abs in
-                  (* Remember the given back value as a meta-value *)
-                  let given_back_meta = nv in
+                  (* Remember the given back value as a meta-value
+                   * TODO: it is a bit annoying to have to deconstruct
+                   * the value... Think about a more elegant way. *)
+                  let given_back_meta = as_symbolic nv.value in
                   (* The loan projector *)
                   let given_back_loans_proj =
                     mk_aproj_loans_value_from_symbolic_value abs.regions sv
@@ -759,14 +761,14 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
     a reference whose region has already ended).
  *)
 let convert_avalue_to_given_back_value (abs_kind : V.abs_kind)
-    (av : V.typed_avalue) : V.typed_value =
+    (av : V.typed_avalue) : V.symbolic_value =
   let sv_kind =
     match abs_kind with
     | V.FunCall -> V.FunCallGivenBack
     | V.SynthRet -> V.SynthRetGivenBack
     | V.SynthInput -> V.SynthInputGivenBack
   in
-  mk_fresh_symbolic_typed_value sv_kind av.V.ty
+  mk_fresh_symbolic_value sv_kind av.V.ty
 
 (** End a borrow identified by its borrow id in a context.
 
@@ -1168,6 +1170,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
             let ended_borrow = V.ABorrow (V.AEndedMutBorrow (v, av)) in
             let ctx = update_aborrow ek_all bid ended_borrow ctx in
             (* Give the value back *)
+            let v = mk_typed_value_from_symbolic_value v in
             give_back_value config bid v ctx
         | V.ASharedBorrow bid ->
             (* Replace the shared borrow with bottom *)
diff --git a/src/SymbolicAstUtils.ml b/src/SymbolicAstUtils.ml
index e74b381f..0f25e6b8 100644
--- a/src/SymbolicAstUtils.ml
+++ b/src/SymbolicAstUtils.ml
@@ -11,7 +11,7 @@ type ('c, 's) ended = EndedConcrete of 'c | EndedSymbolic of 's
 
 type ended_loan = (V.mvalue, V.msymbolic_value list) ended
 
-type ended_borrow = (V.mvalue, V.msymbolic_value) ended
+type ended_borrow = (V.msymbolic_value, V.msymbolic_value) ended
 
 type ended_loan_or_borrow =
   | EndedLoan of ended_loan
diff --git a/src/Values.ml b/src/Values.ml
index 45bd5b6e..90250c63 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -195,12 +195,18 @@ type mvalue = typed_value [@@deriving show]
      Note that we never automatically visit the meta-values with the
      visitors: they really are meta information, and shouldn't be considered
      as part of the environment during a symbolic execution.
+     
+     TODO: we may want to create wrappers, to prevent mixing meta values
+     and regular values.
  *)
 
 type msymbolic_value = symbolic_value [@@deriving show]
 (** "Meta"-symbolic value.
 
      See the explanations for [mvalue]
+
+     TODO: we may want to create wrappers, to prevent mixing meta values
+     and regular values.
  *)
 
 (** When giving shared borrows to functions (i.e., inserting shared borrows inside
@@ -645,7 +651,7 @@ and aborrow_content =
             abstraction so that we can properly call the backward functions
             when generating the pure translation.
        *)
-  | AEndedMutBorrow of mvalue * typed_avalue
+  | AEndedMutBorrow of msymbolic_value * typed_avalue
       (** The sole purpose of [AEndedMutBorrow] is to store the (symbolic) value
           that we gave back as a meta-value, to help with the synthesis.
           We also remember the child [avalue] because this structural information
@@ -656,7 +662,7 @@ and aborrow_content =
   | AEndedIgnoredMutBorrow of {
       child : typed_avalue;
       given_back_loans_proj : typed_avalue;
-      given_back_meta : mvalue;
+      given_back_meta : msymbolic_value;
           (** [given_back_meta] is used to store the (symbolic) value we gave back
               upon ending the borrow.
 
-- 
cgit v1.2.3