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:
The creation of the inital state has evolved several times recently,
time for a refactor:
- do not create then pass the initial state around when callees can
create it instead
- slightly hackish assertions that creating the initial state conditions
cannot fail to simplify the types (could eventually be moved in
AbductiveDomain.ml to avoid breaking abstraction layers like this, but
trivial enough that it doesn't really matter I think)
Reviewed By: skcho
Differential Revision: D29550319
fbshipit-source-id: 63919ae71
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: Typ.pp does not print types by default, use Typ.pp_full instead.
Reviewed By: ngorogiannis
Differential Revision: D29557158
fbshipit-source-id: 62ae20bd5
Summary:
Before, atoms we didn't understand but could be a contradiction became
"true" if they were only about dead variables. This is unsound for
incorrectness logic, and introduces false positives.
Be more conservative and try to identify when that could happen and
prune these paths instead, thus regaining under-approximation.
This is a bit ad-hoc: we expect reasoning on equalities and
disequalities to be precise enough, but we know that inequalities have
very little solving power at the moment (eg we don't detect `x < 0, x >
0 => false`). In addition, we remark that having *one* `<` atom can
never be a contradiction. So, we claim a possible contradiction whenever
we find *two* (>1) atoms containing inequalities and involving the same
variable.
Reviewed By: skcho
Differential Revision: D29232544
fbshipit-source-id: ff91eb1e4
Summary: Add some test cases to potentially non-exhaustive case clauses.
Reviewed By: rgrig
Differential Revision: D29555525
fbshipit-source-id: f710e93e6
Summary: New inferconfig flags which will pass through to buck config flags. Purpose is to allow using a buck target to distribute and use infer binaries as a buck toolchain.
Reviewed By: martintrojer
Differential Revision: D29485801
fbshipit-source-id: 86169cdae
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:
"glue" together the trace from the caller with the trace from the callee
to form the access trace when applying LatentInvalidAccess summaries.
This is consistent with what happens in function calls and allows Pulse
to better keep track of the history of the value. The goal is to prevent
bugs from getting filtered out because the access trace doesn't contain
the invalidation event for the value.
Reviewed By: da319
Differential Revision: D29550320
fbshipit-source-id: b600c188d
Summary:
There should be no change in semantics:
- before: the "crash node" modelling throwing an exception was connected directly to the exit of the procedure
- now: the "crash node" goes to exit_failure, which should end up being connected to the exit of the procedure by the `translate_one_function`
The latter is closer to what we'd need to do when we eventually model
throwing and catching exceptions (rather than just reporting an error
the moment we see them thrown).
Differential Revision: D29540834
fbshipit-source-id: c4de4c391
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: `call-graph-schedule` was a boolean, now we have a variant type for scheduler.
Reviewed By: jvillard
Differential Revision: D29547773
fbshipit-source-id: ec787065c
Summary:
This diff changes the analysis exploration algorithm from considering
only sequential executions to considering executions of the
interleaving semantics. As part of this, symbolic states are changed
so that each thread has its own registers, while all memory is shared
between them.
Currently only a simple threads interface is supported: they can be
created with `thread_create(&thread_routine)`, they can exit by
returning from `thread_routine`, and they can be joined with
`thread_join`. Current simplifications include that newly created
threads are already runnable, thread routines accept no arguments and
return no result, and no failures are possible.
The concurrent exploration algorithm gives preference to executions
which have fewer context switches, thereby performing an incremental
form of context-bounded analysis.
A form of partial-order reduction is performed, where the symbolic
states are joined across (prefixes of) executions with the same number
of context switches which reach a point where the instruction pointers
and call stacks of all threads are the same. This has the effect of
"dagifying" the concurrent execution tree by merging points after
e.g. threads perform actions that commute with each other. This is
unlike traditional partial-order reduction in that it relies on the
symbolic join to combine the results of commuting operations in a way
that the following symbolic execution can take advantage of, rather
than performing some up-front analysis to identify commuting
operations and quotienting the space of executions. The current state
of the symbolic join and execution is significantly suboptimal in this
regard.
Differential Revision: D29441149
fbshipit-source-id: cf801a6b1
Summary:
This diff reworks the analysis scheduler to explicitly use a notion of
"abstract machine state" which makes the distinction with the state of
the analysis exploration algorithm more clear. The instruction
pointer, call stack, symbolic state, and retreating edge depths were,
prior to this change, passed individually to the various `exec_*`
functions. After this change, all this information is combined into an
abstract machine state value.
Additionally, this change explicitly factors out the commonality
between abstract machine states, on which symbolic execution operates,
and the elements of the frontier of exploration, that the analysis
scheduler maintaines. In short, an element of the frontier is simply
an abstract machine state with a control-flow edge instead of an
instruction pointer.
This change is almost entirely a non-functional refactoring. While
this serves as an improvement in code clarity, the main motivation is
that it establishes a code structure which minimizes the structural
changes needed when adding the concurrency analysis.
Differential Revision: D29441152
fbshipit-source-id: 01be87d4e
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
Akos Hajdu
Jules Villard
Daiva Naudziuniene
Nikos Gorogiannis
Radu Grigore
Josh Berdine