Make progress on Interpreter.ml

1 files changed, 80 insertions, 65 deletions

diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index e68790d4..48292968 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -245,7 +245,7 @@ let compute_abs_borrows_loans_maps (no_duplicates : bool)
 (** Destructure all the new abstractions *)
 let destructure_new_abs (loop_id : V.LoopId.id)
     (old_abs_ids : V.AbstractionId.Set.t) (ctx : C.eval_ctx) : C.eval_ctx =
-  let abs_kind = V.Loop (loop_id, None) in
+  let abs_kind = V.Loop (loop_id, None, V.LoopSynthInput) in
   let can_end = false in
   let destructure_shared_values = true in
   let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
@@ -336,7 +336,7 @@ let collapse_ctx (loop_id : V.LoopId.id)
       ("collapse_ctx:\n\n- fixed_ids:\n" ^ show_ids_sets old_ids
      ^ "\n\n- ctx0:\n" ^ eval_ctx_to_string ctx0 ^ "\n\n"));
 
-  let abs_kind = V.Loop (loop_id, None) in
+  let abs_kind = V.Loop (loop_id, None, LoopSynthInput) in
   let can_end = false in
   let destructure_shared_values = true in
   let is_fresh_abs_id (id : V.AbstractionId.id) : bool =
@@ -966,7 +966,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
       let abs =
         {
           V.abs_id = C.fresh_abstraction_id ();
-          kind = V.Loop (S.loop_id, None);
+          kind = V.Loop (S.loop_id, None, LoopSynthInput);
           can_end = false;
           parents = V.AbstractionId.Set.empty;
           original_parents = [];
@@ -1020,7 +1020,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
       let abs =
         {
           V.abs_id = C.fresh_abstraction_id ();
-          kind = V.Loop (S.loop_id, None);
+          kind = V.Loop (S.loop_id, None, LoopSynthInput);
           can_end = false;
           parents = V.AbstractionId.Set.empty;
           original_parents = [];
@@ -1124,7 +1124,7 @@ module MakeJoinMatcher (S : MatchJoinState) : Matcher = struct
             else raise (ValueMatchFailure (LoanInRight id)))
     | None ->
         (* Convert the value to an abstraction *)
-        let abs_kind = V.Loop (S.loop_id, None) in
+        let abs_kind = V.Loop (S.loop_id, None, LoopSynthInput) in
         let can_end = false in
         let destructure_shared_values = true in
         let absl =
@@ -1691,9 +1691,16 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
       (* Return - the returned value is not used, so we can return whatever *)
       v)
 
-  let match_bottom_with_other (_left : bool) (_v : V.typed_value) :
-      V.typed_value =
-    raise Distinct
+  let match_bottom_with_other (left : bool) (v : V.typed_value) : V.typed_value
+      =
+    (* It can happen that some variables get initialized in some branches
+       and not in some others, which causes problems when matching. *)
+    (* TODO: the returned value is not used, while it should: in generality it
+       should be ok to match a fixed-point with the environment we get at
+       a continue, where the fixed point contains some bottom values. *)
+    if left && not (value_has_loans_or_borrows S.ctx v.V.value) then
+      mk_bottom v.V.ty
+    else raise Distinct
 
   let match_distinct_aadts _ _ _ _ _ = raise Distinct
 
@@ -2131,7 +2138,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
         assert (i = 0);
         register_ctx ctx;
         None
