[deadlock] rebrand to starvation

Reviewed By: sblackshear

Differential Revision: D7415034

fbshipit-source-id: a9789eb
master
Nikos Gorogiannis 7 years ago committed by Facebook Github Bot
parent 05ce219962
commit b335fb9c50

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

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

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

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

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

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

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

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

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

@ -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*]

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

@ -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*]
Loading…
Cancel
Save