From bcb49a7ddc86a2d70f7e1010a352c56329f32e14 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 10:33:47 +0100
Subject: Move some functions from Interpreter to InterpreterExpansion

---
 src/InterpreterExpansion.ml | 490 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 490 insertions(+)
 create mode 100644 src/InterpreterExpansion.ml

(limited to 'src/InterpreterExpansion.ml')

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"
-- 
cgit v1.2.3


From 8cac3c5cb5f9c36ffa878cf32ce858d171e4e3c8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 10:52:37 +0100
Subject: Cleanup the dependencies a bit

---
 src/InterpreterExpansion.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'src/InterpreterExpansion.ml')

diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 7b249717..30be657f 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -5,9 +5,7 @@
 
 module T = Types
 module V = Values
-open Scalars
 module E = Expressions
-open Errors
 module C = Contexts
 module Subst = Substitute
 module A = CfimAst
@@ -16,7 +14,6 @@ open TypesUtils
 open ValuesUtils
 module Inv = Invariants
 module S = Synthesis
-open Utils
 open InterpreterUtils
 open InterpreterProjectors
 open InterpreterBorrows
-- 
cgit v1.2.3


From 6a3faa82e09e3fbf23014b53a2b40d420bc70c9b Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 11:01:44 +0100
Subject: Cleanup a bit more the dependencies and activate more warnings/errors

---
 src/InterpreterExpansion.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'src/InterpreterExpansion.ml')

diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 30be657f..46398c84 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -8,7 +8,6 @@ module V = Values
 module E = Expressions
 module C = Contexts
 module Subst = Substitute
-module A = CfimAst
 module L = Logging
 open TypesUtils
 open ValuesUtils
-- 
cgit v1.2.3


From 973e14973ca857ed0b3fd69fa45901c8ae08820e Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 15:31:05 +0100
Subject: Fix some issues when evaluating assertions

---
 src/InterpreterExpansion.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/InterpreterExpansion.ml')

diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 46398c84..7366a819 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -166,6 +166,8 @@ let replace_symbolic_values (at_most_once : bool)
 (** 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...).
+    
+    This function does update the synthesis.
 *)
 let apply_symbolic_expansion_non_borrow (config : C.config)
     (original_sv : V.symbolic_value) (expansion : symbolic_expansion)
-- 
cgit v1.2.3


From 7137e0733650e0ce37eff4ff805c95543f2c1161 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 17:44:17 +0100
Subject: Remove the symbolic_proj_comp def and make the set of ended regions a
 field in the eval_ctx struct

---
 src/InterpreterExpansion.ml | 77 +++++++++++++++++++--------------------------
 1 file changed, 32 insertions(+), 45 deletions(-)

(limited to 'src/InterpreterExpansion.ml')

diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 7366a819..24ec018e 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -152,7 +152,7 @@ let replace_symbolic_values (at_most_once : bool)
       inherit [_] C.map_eval_ctx as super
 
       method! visit_Symbolic env spc =
-        if same_symbolic_id spc.V.svalue original_sv then replace ()
+        if same_symbolic_id spc original_sv then replace ()
         else super#visit_Symbolic env spc
     end
   in
