Summary:
This does several things because it was hard to split it more:
1. Split most of the arithmetic reasoning to PulseArithmetic.ml. This
doesn't need to be reviewed thoroughly because an upcoming diff
changes the domain from just `EqualTo of Const.t` to an interval domain!
2. When going through a prune node intra-procedurally, abduce arithmetic
facts to the pre (instead of just propagating them). This is the "assume
as assert" trick used by biabduction 1.0 too and allows to propagate
arithmetic constraints to callers.
3. Use 2 when applying summaries by pruning specs whose preconditions
have un-satisfiable arithmetic constraints.
This changes one of the tests! Pulse now does a bit more work to find
the false positive, as can be seen in the longer trace.
Reviewed By: skcho
Differential Revision: D18117160
fbshipit-source-id: af3b2c8c0
Summary:
Instead of checking that each address in the pre that must be valid is
not invalid in the caller (and error out if it turns out it is invalid)
as we discover them, save these checks for after we are sure that the
precondition can be applied. It is in fact a bug that we can report an
error when trying to apply a precondition that is actually not
satisfiable in the current state for other reasons than lifetime issues.
We still want to skip calls in case of weird issues like mismatch in
number of formals vs actuals.
This will have more obvious effects later when we also check that
arithmetic facts in preconditions are satisfied at the call site: if a
pre mandates "x=1" and "y must be valid" and we have "x=0" and "y
invalid" then we shouldn't report an error.
Reviewed By: skcho
Differential Revision: D18115229
fbshipit-source-id: ad4ce72ff
Summary:
If a precondition cannot be applied, it means that this program path
somehow doesn't make sense for the caller and so should be pruned. Right
now we just treat this as skipping over the call instead.
This will become more important when specs start mentioning arithmetic
facts that must be satisfied at the call site. As it is we will only
stop if we discover aliasing in the pre not present at the call site or
vice versa.
Reviewed By: dulmarod
Differential Revision: D18115230
fbshipit-source-id: 4f1c7a583
Summary: The way `<=` is used in `AbstractDomain` prevents infix use and forces bracketing it everywhere. Replace with simple `leq`.
Reviewed By: jvillard
Differential Revision: D18201854
fbshipit-source-id: 8175224e4
Summary:
Add a new interval abstract domain. This domain uses the APRON
numerical analysis library to keep track of the range of values held
by llair variables where possible. This works by translating LLAIR
expressions into APRON tree expressions, so only handles the
subset of the LLAIR expression language that can be embedded.
Note also that function summarization is not yet implemented.
Future commits will add summarization and improve coverage of
LLAIR's expression language.
Reviewed By: jberdine
Differential Revision: D17763517
fbshipit-source-id: 826ce4cc5
Summary: Abstract state tracks stuff that is not needed for summaries, wasting space/time.
Reviewed By: jvillard
Differential Revision: D18171499
fbshipit-source-id: 25483ced9
Summary:
Primitive types are not annotated. Because of that, we used to implicitly derive
`DeclaredNonnull` type for them. This worked fine, but this leads to errors in Strict mode, which does
not believe DeclaredNonnull type.
Now lets offifically teach nullsafe that primitive types are
non-nullable.
Reviewed By: jvillard
Differential Revision: D18114623
fbshipit-source-id: 227217931
Summary:
This diff adds SafeInvertedMap, which is similar to InvertedMap but it
guarantees that there is no top elements in the tree of the map.
Reviewed By: ezgicicek
Differential Revision: D18062174
fbshipit-source-id: 2fbc51f31
Summary: `Str.regexp_string` should be used to find a method name instead of `Str.regexp`.
Reviewed By: ezgicicek
Differential Revision: D18136598
fbshipit-source-id: c4b56dd64
Summary:
The reporting phase would go through the critical pairs in the summary roughly three times, once for each major type of warning (starvation, lockless violation, deadlock). This is wasteful, and also led to some code duplication. Fix.
Also, use the more efficient annotation matcher in `ConcurrencyModels` and move some model matchers to `StarvationModels`.
Reviewed By: artempyanykh
Differential Revision: D18118149
fbshipit-source-id: ff4dc3d07
Summary: It is now possible to push the thread status into each critical pair. This leads to higher precision, because when code branches on whether it is on the UI thread, the final abstract state of the procedure will be `AnyThread`, but pairs created in the UI thread branch should know that their status is `UIThread`, not `AnyThread`.
Reviewed By: jvillard
Differential Revision: D18114273
fbshipit-source-id: cbb99b46f
Summary: This will be more useful later when adding another one.
Reviewed By: ezgicicek, jberdine
Differential Revision: D18115231
fbshipit-source-id: a0a01901a
Summary:
The business of translating `Top/True/False` to `true/false` can be
hidden more.
Reviewed By: skcho
Differential Revision: D18115228
fbshipit-source-id: 071fcbddf
Summary:
Warning 33 (unused open) is enabled but the module open is not really
unused, it's just also opened at the top of the file...
Reviewed By: skcho
Differential Revision: D18114385
fbshipit-source-id: 2a8f9512a
Summary:
This diff avoids making top values on unknown non-static function,
such as abstract function, calls. This is necessary because the
generated top values ruin the precision of the cost checker.
Reviewed By: ezgicicek
Differential Revision: D17418611
fbshipit-source-id: aeb759bdd
Summary:
The wrong function was used when we tried to see if the class is
annotated with NullsafeStrict. This made it work only for non-static
methods.
Now we use the proper way.
Reviewed By: ngorogiannis
Differential Revision: D18113848
fbshipit-source-id: 02b7555be
Summary:
Previously, we considered a function which modifies its parameters to be impure even though it might not be modifying the underlying value. This resulted in FPs like the following program in Java:
```
void fresh_pure(int[] a) {
a = new int[1];
}
```
Similarly, in C++, we considered the following program as impure because it was writing to `s`:
```
Simple* reassign_pure(Simple* s) {
s = new Simple{2};
return s;
}
```
This diff fixes that issue by starting the check for address equivalnce in pre-post not directly from the addresses of the stack variables, but from the addresses pointed to by these stack variables. That means, we only consider things to be impure if the actual values pointed by the parameters change.
Reviewed By: skcho
Differential Revision: D18113846
fbshipit-source-id: 3d7c712f3
Summary:
Add some theorems establishing the correspondence between the
implementation of the Convert operation in OCaml and the definition of
Convert in the semantics. Essentially, the OCaml version is in terms of
extracting certain ranges of bits, whereas the semantics is in terms of
integer arithmetic (addition, modulus, and exponentiation)
Reviewed By: jberdine
Differential Revision: D18113878
fbshipit-source-id: c318596d0
Summary:
This commit adds truncation, sign extension and zero extension to LLVM
and the Convert instruction to LLAIR.
The LLVM instructions use HOL's build-in word/int and word/num
conversions. Sanity-checking theorems prove that zero-extending leaves
the value of the word unchanged when considered as an unsigned value,
and that sign-extending leaves the value unchanged when considered as a
signed value.
The llair semantics for Convert uses the truncate_2comp function which
converts an integer to another integer as though they were represented
in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp
255 8 = -1, truncate_2comp -3 2 = 1
Reviewed By: jberdine
Differential Revision: D18058833
fbshipit-source-id: df9de480c
Summary:
The old syntactic invariant in prog_ok was in the wrong direction,
saying that all labels in a phi instruction have to exist, rather than
saying that when we jump to a new block, the label of the block we came
from must be in all of the phi instructions.
Reviewed By: jberdine
Differential Revision: D18058832
fbshipit-source-id: d2ad33b04
Summary:
This required some minor tweaks to how the semantics encode values into
and out of byte lists. The remaining problems have to do with how LLVM
globals are translated into llair. At the moment, llair semantic's state
keeps a mapping for globals to their addresses, following the LLVM
semantics. However, it is not used because the translation (following
the code in frontend.ml) translates LLVM globals into llair locals,
which the llair semantics isn't set up to handle.
Reviewed By: jberdine
Differential Revision: D17930787
fbshipit-source-id: 06c6368e0
Summary: As suggested by artempyanykh, this will make it bit more clear
Reviewed By: artempyanykh
Differential Revision: D18037204
fbshipit-source-id: 65cb96815
Summary: We stop tracking at builder boundaries. Let's tract create methods as well so that trace is more informative.
Reviewed By: skcho
Differential Revision: D18038637
fbshipit-source-id: a99b6431f
Summary:
Although, we have Makefile and BUCK build def, this is a maven project
which is supposed to be released to Maven Central, so it's worth
having a short instruction on how to build it with maven.
Reviewed By: mityal
Differential Revision: D18037109
fbshipit-source-id: 6aebf4384
Summary: Adding support to matching block names. We match mangled block names. We also needed to extend the function for extracting the range for each method, to also traverse the stmts to be able to find the block declarations.
Reviewed By: skcho
Differential Revision: D17956931
fbshipit-source-id: 707908812
Summary:
We support only class level annotations for now. We will add more when
we support more.
Reviewed By: artempyanykh
Differential Revision: D18036213
fbshipit-source-id: 44791318e
Summary:
This is the first take on strict mode semantics.
The main invariant of strict mode is the following:
If the function passes `NullsafeStrict` check and its return value is
NOT annotated as Nullable, then the function does not indeed return
nulls, subject to unsoundness issues (which should either be fixed, or
should rarely happen in practice).
This invariant helps the caller in two ways:
1. Dangerous usages of non strict functions are visible, so the caller is enforced to check them (via assertions or conditions), or strictify them.
2. When the function is strict, the caller does not need to worry about
being defensive.
Biggest known issues so far:
1. Condition redundant and over-annotated warnings don't fully
respect strict mode, and this leads to stupid false positives. (There is
so much more stupid false positives in condition redundant anyway, so
not particularly a big deal for now).
2. Error reporting is not specific to mode. (E.g. we don't distinct real nullables and non-trusted non-nulls, which can be misleading). To be
improved as a follow up.
Reviewed By: artempyanykh
Differential Revision: D17978166
fbshipit-source-id: d6146ad71
Summary:
This is an intermediate nullability type powering future Strict mode.
See the next diff.
Reviewed By: artempyanykh
Differential Revision: D17977909
fbshipit-source-id: 2d5ab66d4
Summary:
Currently, we have NullsafeRules.ml responsible for detecting the
violation fact. All other logic: what should be the error type,
severity, and error message, is in TypeErr.ml.
In this diff, we move logic from NullsafeRules.ml and TypeErr.ml to
dedicated modules like AssignmentRule.ml etc.
Each such module is responsible for:
- detecting the violation fact (this is moved from NullsafeRules.ml)
- rendering the violation error (this is moved from TypeErr.ml).
This approach makes sense for two reasons:
1. The violation fact and the way we show error are logically related to
each other.
2. In future diffs, we will support more features guiding rule behavior,
such as a) decision whether to hide or show the error depending on type
information and mode; b) the way we render error depending on type
information and role.
Having dedicated modules incapsulating knowledge about rules is a natural way to support 2.
Reviewed By: artempyanykh
Differential Revision: D17977891
fbshipit-source-id: a53d916d3
Summary:
1. For each Nullsafe Rule, lets have a dedicated IssueType.
2. Split error reporting to three subfunctions: description, field type,
and infer issue.
This allows to introduce additional capabilities in a consolidated
manner. Example of such capabilities is should we hide or show an error,
what should be error severity depending on strictness mode, and how
exactly the error should be reported depending on how exactly
nullability is violated.
Reviewed By: artempyanykh
Differential Revision: D17977887
fbshipit-source-id: 860d67d2f
Summary:
This function can return `None` if the result is equal to the first
argument of join (why first?). It is unclear if it was an optimization
attempt of over-complicated logic.
Reviewed By: artempyanykh
Differential Revision: D17876561
fbshipit-source-id: 9628fb86e
Summary:
The goal of this logic is unclear:
1/ See the comments
2/ I can not see the scenario where classes and proper types can be
joined in a legit Java program
3/ Even it if was the case, I don't see how this heuristic is justified.
So I assume it is not.
Reviewed By: artempyanykh
Differential Revision: D17876568
fbshipit-source-id: c9c6cd604
Summary:
It is unclear what is the purpose of doing so, and it adds complexity to
codebase.
1/ The semantics of this is not clear, it more or less corresponds to
"where are all original locations that contributed to the type
calculation", but many branches in CFG have nothing to do with
nullability; also it was used not always consistently.
2/ The only place where this was used is logs, so this is no-ops. It is
unclear how seeing all locations can help debugging, given 3/ - see
below
3/ We have the right place to store such informatin, namely TypeOrigin,
where we store locations associated with types where we merge them in
CFG. Currently, we store only "winner" - the most relevant locations
that contributed to nullability in the most informative way. We show
this to the user when we report an error.
4/ If we want to support more things (e.g. show something more to the user), TypeOrigin
seems to be the right place. Or, alternatively, we might still merge
locations in `range`, but this will be better to organize in a tree form
instead of flat list that is not really informative and helpful. It is
all speculative though since need to support things like that seems
unclear.
Reviewed By: artempyanykh
Differential Revision: D17857198
fbshipit-source-id: 6cf6e48a2
Summary:
That module's interface was repeated twice to avoid exposing its
internals to PulseDomain itself. It's also quite long so it makes sense
to move it to its own file.
Reviewed By: ezgicicek
Differential Revision: D17977209
fbshipit-source-id: 56a2dac24
Summary:
Another poorman's library, this time about Pulse Domains. Also renames
`PulseDomain` to `PulseBaseDomain`.
Reviewed By: ezgicicek
Differential Revision: D17955287
fbshipit-source-id: 9c947cf98
Summary:
The name had rotten: it should be `AddrHistPair`. There is little value
of exposing the type of the pair `AbstractValue.t * ValueHistory.t`,
just inline its definition everywhere.
Reviewed By: ezgicicek
Differential Revision: D17955283
fbshipit-source-id: d145251e0
Summary:
See explanations in D17955104.
This renames `AbstractAddress` to `AbstractValue` since they are not
necessarily addresses.
Reviewed By: ezgicicek
Differential Revision: D17955290
fbshipit-source-id: 8bb4c61f2
Summary:
See explanations in D17955104. I put Attributes inside PulseAttribute
instead of creating a new file to avoid exposing more internals about
ranks.
Reviewed By: ezgicicek
Differential Revision: D17955284
fbshipit-source-id: a8719a58f
Jules Villard
Martin Trojer
Nikos Gorogiannis
Benno Stein
Mitya Lyubarskiy
Sungkeun Cho
Dulma Churchill
Ezgi Çiçek
Scott Owens
Artem Pianykh