@ -168,13 +168,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| _ ->
| _ ->
OwnershipAbstractValue . unowned
OwnershipAbstractValue . unowned
in
in
Some
Some { empty_summary with accesses = callee_accesses ; return_ownership }
{ locks = LocksDomain . empty
; threads = ThreadsDomain . empty
; accesses = callee_accesses
; return_ownership
; return_attributes = AttributeSetDomain . empty
; wobbly_paths = StabilityDomain . empty }
let get_summary caller_pdesc callee_pname actuals callee_loc tenv ( astate : Domain . astate ) =
let get_summary caller_pdesc callee_pname actuals callee_loc tenv ( astate : Domain . astate ) =
@ -620,15 +614,6 @@ end
module Analyzer = LowerHil . MakeAbstractInterpreter ( ProcCfg . Normal ) ( TransferFunctions )
module Analyzer = LowerHil . MakeAbstractInterpreter ( ProcCfg . Normal ) ( TransferFunctions )
let empty_post : RacerDDomain . summary =
{ threads = RacerDDomain . ThreadsDomain . empty
; locks = RacerDDomain . LocksDomain . empty
; accesses = RacerDDomain . AccessDomain . empty
; return_ownership = RacerDDomain . OwnershipAbstractValue . unowned
; return_attributes = RacerDDomain . AttributeSetDomain . empty
; wobbly_paths = RacerDDomain . StabilityDomain . empty }
let analyze_procedure { Callbacks . proc_desc ; tenv ; summary } =
let analyze_procedure { Callbacks . proc_desc ; tenv ; summary } =
let open RacerDModels in
let open RacerDModels in
let open ConcurrencyModels in
let open ConcurrencyModels in
@ -691,19 +676,17 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
else
else
(* express that the constructor owns [this] *)
(* express that the constructor owns [this] *)
let init = add_owned_formal own_locals 0 in
let init = add_owned_formal own_locals 0 in
List . fold ~ f : add_conditional_owned_formal ~ init
FormalMap . get_formals_indexes formal_map
( List . filter
| > List . filter ~ f : ( fun ( _ , index ) -> not ( Int . equal 0 index ) )
~ f : ( fun ( _ , index ) -> not ( Int . equal index 0 ) )
| > List . fold ~ init ~ f : add_conditional_owned_formal
( FormalMap . get_formals_indexes formal_map ) )
in
in
{ RacerDDomain . empty with ownership ; threads }
{ RacerDDomain . empty with ownership ; threads }
else
else
(* add Owned ( formal_index ) predicates for each formal to indicate that each one is owned if
(* add Owned ( formal_index ) predicates for each formal to indicate that each one is owned if
it is owned in the caller * )
it is owned in the caller * )
let ownership =
let ownership =
List . fold ~ f: add_conditional_owned_formal
List . fold ~ init: own_locals ~ f: add_conditional_owned_formal
( FormalMap . get_formals_indexes formal_map )
( FormalMap . get_formals_indexes formal_map )
~ init : own_locals
in
in
{ RacerDDomain . empty with ownership ; threads }
{ RacerDDomain . empty with ownership ; threads }
in
in
@ -723,7 +706,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
Payload . update_summary post summary
Payload . update_summary post summary
| None ->
| None ->
summary
summary
else Payload . update_summary empty_ post summary
else Payload . update_summary empty_ summary summary
type conflict = RacerDDomain . TraceElem . t
type conflict = RacerDDomain . TraceElem . t
@ -1090,6 +1073,34 @@ end = struct
M . fold f map a
M . fold f map a
end
end
let should_report_on_proc procdesc tenv =
let proc_name = Procdesc . get_proc_name procdesc in
match proc_name with
| Java java_pname ->
(* return true if procedure is at an abstraction boundary or reporting has been explicitly
requested via @ ThreadSafe in java * )
RacerDModels . is_thread_safe_method proc_name tenv
| | Procdesc . get_access procdesc < > PredSymb . Private
&& ( not ( Typ . Procname . Java . is_autogen_method java_pname ) )
&& not ( Annotations . pdesc_return_annot_ends_with procdesc Annotations . visibleForTesting )
| ObjC_Cpp objc_cpp_pname ->
( match objc_cpp_pname . Typ . Procname . ObjC_Cpp . kind with
| CPPMethod _ | CPPConstructor _ | CPPDestructor _ ->
Procdesc . get_access procdesc < > PredSymb . Private
| ObjCClassMethod | ObjCInstanceMethod | ObjCInternalMethod ->
(* ObjC has no private methods, just a convention that they start with an underscore *)
not ( String . is_prefix objc_cpp_pname . Typ . Procname . ObjC_Cpp . method_name ~ prefix : " _ " ) )
&&
let matcher = ConcurrencyModels . cpp_lock_types_matcher in
Option . exists ( Tenv . lookup tenv objc_cpp_pname . class_name ) ~ f : ( fun class_str ->
(* check if the class contains a lock member *)
List . exists class_str . Typ . Struct . fields ~ f : ( fun ( _ , ft , _ ) ->
Option . exists ( Typ . name ft ) ~ f : ( fun name ->
QualifiedCppName . Match . match_qualifiers matcher ( Typ . Name . qual_name name ) ) ) )
| _ ->
false
(* * Report accesses that may race with each other.
(* * Report accesses that may race with each other.
Principles for race reporting .
Principles for race reporting .
@ -1203,7 +1214,7 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) =
(* Do not report unprotected writes when an access can't run in parallel with itself, or
(* Do not report unprotected writes when an access can't run in parallel with itself, or
for ObjC_Cpp * )
for ObjC_Cpp * )
reported_acc )
reported_acc )
| ( Access . Read _ | ContainerRead _ ) when AccessSnapshot . is_unprotected snapshot -> (
| ( Access . Read _ | ContainerRead _ ) when AccessSnapshot . is_unprotected snapshot ->
(* unprotected read. report all writes as conflicts for java. for c++ filter out
(* unprotected read. report all writes as conflicts for java. for c++ filter out
unprotected writes * )
unprotected writes * )
let is_conflict { snapshot ; threads = other_threads } =
let is_conflict { snapshot ; threads = other_threads } =
@ -1213,15 +1224,15 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) =
ThreadsDomain . is_any threads | | ThreadsDomain . is_any other_threads
ThreadsDomain . is_any threads | | ThreadsDomain . is_any other_threads
else not ( AccessSnapshot . is_unprotected snapshot )
else not ( AccessSnapshot . is_unprotected snapshot )
in
in
match List . find ~ f : is_conflict accesses with
List . find ~ f : is_conflict accesses
| None ->
| > Option . value_map ~ default : reported_acc ~ f : ( fun conflict ->
reported_acc
let make_description =
| Some conflict ->
make_read_write_race_description ~ read_is_sync : false conflict
report_thread_safety_violation tenv procdesc
in
~ make_description : ( make_read_write_race_description ~ read_is_sync : false conflict )
let report_kind = ReadWriteRace conflict . snapshot . access in
~ report_kind : ( ReadWriteRace conflict . snapshot . access ) snapshot . access threads
report_thread_safety_violation tenv procdesc ~ make_description ~ report_kind
wobbly_paths ;
snapshot . access threads wobbly_paths ;
update_reported snapshot . access pname reported_acc )
update_reported snapshot . access pname reported_acc )
| Access . Read _ | ContainerRead _ ->
| Access . Read _ | ContainerRead _ ->
(* protected read. report unprotected writes and opposite protected writes as conflicts *)
(* protected read. report unprotected writes and opposite protected writes as conflicts *)
let can_conflict ( snapshot1 : AccessSnapshot . t ) ( snapshot2 : AccessSnapshot . t ) =
let can_conflict ( snapshot1 : AccessSnapshot . t ) ( snapshot2 : AccessSnapshot . t ) =
@ -1257,14 +1268,7 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) =
let should_report { tenv ; procdesc } =
let should_report { tenv ; procdesc } =
List . exists grouped_accesses ~ f : ( fun ( { threads } : reported_access ) ->
List . exists grouped_accesses ~ f : ( fun ( { threads } : reported_access ) ->
ThreadsDomain . is_any threads )
ThreadsDomain . is_any threads )
&&
&& should_report_on_proc procdesc tenv
match Procdesc . get_proc_name procdesc with
| Java _ ->
should_report_in_java procdesc tenv
| ObjC_Cpp objc_cpp ->
should_report_in_objcpp procdesc objc_cpp tenv
| _ ->
false
in
in
let reportable_accesses = List . filter ~ f : should_report grouped_accesses in
let reportable_accesses = List . filter ~ f : should_report grouped_accesses in
List . fold reportable_accesses ~ init : reported ~ f : ( report_unsafe_access reportable_accesses )
List . fold reportable_accesses ~ init : reported ~ f : ( report_unsafe_access reportable_accesses )
@ -1278,39 +1282,30 @@ let report_unsafe_accesses (aggregated_access_map : ReportMap.t) =
that x . f . g may point to during execution * )
that x . f . g may point to during execution * )
let make_results_table file_env =
let make_results_table file_env =
let open RacerDDomain in
let open RacerDDomain in
let aggregate_post tenv procdesc acc { threads ; accesses ; wobbly_paths } =
let aggregate_post acc ( { threads ; accesses ; wobbly_paths } , tenv , procdesc ) =
AccessDomain . fold
AccessDomain . fold
( fun snapshot acc -> ReportMap . add { threads ; snapshot ; tenv ; procdesc ; wobbly_paths } acc )
( fun snapshot acc -> ReportMap . add { threads ; snapshot ; tenv ; procdesc ; wobbly_paths } acc )
accesses acc
accesses acc
in
in
let aggregate_posts acc ( tenv , proc_desc ) =
List . filter_map file_env ~ f : ( fun ( tenv , proc_desc ) ->
Payload . read proc_desc ( Procdesc . get_proc_name proc_desc )
Procdesc . get_proc_name proc_desc | > Payload . read proc_desc
| > Option . fold ~ init : acc ~ f : ( aggregate_post tenv proc_desc )
| > Option . map ~ f : ( fun payload -> ( payload , tenv , proc_desc ) ) )
in
| > List . fold ~ init : ReportMap . empty ~ f : aggregate_post
List . fold file_env ~ init : ReportMap . empty ~ f : aggregate_posts
(* aggregate all of the procedures in the file env by their declaring
(* aggregate all of the procedures in the file env by their declaring
class . this lets us analyze each class individually * )
class . this lets us analyze each class individually * )
let aggregate_by_class file_env =
let aggregate_by_class file_env =
List . fold file_env ~ init : String . Map . empty ~ f : ( fun acc ( ( _ , pdesc ) as proc ) ->
List . fold file_env ~ init : String . Map . empty ~ f : ( fun acc ( ( _ , pdesc ) as proc ) ->
let classname =
Procdesc . get_proc_name pdesc | > Typ . Procname . get_class_name
match Procdesc . get_proc_name pdesc with
| > Option . fold ~ init : acc ~ f : ( fun acc classname ->
| Typ . Procname . Java java_pname ->
String . Map . add_multi acc ~ key : classname ~ data : proc ) )
Some ( Typ . Procname . Java . get_class_name java_pname )
| ObjC_Cpp objc_cpp_pname ->
Some ( Typ . Procname . ObjC_Cpp . get_class_name objc_cpp_pname )
| _ ->
None
in
Option . fold classname ~ init : acc ~ f : ( fun acc classname ->
String . Map . add_multi acc ~ key : classname ~ data : proc ) )
(* Gathers results by analyzing all the methods in a file, then
(* Gathers results by analyzing all the methods in a file, then
post - processes the results to check an ( approximation of ) thread
post - processes the results to check an ( approximation of ) thread
safety * )
safety * )
let file_analysis { Callbacks . procedures ; source_file } =
let file_analysis { Callbacks . procedures ; source_file } =
String . Map . iter ( aggregate_by_class procedures ) ~ f : ( fun class_env ->
aggregate_by_class procedures
report_unsafe_accesses ( make_results_table class_env ) ) ;
| > String . Map . iter ~ f : ( fun class_env -> report_unsafe_accesses ( make_results_table class_env ) ) ;
IssueLog . store Config . racerd_issues_dir_name source_file
IssueLog . store Config . racerd_issues_dir_name source_file