infer_clone/infer/src/checkers/SiofDomain.ml

(*
 * 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.
 *)

open! IStd

(* 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 AbstractDomain.BottomLifted(SiofTrace)
[SIOF] detect which variables need initialization Summary: - do a semantic analysis of each variable initializer to figure out if they need initialization - add a flag to globals that is true when they are `constexpr`. In that case, no analysis is needed as the user + compile guarantee that it is a compile-time constant. Reviewed By: sblackshear Differential Revision: D4081273 fbshipit-source-id: 44dbe29 8 years ago			`(*`
			`* 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.`
			`*)`

Open Core.Std by default, still use Caml Hashtbl, Map, Set Reviewed By: cristianoc Differential Revision: D4232458 fbshipit-source-id: 3d73c69 8 years ago			`open! IStd`

[SIOF] detect which variables need initialization Summary: - do a semantic analysis of each variable initializer to figure out if they need initialization - add a flag to globals that is true when they are `constexpr`. In that case, no analysis is needed as the user + compile guarantee that it is a compile-time constant. Reviewed By: sblackshear Differential Revision: D4081273 fbshipit-source-id: 44dbe29 8 years ago			`(* 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. *)`
[siof] convert domain to sink trace of pvar's Summary: The Quandary-style traces are too general for checkers like SIOF. This diff adds a "suffix abstraction" of the trace for analyses that just care about sinks. To show how to use it, we add it to SIOF. Note: this diff converts the domain, but isn't actually doing the fancier reporting yet. That will come in a future diff. Reviewed By: jvillard Differential Revision: D4124881 fbshipit-source-id: 5b9fd07 8 years ago			`include AbstractDomain.BottomLifted(SiofTrace)`