Guard or annotate exception catchalls according to the linter

boot/util.ml

@@ -10,7 +10,7 @@
 
 let parse_env_line l =
   try Scanf.sscanf l "%[^=]=%S" (fun name value -> Some(name,value))
-  with _ -> None
+  with Scanf.Scan_failure _ | End_of_file -> None
 
 let with_ic file f =
   let ic = open_in file in

checker/check.ml

@@ -312,7 +312,7 @@ let marshal_in_segment (type a) ~validate ~value ~(segment : a ObjFile.segment)
         let digest = Digest.input ch in
         let () = if not (String.equal digest segment.ObjFile.hash) then raise_notrace Exit in
         v
-      with _ ->
+      with exn when CErrors.noncritical exn ->
         CErrors.user_err (str "Corrupted file " ++ quote (str f))
     in
     let () = Validate.validate value v in

checker/checker.ml

@@ -55,7 +55,7 @@ let get_version () =
     let rev = input_line ch in
     let () = close_in ch in
     Printf.sprintf "%s (%s)" ver rev
-  with _ -> Coq_config.version
+  with Sys_error _ | End_of_file -> Coq_config.version
 
 let print_header () =
   Printf.printf "Welcome to Chicken %s\n%!" (get_version ())
@@ -396,7 +396,7 @@ let init_with_argv argv =
       (List.rev !includes);
     includes := [];
     make_senv ()
-  with e ->
+  with e [@coqlint.allow_catchall "fatal"] ->
     fatal_error (str "Error during initialization :" ++ (explain_exn e)) (is_anomaly e)
 
 let init() = init_with_argv Sys.argv
@@ -405,7 +405,7 @@ let run senv =
   try
     let senv = compile_files senv in
     flush_all(); senv
-  with e ->
+  with e [@coqlint.allow_catchall "fatal"] ->
     if CDebug.(get_flag misc) then Printexc.print_backtrace stderr;
     fatal_error (explain_exn e) (is_anomaly e)
 

clib/terminal.ml

@@ -312,7 +312,7 @@ let parse s =
         let attrs = List.map int_of_string attrs in
         let attrs = parse_style (make ()) attrs in
         (name, attrs) :: accu
-      with _ -> accu
+      with Failure _ | Invalid_argument _ -> accu
     in
     accu
   | _ -> accu

engine/termops.ml

@@ -88,7 +88,10 @@ module Internal = struct
 
   let protect f x =
     try f x
-    with e -> str "EXCEPTION: " ++ str (Printexc.to_string e)
+    with e when
+        (* maybe should be just "not is_interrupted"? *)
+        CErrors.noncritical e || !Flags.in_debugger ->
+      str "EXCEPTION: " ++ str (Printexc.to_string e)
 
   let print_kconstr env sigma a =
     protect (fun c -> print_constr_env env sigma c) a

kernel/nativelib.ml

@@ -43,7 +43,7 @@ let () = at_exit (fun () ->
         let d = Lazy.force my_temp_dir in
         Array.iter (fun f -> Sys.remove (Filename.concat d f)) (Sys.readdir d);
         Unix.rmdir d
-      with e ->
+      with (Unix.Unix_error _ | Sys_error _) as e ->
         Feedback.msg_warning
           Pp.(str "Native compile: failed to cleanup: " ++
               str(Printexc.to_string e) ++ fnl()))

lib/cErrors.ml

@@ -117,7 +117,7 @@ let print_gen ~anomaly (e, info) =
   in
   try
     extra_msg ++ print_gen ~anomaly !handle_stack e
-  with exn ->
+  with exn [@coqlint.allow_catchall "grandfathered"] ->
     let exn, info = Exninfo.capture exn in
     (* exception in error printer *)
     str "<in exception printer>:" ++ spc() ++ print_anomaly anomaly exn ++

lib/envars.ml

@@ -14,7 +14,7 @@ open Util
 
 let parse_env_line l =
   try Scanf.sscanf l "%[^=]=%S" (fun name value -> Some(name,value))
-  with _ -> None
+  with Scanf.Scan_failure _ | End_of_file -> None
 
 let with_ic file f =
   let ic = open_in file in

lib/spawn.ml

@@ -148,7 +148,7 @@ let spawn_with_control prefer_sock env prog args =
 let output_death_sentence pid oob_req =
   prerr_endline ("death sentence for " ^ pid);
   try output_value oob_req ReqDie; flush oob_req
-  with e -> prerr_endline ("death sentence: " ^ Printexc.to_string e)
+  with e when CErrors.noncritical e -> prerr_endline ("death sentence: " ^ Printexc.to_string e)
 
 (* spawn a process and read its output asynchronously *)
 module Async(ML : MainLoopModel) = struct
