Reorganize the symoblic expansions to separate the branching/non-branching ones

3 files changed, 95 insertions, 72 deletions

diff --git a/compiler/InterpreterExpansion.ml b/compiler/InterpreterExpansion.ml
index c2807311..a0fe5ecb 100644
--- a/compiler/InterpreterExpansion.ml
+++ b/compiler/InterpreterExpansion.ml
@@ -210,7 +210,8 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
   apply_symbolic_expansion_to_avalues config allow_reborrows original_sv
     expansion ctx
 
-(** Compute the expansion of an adt value.
+(** Compute the expansion of a non-assumed (i.e.: not [Option], [Box], etc.)
+    adt value.
 
     The function might return a list of values if the symbolic value to expand
     is an enumeration.
@@ -218,7 +219,7 @@ let apply_symbolic_expansion_non_borrow (config : C.config)
     [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)
+let compute_expanded_symbolic_non_assumed_adt_value (expand_enumerations : bool)
     (kind : V.sv_kind) (def_id : T.TypeDeclId.id)
     (regions : T.RegionId.id T.region list) (types : T.rty list)
     (ctx : C.eval_ctx) : V.symbolic_expansion list =
@@ -274,6 +275,31 @@ let compute_expanded_symbolic_box_value (kind : V.sv_kind) (boxed_ty : T.rty) :
   let see = V.SeAdt (None, [ boxed_value ]) in
   see
 
+(** Compute the expansion of an adt value.
+
+    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)
+    (kind : V.sv_kind) (adt_id : T.type_id)
+    (regions : T.RegionId.id T.region list) (types : T.rty list)
+    (ctx : C.eval_ctx) : V.symbolic_expansion list =
+  match (adt_id, regions, types) with
+  | T.AdtId def_id, _, _ ->
+      compute_expanded_symbolic_non_assumed_adt_value expand_enumerations kind
+        def_id regions types ctx
+  | T.Tuple, [], _ -> [ compute_expanded_symbolic_tuple_value kind types ]
+  | T.Assumed T.Option, [], [ ty ] ->
+      compute_expanded_symbolic_option_value expand_enumerations kind ty
+  | T.Assumed T.Box, [], [ boxed_ty ] ->
+      [ compute_expanded_symbolic_box_value kind boxed_ty ]
+  | _ ->
+      raise
+        (Failure "compute_expanded_symbolic_adt_value: unexpected combination")
+
 let expand_symbolic_value_shared_borrow (config : C.config)
     (original_sv : V.symbolic_value) (original_sv_place : SA.mplace option)
     (ref_ty : T.rty) : cm_fun =
@@ -484,11 +510,13 @@ let expand_symbolic_bool (config : C.config) (sv : V.symbolic_value)
   apply_branching_symbolic_expansions_non_borrow config original_sv
     original_sv_place seel ctx
 
-let expand_symbolic_value (config : C.config) (allow_branching : bool)
+let expand_symbolic_value_no_branching (config : C.config)
     (sv : V.symbolic_value) (sv_place : SA.mplace option) : cm_fun =
  fun cf ctx ->
   (* Debug *)
-  log#ldebug (lazy ("expand_symbolic_value:" ^ symbolic_value_to_string ctx sv));
+  log#ldebug
+    (lazy
+      ("expand_symbolic_value_no_branching:" ^ symbolic_value_to_string ctx sv));
   (* Remember the initial context for printing purposes *)
   let ctx0 = ctx in
   (* Compute the expanded value - note that when doing so, we may introduce
@@ -499,52 +527,16 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
   let cc : cm_fun =
    fun cf ctx ->
     match rty with
-    (* TODO: I think it is possible to factorize a lot the below match *)
-    (* "Regular" ADTs *)
-    | T.Adt (T.AdtId def_id, regions, types) ->
+    (* ADTs *)
+    | T.Adt (adt_id, regions, types) ->
         (* Compute the expanded value *)
+        let allow_branching = false in
         let seel =
-          compute_expanded_symbolic_adt_value allow_branching sv.sv_kind def_id
+          compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id
             regions types ctx
         in
-        (* Check for branching *)
-        assert (List.length seel <= 1 || allow_branching);
-        (* Apply *)
-        let seel = List.map (fun see -> (Some see, cf)) seel in
-        apply_branching_symbolic_expansions_non_borrow config original_sv
-          original_sv_place seel ctx
-    (* Options *)
-    | T.Adt (T.Assumed Option, regions, types) ->
-        (* Sanity check *)
-        assert (regions = []);
-        let ty = Collections.List.to_cons_nil types in
-        (* Compute the expanded value *)
-        let seel =
-          compute_expanded_symbolic_option_value allow_branching sv.sv_kind ty
-        in
-
-        (* Check for branching *)
-        assert (List.length seel <= 1 || allow_branching);
-        (* Apply *)
-        let seel = List.map (fun see -> (Some see, cf)) seel in
-        apply_branching_symbolic_expansions_non_borrow config original_sv
-          original_sv_place seel ctx
-    (* Tuples *)
-    | T.Adt (T.Tuple, [], tys) ->
-        (* Generate the field values *)
-        let see = compute_expanded_symbolic_tuple_value sv.sv_kind tys in
-        (* Apply in the context *)
-        let ctx =
-          apply_symbolic_expansion_non_borrow config original_sv see ctx
-        in
-        (* Call the continuation *)
-        let expr = cf ctx in
-        (* Update the synthesized program *)
-        S.synthesize_symbolic_expansion_no_branching original_sv
-          original_sv_place see expr
-    (* Boxes *)
-    | T.Adt (T.Assumed T.Box, [], [ boxed_ty ]) ->
-        let see = compute_expanded_symbolic_box_value sv.sv_kind boxed_ty in
+        (* There should be exacly one branch *)
+        let see = Collections.List.to_cons_nil seel in
         (* Apply in the context *)
         let ctx =
           apply_symbolic_expansion_non_borrow config original_sv see ctx
@@ -558,20 +550,64 @@ let expand_symbolic_value (config : C.config) (allow_branching : bool)
     | T.Ref (region, ref_ty, rkind) ->
         expand_symbolic_value_borrow config original_sv original_sv_place region
           ref_ty rkind cf ctx
-    (* Booleans *)
-    | T.Bool ->
-        assert allow_branching;
-        expand_symbolic_bool config sv sv_place cf cf ctx
     | _ ->
         raise
-          (Failure ("expand_symbolic_value: unexpected type: " ^ T.show_rty rty))
+          (Failure
+             ("expand_symbolic_value_no_branching: unexpected type: "
+            ^ T.show_rty rty))
   in
   (* Debug *)
   let cc =
     comp_unit cc (fun ctx ->
         log#ldebug
           (lazy
-            ("expand_symbolic_value: "
+            ("expand_symbolic_value_no_branching: "
+            ^ symbolic_value_to_string ctx0 sv
+            ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
+            ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
+        (* Sanity check: the symbolic value has disappeared *)
+        assert (not (symbolic_value_id_in_ctx original_sv.V.sv_id ctx)))
+  in
+  (* Continue *)
+  cc cf ctx
+
+let expand_symbolic_adt (config : C.config) (sv : V.symbolic_value)
+    (sv_place : SA.mplace option) : cm_fun =
+ fun cf ctx ->
+  (* Debug *)
+  log#ldebug (lazy ("expand_symbolic_adt:" ^ symbolic_value_to_string ctx sv));
+  (* Remember the initial context for printing purposes *)
+  let ctx0 = ctx in
+  (* 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 = sv in
+  let original_sv_place = sv_place in
+  let rty = original_sv.V.sv_ty in
+  let cc : cm_fun =
+   fun cf ctx ->
+    match rty with
+    (* ADTs *)
+    | T.Adt (adt_id, regions, types) ->
+        let allow_branching = true in
+        (* Compute the expanded value *)
+        let seel =
+          compute_expanded_symbolic_adt_value allow_branching sv.sv_kind adt_id
+            regions types ctx
+        in
+        (* Apply *)
+        let seel = List.map (fun see -> (Some see, cf)) seel in
+        apply_branching_symbolic_expansions_non_borrow config original_sv
+          original_sv_place seel ctx
+    | _ ->
+        raise
+          (Failure ("expand_symbolic_adt: unexpected type: " ^ T.show_rty rty))
+  in
+  (* Debug *)
+  let cc =
+    comp_unit cc (fun ctx ->
+        log#ldebug
+          (lazy
+            ("expand_symbolic_adt: "
             ^ symbolic_value_to_string ctx0 sv
             ^ "\n\n- original context:\n" ^ eval_ctx_to_string ctx0
             ^ "\n\n- new context:\n" ^ eval_ctx_to_string ctx ^ "\n"));
@@ -602,11 +638,6 @@ let expand_symbolic_int (config : C.config) (sv : V.symbolic_value)
   (* Then expand and evaluate - this generates the proper symbolic AST *)
   apply_branching_symbolic_expansions_non_borrow config sv sv_place tgts
 
-let expand_symbolic_value_no_branching (config : C.config)
-    (sv : V.symbolic_value) (sv_place : SA.mplace option) : cm_fun =
-  let allow_branching = false in
-  expand_symbolic_value config allow_branching sv sv_place
-
 (** Expand all the symbolic values which contain borrows.
     Allows us to restrict ourselves to a simpler model for the projectors over
     symbolic values.
diff --git a/compiler/InterpreterExpansion.mli b/compiler/InterpreterExpansion.mli
index ee9f9e44..54f9036f 100644
--- a/compiler/InterpreterExpansion.mli
+++ b/compiler/InterpreterExpansion.mli
@@ -17,18 +17,6 @@ type proj_kind = LoanProj | BorrowProj
 val expand_symbolic_bool :
   C.config -> V.symbolic_value -> SA.mplace option -> m_fun -> m_fun -> m_fun
 
-(** Expand a symbolic value.
-    
-    Parameters:
-    - [config]
-    - [allow_branching]: if [true] we can branch (by expanding enumerations with
-      stricly more than one variant), otherwise we can't.
-    - [sv]
-    - [sv_place]
- *)
-val expand_symbolic_value :
-  C.config -> bool -> V.symbolic_value -> SA.mplace option -> cm_fun
-
 (** Symbolic integers are expanded upon evaluating a [switch], when the integer
     is not an enumeration discriminant.
     Note that a discriminant is never symbolic: we evaluate discriminant values
@@ -67,6 +55,12 @@ val expand_symbolic_int :
 val expand_symbolic_value_no_branching :
   C.config -> V.symbolic_value -> SA.mplace option -> cm_fun
 
+(** Expand a symbolic enumeration (leads to branching if the enumeration has
+    more than one variant).
+ *)
+val expand_symbolic_adt :
+  C.config -> V.symbolic_value -> SA.mplace option -> cm_fun
+
 (** If this mode is activated through the [config], greedily expand the symbolic
     values which need to be expanded. See {!C.config} for more information.
  *)
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 21027ff8..4dd03c1a 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -1029,10 +1029,8 @@ and eval_switch (config : C.config) (switch : A.switch) : st_cm_fun =
               | Some (_, tgt) -> eval_statement config tgt cf ctx)
           | V.Symbolic sv ->
               (* Expand the symbolic value - may lead to branching *)
-              let allow_branching = true in
               let cf_expand =
-                expand_symbolic_value config allow_branching sv
-                  (Some (S.mk_mplace p ctx))
+                expand_symbolic_adt config sv (Some (S.mk_mplace p ctx))
               in
               (* Re-evaluate the switch - the value is not symbolic anymore,
                  which means we will go to the other branch *)