[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

@@ -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 (

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 ->
+        match M.find_opt id_to_schedule worklist_acc with
-          WorkUnit.make t.cfg node_to_schedule
+        | 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

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