Add more location information to IR

8 files changed, 96 insertions, 69 deletions

diff --git a/src/jib/c_backend.ml b/src/jib/c_backend.ml
index a875405d..25331034 100644
--- a/src/jib/c_backend.ml
+++ b/src/jib/c_backend.ml
@@ -662,7 +662,7 @@ let rec insert_heap_returns ret_ctyps = function
         CDEF_fundef (id, Some gs, args, fix_early_heap_return (name gs) ret_ctyp body)
         :: insert_heap_returns ret_ctyps cdefs
      | Some ret_ctyp ->
-        CDEF_fundef (id, None, args, fix_early_stack_return (name gs) ret_ctyp (idecl ret_ctyp (name gs) :: body))
+        CDEF_fundef (id, None, args, fix_early_stack_return (name gs) ret_ctyp (idecl (id_loc id) ret_ctyp (name gs) :: body))
         :: insert_heap_returns ret_ctyps cdefs
      end
 
@@ -723,14 +723,14 @@ let hoist_allocations recursive_functions = function
      let rec hoist = function
        | I_aux (I_decl (ctyp, decl_id), annot) :: instrs when hoist_ctyp ctyp ->
           let hid = hoist_id () in
-          decls := idecl ctyp hid :: !decls;
+          decls := idecl (snd annot) ctyp hid :: !decls;
           cleanups := iclear ctyp hid :: !cleanups;
           let instrs = instrs_rename decl_id hid instrs in
           I_aux (I_reset (ctyp, hid), annot) :: hoist instrs
 
        | I_aux (I_init (ctyp, decl_id, cval), annot) :: instrs when hoist_ctyp ctyp ->
           let hid = hoist_id () in
-          decls := idecl ctyp hid :: !decls;
+          decls := idecl (snd annot) ctyp hid :: !decls;
           cleanups := iclear ctyp hid :: !cleanups;
           let instrs = instrs_rename decl_id hid instrs in
           I_aux (I_reinit (ctyp, hid, cval), annot) :: hoist instrs
@@ -1547,7 +1547,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
      string (Printf.sprintf "  KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name id))
 
   | I_init (ctyp, id, cval) ->
-     codegen_instr fid ctx (idecl ctyp id) ^^ hardline
+     codegen_instr fid ctx (idecl l ctyp id) ^^ hardline
      ^^ codegen_conversion Parse_ast.Unknown (CL_id (id, ctyp)) cval
 
   | I_reinit (ctyp, id, cval) ->
@@ -2169,10 +2169,10 @@ let codegen_def' ctx = function
   | CDEF_let (number, bindings, instrs) ->
      let instrs = add_local_labels instrs in
      let setup =
-       List.concat (List.map (fun (id, ctyp) -> [idecl ctyp (name id)]) bindings)
+       List.concat (List.map (fun (id, ctyp) -> [idecl (id_loc id) ctyp (name id)]) bindings)
      in
      let cleanup =
-       List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (name id)]) bindings)
+       List.concat (List.map (fun (id, ctyp) -> [iclear ~loc:(id_loc id) ctyp (name id)]) bindings)
      in
      separate_map hardline (fun (id, ctyp) -> string (Printf.sprintf "%s%s %s;" (static ()) (sgen_ctyp ctyp) (sgen_id id))) bindings
      ^^ hardline ^^ string (Printf.sprintf "static void create_letbind_%d(void) " number)
diff --git a/src/jib/c_codegen.ml b/src/jib/c_codegen.ml
index b92713ff..59229126 100644
--- a/src/jib/c_codegen.ml
+++ b/src/jib/c_codegen.ml
@@ -826,7 +826,7 @@ let rec codegen_instr fid ctx (I_aux (instr, (_, l))) =
      ksprintf string "  KILL(%s)(&%s);" (sgen_ctyp_name ctyp) (sgen_name ctyp id)
 
   | I_init (ctyp, id, cval) ->
-     codegen_instr fid ctx (idecl ctyp id) ^^ hardline
+     codegen_instr fid ctx (idecl l ctyp id) ^^ hardline
      ^^ codegen_conversion Parse_ast.Unknown ctx (CL_id (id, ctyp)) cval
 
   | I_reinit (ctyp, id, cval) ->
