Add span information to the generated code

12 files changed, 91 insertions, 45 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index fb3364f4..d7b4c152 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -1135,8 +1135,9 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment fmt
-    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ];
+  extract_comment_with_span fmt
+    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ]
+    def.meta.span;
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line *)
@@ -1197,8 +1198,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment fmt
-    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ];
+  extract_comment_with_span fmt
+    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ]
+    def.meta.span;
   F.pp_print_space fmt ();
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line *)
@@ -1251,8 +1253,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx)
   let def_name = ctx_get_decreases_proof def.def_id def.loop_id ctx in
   (* syntax <def_name> term ... term : tactic *)
   F.pp_print_break fmt 0 0;
-  extract_comment fmt
-    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ];
+  extract_comment_with_span fmt
+    [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ]
+    def.meta.span;
   F.pp_print_space fmt ();
   F.pp_open_hvbox fmt 0;
   F.pp_print_string fmt "syntax \"";
@@ -1313,7 +1316,7 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter)
     | [ s ] -> [ comment_pre ^ loop_comment ^ s ]
     | s :: sl -> (comment_pre ^ loop_comment ^ s) :: sl
   in
-  extract_comment fmt comment
+  extract_comment_with_span fmt comment def.meta.span
 
 (** Extract a function declaration.
 
@@ -1765,7 +1768,9 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter)
 
   (* Add a break then the name of the corresponding LLBC declaration *)
   F.pp_print_break fmt 0 0;
-  extract_comment fmt [ "[" ^ name_to_string ctx global.name ^ "]" ];
+  extract_comment_with_span fmt
+    [ "[" ^ name_to_string ctx global.name ^ "]" ]
+    global.meta.span;
   F.pp_print_space fmt ();
 
   let decl_name = ctx_get_global global.def_id ctx in
@@ -2190,8 +2195,9 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment fmt
-    [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ];
+  extract_comment_with_span fmt
+    [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ]
+    decl.meta.span;
   F.pp_print_break fmt 0 0;
   (* Open two outer boxes for the definition, so that whenever possible it gets printed on
      one line and indents are correct.
@@ -2478,8 +2484,9 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter)
   (* Add a break before *)
   F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment fmt
