Add meta data with code locations to the various definitions

10 files changed, 326 insertions, 110 deletions

diff --git a/.gitignore b/.gitignore
index 8713e6e4..1f9bd6a1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -43,7 +43,6 @@ tests/misc/obj/
 /fstar-tests
 *~
 nohup.out
-.ocamlformat
 .vscode
 *#
 *.lock
diff --git a/src/.ocamlformat b/src/.ocamlformat
new file mode 100644
index 00000000..b0ae150e
--- /dev/null
+++ b/src/.ocamlformat
@@ -0,0 +1 @@
+doc-comments=before
\ No newline at end of file
diff --git a/src/InterpreterStatements.ml b/src/InterpreterStatements.ml
index ae9e59fe..275a6c58 100644
--- a/src/InterpreterStatements.ml
+++ b/src/InterpreterStatements.ml
@@ -810,7 +810,7 @@ let rec eval_statement (config : C.config) (st : A.statement) : st_cm_fun =
   (* Evaluate *)
   let cf_eval_st cf : m_fun =
    fun ctx ->
-    match st with
+    match st.content with
     | A.Assign (p, rvalue) ->
         (* Evaluate the rvalue *)
         let cf_eval_rvalue = eval_rvalue config rvalue in
diff --git a/src/LlbcAst.ml b/src/LlbcAst.ml
index ccc870dc..cecd3594 100644
--- a/src/LlbcAst.ml
+++ b/src/LlbcAst.ml
@@ -5,7 +5,9 @@ open Expressions
 open Identifiers
 module FunDeclId = IdGen ()
 module GlobalDeclId = IdGen ()
+open Meta
 
+(** A variable, as used in a function definition *)
 type var = {
   index : VarId.id;  (** Unique variable identifier *)
   name : string option;
@@ -15,7 +17,6 @@ type var = {
        ** variables manipulated by a function body *)
 }
 [@@deriving show]
-(** A variable, as used in a function definition *)
 
 type assumed_fun_id =
   | Replace  (** `core::mem::replace` *)
@@ -47,6 +48,7 @@ type abs_region_group = (AbstractionId.id, RegionId.id) g_region_group
 type abs_region_groups = (AbstractionId.id, RegionId.id) g_region_groups
 [@@deriving show]
 
