1 files changed, 490 insertions, 0 deletions
diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
new file mode 100644
index 00000000..7b249717
--- /dev/null
+++ b/src/InterpreterExpansion.ml
@@ -0,0 +1,490 @@
+(* This module provides the functions which handle expansion of symbolic values.
+ * For now, this file doesn't handle expansion of ⊥ values because they need
+ * some path utilities for replacement. We might change that in the future (by
+ * using indices to identify the values for instance). *)
+
+module T = Types
+module V = Values
+open Scalars
+module E = Expressions
+open Errors
+module C = Contexts
+module Subst = Substitute
+module A = CfimAst
+module L = Logging
+open TypesUtils
+open ValuesUtils
+module Inv = Invariants
+module S = Synthesis
+open Utils
+open InterpreterUtils
+open InterpreterProjectors
+open InterpreterBorrows
+
+(** 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.
+    
+    Also, if this function is called on an expansion for *shared references*,
+    the proj borrows should already have been expanded.
+    
+    TODO: the way this function is used is a bit complex, especially because of
+    the above condition. Maybe we should have:
+    1. a generic function to expand the loan projectors
+    2. a function to expand the borrow projectors for non-borrows
+    3. specialized functions for mut borrows and shared borrows
+    Note that 2. and 3. may have a little bit of duplicated code, but hopefully
+    it would make things clearer.
+*)
+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 same_symbolic_id sv original_sv then
+              (* Apply the projector *)
+              let projected_value =
+                apply_proj_loans_on_symbolic_expansion proj_regions expansion
+                  original_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 same_symbolic_id 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) *)
+              (* WARNING: we mustn't get there if the expansion is for a shared
+               * reference. *)
+              let expansion =
+                symbolic_expansion_non_shared_borrow_to_value 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
+
+(** Auxiliary function.
+
+    Simply replace the symbolic values (*not avalues*) in the context with
+    a given value. Will break invariants if not used properly.
+*)
+let replace_symbolic_values (at_most_once : bool)
+    (original_sv : V.symbolic_value) (nv : V.value) (ctx : C.eval_ctx) :
+    C.eval_ctx =
+  (* Count *)
+  let replaced = ref false in
+  let replace () =
+    if at_most_once then assert (not !replaced);
+    replaced := true;
+    nv
+  in
+  (* Visitor to apply the substitution *)
+  let obj =
+    object
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_Symbolic env spc =
+        if same_symbolic_id spc.V.svalue original_sv then replace ()
+        else super#visit_Symbolic env spc
+    end
+  in
+  (* Apply the substitution *)
+  let ctx = obj#visit_eval_ctx None ctx in
+  (* Check that we substituted *)
+  assert !replaced;
+  (* Return *)
+  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 =
+  (* Apply the expansion to non-abstraction values *)
+  let nv = symbolic_expansion_non_borrow_to_value original_sv expansion in
+  let at_most_once = false in
+  let ctx = replace_symbolic_values at_most_once original_sv nv.V.value 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 the expansion of an adt value.
+
+    The function might return a list of contexts and values if the symbolic
+    value to expand is an enumeration.
+    
+    `expand_enumerations` controls the expansion of enumerations: if false, it
+    doesn't allow the expansion of enumerations *containing several variants*.
+ *)
+let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
+    (ended_regions : T.RegionId.set_t) (def_id : T.TypeDefId.id)
+    (regions : T.RegionId.id T.region list) (types : T.rty 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 = C.ctx_lookup_type_def ctx def_id in
+  assert (List.length regions = List.length def.T.region_params);
+  (* Retrieve, for every variant, the list of its instantiated field types *)
+  let variants_fields_types =
+    Subst.type_def_get_instantiated_variants_fields_rtypes def regions types
+  in
+  (* Check if there is strictly more than one variant *)
+  if List.length variants_fields_types > 1 && not expand_enumerations then
+    failwith "Not allowed to expand enumerations with several variants";
+  (* 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 * 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 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 * symbolic_expansion =
+  (* Generate the field values *)
+  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 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 * symbolic_expansion =
+  (* Introduce a fresh symbolic value *)
+  let ctx, boxed_value =
+    mk_fresh_symbolic_proj_comp ended_regions boxed_ty ctx
+  in
+  let see = SeAdt (None, [ boxed_value ]) in
+  (ctx, see)
+
+let expand_symbolic_value_shared_borrow (config : C.config)
+    (original_sv : V.symbolic_value) (ended_regions : T.RegionId.set_t)
+    (ref_ty : T.rty) (ctx : C.eval_ctx) : C.eval_ctx =
+  (* First, replace the projectors on borrows (AProjBorrow and proj_comp)
+   * The important point is that the symbolic value to expand may appear
+   * several times, if it has been copied. In this case, we need to introduce
+   * one fresh borrow id per instance.
+   *)
+  let borrows = ref V.BorrowId.Set.empty in
+  let borrow_counter = ref ctx.C.borrow_counter in
+  let fresh_borrow () =
+    let bid', cnt' = V.BorrowId.fresh !borrow_counter in
+    borrow_counter := cnt';
+    borrows := V.BorrowId.Set.add bid' !borrows;
+    bid'
+  in
+  (* Small utility used on shared borrows in abstractions (regular borrow
+   * projector and asb).
+   * Returns `Some` if the symbolic value has been expanded to an asb list,
+   * `None` otherwise *)
+  let reborrow_ashared proj_regions (sv : V.symbolic_value) (proj_ty : T.rty) :
+      V.abstract_shared_borrows option =
+    if same_symbolic_id sv original_sv then
+      match proj_ty with
+      | T.Ref (r, ref_ty, T.Shared) ->
+          (* Projector over the shared value *)
+          let shared_asb = V.AsbProjReborrows (sv, ref_ty) in
+          (* Check if the region is in the set of projected regions *)
+          if region_in_set r proj_regions then
+            (* In the set: we need to reborrow *)
+            let bid = fresh_borrow () in
+            Some [ V.AsbBorrow bid; shared_asb ]
+          else (* Not in the set: ignore *)
+            Some [ shared_asb ]
+      | _ -> failwith "Unexpected"
+    else None
+  in
+  (* Visitor to replace the projectors on borrows *)
+  let obj =
+    object
+      inherit [_] C.map_eval_ctx as super
+
+      method! visit_Symbolic env sv =
+        if same_symbolic_id sv.V.svalue original_sv then
+          let bid = fresh_borrow () in
+          V.Borrow (V.SharedBorrow bid)
+        else super#visit_Symbolic env sv
+
+      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
+
+      method! visit_AProjSharedBorrow proj_regions asb =
+        let expand_asb (asb : V.abstract_shared_borrow) :
+            V.abstract_shared_borrows =
+          match asb with
+          | V.AsbBorrow _ -> [ asb ]
+          | V.AsbProjReborrows (sv, proj_ty) -> (
+              match reborrow_ashared (Option.get proj_regions) sv proj_ty with
+              | None -> [ asb ]
+              | Some asb -> asb)
+        in
+        let asb = List.concat (List.map expand_asb asb) in
+        V.AProjSharedBorrow asb
+
+      method! visit_ASymbolic proj_regions aproj =
+        match aproj with
+        | AProjLoans _ ->
+            (* Loans are handled later *)
+            super#visit_ASymbolic proj_regions aproj
+        | AProjBorrows (sv, proj_ty) -> (
+            (* Check if we need to reborrow *)
+            match reborrow_ashared (Option.get proj_regions) sv proj_ty with
+            | None -> super#visit_ASymbolic proj_regions aproj
+            | Some asb -> V.ABorrow (V.AProjSharedBorrow asb))
+    end
+  in
+  (* Call the visitor *)
+  let ctx = obj#visit_eval_ctx None ctx in
+  let ctx = { ctx with C.borrow_counter = !borrow_counter } in
+  (* Finally, replace the projectors on loans *)
+  let bids = !borrows in
+  assert (not (V.BorrowId.Set.is_empty bids));
+  let ctx, shared_sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in
+  let see = SeSharedRef (bids, shared_sv) in
+  let allow_reborrows = true in
+  let ctx =
+    apply_symbolic_expansion_to_avalues config allow_reborrows original_sv see
+      ctx
+  in
+  (* Update the synthesized program *)
+  S.synthesize_symbolic_expansion_no_branching original_sv see;
+  (* Return *)
+  ctx
+
+let expand_symbolic_value_borrow (config : C.config)
+    (original_sv : V.symbolic_value) (ended_regions : T.RegionId.set_t)
+    (region : T.RegionId.id T.region) (ref_ty : T.rty) (rkind : T.ref_kind)
+    (ctx : C.eval_ctx) : C.eval_ctx =
+  (* Check that we are allowed to expand the reference *)
+  assert (not (region_in_set region ended_regions));
+  (* Match on the reference kind *)
+  match rkind with
+  | T.Mut ->
+      (* Simple case: simply create a fresh symbolic value and a fresh
+       * borrow id *)
+      let ctx, sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in
+      let ctx, bid = C.fresh_borrow_id ctx in
+      let see = SeMutRef (bid, sv) in
+      (* Expand the symbolic values - we simply perform a substitution (and
+       * check that we perform exactly one substitution) *)
+      let nv = symbolic_expansion_non_shared_borrow_to_value original_sv see in
+      let at_most_once = true in
+      let ctx =
+        replace_symbolic_values at_most_once original_sv nv.V.value ctx
+      in
+      (* Expand the symbolic avalues *)
+      let allow_reborrows = true in
+      let ctx =
+        apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
+          see ctx
+      in
+      (* Update the synthesized program *)
+      S.synthesize_symbolic_expansion_no_branching original_sv see;
+      (* Return *)
+      ctx
+  | T.Shared ->
+      expand_symbolic_value_shared_borrow config original_sv ended_regions
+        ref_ty ctx
+
+(** Expand a symbolic value which is not an enumeration with several variants
+    (i.e., in a situation where it doesn't lead to branching).
+
+    This function is used when exploring paths.
+ *)
+let expand_symbolic_value_no_branching (config : C.config)
+    (pe : E.projection_elem) (sp : V.symbolic_proj_comp) (ctx : C.eval_ctx) :
+    C.eval_ctx =
+  (* Compute the expanded value - note that when doing so, we may introduce
+   * fresh symbolic values in the context (which thus gets updated) *)
+  let original_sv = sp.V.svalue in
+  let rty = original_sv.V.sv_ty in
+  let ended_regions = sp.V.rset_ended in
+  let ctx =
+    match (pe, rty) with
+    (* "Regular" ADTs *)
+    | ( Field (ProjAdt (def_id, _opt_variant_id), _),
+        T.Adt (T.AdtId def_id', regions, types) ) -> (
+        assert (def_id = def_id');
+        (* Compute the expanded value - there should be exactly one because we
+         * 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 ended_regions
+            def_id regions types ctx
+        with
+        | [ (ctx, see) ] ->
+            (* Apply in the context *)
+            let ctx =
+              apply_symbolic_expansion_non_borrow config original_sv see ctx
+            in
+            (* Update the synthesized program *)
+            S.synthesize_symbolic_expansion_no_branching original_sv see;
+            (* Return *)
+            ctx
+        | _ -> failwith "Unexpected")
+    (* Tuples *)
+    | Field (ProjTuple arity, _), T.Adt (T.Tuple, [], tys) ->
+        assert (arity = List.length tys);
+        (* Generate the field values *)
+        let ctx, see =
+          compute_expanded_symbolic_tuple_value ended_regions tys ctx
+        in
+        (* Apply in the context *)
+        let ctx =
+          apply_symbolic_expansion_non_borrow config original_sv see ctx
+        in
+        (* Update the synthesized program *)
+        S.synthesize_symbolic_expansion_no_branching original_sv see;
+        (* Return *)
+        ctx
+    (* Boxes *)
+    | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
+        let ctx, see =
+          compute_expanded_symbolic_box_value ended_regions boxed_ty ctx
+        in
+        (* Apply in the context *)
+        let ctx =
+          apply_symbolic_expansion_non_borrow config original_sv see ctx
+        in
+        (* Update the synthesized program *)
+        S.synthesize_symbolic_expansion_no_branching original_sv see;
+        (* Return *)
+        ctx
+    (* Borrows *)
+    | Deref, T.Ref (region, ref_ty, rkind) ->
+        expand_symbolic_value_borrow config original_sv ended_regions region
+          ref_ty rkind ctx
+    | _ ->
+        failwith
+          ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)
+  in
+  (* Sanity check: the symbolic value has disappeared *)
+  assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx));
+  (* Return *)
+  ctx
+
+(** Expand a symbolic enumeration value.
+
+    This might lead to branching.
+ *)
+let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_proj_comp)
+    (ctx : C.eval_ctx) : C.eval_ctx list =
+  (* Compute the expanded value - note that when doing so, we may introduce
+   * fresh symbolic values in the context (which thus gets updated) *)
+  let original_sv = sp.V.svalue in
+  let rty = original_sv.V.sv_ty in
+  let ended_regions = sp.V.rset_ended in
+  match rty with
+  (*  The value should be a "regular" ADTs *)
+  | T.Adt (T.AdtId def_id, regions, types) ->
+      (* Compute the expanded value - there should be exactly one because we
+       * don't allow to expand enumerations with strictly more than one variant *)
+      let expand_enumerations = true in
+      let res =
+        compute_expanded_symbolic_adt_value expand_enumerations ended_regions
+          def_id regions types ctx
+      in
+      (* Update the synthesized program *)
+      let seel = List.map (fun (_, x) -> x) res in
+      S.synthesize_symbolic_expansion_enum_branching original_sv seel;
+      (* Apply in the context *)
+      let apply (ctx, see) : C.eval_ctx =
+        let ctx =
+          apply_symbolic_expansion_non_borrow config original_sv see ctx
+        in
+        (* Sanity check: the symbolic value has disappeared *)
+        assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx));
+        (* Return *)
+        ctx
+      in
+      List.map apply res
+  | _ -> failwith "Unexpected"