infer_clone/infer/src/quandary/QuandarySummary.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.
 *)

(** summary type for Quandary taint analysis *)

open! IStd

module F = Format
module L = Logging

module Java = AccessTree.Make(JavaTrace)
module Cpp = AccessTree.Make(CppTrace)

module AccessTree = struct
  type t =
    | Java of Java.t
    | Cpp of Cpp.t

  let pp fmt = function
    | Java access_tree -> Java.pp fmt access_tree
    | Cpp access_tree -> Cpp.pp fmt access_tree
end

type t = AccessTree.t

let pp = AccessTree.pp
[quandary] format for summaries Reviewed By: mbouaziz Differential Revision: D3838520 fbshipit-source-id: 7cd8bcb 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.`
			`*)`

			`(** summary type for Quandary taint analysis *)`

Divide Utils into Utils, Pp, and IStd Summary: Utils contains definitions intended to be in the global namespace for all of the infer code-base, as well as pretty-printing functions, and assorted utility functions mostly for dealing with files and processes. This diff changes the module opened into the global namespace to IStd (Std conflict with extlib), and moves the pretty-printing definitions from Utils to Pp. Reviewed By: jvillard Differential Revision: D4232457 fbshipit-source-id: 1e070e0 8 years ago			`open! IStd`
[quandary] format for summaries Reviewed By: mbouaziz Differential Revision: D3838520 fbshipit-source-id: 7cd8bcb 8 years ago
			`module F = Format`
			`module L = Logging`

[quandary] summaries are access trees too Summary: Previously, summaries worked by flattening the access tree representing the post of the procedure into (in essence) a list of functions from caller input traces to callee output traces. This is inefficient in many ways, and is also much more complex than just using the original access tree as the summary. One big inefficiency of the old way is this: calling `Trace.append` is slow, and we want to do it as few times as possible. Under the old summary system, we would do it at most once for each "function" in the summary list. Now, we'll do it at most once for each node in the access tree summary. This will be a smaller number of calls, since each node can summarize many input/output relationships. Reviewed By: jeremydubreil Differential Revision: D4271579 fbshipit-source-id: 34e407a 8 years ago			`module Java = AccessTree.Make(JavaTrace)`
			`module Cpp = AccessTree.Make(CppTrace)`
[quandary] format for summaries Reviewed By: mbouaziz Differential Revision: D3838520 fbshipit-source-id: 7cd8bcb 8 years ago
[quandary] summaries are access trees too Summary: Previously, summaries worked by flattening the access tree representing the post of the procedure into (in essence) a list of functions from caller input traces to callee output traces. This is inefficient in many ways, and is also much more complex than just using the original access tree as the summary. One big inefficiency of the old way is this: calling `Trace.append` is slow, and we want to do it as few times as possible. Under the old summary system, we would do it at most once for each "function" in the summary list. Now, we'll do it at most once for each node in the access tree summary. This will be a smaller number of calls, since each node can summarize many input/output relationships. Reviewed By: jeremydubreil Differential Revision: D4271579 fbshipit-source-id: 34e407a 8 years ago			`module AccessTree = struct`
			`type t =`
			`\| Java of Java.t`
			`\| Cpp of Cpp.t`
[quandary] format for summaries Reviewed By: mbouaziz Differential Revision: D3838520 fbshipit-source-id: 7cd8bcb 8 years ago
[quandary] summaries are access trees too Summary: Previously, summaries worked by flattening the access tree representing the post of the procedure into (in essence) a list of functions from caller input traces to callee output traces. This is inefficient in many ways, and is also much more complex than just using the original access tree as the summary. One big inefficiency of the old way is this: calling `Trace.append` is slow, and we want to do it as few times as possible. Under the old summary system, we would do it at most once for each "function" in the summary list. Now, we'll do it at most once for each node in the access tree summary. This will be a smaller number of calls, since each node can summarize many input/output relationships. Reviewed By: jeremydubreil Differential Revision: D4271579 fbshipit-source-id: 34e407a 8 years ago			`let pp fmt = function`
			`\| Java access_tree -> Java.pp fmt access_tree`
			`\| Cpp access_tree -> Cpp.pp fmt access_tree`
			`end`
[quandary] format for summaries Reviewed By: mbouaziz Differential Revision: D3838520 fbshipit-source-id: 7cd8bcb 8 years ago
[quandary] summaries are access trees too Summary: Previously, summaries worked by flattening the access tree representing the post of the procedure into (in essence) a list of functions from caller input traces to callee output traces. This is inefficient in many ways, and is also much more complex than just using the original access tree as the summary. One big inefficiency of the old way is this: calling `Trace.append` is slow, and we want to do it as few times as possible. Under the old summary system, we would do it at most once for each "function" in the summary list. Now, we'll do it at most once for each node in the access tree summary. This will be a smaller number of calls, since each node can summarize many input/output relationships. Reviewed By: jeremydubreil Differential Revision: D4271579 fbshipit-source-id: 34e407a 8 years ago			`type t = AccessTree.t`
[quandary] format for summaries Reviewed By: mbouaziz Differential Revision: D3838520 fbshipit-source-id: 7cd8bcb 8 years ago
[quandary] summaries are access trees too Summary: Previously, summaries worked by flattening the access tree representing the post of the procedure into (in essence) a list of functions from caller input traces to callee output traces. This is inefficient in many ways, and is also much more complex than just using the original access tree as the summary. One big inefficiency of the old way is this: calling `Trace.append` is slow, and we want to do it as few times as possible. Under the old summary system, we would do it at most once for each "function" in the summary list. Now, we'll do it at most once for each node in the access tree summary. This will be a smaller number of calls, since each node can summarize many input/output relationships. Reviewed By: jeremydubreil Differential Revision: D4271579 fbshipit-source-id: 34e407a 8 years ago			`let pp = AccessTree.pp`