+(** A function signature, as used when declaring functions *)
 type fun_sig = {
   region_params : region_var list;
   num_early_bound_regions : int;
@@ -56,15 +58,14 @@ type fun_sig = {
   output : sty;
 }
 [@@deriving show]
-(** A function signature, as used when declaring functions *)
 
+(** A function signature, after instantiation *)
 type inst_fun_sig = {
   regions_hierarchy : abs_region_groups;
   inputs : rty list;
   output : rty;
 }
 [@@deriving show]
-(** A function signature, after instantiation *)
 
 type call = {
   func : fun_id;
@@ -83,6 +84,7 @@ class ['self] iter_statement_base =
     method visit_global_assignment : 'env -> global_assignment -> unit =
       fun _ _ -> ()
 
+    method visit_meta : 'env -> meta -> unit = fun _ _ -> ()
     method visit_place : 'env -> place -> unit = fun _ _ -> ()
     method visit_rvalue : 'env -> rvalue -> unit = fun _ _ -> ()
     method visit_id : 'env -> VariantId.id -> unit = fun _ _ -> ()
@@ -102,6 +104,7 @@ class ['self] map_statement_base =
         : 'env -> global_assignment -> global_assignment =
       fun _ x -> x
 
+    method visit_meta : 'env -> meta -> meta = fun _ x -> x
     method visit_place : 'env -> place -> place = fun _ x -> x
     method visit_rvalue : 'env -> rvalue -> rvalue = fun _ x -> x
     method visit_id : 'env -> VariantId.id -> VariantId.id = fun _ x -> x
@@ -116,7 +119,12 @@ class ['self] map_statement_base =
       fun _ x -> x
   end
 
-type statement =
+type statement = {
+  meta : meta;  (** The statement meta-data *)
+  content : raw_statement;  (** The statement itself *)
+}
+
+and raw_statement =
   | Assign of place * rvalue
   | AssignGlobal of global_assignment
   | FakeRead of place
@@ -169,11 +177,17 @@ and switch_targets =
         concrete = true;
       }]
 
-type fun_body = { arg_count : int; locals : var list; body : statement }
+type fun_body = {
+  meta : meta;
+  arg_count : int;
+  locals : var list;
+  body : statement;
+}
 [@@deriving show]
 
 type fun_decl = {
   def_id : FunDeclId.id;
+  meta : meta;
   name : fun_name;
   signature : fun_sig;
   body : fun_body option;
@@ -183,6 +197,7 @@ type fun_decl = {
 
 type global_decl = {
   def_id : GlobalDeclId.id;
+  meta : meta;
   body_id : FunDeclId.id;
   name : global_name;
   ty : ety;
diff --git a/src/LlbcOfJson.ml b/src/LlbcOfJson.ml
index 44abedf2..8598962e 100644
--- a/src/LlbcOfJson.ml
+++ b/src/LlbcOfJson.ml
@@ -11,6 +11,8 @@
 open Yojson.Basic
 open Names
 open OfJsonBasic
+open Identifiers
+open Meta
 module T = Types
 module V = Values
 module S = Scalars
@@ -18,12 +20,108 @@ module E = Expressions
 module A = LlbcAst
 module TU = TypesUtils
 module AU = LlbcAstUtils
+module LocalFileId = IdGen ()
+module VirtualFileId = IdGen ()
 
-(* The default logger *)
+(** The default logger *)
 let log = Logging.llbc_of_json_logger
 
+(** A file identifier *)
+type file_id = LocalId of LocalFileId.id | VirtualId of VirtualFileId.id
+[@@deriving show, ord]
+
+module OrderedIdToFile : Collections.OrderedType with type t = file_id = struct
+  type t = file_id
+
+  let compare fid0 fid1 = compare_file_id fid0 fid1
+
+  let to_string id =
+    match id with
+    | LocalId id -> "Local " ^ LocalFileId.to_string id
+    | VirtualId id -> "Virtual " ^ VirtualFileId.to_string id
+
+  let pp_t fmt x = Format.pp_print_string fmt (to_string x)
+  let show_t x = to_string x
+end
+
+module IdToFile = Collections.MakeMap (OrderedIdToFile)
+
+type id_to_file_map = file_name IdToFile.t
+
+let file_id_of_json (js : json) : (file_id, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("LocalId", id) ] ->
+        let* id = LocalFileId.id_of_json id in
+        Ok (LocalId id)
+    | `Assoc [ ("VirtualId", id) ] ->
+        let* id = VirtualFileId.id_of_json id in
+        Ok (VirtualId id)
+    | _ -> Error "")
+
+let file_name_of_json (js : json) : (file_name, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("Virtual", name) ] ->
+        let* name = string_of_json name in
+        Ok (Virtual name)
+    | `Assoc [ ("Local", name) ] ->
+        let* name = string_of_json name in
+        Ok (Local name)
+    | _ -> Error "")
+
+(** Deserialize a map from file id to file name.
+
+    In the serialized LLBC, the files in the loc spans are refered to by their
+    ids, in order to save space. In a functional language like OCaml this is
+    not necessary: we thus replace the file ids by the file name themselves in
+    the AST.
+    The "id to file" map is thus only used in the deserialization process.
+  *)
+let id_to_file_of_json (js : json) : (id_to_file_map, string) result =
+  combine_error_msgs js __FUNCTION__
+    ((* The map is stored as a list of pairs (key, value): we deserialize
+      * this list then convert it to a map *)
+     let* key_values =
+       list_of_json (pair_of_json file_id_of_json file_name_of_json) js
+     in
+     Ok (IdToFile.of_list key_values))
+
+let loc_of_json (js : json) : (loc, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("line", line); ("col", col) ] ->
+        let* line = int_of_json line in
+        let* col = int_of_json col in
+        Ok { line; col }
+    | _ -> Error "")
+
+let span_of_json (id_to_file : id_to_file_map) (js : json) :
+    (span, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("file_id", file_id); ("beg", beg_loc); ("end", end_loc) ] ->
+        let* file_id = file_id_of_json file_id in
+        let file = IdToFile.find file_id id_to_file in
+        let* beg_loc = loc_of_json beg_loc in
+        let* end_loc = loc_of_json end_loc in
+        Ok { file; beg_loc; end_loc }
+    | _ -> Error "")
+
+let meta_of_json (id_to_file : id_to_file_map) (js : json) :
+    (meta, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("span", span); ("generated_from_span", generated_from_span) ] ->
+        let* span = span_of_json id_to_file span in
+        let* generated_from_span =
+          option_of_json (span_of_json id_to_file) generated_from_span
+        in
+        Ok { span; generated_from_span }
+    | _ -> Error "")
+
 let path_elem_of_json (js : json) : (path_elem, string) result =
-  combine_error_msgs js "path_elem_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("Ident", name) ] ->
         let* name = string_of_json name in
@@ -34,13 +132,13 @@ let path_elem_of_json (js : json) : (path_elem, string) result =
     | _ -> Error "")
 
 let name_of_json (js : json) : (name, string) result =
-  combine_error_msgs js "name_of_json" (list_of_json path_elem_of_json js)
+  combine_error_msgs js __FUNCTION__ (list_of_json path_elem_of_json js)
 
 let fun_name_of_json (js : json) : (fun_name, string) result =
-  combine_error_msgs js "fun_name_of_json" (name_of_json js)
+  combine_error_msgs js __FUNCTION__ (name_of_json js)
 
 let type_var_of_json (js : json) : (T.type_var, string) result =
-  combine_error_msgs js "type_var_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("index", index); ("name", name) ] ->
         let* index = T.TypeVarId.id_of_json index in
@@ -49,7 +147,7 @@ let type_var_of_json (js : json) : (T.type_var, string) result =
     | _ -> Error "")
 
 let region_var_of_json (js : json) : (T.region_var, string) result =
