Add sv_kind ("symbolic value kind") to track the origin of the symbolic

values

7 files changed, 65 insertions, 30 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 2f0f52af..8cab8c47 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -67,7 +67,9 @@ module Test = struct
     let ctx, inst_sg = instantiate_fun_sig type_params sg ctx in
     (* Create fresh symbolic values for the inputs *)
     let input_svs =
-      List.map (fun ty -> mk_fresh_symbolic_value ty) inst_sg.inputs
+      List.map
+        (fun ty -> mk_fresh_symbolic_value V.SynthInput ty)
+        inst_sg.inputs
     in
     (* Initialize the abstractions as empty (i.e., with no avalues) abstractions *)
     let empty_absl =
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index faa63c0a..9d332543 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -746,8 +746,8 @@ let give_back (config : C.config) (l : V.BorrowId.id) (bc : g_borrow_content)
     be expanded (because expanding this symbolic value would require expanding
     a reference whose region has already ended).
  *)
-let convert_avalue_to_value (av : V.typed_avalue) : V.typed_value =
-  mk_fresh_symbolic_typed_value av.V.ty
+let convert_avalue_to_given_back_value (av : V.typed_avalue) : V.typed_value =
+  mk_fresh_symbolic_typed_value V.FunCallGivenBack av.V.ty
 
 (** End a borrow identified by its borrow id in a context
     
@@ -1129,7 +1129,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
         match bc with
         | V.AMutBorrow (bid, av) ->
             (* First, convert the avalue to a (fresh symbolic) value *)
-            let v = convert_avalue_to_value av in
+            let v = convert_avalue_to_given_back_value av in
             give_back_value config bid v ctx
         | V.ASharedBorrow bid -> give_back_shared config bid ctx
         | V.AProjSharedBorrow _ ->
@@ -1148,7 +1148,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
           V.AEndedProjBorrows ctx
       in
       (* Give back a fresh symbolic value *)
-      let nsv = mk_fresh_symbolic_value proj_ty in
+      let nsv = mk_fresh_symbolic_value V.FunCallGivenBack proj_ty in
       let ctx =
         give_back_symbolic_value config abs.regions proj_ty sv nsv ctx
       in
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 8f560083..8b039510 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -217,8 +217,9 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
     doesn't allow the expansion of enumerations *containing several variants*.
  *)
 let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
-    (def_id : T.TypeDefId.id) (regions : T.RegionId.id T.region list)
-    (types : T.rty list) (ctx : C.eval_ctx) : symbolic_expansion list =
+    (kind : V.sv_kind) (def_id : T.TypeDefId.id)
+    (regions : T.RegionId.id T.region list) (types : T.rty list)
+    (ctx : C.eval_ctx) : symbolic_expansion list =
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
   let def = C.ctx_lookup_type_def ctx def_id in
@@ -235,7 +236,7 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
       ((variant_id, field_types) : T.VariantId.id option * T.rty list) :
       symbolic_expansion =
     let field_values =
-      List.map (fun (ty : T.rty) -> mk_fresh_symbolic_value ty) field_types
+      List.map (fun (ty : T.rty) -> mk_fresh_symbolic_value kind ty) field_types
     in
     let see = SeAdt (variant_id, field_values) in
     see
@@ -243,20 +244,20 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
   (* Initialize all the expanded values of all the variants *)
   List.map initialize variants_fields_types
 
-let compute_expanded_symbolic_tuple_value (field_types : T.rty list) :
-    symbolic_expansion =
+let compute_expanded_symbolic_tuple_value (kind : V.sv_kind)
+    (field_types : T.rty list) : symbolic_expansion =
   (* Generate the field values *)
   let field_values =
-    List.map (fun sv_ty -> mk_fresh_symbolic_value sv_ty) field_types
+    List.map (fun sv_ty -> mk_fresh_symbolic_value kind sv_ty) field_types
   in
   let variant_id = None in
   let see = SeAdt (variant_id, field_values) in
   see
 
-let compute_expanded_symbolic_box_value (boxed_ty : T.rty) : symbolic_expansion
-    =
+let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) :
+    symbolic_expansion =
   (* Introduce a fresh symbolic value *)
-  let boxed_value = mk_fresh_symbolic_value boxed_ty in
+  let boxed_value = mk_fresh_symbolic_value kind boxed_ty in
   let see = SeAdt (None, [ boxed_value ]) in
   see
 
@@ -360,7 +361,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
   (* Finally, replace the projectors on loans *)
   let bids = !borrows in
   assert (not (V.BorrowId.Set.is_empty bids));
-  let shared_sv = mk_fresh_symbolic_value ref_ty in
+  let shared_sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
   let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
@@ -382,7 +383,7 @@ let expand_symbolic_value_borrow (config : C.config)
   | T.Mut ->
       (* Simple case: simply create a fresh symbolic value and a fresh
        * borrow id *)
