Add span information to the generated code

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

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

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

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

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

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) ->

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;

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;

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 = _;

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 =