@@ -183,7 +183,7 @@ let kill ({ pid = unixpid; oob_resp; oob_req; cin; cout; alive; watch } as p) =
     Option.iter close_out_noerr oob_req;
     if Sys.os_type = "Unix" then Unix.kill unixpid Sys.sigkill;
     p.watch <- None
-  with e -> prerr_endline ("kill: "^Printexc.to_string e) end
+  with e when CErrors.noncritical e -> prerr_endline ("kill: "^Printexc.to_string e) end
 
 let spawn ?(prefer_sock=prefer_sock) ?(env=Unix.environment ())
     prog args callback
@@ -252,7 +252,7 @@ let kill ({ pid = unixpid; oob_req; oob_resp; cin; cout; alive } as p) =
     Option.iter close_in_noerr oob_resp;
     Option.iter close_out_noerr oob_req;
     if Sys.os_type = "Unix" then Unix.kill unixpid Sys.sigkill;
-  with e -> prerr_endline ("kill: "^Printexc.to_string e) end
+  with e when CErrors.noncritical e -> prerr_endline ("kill: "^Printexc.to_string e) end
 
 let rec wait p =
   (* On windows kill is not reliable, so wait may never return. *)

lib/system.ml

@@ -74,7 +74,7 @@ let apply_subdir f path name =
     | Unix.S_REG -> f (FileRegular name)
     | _ -> ()
 
-let readdir dir = try Sys.readdir dir with any -> [||]
+let readdir dir = try Sys.readdir dir with Sys_error _ -> [||]
 
 let process_directory f path =
   Array.iter (apply_subdir f path) (readdir path)
@@ -362,7 +362,7 @@ let measure_duration f x =
     let y = f x in
     let stop = get_time() in
     Ok (y, duration_between ~start ~stop)
-  with e ->
+  with e [@coqlint.allow_catchall "caller must reraise"] ->
     let stop = get_time() in
     let exn = Exninfo.capture e in
     Error (exn, duration_between ~start ~stop)
@@ -399,7 +399,7 @@ let count_instructions f x =
     let y = f x in
     let c_end = Instr.read_counter () in
     Ok(y, instructions_between ~c_start ~c_end)
-  with e ->
+  with e [@coqlint.allow_catchall "caller must reraise"] ->
     let exn = Exninfo.capture e in
     let c_end = Instr.read_counter () in
     Error(exn, instructions_between ~c_start ~c_end)

plugins/ltac/tactic_debug.ml

@@ -69,7 +69,7 @@ let update_bpt fname offset opt =
           (try
             let p = Loadpath.find_load_path (CUnix.physical_path_of_string dirname) in
             DirPath.repr (Loadpath.logical p)
-          with _ -> []))
+          with exn when CErrors.noncritical exn -> []))
     end
   in
   let dirpath = DirPath.to_string dp in
@@ -170,14 +170,14 @@ let cvt_loc loc =
              let knlen = String.length text in
              let lastdot = String.rindex text '.' in
              String.sub text (lastdot+1) (knlen - (lastdot + 1))
-           with _ -> text
+           with exn when CErrors.noncritical exn -> text
          in
          Printf.sprintf "%s:%d, %s  (%s)" routine line_nb file module_name;
        | Some { fname=ToplevelInput; line_nb } ->
          let items = String.split_on_char '.' text in
          Printf.sprintf "%s:%d, %s" (List.nth items 1) line_nb (List.hd items);
        | _ -> text
-   with _ -> text
+   with exn when CErrors.noncritical exn -> text
 
 let format_stack s =
   List.map (fun (tac, loc) ->

plugins/ltac2/tac2core.ml

@@ -217,7 +217,8 @@ let catchable_exception = function
 *)
 let wrap_exceptions ?(passthrough=false) f =
   try f ()