-      let sv = mk_fresh_symbolic_value ref_ty in
+      let sv = mk_fresh_symbolic_value original_sv.sv_kind ref_ty in
       let bid = C.fresh_borrow_id () in
       let see = SeMutRef (bid, sv) in
       (* Expand the symbolic values - we simply perform a substitution (and
@@ -424,8 +425,8 @@ let expand_symbolic_value_no_branching (config : C.config)
          * don't allow to expand enumerations with strictly more than one variant *)
         let expand_enumerations = false in
         match
-          compute_expanded_symbolic_adt_value expand_enumerations def_id regions
-            types ctx
+          compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind
+            def_id regions types ctx
         with
         | [ see ] ->
             (* Apply in the context *)
@@ -443,7 +444,7 @@ let expand_symbolic_value_no_branching (config : C.config)
     (* Tuples *)
     | T.Adt (T.Tuple, [], tys) ->
         (* Generate the field values *)
-        let see = compute_expanded_symbolic_tuple_value tys in
+        let see = compute_expanded_symbolic_tuple_value sp.sv_kind tys in
         (* Apply in the context *)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -454,7 +455,7 @@ let expand_symbolic_value_no_branching (config : C.config)
         ctx
     (* Boxes *)
     | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
-        let see = compute_expanded_symbolic_box_value boxed_ty in
+        let see = compute_expanded_symbolic_box_value sp.sv_kind boxed_ty in
         (* Apply in the context *)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -500,8 +501,8 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value)
        * don't allow to expand enumerations with strictly more than one variant *)
       let expand_enumerations = true in
       let seel =
-        compute_expanded_symbolic_adt_value expand_enumerations def_id regions
-          types ctx
+        compute_expanded_symbolic_adt_value expand_enumerations sp.sv_kind
+          def_id regions types ctx
       in
       (* Update the synthesized program *)
       S.synthesize_symbolic_expansion_enum_branching original_sv seel;
diff --git a/src/InterpreterExpressions.ml b/src/InterpreterExpressions.ml
index f577a190..2390aa48 100644
--- a/src/InterpreterExpressions.ml
+++ b/src/InterpreterExpressions.ml
@@ -242,7 +242,9 @@ let eval_unary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
     | E.Neg, T.Integer int_ty -> T.Integer int_ty
     | _ -> failwith "Invalid input for unop"
   in
-  let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in
+  let res_sv =
+    { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
+  in
   (* Synthesize *)
   S.synthesize_unary_op unop v res_sv;
   (* Return *)
@@ -360,7 +362,9 @@ let eval_binary_op_symbolic (config : C.config) (ctx : C.eval_ctx)
           | E.Ne | E.Eq -> failwith "Unreachable")
       | _ -> failwith "Invalid inputs for binop"
   in
-  let res_sv = { V.sv_id = res_sv_id; sv_ty = res_sv_ty } in
+  let res_sv =
+    { V.sv_kind = V.FunCallRet; V.sv_id = res_sv_id; sv_ty = res_sv_ty }
+  in
   (* Synthesize *)
   S.synthesize_binary_op binop v1 v2 res_sv;
   (* Return *)
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index 8b29bac9..e92b1c0b 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -885,7 +885,7 @@ and eval_function_call_symbolic_from_inst_sig (config : C.config)
     (args : E.operand list) (dest : E.place) : C.eval_ctx =
   (* Generate a fresh symbolic value for the return value *)
   let ret_sv_ty = inst_sg.A.output in
-  let ret_spc = mk_fresh_symbolic_value ret_sv_ty in
+  let ret_spc = mk_fresh_symbolic_value V.FunCallRet ret_sv_ty in
   let ret_value = mk_typed_value_from_symbolic_value ret_spc in
   let ret_av regions =
     mk_aproj_loans_value_from_symbolic_value regions ret_spc
diff --git a/src/InterpreterUtils.ml b/src/InterpreterUtils.ml
index 971dc801..e00e7dcf 100644
--- a/src/InterpreterUtils.ml
+++ b/src/InterpreterUtils.ml
@@ -53,16 +53,18 @@ let mk_place_from_var_id (var_id : V.VarId.id) : E.place =
   { var_id; projection = [] }
 
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_value (ty : T.rty) : V.symbolic_value =
+let mk_fresh_symbolic_value (sv_kind : V.sv_kind) (ty : T.rty) :
+    V.symbolic_value =
   let sv_id = C.fresh_symbolic_value_id () in
-  let svalue = { V.sv_id; V.sv_ty = ty } in
+  let svalue = { V.sv_kind; V.sv_id; V.sv_ty = ty } in
   svalue
 
 (** Create a fresh symbolic value *)
-let mk_fresh_symbolic_typed_value (rty : T.rty) : V.typed_value =
+let mk_fresh_symbolic_typed_value (sv_kind : V.sv_kind) (rty : T.rty) :
+    V.typed_value =
   let ty = Subst.erase_regions rty in
   (* Generate the fresh a symbolic value *)
-  let value = mk_fresh_symbolic_value rty in
+  let value = mk_fresh_symbolic_value sv_kind rty in
   let value = V.Symbolic value in
   { V.value; V.ty }
 
diff --git a/src/Values.ml b/src/Values.ml
index 59cfbdca..856ccb6f 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -45,7 +45,33 @@ type constant_value =
   | String of string
 [@@deriving show]
 
-type symbolic_value = { sv_id : SymbolicValueId.id; sv_ty : rty }
+(** The kind of a symbolic value, which precises how the value was generated *)
+type sv_kind =
+  | FunCallRet  (** The value is the return value of a function call *)
+  | FunCallGivenBack
+      (** The value is a borrowed value given back by an abstraction
+          (happens when giving a borrow to a function: when the abstraction
+          introduced to model the function call ends we reintroduce a symbolic
+          value in the context for the value modified by the abstraction through
+          the borrow).
+       *)
+  | SynthInput
+      (** The value is an input value of the function whose body we are
+          currently synthesizing.
+       *)
+  | SynthGivenBack
+      (** The value is a borrowed value that the function whose body we are
+          synthesizing returned, and which was given back because we ended
+          one of the lifetimes of this function (we do this to synthesize
+          the backward functions).
+       *)
+[@@deriving show]
+
+type symbolic_value = {
+  sv_kind : sv_kind;
+  sv_id : SymbolicValueId.id;
+  sv_ty : rty;
+}
 [@@deriving show]
 (** A symbolic value *)