-    | EndEnterLoop | EndContinue ->
+    | LoopReturn | EndEnterLoop _ | EndContinue _ ->
         (* We don't support nested loops for now *)
         raise (Failure "Nested loops are not supported for now")
   in
@@ -2246,15 +2253,16 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
 
     let list_loop_abstractions =
       object
-        inherit [_] C.map_eval_ctx as super
+        inherit [_] C.map_eval_ctx
 
-        method! visit_abs env abs =
+        method! visit_abs _ abs =
           match abs.kind with
-          | Loop (loop_id', _) ->
+          | Loop (loop_id', _, kind) ->
               assert (loop_id' = loop_id);
+              assert (kind = V.LoopSynthInput);
               add_aid abs.abs_id;
               { abs with can_end = true }
-          | _ -> super#visit_abs env abs
+          | _ -> abs
       end
     in
     let fp = list_loop_abstractions#visit_eval_ctx () fp in
@@ -2285,7 +2293,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
       | Break _ ->
           (* We enforce that we can't get there: see {!PrePasses.remove_loop_breaks} *)
           raise (Failure "Unreachable")
-      | Unit | EndEnterLoop | EndContinue ->
+      | Unit | LoopReturn | EndEnterLoop _ | EndContinue _ ->
           (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}.
              For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now.
           *)
@@ -2349,7 +2357,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
           | id0 :: ids ->
               let id0 = ref id0 in
               (* Add the proper region group into the abstraction *)
-              let abs_kind = V.Loop (loop_id, Some rg_id) in
+              let abs_kind = V.Loop (loop_id, Some rg_id, V.LoopSynthInput) in
               let abs = C.ctx_lookup_abs !fp !id0 in
               let abs = { abs with V.kind = abs_kind } in
               let fp', _ = C.ctx_subst_abs !fp !id0 abs in
@@ -2372,17 +2380,19 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
     (* Reset the loop abstracions as not endable *)
     let list_loop_abstractions (remove_rg_id : bool) =
       object
-        inherit [_] C.map_eval_ctx as super
+        inherit [_] C.map_eval_ctx
 
-        method! visit_abs env abs =
+        method! visit_abs _ abs =
           match abs.kind with
-          | Loop (loop_id', _) ->
+          | Loop (loop_id', _, kind) ->
               assert (loop_id' = loop_id);
+              assert (kind = V.LoopSynthInput);
               let kind =
-                if remove_rg_id then V.Loop (loop_id, None) else abs.kind
+                if remove_rg_id then V.Loop (loop_id, None, V.LoopSynthInput)
+                else abs.kind
               in
               { abs with can_end = false; kind }
-          | _ -> super#visit_abs env abs
+          | _ -> abs
       end
     in
     let update_kinds_can_end (remove_rg_id : bool) ctx =
@@ -2402,38 +2412,6 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
   (* Return *)
   (fp, fixed_ids)
 
-(*
-(** Introduce region groups in the loop abstractions.
-
-    Initially, the new abstractions in the fixed-point have no region group.
-    We want each one of them to have a unique region group (because we will
-    translate each one of those abstractions to a pair forward
-    function/backward function).
- *)
-let ctx_add_loop_region_groups (loop_id : V.LoopId.id) (fp : C.eval_ctx) :
-    C.eval_ctx =
-  let _, fresh_rid = T.RegionGroupId.fresh_stateful_generator () in
-
-  let introduce_fresh_rids =
-    object
-      inherit [_] C.map_eval_ctx
-
-      method! visit_abs _ abs =
-        match abs.kind with
-        | Loop (loop_id', rg_id) ->
-            assert (loop_id' = loop_id);
-            assert (rg_id = None);
-            let rg_id = Some (fresh_rid ()) in
-            let kind = V.Loop (loop_id, rg_id) in
-            { abs with V.kind }
-        | _ -> abs
-    end
-  in
-  let fp_env = List.rev (introduce_fresh_rids#visit_env () (List.rev fp.env)) in
-  let fp = { fp with env = fp_env } in
-  fp
- *)
-
 (** Split an environment between the fixed abstractions, values, etc. and
     the new abstractions, values, etc.
 
@@ -2452,7 +2430,7 @@ let ctx_split_fixed_new (fixed_ids : ids_sets) (ctx : C.eval_ctx) :
   let is_fresh (ee : C.env_elem) : bool =
     match ee with
     | C.Var (VarBinder _, _) | C.Frame -> false
-    | C.Var (DummyBinder bv, _) -> not (is_fresh_did bv)
+    | C.Var (DummyBinder bv, _) -> is_fresh_did bv
     | C.Abs abs -> is_fresh_abs_id abs.abs_id
   in
   let new_eel, filt_env = List.partition is_fresh ctx.env in
@@ -2785,6 +2763,11 @@ let compute_fixed_point_id_correspondance (fixed_ids : ids_sets)
    values, if they contain borrows - above i points to [s@7], but it should
    be a different symbolic value...).
 
+   Finally, we use the map from symbolic values to values to compute the list of
+   input values of the loop: we simply list the values, by order of increasing
+   symbolic value id. We *do* use the fixed values (though they are in the frame)
+   because they may be *read* inside the loop.
+
    We can then proceed to finishing the symbolic execution and doing the
    synthesis.
 
@@ -2799,8 +2782,9 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
   (* Debug *)
   log#ldebug
     (lazy
-      ("match_ctx_with_target:\n" ^ "\n- src_ctx: " ^ eval_ctx_to_string src_ctx
-     ^ "\n- tgt_ctx: " ^ eval_ctx_to_string tgt_ctx));
+      ("match_ctx_with_target:\n" ^ "\n- fixed_ids: " ^ show_ids_sets fixed_ids
+     ^ "\n\n- src_ctx: " ^ eval_ctx_to_string src_ctx ^ "\n- tgt_ctx: "
+     ^ eval_ctx_to_string tgt_ctx));
 
   (* We first reorganize [src_ctx] so that we can match it with [tgt_ctx] *)
   let rec cf_reorganize_src : cm_fun =
@@ -2810,6 +2794,14 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
     let filt_src_env, _, _ = ctx_split_fixed_new fixed_ids src_ctx in
     let filt_tgt_env, _, _ = ctx_split_fixed_new fixed_ids tgt_ctx in
 
+    log#ldebug
+      (lazy
+        ("match_ctx_with_target:\n" ^ "\n- fixed_ids: "
+       ^ show_ids_sets fixed_ids ^ "\n\n- filt_src_ctx: "
+        ^ env_to_string src_ctx filt_src_env
+        ^ "\n- filt_tgt_ctx: "
+        ^ env_to_string tgt_ctx filt_tgt_env));
+
     (* Remove the abstractions *)
     let filter (ee : C.env_elem) : bool =
       match ee with Var _ -> true | Abs _ | Frame -> false
@@ -3010,7 +3002,7 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
     in
     let visit_tgt =
       object
-        inherit [_] C.map_eval_ctx
+        inherit [_] C.map_eval_ctx as super
 
         method! visit_borrow_id _ bid =
           (* Lookup the id of the loan corresponding to this borrow *)
@@ -3032,6 +3024,17 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
         method! visit_symbolic_value_id _ _ = C.fresh_symbolic_value_id ()
         method! visit_abstraction_id _ _ = C.fresh_abstraction_id ()
         method! visit_region_id _ id = get_rid id
+
+        (** We also need to change the abstraction kind *)
+        method! visit_abs env abs =
+          match abs.kind with
+          | V.Loop (loop_id', rg_id, kind) ->
+              assert (loop_id' = loop_id);
+              assert (kind = V.LoopSynthInput);
+              let kind = V.Loop (loop_id, rg_id, V.LoopSynthRet) in
+              let abs = { abs with kind } in
+              super#visit_abs env abs
+          | _ -> super#visit_abs env abs
       end
     in
     let new_absl = List.map (visit_tgt#visit_abs ()) new_absl in
@@ -3058,8 +3061,19 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
     in
     let cc = InterpreterBorrows.end_borrows config new_borrows in
 
+    (* List the loop input values - when iterating over a map, we iterate
+       over the keys, in increasing order *)
+    let input_values =
+      List.map snd
+        (V.SymbolicValueId.Map.bindings tgt_to_src_maps.sid_to_value_map)
+    in
+
     (* Continue *)
-    cc (cf (if is_loop_entry then EndEnterLoop else EndContinue)) src_ctx
+    cc
+      (cf
+         (if is_loop_entry then EndEnterLoop input_values
+         else EndContinue input_values))
+      src_ctx
   in
 
   (* Compose and continue *)
@@ -3080,7 +3094,8 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun =
   *)
   let rec reeval_loop_body (res : statement_eval_res) : m_fun =
     match res with
-    | Return | Panic -> cf res
+    | Return -> cf LoopReturn
+    | Panic -> cf Panic
     | Break i ->
         (* Break out of the loop by calling the continuation *)
         let res = if i = 0 then Unit else Break (i - 1) in
@@ -3100,7 +3115,7 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun =
          * We prefer to write it this way for consistency and sanity,
          * though. *)
         raise (Failure "Unreachable")
-    | EndEnterLoop | EndContinue ->
+    | LoopReturn | EndEnterLoop _ | EndContinue _ ->
         (* We can't get there: this is only used in symbolic mode *)
         raise (Failure "Unreachable")
   in
@@ -3155,12 +3170,12 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
     | Continue i ->
         (* We don't support nested loops for now *)
         assert (i = 0);
-        let fp_bl_corresp =
-          compute_fixed_point_id_correspondance fixed_ids ctx fp_ctx
+        let cc =
+          match_ctx_with_target config loop_id false fp_bl_corresp fixed_ids
+            fp_ctx
         in
-        match_ctx_with_target config loop_id false fp_bl_corresp fixed_ids
-          fp_ctx cf ctx
-    | Unit | EndEnterLoop | EndContinue ->
+        cc cf ctx
+    | Unit | LoopReturn | EndEnterLoop _ | EndContinue _ ->
         (* For why we can't get [Unit], see the comments inside {!eval_loop_concrete}.
            For [EndEnterLoop] and [EndContinue]: we don't support nested loops for now.
         *)
@@ -3169,7 +3184,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
   let loop_expr = eval_loop_body cf_loop fp_ctx in
 
   (* Put together *)
-  S.synthesize_loop end_expr loop_expr
+  S.synthesize_loop loop_id end_expr loop_expr
 
 (** Evaluate a loop *)
 let eval_loop (config : C.config) (eval_loop_body : st_cm_fun) : st_cm_fun =