Summary:
This allows using the upsteam LLVM 11 library unchanged, only
extensions to the OCaml bindings are needed. Therefore this is to
enable building sledge using e.g. `dnf install llvm-11` or `brew
install llvm@11` instead of cloning and building a fork of llvm.
Reviewed By: jvillard
Differential Revision: D27188301
fbshipit-source-id: f441dbecd
Summary:
They only attach debug info to labels, and have no execution
behavior. At some later point it would be good to scan for these and
gather the attached debug info.
Reviewed By: jvillard
Differential Revision: D27262516
fbshipit-source-id: 2eb91a475
Summary:
This warning (68) triggers when a function argument pattern depends on
mutable state, which prevents the remaining arguments from being
uncurried, causing additional closure allocations.
Reviewed By: jvillard
Differential Revision: D27188311
fbshipit-source-id: a43354e15
Summary:
Not all types of exceptions allowed by LLVM are currently
supported. The types of Resume args and LandingPad params must be
compatible, and so it only makes sense to check they the same
way.
Reviewed By: jvillard
Differential Revision: D27188307
fbshipit-source-id: c88cc46d0
Summary:
This script interoperates with the gllvm wrapper for clang that embeds
bitcode into native object files to support linking closed bitcode for
executables built with gllvm, also linking in the bitcode of needed
dynamic libraries.
Reviewed By: ngorogiannis
Differential Revision: D26903126
fbshipit-source-id: d4b95809a
Summary:
The only difference between `program` and `identified` variables is
terminology, technically they are redundant.
Reviewed By: jvillard
Differential Revision: D26451308
fbshipit-source-id: eb4e7be43
Summary:
It is not necessary to clear tables and sets that do not contain any
pointers to LLVM values.
Reviewed By: jvillard
Differential Revision: D26451306
fbshipit-source-id: 403c588fb
Summary:
The names of instructions that produce void results, other than Call
instructions, are not used. So do not consume ids for them.
There are actually very many of these, so the saved work during
translation can be significant.
Reviewed By: jvillard
Differential Revision: D26250529
fbshipit-source-id: f9eea5684
Summary:
The source block name is normally visible in the LLAIR code, while the
name of e.g. a branch instruction is some internal number. This change
only makes the output LLAIR code slightly easier to read.
Reviewed By: jvillard
Differential Revision: D26250521
fbshipit-source-id: 4723a58f7
Summary:
Sometimes symbols are added to the symbol table multiple times during
translation from LLVM to LLAIR. For example, this happens when a
`llvm.dbg.declare` instruction is encountered that attaches a debug
location to a symbol. Currently when this happens, the symbol name is
regenerated unnecessarily. This is not economical, and since counters
are used in some cases to avoid clashes, this can cause visible
changes to names.
This diff fixes this, and also makes the location update more robust
by not relying on the location added last being the best.
Reviewed By: jvillard
Differential Revision: D26250542
fbshipit-source-id: 5d52ce193
Summary:
Currently the symbolic execution options, obtained from the command
line flags and preanalysis, are passed to the Control entry points as
a record, and then passed around within Control as needed. This diff
simplifies the code in Control by replacing the record mechanism with
an additional functor parameter containing the options. The main
benefit is that the bound option no longer needs to be part of the
analysis state.
This change does make the code in Sledge_cli slightly more
complicated, as it now performs a functor application using a
first-class module computed from the command line flags.
Reviewed By: jvillard
Differential Revision: D25196735
fbshipit-source-id: 80e5d5d62
Summary:
Revise the control-flow exploration scheduling algorithm to fix
several issues. The main difference is to change the priority queue to
keep the control edges on the frontier of exploration in sync with the
states that are waiting to be propagated. This fixes several sorts of
issue where the decision of which control and state joins to perform
was unexpected / wrong. Part of keeping the frontier edges and waiting
states in sync is that the waiting states are associated not only with
a destination block, but the stack of that block. This fixes several
issues.
Combined, these changes lead to the algorithm only attempting joins
for which the pointwise max join on depth maps is correct (with the
caveat of no mathematical proof yet).
Reviewed By: jvillard
Differential Revision: D25196733
fbshipit-source-id: db007fe1f
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:
Use the equality class information in the symbolic state to resolve
callees of indirect calls.
Reviewed By: jvillard
Differential Revision: D25146160
fbshipit-source-id: a1c39bbe1
Summary:
The callee function of a Call can often be resolved
statically. Currently this is resolution is only done dynamically
during symbolic execution by checking if the callee expression is a
function name and looking up the function in the program. This is
wasted and redundant work. Also, the static resolution code is
duplicated in all the domains.
This diff resolves this by resolving known callees statically at
translation time. This involves:
- add an ICall terminator that is the same as Call is currently
- change Call to use a func callee instead of Exp.t
- make callee field mutable since recursive calls can create cycles
- change the Llair.Term.call constructor to return a thunk to perform
the backpatching once the callee has been translated
- modify the Frontend
+ to determine whether to emit Call or ICall depending on whether
the callee in LLVM is already a Function
+ to record the LLVM function -- backpatch thunk pairs encountered during translation
+ record the mapping of LLVM to LLAIR functions during translation
+ to enumerate the calls to backpatch after all functions have been
translated, and find the LLAIR function corresponding to each LLVM
function and backpatch the call to use it as the callee
+ to handle direct calls to undefined functions, when backpatching
translate such function declarations into undefined functions
Reviewed By: jvillard
Differential Revision: D25146152
fbshipit-source-id: 47d2ca1ff
Summary:
Current code partially tries to handle Invoke, but incorrectly, and
these names are only needed for Call. So this diff revises this to be
slightly simpler and less confusing.
Reviewed By: jvillard
Differential Revision: D25146157
fbshipit-source-id: ead4f6f31
Summary: Rework the intrinsic name detection to detect e.g. llvm.memset.*
Reviewed By: jvillard
Differential Revision: D25146150
fbshipit-source-id: 85ebcfb7a
Summary:
The translation of instruction intrinsics that are `Invoke`d is almost
the same as those that are `Call`ed. The same Llair instruction is
produced, but it is wired into the CFG differently. This diff uses the
translation of instruction intrinsics used for `Call`s for `Invoke`s
as well.
Reviewed By: jvillard
Differential Revision: D25146159
fbshipit-source-id: 85a93d915
Summary:
The code that computes the number of actuals is largely duplicated
between the Call and Invoke cases. But some issues have been fixed in
each that ought to be applied to the other. This factors out and
unifies this computation.
Reviewed By: jvillard
Differential Revision: D25146149
fbshipit-source-id: 78552327a
Summary:
Move the translation of Calls to intrinsics that map to instructions
into a separat function.
No functional change.
Reviewed By: jvillard
Differential Revision: D25146169
fbshipit-source-id: 79c640344
Summary:
Currently intrinsics are treated as functions, with Call instructions
to possibly-undefined functions with known names. This diff adds an
Intrinsic instruction form to express these more directly and:
- avoid the overhead of intrinsics needing to end blocks
- avoid the overhead of the function call machiery
- avoid the complexity of doing the string name lookup to find their
specs, repeatedly
This diff only adds the backend support, the added Intrinsic
instructions are not yet generated by the frontend.
Reviewed By: jvillard
Differential Revision: D25146155
fbshipit-source-id: f24024183
Summary:
Previously, when LLAIR was in SSA form, blocks took parameters just
like functions, and it was sometimes necessary to partially apply a
block to some of the parameters. For example, blocks to which function
calls return would need to accept the return value as an argument, and
sometimes immediately jump to another block passing the rest of the
arguments as well. These "trampoline" blocks were partial applications
of the eventual block to all but the final, return value,
argument.
This partial application mechanism meant that function parameters and
arguments were represented as a stack, with the first argument at the
bottom, that is, in reverse order.
Now that LLAIR is free of SSA, this confusion is no longer needed, and
this diff changes the representation of function formal parameters and
actual arguments to be in the natural order. This also brings Call
instructions in line with Intrinsic instructions, which will make
changing the handling of intrinsics from Calls to Intrinsic less
error-prone.
Reviewed By: jvillard
Differential Revision: D25146163
fbshipit-source-id: d3ed07a45
Summary:
Overwritten variables in move instructions are not impossible. Since
Domain_itv does not handle them, the check should be a `todo` rather
than an `assert false`.
Reviewed By: jvillard
Differential Revision: D25146168
fbshipit-source-id: 13d8587c7
Summary:
The use of realpath on paths obtained from debug info and the current
working directory is application-usage-specific behavior that does not
belong in the backend library. This diff moves these uses to the
frontend and cli, respectively. Also, the use of realpath in the
frontend is memoized along the same lines as the other frontend
translation functions.
This was also the last use of `core` in the `sledge` library, so the
dependency is moved to `sledge_cli` and `sledge_report`.
Reviewed By: ngorogiannis
Differential Revision: D24989070
fbshipit-source-id: c21b275f5
Summary:
Currently __llair_choice is left undefined, and so executed as skip.
This has the correct behavior, but makes it hard to distinguish from
calls to unintentionally-undefined procedures.
Reviewed By: ngorogiannis
Differential Revision: D24989068
fbshipit-source-id: f62981857
Summary:
Change `-llair-output` to `-output`, for binary form, and
`-llair-txt-output` to `-llair-output`, for textual form. Also
correspondingly change `.llair` to `.bllair`, for binary, and
`.llair.txt` to `.llair` for text.
This improves command line argument completion, and makes `.llair` the
extension of the files most commonly interacted with.
Reviewed By: ngorogiannis
Differential Revision: D24951506
fbshipit-source-id: ad4c73ca2
Summary:
Global constants have reliable types, and their sizes can be used
instead of storing the size of the initializer separately.
Reviewed By: jvillard
Differential Revision: D24934114
fbshipit-source-id: 2426ab5be
Summary:
Localizing the entry of a procedure needs the globals (that the
procedure uses), but later creating a summary does not.
Reviewed By: jvillard
Differential Revision: D24886570
fbshipit-source-id: 8a7b18c58
Summary:
The general xlate_value function can be used in place of
xlate_func_name.
Reviewed By: jvillard
Differential Revision: D24846677
fbshipit-source-id: 603ebd388
Summary:
Calling an inline asm function that might raise is not currently
supported.
Reviewed By: jvillard
Differential Revision: D24846675
fbshipit-source-id: a7cfe6050
Summary:
Mangled names start with _Z, so only demangle those names. This leaves
unmangled C names alone.
Reviewed By: jvillard
Differential Revision: D24846674
fbshipit-source-id: d239a61aa
Summary:
Distinguish expressions that name globals from registers. This leads
to clearer code, and globals are semantically distinct from general
registers. In particular, they are constant, so any machinery for
handling assignment does not need to consider them. This diff only
adds the distinction to LLAIR, it is not pushed through to FOL, which
will come later.
Reviewed By: jvillard
Differential Revision: D24846676
fbshipit-source-id: 3aca025bf
Summary:
This module represents the definition of a global constant, rather
than the global itself.
Reviewed By: jvillard
Differential Revision: D24846673
fbshipit-source-id: d47e67984
Josh Berdine