Summary: Add the interface that will be used to lock Procedures.
Reviewed By: ngorogiannis
Differential Revision: D19580578
fbshipit-source-id: b5e334b18
Summary:
In an equation such as `x = ⟨n,a⟩`, `x` is implicitly an aggregate of
size `n` (or else the equation is ill-typed). Make this explicit by
normalizing such equations to e.g. `⟨|⟨n,a⟩|,x⟩ = ⟨n,a⟩`.
Reviewed By: ngorogiannis
Differential Revision: D19358546
fbshipit-source-id: 77f67a0da
Summary:
Strengthen Equality.solve_for_vars so that it will solve cases such as
```
∃ a. ⟨n,a⟩ = ⟨m,b⟩^⟨o,c⟩
```
Reviewed By: ngorogiannis
Differential Revision: D19356324
fbshipit-source-id: a57625ba6
Summary:
Due to paying closer attention to which terms are already normalized
by the accumulated solution substitution.
Reviewed By: ngorogiannis
Differential Revision: D19356323
fbshipit-source-id: e162414a0
Summary:
The function transforming terms passed to Sh.map might produce trivial
constraints, filter them out.
Reviewed By: ngorogiannis
Differential Revision: D19286628
fbshipit-source-id: e3d9926ce
Summary:
In order for Equality.solve to generate fresh variables, it needs to
be passed the universal context with respect to which variables must
be chosen fresh.
Reviewed By: ngorogiannis
Differential Revision: D19286630
fbshipit-source-id: ebbedd954
Summary:
Aggregate args of Extract and Concat must be aggregate terms, in
particular, not variables. This maintains the property that the size
of any aggregate can be computed.
Reviewed By: ngorogiannis
Differential Revision: D19286625
fbshipit-source-id: 1af1e4183
Summary:
The byte-array theory used for the contents of memory is strong
enough to express all the constraints arising during symbolic
execution without the ability to extract a slice out of a byte-array.
However, without Extract, it is not possible to solve some equations
for some variables, for example solving ⟨n,α⟩^⟨m,β⟩ = ⟨l,γ⟩ for α.
Solving such equations is needed for quantifier elimination and to
formulate the byte-array theory as a Shostak theory.
Reviewed By: ngorogiannis
Differential Revision: D19286632
fbshipit-source-id: 07dc112d0
Summary:
Revise the ad hoc treatment to drop tautologous constraints such as
∃x,y. x = y to only apply when x and y do not appear elsewhere.
Reviewed By: ngorogiannis
Differential Revision: D19282633
fbshipit-source-id: 7fb9951ec
Summary:
Equality.solve_for_var_contexts can produce solution substitutions
that witness existentials in more cases than the
single-existential-occurrence heuristic, and is more conservative in
cases where the latter is incomplete.
Reviewed By: ngorogiannis
Differential Revision: D19282634
fbshipit-source-id: f86f0a9cb
Summary:
```
val trim : bound:Var.Set.t -> Var.Set.t -> t -> t
(** [trim bound kills subst] is [subst] without mappings that mention
[kills] or [bound ∩ fv x] for removed entries [x ↦ u] *)
```
To be used for existential witnessing and quantifier elimination.
Reviewed By: ngorogiannis
Differential Revision: D19282644
fbshipit-source-id: d981a1cb4
Summary:
```
val solve_for_vars : Var.Set.t list -> t -> Subst.t
(** [solve_for_vars \[v₁;…\] r] is a solution substitution that is
entailed by [r] and consists of oriented equalities [x ↦ u] such that
[fv x ⊈ vᵢ ⊇ fv u] where [i] is minimal such that [vᵢ]
distinguishes [fv x] and [fv u], if one exists. *)
```
To be used for existential witnessing and quantifier elimination.
Reviewed By: ngorogiannis
Differential Revision: D19282636
fbshipit-source-id: c5b006cea
Summary: `String.split(regexp)` returns an array that is split by the given regexp. If the regexp doesn't match, the original string is returned. Hence, the resulting array's length must be in `[1, max(1, n_u -1)]` where`n_u` is the upper bound of the string's length.
Reviewed By: dulmarod
Differential Revision: D19578318
fbshipit-source-id: 675af7376
Summary:
Adding a new check as part of the SelfInBlock checker, for cases when a strong pointer to self, that is not self, is captured in the block.
This will cover the following wrong scenarios:
1. strongSelf is a local variable in a block as it should be, and then it's used in a sub-block, in which case it's a captured variable.
2. weakSelf is defined without the weak attribute by mistake.
Reviewed By: ngorogiannis
Differential Revision: D19538036
fbshipit-source-id: 151871745
Summary:
In practice, condition redundant is extremely noisy and low-signal
warning (hence it is turned off by default).
This diff does minor tweaks, without the intention to change anything
substantially:
1/ Change severity to advice
2/ Change "is" to "might be"
3/ Describe the reason in case the origin comes from a method.
The short term motivation is to use 3/ for specific use-case: running nullsafe on codebase and
identify most suspicious functions (that are not annotated by often
compared with null).
Reviewed By: artempyanykh
Differential Revision: D19553571
fbshipit-source-id: 2b43ea0af
Summary:
This is/can be useful for future changes that make the reporting more
precise based on the exact origin.
See the follow up diff as an example.
Reviewed By: artempyanykh
Differential Revision: D19553567
fbshipit-source-id: c2b2c28a1
Summary: Currently, empty summaries are passed to the cluster callbacks. This is pointless and could potentially lead to recomputing already analysed summaries. This change passes only procnames to the callback, and `Ondemand` is used to load the summary or analyse as needed.
Reviewed By: jvillard
Differential Revision: D19544043
fbshipit-source-id: 28ab642c3
Summary: There is no need to provide type environments to cluster analysers, since the execution environment can be used to retrieve those on demand.
Reviewed By: jvillard
Differential Revision: D19543561
fbshipit-source-id: f9b064011
Summary: We were reporting strongSelf Not Checked when the variable was checked in a conditional, this diff fixes that.
Reviewed By: jvillard
Differential Revision: D19535943
fbshipit-source-id: f8e64e1b7
Summary:
This fixes the segmentation fault in docker master build. See
https://github.com/facebook/infer/issues/1194.
Reviewed By: jvillard
Differential Revision: D19449711
fbshipit-source-id: 0e281df5b
Summary: I noticed when looking into a false positive of strongSelf Not Checked, that there were some inconsistencies in the translation of if statements with an and, with an extra redundant join only if using a method in the condition that returned an object. So I could repro the problem and investigate and found the place of the inconsistency in the translation. This diff fixes it without changing things too much.
Reviewed By: jvillard
Differential Revision: D19518368
fbshipit-source-id: 47a6a778c
Summary:
The order by which the scheduler visits odd and even methods here
will determine if there is any report at all. This is a bad test
so remove.
Reviewed By: fgasperij
Differential Revision: D19535537
fbshipit-source-id: 6b64b0de9
Summary: Adding reporting to strongSelf Not Checked when strongSelf is passed to a method in a not explicitly nullable position.
Reviewed By: ezgicicek
Differential Revision: D19330872
fbshipit-source-id: 95871a70a
Summary: After receiving feedback about this, I'm changing the reporting of strongSelf Not Checked to only in cases where it can cause a crash. Here I'm adding reporting for field access, and removing general reporting. In a next diff, I'll also add reporting for passing strongSelf to methods in not explicitly nullable positions.
Reviewed By: skcho
Differential Revision: D19329842
fbshipit-source-id: 35beb2aa3
Summary:
The RestartScheduler needs to know if the worker finished it's task
because:
1. there was no more work to do or
2. found that a needed Procname was already taken (this part is not yet implemented)
This need was addressed by (i) making the functions that the workers execute
return a value of task_result.t intead of unit and (ii) adding a
constructor to the worker_message.t (FinishedTask).
Reviewed By: ngorogiannis
Differential Revision: D19467783
fbshipit-source-id: a76b02b6c
Summary:
1. One should use either a writer or a stream to send a response, but not both.
2. A response should be forwarded only if it was commited.
Both properties are extracted from API comments on classes in the servlet API.
Reviewed By: jvillard
Differential Revision: D19514568
fbshipit-source-id: 79f0257ed
Summary:
If data comes from an outer OutputStream, then this outer OutputStream
needs to be flushed before getting the byte array.
Reviewed By: jvillard
Differential Revision: D19514569
fbshipit-source-id: e3e025394
Summary: We were lacking this kind of test where one interface refines the nullability of the other.
Reviewed By: ngorogiannis
Differential Revision: D19514245
fbshipit-source-id: fa3e781f3
Summary: `cost.ml` is huge. Let's split it to its logical parts (basically creating new files for the modules that were already in `cost.ml`) and move all cost related files into `\cost` directory. While we are at it, let's add `mli` files too.
Reviewed By: jvillard
Differential Revision: D19496263
fbshipit-source-id: 45096db4c
Summary: Deadlocks often result in two reports if not deduplicated (two traces), so there is some logic for doing that. Locks recently became an opaque type, with the `get_access_path` loophole supporting that deduplication ordering. Fix that here and remove `Lock.get_access_path`.
Reviewed By: jvillard
Differential Revision: D19465223
fbshipit-source-id: b597e3c65
Summary:
This is a common enough case to make error message specific.
Also let's ensure it's modelled.
Reviewed By: artempyanykh
Differential Revision: D19431899
fbshipit-source-id: f34459cb3
Summary:
The previous diff changes the message for params case, this one handles
return.
Reviewed By: artempyanykh
Differential Revision: D19430706
fbshipit-source-id: f897f0e56
Summary:
This diff gets global constant array values from their initializers. The `find_global_array` function is
added to memory domain, which finds values of global array locations during the ondemand value
generation.
Reviewed By: ngorogiannis
Differential Revision: D19300143
fbshipit-source-id: 7b0b84c42
Summary: Use more informative method names, and add comments explaining the logic behind each test. Correct two cases which are FPs instead of legitimate reports.
Reviewed By: artempyanykh
Differential Revision: D19465227
fbshipit-source-id: 29332e2b9
Summary: Change `MayBlock` and `StrictModeCall` constructors from taking a string to a `Procname.t`, which was the sole source of that string anyway.
Reviewed By: ezgicicek
Differential Revision: D19465226
fbshipit-source-id: e3ed6ef88
Jules Villard
Mitya Lyubarskiy
Fernando Gasperi Jabalera
Josh Berdine
Ezgi Çiçek
Dulma Churchill
Nikos Gorogiannis
Sungkeun Cho
Radu Grigore
Artem Pianykh
Martin Trojer