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
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
Akos Hajdu
Jules Villard
Radu Grigore
Nikos Gorogiannis
Josh Berdine
Daiva Naudziuniene
Sungkeun Cho