infer_clone/infer/src/pulse/PulseModels.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.
 *)
open! IStd
open PulseBasicInterface

type exec_fun =
     caller_summary:Summary.t
  -> Location.t
  -> ret:Ident.t * Typ.t
  -> PulseAbductiveDomain.t
  -> PulseAbductiveDomain.t list PulseOperations.access_result

type model = exec_fun

val dispatch :
     Tenv.t
  -> Typ.Procname.t
  -> (AbstractValue.t * ValueHistory.t) ProcnameDispatcher.Call.FuncArg.t list
  -> model option
[pulse] pulse models Summary: Some mild refactoring to isolate the modelling part. Reviewed By: mbouaziz Differential Revision: D10406804 fbshipit-source-id: 3be76a5e9 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.`
[pulse] pulse models Summary: Some mild refactoring to isolate the modelling part. Reviewed By: mbouaziz Differential Revision: D10406804 fbshipit-source-id: 3be76a5e9 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.`
			`*)`
			`open! IStd`
[pulse][7/9] kill `AddrTracePair` Summary: The name had rotten: it should be `AddrHistPair`. There is little value of exposing the type of the pair `AbstractValue.t * ValueHistory.t`, just inline its definition everywhere. Reviewed By: ezgicicek Differential Revision: D17955283 fbshipit-source-id: d145251e0 5 years ago			`open PulseBasicInterface`
[pulse] pulse models Summary: Some mild refactoring to isolate the modelling part. Reviewed By: mbouaziz Differential Revision: D10406804 fbshipit-source-id: 3be76a5e9 6 years ago
[pulse] vector models Summary: Model `x[y]` and `x.push_back(i)` to catch the classic bug of "take reference inside vector, invalidate, then use again". Reviewed By: da319 Differential Revision: D10445824 fbshipit-source-id: 21ffd9677 6 years ago			`type exec_fun =`
[pulse] calling known lambdas calls the corresponding proc name Summary: We know how to do interprocedural calls so let's use that! Reviewed By: mbouaziz Differential Revision: D16008164 fbshipit-source-id: 4c34bf704 6 years ago			`caller_summary:Summary.t`
			`-> Location.t`
[pulse] move to SIL proper Summary: [apologies for the unreviewable diff...] Get rid of HIL expressions in pulse. This finishes the HIL -> SIL migration. The first step made pulse start from SIL instructions but would translate most accesses to HIL to re-use most of the existing pulse code. This diff gets rid of the intermediate translation of SIL expressions to HIL expressions. Big changes: 1. `PulseOperations` mostly rewritten, driven by using `Exp.t` instead of `HilExp.AccessExpression.t` for everything. 2. Stop trying to reverse-engineer what addresses mean in terms of access paths from program variables. Rely on the trace pointing at the right places in the code to be enough. This is because it wasn't that useful (and could even be misleading when wrong) but could be prohibitively expensive in degenerate cases (eg nodes with tens of thousands of successive array accesses...) 3. `PulseAbductiveDomain.apply_post` now returns the computed return value instead of recording it itself. 4. Change of vocabulary: `materialize` -> `eval`, `crumb` -> `event` 5. Function calls arguments are now evaluated prior to doing anything else, which saves everything else from having to (remember to) do that. In particular, this changes how models look quite a bit. Reviewed By: mbouaziz Differential Revision: D15986373 fbshipit-source-id: 1d79935de 6 years ago			`-> ret:Ident.t * Typ.t`
[pulse][interproc 2/3] abductive domain Summary: For each operation on the domain, try to record what it requires of the precondition of the function. This is akin to what happens in the biabduction backend, hence the terminology used. Reviewed By: jberdine Differential Revision: D14387148 fbshipit-source-id: a61fe30c8 6 years ago			`-> PulseAbductiveDomain.t`
[pulse] allow models to return disjuncts Summary: This is useful for the model of `exit` that returns 0 disjuncts. All other models return 1 disjunct for now, but in the future things like `malloc()` will need to return 2 possible states for instance. Reviewed By: ngorogiannis Differential Revision: D14753491 fbshipit-source-id: 3e7387d6d 6 years ago			`-> PulseAbductiveDomain.t list PulseOperations.access_result`
[pulse] pulse models Summary: Some mild refactoring to isolate the modelling part. Reviewed By: mbouaziz Differential Revision: D10406804 fbshipit-source-id: 3be76a5e9 6 years ago
			`type model = exec_fun`

[pulse] Move models to ProcnameDispatcher style Summary: Rather than repeatedly matching actuals, let's use `ProcnameDispatcher.ModeledCall` to pick up the actual arguments with their corresponding values. This simplifies the models. Reviewed By: jvillard Differential Revision: D18685855 fbshipit-source-id: 7788bd8bb 5 years ago			`val dispatch :`
			`Tenv.t`
			`-> Typ.Procname.t`
			`-> (AbstractValue.t * ValueHistory.t) ProcnameDispatcher.Call.FuncArg.t list`
			`-> model option`