diff --git a/Makefile b/Makefile index 7501cc862..35307e3ad 100644 --- a/Makefile +++ b/Makefile @@ -89,7 +89,7 @@ BUILD_SYSTEMS_TESTS += \ DIRECT_TESTS += \ java_checkers java_eradicate java_infer java_lab java_tracing java_quandary \ - java_racerd java_stability java_crashcontext java_deadlock + java_racerd java_stability java_crashcontext java_starvation ifneq ($(ANT),no) BUILD_SYSTEMS_TESTS += ant endif diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index 1bd569203..9160b9858 100644 --- a/infer/src/backend/specs.ml +++ b/infer/src/backend/specs.ml @@ -280,7 +280,7 @@ type payload = ; typestate: unit TypeState.t option ; uninit: UninitDomain.summary option ; cost: CostDomain.summary option - ; deadlock: DeadlockDomain.summary option } + ; starvation: StarvationDomain.summary option } type summary = { phase: phase (** in FOOTPRINT phase or in RE_EXECUTION PHASE *) @@ -424,7 +424,7 @@ let pp_payload pe fmt ; annot_map ; uninit ; cost - ; deadlock } = + ; starvation } = let pp_opt prefix pp fmt = function | Some x -> F.fprintf fmt "%s: %a@\n" prefix pp x @@ -450,8 +450,8 @@ let pp_payload pe fmt uninit (pp_opt "Cost" CostDomain.pp_summary) cost - (pp_opt "Deadlock" DeadlockDomain.pp_summary) - deadlock + (pp_opt "Starvation" StarvationDomain.pp_summary) + starvation let pp_summary_text fmt summary = @@ -632,7 +632,7 @@ let empty_payload = ; buffer_overrun= None ; uninit= None ; cost= None - ; deadlock= None } + ; starvation= None } (** [init_summary (depend_list, nodes, diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 0d00fa516..ae5a1c5df 100644 --- a/infer/src/backend/specs.mli +++ b/infer/src/backend/specs.mli @@ -106,7 +106,7 @@ type payload = ; typestate: unit TypeState.t option ; uninit: UninitDomain.summary option ; cost: CostDomain.summary option - ; deadlock: DeadlockDomain.summary option } + ; starvation: StarvationDomain.summary option } (** Procedure summary *) type summary = diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 48bfe7262..b6ee29b3d 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -678,7 +678,6 @@ and ( annotation_reachability , check_nullable , cost , crashcontext - , deadlock , eradicate , fragment_retains_view , immutable_cast @@ -691,6 +690,7 @@ and ( annotation_reachability , racerd , resource_leak , siof + , starvation , suggest_nullable , uninit ) = let mk_checker ?(default= false) ?(deprecated= []) ~long doc = @@ -719,7 +719,6 @@ and ( annotation_reachability and crashcontext = mk_checker ~long:"crashcontext" "the crashcontext checker for Java stack trace context reconstruction" - and deadlock = mk_checker ~long:"deadlock" ~default:false "deadlock analysis" and eradicate = mk_checker ~long:"eradicate" "the eradicate @Nullable checker for Java annotations" and fragment_retains_view = @@ -747,6 +746,7 @@ and ( annotation_reachability and siof = mk_checker ~long:"siof" ~default:true "the Static Initialization Order Fiasco analysis (C++ only)" + and starvation = mk_checker ~long:"starvation" ~default:false "starvation analysis" and suggest_nullable = mk_checker ~long:"suggest-nullable" ~default:false "Nullable annotation sugesstions analysis" and uninit = mk_checker ~long:"uninit" "checker for use of uninitialized values" in @@ -792,7 +792,6 @@ and ( annotation_reachability , check_nullable , cost , crashcontext - , deadlock , eradicate , fragment_retains_view , immutable_cast @@ -805,6 +804,7 @@ and ( annotation_reachability , racerd , resource_leak , siof + , starvation , suggest_nullable , uninit ) @@ -2393,8 +2393,6 @@ and cxx_infer_headers = !cxx_infer_headers and cxx_scope_guards = !cxx_scope_guards -and deadlock = !deadlock - and debug_level_analysis = !debug_level_analysis and debug_level_capture = !debug_level_capture @@ -2691,6 +2689,8 @@ and stacktrace = !stacktrace and stacktraces_dir = !stacktraces_dir +and starvation = !starvation + and stats_report = !stats_report and subtype_multirange = !subtype_multirange diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 269cf669e..71a43b9b7 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -314,8 +314,6 @@ val cxx_infer_headers : bool val cxx_scope_guards : Yojson.Basic.json -val deadlock : bool - val debug_level_analysis : int val debug_level_capture : int @@ -596,6 +594,8 @@ val stacktrace : string option val stacktraces_dir : string option +val starvation : bool + val stats_report : string option val subtype_multirange : bool diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 01d3d76ff..4d18ac827 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -281,8 +281,6 @@ let parameter_not_null_checked = from_string "PARAMETER_NOT_NULL_CHECKED" let pointer_size_mismatch = from_string "POINTER_SIZE_MISMATCH" -let potential_deadlock = from_string "DEADLOCK" - let precondition_not_found = from_string "PRECONDITION_NOT_FOUND" let precondition_not_met = from_string "PRECONDITION_NOT_MET" @@ -317,6 +315,8 @@ let sql_injection_risk = from_string "SQL_INJECTION_RISK" let stack_variable_address_escape = from_string ~enabled:false "STACK_VARIABLE_ADDRESS_ESCAPE" +let starvation = from_string "STARVATION" + let static_initialization_order_fiasco = from_string "STATIC_INITIALIZATION_ORDER_FIASCO" let symexec_memory_error = diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 3265887a8..736332333 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -198,8 +198,6 @@ val parameter_not_null_checked : t val pointer_size_mismatch : t -val potential_deadlock : t [@@warning "-32"] - val precondition_not_found : t val precondition_not_met : t @@ -234,6 +232,8 @@ val sql_injection_risk : t val stack_variable_address_escape : t +val starvation : t + val static_initialization_order_fiasco : t val symexec_memory_error : t diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 297d574f9..b7a85af3d 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/infer/src/checkers/registerCheckers.ml @@ -103,9 +103,9 @@ let all_checkers = ; active= Config.cost ; callbacks= [(Procedure Cost.checker, Language.Clang); (Procedure Cost.checker, Language.Java)] } - ; { name= "Deadlock analysis" - ; active= Config.deadlock - ; callbacks= [(Procedure Deadlock.analyze_procedure, Language.Java)] } ] + ; { name= "Starvation analysis" + ; active= Config.starvation + ; callbacks= [(Procedure Starvation.analyze_procedure, Language.Java)] } ] let get_active_checkers () = diff --git a/infer/src/concurrency/deadlock.ml b/infer/src/concurrency/starvation.ml similarity index 90% rename from infer/src/concurrency/deadlock.ml rename to infer/src/concurrency/starvation.ml index 8fe559e4b..8360954b9 100644 --- a/infer/src/concurrency/deadlock.ml +++ b/infer/src/concurrency/starvation.ml @@ -14,18 +14,18 @@ module MF = MarkupFormatter let debug fmt = F.kasprintf L.d_strln fmt module Summary = Summary.Make (struct - type payload = DeadlockDomain.summary + type payload = StarvationDomain.summary let update_payload post (summary: Specs.summary) = - {summary with payload= {summary.payload with deadlock= Some post}} + {summary with payload= {summary.payload with starvation= Some post}} - let read_payload (summary: Specs.summary) = summary.payload.deadlock + let read_payload (summary: Specs.summary) = summary.payload.starvation end) module TransferFunctions (CFG : ProcCfg.S) = struct module CFG = CFG - module Domain = DeadlockDomain + module Domain = StarvationDomain type extras = ProcData.no_extras @@ -77,7 +77,7 @@ let get_class_of_pname = function let should_report_if_same_class _ = true (* currently short-circuited until non-determinism in reporting is dealt with *) -(* DeadlockDomain.( +(* StarvationDomain.( LockOrder.get_pair caller_elem |> false_if_none ~f:(fun (b, a) -> let b_class_opt, a_class_opt = (LockEvent.owner_class b, LockEvent.owner_class a) in @@ -87,7 +87,7 @@ let should_report_if_same_class _ = true ) ) )) *) let make_loc_trace pname trace_id start_loc elem = - let open DeadlockDomain in + let open StarvationDomain in let header = Printf.sprintf "[Trace %d]" trace_id in let trace = LockOrder.make_loc_trace elem in let first_step = List.hd_exn trace in @@ -105,7 +105,7 @@ let get_summary caller_pdesc callee_pdesc = let report_deadlocks get_proc_desc tenv pdesc summary = - let open DeadlockDomain in + let open StarvationDomain in let process_callee_elem caller_pdesc caller_elem callee_pdesc elem = if LockOrder.may_deadlock caller_elem elem && should_report_if_same_class caller_elem then ( debug "Possible deadlock:@.%a@.%a@." LockOrder.pp caller_elem LockOrder.pp elem ; @@ -119,9 +119,7 @@ let report_deadlocks get_proc_desc tenv pdesc summary = let error_message = Format.asprintf "Potential deadlock (%a ; %a)" LockIdentity.pp lock LockIdentity.pp lock' in - let exn = - Exceptions.Checkers (IssueType.potential_deadlock, Localise.verbatim_desc error_message) - in + let exn = Exceptions.Checkers (IssueType.starvation, Localise.verbatim_desc error_message) in let first_trace = List.rev (make_loc_trace caller_pname 1 caller_loc caller_elem) in let second_trace = make_loc_trace callee_pname 2 callee_loc elem in let ltr = List.rev_append first_trace second_trace in @@ -158,21 +156,21 @@ let report_deadlocks get_proc_desc tenv pdesc summary = let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} = let proc_data = ProcData.make_default proc_desc tenv in let initial = - if not (Procdesc.is_java_synchronized proc_desc) then DeadlockDomain.empty + if not (Procdesc.is_java_synchronized proc_desc) then StarvationDomain.empty else let attrs = Procdesc.get_attributes proc_desc in List.hd attrs.ProcAttributes.formals - |> Option.value_map ~default:DeadlockDomain.empty ~f:(fun (name, typ) -> + |> Option.value_map ~default:StarvationDomain.empty ~f:(fun (name, typ) -> let pvar = Pvar.mk name (Procdesc.get_proc_name proc_desc) in let path = (AccessPath.base_of_pvar pvar typ, []) in - DeadlockDomain.acquire path DeadlockDomain.empty (Procdesc.get_loc proc_desc) ) + StarvationDomain.acquire path StarvationDomain.empty (Procdesc.get_loc proc_desc) ) in match Analyzer.compute_post proc_data ~initial with | None -> summary | Some lock_state -> - let lock_order = DeadlockDomain.to_summary lock_state in + let lock_order = StarvationDomain.to_summary lock_state in let updated_summary = Summary.update_summary lock_order summary in - Option.iter updated_summary.Specs.payload.deadlock + Option.iter updated_summary.Specs.payload.starvation ~f:(report_deadlocks get_proc_desc tenv proc_desc) ; updated_summary diff --git a/infer/src/concurrency/deadlock.mli b/infer/src/concurrency/starvation.mli similarity index 100% rename from infer/src/concurrency/deadlock.mli rename to infer/src/concurrency/starvation.mli diff --git a/infer/src/concurrency/deadlockDomain.ml b/infer/src/concurrency/starvationDomain.ml similarity index 100% rename from infer/src/concurrency/deadlockDomain.ml rename to infer/src/concurrency/starvationDomain.ml diff --git a/infer/src/concurrency/deadlockDomain.mli b/infer/src/concurrency/starvationDomain.mli similarity index 100% rename from infer/src/concurrency/deadlockDomain.mli rename to infer/src/concurrency/starvationDomain.mli diff --git a/infer/tests/codetoanalyze/java/deadlock/issues.exp b/infer/tests/codetoanalyze/java/deadlock/issues.exp deleted file mode 100644 index 5c59b64c2..000000000 --- a/infer/tests/codetoanalyze/java/deadlock/issues.exp +++ /dev/null @@ -1,3 +0,0 @@ -codetoanalyze/java/deadlock/Interclass.java, void Interclass.interclass1_bad(InterclassA), 0, DEADLOCK, ERROR, [[Trace 1] Lock acquisition: locks this in class Interclass*,Method call: void InterclassA.interclass1_bad(),Lock acquisition: locks this in class InterclassA*,[Trace 2] Lock acquisition: locks this in class InterclassA*,Method call: void Interclass.interclass2_bad(),Lock acquisition: locks this in class Interclass*] -codetoanalyze/java/deadlock/Interproc.java, void Interproc.interproc1_bad(InterprocA), 0, DEADLOCK, ERROR, [[Trace 1] Lock acquisition: locks this in class Interproc*,Method call: void Interproc.interproc2_bad(InterprocA),Lock acquisition: locks b in class InterprocA*,[Trace 2] Lock acquisition: locks this in class InterprocA*,Method call: void InterprocA.interproc2_bad(Interproc),Lock acquisition: locks d in class Interproc*] -codetoanalyze/java/deadlock/Intraproc.java, void IntraprocA.intra_bad(Intraproc), 0, DEADLOCK, ERROR, [[Trace 1] Method start: void IntraprocA.intra_bad(Intraproc),Lock acquisition: locks this in class IntraprocA*,Lock acquisition: locks o in class Intraproc*,[Trace 2] Method start: void Intraproc.intra_bad(IntraprocA),Lock acquisition: locks this in class Intraproc*,Lock acquisition: locks o in class IntraprocA*] diff --git a/infer/tests/codetoanalyze/java/deadlock/Interclass.java b/infer/tests/codetoanalyze/java/starvation/Interclass.java similarity index 100% rename from infer/tests/codetoanalyze/java/deadlock/Interclass.java rename to infer/tests/codetoanalyze/java/starvation/Interclass.java diff --git a/infer/tests/codetoanalyze/java/deadlock/Interproc.java b/infer/tests/codetoanalyze/java/starvation/Interproc.java similarity index 100% rename from infer/tests/codetoanalyze/java/deadlock/Interproc.java rename to infer/tests/codetoanalyze/java/starvation/Interproc.java diff --git a/infer/tests/codetoanalyze/java/deadlock/Intraproc.java b/infer/tests/codetoanalyze/java/starvation/Intraproc.java similarity index 100% rename from infer/tests/codetoanalyze/java/deadlock/Intraproc.java rename to infer/tests/codetoanalyze/java/starvation/Intraproc.java diff --git a/infer/tests/codetoanalyze/java/deadlock/Makefile b/infer/tests/codetoanalyze/java/starvation/Makefile similarity index 89% rename from infer/tests/codetoanalyze/java/deadlock/Makefile rename to infer/tests/codetoanalyze/java/starvation/Makefile index 95a78029c..4af17a0e5 100644 --- a/infer/tests/codetoanalyze/java/deadlock/Makefile +++ b/infer/tests/codetoanalyze/java/starvation/Makefile @@ -8,7 +8,7 @@ TESTS_DIR = ../../.. ANALYZER = checkers -INFER_OPTIONS = --deadlock-only --debug-exceptions +INFER_OPTIONS = --starvation-only --debug-exceptions INFERPRINT_OPTIONS = --issues-tests SOURCES = $(wildcard *.java) diff --git a/infer/tests/codetoanalyze/java/starvation/issues.exp b/infer/tests/codetoanalyze/java/starvation/issues.exp new file mode 100644 index 000000000..0603f66fe --- /dev/null +++ b/infer/tests/codetoanalyze/java/starvation/issues.exp @@ -0,0 +1,3 @@ +codetoanalyze/java/starvation/Interclass.java, void Interclass.interclass1_bad(InterclassA), 0, STARVATION, ERROR, [[Trace 1] Lock acquisition: locks this in class Interclass*,Method call: void InterclassA.interclass1_bad(),Lock acquisition: locks this in class InterclassA*,[Trace 2] Lock acquisition: locks this in class InterclassA*,Method call: void Interclass.interclass2_bad(),Lock acquisition: locks this in class Interclass*] +codetoanalyze/java/starvation/Interproc.java, void Interproc.interproc1_bad(InterprocA), 0, STARVATION, ERROR, [[Trace 1] Lock acquisition: locks this in class Interproc*,Method call: void Interproc.interproc2_bad(InterprocA),Lock acquisition: locks b in class InterprocA*,[Trace 2] Lock acquisition: locks this in class InterprocA*,Method call: void InterprocA.interproc2_bad(Interproc),Lock acquisition: locks d in class Interproc*] +codetoanalyze/java/starvation/Intraproc.java, void IntraprocA.intra_bad(Intraproc), 0, STARVATION, ERROR, [[Trace 1] Method start: void IntraprocA.intra_bad(Intraproc),Lock acquisition: locks this in class IntraprocA*,Lock acquisition: locks o in class Intraproc*,[Trace 2] Method start: void Intraproc.intra_bad(IntraprocA),Lock acquisition: locks this in class Intraproc*,Lock acquisition: locks o in class IntraprocA*]