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 `#define`s the functions to which `assert` compiles to
`abort`. This enables the analyzer to report assertion violations, and
is independent of platform.
Also add a simple test to check that it is detected correctly.
Reviewed By: ngorogiannis
Differential Revision: D27564870
fbshipit-source-id: 5517ca910
Summary:
Currently there is a symbolic execution option to ignore exceptional
control flow. This hack does not fit well, and it is unclear how much
backend functionality should take it into consideration. This diff
removes this option and replaces it with an option during model
compilation. This has the advantage of clarifying and simplifying the
backend, with the disadvantage of no longer supporting switching
between exceptions and no-exceptions modes at analysis time. Since the
possibility of ignoring exceptional control flow is due to it not being
ready yet, this is a good trade to make.
Reviewed By: jvillard
Differential Revision: D25146148
fbshipit-source-id: 1f1299ee1
Summary:
It is now possible to not spew dune files all over the repo, and opam
files aren't needed either.
Reviewed By: jvillard
Differential Revision: D21720978
fbshipit-source-id: 553e1d154
Summary:
Move files, adjust build system, etc.
This also separates out the ppx_trace conditional compilation debug
tracing machinery into an independent package and library.
Reviewed By: jvillard
Differential Revision: D20322876
fbshipit-source-id: a50522462
Summary:
Since version 2, none of the `opam pin` modes work reasonably well for
the standard llvm build procedure. As a workaround to prevent opam
from making several copies of the build directory when pinning, adjust
to move the llvm build and install directories out of the llvm source
tree.
Reviewed By: bennostein
Differential Revision: D17665242
fbshipit-source-id: ac84a4b0b
Summary:
There are many assumptions on the behavior of mutexes, condition
variables, etc. in the implementation of the cxxabi with threads
support. So compile with `_LIBCXXABI_HAS_NO_THREADS` defined to select
the much simpler code paths for the single-threaded case.
Reviewed By: kren1
Differential Revision: D16069454
fbshipit-source-id: 9f975e0e6
Summary:
This diff introduces a `-lib-fuzz` flag to `buck link`, which links in a
simple main that calls the LLVMFuzzerTestOneInput function, which is the
entry point of libFuzzer fuzzer.
Reviewed By: jberdine, jvillard
Differential Revision: D15821512
fbshipit-source-id: cff731ed3
Summary:
This diff adds a `__llair_alloc` intrinsic which is modeled
as a non-failing malloc. Using it instead of `malloc` increases
the readbility of symbolic heaps, because it removes all the cases
where malloc failed.
Note that `assert(malloc())` does not have the desired effect.
Reviewed By: ngorogiannis
Differential Revision: D15778817
fbshipit-source-id: d02784077
Summary:
Include cxa_default_handlers.cpp to bring in definitions for
__cxa_terminate_handler and __cxa_unexpected_handler.
Reviewed By: kren1
Differential Revision: D15712980
fbshipit-source-id: f536930a8
Summary:
* Adds compilation of cxxabi.bc
* Includes the cxxabi.bc into the sledge executable via opam-crunch
* Links cxxabi.bc in sledge frontend
Reviewed By: jberdine
Differential Revision: D15415190
fbshipit-source-id: cc42f09fb
Summary:
Make could get confused and use both the $(MODEL_DIR)/cxxabi.bc and
%.bc rules, leading to build failure.
Reviewed By: jvillard
Differential Revision: D14385600
fbshipit-source-id: 05f0ac6e1
Summary:
Change the license of the source code from BSD + PATENTS to MIT.
Change `checkCopyright` to reflect the new license and learn some new file
types.
Generated with:
```
git grep BSD | xargs -n 1 ./scripts/checkCopyright -i
```
Reviewed By: jeremydubreil, mbouaziz, jberdine
Differential Revision: D8071249
fbshipit-source-id: 97ca23a
markma
Josh Berdine
Timotej Kapus
Jules Villard