From 212b16bd15ea39ae3b35efdce7cef549fe4f1657 Mon Sep 17 00:00:00 2001 From: Alasdair Date: Fri, 5 Mar 2021 16:52:35 +0000 Subject: Add more location information to IR --- src/jib/c_backend.ml | 12 +++---- src/jib/c_codegen.ml | 6 ++-- src/jib/jib_compile.ml | 88 ++++++++++++++++++++++++------------------------- src/jib/jib_ir.ml | 41 +++++++++++++++++++---- src/jib/jib_smt.ml | 8 ++--- src/jib/jib_smt_fuzz.ml | 2 +- src/jib/jib_util.ml | 6 ++-- src/reporting.ml | 2 +- 8 files changed, 96 insertions(+), 69 deletions(-) (limited to 'src') 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 -- cgit v1.2.3