Add more location information to IR

1 files changed, 44 insertions, 44 deletions

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]