-    [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ];
+  extract_comment_with_span fmt
+    [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ]
+    impl.meta.span;
   F.pp_print_break fmt 0 0;
 
   (* Open two outer boxes for the definition, so that whenever possible it gets printed on
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index a74bd532..4dcefabc 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1813,6 +1813,17 @@ let extract_comment (fmt : F.formatter) (sl : string list) : unit =
   F.pp_print_string fmt rd;
   F.pp_close_box fmt ()
 
+let extract_comment_with_span (fmt : F.formatter) (sl : string list)
+    (span : Meta.span) : unit =
+  let file = match span.file with Virtual s | Local s -> s in
+  let span =
+    "Source: '" ^ file ^ "': lines "
+    ^ string_of_int span.beg_loc.line
+    ^ "-"
+    ^ string_of_int span.end_loc.line
+  in
+  extract_comment fmt (sl @ [ span ])
+
 let extract_trait_clause_type (ctx : extraction_ctx) (fmt : F.formatter)
     (no_params_tys : TypeDeclId.Set.t) (clause : trait_clause) : unit =
   let trait_name = ctx_get_trait_decl clause.trait_id ctx in
@@ -2034,7 +2045,9 @@ let extract_type_decl_gen (ctx : extraction_ctx) (fmt : F.formatter)
   if !backend <> HOL4 || not (decl_is_first_from_group kind) then
     F.pp_print_break fmt 0 0;
   (* Print a comment to link the extracted type to its original rust definition *)
-  extract_comment fmt [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ];
+  extract_comment_with_span fmt
+    [ "[" ^ name_to_string ctx def.llbc_name ^ "]" ]
+    def.meta.span;
   F.pp_print_break fmt 0 0;
   (* Open a box for the definition, so that whenever possible it gets printed on
    * one line. Note however that in the case of Lean line breaks are important
diff --git a/compiler/InterpreterLoops.ml b/compiler/InterpreterLoops.ml
index f88fc977..ed2a9587 100644
--- a/compiler/InterpreterLoops.ml
+++ b/compiler/InterpreterLoops.ml
@@ -2,6 +2,7 @@ open Types
 open Values
 open Contexts
 open ValuesUtils
+open Meta
 module S = SynthesizeSymbolic
 open Cps
 open InterpreterUtils
@@ -60,8 +61,8 @@ let eval_loop_concrete (eval_loop_body : st_cm_fun) : st_cm_fun =
   eval_loop_body reeval_loop_body ctx
 
 (** Evaluate a loop in symbolic mode *)
-let eval_loop_symbolic (config : config) (eval_loop_body : st_cm_fun) :
-    st_cm_fun =
+let eval_loop_symbolic (config : config) (meta : meta)
+    (eval_loop_body : st_cm_fun) : st_cm_fun =
  fun cf ctx ->
   (* Debug *)
   log#ldebug
@@ -205,9 +206,10 @@ let eval_loop_symbolic (config : config) (eval_loop_body : st_cm_fun) :
 
   (* Put together *)
   S.synthesize_loop loop_id input_svalues fresh_sids rg_to_given_back end_expr
-    loop_expr
+    loop_expr meta
 
-let eval_loop (config : config) (eval_loop_body : st_cm_fun) : st_cm_fun =
+let eval_loop (config : config) (meta : meta) (eval_loop_body : st_cm_fun) :
+    st_cm_fun =
  fun cf ctx ->
   match config.mode with
   | ConcreteMode -> eval_loop_concrete eval_loop_body cf ctx
@@ -231,4 +233,4 @@ let eval_loop (config : config) (eval_loop_body : st_cm_fun) : st_cm_fun =
          *non-fixed* abstractions.
       *)
       let cc = prepare_ashared_loans None in
-      comp cc (eval_loop_symbolic config eval_loop_body) cf ctx
+      comp cc (eval_loop_symbolic config meta eval_loop_body) cf ctx
diff --git a/compiler/InterpreterLoops.mli b/compiler/InterpreterLoops.mli
index 320e4bcb..03633861 100644
--- a/compiler/InterpreterLoops.mli
+++ b/compiler/InterpreterLoops.mli
@@ -58,6 +58,7 @@
 
 open Contexts
 open Cps
+open Meta
 
 (** Evaluate a loop *)
-val eval_loop : config -> st_cm_fun -> st_cm_fun
+val eval_loop : config -> meta -> st_cm_fun -> st_cm_fun
diff --git a/compiler/InterpreterStatements.ml b/compiler/InterpreterStatements.ml
index e8069e31..9ea5387f 100644
--- a/compiler/InterpreterStatements.ml
+++ b/compiler/InterpreterStatements.ml
@@ -739,7 +739,7 @@ let rec eval_statement (config : config) (st : statement) : st_cm_fun =
         (* Compose and apply *)
         comp cf_st1 cf_st2 cf ctx
     | Loop loop_body ->
-        InterpreterLoops.eval_loop config
+        InterpreterLoops.eval_loop config st.meta
           (eval_statement config loop_body)
           cf ctx
     | Switch switch -> eval_switch config switch cf ctx
diff --git a/compiler/PrintPure.ml b/compiler/PrintPure.ml
index 49e74b6c..5d8297d3 100644
--- a/compiler/PrintPure.ml
+++ b/compiler/PrintPure.ml
@@ -590,7 +590,7 @@ let rec texpression_to_string (env : fmt_env) (inside : bool) (indent : string)
           "[ " ^ String.concat ", " fields ^ " ]"
       | _ -> raise (Failure "Unexpected"))
   | Meta (meta, e) -> (
-      let meta_s = meta_to_string env meta in
+      let meta_s = emeta_to_string env meta in
       let e = texpression_to_string env inside indent indent_incr e in
       match meta with
       | Assignment _ | SymbolicAssignment _ | Tag _ ->
@@ -724,7 +724,7 @@ and loop_to_string (env : fmt_env) (indent : string) (indent_incr : string)
   ^ indent1 ^ "loop_body: {\n" ^ indent2 ^ loop_body ^ "\n" ^ indent1 ^ "}\n"
   ^ indent ^ "}"
 
-and meta_to_string (env : fmt_env) (meta : meta) : string =
+and emeta_to_string (env : fmt_env) (meta : emeta) : string =
   let meta =
     match meta with
     | Assignment (lp, rv, rp) ->
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index ebcaa68d..42f51075 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -48,6 +48,10 @@ type fun_decl_id = A.fun_decl_id [@@deriving show, ord]
 type loop_id = LoopId.id [@@deriving show, ord]
 type region_group_id = T.region_group_id [@@deriving show, ord]
 type mutability = Mut | Const [@@deriving show, ord]
+type loc = Meta.loc [@@deriving show, ord]
+type file_name = Meta.file_name [@@deriving show, ord]
+type span = Meta.span [@@deriving show, ord]
+type meta = Meta.meta [@@deriving show, ord]
 
 (** The assumed types for the pure AST.
 
@@ -389,6 +393,7 @@ type type_decl = {
           the name used at extraction time will be derived from the
           llbc_name.
        *)
+  meta : meta;
   generics : generic_params;
   kind : type_decl_kind;
   preds : predicates;
@@ -717,7 +722,7 @@ type expression =
   | Switch of texpression * switch_body
   | Loop of loop  (** See the comments for {!loop} *)
   | StructUpdate of struct_update  (** See the comments for {!struct_update} *)
-  | Meta of (meta[@opaque]) * texpression  (** Meta-information *)
+  | Meta of (emeta[@opaque]) * texpression  (** Meta-information *)
 
 and switch_body = If of texpression * texpression | Match of match_branch list
 and match_branch = { pat : typed_pattern; branch : texpression }
@@ -736,6 +741,7 @@ and match_branch = { pat : typed_pattern; branch : texpression }
 and loop = {
   fun_end : texpression;
   loop_id : loop_id;
+  meta : meta; [@opaque]
   fuel0 : var_id;
   fuel : var_id;
   input_state : var_id option;
@@ -791,7 +797,7 @@ and texpression = { e : expression; ty : ty }
 and mvalue = (texpression[@opaque])
 
 (** Meta-information stored in the AST *)
-and meta =
+and emeta =
   | Assignment of mplace * mvalue * mplace option
       (** Information about an assignment which occured in LLBC.
           We use this to guide the heuristics which derive pretty names.
@@ -993,6 +999,7 @@ type fun_kind = A.fun_kind [@@deriving show]
 type fun_decl = {
   def_id : FunDeclId.id;
   is_local : bool;
+  meta : meta;
   kind : fun_kind;
   num_loops : int;
       (** The number of loops in the parent forward function (basically the number
@@ -1019,6 +1026,7 @@ type trait_decl = {
   is_local : bool;
   llbc_name : llbc_name;
   name : string;
+  meta : meta;
   generics : generic_params;
   preds : predicates;
   parent_clauses : trait_clause list;
@@ -1034,6 +1042,7 @@ type trait_impl = {
   is_local : bool;
   llbc_name : llbc_name;
   name : string;
+  meta : meta;
   impl_trait : trait_decl_ref;
   generics : generic_params;
   preds : predicates;
diff --git a/compiler/PureMicroPasses.ml b/compiler/PureMicroPasses.ml
index 1565f252..8463f56c 100644
--- a/compiler/PureMicroPasses.ml
+++ b/compiler/PureMicroPasses.ml
@@ -391,7 +391,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       | Switch (scrut, body) -> update_switch_body scrut body ctx
       | Loop loop -> update_loop loop ctx
       | StructUpdate supd -> update_struct_update supd ctx
-      | Meta (meta, e) -> update_meta meta e ctx
+      | Meta (meta, e) -> update_emeta meta e ctx
     in
     (ctx, { e; ty })
   (* *)
@@ -449,6 +449,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     let {
       fun_end;
       loop_id;
+      meta;
       fuel0;
       fuel;
       input_state;
@@ -467,6 +468,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       {
         fun_end;
         loop_id;
+        meta;
         fuel0;
         fuel;
         input_state;
@@ -490,7 +492,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
     let supd = { struct_id; init; updates } in
     (ctx, StructUpdate supd)
   (* *)
-  and update_meta (meta : meta) (e : texpression) (ctx : pn_ctx) :
+  and update_emeta (meta : emeta) (e : texpression) (ctx : pn_ctx) :
       pn_ctx * expression =
     let ctx =
       match meta with
@@ -516,7 +518,7 @@ let compute_pretty_names (def : fun_decl) : fun_decl =
       | Tag _ -> ctx
     in
     let ctx, e = update_texpression e ctx in
-    let e = mk_meta meta e in
+    let e = mk_emeta meta e in
     (ctx, e.e)
   in
 
@@ -1428,6 +1430,7 @@ let decompose_loops (def : fun_decl) : fun_decl * fun_decl list =
               {
                 def_id = def.def_id;
                 is_local = def.is_local;
+                meta = loop.meta;
                 kind = def.kind;
                 num_loops;
                 loop_id = Some loop.loop_id;
diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml
index d410abdc..992ea499 100644
--- a/compiler/PureUtils.ml
+++ b/compiler/PureUtils.ml
@@ -453,13 +453,13 @@ let mk_dummy_pattern (ty : ty) : typed_pattern =
   let value = PatDummy in
   { value; ty }
 
-let mk_meta (m : meta) (e : texpression) : texpression =
+let mk_emeta (m : emeta) (e : texpression) : texpression =
   let ty = e.ty in
   let e = Meta (m, e) in
   { e; ty }
 
 let mk_mplace_texpression (mp : mplace) (e : texpression) : texpression =
-  mk_meta (MPlace mp) e
+  mk_emeta (MPlace mp) e
 
 let mk_opt_mplace_texpression (mp : mplace option) (e : texpression) :
     texpression =
@@ -649,6 +649,7 @@ let trait_decl_is_empty (trait_decl : trait_decl) : bool =
     is_local = _;
     name = _;
     llbc_name = _;
+    meta = _;
     generics = _;
     preds = _;
     parent_clauses;
@@ -668,6 +669,7 @@ let trait_impl_is_empty (trait_impl : trait_impl) : bool =
     is_local = _;
     name = _;
     llbc_name = _;
+    meta = _;
     impl_trait = _;
     generics = _;
     preds = _;
diff --git a/compiler/SymbolicAst.ml b/compiler/SymbolicAst.ml
index c9820ba5..a9f45926 100644
--- a/compiler/SymbolicAst.ml
+++ b/compiler/SymbolicAst.ml
@@ -51,11 +51,10 @@ type call = {
 }
 [@@deriving show]
 
-(** Meta information, not necessary for synthesis but useful to guide it to
-    generate a pretty output.
+(** Meta information for expressions, not necessary for synthesis but useful to
+    guide it to generate a pretty output.
  *)
-
-type meta =
+type emeta =
   | Assignment of Contexts.eval_ctx * mplace * typed_value * mplace option
       (** We generated an assignment (destination, assigned value, src) *)
 [@@deriving show]
@@ -82,7 +81,8 @@ class ['self] iter_expression_base =
       fun _ _ -> ()
 
     method visit_mplace : 'env -> mplace -> unit = fun _ _ -> ()
-    method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
+    method visit_emeta : 'env -> emeta -> unit = fun _ _ -> ()
+    method visit_meta : 'env -> Meta.meta -> unit = fun _ _ -> ()
 
     method visit_region_group_id_map
         : 'a. ('env -> 'a -> unit) -> 'env -> 'a region_group_id_map -> unit =
@@ -200,7 +200,7 @@ type expression =
 
           The boolean is [is_continue].
        *)
-  | Meta of meta * expression  (** Meta information *)
+  | Meta of emeta * expression  (** Meta information *)
 
 and loop = {
   loop_id : loop_id;
@@ -215,6 +215,7 @@ and loop = {
   end_expr : expression;
       (** The end of the function (upon the moment it enters the loop) *)
   loop_expr : expression;  (** The symbolically executed loop body *)
+  meta : Meta.meta;  (** Information about where the origin of the loop body *)
 }
 
 and expansion =
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml
index 9899a0c6..5dee23db 100644
--- a/compiler/SymbolicToPure.ml
+++ b/compiler/SymbolicToPure.ml
@@ -496,7 +496,8 @@ let translate_type_decl (ctx : Contexts.decls_ctx) (def : T.type_decl) :
   let kind = translate_type_decl_kind def.T.kind in
   let preds = translate_predicates def.preds in
   let is_local = def.is_local in
-  { def_id; is_local; llbc_name; name; generics; kind; preds }
+  let meta = def.meta in
+  { def_id; is_local; llbc_name; name; meta; generics; kind; preds }
 
 let translate_type_id (id : T.type_id) : type_id =
   match id with
@@ -1489,11 +1490,11 @@ let get_abs_ancestors (ctx : bs_ctx) (abs : V.abs) (call_id : V.FunCallId.id) :
   (call_info.forward, abs_ancestors)
 
 (** Add meta-information to an expression *)
-let mk_meta_symbolic_assignments (vars : var list) (values : texpression list)
+let mk_emeta_symbolic_assignments (vars : var list) (values : texpression list)
     (e : texpression) : texpression =
   let var_values = List.combine vars values in
   List.fold_right
-    (fun (var, arg) e -> mk_meta (SymbolicAssignment (var_get_id var, arg)) e)
+    (fun (var, arg) e -> mk_emeta (SymbolicAssignment (var_get_id var, arg)) e)
     var_values e
 
 let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
@@ -1509,7 +1510,7 @@ let rec translate_expression (e : S.expression) (ctx : bs_ctx) : texpression =
   | Expansion (p, sv, exp) -> translate_expansion p sv exp ctx
   | IntroSymbolic (ectx, p, sv, v, e) ->
       translate_intro_symbolic ectx p sv v e ctx
-  | Meta (meta, e) -> translate_meta meta e ctx
+  | Meta (meta, e) -> translate_emeta meta e ctx
   | ForwardEnd (ectx, loop_input_values, e, back_e) ->
       translate_forward_end ectx loop_input_values e back_e ctx
   | Loop loop -> translate_loop loop ctx
@@ -2206,7 +2207,7 @@ and translate_end_abstraction_loop (ectx : C.eval_ctx) (abs : V.abs)
                 var_values
             in
             let vars, values = List.split var_values in
-            mk_meta_symbolic_assignments vars values next_e
+            mk_emeta_symbolic_assignments vars values next_e
           else next_e
         in
 
@@ -2637,7 +2638,7 @@ and translate_forward_end (ectx : C.eval_ctx)
          We then remove all the meta information from the body *before* calling
          {!PureMicroPasses.decompose_loops}.
       *)
-      mk_meta_symbolic_assignments loop_info.input_vars org_args e
+      mk_emeta_symbolic_assignments loop_info.input_vars org_args e
 
 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
@@ -2795,6 +2796,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
       {
         fun_end;
         loop_id;
+        meta = loop.meta;
         fuel0 = ctx.fuel0;
         fuel = ctx.fuel;
         input_state;
@@ -2810,7 +2812,7 @@ and translate_loop (loop : S.loop) (ctx : bs_ctx) : texpression =
   let ty = fun_end.ty in
   { e = loop; ty }
 
-and translate_meta (meta : S.meta) (e : S.expression) (ctx : bs_ctx) :
+and translate_emeta (meta : S.emeta) (e : S.expression) (ctx : bs_ctx) :
     texpression =
   let next_e = translate_expression e ctx in
   let meta =
@@ -3028,6 +3030,7 @@ let translate_fun_decl (ctx : bs_ctx) (body : S.expression option) : fun_decl =
     {
       def_id;
       is_local = def.is_local;
+      meta = def.meta;
       kind = def.kind;
       num_loops;
       loop_id;
@@ -3108,6 +3111,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     def_id;
     is_local;
     name = llbc_name;
+    meta;
     generics;
     preds;
     parent_clauses;
@@ -3145,6 +3149,7 @@ let translate_trait_decl (ctx : Contexts.decls_ctx) (trait_decl : A.trait_decl)
     is_local;
     llbc_name;
     name;
+    meta;
     generics;
     preds;
     parent_clauses;
@@ -3160,6 +3165,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     A.def_id;
     is_local;
     name = llbc_name;
+    meta;
     impl_trait;
     generics;
     preds;
@@ -3201,6 +3207,7 @@ let translate_trait_impl (ctx : Contexts.decls_ctx) (trait_impl : A.trait_impl)
     is_local;
     llbc_name;
     name;
+    meta;
     impl_trait;
     generics;
     preds;
diff --git a/compiler/SynthesizeSymbolic.ml b/compiler/SynthesizeSymbolic.ml
index 9e14a4d6..efcf001a 100644
--- a/compiler/SynthesizeSymbolic.ml
+++ b/compiler/SynthesizeSymbolic.ml
@@ -15,7 +15,7 @@ let mk_opt_place_from_op (op : operand) (ctx : Contexts.eval_ctx) :
     mplace option =
   match op with Copy p | Move p -> Some (mk_mplace p ctx) | Constant _ -> None
 
-let mk_meta (m : meta) (e : expression) : expression = Meta (m, e)
+let mk_emeta (m : emeta) (e : expression) : expression = Meta (m, e)
 
 let synthesize_symbolic_expansion (sv : symbolic_value) (place : mplace option)
     (seel : symbolic_expansion option list) (el : expression list option) :
@@ -163,8 +163,8 @@ let synthesize_forward_end (ctx : Contexts.eval_ctx)
 let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list)
     (fresh_svalues : SymbolicValueId.Set.t)
     (rg_to_given_back_tys : (RegionId.Set.t * ty list) RegionGroupId.Map.t)
-    (end_expr : expression option) (loop_expr : expression option) :
-    expression option =
+    (end_expr : expression option) (loop_expr : expression option)
+    (meta : Meta.meta) : expression option =
   match (end_expr, loop_expr) with
   | None, None -> None
   | Some end_expr, Some loop_expr ->
@@ -177,5 +177,6 @@ let synthesize_loop (loop_id : LoopId.id) (input_svalues : symbolic_value list)
              rg_to_given_back_tys;
              end_expr;
              loop_expr;
+             meta;
            })
   | _ -> raise (Failure "Unreachable")