Fix some bugs

8 files changed, 175 insertions, 85 deletions

diff --git a/compiler/Cps.ml b/compiler/Cps.ml
index 8763ff78..c0dd0ae2 100644
--- a/compiler/Cps.ml
+++ b/compiler/Cps.ml
@@ -16,7 +16,8 @@ type statement_eval_res =
   | Continue of int
   | Return
   | Panic
-  | LoopReturn  (** We reached a return statement *while inside a loop* *)
+  | LoopReturn of V.loop_id
+      (** We reached a return statement *while inside a loop* *)
   | EndEnterLoop of V.loop_id * V.typed_value V.SymbolicValueId.Map.t
       (** When we enter a loop, we delegate the end of the function is
           synthesized with a call to the loop translation. We use this
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index 82a9011c..7a72f8e3 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -1521,6 +1521,8 @@ end
     - to compute a mapping between the borrows and the symbolic values in a
       target context to the values and borrows in a source context (see
       {!match_ctx_with_target}).
+
+    TODO: rename
  *)
 module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
   module MkGetSetM (Id : Identifiers.Id) = struct
@@ -1599,7 +1601,7 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
     if S.check_equiv then GetSetSid.match_e S.sid_map
     else fun _ -> raise (Failure "Unexpected")
 
-  let match_value_with_sid (v : V.typed_value) (id : V.SymbolicValueId.id) :
+  let match_sid_with_value (id : V.SymbolicValueId.id) (v : V.typed_value) :
       unit =
     (* Even when we don't use it, the sids map contains the fixed ids: check
        that we are not trying to map a fixed id. *)
@@ -1611,9 +1613,6 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
     (* Add the mapping *)
     S.sid_to_value_map := V.SymbolicValueId.Map.add id v !S.sid_to_value_map
 
-  (*  let match_sidl = GetSetSid.match_el S.sid_map *)
-  (*  let match_sids = GetSetSid.match_es S.sid_map *)
-
   module GetSetAid = MkGetSetM (V.AbstractionId)
 
   let match_aid = GetSetAid.match_e S.aid_map
@@ -1666,9 +1665,9 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
 
   let match_symbolic_values (sv0 : V.symbolic_value) (sv1 : V.symbolic_value) :
       V.symbolic_value =
+    let id0 = sv0.sv_id in
     let id1 = sv1.sv_id in
     if S.check_equiv then
-      let id0 = sv0.sv_id in
       let sv_id = match_sid id0 id1 in
       let sv_ty = match_rtys sv0.V.sv_ty sv1.V.sv_ty in
       let sv_kind =
@@ -1677,7 +1676,7 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
       { V.sv_id; sv_ty; sv_kind }
     else (
       (* Update the binding for the target symbolic value *)
-      match_value_with_sid (mk_typed_value_from_symbolic_value sv0) id1;
+      match_sid_with_value id0 (mk_typed_value_from_symbolic_value sv1);
       (* Return - the returned value is not used, so we can return whatever *)
       sv1)
 
@@ -1685,9 +1684,9 @@ module MakeCheckEquivMatcher (S : MatchCheckEquivState) = struct
       (v : V.typed_value) : V.typed_value =
     if S.check_equiv then raise Distinct
     else (
-      assert (not left);
+      assert left;
       (* Update the binding for the target symbolic value *)
-      match_value_with_sid v sv.sv_id;
+      match_sid_with_value sv.sv_id v;
       (* Return - the returned value is not used, so we can return whatever *)
       v)
 
@@ -2122,8 +2121,7 @@ let loop_join_origin_with_continue_ctxs (config : C.config)
     the values which are read or modified (some symbolic values may be ignored).
  *)
 let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
