infer_clone/sledge/lib/domain_sh.mli

(*
 * Copyright (c) Facebook, Inc. and its affiliates.
 *
 * This source code is licensed under the MIT license found in the
 * LICENSE file in the root directory of this source tree.
 *)

(** Abstract domain *)

include Domain_intf.Dom

(* formals should include all the parameters of the summary. That is both
   formals and globals. *)
val create_summary :
     locals:Reg.Set.t
  -> formals:Reg.Set.t
  -> entry:t
  -> current:t
  -> summary * t

val simplify_states : bool ref
[sledge] Print pre/post on function return Summary: Print pre- and post- conditions (aka, summaries) when analyzer hits a function return - plumbing the precondition through the analyzer so that it is available when return is hit Reviewed By: jberdine Differential Revision: D15713725 fbshipit-source-id: b10b6206f 6 years ago			`(*`
[copyright] Remove years Reviewed By: jvillard Differential Revision: D15771884 fbshipit-source-id: e2997e3a3 6 years ago			`* Copyright (c) Facebook, Inc. and its affiliates.`
[sledge] Print pre/post on function return Summary: Print pre- and post- conditions (aka, summaries) when analyzer hits a function return - plumbing the precondition through the analyzer so that it is available when return is hit Reviewed By: jberdine Differential Revision: D15713725 fbshipit-source-id: b10b6206f 6 years ago			`*`
			`* This source code is licensed under the MIT license found in the`
			`* LICENSE file in the root directory of this source tree.`
			`*)`

			`(** Abstract domain *)`

[sledge] Rearrange into CLI binary and LLVM-independent library Summary: Move files, adjust build system, etc. This also separates out the ppx_trace conditional compilation debug tracing machinery into an independent package and library. Reviewed By: jvillard Differential Revision: D20322876 fbshipit-source-id: a50522462 5 years ago			`include Domain_intf.Dom`
[sledge] Generate and apply summaries Summary: Define a new function summary type and compute it on function return. As an intermediary step also apply the just computed summary to function pre so it can be compared to what was actually computed. Reviewed By: jvillard Differential Revision: D16149833 fbshipit-source-id: b826c17e8 5 years ago
			`(* formals should include all the parameters of the summary. That is both`
[sledge] Distinguish program expressions and formula terms Summary: There are a number if issues with using the same type for expressions in code and in formulas. One is that the type systems of the two should be different. Another is that conflating the two compromises the ability of Llair to correctly express aspects such as integer overflow, floating point rounding, etc. Also, it could be beneficial to have more source locations for program expressions than makes sense for terms. This diff simply unshares Exp, leading to a copy named Term. Likewise, Reg is now a copy of Var. Simplifications to come. Reviewed By: bennostein Differential Revision: D17665250 fbshipit-source-id: 4359a80d5 5 years ago			`formals and globals. *)`
[sledge] Generate and apply summaries Summary: Define a new function summary type and compute it on function return. As an intermediary step also apply the just computed summary to function pre so it can be compared to what was actually computed. Reviewed By: jvillard Differential Revision: D16149833 fbshipit-source-id: b826c17e8 5 years ago			`val create_summary :`
[sledge] Distinguish program expressions and formula terms Summary: There are a number if issues with using the same type for expressions in code and in formulas. One is that the type systems of the two should be different. Another is that conflating the two compromises the ability of Llair to correctly express aspects such as integer overflow, floating point rounding, etc. Also, it could be beneficial to have more source locations for program expressions than makes sense for terms. This diff simply unshares Exp, leading to a copy named Term. Likewise, Reg is now a copy of Var. Simplifications to come. Reviewed By: bennostein Differential Revision: D17665250 fbshipit-source-id: 4359a80d5 5 years ago			`locals:Reg.Set.t`
			`-> formals:Reg.Set.t`
[sledge] Actually use function summaries Summary: If function summaries are enabled calling a function first tries to apply a summary, if succesful, it directly jumps to the return site of the call. Otherwise it proceeds as before. Reviewed By: jvillard Differential Revision: D16201251 fbshipit-source-id: cec52e0e5 5 years ago			`-> entry:t`
			`-> current:t`
[sledge] Functorize worklist, separate out domain-specific logic Summary: Add support for future development of new abstract domains by eliminating hard-wired dependencies from the worklist into the symbolic heap domain. Also includes an implementation of a trivial unit domain and a CLI flag to enable its use, for debugging purposes. Reviewed By: jberdine Differential Revision: D17281681 fbshipit-source-id: 5858fd420 5 years ago			`-> summary * t`
[sledge] Simplify states during symbolic execution Summary: `Sh.simplify` formulas after each manipulation during symbolic execution, unless `-no-simplify-states` is passed. Reviewed By: ngorogiannis Differential Revision: D20120265 fbshipit-source-id: 11464cfb2 5 years ago
			`val simplify_states : bool ref`