Summary:
In the sequential analysis there is no control-flow within a basic
block. This changes in the concurrent analyis as context switches can
occur within basic blocks. To support this, this diff adds a notion of
"instruction pointer" to Llair and adjusts Control to use it to
iterate blocks.
Differential Revision: D29441164
fbshipit-source-id: b9c977545
Summary:
The width of joins in the concurrency analysis is much wider, making
it worthwhile to use an n-ary version of join in order to avoid
repeated formula simplifiaction.
Differential Revision: D29441154
fbshipit-source-id: ae17de37b
Summary:
Memoize the translation from program registers to logical
variables. Currently this is not significant, but is semantically
necessary for the concurrency analysis.
Differential Revision: D29441162
fbshipit-source-id: ff674c4c3
Summary:
The output generated for `pp_raw` was incorrectly less raw for
disjuncts than for their parent formulas.
Differential Revision: D29441156
fbshipit-source-id: 3e4b42fe3
Summary:
The initializers of globals are constant expressions, and therefore
contain no registers. This change adds an assertion to make this
existing invariant explicit.
Differential Revision: D29441160
fbshipit-source-id: 4da4e74d1
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:
This allows easily defining lexicographic orders as a composition of
other orders. For example, the natural ordering on `int * string`
pairs can be written:
```
Ord.Infix.((Int.compare >|= fst) @? (String.compare >|= snd))
```
The `@?` name is chosen as a hybrid between `@@` which denotes
function composition and `<?>` which is the infix operator of
`Containers.Ord` for defining lexicographic orders.
Differential Revision: D29441161
fbshipit-source-id: ae9143cdc
Summary: Adding more logging for cases where we see a lock/unlock but we see no arguments.
Reviewed By: skcho
Differential Revision: D29427413
fbshipit-source-id: 58b76b865
Summary: Add support for translating binary expressions, and implement a few operators.
Reviewed By: rgrig
Differential Revision: D29452471
fbshipit-source-id: d7c25ae91
Summary: Extract helper methods related to block creation into a module.
Reviewed By: rgrig
Differential Revision: D29436139
fbshipit-source-id: 92f9466d3
Summary: Add support for translating case expressions (without guards yet) and integer literals (including in patterns). Note that we use the same infrastructure for case expressions and function clauses, so adding support for guards will only have to be implemented once.
Reviewed By: rgrig
Differential Revision: D29424141
fbshipit-source-id: 0d6f1e661
Summary: Flag defaults to false. (For now, only the buck integration supports capturing any Kotlin.)
Reviewed By: jvillard
Differential Revision: D29388274
fbshipit-source-id: 8dbec9555
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: Refactor Erlang expression translation. Previously expressions were translated to a list of instructions to be put in the single node. This will not work for expressions that require control flow (e.g., case, if). With this change, expressions are translated to blocks.
Reviewed By: skcho
Differential Revision: D29391068
fbshipit-source-id: 5f353e490
Summary:
Change the Makefile comment about how to enable shared library linking
despite llvm-config being broken into a rule.
Reviewed By: ngorogiannis
Differential Revision: D28907814
fbshipit-source-id: ac63d0104
Summary:
At least when installation of the conf-llvm package uses a non-system
llvm, additional compilation flags are needed. These can be queries by
asking opam for the location of the llvm-config binary, and asking
that for the compilation flags.
Reviewed By: ngorogiannis
Differential Revision: D28907810
fbshipit-source-id: 6806c78a8
Summary:
Generating the help file runs sledge, which refers to the
SLEDGE_CONFIG environment variable. This dependency was missing from
the build rule.
Reviewed By: ngorogiannis
Differential Revision: D28907804
fbshipit-source-id: e20178c6e
Summary:
Broken html could be generated if there were multiple status entries
for a single test.
Reviewed By: ngorogiannis
Differential Revision: D28907807
fbshipit-source-id: 5fcb30b5f
Summary:
It is possible for normalization to change a term from an
uninterpreted application to e.g. an interpreted atom. For instance,
the conversion `(u1)-1` evaluates to `1`. Context.canon_extend was not
taking this into account, and as a result could violate the
representation invariant of Context.t.
Reviewed By: ngorogiannis
Differential Revision: D28907806
fbshipit-source-id: 9b5171e15
Summary:
Allow joining relations with distinct entry states, since the
destinations will be the same, there is no loss of context
sensitivity. As a result, check that the call stack of the
destinations of edges are equal before joining, as it is no longer
implicitly ensured by the equal entry state check.
This change leads to joining a state with itself often, as the entry
states are often idential, so this diff also adds an optimization of
join with a fast path for joining identical states.
Reviewed By: ngorogiannis
Differential Revision: D28907809
fbshipit-source-id: 2c66223ff
Summary:
The control scheduler treats functions as if they were syntactically
inlined, by including a call stack in each control flow edge,
implicitly copying each function's control-flow graph for each calling
context. A "depth" is maintained for each retreating edge,
representing the number of times the edge has been crossed. The depths
are used to explore executions with fewer loop iterations before those
with more iterations.
The current implementation is incorrect in some situations involving
mutually recursive functions where the cycle detection algorithm
determines that calls to one of the mutually recursive functions need
not be considered retreating. Currently return frames of recursive
calls are filtered out of call stacks for the purposes of tracking
edge depths. This is insufficient in such mutual recursive
situations. This diff fixes this by explicity ignoring the entire
stack of recursive call edges.
Reviewed By: ngorogiannis
Differential Revision: D28907813
fbshipit-source-id: e04849ca8
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: Option is not used anywhere. More importantly the list of source file extensions in `Config` might give someone the impression the rest of Infer cares about it somehow.
Reviewed By: skcho
Differential Revision: D29361222
fbshipit-source-id: 22f7f66b2
Summary: Narrow container read/write modelled methods by requiring they are all non-static.
Reviewed By: ezgicicek
Differential Revision: D29331533
fbshipit-source-id: e0e445573
Summary:
After activation, a few bugs manifested and are fixed in this commit:
1. Create an (empty) Tenv per file. Previously, each file said there
will be a global Tenv, but no such global Tenv was ever saved. (There is
no static typing at all at the moment in the Erlang frontend.)
2. Procedures are now marked as defined. If the is_defined attribute is
false, then the analysis will not run even if the flowgraph in Procdesc
is nontrivial.
3. Non-dummy Start/Exit nodes for Procdesc. When a Procdesc is created,
it gets dummy Start/Exit nodes. These dummy nodes have a dummy location,
which causes debug output to have wrong directories/links.
4. Filenames from Erlang function names. By default, the verbose
procedure name was used to make file names for the debug output. But,
Erlang function names contain '/', which doesn't play well with
filenames. That's now replaced by '#' for the purposes of constructing
filenames.
Reviewed By: jvillard
Differential Revision: D29166049
fbshipit-source-id: 48346a05b
Summary:
Generates Sil instructions for Erlang some expressions:
- empty list: e.g. []
- cons: e.g. [1,2]
- atom literals: e.g. ok
- string literals: e.g. "foo"
- calls to particular (no higher-order), unqualified functions
Differential Revision: D28996467
fbshipit-source-id: fc7f7e3e9
Josh Berdine
Radu Grigore
Nikos Gorogiannis
Akos Hajdu
Daiva Naudziuniene
Jules Villard
Sungkeun Cho