@@ -1496,10 +1496,10 @@ let codegen_def_body ctx = function
   | CDEF_let (number, bindings, instrs) ->
      let instrs = add_local_labels instrs in
      let setup =
-       List.concat (List.map (fun (id, ctyp) -> [idecl ctyp (global id)]) bindings)
+       List.concat (List.map (fun (id, ctyp) -> [idecl (id_loc id) ctyp (global id)]) bindings)
      in
      let cleanup =
-       List.concat (List.map (fun (id, ctyp) -> [iclear ctyp (global id)]) bindings)
+       List.concat (List.map (fun (id, ctyp) -> [iclear ~loc:(id_loc id) ctyp (global id)]) bindings)
      in
      hardline ^^ string (Printf.sprintf "void sail_create_letbind_%d(sail_state *state) " number)
      ^^ string "{"
diff --git a/src/jib/jib_compile.ml b/src/jib/jib_compile.ml
index 8b886d14..e4578a26 100644
--- a/src/jib/jib_compile.ml
+++ b/src/jib/jib_compile.ml
@@ -262,7 +262,7 @@ let rec compile_aval l ctx = function
      let ctyp' = ctyp_of_typ ctx typ in
      if not (ctyp_equal ctyp ctyp') then
        let gs = ngensym () in
-       [iinit ctyp' gs cval], V_id (gs, ctyp'), [iclear ctyp' gs]
+       [iinit l ctyp' gs cval], V_id (gs, ctyp'), [iclear ctyp' gs]
      else
        [], cval, []
 
@@ -285,13 +285,13 @@ let rec compile_aval l ctx = function
 
   | AV_lit (L_aux (L_num n, _), typ) when Big_int.less_equal (min_int 64) n && Big_int.less_equal n (max_int 64) ->
      let gs = ngensym () in
-     [iinit CT_lint gs (V_lit (VL_int n, CT_fint 64))],
+     [iinit l CT_lint gs (V_lit (VL_int n, CT_fint 64))],
      V_id (gs, CT_lint),
      [iclear CT_lint gs]
 
   | AV_lit (L_aux (L_num n, _), typ) ->
      let gs = ngensym () in
-     [iinit CT_lint gs (V_lit (VL_string (Big_int.to_string n), CT_string))],
+     [iinit l CT_lint gs (V_lit (VL_string (Big_int.to_string n), CT_string))],
      V_id (gs, CT_lint),
      [iclear CT_lint gs]
 
@@ -306,7 +306,7 @@ let rec compile_aval l ctx = function
        [], V_lit (VL_real str, CT_real), []
      else
        let gs = ngensym () in
-       [iinit CT_real gs (V_lit (VL_string str, CT_string))],
+       [iinit l CT_real gs (V_lit (VL_string str, CT_string))],
        V_id (gs, CT_real),
        [iclear CT_real gs]
 
@@ -327,7 +327,7 @@ let rec compile_aval l ctx = function
      let tup_ctyp = CT_tup (List.map cval_ctyp cvals) in
      let gs = ngensym () in
      setup
-     @ [idecl tup_ctyp gs]
+     @ [idecl l tup_ctyp gs]
      @ List.mapi (fun n cval -> icopy l (CL_tuple (CL_id (gs, tup_ctyp), n)) cval) cvals,
      V_id (gs, CT_tup (List.map cval_ctyp cvals)),
      [iclear tup_ctyp gs]
@@ -346,7 +346,7 @@ let rec compile_aval l ctx = function
      let setup = List.concat (List.map (fun (s, _, _) -> s) field_triples) in
      let fields = List.map (fun (_, f, _) -> f) field_triples in
      let cleanup = List.concat (List.map (fun (_, _, c) -> c) field_triples) in
-     [idecl ctyp gs],
+     [idecl l ctyp gs],
      V_struct (fields, ctyp),
      [iclear ctyp gs]
 
@@ -359,7 +359,7 @@ let rec compile_aval l ctx = function
        @ [icopy l (CL_field (CL_id (gs, ctyp), (id, []))) cval]
        @ field_cleanup
      in
-     [idecl ctyp gs]
+     [idecl l ctyp gs]
      @ List.concat (List.map compile_fields (Bindings.bindings fields)),
      V_id (gs, ctyp),
      [iclear ctyp gs]
@@ -371,7 +371,7 @@ let rec compile_aval l ctx = function
            [], V_lit (VL_bits ([], ord), vector_ctyp), []
         | _ ->
         let gs = ngensym () in
-        [idecl vector_ctyp gs;
+        [idecl l vector_ctyp gs;
          iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init", []) [V_lit (VL_int Big_int.zero, CT_fint 64)]],
         V_id (gs, vector_ctyp),
         [iclear vector_ctyp gs]
@@ -401,10 +401,10 @@ let rec compile_aval l ctx = function
      let first_chunk = bitstring (Util.take (len mod 64) avals) in
      let chunks = Util.drop (len mod 64) avals |> chunkify 64 |> List.map bitstring in
      let gs = ngensym () in
-     [iinit (CT_lbits true) gs (V_lit (first_chunk, CT_fbits (len mod 64, true)))]
-     @ List.map (fun chunk -> ifuncall (CL_id (gs, CT_lbits true))
-                                       (mk_id "append_64", [])
-                                       [V_id (gs, CT_lbits true); V_lit (chunk, CT_fbits (64, true))]) chunks,
+     [iinit l (CT_lbits true) gs (V_lit (first_chunk, CT_fbits (len mod 64, true)))]
+     @ List.map (fun chunk -> ifuncall l (CL_id (gs, CT_lbits true))
+                                (mk_id "append_64", [])
+                                [V_id (gs, CT_lbits true); V_lit (chunk, CT_fbits (64, true))]) chunks,
      V_id (gs, CT_lbits true),
      [iclear (CT_lbits true) gs]
 
@@ -433,7 +433,7 @@ let rec compile_aval l ctx = function
                      [V_id (gs, ctyp); V_lit (VL_int (Big_int.of_int i), CT_constant (Big_int.of_int i)); cval]]
           @ cleanup
      in
-     [idecl ctyp gs;
+     [idecl l ctyp gs;
       icopy l (CL_id (gs, ctyp)) (V_lit (VL_bits (Util.list_init len (fun _ -> Sail2_values.B0), direction), ctyp))]
      @ List.concat (List.mapi aval_mask (List.rev avals)),
      V_id (gs, ctyp),
@@ -458,7 +458,7 @@ let rec compile_aval l ctx = function
                   [V_id (gs, vector_ctyp); V_lit (VL_int (Big_int.of_int i), CT_fint 64); cval]]
        @ cleanup
      in
-     [idecl vector_ctyp gs;
+     [idecl l vector_ctyp gs;
       iextern (CL_id (gs, vector_ctyp)) (mk_id "internal_vector_init", []) [V_lit (VL_int (Big_int.of_int len), CT_fint 64)]]
      @ List.concat (List.mapi aval_set (if direction then List.rev avals else avals)),
      V_id (gs, vector_ctyp),
@@ -477,7 +477,7 @@ let rec compile_aval l ctx = function
        let setup, cval, cleanup = compile_aval l ctx aval in
        setup @ [iextern (CL_id (gs, CT_list ctyp)) (mk_id "cons", [ctyp]) [cval; V_id (gs, CT_list ctyp)]] @ cleanup
      in
-     [idecl (CT_list ctyp) gs]
+     [idecl l (CT_list ctyp) gs]
      @ List.concat (List.map mk_cons (List.rev avals)),
      V_id (gs, CT_list ctyp),
      [iclear (CT_list ctyp) gs]
@@ -496,18 +496,18 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp =
             cval
           else
             let gs = ngensym () in
-            setup := iinit ctyp gs cval :: !setup;
+            setup := iinit l ctyp gs cval :: !setup;
             cleanup := iclear ctyp gs :: !cleanup;
             V_id (gs, ctyp))
         arg_ctyps args
     in
     if C.specialize_calls || ctyp_equal (clexp_ctyp clexp) ret_ctyp then
-      !setup @ [ifuncall clexp id cast_args] @ !cleanup
+      !setup @ [ifuncall l clexp id cast_args] @ !cleanup
     else
       let gs = ngensym () in
       List.rev !setup
-      @ [idecl ret_ctyp gs;
-         ifuncall (CL_id (gs, ret_ctyp)) id cast_args;
+      @ [idecl l ret_ctyp gs;
+         ifuncall l (CL_id (gs, ret_ctyp)) id cast_args;
          icopy l clexp (V_id (gs, ret_ctyp));
          iclear ret_ctyp gs]
       @ !cleanup
@@ -517,7 +517,7 @@ let optimize_call l ctx clexp id args arg_ctyps ret_ctyp =
     begin match extern, List.map cval_ctyp args, clexp_ctyp clexp with
     | "slice", [CT_fbits _; CT_lint; _], CT_fbits (n, _) ->
        let start = ngensym () in
-       [iinit (CT_fint 64) start (List.nth args 1);
+       [iinit l (CT_fint 64) start (List.nth args 1);
         icopy l clexp (V_call (Slice n, [List.nth args 0; V_id (start, CT_fint 64)]))]
     | "sail_unsigned", [CT_fbits _], CT_fint 64 ->
        [icopy l clexp (V_call (Unsigned 64, [List.nth args 0]))]
@@ -588,20 +588,20 @@ let rec compile_match ctx (AP_aux (apat_aux, env, l)) cval case_label =
 
   | AP_id (pid, _) when is_ct_enum ctyp ->
      begin match Env.lookup_id pid ctx.tc_env with
-     | Unbound -> [idecl ctyp (name pid); icopy l (CL_id (name pid, ctyp)) cval], [], ctx
+     | Unbound -> [idecl l ctyp (name pid); icopy l (CL_id (name pid, ctyp)) cval], [], ctx
      | _ -> [ijump l (V_call (Neq, [V_id (name pid, ctyp); cval])) case_label], [], ctx
      end
 
   | AP_id (pid, typ) ->
      let id_ctyp = ctyp_of_typ ctx typ in
      let ctx = { ctx with locals = Bindings.add pid (Immutable, id_ctyp) ctx.locals } in
-     [idecl id_ctyp (name pid); icopy l (CL_id (name pid, id_ctyp)) cval], [iclear id_ctyp (name pid)], ctx
+     [idecl l id_ctyp (name pid); icopy l (CL_id (name pid, id_ctyp)) cval], [iclear id_ctyp (name pid)], ctx
 
   | AP_as (apat, id, typ) ->
      let id_ctyp = ctyp_of_typ ctx typ in
      let instrs, cleanup, ctx = compile_match ctx apat cval case_label in
      let ctx = { ctx with locals = Bindings.add id (Immutable, id_ctyp) ctx.locals } in
-     instrs @ [idecl id_ctyp (name id); icopy l (CL_id (name id, id_ctyp)) cval], iclear id_ctyp (name id) :: cleanup, ctx
+     instrs @ [idecl l id_ctyp (name id); icopy l (CL_id (name id, id_ctyp)) cval], iclear id_ctyp (name id) :: cleanup, ctx
 
   | AP_tup apats ->
      begin
@@ -686,7 +686,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let binding_ctyp = ctyp_of_typ { ctx with local_env = body_env } binding_typ in
      let setup, call, cleanup = compile_aexp ctx binding in
      let letb_setup, letb_cleanup =
-       [idecl binding_ctyp (name id);
+       [idecl l binding_ctyp (name id);
         iblock1 (setup @ [call (CL_id (name id, binding_ctyp))] @ cleanup)],
        [iclear binding_ctyp (name id)]
      in
@@ -725,7 +725,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        let case_instrs =
          destructure
          @ (if not trivial_guard then
-              guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup
+              guard_setup @ [idecl l CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup
               @ [iif l (V_call (Bnot, [V_id (gs, CT_bool)])) (destructure_cleanup @ [igoto case_label]) [] CT_unit]
             else [])
          @ (if num_cases > 1 then coverage_branch_taken branch_id body else [])
@@ -740,7 +740,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      in
      aval_setup
      @ (if num_cases > 1 then on_reached else [])
-     @ [idecl ctyp case_return_id]
+     @ [idecl l ctyp case_return_id]
      @ List.concat (List.map compile_case cases)
      @ [imatch_failure ()]
      @ [ilabel finish_match_label],
@@ -769,7 +769,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        let case_instrs =
          destructure @ [icomment "end destructuring"]
          @ (if not trivial_guard then
-              guard_setup @ [idecl CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup
+              guard_setup @ [idecl l CT_bool gs; guard_call (CL_id (gs, CT_bool))] @ guard_cleanup
               @ [ijump l (V_call (Bnot, [V_id (gs, CT_bool)])) try_label]
               @ [icomment "end guard"]
             else [])
@@ -779,7 +779,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        [iblock case_instrs; ilabel try_label]
      in
      assert (ctyp_equal ctyp (ctyp_of_typ ctx typ));
-     [idecl ctyp try_return_id;
+     [idecl l ctyp try_return_id;
       itry_block (aexp_setup @ [aexp_call (CL_id (try_return_id, ctyp))] @ aexp_cleanup);
       ijump l (V_call (Bnot, [V_id (have_exception, CT_bool)])) post_exception_handlers_label;
       icopy l (CL_id (have_exception, CT_bool)) (V_lit (VL_bool false, CT_bool))]
@@ -827,7 +827,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
        @ field_cleanup
      in
      let setup, cval, cleanup = compile_aval l ctx aval in
-     [idecl ctyp gs]
+     [idecl l ctyp gs]
      @ setup
      @ [icopy l (CL_id (gs, ctyp)) cval]
      @ cleanup
@@ -843,7 +843,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let gs = ngensym () in
      left_setup
      @ on_reached
-     @ [ idecl CT_bool gs;
+     @ [ idecl l CT_bool gs;
          iif l cval
              (right_coverage @ right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup)
              [icopy l (CL_id (gs, CT_bool)) (V_lit (VL_bool false, CT_bool))]
@@ -859,7 +859,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let gs = ngensym () in
      left_setup
      @ on_reached
-     @ [ idecl CT_bool gs;
+     @ [ idecl l CT_bool gs;
          iif l cval
              [icopy l (CL_id (gs, CT_bool)) (V_lit (VL_bool true, CT_bool))]
              (right_coverage @ right_setup @ [call (CL_id (gs, CT_bool))] @ right_cleanup)
@@ -899,7 +899,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let gs = ngensym () in
      let unit_gs = ngensym () in
      let loop_test = V_call (Bnot, [V_id (gs, CT_bool)]) in
-     [idecl CT_bool gs; idecl CT_unit unit_gs]
+     [idecl l CT_bool gs; idecl l CT_unit unit_gs]
      @ [ilabel loop_start_label]
      @ [iblock (cond_setup
                 @ [cond_call (CL_id (gs, CT_bool))]
@@ -921,7 +921,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let gs = ngensym () in
      let unit_gs = ngensym () in
      let loop_test = V_id (gs, CT_bool) in
-     [idecl CT_bool gs; idecl CT_unit unit_gs]
+     [idecl l CT_bool gs; idecl l CT_unit unit_gs]
      @ [ilabel loop_start_label]
      @ [iblock (body_setup
                 @ [body_call (CL_id (unit_gs, CT_unit))]
@@ -949,7 +949,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
          [ireturn cval]
        else
          let gs = ngensym () in
-         [idecl fn_return_ctyp gs;
+         [idecl l fn_return_ctyp gs;
           icopy l (CL_id (gs, fn_return_ctyp)) cval;
           ireturn (V_id (gs, fn_return_ctyp))]
      in
@@ -1007,7 +1007,7 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      let step_setup, step_call, step_cleanup = compile_aexp ctx loop_step in
      let step_gs = ngensym () in
      let variable_init gs setup call cleanup =
-       [idecl (CT_fint 64) gs;
+       [idecl l (CT_fint 64) gs;
         iblock (setup @ [call (CL_id (gs, CT_fint 64))] @ cleanup)]
      in
 
@@ -1036,9 +1036,9 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
      variable_init from_gs from_setup from_call from_cleanup
      @ variable_init to_gs to_setup to_call to_cleanup
      @ variable_init step_gs step_setup step_call step_cleanup
-     @ [iblock ([idecl (CT_fint 64) loop_var;
+     @ [iblock ([idecl l (CT_fint 64) loop_var;
                  icopy l (CL_id (loop_var, (CT_fint 64))) (V_id (from_gs, CT_fint 64));
-                 idecl CT_unit body_gs]
+                 idecl l CT_unit body_gs]
                 @ body
                 @ [ilabel loop_end_label])],
      (fun clexp -> icopy l clexp unit_cval),
@@ -1046,11 +1046,11 @@ let rec compile_aexp ctx (AE_aux (aexp_aux, env, l)) =
 
 and compile_block ctx = function
   | [] -> []
-  | exp :: exps ->
+  | (AE_aux (_, _, l) as exp) :: exps ->
      let setup, call, cleanup = compile_aexp ctx exp in
      let rest = compile_block ctx exps in
      let gs = ngensym () in
-     iblock (setup @ [idecl CT_unit gs; call (CL_id (gs, CT_unit))] @ cleanup) :: rest
+     iblock (setup @ [idecl l CT_unit gs; call (CL_id (gs, CT_unit))] @ cleanup) :: rest
 
 let fast_int = function
   | CT_lint when !optimize_aarch64_fast_struct -> CT_fint 64
@@ -1209,7 +1209,7 @@ let rec compile_arg_pats ctx label (P_aux (p_aux, (l, _)) as pat) ctyps =
      let arg_id, (destructure, cleanup) = compile_arg_pat ctx label pat (CT_tup ctyps) in
      let new_ids = List.map (fun ctyp -> gensym (), ctyp) ctyps in
      destructure
-     @ [idecl (CT_tup ctyps) (name arg_id)]
+     @ [idecl l (CT_tup ctyps) (name arg_id)]
      @ List.mapi (fun i (id, ctyp) -> icopy l (CL_tuple (CL_id (name arg_id, CT_tup ctyps), i)) (V_id (name id, ctyp))) new_ids,
      List.map (fun (id, _) -> id, ([], [])) new_ids,
      [iclear (CT_tup ctyps) (name arg_id)]
@@ -1315,14 +1315,14 @@ let compile_funcl ctx id pat guard exp =
   let guard_bindings = ref IdSet.empty in
   let guard_instrs = match guard with
     | Some guard ->
-       let guard = anf guard in
+       let (AE_aux (_, _, l) as guard) = anf guard in
        guard_bindings := aexp_bindings guard;
        let guard_aexp = C.optimize_anf ctx (no_shadow (pat_ids pat) guard) in
        let guard_setup, guard_call, guard_cleanup = compile_aexp ctx guard_aexp in
        let guard_label = label "guard_" in
        let gs = ngensym () in
        [iblock (
-            [idecl CT_bool gs]
+            [idecl l CT_bool gs]
             @ guard_setup
             @ [guard_call (CL_id (gs, CT_bool))]
             @ guard_cleanup
@@ -1443,7 +1443,7 @@ and compile_def' n total ctx = function
      let end_label = label "let_end_" in
      let destructure, destructure_cleanup, _ = compile_match ctx apat (V_id (gs, ctyp)) end_label in
      let gs_setup, gs_cleanup =
-       [idecl ctyp gs], [iclear ctyp gs]
+       [idecl (exp_loc exp) ctyp gs], [iclear ctyp gs]
      in
      let bindings = List.map (fun (id, typ) -> id, ctyp_of_typ ctx typ) (apat_globals apat) in
      let n = !letdef_count in
@@ -1515,7 +1515,7 @@ let rec specialize_variants ctx prior =
            [], unpoly cval, []
          else
            let gs = ngensym () in
-           [idecl suprema gs;
+           [idecl l suprema gs;
             icopy l (CL_id (gs, suprema)) (unpoly cval)],
            V_id (gs, suprema),
            [iclear suprema gs]
diff --git a/src/jib/jib_ir.ml b/src/jib/jib_ir.ml
index d30fe183..fe2cc125 100644
--- a/src/jib/jib_ir.ml
+++ b/src/jib/jib_ir.ml
@@ -98,12 +98,34 @@ module Ir_formatter = struct
   end
 
   module Make (C : Config) = struct
+    let file_map = ref []
+
+    let file_number file_name =
+      let rec scan n = function
+        | (f :: fs) -> if f = file_name then n else scan (n + 1) fs
+        | [] -> (file_map := !file_map @ [file_name]; n)
+      in
+      scan 0 !file_map
+
+    let output_loc l =
+      match Reporting.simp_loc l with
+      | None -> "`"
+      | Some (p1, p2) ->
+         Printf.sprintf "%d %d:%d-%d:%d"
+           (file_number p1.pos_fname) p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol)
+
+    let output_files buf =
+      Buffer.add_string buf (C.keyword "files");
+      List.iter (fun file_name ->
+          Buffer.add_string buf (" \"" ^ file_name ^ "\"")
+        ) !file_map
+        
     let rec output_instr n buf indent label_map (I_aux (instr, (_, l))) =
       match instr with
       | I_decl (ctyp, id) | I_reset (ctyp, id) ->
-         add_instr n buf indent (string_of_name id ^ " : " ^ C.typ ctyp)
+         add_instr n buf indent (string_of_name id ^ " : " ^ C.typ ctyp ^ " `" ^ output_loc l)
       | I_init (ctyp, id, cval) | I_reinit (ctyp, id, cval) ->
-         add_instr n buf indent (string_of_name id ^ " : " ^ C.typ ctyp ^ " = " ^ C.value cval)
+         add_instr n buf indent (string_of_name id ^ " : " ^ C.typ ctyp ^ " = " ^ C.value cval ^ " `" ^ output_loc l)
       | I_clear (ctyp, id) ->
          add_instr n buf indent ("!" ^ string_of_name id)
       | I_label label ->
@@ -111,7 +133,7 @@ module Ir_formatter = struct
       | I_jump (cval, label) ->
          add_instr n buf indent (C.keyword "jump" ^ " " ^ C.value cval ^ " "
                                  ^ C.keyword "goto" ^ " " ^ C.string_of_label (StringMap.find label label_map)
-                                 ^ " ` \"" ^ Reporting.short_loc_to_string l ^ "\"")
+                                 ^ " `" ^ output_loc l)
       | I_goto label ->
          add_instr n buf indent (C.keyword "goto" ^ " " ^ C.string_of_label (StringMap.find label label_map))
       | I_match_failure ->
@@ -123,9 +145,9 @@ module Ir_formatter = struct
       | I_copy (clexp, cval) ->
          add_instr n buf indent (string_of_clexp clexp ^ " = " ^ C.value cval)
       | I_funcall (clexp, false, id, args) ->
-         add_instr n buf indent (string_of_clexp clexp ^ " = " ^ string_of_uid id ^ "(" ^ Util.string_of_list ", " C.value args ^ ")")
+         add_instr n buf indent (string_of_clexp clexp ^ " = " ^ string_of_uid id ^ "(" ^ Util.string_of_list ", " C.value args ^ ")" ^ " `" ^ output_loc l)
       | I_funcall (clexp, true, id, args) ->
-         add_instr n buf indent (string_of_clexp clexp ^ " = $" ^ string_of_uid id ^ "(" ^ Util.string_of_list ", " C.value args ^ ")")
+         add_instr n buf indent (string_of_clexp clexp ^ " = $" ^ string_of_uid id ^ "(" ^ Util.string_of_list ", " C.value args ^ ")" ^ " `" ^ output_loc l)
       | I_return cval ->
          add_instr n buf indent (C.keyword "return" ^ " " ^ C.value cval)
       | I_comment str ->
@@ -184,13 +206,18 @@ module Ir_formatter = struct
       | CDEF_startup _ | CDEF_finish _ ->
          Reporting.unreachable Parse_ast.Unknown __POS__ "Unexpected startup / finish"
 
-    let rec output_defs buf = function
+    let rec output_defs' buf = function
       | def :: defs ->
          output_def buf def;
          Buffer.add_string buf "\n\n";
-         output_defs buf defs
+         output_defs' buf defs
       | [] -> ()
 
+    let output_defs buf defs =
+      output_defs' buf defs;
+      output_files buf;
+      Buffer.add_string buf "\n\n"
+      
   end
 end
 
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 434ca8a9..78c15226 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1962,7 +1962,7 @@ let rec find_function lets id = function
   | CDEF_fundef (id', heap_return, args, body) :: _ when Id.compare id id' = 0 ->
      lets, Some (heap_return, args, body)
   | CDEF_let (_, vars, setup) :: cdefs ->
-     let vars = List.map (fun (id, ctyp) -> idecl ctyp (global id)) vars in
+     let vars = List.map (fun (id, ctyp) -> idecl (id_loc id) ctyp (global id)) vars in
      find_function (lets @ vars @ setup) id cdefs;
   | _ :: cdefs ->
      find_function lets id cdefs
@@ -2148,7 +2148,7 @@ let expand_reg_deref env register_map = function
            let try_reg r =
              let next_label = label "next_reg_write_" in
              [ijump l (V_call (Neq, [V_lit (VL_ref (string_of_id r), reg_ctyp); V_id (id, ctyp)])) next_label;
-              ifuncall (CL_id (global r, reg_ctyp)) function_id args;
+              ifuncall l (CL_id (global r, reg_ctyp)) function_id args;
               igoto end_label;
               ilabel next_label]
            in
@@ -2270,7 +2270,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function
         (* When we create each argument declaration, give it a unique
            location from the $property pragma, so we can identify it later. *)
         let arg_decls =
-          List.map2 (fun id ctyp -> let l = unique pragma_l in idecl ~loc:l ctyp (name id)) args arg_ctyps
+          List.map2 (fun id ctyp -> let l = unique pragma_l in idecl l ctyp (name id)) args arg_ctyps
         in
         let instrs =
           let open Jib_optimize in
@@ -2328,7 +2328,7 @@ let smt_cdef props lets name_file ctx all_cdefs = function
 let rec smt_cdefs props lets name_file ctx ast =
   function
   | CDEF_let (_, vars, setup) :: cdefs ->
-     let vars = List.map (fun (id, ctyp) -> idecl ctyp (global id)) vars in
+     let vars = List.map (fun (id, ctyp) -> idecl (id_loc id) ctyp (global id)) vars in
      smt_cdefs props (lets @ vars @ setup) name_file ctx ast cdefs;
   | cdef :: cdefs ->
      smt_cdef props lets name_file ctx ast cdef;
diff --git a/src/jib/jib_smt_fuzz.ml b/src/jib/jib_smt_fuzz.ml
index 58665bde..68e5751d 100644
--- a/src/jib/jib_smt_fuzz.ml
+++ b/src/jib/jib_smt_fuzz.ml
@@ -187,7 +187,7 @@ let fuzz_cdef ctx all_cdefs = function
 
                  let jib =
                    let gs = ngensym () in
-                   [ifuncall (CL_id (gs, ret_ctyp)) (id, []) (List.map snd values)]
+                   [ifuncall (id_loc id) (CL_id (gs, ret_ctyp)) (id, []) (List.map snd values)]
                    @ gen_assertion ret_ctyp result gs
                    @ [iend ()]
                  in
diff --git a/src/jib/jib_util.ml b/src/jib/jib_util.ml
index 88f09bcf..179826ed 100644
--- a/src/jib/jib_util.ml
+++ b/src/jib/jib_util.ml
@@ -74,19 +74,19 @@ let instr_number () =
   incr instr_counter;
   n
 
-let idecl ?loc:(l=Parse_ast.Unknown) ctyp id =
+let idecl l ctyp id =
   I_aux (I_decl (ctyp, id), (instr_number (), l))
 
 let ireset ?loc:(l=Parse_ast.Unknown) ctyp id =
   I_aux (I_reset (ctyp, id), (instr_number (), l))
 
-let iinit ?loc:(l=Parse_ast.Unknown) ctyp id cval =
+let iinit l ctyp id cval =
   I_aux (I_init (ctyp, id, cval), (instr_number (), l))
 
 let iif l cval then_instrs else_instrs ctyp =
   I_aux (I_if (cval, then_instrs, else_instrs, ctyp), (instr_number (), l))
 
-let ifuncall ?loc:(l=Parse_ast.Unknown) clexp id cvals =
+let ifuncall l clexp id cvals =
   I_aux (I_funcall (clexp, false, id, cvals), (instr_number (), l))
 
 let iextern ?loc:(l=Parse_ast.Unknown) clexp id cvals =
diff --git a/src/reporting.ml b/src/reporting.ml
index 603bc84f..b910de1e 100644
--- a/src/reporting.ml
+++ b/src/reporting.ml
@@ -126,7 +126,7 @@ let short_loc_to_string l =
   | Some (p1, p2) ->
      Printf.sprintf "%s %d:%d - %d:%d"
        p1.pos_fname p1.pos_lnum (p1.pos_cnum - p1.pos_bol) p2.pos_lnum (p2.pos_cnum - p2.pos_bol)
-
+ 
 let loc_to_coverage l =
   match simp_loc l with
   | None -> None