-  combine_error_msgs js "region_var_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("index", index); ("name", name) ] ->
         let* index = T.RegionVarId.id_of_json index in
@@ -58,7 +156,7 @@ let region_var_of_json (js : json) : (T.region_var, string) result =
     | _ -> Error "")
 
 let region_of_json (js : json) : (T.RegionVarId.id T.region, string) result =
-  combine_error_msgs js "region_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `String "Static" -> Ok T.Static
     | `Assoc [ ("Var", rid) ] ->
@@ -67,7 +165,7 @@ let region_of_json (js : json) : (T.RegionVarId.id T.region, string) result =
     | _ -> Error "")
 
 let erased_region_of_json (js : json) : (T.erased_region, string) result =
-  combine_error_msgs js "erased_region_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with `String "Erased" -> Ok T.Erased | _ -> Error "")
 
 let integer_type_of_json (js : json) : (T.integer_type, string) result =
@@ -93,7 +191,7 @@ let ref_kind_of_json (js : json) : (T.ref_kind, string) result =
   | _ -> Error ("ref_kind_of_json failed on: " ^ show js)
 
 let assumed_ty_of_json (js : json) : (T.assumed_ty, string) result =
-  combine_error_msgs js "assumed_ty_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `String "Box" -> Ok T.Box
     | `String "Vec" -> Ok T.Vec
@@ -101,7 +199,7 @@ let assumed_ty_of_json (js : json) : (T.assumed_ty, string) result =
     | _ -> Error "")
 
 let type_id_of_json (js : json) : (T.type_id, string) result =
-  combine_error_msgs js "type_id_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("Adt", id) ] ->
         let* id = T.TypeDeclId.id_of_json id in
@@ -114,7 +212,7 @@ let type_id_of_json (js : json) : (T.type_id, string) result =
 
 let rec ty_of_json (r_of_json : json -> ('r, string) result) (js : json) :
     ('r T.ty, string) result =
-  combine_error_msgs js "ty_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("Adt", `List [ id; regions; types ]) ] ->
         let* id = type_id_of_json id in
@@ -147,43 +245,48 @@ let rec ty_of_json (r_of_json : json -> ('r, string) result) (js : json) :
     | _ -> Error "")
 
 let sty_of_json (js : json) : (T.sty, string) result =
-  combine_error_msgs js "sty_of_json" (ty_of_json region_of_json js)
+  combine_error_msgs js __FUNCTION__ (ty_of_json region_of_json js)
 
 let ety_of_json (js : json) : (T.ety, string) result =
-  combine_error_msgs js "ety_of_json" (ty_of_json erased_region_of_json js)
+  combine_error_msgs js __FUNCTION__ (ty_of_json erased_region_of_json js)
 
-let field_of_json (js : json) : (T.field, string) result =
-  combine_error_msgs js "field_of_json"
+let field_of_json (id_to_file : id_to_file_map) (js : json) :
+    (T.field, string) result =
+  combine_error_msgs js __FUNCTION__
     (match js with
-    | `Assoc [ ("name", name); ("ty", ty) ] ->
+    | `Assoc [ ("meta", meta); ("name", name); ("ty", ty) ] ->
+        let* meta = meta_of_json id_to_file meta in
         let* name = option_of_json string_of_json name in
         let* ty = sty_of_json ty in
-        Ok { T.field_name = name; field_ty = ty }
+        Ok { T.meta; field_name = name; field_ty = ty }
     | _ -> Error "")
 
-let variant_of_json (js : json) : (T.variant, string) result =
-  combine_error_msgs js "variant_of_json"
+let variant_of_json (id_to_file : id_to_file_map) (js : json) :
+    (T.variant, string) result =
+  combine_error_msgs js __FUNCTION__
     (match js with
-    | `Assoc [ ("name", name); ("fields", fields) ] ->
+    | `Assoc [ ("meta", meta); ("name", name); ("fields", fields) ] ->
+        let* meta = meta_of_json id_to_file meta in
         let* name = string_of_json name in
-        let* fields = list_of_json field_of_json fields in
-        Ok { T.variant_name = name; fields }
+        let* fields = list_of_json (field_of_json id_to_file) fields in
+        Ok { T.meta; variant_name = name; fields }
     | _ -> Error "")
 
-let type_decl_kind_of_json (js : json) : (T.type_decl_kind, string) result =
-  combine_error_msgs js "type_decl_kind_of_json"
+let type_decl_kind_of_json (id_to_file : id_to_file_map) (js : json) :
+    (T.type_decl_kind, string) result =
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("Struct", fields) ] ->
-        let* fields = list_of_json field_of_json fields in
+        let* fields = list_of_json (field_of_json id_to_file) fields in
         Ok (T.Struct fields)
     | `Assoc [ ("Enum", variants) ] ->
-        let* variants = list_of_json variant_of_json variants in
+        let* variants = list_of_json (variant_of_json id_to_file) variants in
         Ok (T.Enum variants)
     | `String "Opaque" -> Ok T.Opaque
     | _ -> Error "")
 
 let region_var_group_of_json (js : json) : (T.region_var_group, string) result =