-    (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) :
-    C.eval_ctx * ids_sets * V.symbolic_value list =
+    (eval_loop_body : st_cm_fun) (ctx0 : C.eval_ctx) : C.eval_ctx * ids_sets =
   (* The continuation for when we exit the loop - we register the
      environments upon loop *reentry*, and synthesize nothing by
      returning [None]
@@ -2143,7 +2141,7 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
         assert (i = 0);
         register_ctx ctx;
         None
-    | LoopReturn | EndEnterLoop _ | EndContinue _ ->
+    | LoopReturn _ | EndEnterLoop _ | EndContinue _ ->
         (* We don't support nested loops for now *)
         raise (Failure "Nested loops are not supported for now")
   in
@@ -2216,30 +2214,14 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
     let fixed_ids = { aids; blids; borrow_ids; loan_ids; dids; rids; sids } in
     fixed_ids
   in
-  let equiv_ctxs (ctx1 : C.eval_ctx) (ctx2 : C.eval_ctx) :
-      V.symbolic_value list option =
+  let equiv_ctxs (ctx1 : C.eval_ctx) (ctx2 : C.eval_ctx) : bool =
     let fixed_ids = compute_fixed_ids ctx1 ctx2 in
     let check_equivalent = true in
-    match match_ctxs check_equivalent fixed_ids ctx1 ctx2 with
-    | None -> None
-    | Some maps ->
-        (* Compute the list of symbolic value ids *)
-        let sidl =
-          List.map fst (V.SymbolicValueId.Map.bindings maps.sid_to_value_map)
-        in
-        (* Lookup the symbolic value themselves *)
-        let _, ids_to_values = compute_context_ids ctx1 in
-        let svl =
-          List.map
-            (fun sid ->
-              V.SymbolicValueId.Map.find sid ids_to_values.sids_to_values)
-            sidl
-        in
-        Some svl
+    Option.is_some (match_ctxs check_equivalent fixed_ids ctx1 ctx2)
   in
   let max_num_iter = Config.loop_fixed_point_max_num_iters in
   let rec compute_fixed_point (ctx : C.eval_ctx) (i0 : int) (i : int) :
-      C.eval_ctx * V.symbolic_value list =
+      C.eval_ctx =
     if i = 0 then
       raise
         (Failure
@@ -2262,11 +2244,9 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
           ^ "\n\n"));
 
       (* Check if we reached a fixed point: if not, iterate *)
-      match equiv_ctxs ctx ctx1 with
-      | Some svl -> (ctx1, svl)
-      | None -> compute_fixed_point ctx1 i0 (i - 1)
+      if equiv_ctxs ctx ctx1 then ctx1 else compute_fixed_point ctx1 i0 (i - 1)
   in
-  let fp, fp_svl = compute_fixed_point ctx0 max_num_iter max_num_iter in
+  let fp = compute_fixed_point ctx0 max_num_iter max_num_iter in
 
   (* Make sure we have exactly one loop abstraction per function region (merge
      abstractions accordingly).
@@ -2323,7 +2303,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 | LoopReturn | 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.
           *)
@@ -2434,22 +2414,13 @@ let compute_loop_entry_fixed_point (config : C.config) (loop_id : V.LoopId.id)
        while allowing exactly one iteration to see if it fails *)
     let _ = compute_fixed_point (update_kinds_can_end true fp) 1 1 in
 
-    (* Sanity check: the set of symbolic value ids is still valid *)
-    let _ =
-      let all_ids, _ = compute_context_ids fp in
-      let fp_sids =
-        V.SymbolicValueId.Set.of_list (List.map (fun sv -> sv.V.sv_id) fp_svl)
-      in
-      assert (V.SymbolicValueId.Set.subset fp_sids all_ids.sids)
-    in
-
     (* Return *)
     fp
   in
   let fixed_ids = compute_fixed_ids (Option.get !ctx_upon_entry) fp in
 
   (* Return *)
