Summary: Change the domain of SIOF to be based on sets of pvar * location instead of single pvars. This allows us to group several accesses together. However, we still get different trace elems for different instructions in a proc. We do two things to get around this limitation and get a trace where all accesses within the same proc are grouped together, instead of one trace for each access: 1. A post-processing phase at the end of the analysis of one proc collects all the globals directly accessed in the proc into a single trace elem. 2. When creating the error trace, unpack this set into several trace elements to see each access (at its correct location) separately in the trace. This is a bit hacky and another way would be to extend the API of traces to handle in-procedure accesses natively instead of shoe-horning them. However since SIOF is the only one to use this, it introduces less boilerplate to do it that way for now. Also, a few .mlis for good measure. Reviewed By: sblackshear Differential Revision: D4299070 fbshipit-source-id: 3bbb5c2master
Jules Villard
8 years ago
committed by
Facebook Github Bot
parent
a9d5b5afdb
commit
c51c4a21ae
@ -0,0 +1,23 @@
|
|||||||
|
(*
|
||||||
|
* Copyright (c) 2016 - present Facebook, Inc.
|
||||||
|
* All rights reserved.
|
||||||
|
*
|
||||||
|
* This source code is licensed under the BSD style license found in the
|
||||||
|
* LICENSE file in the root directory of this source tree. An additional grant
|
||||||
|
* of patent rights can be found in the PATENTS file in the same directory.
|
||||||
|
*)
|
||||||
|
|
||||||
|
(* The domain for the analysis is sets of global variables if an initialization is needed at
|
||||||
|
runtime, or Bottom if no initialization is needed. For instance, `int x = 32; int y = x * 52;`
|
||||||
|
gives a summary of Bottom for both initializers corresponding to these globals, but `int x =
|
||||||
|
foo();` gives a summary of at least "NonBottom {}" for x's initializer since x will need runtime
|
||||||
|
initialization.
|
||||||
|
|
||||||
|
The encoding in terms of a BottomLifted domain is an efficiency hack to represent two pieces of
|
||||||
|
information: whether a global variable (via its initializer function) requires runtime
|
||||||
|
initialization, and which globals requiring initialization a given function (transitively)
|
||||||
|
accesses. *)
|
||||||
|
include module type of (AbstractDomain.BottomLifted(SiofTrace))
|
||||||
|
|
||||||
|
(** group together procedure-local accesses *)
|
||||||
|
val normalize : astate -> astate
|
||||||
@ -0,0 +1,33 @@
|
|||||||
|
(*
|
||||||
|
* Copyright (c) 2016 - present Facebook, Inc.
|
||||||
|
* All rights reserved.
|
||||||
|
*
|
||||||
|
* This source code is licensed under the BSD style license found in the
|
||||||
|
* LICENSE file in the root directory of this source tree. An additional grant
|
||||||
|
* of patent rights can be found in the PATENTS file in the same directory.
|
||||||
|
*)
|
||||||
|
|
||||||
|
module type Helper = sig
|
||||||
|
type summary
|
||||||
|
|
||||||
|
(** update the specs payload with [summary] *)
|
||||||
|
val update_payload : summary -> Specs.payload -> Specs.payload
|
||||||
|
|
||||||
|
(** extract [summmary] from the specs payload *)
|
||||||
|
val read_from_payload : Specs.payload -> summary option
|
||||||
|
end
|
||||||
|
|
||||||
|
module type S = sig
|
||||||
|
type summary
|
||||||
|
|
||||||
|
(** Write the [summary] for the procname to persistent storage. Returns the summary actually
|
||||||
|
written. *)
|
||||||
|
val write_summary : Procname.t -> summary -> unit
|
||||||
|
|
||||||
|
(** read and return the summary for [callee_pname] called from [caller_pdesc]. does the analysis
|
||||||
|
to create the summary if needed *)
|
||||||
|
val read_summary : Procdesc.t -> Procname.t -> summary option
|
||||||
|
|
||||||
|
end
|
||||||
|
|
||||||
|
module Make (H : Helper) : S with type summary = H.summary
|
||||||
@ -1,9 +1,9 @@
|
|||||||
codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_X::static_pod_accesses_non_pod, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of X::static_pod_accesses_non_pod,call to access_to_non_pod,access to global_object2]
|
codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_X::static_pod_accesses_non_pod, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of X::static_pod_accesses_non_pod,call to access_to_non_pod,access to global_object2,access to some_other_global_object2]
|
||||||
codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_another_global_object, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_global_object,call to SomeOtherNonPODObject_SomeOtherNonPODObject,access to extern_global_object]
|
codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_another_global_object, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_global_object,call to SomeOtherNonPODObject_SomeOtherNonPODObject,access to extern_global_object]
|
||||||
codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_another_global_object2, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_global_object2,call to access_to_non_pod,access to global_object2]
|
codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_another_global_object2, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_global_object2,call to access_to_non_pod,access to global_object2,access to some_other_global_object2]
|
||||||
codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_another_global_object3, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_global_object3,call to access_to_templated_non_pod,access to global_object3]
|
codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_another_global_object3, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_global_object3,call to access_to_templated_non_pod,access to global_object3]
|
||||||
codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_initWithGlobal, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of initWithGlobal,call to getGlobalNonPOD,access to global_object2]
|
codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_initWithGlobal, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of initWithGlobal,call to getGlobalNonPOD,access to some_other_global_object2,access to global_object2]
|
||||||
codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_pod_accesses_non_pod, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of pod_accesses_non_pod,call to access_to_non_pod,access to global_object2]
|
codetoanalyze/cpp/checkers/siof/siof.cpp, __infer_globals_initializer_pod_accesses_non_pod, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of pod_accesses_non_pod,call to access_to_non_pod,access to global_object2,access to some_other_global_object2]
|
||||||
codetoanalyze/cpp/checkers/siof/siof_templated.cpp, __infer_globals_initializer_another_templated_global_object, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_templated_global_object,call to SomeOtherTemplatedNonPODObject<_Bool>_SomeOtherTemplatedNonPODObject,access to extern_global_object]
|
codetoanalyze/cpp/checkers/siof/siof_templated.cpp, __infer_globals_initializer_another_templated_global_object, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_templated_global_object,call to SomeOtherTemplatedNonPODObject<_Bool>_SomeOtherTemplatedNonPODObject,access to extern_global_object]
|
||||||
codetoanalyze/cpp/checkers/siof/siof_templated.cpp, __infer_globals_initializer_another_templated_global_object2, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_templated_global_object2,call to access_to_non_pod,access to global_object2]
|
codetoanalyze/cpp/checkers/siof/siof_templated.cpp, __infer_globals_initializer_another_templated_global_object2, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_templated_global_object2,call to access_to_non_pod,access to global_object2,access to some_other_global_object2]
|
||||||
codetoanalyze/cpp/checkers/siof/siof_templated.cpp, __infer_globals_initializer_another_templated_global_object3, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_templated_global_object3,call to access_to_templated_non_pod,access to global_object3]
|
codetoanalyze/cpp/checkers/siof/siof_templated.cpp, __infer_globals_initializer_another_templated_global_object3, 0, STATIC_INITIALIZATION_ORDER_FIASCO, [initialization of another_templated_global_object3,call to access_to_templated_non_pod,access to global_object3]
|
||||||
|
|||||||
Loading…
Reference in new issue