Summary:
This diff reports paths under the xcode isysroot as relative in tests.
This was a problem when another machine that has a different isysroot
directory is running the test.
Reviewed By: ezgicicek
Differential Revision: D23729222
fbshipit-source-id: 4e9681f65
Summary:
ObjC++ models are a copy (symlink) into the ObjC ones, albeit with different compile time flags. However, the resulting procnames are identical, and we are left with only one copy of models anyway. This means that only one version (chosen arbitrarily by the build order) is used for analysis.
This diff deletes the ObjC++ version.
Reviewed By: jvillard
Differential Revision: D23704266
fbshipit-source-id: 1dc94251f
Summary:
Handle the case of
- computing the range of `[lb, ub]` where `lb` contains length path and `ub` is constant. E.g. `[a.length, 2]` would give `3` range
- simplifying `c1 +/- min(c2, a.length)` to `c1 +/- min(c2, 0)`
since the length of a collection/array is always nonnegative.
This also removes some existing FPs in tests results.
Facebook
Context: we stumbled upon this issue in ObjC results TV109717121 which is corresponding to the added test case.
Reviewed By: skcho
Differential Revision: D23648807
fbshipit-source-id: 1e89ea246
Summary: This diff adds trace field for autoreleasepool size. Unlike to the other checkers, eg inferbo and operation cost, the autoreleasepool size checker should have traces for constants.
Reviewed By: ezgicicek
Differential Revision: D23678084
fbshipit-source-id: 35e6cf5f5
Summary:
For complexity issues from O(m) to O(n), we only include the trace of the current complexity O(n). However, this makes it difficult to understand what the original complexity O(m) was. Especially in fixed issues where n=1, we only get a constant cost with no trace attached, so it is difficult to see how the symbol m disappeared.
This diff includes the traces for the previous cost in the cost issues.
Reviewed By: skcho
Differential Revision: D23680360
fbshipit-source-id: 3f2b21b20
Summary:
The best-fit allocator with overhead 120 is slightly faster, and
significantly reduces peak memory usages in the workers.
Reviewed By: jvillard
Differential Revision: D23678794
fbshipit-source-id: ccdfced74
Summary:
The `attr_kind` column has now exactly two possible values: defined and undefined (since D22187238 (61ae2d1e1b)). This is also what should be stored in the field `is_defined` in the procedure attributes. Finally, the cfg can be `NULL` or not. This diff makes all three of these agree, in order to allow for the removal of the `attr_kind` column up the stack, since it will be equivalent to `cfg is NOT NULL`.
The changes in the tests indicate improved correctness: previously, specialising a modelled callee would result in a dummy entry in the procedures table, because all clang procedures were given a procdesc, so the specialisation would specialise the empty procdesc. Now, the model is not shadowed by the specialised dummy procdesc, and is specialised itself (and that's why it also ends up in the capture DB, which is slightly counter-intuitive).
Reviewed By: jvillard
Differential Revision: D23536931
fbshipit-source-id: 983216cb6
Summary: So that it can be meaningfully used for diffing across infer versions, say.
Reviewed By: martintrojer
Differential Revision: D23648560
fbshipit-source-id: 98d634e37
Summary:
Since we don't yet support `.sig` files for fields, hardcoding this in Ocaml
for now.
Reviewed By: jvillard
Differential Revision: D23627390
fbshipit-source-id: 8df78068d
Summary: Polynomial category zero corresponds to unreachable but "zero" is a misnomer and rather confusing. Let's fix it.
Reviewed By: skcho
Differential Revision: D23597735
fbshipit-source-id: f0c96ed26
Summary:
Eliminate the need to serialise procnames when sending work from the restart scheduler to the workers, by sending the proc_uid instead. This is (much) shorter than the byte representation of the proc_name and it's the primary DB key of the procedures table, so it can be used by the worker to obtain the full procname.
Also, reduce GC churn by using folds in the scheduler startup instead of copying lists over and over.
Reviewed By: jberdine
Differential Revision: D23566131
fbshipit-source-id: 1472aa990
Summary:
- freshen up /docs/next/absint-framework to give sensible advice, and
delete outdated bits that are now in the API docs so they remain fresh
- delete SimpleChecker.ml as it's just a source of bitrot
- delete the "adding checkers" page as it's completely outdated and
subsumed by the "AI framework" page + the labs.
Reviewed By: jberdine
Differential Revision: D23597271
fbshipit-source-id: 78b541746
Summary:
We defined cost's plus as "zero+unreachable = unreachable" for the operation cost. The meaning of
the zero cost is that no statment is analyzed yet, and the unreachable(bottom) cost means a program
point is analyzed as unreachable. We thought "zero+unreachable" happens in very specific cases we
need to check, or due to an analyzer bug. For debugging purpose, we defined it to return more
specific unreachable cost.
However, in allocation/autoreleasepool costs, the zero cost is not very special value. If there is
no alloc/autorelease calls, they can have the zero cost. "zero+unreachable = unreachable" doesn't
make sense there.
This diff changes the plus as "zero+unreachable = zero" for the non-operation costs.
Reviewed By: ezgicicek
Differential Revision: D23578869
fbshipit-source-id: 5392eca1c
Summary: This diff adds some tests run with ARC/non-ARC compiled objective-c sources.
Reviewed By: ezgicicek
Differential Revision: D23542135
fbshipit-source-id: 8e089666b
Summary:
This would previously print that we ran out of fuel even if we didn't
and we simply reached a normal form.
Reviewed By: ezgicicek
Differential Revision: D23575571
fbshipit-source-id: 37d02ca8d
Summary:
This diff adds a new experimental checker for detecting size of objects in autorelease pool in ObjC. The basic mechanism is almost the same with the previous cost calculation:
* Autorelease pool size is increased at explicit `autorelease` call
* Autorelease pool size is set as zero by the `autoreleasepool` block.
While it only supports the explicit calls as of now, we will extend the checker to handle more cases in the following diffs.
Reviewed By: ezgicicek
Differential Revision: D23473145
fbshipit-source-id: 416488176
Summary:
This diff extends the cost_item json format to print the autoreleasepool_size field. Not yet, there
is no semantics for that code kind, so the results will always be zero with no traces.
Reviewed By: ezgicicek
Differential Revision: D23540665
fbshipit-source-id: 94442e376
Summary:
Limit communication bandwidth and serialisation burden by sending procedure filename strings (which are bounded at ~100 bytes) instead of serialising procnames through the socket to the scheduler (which are unbounded and have been seen to reach ~30kB in the worst case for templated procedures).
Context:
Under the restart scheduler, a worker working on a procedure X that discovers a race on a dependency Y it needs fails the computation of X and sends to the scheduler the procname Y. The next time X is about to be rescheduled, the scheduler checks whether Y is still being analysed, by checking if the lock for Y still exists. This check uses the procedure filename already, so we can send that instead.
Reviewed By: jvillard
Differential Revision: D23554995
fbshipit-source-id: 9828e71a2
Summary: Most of the time, when the procdesc of a callee is requested, all that is really required is the procedure attributes. However, requesting the procdesc may return `None` when the procedure is undefined (in Java, and soon for Clang too). So, change all callsites to using attributes instead, where possible.
Reviewed By: jvillard
Differential Revision: D23539422
fbshipit-source-id: 3b1a52d48
Summary: Given the brittleness of DB-indexing over marshalled values (one example exposed in D23191601), the serializer "for comparison" must be removed. Its only use is for source files, and these have an obvious, trivial (and possibly faster and less space hungry) protocol.
Reviewed By: jberdine
Differential Revision: D23499481
fbshipit-source-id: 57ad0ced6
Summary: Given the brittleness of DB-indexing over marshalled values (one example exposed in D23191601), the serializer "for comparison" must be removed. Serialized procnames are no longer used as keys, so their serializer can be converted to the one which preserves sharing (saving some space in the process).
Reviewed By: jberdine
Differential Revision: D23425123
fbshipit-source-id: 9c82da778
Summary:
Store model summaries in the `model_specs` database table instead of in spec files.
This table is populated when a new database is created by loading a dump of the `specs` table in the models database. This avoids the perf and reliability implications of ATTACHing the same, non-read-only models-DB by many processes.
- `BiabductionModels` is moved into `IR` so that `JsonReports` can access it.
- The binary `sqlite3` is now required on the host compiling infer.
Reviewed By: skcho
Differential Revision: D23191601
fbshipit-source-id: 1532481ee
Summary: Since the unique string ID used as a key is also human-readable, remove the now-redundant `proc_name_hum` field, which is only used for debug purposes anyway.
Reviewed By: jberdine
Differential Revision: D23446223
fbshipit-source-id: 5027066ee
Summary: There is still a bug in using marshalled values as keys (exposed up the diff stack) where structurally equal procnames get serialised to distinct keys. This diff addresses that bug by using the existing functionality for string unique IDs.
Reviewed By: ezgicicek
Differential Revision: D23133761
fbshipit-source-id: 3cbafb51b
Summary: There is no reason to write back to the database here, as the resulting procdesc is anyway stored in the summary. This is a source of non-determinism.
Reviewed By: skcho
Differential Revision: D23500220
fbshipit-source-id: 7434e6239
Summary: We don't report and IO Cost and are not planning to do so in the near future. Let's remove it from cost kinds.
Reviewed By: ngorogiannis
Differential Revision: D23499160
fbshipit-source-id: 7281da3af
Summary:
As title.
Facebook
Found this case by examining db.
>
D23394545
Time complexity of `_registerTabPreloadables` has **decreased** from `Top` to `O(1)`. Please make sure this is an expected change. You can inspect the trace to understand the complexity increase:
Reviewed By: ezgicicek
Differential Revision: D23448099
fbshipit-source-id: 108fd1ef2
Summary:
This diff adds translation of `dictionaryWithObjects:forKeys:count:`. In the previous implementation it was
translated as if it was `dictionaryWtihObjectsAndKeys:`, but their function parameters are different.
In this diff, it translates an array literal `NSDictionary* a = @ [ @"firstName": @"Foo", @"lastName":@"Bar" ];` to
```
n$1=NSString.stringWithUTF8:(@"firstName")
n$2=NSNumber.stringWithUTF8:(@"Foo")
n$3=NSNumber.stringWithUTF8:(@"lastName")
n$4=NSNumber.stringWithUTF8:(@"Bar")
temp1[0]:objc_object*=n$1
temp1[1]:objc_object*=n$3
temp2[0]:objc_object*=n$2
temp2[1]:objc_object*=n$4
n$3=NSDictionary.dictionaryWithObjects:forKeys:count:(temp2:objc_object* const [2*8], temp1:objc_object*const [2*8], 2:int)
```
where `temp` is an additional local variable declared as array.
See,
https://developer.apple.com/documentation/foundation/nsdictionary/1574184-dictionarywithobjects?language=objchttps://developer.apple.com/documentation/foundation/nsdictionary/1574181-dictionarywithobjectsandkeys
{F316854542}
Reviewed By: skcho
Differential Revision: D23447042
fbshipit-source-id: 14b7c3f2b
Summary: Added a model for copy constructor for `std::function`. In most cases, the SIL instruction `std::function::function(&dest, &src)` gives us pointers to `dest` and `src`, hence, we model the copy constructor as a shallow copy. However, in some cases, e.g. `std::function f = lambda_literal`, SIL instruction contains the closure itself `std::function::function(&dest, (operator(), captured_vars)`, hence, we need to make sure we copy the right value.
Reviewed By: ezgicicek
Differential Revision: D23396568
fbshipit-source-id: 0acb8f6bc
Summary:
Move Sqlite registered statements inside the functions that use them, since these are only ever used in one place.
Also, reformat some SQL.
Also, make `mark_all_source_files_stale` use an un-prepared statement, as it is used at most once per run, wasting resources if registered.
Reviewed By: skcho
Differential Revision: D23423844
fbshipit-source-id: 07362d19c
Summary: We only added suffix-stripped prefixes of props but this causes FPS if a component declares props that actually contain suffixes since we strip them when we are adding builder calls. The fix is to add both normal and stripped versions.
Reviewed By: skcho, Katalune
Differential Revision: D23375405
fbshipit-source-id: e99cb4dd8
Summary:
This diff finishes the migration from the specialization of methods that take blocks as arguments. Here we delete all the old code and change the way we model dispatch functions so that the tests pass.
- Remove the code for specializing the methods in biabduction.
- Remove the call flags `cf_with_block_parameters` that was only used in this algorithm.
- Removes models for dispatch functions.
- Adds models for dispatch functions as program transformation only in biabduction. To be added in other checkers in the future.
Reviewed By: ngorogiannis
Differential Revision: D23345342
fbshipit-source-id: b5e8542ce
Summary:
This preanalysis in general aims to create specialized clones of methods that have blocks as arguments and that are called with concrete closures, and then call these clone methods instead of the original ones.
One complication is what happens with the captured variables in the closure. What we do is we add them to the formals of the cloned method and passed them through to the concrete blocks.
We do this transformation in two steps:
1. Go through all the callers of methods with blocks as parameters, and create the clone methods. In this preanalysis we only create the attributes for the new method, not the code. We also update the call instructions in the callers to represent a call to the cloned method with updated arguments: we don't need to pass closures arguments anymore, we instead pass the captured variables as new arguments.
2. We add the corresponding code to the newly created clones: this means swapping the call to the block variable with a call to the corresponding block. Moreover, we add some of the new formals (that correspond to the captured variables) to the arguments of the call.
This diff implements step 1 of the analysis. The next diff D23216021 implements step 2.
Reviewed By: ngorogiannis
Differential Revision: D23109204
fbshipit-source-id: 91a5eb16b
Summary: There was a mismatch between formals and actuals in `std::function::operator()` because we were not passing the first argument corresponding to the closure.
Reviewed By: ezgicicek
Differential Revision: D23372104
fbshipit-source-id: d0f9b27d6
Summary: When we evaluate lambdas in pulse, we create a closure object with `fake` fields to store captured variables. However, during the function call we were not linking the captured values from the closure object. We address this missing part here.
Reviewed By: jvillard
Differential Revision: D23316750
fbshipit-source-id: 14751aa58
Summary:
Report errors found by running Topl on top of Pulse, when using
--topl-pulse. Topl tests now run on top of Pulse.
Reviewed By: jvillard
Differential Revision: D23030771
fbshipit-source-id: 8770c2902
Summary:
Two issues are fixed
1. For this diff, when the condition `curr_langauge_is Java` is removed in some part of the analysis, some c bufferoverrun tests are broken. This is fixed in this diff by inspecting if we are dealing with a `Size` alias referring to an `objc_internal_collection_array`.
2. Previously, when we are modifying mutable array in a loop, e.g. adding element to the array or removing element from the array, we are unable to give an estimable size of the array after exiting the loop. This is now fixed, and the corresponding FPs are resolved.
Reviewed By: skcho
Differential Revision: D23342350
fbshipit-source-id: 200f5261c
Summary:
This diff fixes `--reanalyze` option that is to reanalyze specific procedures by removing their
summaries. It was broken because it tried to store an empty summary with `Status.Analyzed`.
Reviewed By: ezgicicek
Differential Revision: D23344633
fbshipit-source-id: 1c4eca6c0
Summary:
The generated code used to contain Prune statements that had boolean
connectives in their conditions. After this commit, all conditions
should have no boolean connective (LNot, LOr, LAnd) at top-level; that
is, prune conditions should be atomic.
The main motivation behind this change is that (a) frontends follow this
convention, and (b) Pulse assumes this convention.
Reviewed By: jvillard
Differential Revision: D23022273
fbshipit-source-id: 1313328e4
Summary:
In the previous diffs, we implement enumerator in order to estimate the cost of for-each loop in ObjC, but when we have FP case when enumerator is used not in for-each loop. For example, the following code has top cost before the fix.
```
void nsarray_enumerator_linear_FP(NSArray* array) {
id obj;
NSInteger sum = 0;
NSEnumerator* enumerator = [array objectEnumerator];
while (obj = [enumerator nextObject]) {
sum += (NSInteger)obj;
}
}
```
Reviewed By: skcho
Differential Revision: D23294895
fbshipit-source-id: 50c7b359f
Summary:
When normalizing discovers new linear arithmetic facts in
`normalize_linear_eqs` we go around once more. Do the same when atoms
become linear equalities.
Reviewed By: skcho
Differential Revision: D23264425
fbshipit-source-id: b355875f3
Summary:
Mostly cosmetic except for a change in [solve_eq] to try harder at
normalization (improves unit tests!). Add more comments and do minor
renamings.
Reviewed By: skcho
Differential Revision: D23243629
fbshipit-source-id: 55bdaf8a8
Summary:
This function had become a bit hard to read and the part about embedded
atoms was not very clear and also a bit incomplete (need to handle "= 1"
and "≠ 1" too).
Reviewed By: skcho
Differential Revision: D23242216
fbshipit-source-id: 239fade97
Summary:
This does a bunch of things at once (sorry):
- Refactor atom/term normalisation so that terms that are really just
atoms become atoms.
- Use this to not bother adding special cases in the functions exported
in the .mli: `and_less_than`, `and_equal_binop`, `prune_binop`, etc.
all had special cases to avoid introducing terms that could be atoms.
That's not great because the same smarts wasn't applied to terms that
would only become atom-like after some normalisation, and led to weird
and duplicated code. Now it's much cleaner: just add the most
straighforward fact and normalise!
- Fix a bug: adding a new equality `x = linear` should *not* be done
using `Normalizer.merge_var_linarith` as this is an internal function
that assumes that `x` is the right representative in `x - linear`.
Instead, for abitrary equations of that form, `solve_eq` should be used.
- When `normalize_linear_eqs` discovers new linear equalities, normalize
again. Add fuel there too to avoid spending too much time doing that.
It could be that we don't need/want fuel there but then we'd need to
think very hard about why there's no infinite recursion possible and
that seems harder.
Reviewed By: skcho
Differential Revision: D23241282
fbshipit-source-id: e5b8c4759
Summary:
This is used for variable substitution and will often be a no-op when
normalising terms over and over again (after the first normalisation,
the expression should stay the same). The equivalent function for terms
was already being careful about not re-allocating identical terms so
extend that care to linear expression.
Reviewed By: skcho
Differential Revision: D23241601
fbshipit-source-id: b365eb87a
Summary:
This allows further normalisation now that terms contain linear
expressions in normal form.
Reviewed By: skcho
Differential Revision: D23241499
fbshipit-source-id: f8e4e759c
Summary:
Linear arithmetic is able to simplify more atoms, eg `x+y <= x+y`
becomes `True` by normalising to "lhs - rhs <= 0". This does the first
step of normalisation, but to get True in this example we also need to
substitute inside atoms according to the linear equalities, which is the
next diff (for now we only substitute variables inside atoms for other
variables or for constants).
Reviewed By: skcho
Differential Revision: D23241457
fbshipit-source-id: 0da0b545c
Summary:
More scaffolding, nothing creates `Linear _` terms yet. Some changes to
variables substitution to allow substituting variables for linear terms
(as well as constants and other variables).
Reviewed By: skcho
Differential Revision: D23241461
fbshipit-source-id: fc870255e
Summary:
This is needed for the rest of the stack that introduces a `Linear of
LinArith.t` variant in `Term.t` to enable more normalisation inside of
terms.
Reviewed By: skcho
Differential Revision: D23241353
fbshipit-source-id: ad765cd13
Summary:
Make term simplification a bit more structured and separate the
"simplification" phase from the "evaluating constant expressions" phase.
Also implement the latter for all possible terms.
Reviewed By: skcho
Differential Revision: D23241334
fbshipit-source-id: 2964aa477
Summary: Not much to see here, extracted to make further changes more readable.
Reviewed By: da319
Differential Revision: D23241335
fbshipit-source-id: 81181f23a
Summary:
`delete` works exactly like `free` so merge both models together. Also
move the `free(0)` test to nullptr.cpp as it seems more appropriate.
Reviewed By: da319
Differential Revision: D23241297
fbshipit-source-id: 20a32ac54
Summary:
Since this is where almost all of the reasoning is concentrated, let's
make sure we use it at every opportunity!
Reviewed By: skcho
Differential Revision: D23194224
fbshipit-source-id: fedb2811e
Summary:
Fix the FP when iterating through constant collection.
facebook
This fix is a hack for now.
Reviewed By: ezgicicek, skcho
Differential Revision: D23241338
fbshipit-source-id: e2e0c05f8
Summary:
As title.
This diff is co-authored by SungKeun Cho and me.
facebook
This diff is co-authored by skcho and me.
Original comments from skcho
"For the record:
1. Rory and I tried to write models for ObjC iterator.
2. We could not use Java's iterator semantics: In Java's, `hasNext` returns the size of collection, rather than a boolean, and which is used as a control variable. On the other hand, in ObjC, it calls only `nextObject`, not calling `hasNext`, and the return value of which is being checked as `null`.
3. We added an artificial field `objc_iterator_offset` to keep the index of the iterator, and the models added in this diff are handling that integer value.
A problem is that `array.objc_iterator_offset` is not included in the control variables, since the condition of the loop is `nextObject() != null` that does not include the iterator offset. We need to make `array.objc_iterator_offset` as a control variable, by changing the part collecting control variables.
"
Reviewed By: ezgicicek, skcho
Differential Revision: D22944278
fbshipit-source-id: 7e71b79c1
Summary:
`Obj.reachable_words` can be very slow on large values, so only call it in debug mode.
Also, measure the time we spend for compressing/storing the global type environment.
Reviewed By: jvillard
Differential Revision: D23264532
fbshipit-source-id: 4a9456ab7
Summary: Use `SqliteUtils.exec` where appropriate, reformat some queries for readability.
Reviewed By: ezgicicek
Differential Revision: D23240945
fbshipit-source-id: 24d921a3a
Summary:
Reset the state before each test so that adding tests doesn't affect
other tests by shifting the ids of their anonymous variables.
Reviewed By: skcho
Differential Revision: D23194171
fbshipit-source-id: 7b717f160
Summary:
Before: 3 modes: (where "lenient" build has warnings not crash the
build, while "strict" build errors on warning):
- opt (default): flambda optimisations + lenient build
- dev (recommand for dev): lenient build, no flambda
- test: strict build (used in tests), no flambda
Now:
- dev (default): *strict* build, no flambda
- opt: lenient build, flambda
- dev-noerror: lenient build, no flambda (use when you want to test
infer but there are build warnings)
The goal is to give faster feedback to infer developers and reduce the
amount of times diffs are sent with build warnings. Also it's now faster
to alternate between changing infer and running unit tests since test
mode is just dev mode.
Reviewed By: ngorogiannis
Differential Revision: D23167416
fbshipit-source-id: d663b6054
Summary: Moving specs to the DB missed out cleaning out all specs when reanalysing. This is the fix.
Reviewed By: jvillard
Differential Revision: D23188958
fbshipit-source-id: 5b50fdda8
Summary:
These are the only ones we need, it turns out the other types (string,
proc names, ...) were dead code. The changes the integer constants to
rational constants, to match the domain of the linear arithmetic engine.
Reviewed By: skcho
Differential Revision: D23164136
fbshipit-source-id: 755c3f526
Summary: In the frontend captured variables for blocks are added as formal parameters in procdesc at the beginning.
Reviewed By: dulmarod
Differential Revision: D23163619
fbshipit-source-id: 2bcbe9b9c
Summary:
There was a syntax error in the comment as `[code]` is interpreted as
code but backticks were used instead. This made `ocamlformat` produce a
warning but no error.
Reviewed By: skcho
Differential Revision: D23167273
fbshipit-source-id: a7fad10d5
Summary:
Instead of alternating between a normal form and a tree structure,
always keep a normal form. Except the normal form is not always fully
normalized. Overall, it's a bit faster than the previous iteration,
while being more precise! In particular, linear arithmetic aims at being
much more complete.
Reviewed By: skcho
Differential Revision: D23134209
fbshipit-source-id: 5f9ec6ece
Summary:
When implementing iterator, we find out that because some semantics of inferbo is Java-specific, we cannot simply use Java's `Collection` model for `NSCollection`.
So this diff writing `NSCollection` model separately.
This diff also extracts the common parts of `NSCollection` and `Collection` into `AbstractCollection` to combine the duplicate the parts.
Reviewed By: ezgicicek
Differential Revision: D22975159
fbshipit-source-id: daed3f99f
Summary:
We already take into account inheritance if the method inherits a known
modelled initializer method (e.g. Activity.onCreate()).
But if the method is explicitly marked as Initializer, we require its
overrides to be also marked.
This diffs fixes the behavior and makes it consistent, now this is
enough to annotate only parent class.
Reviewed By: jvillard
Differential Revision: D23135177
fbshipit-source-id: a21ff4a0e
Summary:
This is part of work aimed to reduce usage of language-agnostics modules
in Java-specific parts of nullsafe.
Reviewed By: ngorogiannis
Differential Revision: D23075333
fbshipit-source-id: 4029732b4
Summary:
This is one of two files in nullsafe that remains interface-less.
Let's fix it!
Reviewed By: jvillard
Differential Revision: D23056324
fbshipit-source-id: a6592f7ae
Summary: Before we were modelling `vector.end()` as returning a fresh pointer every time is was called. It is common to check if an iterator is not the `end()` iterator and proceed to dereference the iterator in that case. In such code pattern `vector.end()` is called twice and returns different fresh values which causes false positives. To fix this, we add a special internal field `__infer_model_backing_array_pointer_to_last_element` to a vector to denote its end. Now, every time we call `vector.end()` we return the value of this field. We introduce a new attribute `EndOfCollection` to mark `end` iterator as the existing `EndIterator` invalidation is not suitable when we need to read the same value multiple times.
Reviewed By: jvillard
Differential Revision: D23101185
fbshipit-source-id: fa8a33b58
Summary:
Constructing the report is done by reading all the summaries, and using certain parts thereof. However, the payloads, which typically account for the greatest size, are not used (with the exception of costs).
This diff splits the storage of summaries into analysis and report summaries, and only reads and deserialises the latter for the report phase. This makes a big difference for runs with a large number of procedures.
Reviewed By: jvillard
Differential Revision: D23105072
fbshipit-source-id: 359067a0f
Summary:
As preparation for splitting summaries into some of their components, and then iterating over only those when reporting (thus gaining performance) we need procnames in the table.
Also, this fixes the now-broken use case of `infer report` with spec files, by using `--procedures-filter` to restrict printing of summaries accordingly.
Reviewed By: skcho
Differential Revision: D23101853
fbshipit-source-id: 1ae878d8e
Summary: Implement specs storage in DB, apart from biabduction models which are still left in specs files.
Reviewed By: skcho
Differential Revision: D22795638
fbshipit-source-id: 140801d3f
Summary: Extra info helps in debugging frontend issues and such.
Reviewed By: ngorogiannis
Differential Revision: D23101854
fbshipit-source-id: 27024675d
Summary:
At the end of analysing a procedure we call `simplify
~keep:vars_live_in_pre_post`. Any variable not in
`vars_live_in_pre_post` is not mentioned anywhere else in the state and
therefore is not going to contribute constraints in callers of the
procedure (in other words: they're dead). We want to also forget
arithmetic facts about these variables as this is a good opportunity to
make the path condition smaller, sometimes by a lot!
The main issue is that dead variables may be useful intermediate terms
in the formula, eg trying to keep only facts about `x` in `y = x + 1 &&
y = 0` is going to lose a lot of precision. But, if a variable not in
`keep` is only mentioned in a simple atom `z = 42` atom, for example,
it's safe to forget about it, eg it's safe to remember only `x=0` in
`x=0 && z=42` (if only `x` is live).
In other words, we can get rid of all atoms containing variables not
transitively involved in other atoms that eventually involve live
variables. A graph problem! This is guaranteed not to forget anything
important and can still trim a lot of atoms in certain situations.
Reviewed By: skcho
Differential Revision: D22921313
fbshipit-source-id: 6d5db7cbe
Summary:
Perhaps a bit overkill to introduce all this extra complexity but it
makes the unit tests much more readable. In fact, this uncovered a bug
in the dead variable elimination!
Reviewed By: dulmarod
Differential Revision: D22925548
fbshipit-source-id: d1f411683
Summary:
Do not always add parens around sub-terms, and add more parens around
terms in atoms and normal forms when they can be confused with the atom
or normal form structure.
Reviewed By: skcho
Differential Revision: D22925549
fbshipit-source-id: 8646e96a5
Summary: These will change to more interesting outputs in the next diff.
Reviewed By: dulmarod
Differential Revision: D22921349
fbshipit-source-id: c58c6240a
Summary:
Add unit tests to pulse in order to write tests for the arithmetic
solver, because it is a pain to write programs to do that end to end.
Reviewed By: ezgicicek
Differential Revision: D22864607
fbshipit-source-id: 0a20a3593
Summary:
This is needed to make dune auto-updating of unit tests introduced in
the next diff cohabit peacefully with our tests to make sure code stays
correctly formatted wrt ocamlformat.
Also, more auto-formatting = better.
Reviewed By: da319
Differential Revision: D22865004
fbshipit-source-id: 91c47ab08
Summary:
Normalization is potentially expensive and its result should be
remembered if the formula keeps being used. In the future we might use
this to make normalization more incremental.
Also rename PathCondition.satisfiable -> is_unsat to match
PulseFormula.is_unsat.
Reviewed By: skcho
Differential Revision: D22728264
fbshipit-source-id: 7759b33ac
Summary:
Now that this is a cheap operation, use it whenever we are checking the
satisfiability of the path condition.
Reviewed By: skcho
Differential Revision: D22724373
fbshipit-source-id: df31c6010
Summary:
Pausing the experiment in favour of new PulseFormula. Can be resurrected
later.
Reviewed By: skcho
Differential Revision: D22576274
fbshipit-source-id: 76529d767
Summary:
This time it's personal.
Roll out pulse's own arithmetic domain to be fast and be able to add
precision as needed. Formulas are precise representations of the path
condition to allow for good inter-procedural precision. Reasoning on
these is somewhat ad-hoc (except for equalities, but even these aren't
quite properly saturated in general), so expect lots of holes.
Skipping dead code in the interest of readability as this (at least
temporarily) doesn't use pudge anymore. This may make a come-back as
pudge has/will have better precision: the proposed implementation of
`PulseFormula` is very cheap so can be used any time we could want to
prune paths (see following commits), but this comes at the price of some
precision. Calling into pudge at reporting time still sounds like a good
idea to reduce false positives due to infeasible paths.
#skipdeadcode
Reviewed By: skcho
Differential Revision: D22576004
fbshipit-source-id: c91793256
Summary:
Current handling of lambdas is quite rudimentary. Looking at test
results we can see that errors are all over the place: False Positives,
False Negatives and just plain wrong results.
These tests can be grouped in 2 sets:
1. Basic support which implies:
- understanding method signatures,
- providing comprehensible error messages.
2. Extended support with implies:
- understanding scoping of values captures in lambdas (needs proper aliasing analysis).
- understanding parametric nullability in generics (needs "some"
support for Generics in our Java frontend).
With follow-up patches I'll attempt to implement "Basic" support for
Lambdas. "Extended" support will be out of scope unless there's
significant demand.
Reviewed By: mityal
Differential Revision: D23058673
fbshipit-source-id: 621551cca
Summary:
Absence of kotlin-annotations led to warnings messages during tests compilation:
```
$ make
warning: unknown enum constant MigrationStatus.STRICT
reason: class file for kotlin.annotations.jvm.MigrationStatus not found
```
This doesn't affect test results but is annoying, hence the fix.
Reviewed By: mityal
Differential Revision: D23051769
fbshipit-source-id: e45fbe7be
Summary:
This is part of work aimed to reduce usage of language-agnostics modules
in Java-specific parts of nullsafe.
As usual, in this diff we don't convert everything and take some
shorthands.
Reviewed By: ngorogiannis
Differential Revision: D23054169
fbshipit-source-id: 70913ddfd
Summary:
Note that the current implementation lists classes and methods (not
<class:method> pairs.
This is bit clowny, but works for now (given the list of classes is small).
So I'll leave it out of the scope of this diff.
Reviewed By: ngorogiannis
Differential Revision: D23076671
fbshipit-source-id: 71c94ebd9
Summary: This diff separates purity analysis and its reporting, since sometimes we want to use the purity analysis results in other checkers, but don't want to report purity issues.
Reviewed By: ezgicicek, jvillard
Differential Revision: D23054913
fbshipit-source-id: 12cc1fc42
Summary: Since there is no discernible downside in using the write daemon unless in single-thread mode or in buck, make it only depend on these circumstances, not a command line flag.
Reviewed By: skcho
Differential Revision: D23004451
fbshipit-source-id: 5c1d06ed1
Summary:
This is part of work aimed to reduce usage of language-agnostics modules
in Java-specific parts of nullsafe.
Reviewed By: artempyanykh
Differential Revision: D23052773
fbshipit-source-id: aacd07f27
Summary:
This is part of work aimed to reduce usage of language-agnostics modules
in Java-specific parts of nullsafe.
Reviewed By: artempyanykh
Differential Revision: D23052339
fbshipit-source-id: 665126957
Summary:
This is part of work aimed to reduce usage of language-agnostics modules
in Java-specific parts of nullsafe.
This diff:
1/ migrates AssignmentRule
2/ passes Procname.Java.t around from the start of analysis.
For now we have places where we have both procname and java procname.
This is fine as we can get rid of it in follow up diffs.
Reviewed By: artempyanykh
Differential Revision: D23052226
fbshipit-source-id: 0125de297
Summary:
This is part of work aimed to reduce number of language-agnostic methods
used in Nullsafe codebase.
Reviewed By: artempyanykh
Differential Revision: D23052328
fbshipit-source-id: 2b69f5f7a
Summary:
This diff adds a false positive test that is introduced imprecise loop
invariant detection.
In the example, `i` and a temp variable `$irvar = get_size(arr)` are
all included in the control variables, so the complexity becomes
quadratic. The problem is that `$irvar` is not addressed as a loop
invariant:
* `is.read` is analyzed as modifying a global
* all return variables, including `$irvar`, of unmodeled functions are invalidated
Reviewed By: ezgicicek
Differential Revision: D23051414
fbshipit-source-id: 011fd086b
Summary: To avoid dead store false positives we skip initialization of a variable that has an `unused` attribute. However, this causes uninitialized value false positives when the variable is later used in macros. To fix this, instead of skipping initialization we record the information about `unused` attribute in local variable data that we can later use for filtering out dead store issues.
Reviewed By: jvillard
Differential Revision: D22868050
fbshipit-source-id: 4a2d0e680
Summary:
In the current implementation, we record 3 states: modelled internally,
modelled intenally, not modelled.
The follow up diffs will need to distinct first- and third- party, given
annotated signature. This diff makes it possible.
Reviewed By: artempyanykh
Differential Revision: D22977962
fbshipit-source-id: b8f3616b5
Summary:
We get duplicated variable declaration instruction for primitive type variable initialized using list initializer, e.g.
```
int* p{nullptr};
```
This happens because we add variable declaration instruction when we translate both `DeclStmt` and `InitListExpr`. To fix this, we do not add the duplicated variable declaration when we translate `InitListExpr`.
Reviewed By: jvillard
Differential Revision: D22844726
fbshipit-source-id: 422806924
Summary:
Synthetic/autogenerated methods/fields usually contain `$` in their names.
Reporting nullability violations on such code doesn't make much sense
since the violations are not actionable for users and likely need to be
resolved on another level.
This diff contributes:
1. Several test cases that involve synthetic code of different
complexity.
2. Code that handles some particular types of errors (but not all!).
Reviewed By: mityal
Differential Revision: D22984578
fbshipit-source-id: d25806209
Summary:
Use `Typ.t` for parameter types in procnames, instead of `JavaSplitName.t`. This allows more precise and usable types stored in procnames, as well as not using the string-based representation of `JavaSplitName` which meant parsing strings whenever one needed a `Typ.t`.
This also makes `JavaSplitName` dead code, so it is removed.
Reviewed By: skcho
Differential Revision: D20500423
fbshipit-source-id: a72728e3f
Summary: Since types from the java frontend are a subtype of `Typ.t` provide the means to check and enforce that for return types in procnames.
Reviewed By: ezgicicek
Differential Revision: D20495527
fbshipit-source-id: b99c784af
Summary:
`java_type` aka `JavaSplitName.t` is a pair of strings. It's used in a procname to store the return type. Replace that with `Typ.t`.
This is step one of deleting `JavaSplitName`. Step two will be to replace parameters with `Typ.t`.
Reviewed By: skcho
Differential Revision: D20323748
fbshipit-source-id: f0029c3ca
Summary:
This diff adds an option `max-jobs` that restrict the number of jobs
running simultaneously.
Reviewed By: ngorogiannis
Differential Revision: D22978328
fbshipit-source-id: 544153c1c
Summary:
Currently, the notion of a third party method signature (corresponding to
a single record in a .sig file) is scattered between unique_repr and
nullability.
Logically, ThirdPartyMethod.t should not "know" about unique_repr
because this is a detail needed only for searching for a method
definition in `.sig` storage.
This diff:
1. Introduces ThirdPartyMethod.t which exposes exactly information
stored in .sig file. We are going to use this abstraction more in follow
up diffs.
2. Moves functionality operating with `unique_repr` to the module
responsible for searching in the repository.
3. Deletes `ThirdPartyMethod.nullability` abstraction - we don't need it as we can just store ThirdPartyMethod.t where was previously `nullability` stored.
4. Introduces `to_canonical_string` method that prints back third party
method in a format needed for `.sig` file, and a test ensuring that
parsing works back and forth consistently. We are going to use this
method in follow up diffs as well.
Reviewed By: artempyanykh
Differential Revision: D22950706
fbshipit-source-id: a0e72ccdb
Summary: As per title. Eases next diffs by making Summary the only source of truth for how spec files are accessed/stored.
Reviewed By: ezgicicek
Differential Revision: D22794742
fbshipit-source-id: 0ee20ec1c
Summary: New, experimental for now, integration with buck on Java using the `#infer-java-capture` flavor.
Reviewed By: artempyanykh
Differential Revision: D22187748
fbshipit-source-id: 62cdafe6b
Summary:
This diff removes a dead field `Struct.subs`, which was used in
heuristics finding methods from sub-classes.
Reviewed By: ezgicicek
Differential Revision: D22945346
fbshipit-source-id: 4b3bf0093
Summary: This diff is on par with this change, with the same motivation
Reviewed By: artempyanykh
Differential Revision: D22924891
fbshipit-source-id: 578ca5869
Summary:
This change will simplify the further refactoring I am doing in follow
up diffs.
Logically, AssignmentRule is about passing actual value to the declared
one, and the proper abstactions for this is exactly AnnotatedNullability
and InferredNullability.
This will also make the client less error prone (no way to call if you
don't have a declaration and actual value to compare).
In the next diff, we will do the same in DereferenceRule.
Reviewed By: artempyanykh
Differential Revision: D22923779
fbshipit-source-id: 5f8f0931c
Summary: Before, `NSCollection` are modelled like array, but this will have issue when we want to say add object to array. This diff changes `NSCollection`'s model to use Java's Collection model.
Reviewed By: ezgicicek
Differential Revision: D22840079
fbshipit-source-id: b944b743b
Summary:
In Cost/Inferbo checkers, it tried to find a subclass with heuristics when a method of interface or
abstract class is called. While it makes preciser analysis results in general, sometimes introduced
tricky FPs since the behavior of the heuristics depends on targets. This diff revert the heuristics
to suppress the FPs.
Reviewed By: ngorogiannis
Differential Revision: D22924485
fbshipit-source-id: 9f151231f
Summary: Implement `alloc` and implement initialisation method that uses the return value of `alloc`, i.e. `NSString.init`.
Reviewed By: ezgicicek
Differential Revision: D22840080
fbshipit-source-id: 47a7523e3
Summary:
This diff translates for-in block in objc as a simple for-loop. For example,
`for (item_type item in items) { body }` is translated to
```
NSEnumerator *enumerator = [items objectEnumerator];
item_type item;
while (item = [enumerator nextObject]) { body }
```
Reviewed By: ezgicicek
Differential Revision: D22841524
fbshipit-source-id: 296ee84df
Summary:
Capture of certain Kotlin files fails at the javalib level (probably,
some unanticipated bytecode pattern). We however can't just completely
skip Kotlin class-files during capture as those have NotNull/Nullable
annotations on methods/params that are important for Java <- Kotlin
interop (using Kt classes from Java).
Instead we can skip translation of concrete methods from Kotlin classes
while retaining method signatures with annots in the TEnv.
Reviewed By: ngorogiannis
Differential Revision: D22897638
fbshipit-source-id: 67909aa43
Summary:
There are two ways to suppress it.
1. Field level suppression annotation (was already tested). This will
apply to all constructors.
2. Constructor level annotation (this is what this test does). Sometimes
there are "fake" constructors that are not intended to be called in
prod, they might leave some fields not initialized.
Note that there are two ways to add a suppression; one has a known
problem that is documented here.
Reviewed By: artempyanykh
Differential Revision: D22864869
fbshipit-source-id: f95aaa26a
Summary: `alloc` actually allocates the array, not the `init`. Let's reflect that in our models.
Reviewed By: roro47
Differential Revision: D22864198
fbshipit-source-id: 687f9f247
Summary:
It's typically used inside another ~fold argument and it gets too
verbose.
Reviewed By: da319
Differential Revision: D22846501
fbshipit-source-id: 2fdd4271f
Summary: `Array.copyOf` model has nothing to do with Collections. Refactor it to the appropriate place
Reviewed By: roro47
Differential Revision: D22844638
fbshipit-source-id: 48dde4d53
Summary:
When expressions use generics or typecasts, CFG contains intermediate `_fun_cast` nodes which break some nullsafe heuristics and lead to false positives.
This affects different types of checks (null-check on assignment expressions, `map.containsKey` checks in assignment expressions, regular typecasts, etc.
See added tests for examples.
Reviewed By: mityal
Differential Revision: D22815631
fbshipit-source-id: 80d444b1c
Summary:
We check for supertypes in Java. Why not ObjC?
Would be good to get dulmarod's input here.
Reviewed By: roro47
Differential Revision: D22817126
fbshipit-source-id: 52c1c3f3c
Summary: This diff adds an option to shard spec files in `infer-out/specs`. For some big analysis targets, there can be too many of spec files in the one directory, which slows down IO speed for reading the spec files.
Reviewed By: jvillard
Differential Revision: D20002128
fbshipit-source-id: bd7722883
Summary: There used to be `JoinAfter n` mode where we would try to join `n` states instead of always making disjunctions. It got deleted in D14258485 and Pulse's underlying (pre-disjuncts) domain doesn't even have a join operation. `NeverJoin` mode is not useful in Pulse anymore: pulse will diverge or OOM if we don't limit the number of disjuncts. It is also not used by any other analyzer. Let's remove it.
Reviewed By: jvillard
Differential Revision: D22817425
fbshipit-source-id: 1e658f11d
Summary: This diff refactors Java specific `PatternMatch` functions into its own module. When `PatternMatch.ml` was originally created, it was mainly for Java but now it also supports ObjC. Let's refactor it to reflect the Java/ObjC separation: move all functions that operate on Java procnames into Java submodule.
Reviewed By: jvillard
Differential Revision: D22816504
fbshipit-source-id: ff6b64b29
Summary:
This avoids wasting potentially large amount of work in some
pathological situations. Suppose `foo()` has D specs/disjuncts in its
Pulse summary, and consider a node that calls `foo()` N times, starting
with just one disjunct:
```
[x]
foo()
[x1, ..., xD]
foo()
[y1, ..., yD^2]
foo()
...
```
At the end we get `D^N` disjuncts. Except, currently (before this diff),
we prune the number of disjuncts to the limit L at each step, so really
what happens is that we (very) quickly reach the L limit, then perform
`L*D` work at each step (where we take "apply one pre/post pair to the
current state" to be one unit of work), thus doing `O(L*D*n)` amount of
work.
Instead, this diff counts how many disjuncts we get after each
instruction is executed, and we already reched the limit L then doesn't
bother accumulating more disjuncts (as they'd get discarded any way),
and crucially also doesn't bother executing the current instruction on
these extra disjuncts. This means we only do `O(L*n)` work now, which is
exactly how we expect pulse to scale: execute each instruction (in
loop-free code) at most L times.
This helps with new arithmetic domains that are more expensive and
exhibit huge slowdowns without this diff but no slowdown with this diff
(at least on a few examples).
Reviewed By: skcho
Differential Revision: D22815241
fbshipit-source-id: ce9928e7c
Summary:
The old --topl-only is now --topl-biabd-only, and there's also
--topl-pulse-only. This is WIP: the latter runs pulse, but it doesn't yet
extract Topl errors from pulse summaries. (The citv part of pulse path
conditions appears to have the necessary information.)
Reviewed By: jvillard
Differential Revision: D22815250
fbshipit-source-id: a01792945
Summary:
This diff:
1. Adds general capability to model any field as nullable /
non-nullable.
2. Uses it for Boolean.TRUE and Boolean.FALSE
Reviewed By: artempyanykh
Differential Revision: D22794226
fbshipit-source-id: 95f586592
Summary: D17500386 had added the ability to give symbolic values on functions returning exceptions. However, this might cause FPs or cryptic complexity reports (especially with subclass heuristics). This diff aims to revert it back.
Reviewed By: skcho
Differential Revision: D22764266
fbshipit-source-id: 1615544d8
Summary: We model internal builtin `__new` function to return a non-null value. This fixes nullptr_dereference false positives where we explicitly check the result of a function call for nullptr when the function returns a newly created object.
Reviewed By: jvillard
Differential Revision: D22772217
fbshipit-source-id: 37d209697
Summary:
This stopped compiling on my Debian and it seems hard to fix. It was
already having compilation issues between osx and Linux but here I don't
know how to detect which type it wants since the OS is Linux too.
Reviewed By: ezgicicek
Differential Revision: D22728282
fbshipit-source-id: 818ae87e6
Summary:
This step does extra normalization so it's useful to see what's going on
when debugging. Log stuff in the html debug of the exit node.
Reviewed By: da319
Differential Revision: D22596248
fbshipit-source-id: cde3bbb6c
Summary:
Pulse has models for iterators that make them use a fake field to
remember the element of the collection they point to. But, not all
methods are modelled, and some of them look at the real field, eg
`operator==`. Since we don't update the real field in the model, this
causes imprecision.
The imprecision was visible in pudge.
Reviewed By: skcho
Differential Revision: D22576003
fbshipit-source-id: 2af6be646
Summary:
The java frontend used an unsound flow insensitive class analysis to devirtualize
some virtual calls. We remove it and let the recent devirtualizer preanalysis do the job.
This unsoudness in the Java frontend may have been here for a long time. Removing it may
modify several analysis results (specially Nullsafe) where virtual calls may look different
now.
Reviewed By: jvillard
Differential Revision: D22662739
fbshipit-source-id: c45296dce
Summary:
Changing the order of the superclasses of a struct exposes a bug in both biabduction and the devirtualiser where a method would be resolved into a still virtual method (an interface method).
The reason is that we don't check whether a super class is an interface before exploring it, and seemingly we assume that there is only one (first) superclass worth exploring. This also ignores multiple inheritance in C++.
To fix this, refactor the resolution to a complete search (not just the first super class!) which ignores Java interface methods. Also moved it to `Tenv` so that both biabduction and the devirtualiser can use it.
Reviewed By: jvillard
Differential Revision: D22357488
fbshipit-source-id: 54b96c1f4
Summary: We recently changed the translation of NSArray literals in a way that we pass a different type of argument to `arrayWithObjects:count`, such that the biabduction model doesn't work anymore. So we remove the model for now.
Reviewed By: skcho
Differential Revision: D22691611
fbshipit-source-id: 03cd940ed
Summary:
Merging global type environments for Java needs some form of non-trivial type definition merging because:
- The frontend is likely non-deterministic, so it can capture the same type differently.
- There are classes that appear with two distinct definitions (usually ordered by inclusion) when one is produced by an ABI-like compilation process (so only public fields/methods would appear for example), and one full version.
- The frontend produces dummy versions (empty definitions), and full ones.
- The location information is variously missing/present.
This diff tries to strike a balance between a full semantic merge (which depends on the frontend/buck integration) and the current code which "merges" by clobbering old definitions with new ones.
One side-effect of this diff is that code cannot expect a special order for supers.
Reviewed By: jvillard
Differential Revision: D22630286
fbshipit-source-id: fc66c7000
Summary:
This diff adds translation of `arrayWithObjects:count:`. In the previous implementation it was
translated as if it was `arrayWithObjects:`, but their function parameters are different.
In this diff, it translates an array literal `NSArray* a = @ [ 2, 3 ];` to
```
n$1=NSNumber.numberWithInt:(2:int)
n$2=NSNumber.numberWithInt:(3:int)
temp[0]:objc_object*=n$1
temp[1]:objc_object*=n$2
n$3=NSArray.arrayWithObjects:count:(temp:objc_object* const [2*8],2:int)
a:NSArray*=n$3
```
where `temp` is an additional local variable declared as array.
See,
https://developer.apple.com/documentation/foundation/nsarray/1460145-arraywithobjectshttps://developer.apple.com/documentation/foundation/nsarray/1460096-arraywithobjects?language=objc
Reviewed By: jvillard
Differential Revision: D22631305
fbshipit-source-id: 5be0a55d4
Summary:
Add a test to the repo to try and detect perf regressions in pulse.
Currently analyzed in ~0.1s. With `--pudge`, takes ~10s.
Sledge does eager normalization and canonicalization when incorporating new facts into formula contexts and the algorithm is polynomial in the number of equalities. This example generates one equality per location in the array => boom. This bypasses the recency model of arrays because the formula needs to be constructed before it can be simplified to get rid of dead variables.
The new arithmetic is not as complete as sledge's algorithm but linear in time. We could use it to simplify the formula *before* passing it to sledge. In fact, that was the original motivation.
Reviewed By: skcho
Differential Revision: D22574366
fbshipit-source-id: e9044ae09
Summary:
When applying function summaries, we are careful not to violate the
summary's assumptions about non-aliasing. For example, the summary we
generate for `foo(x,y) { *x = *y; }` will have `x` and `y` be allocated
to two different `AbstractValue.t` in the heap, representing
disjointness.
However, the current logic is too coarse and also rejects passing the
same pure value to functions that made no assumption about them being
equal or different, eg `goo(int x,int y) { int z = x + y; }`. This is
because the corresponding `AbstractValue.t` are different in the
callee's summary, but are represented by only one same value in callers
such as `goo(i,i)`.
This diff restricts the "don't violate aliasing" condition to only
consider heap-allocated values. This is consistent with separation logic
by the way: we use the implication `x|->- * y|->- |- x≠y`, which is
valid only when both `x` and `y` are both allocated in the heap as in
the left-hand-side of `|-`.
Reviewed By: skcho
Differential Revision: D22574297
fbshipit-source-id: 206a18499
Summary:
This will allow all the analyses to be able to call closures without any special treatment: we transform the call to variables that point to closures into normal function calls. We treat only ObjC blocks at the moment, with C++ lambdas to be done as a next step.
We aimed to achieve certain results in Pulse (see tests: avoid memory leaks and NPEs FPs) while also keeping the biabduction analysis working as before.
We also checked that for the examples analyzed Pulse behaves like the correct semantics of ObjC programs with blocks.
Reviewed By: jvillard
Differential Revision: D22547333
fbshipit-source-id: efe56ed51
Summary: Lambda is called using `operator()`. We need to know the information of captured variables when `operator()` procedure is being analysed. This diff records lambda captured variables in `operator()` procdesc. The complication arises from the fact that procdesc for `operator()` is created before translating lambda expression or during the translation of lambda expression where captured variables are translated. To solve this issue, we update existing `operator()` procdesc attributes with captured variable information when we translate lambda expression.
Reviewed By: jvillard
Differential Revision: D22374495
fbshipit-source-id: 44909adea
Summary:
This diff fixes a bug that eval_arr misses the case when a stack
variable points to an array.
Reviewed By: ezgicicek, roro47
Differential Revision: D22596999
fbshipit-source-id: 7c4a13d01
Summary: Add cost model for most common `NSString` functions in cost analysis
Reviewed By: skcho
Differential Revision: D22433005
fbshipit-source-id: 2f57bbda9
Summary: If a node is unreachable and the cost of the node is Top, we were giving Top cost :( Let's fix it.
Reviewed By: skcho
Differential Revision: D22548269
fbshipit-source-id: d79743669
Summary:
We update the type of captured variables to include information about capture mode (`ByReference` or `ByValue`) both for procdesc attributes and the closure expression.
For lambda: closure expression now contains correct capture mode for capture variables. Procdesc still does not contain information about captured variables which we will address in the next diff.
For objc blocks: at the moment all captured variables have mode `ByReference`. Added TODOs to fix this.
Reviewed By: jvillard
Differential Revision: D22572054
fbshipit-source-id: 4c88678ee
Summary: This diff prints where the cost becomes top by calling `html_debug_new_node_session`. This will print them in the start node of the procedure in html. There are already printing functions in `get_instr_node_cost_record`.
Reviewed By: ezgicicek
Differential Revision: D22547578
fbshipit-source-id: 257e957c0
Summary:
The frontend was hackily adding protocols as superclasses in the tenv, with the implicit encoding that the first element in the list was the actual superclass. This was clearly very fragile.
Protocols are not used in the backend at the moment, so for now we will remove them from the list of superclasses to have more consistency in the tenv.
Reviewed By: ngorogiannis
Differential Revision: D22525078
fbshipit-source-id: 2aef1fab1
Summary: This diff extends the value domain to express multiple markers.
Reviewed By: ngorogiannis
Differential Revision: D22524864
fbshipit-source-id: b8e4af2eb
Summary:
As title
Model `NSString` as `JavaString`.
Since `NSArray` does not contain information about its type of element, we do not use associate string with collection as in Java and C++. In Java, String model is implemented using java collection, and for C++, string model is implemented using vector.
So instead, we use existing `JavaString` model.
Reviewed By: skcho
Differential Revision: D22431949
fbshipit-source-id: 7cdde1ad7
Summary:
In order to allow implementations of the single Fol interface using
multiple backend first-order logic solvers, add explicit definitions
of terms and formulas in the Fol module, and implement Context in
terms of them.
The Fol interface supports freely mixing Terms and Formulas, in
particular there is `Term.ite : cnd:Formula.t -> thn:Term.t ->
els:Term.t -> Term.t` which allows Formulas to appear in Terms. The
Fol implementation performs enough normalization to enable using an
internal representation of terms that is strictly partitioned into
"theory terms" and "formulas", which are stratified below "conditional
terms" and then below "general terms". This partitioning and
stratification enables using backend solvers that do not support
mixing formulas in terms.
Reviewed By: jvillard
Differential Revision: D22170506
fbshipit-source-id: a014ee7d7
Summary: To avoid NULLPTR_DEREFERENCE false positives we want to model some functions as returning non-null. A new flag --pulse-model-return-nonnull allows us to provide a list of such functions.
Reviewed By: ezgicicek
Differential Revision: D22431564
fbshipit-source-id: 9944c7382
Summary: Make the module interface safe wrt closing the classpath channel when done, plus reducing the exposed API.
Reviewed By: skcho
Differential Revision: D22411685
fbshipit-source-id: 11316c577
Summary: `addAll` adds elements one by one and hence takes linear time. We didn't have a model for this and considered it O(1).
Reviewed By: skcho
Differential Revision: D22375157
fbshipit-source-id: 65b82bfae
Summary: This diff prevents printing line numbers of loop in the trace description, which helps to keep the same descriptions even when the line number of a function is changed in tests.
Reviewed By: ezgicicek
Differential Revision: D22375584
fbshipit-source-id: 676d1a7cc
Summary:
This one is observed to be more memory efficient. Intuitively, maps need
to be re-allocated more often than lists for balancing. In pulse, we'll
often only ever add new values, in increasing order (when they are fresh
variables created as we symbolically execute the program), which pushes
maps into their worst-case allocation pattern. At least I suspect that's
what happens. With lists, this case is handled much better as lists are
not re-allocated when adding elements.
This is somewhat confirmed by benchmarking and observing GC stats.
Reviewed By: skcho
Differential Revision: D22140908
fbshipit-source-id: 29815112f
Summary:
Messed up the aggregation of GC stats in the previous commit.
It's cleaner to have GC stats (and analysis time) outside of
BackendStats as the rules for computing them is different than the rest,
eg notice how "analysis time" needed to be corrected at the end of the
run, and similarly for GC stats. Thus, refactor this part.
Also output different aggregations of GC stats: +/max/average.
Reviewed By: skcho
Differential Revision: D22332496
fbshipit-source-id: eefd9dd72
Summary:
Keyword `thread_local` in cpp allows us to create a variable with thread storage duration, meaning that the object's lifetime begins when the thread begins and ends when the thread ends.
We get `NULLPTR_DEREFERENCE` false positive for `thread_local` variable since we reallocate it in the `VariableLifetimeBegins` metadata instruction and we do not see further updates to the variable. To solve the issue we special case `VariableLifetimeBegins` instruction for global variables.
Reviewed By: jvillard
Differential Revision: D22284135
fbshipit-source-id: 13c14ef90
Summary: Create test for the most common unmodeled function in inferbo that acts as control variable.
Reviewed By: skcho
Differential Revision: D22331168
fbshipit-source-id: 1913682db
Summary: Add objc test for customized class and blocks. Mostly sanity test.
Reviewed By: ezgicicek
Differential Revision: D22043918
fbshipit-source-id: 917deeea7
Summary:
This diff adds a model of `File.listFiles` as returning an array with
a symbolic length.
Reviewed By: ezgicicek
Differential Revision: D22332258
fbshipit-source-id: 6ca593b8b
Summary: This diff adds support for `com.facebook.litho.sections.Section` which mimics the behavior for `com.facebook.litho.Component`.
Reviewed By: skcho
Differential Revision: D22309039
fbshipit-source-id: 3510441a8
Summary:
Following from previous diff.
**Idea** - 80% of functions with Top cost are caused by calling top-costed callees, i.e. callee's Top cost is simply propagated to its transitive callers, so the aim is to investigate such root callees along with the number of their transitive callers.
Consider the following code
```
void bar1() {
// top cost function
}
void bar2() {
// another top cost function
}
void baz(){
// baz have top cost because of bar
bar1();
}
void foo() {
// goo have top cost because of baz
baz();
bar2()
}
```
Clearly, the root cause of the foo being top cost is `bar1` and `bar2`.
1. When we are analyzing `baz`, we know that it calls `bar1`, which is top cost, so we record that `baz = { T, bar1 } `.
2. Now, say we are analyzing foo.
When we analyze the call to `baz`, we found out that the top cost of `baz` is caused by `bar1`, so we record `foo = { T, bar1 }`.
When we analyze the call to `bar2`, we know that `bar2` is top cost, but since at this stage we only want to deal with the first top cost function we met, so we ignore it.
Since we are keeping track of top cost function by examining the `Call` instruction, we would expect to see two log of `bar1` in the result. The test plan confirms it.
Reviewed By: ezgicicek
Differential Revision: D22231457
fbshipit-source-id: 45d48e4a7
Summary:
New `debug` command takes over from `explore` the `--procedures`, `--source-files` functionality and adds `--global-tenv` for printing the global type environment.
Also, uncrustify printing of type environments.
Reviewed By: jvillard
Differential Revision: D22284807
fbshipit-source-id: 9c6fb0c7a
Summary:
Log stats obtained via `Gc.stat ()` for various phases:
- capture (doesn't include child infer processes created by the build
system)
- analysis
- worker processes of the analysis, aggregated
- reporting phase
- total GC stats for the main infer process
Reviewed By: jberdine
Differential Revision: D22140131
fbshipit-source-id: b0ee39559
Summary:
We already had a heuristic to deal with assignment expressions, but it
relied on the very previous CFG node to have a non-empty list of instrs.
In some cases, however, this previous node is a Join_node with no instrs,
so we need to take one more step back to find what we're looking for.
I've also added a bit more logging around this functionality, so it's
easier to debug/tune in future.
Reviewed By: ngorogiannis
Differential Revision: D22282930
fbshipit-source-id: 024eec145
Summary:
This model is very important in the analysis of ObjC classes because the pattern
```
- (instancetype)init {
if (self = [super init]) {
...
}
return self;
}
```
is very common, so we need to know that if the super class is `NSObject`, the implementation of `init` is returning `self`, otherwise it's a skip function and we don't get the correct spec for the function. We fix some memory leak FP with this model, see test.
Reviewed By: ezgicicek
Differential Revision: D22259281
fbshipit-source-id: 3ee48c827
Summary:
We need to check if `folly::Optional` is not `folly::none` if we want to retrieve the value, otherwise a runtime exception is thrown:
```
folly::Optional<int> foo{folly::none};
return foo.value(); // bad
```
```
folly::Optional<int> foo{folly::none};
if (foo) {
return foo.value(); // ok
}
```
This diff adds a new issue type that reports if we try to access `folly::Optional` value when it is known to be `folly::none`.
Reviewed By: ezgicicek
Differential Revision: D22053352
fbshipit-source-id: 32cb00a99
Summary: This linters were not used much anymore, so we can delete them.
Reviewed By: ngorogiannis
Differential Revision: D22233895
fbshipit-source-id: f31180a05
Summary: There is now a compilation check for UNAVAILABLE_API_IN_SUPPORTED_IOS_SDK so this check is less useful. Also the check REGISTERED_OBSERVER_BEING_DEALLOCATED is useful only in an old version of iOS.
Reviewed By: ngorogiannis
Differential Revision: D22231851
fbshipit-source-id: 72151fef5
Summary:
Extend BasicCost to BasicCostWithReason which contains a record of the form
```{cost: BasicCost.t; proc_name_list: Procname.t list}```
This is done so that we can keep track of top cost function.
So the idea is that 80% of functions with Top cost are caused by calling top-costed callees, i.e. callee's Top cost is simply propagated to its transitive callers, so the aim is to investigate such root callees along with the number of their transitive callers.
Therefore, we create an extension that match `cost` to the root cause function.
This diff only handles the extension. Details about how we update the root cause function is in the next diff.
Reviewed By: skcho
Differential Revision: D22158717
fbshipit-source-id: 6498d904f
Summary:
This diff tries to support a specific form of linked list iteration in Java.
```
while (p != null) {
p = p.getNext();
}
```
This example was a constant cost before because the cost checker could not detect that it is an iteration on a linked list.
The heuristic this diff implemented is:
(1) `p = p.getNext()`: It tries to find this specific form of assignment. Then, it increments `p.linked_list_index` by 1. Note that `linked_list_index` is a virtual field for keeping an index in the linked list. Its initial value is always 0.
(2) At `p != null`, it tries to prune the value of `p.linked_list_index`: the upper-bound of `p.linked_list_index` is pruned by `<= p.linked_list_length`. Here again, `p.linked_list_length` is also a virtual field to denote the length of the linked list.
Reviewed By: ezgicicek
Differential Revision: D22234892
fbshipit-source-id: 2fee176bb
Summary: Log unmodeled function in cost analysis and send result to scuba.
Reviewed By: ezgicicek
Differential Revision: D22158510
fbshipit-source-id: c6eade67e
Summary: This continues on the previous diff by removing the model for `__bridge_transfer` in biabduction. This also had the name __free_cf which we kept for compatibility with biabduction until now but that we can now change.
Reviewed By: ezgicicek
Differential Revision: D22207396
fbshipit-source-id: 7a175eca6
Summary: These models for Memory Leaks have been ported to Pulse, so we can remove the models in biabduction and corresponding tests.
Reviewed By: skcho
Differential Revision: D22206287
fbshipit-source-id: e17499ad3
Summary:
Move the implementation of implicit getters and setters from the biabduction to the clang frontend so these methods are accessible to all the checkers.
*Background*: In Objective-C when properties are created in the interface of a class, the compiler creates automatically the instance variable for it and also the getter and setter in the implementation of the class. In the frontend we collect the information about which method is the implicit getter and setter of which instance variable (we get the method declaration but not the implementation), and here we add the implicit implementation.
Reviewed By: skcho
Differential Revision: D22187238
fbshipit-source-id: 76e0508ed
Summary: Let's make package name match the directory name to follow Java's file lookup conventions
Reviewed By: skcho
Differential Revision: D22183964
fbshipit-source-id: b9958b975
Summary:
Document FP due to imprecision in tracking outer lock release. In a nested `synchronized` block the outer release is not registered by the abstract domain. The reason is that HIL is not resolving what `$bcvarX` is pointing to (in this case to `lockE`).
Reported by Andreea Costea.
Reviewed By: ezgicicek
Differential Revision: D22186240
fbshipit-source-id: 84e5e72b1
Summary:
There is a lot of subtlety in our parsing of buck targets on the command line, that is then just thrown away. Push this one level up, getting rid of the special case where in Clang mode if we only have "normal" targets we don't resolve them.
Also introduce a proper variant for buck target types.
Reviewed By: skcho
Differential Revision: D22160490
fbshipit-source-id: 500c1b12c
Summary:
This diff revises assignment semantics, so it can store/load from the
heap location.
Reviewed By: ezgicicek
Differential Revision: D22042823
fbshipit-source-id: 20d91bfc5
Summary:
Nullability of the assignment result is not refined in code snippets
like:
```
while ((a = foo.getA()) != null) {
nonNullableVal = a;
}
```
Let's add a test for this.
Reviewed By: jvillard
Differential Revision: D22136218
fbshipit-source-id: 206c368d6
Summary:
Better API for creating issue types:
- distinguish hidden/normal/dynamic issue types
- normal issue types should always be documented
- add "TODO" to missing documentation
- dynamic issue types are the only ones that can be created outside of
IssueType.ml
I had to document the new CCBM and the resource leak lab exercise to
keep Help.ml happy, did `make doc-publish`.
Reviewed By: ngorogiannis
Differential Revision: D22118766
fbshipit-source-id: 3d0194518
Sungkeun Cho
Nikos Gorogiannis
Ezgi Çiçek
Josh Berdine
Mitya Lyubarskiy
Jules Villard
Qianyi Shu
Daiva Naudziuniene
Dulma Churchill
Radu Grigore
Artem Pianykh
David Pichardie
GaloisNeko