-  with e ->
+  with e [@coqlint.allow_catchall "will be reraised if critical"] ->
+    (* not sure if it's fully correct to do a tclBIND when we got a critical exn *)
     let e, info = Exninfo.capture e in
     set_bt info >>= fun info ->
     if not passthrough && catchable_exception e

plugins/ltac2/tac2print.ml

@@ -870,20 +870,26 @@ end
 
 let () = register_init "constr" begin fun env sigma c ->
   let c = to_constr c in
-  let c = try Printer.pr_leconstr_env env sigma c with _ -> str "..." in
+  let c = try Printer.pr_leconstr_env env sigma c
+    with _ [@coqlint.allow_catchall "grandfathered"] -> str "..."
+  in
   hov 2 (str "constr:(" ++ c ++ str ")")
 end
 
 let () = register_init "preterm" begin fun env sigma c ->
   let c = to_preterm c in
   (* XXX should we get the ltac2 env out of the closure and print it too? Maybe with a debug flag? *)
-  let c = try Printer.pr_closed_glob_env env sigma c with _ -> str "..." in
+  let c = try Printer.pr_closed_glob_env env sigma c
+    with _ [@coqlint.allow_catchall "grandfathered"] -> str "..."
+  in
   hov 2 (str "preterm:(" ++ c ++ str ")")
 end
 
 let () = register_init "pattern" begin fun env sigma c ->
   let c = to_pattern c in
-  let c = try Printer.pr_lconstr_pattern_env env sigma c with _ -> str "..." in
+  let c = try Printer.pr_lconstr_pattern_env env sigma c
+    with _ [@coqlint.allow_catchall "grandfathered"] -> str "..."
+  in
   hov 2 (str "pat:(" ++ c ++ str ")")
 end
 

plugins/micromega/coq_micromega.ml

@@ -1971,11 +1971,7 @@ Tacticals.tclTHEN
                   ( EConstr.mkVar goal_name
                   , arith_args @ List.map EConstr.mkVar ids )))
       with
-      | CsdpNotFound -> fail_csdp_not_found ()
-      | x ->
-        if debug then
-          Tacticals.tclFAIL (Pp.str (Printexc.get_backtrace ()))
-        else raise x)
+      | CsdpNotFound -> fail_csdp_not_found ())
 
 let micromega_wit_gen pre_process cnf spec prover wit_id ff =
   Proofview.Goal.enter (fun gl ->
@@ -1997,12 +1993,7 @@ let micromega_wit_gen pre_process cnf spec prover wit_id ff =
           let tres' = EConstr.mkApp (Lazy.force coq_list, [|spec.proof_typ|]) in
           Tactics.letin_tac
             None (Names.Name wit_id) res' (Some tres') Locusops.nowhere
-      with
-      | CsdpNotFound -> fail_csdp_not_found ()
-      | x ->
-        if debug then
-          Tacticals.tclFAIL (Pp.str (Printexc.get_backtrace ()))
-        else raise x)
+      with CsdpNotFound -> fail_csdp_not_found ())
 
 let micromega_order_changer cert env ff =
   (*let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *)
@@ -2126,8 +2117,7 @@ let micromega_genr prover tac =
                 [ Generalize.generalize (List.map EConstr.mkVar ids)
                 ; Tactics.exact_check
                     (EConstr.applist (EConstr.mkVar goal_name, arith_args)) ] ]
-      with
-      | CsdpNotFound -> fail_csdp_not_found ())
+      with CsdpNotFound -> fail_csdp_not_found ())
 
 let lift_ratproof prover l =
   match prover l with

plugins/micromega/mutils.ml

@@ -360,10 +360,11 @@ let command exe_path args vl =
       | Unix.WEXITED 0 -> (
         let inch = Unix.in_channel_of_descr stdout_read in
         try Marshal.from_channel inch
-        with any ->
+        with (End_of_file | Failure _) as exn ->
           failwith
-            (Printf.sprintf "command \"%s\" exited %s" exe_path
-               (Printexc.to_string any)) )
+            (Printf.sprintf "command \"%s\" exited with code 0 but result could not be read back: %s"
+               exe_path
+               (Printexc.to_string exn)) )
       | Unix.WEXITED i ->
         failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i)
       | Unix.WSIGNALED i ->
