From 71f20908a19e508635c55631b59bf3d6a2ba48fb Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Wed, 24 May 2017 06:53:55 -0700 Subject: [PATCH] [logging] revert to using `assert false` since we catch `Assert_failure` in some places Summary: A recent diff tried to replace `L.out "error message"; assert false` with `failwith "error message"` but infer relies on the type of raised exceptions to sometimes keep going. A more careful change will be needed but in the meantime restore the old behaviour. Reviewed By: jberdine Differential Revision: D5112969 fbshipit-source-id: 713fe20 --- infer/src/IR/Procdesc.re | 4 +++- infer/src/IR/Typ.re | 5 ++++- infer/src/backend/abs.ml | 11 ++++++----- infer/src/backend/dotty.ml | 10 ++++++---- infer/src/backend/interproc.ml | 6 ++++-- infer/src/backend/match.ml | 9 ++++----- infer/src/backend/prop.ml | 14 +++++++------- infer/src/backend/symExec.ml | 3 ++- infer/src/base/DB.ml | 3 ++- infer/src/base/Logging.ml | 2 +- infer/src/base/Logging.mli | 2 +- infer/src/clang/Capture.re | 3 ++- infer/src/clang/cFrontend_errors.ml | 10 +++++++--- infer/src/clang/cTrans.ml | 3 ++- infer/src/clang/cTrans_utils.ml | 3 ++- infer/src/harness/inhabit.ml | 3 ++- 16 files changed, 55 insertions(+), 36 deletions(-) diff --git a/infer/src/IR/Procdesc.re b/infer/src/IR/Procdesc.re index cdc7fc78b..3c70b4e12 100644 --- a/infer/src/IR/Procdesc.re +++ b/infer/src/IR/Procdesc.re @@ -119,7 +119,9 @@ module Node = { /** Get the name of the procedure the node belongs to */ let get_proc_name node => switch node.pname_opt { - | None => failwithf "get_proc_name: at node %d" node.id + | None => + L.out "get_proc_name: at node %d@\n" node.id; + assert false | Some pname => pname }; diff --git a/infer/src/IR/Typ.re b/infer/src/IR/Typ.re index 5eea23f98..57a66b779 100644 --- a/infer/src/IR/Typ.re +++ b/infer/src/IR/Typ.re @@ -371,7 +371,10 @@ let name typ => let unsome s => fun | Some default_typ => default_typ - | None => failwithf "No default typ in %s@." s; + | None => { + L.out "No default typ in %s@." s; + assert false + }; /** turn a *T into a T. fails if [typ] is not a pointer type */ diff --git a/infer/src/backend/abs.ml b/infer/src/backend/abs.ml index a5bcaece1..d49174ff2 100644 --- a/infer/src/backend/abs.ml +++ b/infer/src/backend/abs.ml @@ -99,7 +99,7 @@ let mk_rule_ptspts_ls tenv impl_ok1 impl_ok2 (para: Sil.hpara) = let (para_fst_start, para_fst_rest) = let mark_impl_flag hpred = { Match.hpred = hpred; Match.flag = impl_ok1 } in match para_fst with - | [] -> failwithf "mk_rule_ptspts_ls (Empty Para): %a" (Sil.pp_hpara Pp.text) para + | [] -> L.out "@.@.ERROR (Empty Para): %a @.@." (Sil.pp_hpara Pp.text) para; assert false | hpred :: hpreds -> let hpat = mark_impl_flag hpred in let hpats = List.map ~f:mark_impl_flag hpreds in @@ -128,7 +128,7 @@ let mk_rule_ptsls_ls tenv k2 impl_ok1 impl_ok2 para = let (ids_exist, para_inst) = Sil.hpara_instantiate para exp_base exp_next exps_shared in let (para_inst_start, para_inst_rest) = match para_inst with - | [] -> failwithf "mk_rule_ptsls_ls (Empty Para): %a" (Sil.pp_hpara Pp.text) para + | [] -> L.out "@.@.ERROR (Empty Para): %a @.@." (Sil.pp_hpara Pp.text) para; assert false | hpred :: hpreds -> let allow_impl hpred = { Match.hpred = hpred; Match.flag = impl_ok1 } in (allow_impl hpred, List.map ~f:allow_impl hpreds) in @@ -252,7 +252,7 @@ let mk_rule_ptspts_dll tenv impl_ok1 impl_ok2 para = let (para_fst_start, para_fst_rest) = let mark_impl_flag hpred = { Match.hpred = hpred; Match.flag = impl_ok1 } in match para_fst with - | [] -> failwithf "mk_rule_ptspts_dll (Empty DLL para): %a" (Sil.pp_hpara_dll Pp.text) para + | [] -> L.out "@.@.ERROR (Empty DLL para): %a@.@." (Sil.pp_hpara_dll Pp.text) para; assert false | hpred :: hpreds -> let hpat = mark_impl_flag hpred in let hpats = List.map ~f:mark_impl_flag hpreds in @@ -430,7 +430,8 @@ let typ_get_recursive_flds tenv typ_exp = | Exp.Var _ -> [] (* type of |-> not known yet *) | Exp.Const _ -> [] | _ -> - failwithf "@.typ_get_recursive: unexpected type expr: %a@." Exp.pp typ_exp + L.out "@.typ_get_recursive: unexpected type expr: %a@." Exp.pp typ_exp; + assert false let discover_para_roots tenv p root1 next1 root2 next2 : Sil.hpara option = let eq_arg1 = Exp.equal root1 next1 in @@ -601,7 +602,7 @@ let eqs_solve ids_in eqs_in = if not (List.exists ~f:(fun id' -> Ident.equal id id') ids_in) then None else let sub' = match Sil.extend_sub sub id e with - | None -> failwithf "ERROR : Buggy Implementation" + | None -> L.out "@.@.ERROR : Buggy Implementation.@.@."; assert false | Some sub' -> sub' in let eqs_rest' = eqs_sub sub' eqs_rest in solve sub' eqs_rest' in diff --git a/infer/src/backend/dotty.ml b/infer/src/backend/dotty.ml index d31d68cb6..01fd5c19d 100644 --- a/infer/src/backend/dotty.ml +++ b/infer/src/backend/dotty.ml @@ -113,8 +113,10 @@ let strip_special_chars b = let replace st c c' = if String.contains st c then begin let idx = String.index_exn st c in - String.set st idx c'; - st + try + String.set st idx c'; + st + with Invalid_argument _ -> L.out "@\n@\n Invalid argument!!! @\n @.@.@."; assert false end else st in let s0 = replace b '(' 'B' in let s1 = replace s0 '$' 'D' in @@ -427,7 +429,7 @@ let rec compute_target_struct_fields dotnodes list_fld p f lambda cycle = end else [(LinkStructToExp, Fieldname.to_string fn, n,"")] | _ -> (* by construction there must be at most 2 nodes for an expression*) - failwithf "Got more than 2 nodes, this should never happen!") + L.out "@\n Too many nodes! Error! @\n@.@."; assert false) | Sil.Estruct (_, _) -> [] (* inner struct are printed by print_struc function *) | Sil.Earray _ -> [] (* inner arrays are printed by print_array function *) in match list_fld with @@ -460,7 +462,7 @@ let rec compute_target_array_elements dotnodes list_elements p f lambda = end else [(LinkArrayToExp, Exp.to_string idx, n,"")] | _ -> (* by construction there must be at most 2 nodes for an expression*) - failwithf "Got more than 2 nodes, this should never happen!" + L.out "@\n Too many nodes! Error! @\n@.@."; assert false ) | Sil.Estruct (_, _) -> [] (* inner struct are printed by print_struc function *) | Sil.Earray _ ->[] (* inner arrays are printed by print_array function *) diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 1e27f6c73..b5f13940e 100644 --- a/infer/src/backend/interproc.ml +++ b/infer/src/backend/interproc.ml @@ -117,7 +117,8 @@ module Worklist = struct Procdesc.NodeMap.add min.node (min.visits + 1) wl.visit_map; (* increase the visits *) min.node with Not_found -> begin - failwithf "Work list is empty! Impossible to remove edge." + L.out "@\n...Work list is empty! Impossible to remove edge...@\n"; + assert false end end (* =============== END of module Worklist =============== *) @@ -161,7 +162,8 @@ let path_set_checkout_todo (wl : Worklist.t) (node: Procdesc.Node.t) : Paths.Pat Hashtbl.replace wl.Worklist.path_set_visited node_id new_visited; todo with Not_found -> - failwithf "could not find todo for node %a" Procdesc.Node.pp node + L.out "@.@.ERROR: could not find todo for node %a@.@." Procdesc.Node.pp node; + assert false (* =============== END of the edge_set object =============== *) diff --git a/infer/src/backend/match.ml b/infer/src/backend/match.ml index cf1d3cc90..865fe4f68 100644 --- a/infer/src/backend/match.ml +++ b/infer/src/backend/match.ml @@ -143,11 +143,10 @@ and isel_match isel1 sub vars isel2 = let sanity_check = not (List.exists ~f:(fun id -> Sil.ident_in_exp id idx2) vars) in if (not sanity_check) then begin let pe = Pp.text in - failwithf "@[.... Sanity Check Failure while Matching Index-Strexps ....@\n\ - @[<4> IDX1: %a, STREXP1: %a@\n\ - @[<4> IDX2: %a, STREXP2: %a@\n@." - (Sil.pp_exp_printenv pe) idx1 (Sil.pp_sexp pe) se1' - (Sil.pp_exp_printenv pe) idx2 (Sil.pp_sexp pe) se2' + L.out "@[.... Sanity Check Failure while Matching Index-Strexps ....@."; + L.out "@[<4> IDX1: %a, STREXP1: %a@." (Sil.pp_exp_printenv pe) idx1 (Sil.pp_sexp pe) se1'; + L.out "@[<4> IDX2: %a, STREXP2: %a@\n@." (Sil.pp_exp_printenv pe) idx2 (Sil.pp_sexp pe) se2'; + assert false end else if Exp.equal idx1 idx2 then begin match strexp_match se1' sub vars se2' with diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 098b1220c..28395f4a0 100644 --- a/infer/src/backend/prop.ml +++ b/infer/src/backend/prop.ml @@ -1356,7 +1356,8 @@ module Normalize = struct | Var _ -> Estruct ([], inst) | te -> - failwithf "trying to create ptsto with type: %a@\n@." (Sil.pp_texp_full Pp.text) te in + L.out "trying to create ptsto with type: %a@\n@." (Sil.pp_texp_full Pp.text) te; + assert false in let strexp : Sil.strexp = match expo with | Some e -> Eexp (e, inst) | None -> default_strexp () in @@ -2360,12 +2361,11 @@ let prop_iter_make_id_primed tenv id iter = begin match eq with | Aeq (Var id1, e1) when Sil.ident_in_exp id1 e1 -> - failwithf "@[<2>#### ERROR: an assumption of the analyzer broken ####@\n\ - Broken Assumption: id notin e for all (id,e) in sub@\n\ - (id,e) : (%a,%a)@\n\ - PROP : %a@\n@." - (Ident.pp Pp.text) id1 Exp.pp e1 - (pp_prop Pp.text) (prop_iter_to_prop tenv iter) + L.out "@[<2>#### ERROR: an assumption of the analyzer broken ####@\n"; + L.out "Broken Assumption: id notin e for all (id,e) in sub@\n"; + L.out "(id,e) : (%a,%a)@\n" (Ident.pp Pp.text) id1 Exp.pp e1; + L.out "PROP : %a@\n@." (pp_prop Pp.text) (prop_iter_to_prop tenv iter); + assert false | Aeq (Var id1, e1) when Ident.equal pid id1 -> split pairs_unpid ((id1, e1):: pairs_pid) eqs_cur | Aeq (Var id1, e1) -> diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml index 985682569..94495c39c 100644 --- a/infer/src/backend/symExec.ml +++ b/infer/src/backend/symExec.ml @@ -1235,7 +1235,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path | [], _ -> ret_old_path [prop_] | _ -> - failwithf "Pvar %a appears on the LHS of >1 heap predicate!@." (Pvar.pp Pp.text) pvar + L.out "Pvar %a appears on the LHS of >1 heap predicate!@." (Pvar.pp Pp.text) pvar; + assert false end | Sil.Abstract _ -> let node = State.get_node () in diff --git a/infer/src/base/DB.ml b/infer/src/base/DB.ml index b4fdfdb78..523ccf56e 100644 --- a/infer/src/base/DB.ml +++ b/infer/src/base/DB.ml @@ -164,7 +164,8 @@ let update_file_with_lock dir fname update = Unix.lockf fd ~mode:Unix.F_ULOCK ~len:0L; Unix.close fd ) else ( - failwithf "save_with_lock: fail on path: %s@." path + L.out "@.save_with_lock: fail on path: %s@." path; + assert false ) (** Read a file using a lock to allow write attempts in parallel. *) diff --git a/infer/src/base/Logging.ml b/infer/src/base/Logging.ml index b453d688f..b73a70e47 100644 --- a/infer/src/base/Logging.ml +++ b/infer/src/base/Logging.ml @@ -227,7 +227,7 @@ let assert_false ((file, lnum, cnum, _) as ml_loc) = raise (Assert_failure (file, lnum, cnum)) (** print a warning with information of the position in the ml source where it oririnated. - use as: warning_position "description" (try assert false with Assert_failure x -> x); *) + use as: warning_position "description" __POS__; *) let warning_position (s: string) (ml_loc: ml_loc) = out "WARNING: %s in %a@." s pp_ml_loc_opt (Some ml_loc) diff --git a/infer/src/base/Logging.mli b/infer/src/base/Logging.mli index 0956fe5d8..55de4d907 100644 --- a/infer/src/base/Logging.mli +++ b/infer/src/base/Logging.mli @@ -108,7 +108,7 @@ val pp_ml_loc_opt : Format.formatter -> ml_loc option -> unit val assert_false : ml_loc -> 'a (** print a warning with information of the position in the ml source where it oririnated. - use as: warning_position "description" (try assert false with Assert_failure x -> x); *) + use as: warning_position "description" __POS__; *) val warning_position: string -> ml_loc -> unit (** dump a string *) diff --git a/infer/src/clang/Capture.re b/infer/src/clang/Capture.re index ce2e799ed..52c7651ef 100644 --- a/infer/src/clang/Capture.re +++ b/infer/src/clang/Capture.re @@ -22,7 +22,8 @@ let catch_biniou_buffer_errors f x => /* suppress warning: allow this one case because we're just reraising the error with another error message so it doesn't really matter if this eventually fails */ | Invalid_argument "Bi_inbuf.refill_from_channel" => - failwith "WARNING: biniou buffer too short, skipping the file" + Logging.out "WARNING: biniou buffer too short, skipping the file@\n"; + assert false } ) [@warning "-52"]; diff --git a/infer/src/clang/cFrontend_errors.ml b/infer/src/clang/cFrontend_errors.ml index b3ed5f039..8547a2c96 100644 --- a/infer/src/clang/cFrontend_errors.ml +++ b/infer/src/clang/cFrontend_errors.ml @@ -82,7 +82,8 @@ let evaluate_place_holder ph an = | "%iphoneos_target_sdk_version%" -> MF.monospaced_to_string (CFrontend_checkers.iphoneos_target_sdk_version an) | "%available_ios_sdk%" -> MF.monospaced_to_string (CFrontend_checkers.available_ios_sdk an) - | _ -> failwithf "Helper function %s is unknown" ph + | _ -> (Logging.out "ERROR: helper function %s is unknown. Stop.\n" ph; + assert false) (* given a message this function searches for a place-holder identifier, eg %id%. Then it evaluates id and replaces %id% in message @@ -113,13 +114,16 @@ let string_to_err_kind = function | "ERROR" -> Exceptions.Kerror | "INFO" -> Exceptions.Kinfo | "ADVICE" -> Exceptions.Kadvice - | s -> failwithf "Severity %s does not exist" s + | s -> (Logging.out "\n[ERROR] Severity %s does not exist. Stop.\n" s; + assert false) let string_to_issue_mode m = match m with | "ON" -> CIssue.On | "OFF" -> CIssue.Off - | s -> failwithf "Mode %s does not exist. Please specify ON/OFF" s + | s -> + (Logging.out "\n[ERROR] Mode %s does not exist. Please specify ON/OFF\n" s; + assert false) (** Convert a parsed checker in list of linters *) let create_parsed_linters linters_def_file checkers : linter list = diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index aec4d4624..71cfef936 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -880,7 +880,8 @@ struct if Int.equal (List.length params) (List.length params_stmt) then params else - failwith "ERROR: stmt_list and res_trans_par.exps must have same size" in + (Logging.out "ERROR: stmt_list and res_trans_par.exps must have same size\n"; + assert false) in let act_params = if is_cf_retain_release then (Exp.Const (Const.Cint IntLit.one), Typ.mk (Tint Typ.IBool)) :: act_params else act_params in diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 637b5dd0e..9ae3abb05 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -572,7 +572,8 @@ let rec get_type_from_exp_stmt stmt = get_type_from_exp_stmt (extract_stmt_from_singleton stmt_list "WARNING: We expect only one stmt.") | DeclRefExpr(_, _, _, info) -> do_decl_ref_exp info | _ -> - failwithf "Cannot get type fo stmt %s" (Clang_ast_j.string_of_stmt stmt) + Logging.out "Failing with: %s@\n%!" (Clang_ast_j.string_of_stmt stmt); + assert false module Self = struct diff --git a/infer/src/harness/inhabit.ml b/infer/src/harness/inhabit.ml index fe007eeb7..8c803fbcd 100644 --- a/infer/src/harness/inhabit.ml +++ b/infer/src/harness/inhabit.ml @@ -142,7 +142,8 @@ let rec inhabit_typ tenv typ cfg env = | Typ.Tint (_) -> (Exp.Const (Const.Cint (IntLit.zero)), env) | Typ.Tfloat (_) -> (Exp.Const (Const.Cfloat 0.0), env) | _ -> - failwithf "Couldn't inhabit typ: %a" (Typ.pp Pp.text) typ in + L.out "Couldn't inhabit typ: %a@." (Typ.pp Pp.text) typ; + assert false in let (inhabited_exp, env') = inhabit_internal typ { env with cur_inhabiting = TypSet.add typ env.cur_inhabiting } in (inhabited_exp, { env' with cache = TypMap.add typ inhabited_exp env.cache;