-  combine_error_msgs js "region_var_group_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("id", id); ("regions", regions); ("parents", parents) ] ->
         let* id = T.RegionGroupId.id_of_json id in
@@ -194,15 +297,16 @@ let region_var_group_of_json (js : json) : (T.region_var_group, string) result =
 
 let region_var_groups_of_json (js : json) : (T.region_var_groups, string) result
     =
-  combine_error_msgs js "region_var_group_of_json"
-    (list_of_json region_var_group_of_json js)
+  combine_error_msgs js __FUNCTION__ (list_of_json region_var_group_of_json js)
 
-let type_decl_of_json (js : json) : (T.type_decl, string) result =
-  combine_error_msgs js "type_decl_of_json"
+let type_decl_of_json (id_to_file : id_to_file_map) (js : json) :
+    (T.type_decl, string) result =
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc
         [
           ("def_id", def_id);
+          ("meta", meta);
           ("name", name);
           ("region_params", region_params);
           ("type_params", type_params);
@@ -210,14 +314,16 @@ let type_decl_of_json (js : json) : (T.type_decl, string) result =
           ("kind", kind);
         ] ->
         let* def_id = T.TypeDeclId.id_of_json def_id in
+        let* meta = meta_of_json id_to_file meta in
         let* name = name_of_json name in
         let* region_params = list_of_json region_var_of_json region_params in
         let* type_params = list_of_json type_var_of_json type_params in
-        let* kind = type_decl_kind_of_json kind in
+        let* kind = type_decl_kind_of_json id_to_file kind in
         let* regions_hierarchy = region_var_groups_of_json regions_hierarchy in
         Ok
           {
             T.def_id;
+            meta;
             name;
             region_params;
             type_params;
@@ -227,7 +333,7 @@ let type_decl_of_json (js : json) : (T.type_decl, string) result =
     | _ -> Error "")
 
 let var_of_json (js : json) : (A.var, string) result =
-  combine_error_msgs js "var_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("index", index); ("name", name); ("ty", ty) ] ->
         let* index = V.VarId.id_of_json index in
@@ -237,7 +343,7 @@ let var_of_json (js : json) : (A.var, string) result =
     | _ -> Error "")
 
 let big_int_of_json (js : json) : (V.big_int, string) result =
-  combine_error_msgs js "big_int_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Int i -> Ok (Z.of_int i)
     | `String is -> Ok (Z.of_string is)
@@ -251,7 +357,7 @@ let big_int_of_json (js : json) : (V.big_int, string) result =
  *)
 let scalar_value_of_json (js : json) : (V.scalar_value, string) result =
   let res =
-    combine_error_msgs js "scalar_value_of_json"
+    combine_error_msgs js __FUNCTION__
       (match js with
       | `Assoc [ ("Isize", `List [ bi ]) ] ->
           let* bi = big_int_of_json bi in
@@ -300,7 +406,7 @@ let scalar_value_of_json (js : json) : (V.scalar_value, string) result =
       res
 
 let field_proj_kind_of_json (js : json) : (E.field_proj_kind, string) result =
-  combine_error_msgs js "field_proj_kind_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("ProjAdt", `List [ def_id; opt_variant_id ]) ] ->
         let* def_id = T.TypeDeclId.id_of_json def_id in
@@ -317,7 +423,7 @@ let field_proj_kind_of_json (js : json) : (E.field_proj_kind, string) result =
     | _ -> Error "")
 
 let projection_elem_of_json (js : json) : (E.projection_elem, string) result =
-  combine_error_msgs js "projection_elem_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `String "Deref" -> Ok E.Deref
     | `String "DerefBox" -> Ok E.DerefBox
@@ -328,11 +434,10 @@ let projection_elem_of_json (js : json) : (E.projection_elem, string) result =
     | _ -> Error ("projection_elem_of_json failed on:" ^ show js))
 
 let projection_of_json (js : json) : (E.projection, string) result =
-  combine_error_msgs js "projection_of_json"
-    (list_of_json projection_elem_of_json js)
+  combine_error_msgs js __FUNCTION__ (list_of_json projection_elem_of_json js)
 
 let place_of_json (js : json) : (E.place, string) result =
-  combine_error_msgs js "place_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("var_id", var_id); ("projection", projection) ] ->
         let* var_id = V.VarId.id_of_json var_id in
@@ -378,7 +483,7 @@ let binop_of_json (js : json) : (E.binop, string) result =
   | _ -> Error ("binop_of_json failed on:" ^ show js)
 
 let constant_value_of_json (js : json) : (V.constant_value, string) result =
-  combine_error_msgs js "constant_value_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("Scalar", scalar_value) ] ->
         let* scalar_value = scalar_value_of_json scalar_value in
@@ -395,7 +500,7 @@ let constant_value_of_json (js : json) : (V.constant_value, string) result =
     | _ -> Error "")
 
 let operand_of_json (js : json) : (E.operand, string) result =
-  combine_error_msgs js "operand_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("Copy", place) ] ->
         let* place = place_of_json place in
@@ -410,7 +515,7 @@ let operand_of_json (js : json) : (E.operand, string) result =
     | _ -> Error "")
 
 let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result =
-  combine_error_msgs js "operand_kind_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `String "AggregatedTuple" -> Ok E.AggregatedTuple
     | `Assoc [ ("AggregatedOption", `List [ variant_id; ty ]) ] ->
