Make more progress on symbolic expansion

1 files changed, 160 insertions, 156 deletions

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 9c806e8f..c871d530 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -69,12 +69,18 @@ let mk_box_value (v : V.typed_value) : V.typed_value =
   let box_v = V.Adt { variant_id = None; field_values = [ v ] } in
   mk_typed_value box_ty box_v
 
-(** Create a fresh symbolic value (as a complementary projector) *)
+(** Create a fresh symbolic proj comp *)
 let mk_fresh_symbolic_proj_comp (ended_regions : T.RegionId.set_t) (ty : T.rty)
-    (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
+    (ctx : C.eval_ctx) : C.eval_ctx * V.symbolic_proj_comp =
   let ctx, sv_id = C.fresh_symbolic_value_id ctx in
   let svalue = { V.sv_id; V.sv_ty = ty } in
   let sv = { V.svalue; rset_ended = ended_regions } in
+  (ctx, sv)
+
+(** Create a fresh symbolic value (as a complementary projector) *)
+let mk_fresh_symbolic_proj_comp_value (ended_regions : T.RegionId.set_t)
+    (ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
+  let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ty ctx in
   let value : V.value = V.Symbolic sv in
   let ty : T.ety = Subst.erase_regions ty in
   let sv : V.typed_value = { V.value; ty } in
@@ -2681,6 +2687,139 @@ let write_place_unwrap (config : C.config) (access : access_kind) (p : E.place)
   | Error _ -> failwith "Unreachable"
   | Ok ctx -> ctx
 
+(** Projector kind *)
+type proj_kind = LoanProj | BorrowProj
+
+(** Auxiliary function.
+    Apply a symbolic expansion to avalues in a context, targetting a specific
+    kind of projectors.
+    
+    [proj_kind] controls whether we apply the expansion to projectors
+    on loans or projectors on borrows.
+    
+    When dealing with reference expansion, it is necessary to first apply the
+    expansion on loan projectors, then on borrow projectors. The reason is
+    that reducing the borrow projectors might require to perform some reborrows,
+    in which case we need to lookup the corresponding loans in the context.
+    
+    [allow_reborrows] controls whether we allow reborrows or not. It is useful
+    only if we target borrow projectors.
+*)
+let apply_symbolic_expansion_to_target_avalues (config : C.config)
+    (allow_reborrows : bool) (proj_kind : proj_kind)
+    (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Symbolic values contained in the expansion might contain already ended regions *)
+  let check_symbolic_no_ended = false in
+  (* Prepare reborrows registration *)
+  let fresh_reborrow, apply_registered_reborrows =
+    prepare_reborrows config allow_reborrows ctx
+  in
+  (* Visitor to apply the expansion *)
+  let obj =
+    object
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_abs proj_regions abs =
+        assert (Option.is_none proj_regions);
+        let proj_regions = Some abs.V.regions in
+        super#visit_abs proj_regions abs
+      (** When visiting an abstraction, we remember the regions it owns to be
+          able to properly reduce projectors when expanding symbolic values *)
+
+      method! visit_ASymbolic proj_regions aproj =
+        let proj_regions = Option.get proj_regions in
+        match (aproj, proj_kind) with
+        | V.AProjLoans sv, LoanProj ->
+            (* Check if this is the symbolic value we are looking for *)
+            if sv = original_sv then
+              (* Apply the projector *)
+              let projected_value =
+                apply_proj_loans_on_symbolic_expansion ctx proj_regions
+                  expansion sv.V.sv_ty
+              in
+              (* Replace *)
+              projected_value.V.value
+            else
+              (* Not the searched symbolic value: nothing to do *)
+              super#visit_ASymbolic (Some proj_regions) aproj
+        | V.AProjBorrows (sv, proj_ty), BorrowProj ->
+            (* Check if this is the symbolic value we are looking for *)
+            if sv = original_sv then
+              (* Convert the symbolic expansion to a value on which we can
+               * apply a projector (if the expansion is a reference expansion,
+               * convert it to a borrow) *)
+              let expansion =
+                symbolic_expansion_to_value_with_borrows original_sv expansion
+              in
+              (* Apply the projector *)
+              let projected_value =
+                apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
+                  proj_regions expansion proj_ty
+              in
+              (* Replace *)
+              projected_value.V.value
+            else
+              (* Not the searched symbolic value: nothing to do *)
+              super#visit_ASymbolic (Some proj_regions) aproj
+        | V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj ->
+            (* Nothing to do *)
+            super#visit_ASymbolic (Some proj_regions) aproj
+    end
+  in
+  (* Apply the expansion *)
+  let ctx = obj#visit_eval_ctx None ctx in
+  (* Apply the reborrows *)
+  apply_registered_reborrows ctx
+
+(** Auxiliary function.
+    Apply a symbolic expansion to avalues in a context.
+*)
+let apply_symbolic_expansion_to_avalues (config : C.config)
+    (allow_reborrows : bool) (original_sv : V.symbolic_value)
+    (expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx =
+  let apply_expansion proj_kind ctx =
+    apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind
+      original_sv expansion ctx
+  in
+  (* First target the loan projectors, then the borrow projectors *)
+  let ctx = apply_expansion LoanProj ctx in
+  let ctx = apply_expansion BorrowProj ctx in
+  ctx
+
+(** Apply a symbolic expansion to a context, by replacing the original
+    symbolic value with its expanded value. Is valid only if the expansion
+    is not a borrow (i.e., an adt...).
+*)
+let apply_symbolic_expansion_non_borrow (config : C.config)
+    (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Convert the expansion to a value *)
+  let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
+  (* Visitor to apply the expansion to *non-abstraction* values *)
+  let obj =
+    object
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_Symbolic env spc =
+        if spc.V.svalue = original_sv then nv.V.value
+        else super#visit_Symbolic env spc
+      (** Replace a symbolic value with its expansion.
+          Note that there may be several references to the same symbolic value
+          in the context, if the value has been copied. Expansion is then a bit
+          subtle in the case we expand shared borrows, in which case we need to
+          introduce a unique borrow identifier for every borrow (this is not
+          the case here: this function should NOT be used to expand borrows).
+      *)
+    end
+  in
+  (* Apply the expansion to non-abstraction values *)
+  let ctx = obj#visit_eval_ctx None ctx in
+  (* Apply the expansion to abstraction values *)
+  let allow_reborrows = false in
+  apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
+    expansion ctx
+
 (** Compute an expanded ADT bottom value *)
 let compute_expanded_bottom_adt_value (tyctx : T.type_def list)
     (def_id : T.TypeDefId.id) (opt_variant_id : T.VariantId.id option)
@@ -2795,7 +2934,7 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
     (ended_regions : T.RegionId.set_t) (def_id : T.TypeDefId.id)
     (opt_variant_id : T.VariantId.id option)
     (regions : T.RegionId.id T.region list) (types : T.rty list)
-    (ctx : C.eval_ctx) : (C.eval_ctx * V.typed_value) list =
+    (ctx : C.eval_ctx) : (C.eval_ctx * symbolic_expansion) list =
   (* Lookup the definition and check if it is an enumeration with several
    * variants *)
   let def = T.TypeDefId.nth ctx.type_context def_id in
@@ -2810,42 +2949,40 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
   (* Initialize the expanded value for a given variant *)
   let initialize (ctx : C.eval_ctx)
       ((variant_id, field_types) : T.VariantId.id option * T.rty list) :
-      C.eval_ctx * V.typed_value =
+      C.eval_ctx * symbolic_expansion =
     let ctx, field_values =
       List.fold_left_map
         (fun ctx (ty : T.rty) ->
           mk_fresh_symbolic_proj_comp ended_regions ty ctx)
         ctx field_types
     in
-    let av = V.Adt { variant_id; field_values } in
-    let ty = T.Adt (T.AdtId def_id, regions, types) in
-    let ty = Subst.erase_regions ty in
-    (ctx, { V.value = av; V.ty })
+    let see = SeAdt (variant_id, field_values) in
+    (ctx, see)
   in
   (* Initialize all the expanded values of all the variants *)
   List.map (initialize ctx) variants_fields_types
 
 let compute_expanded_symbolic_tuple_value (ended_regions : T.RegionId.set_t)
-    (field_types : T.rty list) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
+    (field_types : T.rty list) (ctx : C.eval_ctx) :
+    C.eval_ctx * symbolic_expansion =
   (* Generate the field values *)
-  let ctx, fields =
+  let ctx, field_values =
     List.fold_left_map
       (fun ctx sv_ty -> mk_fresh_symbolic_proj_comp ended_regions sv_ty ctx)
       ctx field_types
   in
-  let v = V.Adt { variant_id = None; field_values = fields } in
-  let field_types = List.map Subst.erase_regions field_types in
-  let ty = T.Adt (T.Tuple, [], field_types) in
-  (ctx, { V.value = v; V.ty })
+  let variant_id = None in
+  let see = SeAdt (variant_id, field_values) in
+  (ctx, see)
 
 let compute_expanded_symbolic_box_value (ended_regions : T.RegionId.set_t)
-    (boxed_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * V.typed_value =
+    (boxed_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx * symbolic_expansion =
   (* Introduce a fresh symbolic value *)
   let ctx, boxed_value =
     mk_fresh_symbolic_proj_comp ended_regions boxed_ty ctx
   in
-  let box_value = mk_box_value boxed_value in
-  (ctx, box_value)
+  let see = SeAdt (None, [ boxed_value ]) in
+  (ctx, see)
 
 let expand_symbolic_value_borrow (ended_regions : T.RegionId.set_t)
     (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind)
@@ -2862,139 +2999,6 @@ let expand_symbolic_value_borrow (ended_regions : T.RegionId.set_t)
       raise Unimplemented
   | T.Shared -> raise Unimplemented
 
-(** Projector kind *)
-type proj_kind = LoanProj | BorrowProj
-
-(** Auxiliary function.
-    Apply a symbolic expansion to avalues in a context, targetting a specific
-    kind of projectors.
-    
-    [proj_kind] controls whether we apply the expansion to projectors
-    on loans or projectors on borrows.
-    
-    When dealing with reference expansion, it is necessary to first apply the
-    expansion on loan projectors, then on borrow projectors. The reason is
-    that reducing the borrow projectors might require to perform some reborrows,
-    in which case we need to lookup the corresponding loans in the context.
-    
-    [allow_reborrows] controls whether we allow reborrows or not. It is useful
-    only if we target borrow projectors.
-*)
-let apply_symbolic_expansion_to_target_avalues (config : C.config)
-    (allow_reborrows : bool) (proj_kind : proj_kind)
-    (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Symbolic values contained in the expansion might contain already ended regions *)
-  let check_symbolic_no_ended = false in
-  (* Prepare reborrows registration *)
-  let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows config allow_reborrows ctx
-  in
-  (* Visitor to apply the expansion *)
-  let obj =
-    object
-      inherit [_] C.map_eval_ctx as super
-
-      method! visit_abs proj_regions abs =
-        assert (Option.is_none proj_regions);
-        let proj_regions = Some abs.V.regions in
-        super#visit_abs proj_regions abs
-      (** When visiting an abstraction, we remember the regions it owns to be
-          able to properly reduce projectors when expanding symbolic values *)
-
-      method! visit_ASymbolic proj_regions aproj =
-        let proj_regions = Option.get proj_regions in
-        match (aproj, proj_kind) with
-        | V.AProjLoans sv, LoanProj ->
-            (* Check if this is the symbolic value we are looking for *)
-            if sv = original_sv then
-              (* Apply the projector *)
-              let projected_value =
-                apply_proj_loans_on_symbolic_expansion ctx proj_regions
-                  expansion sv.V.sv_ty
-              in
-              (* Replace *)
-              projected_value.V.value
-            else
-              (* Not the searched symbolic value: nothing to do *)
-              super#visit_ASymbolic (Some proj_regions) aproj
-        | V.AProjBorrows (sv, proj_ty), BorrowProj ->
-            (* Check if this is the symbolic value we are looking for *)
-            if sv = original_sv then
-              (* Convert the symbolic expansion to a value on which we can
-               * apply a projector (if the expansion is a reference expansion,
-               * convert it to a borrow) *)
-              let expansion =
-                symbolic_expansion_to_value_with_borrows original_sv expansion
-              in
-              (* Apply the projector *)
-              let projected_value =
-                apply_proj_borrows check_symbolic_no_ended ctx fresh_reborrow
-                  proj_regions expansion proj_ty
-              in
-              (* Replace *)
-              projected_value.V.value
-            else
-              (* Not the searched symbolic value: nothing to do *)
-              super#visit_ASymbolic (Some proj_regions) aproj
-        | V.AProjLoans _, BorrowProj | V.AProjBorrows (_, _), LoanProj ->
-            (* Nothing to do *)
-            super#visit_ASymbolic (Some proj_regions) aproj
-    end
-  in
-  (* Apply the expansion *)
-  let ctx = obj#visit_eval_ctx None ctx in
-  (* Apply the reborrows *)
-  apply_registered_reborrows ctx
-
-(** Auxiliary function.
-    Apply a symbolic expansion to avalues in a context.
-*)
-let apply_symbolic_expansion_to_avalues (config : C.config)
-    (allow_reborrows : bool) (original_sv : V.symbolic_value)
-    (expansion : symbolic_expansion) (ctx : C.eval_ctx) : C.eval_ctx =
-  let apply_expansion proj_kind ctx =
-    apply_symbolic_expansion_to_target_avalues config allow_reborrows proj_kind
-      original_sv expansion ctx
-  in
-  (* First target the loan projectors, then the borrow projectors *)
-  let ctx = apply_expansion LoanProj ctx in
-  let ctx = apply_expansion BorrowProj ctx in
-  ctx
-
-(** Apply a symbolic expansion to a context, by replacing the original
-    symbolic value with its expanded value. Is valid only if the expansion
-    is not a borrow (i.e., an adt...).
-*)
-let apply_symbolic_expansion_non_borrow (config : C.config)
-    (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
-    (ctx : C.eval_ctx) : C.eval_ctx =
-  (* Convert the expansion to a value *)
-  let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
-  (* Visitor to apply the expansion to *non-abstraction* values *)
-  let obj =
-    object
-      inherit [_] C.map_eval_ctx as super
-
-      method! visit_Symbolic env spc =
-        if spc.V.svalue = original_sv then nv.V.value
-        else super#visit_Symbolic env spc
-      (** Replace a symbolic value with its expansion.
-          Note that there may be several references to the same symbolic value
-          in the context, if the value has been copied. Expansion is then a bit
-          subtle in the case we expand shared borrows, in which case we need to
-          introduce a unique borrow identifier for every borrow (this is not
-          the case here: this function should NOT be used to expand borrows).
-      *)
-    end
-  in
-  (* Apply the expansion to non-abstraction values *)
-  let ctx = obj#visit_eval_ctx None ctx in
-  (* Apply the expansion to abstraction values *)
-  let allow_reborrows = false in
-  apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
-    expansion ctx
-
 (** Expand a symbolic value which is not an enumeration with several variants.
 
     This function is used when exploring a path.
@@ -3030,12 +3034,6 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem)
       in
       (* Apply in the context *)
       apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx
-  (* Borrows *)
-  | Deref, T.Ref (region, ref_ty, rkind) ->
-      let _ =
-        expand_symbolic_value_borrow ended_regions region ref_ty rkind ctx
-      in
-      raise Unimplemented
   (* Boxes *)
   | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
       let ctx, nv =
@@ -3043,6 +3041,12 @@ let expand_symbolic_value_non_enum (config : C.config) (pe : E.projection_elem)
       in
       (* Apply in the context *)
       apply_symbolic_expansion_non_borrow config sp.V.svalue nv ctx
+  (* Borrows *)
+  | Deref, T.Ref (region, ref_ty, rkind) ->
+      let _ =
+        expand_symbolic_value_borrow ended_regions region ref_ty rkind ctx
+      in
+      raise Unimplemented
   | _ ->
       failwith
         ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)