@@ -190,9 +190,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)
-    (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 =
+    (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
@@ -210,8 +210,7 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
       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)
+        (fun ctx (ty : T.rty) -> mk_fresh_symbolic_value ty ctx)
         ctx field_types
     in
     let see = SeAdt (variant_id, field_values) in
@@ -220,32 +219,29 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
   (* 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 =
+let compute_expanded_symbolic_tuple_value (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)
+      (fun ctx sv_ty -> mk_fresh_symbolic_value 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 =
+let compute_expanded_symbolic_box_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 ctx, boxed_value = mk_fresh_symbolic_value 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)
+    (original_sv : V.symbolic_value) (ref_ty : T.rty) (ctx : C.eval_ctx) :
+    C.eval_ctx =
+  (* First, replace the projectors on borrows.
    * 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.
@@ -285,7 +281,7 @@ let expand_symbolic_value_shared_borrow (config : C.config)
       inherit [_] C.map_eval_ctx as super
 
       method! visit_Symbolic env sv =
-        if same_symbolic_id sv.V.svalue original_sv then
+        if same_symbolic_id sv original_sv then
           let bid = fresh_borrow () in
           V.Borrow (V.SharedBorrow bid)
         else super#visit_Symbolic env sv
@@ -326,7 +322,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 ctx, shared_sv = mk_fresh_symbolic_proj_comp ended_regions ref_ty ctx in
+  let ctx, shared_sv = mk_fresh_symbolic_value ref_ty ctx in
   let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
@@ -339,17 +335,16 @@ let expand_symbolic_value_shared_borrow (config : C.config)
   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 =
+    (original_sv : V.symbolic_value) (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));
+  assert (not (region_in_set region ctx.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, sv = mk_fresh_symbolic_value 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
@@ -370,8 +365,7 @@ let expand_symbolic_value_borrow (config : C.config)
       (* Return *)
       ctx
   | T.Shared ->
-      expand_symbolic_value_shared_borrow config original_sv ended_regions
-        ref_ty ctx
+      expand_symbolic_value_shared_borrow config original_sv 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).
@@ -379,13 +373,12 @@ let expand_symbolic_value_borrow (config : C.config)
     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) :
+    (pe : E.projection_elem) (sp : V.symbolic_value) (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 original_sv = sp 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 *)
@@ -396,8 +389,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 ended_regions
-            def_id regions types ctx
+          compute_expanded_symbolic_adt_value expand_enumerations def_id regions
+            types ctx
         with
         | [ (ctx, see) ] ->
             (* Apply in the context *)
@@ -413,9 +406,7 @@ let expand_symbolic_value_no_branching (config : C.config)
     | 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
+        let ctx, see = compute_expanded_symbolic_tuple_value tys ctx in
         (* Apply in the context *)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -426,9 +417,7 @@ let expand_symbolic_value_no_branching (config : C.config)
         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
+        let ctx, see = compute_expanded_symbolic_box_value boxed_ty ctx in
         (* Apply in the context *)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -439,8 +428,7 @@ let expand_symbolic_value_no_branching (config : C.config)
         ctx
     (* Borrows *)
     | Deref, T.Ref (region, ref_ty, rkind) ->
-        expand_symbolic_value_borrow config original_sv ended_regions region
-          ref_ty rkind ctx
+        expand_symbolic_value_borrow config original_sv region ref_ty rkind ctx
     | _ ->
         failwith
           ("Unreachable: " ^ E.show_projection_elem pe ^ ", " ^ T.show_rty rty)
@@ -454,13 +442,12 @@ let expand_symbolic_value_no_branching (config : C.config)
 
     This might lead to branching.
  *)
-let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_proj_comp)
+let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value)
     (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 original_sv = sp 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) ->
@@ -468,8 +455,8 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_proj_comp)
        * 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
+        compute_expanded_symbolic_adt_value expand_enumerations def_id regions
+          types ctx
       in
       (* Update the synthesized program *)
       let seel = List.map (fun (_, x) -> x) res in
-- 
cgit v1.2.3


From f3982cbe9782405b50b04c948ba7cb0bd89ef85f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 18:20:24 +0100
Subject: Make the symbolic, borrow, region and abstration counters global and
 stateful

---
 src/InterpreterExpansion.ml | 65 +++++++++++++++++++--------------------------
 1 file changed, 28 insertions(+), 37 deletions(-)

(limited to 'src/InterpreterExpansion.ml')

diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 24ec018e..2de06f24 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -183,16 +183,15 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
 
 (** 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.
+    The function might return a list of 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)
     (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 =
+    (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
@@ -205,38 +204,34 @@ let compute_expanded_symbolic_adt_value (expand_enumerations : bool)
   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)
+  let initialize
       ((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_value ty ctx)
-        ctx field_types
+      symbolic_expansion =
+    let field_values =
+      List.map (fun (ty : T.rty) -> mk_fresh_symbolic_value ty) field_types
     in
     let see = SeAdt (variant_id, field_values) in
-    (ctx, see)
+    see
   in
   (* Initialize all the expanded values of all the variants *)
-  List.map (initialize ctx) variants_fields_types
+  List.map initialize variants_fields_types
 
-let compute_expanded_symbolic_tuple_value (field_types : T.rty list)
-    (ctx : C.eval_ctx) : C.eval_ctx * symbolic_expansion =
+let compute_expanded_symbolic_tuple_value (field_types : T.rty list) :
+    symbolic_expansion =
   (* Generate the field values *)
-  let ctx, field_values =
-    List.fold_left_map
-      (fun ctx sv_ty -> mk_fresh_symbolic_value sv_ty ctx)
-      ctx field_types
+  let field_values =
+    List.map (fun sv_ty -> mk_fresh_symbolic_value sv_ty) field_types
   in
   let variant_id = None in
   let see = SeAdt (variant_id, field_values) in
-  (ctx, see)
+  see
 
-let compute_expanded_symbolic_box_value (boxed_ty : T.rty) (ctx : C.eval_ctx) :
-    C.eval_ctx * symbolic_expansion =
+let compute_expanded_symbolic_box_value (boxed_ty : T.rty) : symbolic_expansion
+    =
   (* Introduce a fresh symbolic value *)
-  let ctx, boxed_value = mk_fresh_symbolic_value boxed_ty ctx in
+  let boxed_value = mk_fresh_symbolic_value boxed_ty in
   let see = SeAdt (None, [ boxed_value ]) in
-  (ctx, see)
+  see
 
 let expand_symbolic_value_shared_borrow (config : C.config)
     (original_sv : V.symbolic_value) (ref_ty : T.rty) (ctx : C.eval_ctx) :
@@ -247,10 +242,8 @@ let expand_symbolic_value_shared_borrow (config : C.config)
    * 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';
+    let bid' = C.fresh_borrow_id () in
     borrows := V.BorrowId.Set.add bid' !borrows;
     bid'
   in
@@ -318,11 +311,10 @@ let expand_symbolic_value_shared_borrow (config : C.config)
   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_value ref_ty ctx in
+  let shared_sv = mk_fresh_symbolic_value ref_ty in
   let see = SeSharedRef (bids, shared_sv) in
   let allow_reborrows = true in
   let ctx =
@@ -344,8 +336,8 @@ let expand_symbolic_value_borrow (config : C.config)
   | T.Mut ->
       (* Simple case: simply create a fresh symbolic value and a fresh
        * borrow id *)
-      let ctx, sv = mk_fresh_symbolic_value ref_ty ctx in
-      let ctx, bid = C.fresh_borrow_id ctx in
+      let sv = mk_fresh_symbolic_value 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
        * check that we perform exactly one substitution) *)
@@ -392,7 +384,7 @@ let expand_symbolic_value_no_branching (config : C.config)
           compute_expanded_symbolic_adt_value expand_enumerations def_id regions
             types ctx
         with
-        | [ (ctx, see) ] ->
+        | [ see ] ->
             (* Apply in the context *)
             let ctx =
               apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -406,7 +398,7 @@ let expand_symbolic_value_no_branching (config : C.config)
     | 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 tys ctx in
+        let see = compute_expanded_symbolic_tuple_value tys in
         (* Apply in the context *)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -417,7 +409,7 @@ let expand_symbolic_value_no_branching (config : C.config)
         ctx
     (* Boxes *)
     | DerefBox, T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
-        let ctx, see = compute_expanded_symbolic_box_value boxed_ty ctx in
+        let see = compute_expanded_symbolic_box_value boxed_ty in
         (* Apply in the context *)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -454,15 +446,14 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value)
       (* 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 =
+      let seel =
         compute_expanded_symbolic_adt_value expand_enumerations 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 apply see : C.eval_ctx =
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
         in
@@ -471,5 +462,5 @@ let expand_symbolic_enum_value (config : C.config) (sp : V.symbolic_value)
         (* Return *)
         ctx
       in
-      List.map apply res
+      List.map apply seel
   | _ -> failwith "Unexpected"
-- 
cgit v1.2.3


From 1d0254f555e26968badf05d605cd630c018dcaa8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jan 2022 18:25:09 +0100
Subject: Cleanup

---
 src/InterpreterExpansion.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'src/InterpreterExpansion.ml')

diff --git a/src/InterpreterExpansion.ml b/src/InterpreterExpansion.ml
index 2de06f24..345c3df3 100644
--- a/src/InterpreterExpansion.ml
+++ b/src/InterpreterExpansion.ml
@@ -10,7 +10,6 @@ module C = Contexts
 module Subst = Substitute
 module L = Logging
 open TypesUtils
-open ValuesUtils
 module Inv = Invariants
 module S = Synthesis
 open InterpreterUtils
@@ -54,7 +53,7 @@ let apply_symbolic_expansion_to_target_avalues (config : C.config)
   let check_symbolic_no_ended = false in
   (* Prepare reborrows registration *)
   let fresh_reborrow, apply_registered_reborrows =
-    prepare_reborrows config allow_reborrows ctx
+    prepare_reborrows config allow_reborrows
   in
   (* Visitor to apply the expansion *)
   let obj =
-- 
cgit v1.2.3