@@ -429,7 +534,7 @@ let aggregate_kind_of_json (js : json) : (E.aggregate_kind, string) result =
     | _ -> Error "")
 
 let rvalue_of_json (js : json) : (E.rvalue, string) result =
-  combine_error_msgs js "rvalue_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("Use", op) ] ->
         let* op = operand_of_json op in
@@ -472,7 +577,7 @@ let assumed_fun_id_of_json (js : json) : (A.assumed_fun_id, string) result =
   | _ -> Error ("assumed_fun_id_of_json failed on:" ^ show js)
 
 let fun_id_of_json (js : json) : (A.fun_id, string) result =
-  combine_error_msgs js "fun_id_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("Regular", id) ] ->
         let* id = A.FunDeclId.id_of_json id in
@@ -483,7 +588,7 @@ let fun_id_of_json (js : json) : (A.fun_id, string) result =
     | _ -> Error "")
 
 let assertion_of_json (js : json) : (A.assertion, string) result =
-  combine_error_msgs js "assertion_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("cond", cond); ("expected", expected) ] ->
         let* cond = operand_of_json cond in
@@ -492,7 +597,7 @@ let assertion_of_json (js : json) : (A.assertion, string) result =
     | _ -> Error "")
 
 let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
-  combine_error_msgs js "fun_sig_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc
         [
@@ -521,7 +626,7 @@ let fun_sig_of_json (js : json) : (A.fun_sig, string) result =
     | _ -> Error "")
 
 let call_of_json (js : json) : (A.call, string) result =
-  combine_error_msgs js "call_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc
         [
@@ -539,8 +644,19 @@ let call_of_json (js : json) : (A.call, string) result =
         Ok { A.func; region_args; type_args; args; dest }
     | _ -> Error "")
 
-let rec statement_of_json (js : json) : (A.statement, string) result =
-  combine_error_msgs js "statement_of_json"
+let rec statement_of_json (id_to_file : id_to_file_map) (js : json) :
+    (A.statement, string) result =
+  combine_error_msgs js __FUNCTION__
+    (match js with
+    | `Assoc [ ("meta", meta); ("content", content) ] ->
+        let* meta = meta_of_json id_to_file meta in
+        let* content = raw_statement_of_json id_to_file content in
+        Ok { A.meta; content }
+    | _ -> Error "")
+
+and raw_statement_of_json (id_to_file : id_to_file_map) (js : json) :
+    (A.raw_statement, string) result =
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("Assign", `List [ place; rvalue ]) ] ->
         let* place = place_of_json place in
