From 5478f3be642e71d0f0309ed093647429dd8d590b Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Tue, 18 Sep 2018 09:03:22 -0700 Subject: [PATCH] [log] source location info when dying in the backend Summary: Now we see which file/procedure/instruction is responsible for a crash in the backend. Biabduction and eradicate not supported yet for the instruction-level debug. Reviewed By: mbouaziz, da319 Differential Revision: D9915666 fbshipit-source-id: 279472305 --- infer/src/absint/AbstractInterpreter.ml | 6 +++++- infer/src/absint/Scheduler.ml | 7 +++++-- infer/src/backend/ondemand.ml | 10 ++++++++-- 3 files changed, 18 insertions(+), 5 deletions(-) diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 53bf21384..41a9ab3d3 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -94,7 +94,11 @@ struct ~pp_name:(TransferFunctions.pp_session_name node) (Node.underlying_node node) ; let astate_post = - let compute_post pre instr = TransferFunctions.exec_instr pre proc_data node instr in + let compute_post pre instr = + try TransferFunctions.exec_instr pre proc_data node instr with exn -> + IExn.reraise_after exn ~f:(fun () -> + L.internal_error "In instruction %a@\n" (Sil.pp_instr Pp.text) instr ) + in Instrs.fold ~f:compute_post ~init:pre instrs in if debug then ( diff --git a/infer/src/absint/Scheduler.ml b/infer/src/absint/Scheduler.ml index f7e457b49..aadd98f67 100644 --- a/infer/src/absint/Scheduler.ml +++ b/infer/src/absint/Scheduler.ml @@ -73,8 +73,11 @@ module ReversePostorder (CFG : ProcCfg.S) = struct let schedule_succ worklist_acc node_to_schedule = let id_to_schedule = CFG.Node.id node_to_schedule in let old_work = - try M.find id_to_schedule worklist_acc with Caml.Not_found -> - WorkUnit.make t.cfg node_to_schedule + match M.find_opt id_to_schedule worklist_acc with + | Some work -> + work + | None -> + WorkUnit.make t.cfg node_to_schedule in let new_work = WorkUnit.add_visited_pred t.cfg old_work node_id in M.add id_to_schedule new_work worklist_acc diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index 418ea5724..a0dca52cd 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -164,8 +164,8 @@ let run_proc_analysis analyze_proc ~caller_pdesc callee_pdesc = in let old_state = save_global_state () in let initial_summary = preprocess () in + let attributes = Procdesc.get_attributes callee_pdesc in try - let attributes = Procdesc.get_attributes callee_pdesc in let summary = if attributes.ProcAttributes.is_defined then analyze_proc initial_summary callee_pdesc else initial_summary @@ -173,7 +173,13 @@ let run_proc_analysis analyze_proc ~caller_pdesc callee_pdesc = let final_summary = postprocess summary in restore_global_state old_state ; final_summary with exn -> ( - IExn.reraise_if exn ~f:(fun () -> restore_global_state old_state ; not Config.keep_going) ; + IExn.reraise_if exn ~f:(fun () -> + let source_file = attributes.ProcAttributes.translation_unit in + let location = attributes.ProcAttributes.loc in + L.internal_error "While analysing function %a:%a at %a@\n" SourceFile.pp source_file + Typ.Procname.pp callee_pname Location.pp_file_pos location ; + restore_global_state old_state ; + not Config.keep_going ) ; L.internal_error "@\nERROR RUNNING BACKEND: %a %s@\n@\nBACK TRACE@\n%s@?" Typ.Procname.pp callee_pname (Exn.to_string exn) (Printexc.get_backtrace ()) ; match exn with