@@ -373,7 +374,7 @@ let command exe_path args vl =
     (* Cleanup  *)
       (fun () ->
       List.iter
-        (fun x -> try Unix.close x with any -> ())
+        (fun x -> try Unix.close x with Unix.Unix_error _ -> ())
         [ stdin_read
         ; stdin_write
         ; stdout_read

plugins/ssr/ssrcommon.ml

@@ -795,8 +795,7 @@ let saturate ?(beta=false) ?(bi_types=false) env sigma c ?(ty=Retyping.get_type_
    loop ty [] sigma m
 
 let dependent_apply_error =
-  try CErrors.user_err (Pp.str "Could not fill dependent hole in \"apply\"")
-  with err -> err
+  CErrors.UserError (Pp.str "Could not fill dependent hole in \"apply\"")
 
 (* TASSI: Sometimes Coq's apply fails. According to my experience it may be
  * related to goals that are products and with beta redexes. In that case it

pretyping/reductionops.ml

@@ -1229,7 +1229,7 @@ let is_fconv ?(reds=TransparentState.full) pb env sigma t1 t2 =
       | Result.Error (Some e) -> Empty.abort e
       end
     with
-    | e ->
+    | e [@coqlint.allow_catchall "report_anomaly"] ->
       let e = Exninfo.capture e in
       report_anomaly e
 
@@ -1337,7 +1337,7 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Conversion.CUMUL)
             | Result.Error (Some e) -> raise (UGraph.UniverseInconsistency e)
   with
   | UGraph.UniverseInconsistency _ when catch_incon -> None
-  | e ->
+  | e [@coqlint.allow_catchall "report_anomaly"] ->
     let e = Exninfo.capture e in
     report_anomaly e
 
@@ -1368,7 +1368,7 @@ let infer_conv_ustate ?(catch_incon=true) ?(pb=Conversion.CUMUL)
         | Result.Error (Some e) -> raise (UGraph.UniverseInconsistency e)
   with
   | UGraph.UniverseInconsistency _ when catch_incon -> None
-  | e ->
+  | e [@coqlint.allow_catchall "report_anomaly"] ->
     let e = Exninfo.capture e in
     report_anomaly e
 

stm/asyncTaskQueue.ml

@@ -336,7 +336,7 @@ module Make(T : Task) () = struct
         stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2
       | End_of_file ->
         stm_prerr_endline "connection lost"; flush_all (); exit 2
-      | e ->
+      | e [@coqlint.allow_catchall "fatal"] ->
         stm_pr_err Pp.(seq [str "Slave: critical exception: "; print e]);
         flush_all (); exit 1
     done

stm/partac.ml

@@ -131,7 +131,7 @@ end = struct (* {{{ *)
                       str" solves the goal and leaves no unresolved existential variables. The following" ++
                       str" existentials remain unsolved: " ++ prlist (Termops.pr_existential_key (Global.env ()) sigma) (Evar.Set.elements evars))
        )
-    with e ->
+    with e [@coqlint.allow_catchall "grandfathered"] ->
       let noncrit = CErrors.noncritical e in
       RespError (noncrit, CErrors.print e ++ spc() ++ str "(for goal "++int r_goalno ++ str ")")
 

stm/spawned.ml

@@ -34,7 +34,7 @@ let controller h pr pw =
         | Hello _ -> prerr_endline "internal protocol error"; exit 1
         | ReqDie -> prerr_endline "death sentence received"; exit 0
       with
-      | e ->
+      | e [@coqlint.allow_catchall "fatal"] ->
         prerr_endline ("control channel broken: " ^ Printexc.to_string e);
         exit 1 in
     loop () in

stm/stm.ml

@@ -772,7 +772,7 @@ end = struct (* {{{ *)
 
     let run_command () =
       try while true do get_last_job () () done
-      with e -> () (* No failure *)
+      with e [@coqlint.allow_catchall "grandfathered"] -> () (* No failure *)
 
     let command ~now job =
       if now then job ()
@@ -2538,7 +2538,7 @@ let process_transaction ~doc ?(newtip=Stateid.fresh ()) x c =
     stm_pperr_endline (fun () -> str "processed with " ++ pr_rc rc ++ str " }}}");
     VCS.print ();
     rc
-  with e ->
+  with e [@coqlint.allow_catchall "handle_failure reraises"] ->
     let e = Exninfo.capture e in
     handle_failure e vcs
 
@@ -2754,11 +2754,12 @@ let edit_at ~doc id =
     doc, rc
   with
   | Vcs_aux.Expired -> user_err Pp.(str "Unknown state " ++ Stateid.print id ++ str".")
-  | e ->
+  | e [@coqlint.allow_catchall "reraises"] ->
     let (e, info) = Exninfo.capture e in
     match Stateid.get info with
     | None ->
         VCS.print ();
+        (* should we be raising the original exn when it's critical? *)
         anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
           CErrors.print_no_report e ++ str ".")
     | Some (_, id) ->

stm/stmargs.ml

@@ -133,7 +133,7 @@ let parse_args ~init arglist : Stm.AsyncOpts.stm_opt * string list =
   in
   try
     parse init
-  with any -> fatal_error any
+  with any [@coqlint.allow_catchall "fatal"] -> fatal_error any
 
 let usage = "\
 \n  -stm-debug             STM debug mode (will trace every transaction)\

sysinit/coqargs.ml

@@ -444,7 +444,7 @@ let parse_args ~usage ~init arglist : t * string list =
   in
   try
     parse init
-  with any -> fatal_error any
+  with any [@coqlint.allow_catchall "fatal"] -> fatal_error any
 
 (* We need to reverse a few lists *)
 let parse_args ~usage ~init args =

sysinit/coqinit.ml

@@ -120,7 +120,7 @@ let print_memory_stat () =
     let oc = open_out fn in
     Gc.print_stat oc;
     close_out oc
-  with _ -> ()
+  with exn when CErrors.noncritical exn -> ()
 
 let init_load_paths opts =
   let open Coqargs in