@@ -576,61 +692,76 @@ let rec statement_of_json (js : json) : (A.statement, string) result =
         Ok (A.Continue i)
     | `String "Nop" -> Ok A.Nop
     | `Assoc [ ("Sequence", `List [ st1; st2 ]) ] ->
-        let* st1 = statement_of_json st1 in
-        let* st2 = statement_of_json st2 in
+        let* st1 = statement_of_json id_to_file st1 in
+        let* st2 = statement_of_json id_to_file st2 in
         Ok (A.Sequence (st1, st2))
     | `Assoc [ ("Switch", `List [ op; tgt ]) ] ->
         let* op = operand_of_json op in
-        let* tgt = switch_targets_of_json tgt in
+        let* tgt = switch_targets_of_json id_to_file tgt in
         Ok (A.Switch (op, tgt))
     | `Assoc [ ("Loop", st) ] ->
-        let* st = statement_of_json st in
+        let* st = statement_of_json id_to_file st in
         Ok (A.Loop st)
     | _ -> Error "")
 
-and switch_targets_of_json (js : json) : (A.switch_targets, string) result =
-  combine_error_msgs js "switch_targets_of_json"
+and switch_targets_of_json (id_to_file : id_to_file_map) (js : json) :
+    (A.switch_targets, string) result =
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("If", `List [ st1; st2 ]) ] ->
-        let* st1 = statement_of_json st1 in
-        let* st2 = statement_of_json st2 in
+        let* st1 = statement_of_json id_to_file st1 in
+        let* st2 = statement_of_json id_to_file st2 in
         Ok (A.If (st1, st2))
     | `Assoc [ ("SwitchInt", `List [ int_ty; tgts; otherwise ]) ] ->
         let* int_ty = integer_type_of_json int_ty in
         let* tgts =
           list_of_json
-            (pair_of_json (list_of_json scalar_value_of_json) statement_of_json)
+            (pair_of_json
+               (list_of_json scalar_value_of_json)
+               (statement_of_json id_to_file))
             tgts
         in
-        let* otherwise = statement_of_json otherwise in
+        let* otherwise = statement_of_json id_to_file otherwise in
         Ok (A.SwitchInt (int_ty, tgts, otherwise))
     | _ -> Error "")
 
-let fun_body_of_json (js : json) : (A.fun_body, string) result =
-  combine_error_msgs js "fun_body_of_json"
+let fun_body_of_json (id_to_file : id_to_file_map) (js : json) :
+    (A.fun_body, string) result =
+  combine_error_msgs js __FUNCTION__
     (match js with
-    | `Assoc [ ("arg_count", arg_count); ("locals", locals); ("body", body) ] ->
+    | `Assoc
+        [
+          ("meta", meta);
+          ("arg_count", arg_count);
+          ("locals", locals);
+          ("body", body);
+        ] ->
+        let* meta = meta_of_json id_to_file meta in
         let* arg_count = int_of_json arg_count in
         let* locals = list_of_json var_of_json locals in
-        let* body = statement_of_json body in
-        Ok { A.arg_count; locals; body }
+        let* body = statement_of_json id_to_file body in
+        Ok { A.meta; arg_count; locals; body }
     | _ -> Error "")
 
-let fun_decl_of_json (js : json) : (A.fun_decl, string) result =
-  combine_error_msgs js "fun_decl_of_json"
+let fun_decl_of_json (id_to_file : id_to_file_map) (js : json) :
+    (A.fun_decl, string) result =
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc
         [
           ("def_id", def_id);
+          ("meta", meta);
           ("name", name);
           ("signature", signature);
           ("body", body);
         ] ->
         let* def_id = A.FunDeclId.id_of_json def_id in
+        let* meta = meta_of_json id_to_file meta in
         let* name = fun_name_of_json name in
         let* signature = fun_sig_of_json signature in
-        let* body = option_of_json fun_body_of_json body in
-        Ok { A.def_id; name; signature; body; is_global_decl_body = false }
+        let* body = option_of_json (fun_body_of_json id_to_file) body in
+        Ok
+          { A.def_id; meta; name; signature; body; is_global_decl_body = false }
     | _ -> Error "")
 
 (* Strict type for the number of function declarations (see [global_to_fun_id] below) *)
@@ -646,17 +777,25 @@ let global_to_fun_id (conv : global_id_converter) (gid : A.GlobalDeclId.id) :
 
 (* Converts a global declaration to a function declaration.
  *)
-let global_decl_of_json (js : json) (gid_conv : global_id_converter) :
+let global_decl_of_json (id_to_file : id_to_file_map) (js : json)
+    (gid_conv : global_id_converter) :
     (A.global_decl * A.fun_decl, string) result =
-  combine_error_msgs js "global_decl_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
-    | `Assoc [ ("def_id", def_id); ("name", name); ("ty", ty); ("body", body) ]
-      ->
+    | `Assoc
+        [
+          ("def_id", def_id);
+          ("meta", meta);
+          ("name", name);
+          ("ty", ty);
+          ("body", body);
+        ] ->
         let* global_id = A.GlobalDeclId.id_of_json def_id in
         let fun_id = global_to_fun_id gid_conv global_id in
+        let* meta = meta_of_json id_to_file meta in
         let* name = fun_name_of_json name in
         let* ty = ety_of_json ty in
-        let* body = option_of_json fun_body_of_json body in
+        let* body = option_of_json (fun_body_of_json id_to_file) body in
         let signature : A.fun_sig =
           {
             region_params = [];
@@ -668,9 +807,10 @@ let global_decl_of_json (js : json) (gid_conv : global_id_converter) :
           }
         in
         Ok
-          ( { A.def_id = global_id; body_id = fun_id; name; ty },
+          ( { A.def_id = global_id; meta; body_id = fun_id; name; ty },
             {
               A.def_id = fun_id;
+              meta;
               name;
               signature;
               body;
@@ -680,7 +820,7 @@ let global_decl_of_json (js : json) (gid_conv : global_id_converter) :
 
 let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
     (js : json) : ('id Crates.g_declaration_group, string) result =
-  combine_error_msgs js "g_declaration_group_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("NonRec", `List [ id ]) ] ->
         let* id = id_of_json id in
@@ -692,17 +832,17 @@ let g_declaration_group_of_json (id_of_json : json -> ('id, string) result)
 
 let type_declaration_group_of_json (js : json) :
     (Crates.type_declaration_group, string) result =
-  combine_error_msgs js "type_declaration_group_of_json"
+  combine_error_msgs js __FUNCTION__
     (g_declaration_group_of_json T.TypeDeclId.id_of_json js)
 
 let fun_declaration_group_of_json (js : json) :
     (Crates.fun_declaration_group, string) result =
-  combine_error_msgs js "fun_declaration_group_of_json"
+  combine_error_msgs js __FUNCTION__
     (g_declaration_group_of_json A.FunDeclId.id_of_json js)
 
 let global_declaration_group_of_json (js : json) :
     (A.GlobalDeclId.id, string) result =
-  combine_error_msgs js "global_declaration_group_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("NonRec", `List [ id ]) ] ->
         let* id = A.GlobalDeclId.id_of_json id in
@@ -712,7 +852,7 @@ let global_declaration_group_of_json (js : json) :
 
 let declaration_group_of_json (js : json) :
     (Crates.declaration_group, string) result =
-  combine_error_msgs js "declaration_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc [ ("Type", `List [ decl ]) ] ->
         let* decl = type_declaration_group_of_json decl in
@@ -726,17 +866,18 @@ let declaration_group_of_json (js : json) :
     | _ -> Error "")
 
 let length_of_json_list (js : json) : (int, string) result =
-  combine_error_msgs js "get_json_list_len"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `List jsl -> Ok (List.length jsl)
     | _ -> Error ("not a list: " ^ show js))
 
 let llbc_crate_of_json (js : json) : (Crates.llbc_crate, string) result =
-  combine_error_msgs js "llbc_crate_of_json"
+  combine_error_msgs js __FUNCTION__
     (match js with
     | `Assoc
         [
           ("name", name);
+          ("id_to_file", id_to_file);
           ("declarations", declarations);
           ("types", types);
           ("functions", functions);
@@ -745,11 +886,12 @@ let llbc_crate_of_json (js : json) : (Crates.llbc_crate, string) result =
         (* We first deserialize the declaration groups (which simply contain ids)
          * and all the declarations *butù* the globals *)
         let* name = string_of_json name in
+        let* id_to_file = id_to_file_of_json id_to_file in
         let* declarations =
           list_of_json declaration_group_of_json declarations
         in
-        let* types = list_of_json type_decl_of_json types in
-        let* functions = list_of_json fun_decl_of_json functions in
+        let* types = list_of_json (type_decl_of_json id_to_file) types in
+        let* functions = list_of_json (fun_decl_of_json id_to_file) functions in
         (* When deserializing the globals, we split the global declarations
          * between the globals themselves and their bodies, which are simply
          * functions with no arguments. We add the global bodies to the list
@@ -757,7 +899,9 @@ let llbc_crate_of_json (js : json) : (Crates.llbc_crate, string) result =
          * are simply given by: `num_functions + global_id` *)
         let gid_conv = { fun_count = List.length functions } in
         let* globals =
-          list_of_json (fun js -> global_decl_of_json js gid_conv) globals
+          list_of_json
+            (fun js -> global_decl_of_json id_to_file js gid_conv)
+            globals
         in
         let globals, global_bodies = List.split globals in
         Ok
diff --git a/src/Meta.ml b/src/Meta.ml
new file mode 100644
index 00000000..cca6f047
--- /dev/null
+++ b/src/Meta.ml
@@ -0,0 +1,44 @@
+(** Meta data like code spans *)
+
+(** A line location *)
+type loc = {
+  line : int;  (** The (1-based) line number. *)
+  col : int;  (** The (0-based) column offset. *)
+}
+[@@deriving show]
+
+type file_name =
+  | Virtual of string  (** A remapped path (namely paths into stdlib) *)
+  | Local of string
+      (** A local path (a file coming from the current crate for instance) *)
+[@@deriving show]
+
+(** Span data *)
+type span = { file : file_name; beg_loc : loc; end_loc : loc } [@@deriving show]
+
+type meta = {
+  span : span;
+      (** The source code span.
+
+          If this meta information is for a statement/terminator coming from a macro
+          expansion/inlining/etc., this span is (in case of macros) for the macro
+          before expansion (i.e., the location the code where the user wrote the call
+          to the macro).
+
+          Ex:
+          ```text
+          // Below, we consider the spans for the statements inside `test`
+
+          //   the statement we consider, which gets inlined in `test`
+                                   VV
+          macro_rules! macro { ... st ... } // `generated_from_span` refers to this location
+
+          fn test() {
+              macro!(); // <-- `span` refers to this location
+          }
+          ```
+       *)
+  generated_from_span : span option;
+      (** Where the code actually comes from, in case of macro expansion/inlining/etc. *)
+}
+[@@deriving show]
diff --git a/src/PrePasses.ml b/src/PrePasses.ml
index 3159907e..cd14c398 100644
--- a/src/PrePasses.ml
+++ b/src/PrePasses.ml
@@ -31,12 +31,12 @@ let filter_drop_assigns (f : A.fun_decl) : A.fun_decl =
       inherit [_] A.map_statement as super
 
       method! visit_Sequence env st1 st2 =
-        match (st1, st2) with
+        match (st1.content, st2.content) with
         | Drop p1, Assign (p2, _) ->
-            if p1 = p2 then self#visit_statement env st2
+            if p1 = p2 then (self#visit_statement env st2).content
             else super#visit_Sequence env st1 st2
-        | Drop p1, Sequence (Assign (p2, _), _) ->
-            if p1 = p2 then self#visit_statement env st2
+        | Drop p1, Sequence ({ content = Assign (p2, _); meta = _ }, _) ->
+            if p1 = p2 then (self#visit_statement env st2).content
             else super#visit_Sequence env st1 st2
         | _ -> super#visit_Sequence env st1 st2
     end
diff --git a/src/Print.ml b/src/Print.ml
index 1439a74d..03cab6ee 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -935,6 +935,10 @@ module LlbcAst = struct
 
   let rec statement_to_string (fmt : ast_formatter) (indent : string)
       (indent_incr : string) (st : A.statement) : string =
+    raw_statement_to_string fmt indent indent_incr st.content
+
+  and raw_statement_to_string (fmt : ast_formatter) (indent : string)
+      (indent_incr : string) (st : A.raw_statement) : string =
     match st with
     | A.Assign (p, rv) ->
         indent ^ place_to_string fmt p ^ " := " ^ rvalue_to_string fmt rv
diff --git a/src/Substitute.ml b/src/Substitute.ml
index 5a21e637..b99baafa 100644
--- a/src/Substitute.ml
+++ b/src/Substitute.ml
@@ -276,6 +276,10 @@ let call_substitute (tsubst : T.TypeVarId.id -> T.ety) (call : A.call) : A.call
 (** Apply a type substitution to a statement *)
 let rec statement_substitute (tsubst : T.TypeVarId.id -> T.ety)
     (st : A.statement) : A.statement =
+  { st with A.content = raw_statement_substitute tsubst st.content }
+
+and raw_statement_substitute (tsubst : T.TypeVarId.id -> T.ety)
+    (st : A.raw_statement) : A.raw_statement =
   match st with
   | A.Assign (p, rvalue) ->
       let p = place_substitute tsubst p in
diff --git a/src/Types.ml b/src/Types.ml
index 5bd172cb..48dd9ab0 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -1,15 +1,16 @@
 open Identifiers
 open Names
+open Meta
 module TypeVarId = IdGen ()
 module TypeDeclId = IdGen ()
 module VariantId = IdGen ()
 module FieldId = IdGen ()
 
-module RegionVarId = IdGen ()
 (** Region variable ids. Used in function signatures. *)
+module RegionVarId = IdGen ()
 
-module RegionId = IdGen ()
 (** Region ids. Used for symbolic executions. *)
+module RegionId = IdGen ()
 
 module RegionGroupId = IdGen ()
 
@@ -39,12 +40,6 @@ type 'rid region =
  *)
 type erased_region = Erased [@@deriving show, ord]
 
-type ('id, 'r) g_region_group = {
-  id : 'id;
-  regions : 'r list;
-  parents : 'id list;
-}
-[@@deriving show]
 (** A group of regions.
 
     Results from a lifetime analysis: we group the regions with the same
@@ -52,6 +47,12 @@ type ('id, 'r) g_region_group = {
     This is necessary to introduce the proper abstraction with the
     proper constraints, when evaluating a function call in symbolic mode.
 *)
+type ('id, 'r) g_region_group = {
+  id : 'id;
+  regions : 'r list;
+  parents : 'id list;
+}
+[@@deriving show]
 
 type ('r, 'id) g_region_groups = ('r, 'id) g_region_group list [@@deriving show]
 
@@ -157,30 +158,33 @@ type 'r ty =
       }]
 (* TODO: group Bool, Char, etc. in Constant *)
 
-type 'r gr_ty = 'r region ty [@@deriving show, ord]
 (** Generic type with regions *)
+type 'r gr_ty = 'r region ty [@@deriving show, ord]
 
-type sty = RegionVarId.id gr_ty [@@deriving show, ord]
 (** *S*ignature types.
 
     Used in function signatures and type definitions.
  *)
+type sty = RegionVarId.id gr_ty [@@deriving show, ord]
 
-type rty = RegionId.id gr_ty [@@deriving show, ord]
 (** Type with *R*egions.
 
     Used to project borrows/loans inside of abstractions, during symbolic
     execution.
  *)
+type rty = RegionId.id gr_ty [@@deriving show, ord]
 
-type ety = erased_region ty [@@deriving show, ord]
 (** Type with *E*rased regions.
     
     Used in function bodies, "regular" value types, etc.
  *)
+type ety = erased_region ty [@@deriving show, ord]
 
-type field = { field_name : string option; field_ty : sty } [@@deriving show]
-type variant = { variant_name : string; fields : field list } [@@deriving show]
+type field = { meta : meta; field_name : string option; field_ty : sty }
+[@@deriving show]
+
+type variant = { meta : meta; variant_name : string; fields : field list }
+[@@deriving show]
 
 type type_decl_kind =
   | Struct of field list
@@ -191,6 +195,7 @@ type type_decl_kind =
 
 type type_decl = {
   def_id : TypeDeclId.id;
+  meta : meta;
   name : type_name;
   region_params : region_var list;
   type_params : type_var list;