Summary:
Looks like this one was already causing circular dependency issues!
Saves threading the callback through *many* functions.
Reviewed By: ngorogiannis
Differential Revision: D21261636
fbshipit-source-id: 2b23aa07d
Summary:
- needed to make biabduction/ its own library as it shouldn't depend on
backend/Printer as a result
- it's a higher level of abstraction
Changed NodePrinter to not swallow biabduction timeouts, thereby
removing its footgunness.
Reviewed By: ngorogiannis
Differential Revision: D21261645
fbshipit-source-id: 592526d85
Summary:
absint/ is its own dune library. There was one last obstacle: we need
callbacks to `NodePrinter`. We'll add more to `AnalysisCallbacks` in future
diffs.
Reviewed By: ngorogiannis
Differential Revision: D21257476
fbshipit-source-id: 3a2ddef14
Summary:
`State` is used by the AI framework, which isn't supposed to know about
biabduction/. Split the biabduction-specific parts into
biabduction/State.ml and keep the rest in absint/AnalysisState.ml.
Reviewed By: ngorogiannis
Differential Revision: D21257470
fbshipit-source-id: e01d1fed3
Summary:
`ProcData.t` contains a `Summary.t`. Eventually we want to fix this too
so that checkers don't depend on backend/, i.e. on all the other
checkers via Summary.ml. But in order to migrate progressively we can
first migrate absint/ and one step on the way is for it to not know what
kind of analysis data it is passing around.
This extra flexibility only costs us passing an extra `Procdesc.t` in a
couple more functions so it's actually not a bad change in itself.
Reviewed By: ngorogiannis
Differential Revision: D21257466
fbshipit-source-id: a91f7b191
Summary:
This is needed to make absint/ its own dune library. Modules in absint/
cannot depend on modules in backend/. This is because backend/Summary.ml
depends on *all* the (inteprocedural) analyses since its stores elements
of their domains. But analyses are supposed to depend on absint/ to
use the AI framework and others. Thus absint/ cannot depend on backend/
otherwise it creates a dependency cycle.
Right now infer builds with this cycle because we consider all these
directories to be one library and there is no dependency cycle between
the individual modules, but making absint/ a library makes the situation
coarser.
One actual change in there: one function in PatternMatch was specific to
nullsafe and was moved there.
Reviewed By: ngorogiannis
Differential Revision: D21257467
fbshipit-source-id: 42af43315
Summary:
This is a step in disentangling the various analyses: that file used to
make every checker on biabduction because of a few of its functions that
use biabduction datatypes.
Split reporting.ml into:
- Reporting.ml: the functions all checkers need to report errors. This
is put in absint/ with the other files that are needed by all
checkers.
- SummaryReporting.ml: functions that need to depend on Summary.ml
(useful for later). This is put in backend/ where Summary.ml lives.
- BiabductionReporting.ml: for the biabduction analysis
The rest of the changes are renames to use the appropriate module
amongst the above.
Reviewed By: ngorogiannis
Differential Revision: D21257468
fbshipit-source-id: fa28cefbc
Summary:
This doesn't depend on the java frontend, as we can see from the fact
that it was symlinked from java/ into java_stubs/. So instead of having
these fake stubs (double negation!) put that file in IR/.
Reviewed By: ngorogiannis
Differential Revision: D21257469
fbshipit-source-id: 1c9e88bcc
Summary:
We re-raise all exceptions a few lines below already so this is not
needed. In fact it prevents us from writing the html cleanly before
hitting the exception, which was bad.
Reviewed By: ngorogiannis
Differential Revision: D21257474
fbshipit-source-id: 0b7e2b8d3
Summary:
This fixes a long-standing TODO. I re-ordered the lines by:
- first putting each entry on a single line (replacing "^J " -> " "
in emacs)
- then using emacs' M-x reverse-region
- then auto-formatting again
Reviewed By: skcho
Differential Revision: D21257475
fbshipit-source-id: 91b780a5d
Summary:
The are already ignored by git and can be useful to 1) debug when the
deadcode Makefile has a bug, and 2) help incremental analysis.
Reviewed By: ngorogiannis
Differential Revision: D21277538
fbshipit-source-id: dc6394ed7
Summary: We currently don't support abducing the spec that we need to delete an attribute, that makes the model for `CFBridgingRelease` work les well when it is, for instance, wrapped in a method. We show examples of how this doesn't work at the moment.
Reviewed By: jvillard
Differential Revision: D21176108
fbshipit-source-id: 79aed7a5d
Summary:
We model `malloc` in Objective-C as `malloc_not_fail` I think because the null case is not normally handled in iOS apps because the OS will just killed the app after giving some memory warnings.
So adding `malloc_not_fail` model to Pulse.
Reviewed By: jvillard
Differential Revision: D21278527
fbshipit-source-id: 17a5008fe
Summary:
This translates the construct `ObjCBridgedCastExpr` when the cast_kind is `OBC_BridgeTransfer`, or in syntax, the cast (`__bridge_transfer`).
This cast means that the object is passed from manual memory management to ARC, so one doesn't need to call `release` manually. It is important to model this to avoid false positives.
It translates it as a builtin that we then model in Pulse, the same way we modelled `CFBridgingRelease` which does the same thing.
The name of the builtin is `__free_cf` which is not ideal but I left it like that for compatibility with biabduction. We can change it once we remove this check from biabduction.
update-submodule: facebook-clang-plugins
Reviewed By: jvillard
Differential Revision: D21176337
fbshipit-source-id: 736ceeb9b
Summary:
Good night, sweet prince. This was never used and hasn't seen progress
in a while.
Reviewed By: jberdine
Differential Revision: D21201932
fbshipit-source-id: e6f537b30
Summary:
In the previous diffs, nullsafe behavior was changed to the following:
nested class mode is inherited from the outer class mode.
Though it is possible to e.g. make nested class Nullsafe and outer not,
or make nested class STRICT and outer just LOCAL, this is an edge case
and we don't want to recommend annotating nested classes by default. The
right way is to make outer class Nullsafe instead.
In this decision, we take into account user experience and codebase
readability.
Reviewed By: ngorogiannis
Differential Revision: D21255806
fbshipit-source-id: 0200cb555
Summary:
With this change, set of possibilities will be more actionable. Most
importantly, this will also educate users and make them realize how
Nullsafe trust works.
NOTE: yes, parenthesis are bit clumsy, but it was the easiest way to
make this change and let the phrase remain grammatically correct.
Reviewed By: artempyanykh
Differential Revision: D21231468
fbshipit-source-id: 4b5349fb5
Summary:
As artempyanykh pointed out, exposing trust list might encourage clients to
start writing business logic manipulating with trust lists outside of
NullsafeMode module, which we don't like to happen.
Reviewed By: artempyanykh
Differential Revision: D21230973
fbshipit-source-id: 39bd0b0d8
Summary:
In the previous diff we changed the semantics of nested classes w.r.t.
to Nullsafe.
Let's make it clear if users will attempt to misuse it.
Reviewed By: artempyanykh
Differential Revision: D21230717
fbshipit-source-id: 0ecc0dd06
Summary:
The order of model list is important to understand which model will be dispatched. Previously, the
models were shuffled with no pattern or rule. This diff sorts them and collects them as groups, so
making it easier to anticipate the dispatch.
Reviewed By: jvillard
Differential Revision: D21227541
fbshipit-source-id: 80be46d86
Summary: Similarly to Enum.name, we model Class.getCanonicalName as returning an arbitrary non-empty string.
Reviewed By: ngorogiannis
Differential Revision: D21207120
fbshipit-source-id: 1e2dbd1fd
Summary:
From the user perspective, the current behavior is confusing.
The users intutitively expect the inner class to inherit Nullsafe mode
from the outer one.
Having a class that is Nullsafe but the inner is not is hence dangerous
and misleading.
For the sake of completeness and to support gradual strictification, we
allow the nested class to improse additional strictness. Particularly,
the inner class can be Nullsafe but the outer can be not.
A follow up to this diff will include warnings telling about redundant and wrong usages of nested annotations.
Reviewed By: artempyanykh
Differential Revision: D21228055
fbshipit-source-id: 75755ad1d
Summary:
1. Most of trust list operations are abstract anyway, we don't actually
rely on the fact that this is list
2. Inside NullsafeMode.ml, we effectively need set operations, which is both more
idiomatic to express and Ocaml and faster
3. This will simplify implementation of the next diff which introduces
mode intersect operation
Reviewed By: artempyanykh
Differential Revision: D21207207
fbshipit-source-id: 0c1fc4426
Summary: Iterator invalidation traces were based on vector rather than iterator itself.
Reviewed By: ezgicicek
Differential Revision: D21202047
fbshipit-source-id: 62ce8a488
Summary: The transition function was using a complicated-looking and possibly-inefficient pattern of options for everything, when simple pattern matching with guards is sufficient.
Reviewed By: skcho
Differential Revision: D21179606
fbshipit-source-id: a37f97594
Summary:
Lets move the logic dealing with non-java classes outside of this module
so we can modify it easier in the next diff.
Reviewed By: artempyanykh
Differential Revision: D21204822
fbshipit-source-id: 67b5937bc
Summary:
Because of this bug, we evaluated anonymous class constructors in
Default mode, even if the underlying class was Nullsafe
Reviewed By: artempyanykh
Differential Revision: D21202986
fbshipit-source-id: a31318901
Summary: Specialise the above option to `true` and remove resulting dead code.
Reviewed By: dulmarod
Differential Revision: D21177041
fbshipit-source-id: 4a1c65850
Summary: This option makes RacerD angelic wrt the ownership of returned objects from procedures without summary. This will now be made the default and the option deprecated up the diff stack.
Reviewed By: dulmarod
Differential Revision: D21174676
fbshipit-source-id: 9c48d3d7d
Summary:
We model Enum.name as returing a constant name, rather than getting real field names. We did this
because we couldn't think of any big gains, in terms of analysis precision/performance, from getting
the real names.
Reviewed By: ezgicicek
Differential Revision: D21201730
fbshipit-source-id: a2dc01a44
Summary: This diff revises the models of Collection.set and get to handle its elements.
Reviewed By: ezgicicek
Differential Revision: D21201242
fbshipit-source-id: 9c248453d
Summary:
We ignored allocator models for vectors, and were not able to initialize vectors properly. This diff fixes this issue.
It also adds a test which was a FN before.
Reviewed By: skcho, jvillard
Differential Revision: D21089492
fbshipit-source-id: 6906cd1d1
Summary: D21155014 replaced `skip` call with a Load but this was not right. Instead, let's add a new builtin function (rather than skip) so that other analyses can freely model it as they want.
Reviewed By: jvillard
Differential Revision: D21178286
fbshipit-source-id: c214ccfb0
Summary: Java has this pattern of wrapping non-thread-safe containers in factory methods producing identically-typed results, but wrapped in a synchronised shell. This diff teaches RacerD about some common factory methods and uses the attribute domain to track the dynamic type of their results.
Reviewed By: ezgicicek
Differential Revision: D21155538
fbshipit-source-id: 42ebe6251
Summary: Complete the set of models for java containers that Infer should not report thread safety violations.
Reviewed By: ezgicicek
Differential Revision: D21138280
fbshipit-source-id: 01e1944b6
Summary: Models were partial and/or simply missing (`Map` writes!). Now the modelled containers use inheritance for conciseness (`List` reads are only those not caught by the `Collection` matcher, etc). Also, add URLs to documentation sources.
Reviewed By: ezgicicek
Differential Revision: D21132069
fbshipit-source-id: fefb360f0
Summary: `CFBridgingRelease` and `__bridge_transfer` which I'll model later, transfer the memory model from manual memory ref count to ARC (automatic ref count), so to avoid false positives this needs to be modelled. We can simply remove the Allocated attribute from the state, which means we won't try to track that memory anymore.
Reviewed By: skcho
Differential Revision: D21088218
fbshipit-source-id: 3520a0d59
Summary: This diff suppresses cost issues on lambda and auto-generated procedures, since they were too noisy.
Reviewed By: ezgicicek
Differential Revision: D21153619
fbshipit-source-id: 65ad6dcc3
Summary:
Replace horrible hack with ok hack.
The main difficulty in implementing the disjunctive domain is to avoid
the quadratic time complexity of executing the same disjuncts over and
over again when going around loops:
First time around a loop, assuming for example a single disjunct `d`:
```
[d]
loop body
[d1' \/ d2']
```
Second time around the same loop: the new pre will be the join of the
posts of predecessor nodes, so `old_pre \/ post(loop,old_pre)`, i.e.
`d \/ d1' \/ d2'`. Now we need to execute `loop body` again
*without running the symbolic execution of `d` again* (and the time after
that we'll want to not execute `d`, `d1'`, or `d2'`).
Horrible hack (before): Disjuncts have a boolean "visited" attached
that does its best to keep track of whether a given disjunct is old or
new. When executing a single *instruction* look at the flag and skip the
state if it's old. Of course we have no way to know for sure so it turns
out it was often wrongly re-executing old disjuncts. This was also
producing the wrong results over even simple loops: only the last
iteration would make it outside the loop for some reason. Overall, the
semantics were pretty untractable and shady at best.
New hack (this diff): only run instructions of a given *node* on
disjuncts that are not physically equal to the "pre" ones already in the
invariant map for the current node.
This gives the correct result over simple loops and a nice performance
improvement in general (probably the old heuristic was hitting the
quadratic bad case more often).
Reviewed By: skcho
Differential Revision: D21154063
fbshipit-source-id: 5ee38c68c
Summary:
This is a preparatory diff to make the actual change more readable. This
just moves the code around, trying to change it as little as possible.
Reviewed By: skcho
Differential Revision: D21154065
fbshipit-source-id: e086318c1
Summary:
This makes the API of [instrs] easier to work with at the price of some
duplication in the GADT.
This allows us to construct `[skip]` in `AbstractInterpreter` without
imposing a particular direction. This will make it the next diffs about
a disjunctive domain easier.
Reviewed By: skcho
Differential Revision: D21153694
fbshipit-source-id: f86c180fa
Jules Villard
Dulma Churchill
Mitya Lyubarskiy
Sungkeun Cho
Daiva Naudziuniene
Nikos Gorogiannis
Ezgi Çiçek
Josh Berdine