Summary:
If both the library and binary are named `sledge`, then compilation
works fine and resolves the names correctly, but merlin gets confused
and cannot find the sledge library modules used in the bin sources. So
the binary and library need different names. The name of the library
gets exposed to clients, while the name of the binary only determines
the name of some files in the _build directory, which can be renamed
as desired. Therefore, use the `sledge` name for the library module,
and rename the binary module to `sledge_cli`, but still have dune
install it as `sledge.exe`.
Reviewed By: jvillard
Differential Revision: D20589431
fbshipit-source-id: 14b65907d
Summary:
Integer `div` and `rem` are a pair of functions that satisfy the
division rule, where the result of `div` is truncated toward zero:
```
| Div (** Division, for integers result is truncated toward zero *)
| Rem
(** Remainder of division, satisfies [a = b * div a b + rem a b] and
for integers [rem a b] has same sign as [a], and [|rem a b| < |b|] *)
```
Reviewed By: jvillard
Differential Revision: D20584626
fbshipit-source-id: fa02a3a98
Summary:
This diff adds wrappers for Equality entry points that augment
exceptions escaping out of Equality with an sexp that can be given
back to Equality.replay in order to reexecute the function call that
failed.
A (bogus) example could be raising:
```
((Failure "domains intersect: ((u8) %x_5)")
(And_eq () (Ap1 (Unsigned (bits 8)) (Var (id 5) (name x)))
(Var (id 6) (name y))
((xs ()) (sat true)
(rep (((Var (id 6) (name y)) (Var (id 5) (name x))))))))
```
and then calling `Equality.replay {|(And_eq ...)|}`.
Reviewed By: jvillard
Differential Revision: D20583753
fbshipit-source-id: 80d855950
Summary:
It is more convenient, and harder to misunderstand, if the verbose
tracing setting comes commented-out after the default non-verbose
setting.
Reviewed By: jvillard
Differential Revision: D20583755
fbshipit-source-id: 06ecb0e9a
Summary:
Work on the containers revealed that 1b8746d21 was premature, and this
diff is in part a revert of that. The objectives for the global
namespace are:
- self-consistent as much as possible
- rich data type operations
- does not require maintaining lots of tedious library wrapping code
- has Marshalable containers
- has containers with functorial interfaces
For these aims, it's best to stick with Core. Base isn't enough to
define functorial interfaces for collections (without a lot of tedious
wrapping code to keep in sync manually), and since a few modules not
in Core_kernel are needed anyhow.
Reviewed By: ngorogiannis
Differential Revision: D20583756
fbshipit-source-id: d939be7d0
Summary:
This diff defines Map as a functorover the underlying implementation
of Core.Map. This results in map values that are just trees, with no
comparison function closures, and with the same interface (almost) and
underlying data structure implementation as Core.Map.
Reviewed By: ngorogiannis
Differential Revision: D20583758
fbshipit-source-id: 5a4997b51
Summary:
This diff defines Set as a functorover the underlying implementation
of Core.Set. This results in set values that are just trees, with no
comparison function closures, and with the same interface (almost) and
underlying data structure implementation as Core.Set.
Reviewed By: ngorogiannis
Differential Revision: D20583754
fbshipit-source-id: 79aa7477a
Summary:
This is likely not the final refinement, rather one step forward.
We classify all classes by 3 categories:
- Nullsafe and 0 issues
- can add Nullsafe and will be 0 issues
- the rest (class needs improvement)
Each class will fall into exactly one category.
Error messaging is WIP, they are not intended to be surfaced to the user
just yet.
Note how this diff uses the result of the previous refactoring.
Reviewed By: artempyanykh
Differential Revision: D20512999
fbshipit-source-id: 7f462d29d
Summary: Add a flag `is-inclusive-cost` (`true` by default) which computes inclusive cost for each function. Setting the flag to `false` computes exclusive cost of the function where the cost of the callees are assumed to be `0`.
Reviewed By: skcho
Differential Revision: D20558275
fbshipit-source-id: 6b5798916
Summary:
This function is used to adapt the callee summary at a call site. It did two things for every domain element in the callee summary:
- A linear search through the list of actuals.
- For each such actual, it would (repeatedly) compute its ownership (!).
For large summaries this can be substantial. The right way is to precompute the ownership for all actuals once and then simply retrieve it (via an array).
Reviewed By: jberdine
Differential Revision: D20564447
fbshipit-source-id: 1ca3121c2
Summary: The attribute types present are exclusive, so sets are not needed for the attribute map domain. This changes `Attribute` to a flat domain and removes the set on top of that.
Reviewed By: jberdine
Differential Revision: D20560240
fbshipit-source-id: 83e59d73e
Summary:
Both modules define properties the analysis maps to addresses, there is no reason to have two modules for this.
Also remove an instance of `Caml.Not_found` usage.
Reviewed By: jberdine
Differential Revision: D20558683
fbshipit-source-id: eacafd780
Summary:
# Problem
Consider
```
some_method(Object a) { a.deref(); }
```
What is nullability of `a` when we dereference it?
Logically, things like "LocallyCheckedNonnull" etc are not applicable
here.
This would be applicable if we called some_method() outside! But not
inside. Inside the function, it can freely treat params as non-null, as
long they are declared as non-nullable.
The best we can capture it is via StrictNonnull nullability.
Reviewed By: artempyanykh
Differential Revision: D20536586
fbshipit-source-id: 5c2ba7f0d
Summary:
# Problem
Yes, nullsafe is not null-safe, such an irony.
ErrorRenderingUtils overuses `option` and `let+` constructions. Most of
internal functions can return `None` when "something is wrong".
On top of this, "default" pattern match is overused either.
Because of this, `ErrorRenderingUtils.mk_nullsafe_special_issue` returns
optional type. In practice, this result can be None for many unclear
reasons, and it is super tricky to even understand them all.
This in turn forced AssignmentRule and DereferenceRule to process this
None is defensive way. The rules have some theory why None was returned,
and have assertions along the way.
Turns out those theories might be wrong. This diff will make triaging wrong assumptions easier.
Reviewed By: artempyanykh
Differential Revision: D20535720
fbshipit-source-id: 2b81e25b7
Summary: When we have clashing args to bug (for instance -j and -Xbuck --num-threads) CLI passed -Xbuck args should win.
Reviewed By: jvillard
Differential Revision: D20557060
fbshipit-source-id: 726fc501a
Summary:
`make test` failed in some test directories, because we were getting warnings
```
Foo.java uses unchecked or unsafe operations.
```
This diff fixes or suppresses these warnings.
Reviewed By: skcho
Differential Revision: D20557572
fbshipit-source-id: 63ecd3dfa
Summary:
First version of a new memory leak check based on Pulse. The idea is to examine unreachable cells in the heap and check that the "Allocated" attribute is available but the "Invalid CFree" isn't. This is done when we remove variables from the state.
Currently it only works for malloc, we can extend it to other allocation functions later.
Reviewed By: jvillard
Differential Revision: D20444097
fbshipit-source-id: 33b6b25a2
Summary:
- Add more naive pulse models for:
- `System.arraycopy`
- `StringBuilder.setLength`
- `StringBuilder.delete`
- Model the following as pure
- `SparseArrayCompat.valueAt`
- `File.get...`
- Add a nice test
Reviewed By: jvillard
Differential Revision: D20513397
fbshipit-source-id: 6d412d13a
Summary:
Manuals were previously built as part of `make test`, but `test` takes
too long so `make manuals` is a convenient replacement.
Reviewed By: ngorogiannis
Differential Revision: D20517145
fbshipit-source-id: 404c9921f
Summary:
Bumps [acorn](https://github.com/acornjs/acorn) from 6.4.0 to 6.4.1.
<details>
<summary>Commits</summary>
<ul>
<li><a href="9a2e9b6678"><code>9a2e9b6</code></a> Mark version 6.4.1</li>
<li><a href="90a9548ea0"><code>90a9548</code></a> More rigorously check surrogate pairs in regexp validator</li>
<li>See full diff in <a href="https://github.com/acornjs/acorn/compare/6.4.0...6.4.1">compare view</a></li>
</ul>
</details>
<br />
[](https://help.github.com/articles/configuring-automated-security-fixes)
Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting `dependabot rebase`.
[//]: # (dependabot-automerge-start)
[//]: # (dependabot-automerge-end)
---
<details>
<summary>Dependabot commands and options</summary>
<br />
You can trigger Dependabot actions by commenting on this PR:
- `dependabot rebase` will rebase this PR
- `dependabot recreate` will recreate this PR, overwriting any edits that have been made to it
- `dependabot merge` will merge this PR after your CI passes on it
- `dependabot squash and merge` will squash and merge this PR after your CI passes on it
- `dependabot cancel merge` will cancel a previously requested merge and block automerging
- `dependabot reopen` will reopen this PR if it is closed
- `dependabot close` will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually
- `dependabot ignore this major version` will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
- `dependabot ignore this minor version` will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
- `dependabot ignore this dependency` will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)
- `dependabot use these labels` will set the current labels as the default for future PRs for this repo and language
- `dependabot use these reviewers` will set the current reviewers as the default for future PRs for this repo and language
- `dependabot use these assignees` will set the current assignees as the default for future PRs for this repo and language
- `dependabot use this milestone` will set the current milestone as the default for future PRs for this repo and language
You can disable automated security fix PRs for this repo from the [Security Alerts page](https://github.com/facebook/infer/network/alerts).
</details>
Pull Request resolved: https://github.com/facebook/infer/pull/1238
Reviewed By: dulmarod
Differential Revision: D20513549
Pulled By: jvillard
fbshipit-source-id: 92cc20052
Summary:
`to_reportable_violation` is responsible for identifying if the
violation is reportable in this mode or not.
This logic is higly coupled with other functions in
`ReportableViolation`, such as `get_description`: You can not have
sensible description on the violation that is NOT reportable in a given
mode.
So from logical perpsective, creation of `ReportableViolation.t` should
belong to this module itself, not to the parent `Rule` module.
This change will make design clearer.
Reviewed By: artempyanykh
Differential Revision: D20511756
fbshipit-source-id: ef27b5057
Summary:
- Rename to `combine_adjacent` for clarity
- Reimplement without needing to filter out a dummy value, by keeping
track of the numer of adjacent pairs that have been combined
together
- Use this counting to replace the probably-confusing lazy copy with
explicit eager copy at the right time
- Remove the now-unneeded dummy value argument
Reviewed By: jvillard
Differential Revision: D20482752
fbshipit-source-id: db80bbbe3
Summary:
This diff finishes work in D20491716.
We removed dependency on nullsafe mode for field initialization in
D20491716, so this diff just formalizes it.
Reviewed By: jvillard
Differential Revision: D20493164
fbshipit-source-id: 6ac612e78
Summary:
This diff continues work in D20491716.
This time for Inheritance Rule.
Reviewed By: jvillard
Differential Revision: D20492889
fbshipit-source-id: c4dfd95c3
Summary:
This diff continues work in D20491716.
This time for Dereference Rule.
Reviewed By: jvillard
Differential Revision: D20492296
fbshipit-source-id: ff7f824f9
Summary:
# Problem
In current design, Rules (assignment rule, dereference rule, inheritance
rule) decide, depending on the mode, wether the issue is legit or not.
If the issue is not actionable for the given mode, it won't be created
and registered.
For meta-issues, we want to be able to do smart things like:
- Identify if we can raise strictness of the mode without
introducing new issues
- Classify classes on "clean" vs "broken", taking into account issues
that are currently invisible.
# Solution
In the new design:
1. Rules are issuing violations independently of mode. This makes sense
semantically. Mode is "level of trust we have for suspicious things",
but the thing does not cease to be suspicious in any mode.
2. Each Rule decides if it is reportable or not in a given mode.
3. `nullsafe_mode` is passed to the function `register_error`, that 1)
adds error so it can be recorded in summary for file-level analysis
phase 2) reports some of them to the user.
# This diff
This diff converts only AssignmentRule, follow up will include
conversion of other rules, so no issue encapsutes the mode.
Reviewed By: jvillard
Differential Revision: D20491716
fbshipit-source-id: af17dd66d
Summary:
`make deadcode` is failing on master but our CI jobs didn't catch it :(
Let's fix existing deadcode for now.
Reviewed By: martintrojer
Differential Revision: D20510062
fbshipit-source-id: 4a5e5f849
Summary:
Previously, at each function call, we added a `WrittenTo` attribute for applying the address of the actuals. However, this results in mistakenly considering each function application that inspects its argument as impure. Instead, we should only propagate `WrittenTo` if the actuals have already `WrittenTo` attributes.
For instance, for the following functions
```
public static boolean is_null(Byte a) {
return a == null;
}
public static boolean call_is_null(Byte a) {
return is_null(a);
}
```
We used to get the following pulse summary for `call_is_null` (showing only one of the disjuncts):
```
#0: PRE:
{ roots={ &a=v1 };
mem ={ v1 -> { * -> v2 } };
attrs={ v1 -> { MustBeValid },
v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };}
POST:
{ roots={ &a=v1, &return=v8 };
mem ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } };
attrs={ v2 -> { Arith =null,
BoItv ([max(0, v2), min(0, v2)]),
WrittenTo-----------WRONG },
v4 -> { Arith =1,
BoItv (1),
Invalid ConstantDereference(is the constant 1),
WrittenTo-----------WRONG },
v8 -> { WrittenTo } };}
SKIPPED_CALLS: { }
```
where we mistakenly recorded a `WrittenTo` for `v2` (what `a` points to). As a result, we considered `call_is_null` as impure :( This diff fixes that since the callee `is_null` doesn't have any `WrittenTo` attributes for its parameter `a`. So, we don't propagate `WrittenTo` and get the following summary
```
#0: PRE:
{ roots={ &a=v1 };
mem ={ v1 -> { * -> v2 } };
attrs={ v1 -> { MustBeValid },
v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) } };}
POST:
{ roots={ &a=v1, &return=v8 };
mem ={ v1 -> { * -> v2 }, v8 -> { * -> v4 } };
attrs={ v2 -> { Arith =null, BoItv ([max(0, v2), min(0, v2)]) },
v4 -> { Arith =1,
BoItv (1),
Invalid ConstantDereference(is the constant 1) },
v8 -> { WrittenTo } };}
SKIPPED_CALLS: { }
```
Reviewed By: skcho
Differential Revision: D20490102
fbshipit-source-id: 253d8ef64
Summary:
Make all arguments named and move function from `Procname.Java` to `Procname`, and making it return a `Procname.t` as opposed to `Procname.Java.t` (all callers want a `Procname` eventually).
Various other small fixes in the callers.
Reviewed By: skcho
Differential Revision: D20492305
fbshipit-source-id: e646cc799
Summary:
`dune build fmt` applies to all contexts, but we only need one, so
use `dune build @_build/dbg/fmt` instead. Also swallow stderr as it's
useless with `--auto-promote`.
Reviewed By: ngorogiannis
Differential Revision: D20482767
fbshipit-source-id: a7642f65d
Summary:
The term "vector" evokes expectations of being automatically growable,
and these are just immutable arrays.
Reviewed By: ngorogiannis
Differential Revision: D20482762
fbshipit-source-id: 0cd2c9c23
Josh Berdine
Nikos Gorogiannis
Mitya Lyubarskiy
Ezgi Çiçek
Martin Trojer
Jules Villard
Dulma Churchill
Artem Pianykh
Amar1729
dependabot[bot]