-  (fp, fixed_ids, fp_svl)
+  (fp, fixed_ids)
 
 (** Split an environment between the fixed abstractions, values, etc. and
     the new abstractions, values, etc.
@@ -3117,6 +3088,9 @@ let match_ctx_with_target (config : C.config) (loop_id : V.LoopId.id)
 (** Evaluate a loop in concrete mode *)
 let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun =
  fun cf ctx ->
+  (* We need a loop id for the [LoopReturn]. In practice it won't be used
+     (it is useful only for the symbolic execution *)
+  let loop_id = C.fresh_loop_id () in
   (* Continuation for after we evaluate the loop body: depending the result
      of doing one loop iteration:
      - redoes a loop iteration
@@ -3129,7 +3103,7 @@ 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 -> cf LoopReturn
+    | Return -> cf (LoopReturn loop_id)
     | Panic -> cf Panic
     | Break i ->
         (* Break out of the loop by calling the continuation *)
@@ -3150,7 +3124,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")
-    | LoopReturn | EndEnterLoop _ | EndContinue _ ->
+    | LoopReturn _ | EndEnterLoop _ | EndContinue _ ->
         (* We can't get there: this is only used in symbolic mode *)
         raise (Failure "Unreachable")
   in
@@ -3169,7 +3143,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
   (* Compute a fresh loop id *)
   let loop_id = C.fresh_loop_id () in
   (* Compute the fixed point at the loop entrance *)
-  let fp_ctx, fixed_ids, input_svalues =
+  let fp_ctx, fixed_ids =
     compute_loop_entry_fixed_point config loop_id eval_loop_body ctx
   in
 
@@ -3210,7 +3184,7 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
             fp_ctx
         in
         cc cf ctx
-    | Unit | LoopReturn | 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.
         *)
@@ -3219,14 +3193,29 @@ let eval_loop_symbolic (config : C.config) (eval_loop_body : st_cm_fun) :
   let loop_expr = eval_loop_body cf_loop fp_ctx in
 
   (* Compute the list of fresh symbolic values *)
-  let fresh_sids =
-    let input_sids =
-      V.SymbolicValueId.Set.of_list
-        (List.map (fun sv -> sv.V.sv_id) input_svalues)
+  let fresh_sids, input_svalues =
+    let old_ids, _ = compute_context_ids ctx in
+    let fp_ids, fp_ids_maps = compute_context_ids fp_ctx in
+    let fresh_sids = V.SymbolicValueId.Set.diff fp_ids.sids old_ids.sids in
+    (* The value ids should be listed in increasing order *)
+    let input_svalues =
+      List.map
+        (fun sid -> V.SymbolicValueId.Map.find sid fp_ids_maps.sids_to_values)
+        (V.SymbolicValueId.Set.elements fresh_sids)
     in
-    V.SymbolicValueId.Set.diff input_sids fixed_ids.sids
+    (fresh_sids, input_svalues)
   in
 
+  log#ldebug
+    (lazy
+      ("eval_loop_symbolic: result:" ^ "\n- src context:\n"
+     ^ eval_ctx_to_string ctx ^ "\n- fixed point:\n" ^ eval_ctx_to_string fp_ctx
+     ^ "\n- fixed_sids: "
+      ^ V.SymbolicValueId.Set.show fixed_ids.sids
+      ^ "\n- input_svalues: "
+      ^ V.SymbolicValueId.Set.show fresh_sids
+      ^ "\n\n"));
+
   (* Put together *)
   S.synthesize_loop loop_id input_svalues fresh_sids end_expr loop_expr
 
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index 7e4722b8..fe508f6b 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -851,8 +851,8 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
           (* Evaluation successful: evaluate the second statement *)
           | Unit -> eval_statement config st2 cf
           (* Control-flow break: transmit. We enumerate the cases on purpose *)
-          | Panic | Break _ | Continue _ | Return | LoopReturn | EndEnterLoop _
-          | EndContinue _ ->
+          | Panic | Break _ | Continue _ | Return | LoopReturn _
+          | EndEnterLoop _ | EndContinue _ ->
               cf res
         in
         (* Compose and apply *)
@@ -1100,8 +1100,8 @@ and eval_local_function_call_concrete (config : C.config) (fid : A.FunDeclId.id)
         (* Pop the stack frame, retrieve the return value, move it to
          * its destination and continue *)
         pop_frame_assign config dest (cf Unit)
-    | Break _ | Continue _ | Unit | LoopReturn | EndEnterLoop _ | EndContinue _
-      ->
+    | Break _ | Continue _ | Unit | LoopReturn _ | EndEnterLoop _
+    | EndContinue _ ->
         raise (Failure "Unreachable")
   in
   let cc = comp cc cf_finish in
diff --git a/compiler/Logging.ml b/compiler/Logging.ml
index 71f72471..706ea5cb 100644
--- a/compiler/Logging.ml
+++ b/compiler/Logging.ml
@@ -49,7 +49,7 @@ let borrows_log = L.get_logger "MainLogger.Interpreter.Borrows"
 let invariants_log = L.get_logger "MainLogger.Interpreter.Invariants"
 
 (** Logger for SCC *)
-let scc_log = L.get_logger "MainLogger.SCC"
+let scc_log = L.get_logger "MainLogger.Graph.SCC"
 
 (** Logger for ReorderDecls *)
-let reorder_decls_log = L.get_logger "MainLogger.ReorderDecls"
+let reorder_decls_log = L.get_logger "MainLogger.Graph.ReorderDecls"
diff --git a/compiler/Print.ml b/compiler/Print.ml
index 82c5dac5..e2bc3777 100644
--- a/compiler/Print.ml
+++ b/compiler/Print.ml
@@ -486,8 +486,8 @@ module Contexts = struct
     let frames = split_aux [] [] env in
     frames
 
-  let eval_ctx_to_string_gen (filter : bool) (ctx : C.eval_ctx) : string =
-    let fmt = eval_ctx_to_ctx_formatter ctx in
+  let fmt_eval_ctx_to_string_gen (fmt : ctx_formatter) (filter : bool)
+      (ctx : C.eval_ctx) : string =
     let ended_regions = T.RegionId.Set.to_string None ctx.ended_regions in
     let frames = split_env_according_to_frames ctx.env in
     let num_frames = List.length frames in
@@ -515,6 +515,10 @@ module Contexts = struct
     "# Ended regions: " ^ ended_regions ^ "\n" ^ "# " ^ string_of_int num_frames
     ^ " frame(s)\n" ^ String.concat "" frames
 
+  let eval_ctx_to_string_gen (filter : bool) (ctx : C.eval_ctx) : string =
+    let fmt = eval_ctx_to_ctx_formatter ctx in
+    fmt_eval_ctx_to_string_gen fmt filter ctx
+
   let eval_ctx_to_string (ctx : C.eval_ctx) : string =
     eval_ctx_to_string_gen true ctx
 
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index 10ce876f..6fb20b22 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -567,6 +567,7 @@ type fun_effect_info = {
   is_rec : bool;
       (** [true] if the function is recursive (or in a mutually recursive group) *)
 }
+[@@deriving show]
 
 (** Meta information about a function signature *)
 type fun_sig_info = {
@@ -585,6 +586,7 @@ type fun_sig_info = {
           with the state (if there is one) *)
   effect_info : fun_effect_info;
 }
+[@@deriving show]
 
 (** A function signature.
 
@@ -600,7 +602,7 @@ type fun_sig_info = {
       [in_ty0 -> ... -> in_tyn -> state -> back_in0 -> ... back_inm -> state ->
        result (state & (back_out0 & ... & back_outp))] (* state-error *)
        
-       Note that a stateful backward function takes two states as inputs: the
+       Note that a stateful backward function may take two states as inputs: the
        state received by the associated forward function, and the state at which
        the backward is called. This leads to code of the following shape:
 
@@ -611,7 +613,7 @@ type fun_sig_info = {
        ]}
 
     The function's type should be given by [mk_arrows sig.inputs sig.output].
-    We provide additional meta-information:
+    We provide additional meta-information with {!fun_sig.info}:
     - we divide between forward inputs and backward inputs (i.e., inputs specific
       to the forward functions, and additional inputs necessary if the signature is
       for a backward function)
@@ -622,7 +624,32 @@ type fun_sig_info = {
 type fun_sig = {
   type_params : type_var list;
   inputs : ty list;
+      (** The input types.
+
+          Note that those input types take into account the [fuel] parameter,
+          if the function uses fuel for termination, and the [state] parameter,
+          if the function is stateful.
+
+          For instance, if we have the following Rust function:
+          {[
+            fn f(x : int);
+          ]}
+
+          If we translate it to a stateful function which uses fuel we get:
+          {[
+            val f : nat -> int -> state -> result (state * unit);
+          ]}
+
+          In particular, the list of input types is: [[nat; int; state]].
+       *)
   output : ty;
+      (** The output type.
+
+          Note that this type contains the "effect" of the function (i.e., it is
+          not just a purification of the Rust return type). For instance, it will
+          be a tuple with a [state] if the function is stateful, and will be wrapped
+          in a [result] if the function can fail.
+       *)
   doutputs : ty list;
       (** The "decomposed" list of outputs.
 
@@ -641,9 +668,13 @@ type fun_sig = {
           - forward function:  [[T]]
           - backward function: [[T; T]] (for "x" and "y")
           
+          Non-decomposed ouputs (if the function can fail, but is not stateful):
+          - [result T]
+          - [[result (T * T)]
        *)
   info : fun_sig_info;  (** Additional information *)
 }
+[@@deriving show]
 
 (** An instantiated function signature. See {!fun_sig} *)
 type inst_fun_sig = {
@@ -652,6 +683,7 @@ type inst_fun_sig = {
   doutputs : ty list;
   info : fun_sig_info;
 }
+[@@deriving show]
 
 type fun_body = {
   inputs : var list;
@@ -660,6 +692,7 @@ type fun_body = {
           to replace unused variables by [_] *)
   body : texpression;
 }
+[@@deriving show]
 
 type fun_decl = {
   def_id : FunDeclId.id;
@@ -681,3 +714,4 @@ type fun_decl = {
   is_global_decl_body : bool;
   body : fun_body option;
 }
+[@@deriving show]
diff --git a/compiler/SCC.ml b/compiler/SCC.ml
index 2095c350..d9a4cd3e 100644
--- a/compiler/SCC.ml
+++ b/compiler/SCC.ml
@@ -94,15 +94,6 @@ module Make (Id : OrderedType) = struct
   *)
   let reorder_sccs (id_deps : Id.t list IdMap.t) (ids : Id.t list)
       (sccs : Id.t list list) : sccs =
-    log#ldebug
-      (lazy
-        ("reorder_sccs:" ^ "\n- id_deps: "
-        ^ IdMap.show (Print.list_to_string Id.show_t) id_deps
-        ^ "\n- ids: "
-        ^ Print.list_to_string Id.show_t ids
-        ^ "\n- sccs: "
-        ^ Print.list_to_string (Print.list_to_string Id.show_t) sccs));
-
     (* Map the identifiers to the SCC indices *)
     let id_to_scc =
       IdMap.of_list
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 006fdda7..f06e6542 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -9,6 +9,7 @@ module TA = TypesAnalysis
 module L = Logging
 module PP = PrintPure
 module FA = FunsAnalysis
+module IU = InterpreterUtils
 
 (** The local logger *)
 let log = L.symbolic_to_pure_log
@@ -23,6 +24,7 @@ type type_context = {
        *)
   types_infos : TA.type_infos; (* TODO: rename to type_infos *)
 }
+[@@deriving show]
 
 type fun_sig_named_outputs = {
   sg : fun_sig;  (** A function signature *)
@@ -37,14 +39,17 @@ type fun_sig_named_outputs = {
           which case we use those names).
        *)
 }
+[@@deriving show]
 
 type fun_context = {
   llbc_fun_decls : A.fun_decl A.FunDeclId.Map.t;
   fun_sigs : fun_sig_named_outputs RegularFunIdMap.t;  (** *)
   fun_infos : FA.fun_info A.FunDeclId.Map.t;
 }
+[@@deriving show]
 
 type global_context = { llbc_global_decls : A.global_decl A.GlobalDeclId.Map.t }
+[@@deriving show]
 
 (** Whenever we translate a function call or an ended abstraction, we
     store the related information (this is useful when translating ended
@@ -64,6 +69,7 @@ type call_info = {
           TODO: remove? it is also in the bs_ctx ("abstractions" field)
        *)
 }
+[@@deriving show]
 
 (** Contains information about a loop we entered.
 
@@ -101,9 +107,10 @@ type loop_info = {
   type_args : ty list;
   forward_inputs : texpression list option;
       (** The forward inputs are initialized at [None] *)
-  forward_output_no_state : var option;
+  forward_output_no_state_no_result : var option;
       (** The forward outputs are initialized at [None] *)
 }
+[@@deriving show]
 
 (** Body synthesis context *)
 type bs_ctx = {
@@ -179,6 +186,7 @@ type bs_ctx = {
           AST in a single function.
        *)
 }
+[@@deriving show]
 
 let type_check_pattern (ctx : bs_ctx) (v : typed_pattern) : unit =
   let env = VarId.Map.empty in
@@ -209,6 +217,22 @@ let bs_ctx_to_ast_formatter (ctx : bs_ctx) : Print.Ast.ast_formatter =
     ctx.fun_context.llbc_fun_decls ctx.global_context.llbc_global_decls
     ctx.fun_decl
 
+let bs_ctx_to_ctx_formatter (ctx : bs_ctx) : Print.Contexts.ctx_formatter =
+  let rvar_to_string = Print.Types.region_var_id_to_string in
+  let r_to_string = Print.Types.region_id_to_string in
+  let type_var_id_to_string = Print.Types.type_var_id_to_string in
+  let var_id_to_string = Print.Expressions.var_id_to_string in
+  let ast_fmt = bs_ctx_to_ast_formatter ctx in
+  {
+    Print.Values.rvar_to_string;
+    r_to_string;
+    type_var_id_to_string;
+    type_decl_id_to_string = ast_fmt.type_decl_id_to_string;
+    adt_variant_to_string = ast_fmt.adt_variant_to_string;
+    var_id_to_string;
+    adt_field_names = ast_fmt.adt_field_names;
+  }
+
 let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
   let type_params = ctx.fun_decl.signature.type_params in
   let type_decls = ctx.type_context.llbc_type_decls in
@@ -216,6 +240,11 @@ let bs_ctx_to_pp_ast_formatter (ctx : bs_ctx) : PrintPure.ast_formatter =
   let global_decls = ctx.global_context.llbc_global_decls in
   PrintPure.mk_ast_formatter type_decls fun_decls global_decls type_params
 
+let symbolic_value_to_string (ctx : bs_ctx) (sv : V.symbolic_value) : string =
+  let fmt = bs_ctx_to_ctx_formatter ctx in
+  let fmt = Print.PC.ctx_to_rtype_formatter fmt in
+  Print.PV.symbolic_value_to_string fmt sv
+
 let ty_to_string (ctx : bs_ctx) (ty : ty) : string =
   let fmt = bs_ctx_to_pp_ast_formatter ctx in
   let fmt = PrintPure.ast_to_type_formatter fmt in
@@ -843,7 +872,13 @@ let fresh_vars (vars : (string option * ty) list) (ctx : bs_ctx) :
   List.fold_left_map (fun ctx (name, ty) -> fresh_var name ty ctx) ctx vars
 
 let lookup_var_for_symbolic_value (sv : V.symbolic_value) (ctx : bs_ctx) : var =
-  V.SymbolicValueId.Map.find sv.sv_id ctx.sv_to_var
+  match V.SymbolicValueId.Map.find_opt sv.sv_id ctx.sv_to_var with
+  | Some v -> v
+  | None ->
+      raise
+        (Failure
+           ("Could not find var for symbolic value: "
+           ^ V.SymbolicValueId.to_string sv.sv_id))
 
 (** Peel boxes as long as the value is of the form [Box<T>] *)
 let rec unbox_typed_value (v : V.typed_value) : V.typed_value =
@@ -1319,7 +1354,8 @@ and translate_return_with_loop (loop_id : V.LoopId.id) (is_continue : bool)
     match ctx.bid with
     | None ->
         (* Forward *)
-        mk_texpression_from_var (Option.get loop_info.forward_output_no_state)
+        mk_texpression_from_var
+          (Option.get loop_info.forward_output_no_state_no_result)
     | Some bid ->
         (* Backward *)
         (* Group the variables in which we stored the values we need to give back.
@@ -1478,12 +1514,17 @@ and translate_end_abstraction (ectx : C.eval_ctx) (abs : V.abs)
   | V.FunCall (call_id, rg_id) ->
       translate_end_abstraction_fun_call ectx abs e ctx call_id rg_id
   | V.SynthRet rg_id -> translate_end_abstraction_synth_ret ectx abs e ctx rg_id
-  | Loop (loop_id, rg_id, abs_kind) ->
+  | V.Loop (loop_id, rg_id, abs_kind) ->
       translate_end_abstraction_loop ectx abs e ctx loop_id rg_id abs_kind
 
 and translate_end_abstraction_synth_input (ectx : C.eval_ctx) (abs : V.abs)
     (e : S.expression) (ctx : bs_ctx) (rg_id : T.RegionGroupId.id) : texpression
     =
+  log#ldebug
+    (lazy
+      ("translate_end_abstraction_synth_input:" ^ "\n- eval_ctx:\n"
+     ^ IU.eval_ctx_to_string ectx ^ "\n- abs:\n" ^ IU.abs_to_string ectx abs
+     ^ "\n"));
   (* When we end an input abstraction, this input abstraction gets back
    * the borrows which it introduced in the context through the input
    * values: by listing those values, we get the values which are given
@@ -1763,7 +1804,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
           ([ back_state ], ctx, Some nstate)
         else ([], ctx, None)
       in
-      (* Concatenate all the inpus *)
+      (* Concatenate all the inputs *)
       let inputs = List.concat [ fwd_inputs; back_inputs; back_state ] in
       (* Retrieve the values given back by this function *)
       let ctx, outputs = abs_to_given_back None abs ctx in
@@ -2057,12 +2098,11 @@ and translate_forward_end (ectx : C.eval_ctx)
     translate_expression e ctx
   in
 
-  (* If we entered/are entering a loop, we need to introduce a call to the
+  (* If we are (re-)entering a loop, we need to introduce a call to the
      forward translation of the loop. *)
   match loop_input_values with
   | None ->
-      (* "Regular" case: not a loop *)
-      assert (ctx.loop_id = None);
+      (* "Regular" case: we reached a return *)
       translate_end ctx
   | Some loop_input_values ->
       (* Loop *)
@@ -2089,7 +2129,7 @@ and translate_forward_end (ectx : C.eval_ctx)
 
       (* Introduce a fresh output value for the forward function *)
       let ctx, output_var =
-        let output_ty = ctx.sg.output in
+        let output_ty = mk_simpl_tuple_ty ctx.sg.doutputs in
         fresh_var None output_ty ctx
       in
       let args, ctx, out_pats =
@@ -2116,7 +2156,7 @@ and translate_forward_end (ectx : C.eval_ctx)
         {
           loop_info with
           forward_inputs = Some args;
-          forward_output_no_state = Some output_var;
+          forward_output_no_state_no_result = Some output_var;
         }
       in
       let ctx =
@@ -2145,6 +2185,33 @@ and translate_forward_end (ectx : C.eval_ctx)
 and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   let loop_id = V.LoopId.Map.find loop.loop_id ctx.loop_ids_map in
 
+  (* Translate the loop inputs - some inputs are symbolic values already
+     in the context, some inputs are introduced by the loop fixed point:
+     we need to introduce fresh variables for those. *)
+  (* First introduce fresh variables for the new inputs *)
+  let ctx =
+    (* We have to filter the list of symbolic values, to remove the not fresh ones *)
+    let svl =
+      List.filter
+        (fun (sv : V.symbolic_value) ->
+          V.SymbolicValueId.Set.mem sv.sv_id loop.fresh_svalues)
+        loop.input_svalues
+    in
+    log#ldebug
+      (lazy
+        ("translate_loop:" ^ "\n- filtered svl: "
+        ^ (Print.list_to_string (symbolic_value_to_string ctx)) svl));
+    let ctx, _ = fresh_vars_for_symbolic_values svl ctx in
+    ctx
+  in
+
+  (* Sanity check: all the non-fresh symbolic values are in the context *)
+  assert (
+    List.for_all
+      (fun (sv : V.symbolic_value) ->
+        V.SymbolicValueId.Map.mem sv.sv_id ctx.sv_to_var)
+      loop.input_svalues);
+
   (* Translate the loop inputs *)
   let inputs =
     List.map
@@ -2172,7 +2239,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
         input_svl = loop.input_svalues;
         type_args;
         forward_inputs = None;
-        forward_output_no_state = None;
+        forward_output_no_state_no_result = None;
       }
     in
     let loops = LoopId.Map.add loop_id loop_info ctx.loops in
@@ -2196,6 +2263,10 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
           V.SymbolicValueId.Set.mem sv.sv_id loop.fresh_svalues)
         loop.input_svalues
     in
+    log#ldebug
+      (lazy
+        ("translate_loop:" ^ "\n- filtered svl: "
+        ^ (Print.list_to_string (symbolic_value_to_string ctx)) svl));
     let ctx_loop, _ = fresh_vars_for_symbolic_values svl ctx_loop in
     ctx_loop
   in