Summary: Some more tests to make sure we consider the size of tuples when pattern matching.
Reviewed By: mmarescotti
Differential Revision: D30132889
fbshipit-source-id: 74ae4d1a1
Summary: Report `badrecord` errors with Pulse when trying to access or update a record with a wrong name.
Reviewed By: rgrig
Differential Revision: D30068424
fbshipit-source-id: b88abb7ca
Summary:
Add support for Erlang records, including:
- Parsing record definitions, storing info in environment
- Record index expressions and patterns
- Record creation expression, including initializers
- Record update expressions and patterns
- Record field access expressions
- Pulse models
The key idea is to translate records to tagged tuples (just as Erlang does under the hood), but this requires some bookkeeping to figure out which field maps to which tuple element.
Reviewed By: rgrig
Differential Revision: D29991819
fbshipit-source-id: a1c713b41
Summary: Nil insertion into collection tests are not c++ specific, so also moving them into objc folder.
Reviewed By: skcho
Differential Revision: D30013858
fbshipit-source-id: d103a69ef
Summary: Add support for tuples, including expressions, pattern matching and pulse models. Tuples are modeled similarly to `Cons` (lists): they have a dynamic type (including the size of the tuple) and elements as fields.
Reviewed By: mmarescotti
Differential Revision: D29875650
fbshipit-source-id: f0262a42c
Summary: Add some tests for lists: nil, cons, and some basic pattern matching. We can extend this suite later with more features on lists (e.g. concatenation).
Reviewed By: skcho
Differential Revision: D29844279
fbshipit-source-id: 62c8b92c3
Summary: Add support for the xor operator by reducing `(X xor Y)` to `(X and not Y) or (not X and Y)`. Alternatively, `(X != Y)` could have been used but that might not be safe since SIL models Booleans with integers.
Reviewed By: skcho
Differential Revision: D29816793
fbshipit-source-id: 2496b718b
Summary: Add support for short circuit counterparts (andalso, orelse) of the logic operators (and, or).
Reviewed By: skcho
Differential Revision: D29815177
fbshipit-source-id: 98d28deed
Summary: Pulse evaluated (e1+e2) as a new value that is a sum of evaluation results of e1 and e2. However, when e2 is known as zero, we can have a simpler evaluation result without introducing the new value. This diff returns the evaluation result of e1 when e2 is known as zero.
Reviewed By: ngorogiannis
Differential Revision: D29736444
fbshipit-source-id: d5ce5a60e
Summary: Previously we just reported NONEXHAUSTIVE_PATTERN_MATCH, which was (1) not correct because not only patterns can cause nonexhaustive behavior, but also guards, and (2) the Erlang runtime reports errors more precisely, indicating whether the nonexhaustive behavior occurs with `if`, `case`, functions or match expressions.
Reviewed By: rgrig
Differential Revision: D29681637
fbshipit-source-id: 74a25b371
Summary:
This fixes a bug that caused imprecise tracking of dynamic types.
Suppose we knew
term_eqs:
(x instanceof T)=v1
(y instanceof T)=v2
0=v2
attrs:
x has DynamicType T
y has DynamicType T
The simplification used to produce
term_eqs:
1=v1
0=v2
That's because term_eqs is a map and 1 can appear at most once as a key.
Note that the missing fact (1=v2) contradicts (0=v2). The imprecision
came from not noticing such contradictions. Most of these imprecisions
were observed in Erlang tests.
The fix is to go from using Term.VarMap to the smarter functions in
PulseFormula.Normalizer.
Reviewed By: jvillard
Differential Revision: D29541209
fbshipit-source-id: e4e077c87
Summary: Add support for guards, both in function clauses and case clauses.
Reviewed By: rgrig
Differential Revision: D29634937
fbshipit-source-id: 5a9f8ec2d
Summary: Add support for *unary minus* and *logical not* in the Erlang translation, both as expression (e.g., `X = -Y`) and pattern (e.g., `case X of -3 -> ...`).
Reviewed By: rgrig
Differential Revision: D29582176
fbshipit-source-id: 17ef89496
Summary: Group tests based on the different constructs: functions, case expressions and match expressions.
Reviewed By: rgrig
Differential Revision: D29559982
fbshipit-source-id: eb645ed8d
Summary: Add some tests for binary expressions. The idea is that tests come in pairs: in both cases we do the same calculations, one is asserting the good result and one is not, where only the latter should trigger a warning.
Reviewed By: rgrig
Differential Revision: D29556364
fbshipit-source-id: 5b601d141
Summary:
This way we don't rely on existing summaries already having a
MustBeValid for self and on them having possibly other conditions that
might prevent a report.
Reviewed By: skcho
Differential Revision: D29550321
fbshipit-source-id: b9822fcd4
Summary: Add some test cases to potentially non-exhaustive case clauses.
Reviewed By: rgrig
Differential Revision: D29555525
fbshipit-source-id: f710e93e6
Summary: If a test function `F` has multiple calls to a possibly problematic function `G`, our current expected output does not tell exactly which call to `G` causes the problem. This diff splits up such functions `F` into smaller parts `F1`, `F2`, ..., so that each part only calls `G` once. This way our expected output can match more precisely.
Reviewed By: rgrig
Differential Revision: D29554848
fbshipit-source-id: bdc62731c
Summary:
Topl matches procedure names against whatever Procname.hashable_name
returns. For Java, it returns something like "java.util.ArrayList.add(...)",
but for Erlang it used to return something like "add/1": no module and
no parenthesis after. Now, Erlang returns "lists:add/1"; that is, it
includes module name. Also, Topl doesn't insist anymore on having a
paranthesis after the name.
Differential Revision: D29520365
fbshipit-source-id: d23be1cc8
Summary:
The gist of this diff is a set of Pulse models for the built-ins
that have been put in Sil by the Erlang frontend:
- __erlang_make_nil, for creating an empty list like []
- __erlang_make_cons, for creating a nonempty list like [1|[]]
- __erlang_pattern_fail, which marks that no pattern matched
The models for the first two update the abstract state. The model for
the third generates a reportable error.
The diff also includes a test.
And also a few bugfixes:
- a type ErlangAny was used sometimes instead of ErlangAny*
- a load that was meant to be n=13 was instead n=*13;
changed to (*tmp=13; n=*tmp)
- the Makefile's guard for the rebar build-system test was inside the large
guard for java analyzers; of course, we don't need java to run rebar
Reviewed By: jvillard
Differential Revision: D29230161
fbshipit-source-id: c8fd6d88a
Summary: Adding constraint `self > 0` after computing specs for Objective-C instance methods were causing false positives of the heuristics not to discard `self=0 /\ self|->-` (added new test testAnotherObjectUseSelfOk was FP). This diff adds constrain `self > 0` before computing Objective-C specs, discarding unsatisfiable `self > 0 /\ self =0`.
Reviewed By: skcho
Differential Revision: D29462462
fbshipit-source-id: 088ee447e
Summary: Useful to write other tests, and also probably worth modelling.
Reviewed By: ezgicicek
Differential Revision: D29232545
fbshipit-source-id: ecb24f6f7
Summary:
Investigations into the number of disjuncts we get in summaries
revealed that we sometimes blow past the limit. Rework the code to make
sure that does not happen.
We can probably raise the disjunct limit as a result, more experiments
needed.
Reviewed By: ezgicicek
Differential Revision: D29229249
fbshipit-source-id: 4a06594fa
Summary:
There are two changes:
1/ Fix incorrect merge of two cases (empty and not-empty)
```
let<*> astate_equal_zero = ... in
let<*> astate_not_zero = ... in
[Ok (ContinueProgram astate_equal_zero); Ok (ContinueProgram astate_not_zero)]
```
This was an incorrect merge, because if there is an error in the former
case `astate_equal_zero`, it doesn't even evaluate the latter case
`astate_not_zero`.
2/ Cover all cases precisely. There are actually three cases to cover:
* `TextUtils.is_empty(null) = true`
* `TextUtils.is_empty("") = true`
* `TextUtils.is_empty("abc") = false`
However, in the previous model, it missed the second case.
Reviewed By: jvillard
Differential Revision: D29393579
fbshipit-source-id: e59d9a60d
Summary:
This diff adds some semantic models for C++ string length. It introduces
an virtual field for string length and use the value in the models.
* basic_string constructor given a constant string
* string.empty
* string.length
Reviewed By: jvillard
Differential Revision: D29390815
fbshipit-source-id: 99d67e48e
Summary:
`Initializer` is used (mostly by Nullsafe) to signal that a method will only be run from/as a constructor, even if public.
RacerD should recognise this annotation; this diff makes RacerD treat methods annotated as `Initializer` like constructors with regards to the ownership of the receiver object.
Reviewed By: skcho
Differential Revision: D28748068
fbshipit-source-id: 5dd060865
Summary:
Some funky C++ way of calling the parent's constructor triggers a
function in the frontend that used to reverse the order of parameters.
Reviewed By: skcho
Differential Revision: D28832500
fbshipit-source-id: 1032de2ca
Summary:
Unknown functions may create false positives as well as false negatives
for Pulse. Let's consider that unknown functions behave "functionally",
or at least that a functional behaviour is a possible behaviour for
them: when called with the same parameter values, they should return the
same value.
This is implemented purely in the arithmetic domain by recording
`v_return = f_unknown(v1, v2, ..., vN)` for each call to unknown
functions `f_unknown` with values `v1`, `v2`, ..., `vN` (and return
`v_return`). The hope is that this will create more false negatives than
false positives, as several FPs have been observed on real code that
would be suppressed with this heuristic.
The other effect this has on reports is to record hypotheses made on the
return values of unknown functions into the "pruned" part of formulas,
which inhibits reporting on paths whose feasibility depends on the
return value of unknown functions (by making these issues latent
instead). This should allow us to control the amount of FPs until we
model more functions.
Reviewed By: skcho
Differential Revision: D27798275
fbshipit-source-id: d31cfb8b6
Summary: Same as MustBeValid: we want to report the first error on the path.
Reviewed By: skcho
Differential Revision: D28674724
fbshipit-source-id: a2ac04b5b
Summary:
Add a new `PathContext.t` component to the abstract state. For now it
tracks only the current "timestamp" of symbolic execution inside the
procedure, i.e. which step of symbolic execution we are in (bumped by 1
each time we've executed one instruction). In the future this will also
hold, eg, which conditionals we've been through on the path (for
reporting traces with that information).
Most of the diff is about propagating the path context through many of
the APIs.
We use timestamps only in `MustBeValid` attributes to report the first
incorrect access in a function call for now.
Reviewed By: skcho
Differential Revision: D28674726
fbshipit-source-id: 2cd825e73
Summary:
It's better to remember the first reason why an address must be valid,
etc.
Reviewed By: skcho
Differential Revision: D28674729
fbshipit-source-id: 3b69de7ef
markma
Akos Hajdu
Daiva Naudziuniene
Sungkeun Cho
Radu Grigore
Loc Le
Jules Villard
Nikos Gorogiannis