Summary:
Improve Trace.fail to log the error and raise informative exceptions.
Eliminate the confusion between Import.fail and Trace.fail by removing
Import.fail.
Reviewed By: bennostein
Differential Revision: D17725608
fbshipit-source-id: 79fdfbd86
Summary:
By default all functions except those specified as entry points in the
config file are "internalized". Internal functions are removed if they
are not called. It is sometimes necessary to disable internalization,
e.g. to analyze the llvm tests.
Reviewed By: bennostein
Differential Revision: D17725614
fbshipit-source-id: 4b13501f5
Summary:
Sometimes the models for the C/C++ runtime and standard libraries are
not needed. Furthermore, sometimes, e.g. when analyzing llvm tests,
trying to link them fails.
Reviewed By: bennostein
Differential Revision: D17725616
fbshipit-source-id: 76a4bcf90
Summary:
The `(t, unit) result` type is no more informative than `t option` and
less convenient.
Reviewed By: bennostein
Differential Revision: D17665244
fbshipit-source-id: fa969d8b7
Summary:
This puts the mediation between Exp and Term together in Sh_domain
rather than being spread across the two.
Reviewed By: bennostein
Differential Revision: D17665235
fbshipit-source-id: edf277d45
Summary:
The move instruction takes a vector of assignments to perform in
parallel, so generalize exec_move from one to a vector.
Reviewed By: bennostein
Differential Revision: D17665248
fbshipit-source-id: 52aae5ff9
Summary:
Extend the encoding using `id` from 0 indicating a program variable to
also -1 indicating a global program variable.
Reviewed By: bennostein
Differential Revision: D17665229
fbshipit-source-id: 848b8a31e
Summary:
The sorting of heap blocks when printing formulas was broken by the
change to the direct representation of polynomials.
Reviewed By: bennostein
Differential Revision: D17665246
fbshipit-source-id: 4ebea9f20
Summary: It is not necessary to have both < and >=, and similarly for <= and >.
Reviewed By: bennostein
Differential Revision: D17665232
fbshipit-source-id: 01b3511f5
Summary:
Now that terms operate over unbounded, signed, integers rather than
bounded integers, and Boolean operations are treated uniformly with
bitwise operations, it is not necessary to propagate types throughout
arithmetic term manipulation.
Reviewed By: bennostein
Differential Revision: D17665257
fbshipit-source-id: 5236b101d
Summary:
Z.numbits ignores the sign, which allows 2^(N - 1) as representable
within N bits, while it is not. So check explicitly.
Reviewed By: bennostein
Differential Revision: D17665231
fbshipit-source-id: 0d3940517
Summary:
Instead of having separate signed and unsigned operations, use the
signed operations applied to explicit conversion of the arguments
using an unsigned integer interpretation.
Reviewed By: bennostein
Differential Revision: D17665267
fbshipit-source-id: 0b3271e71
Summary:
Add an Extract term form to interpret an integer with given signedness
and bitwidth.
Reviewed By: bennostein
Differential Revision: D17665263
fbshipit-source-id: 1d8917f3c
Summary:
Be more explicit about semantics of unsigned vs. signed conversions,
and fix a few related corner cases.
Reviewed By: bennostein
Differential Revision: D17665268
fbshipit-source-id: 67fecdf34
Summary:
With terms using unbounded two's complement arithmetic, it is not
necessary to special-case 1-bit integers as Booleans.
Reviewed By: ngorogiannis
Differential Revision: D17665228
fbshipit-source-id: a2f280fc3
Summary:
Remove the guards that prevent normalizing in some cases where the
corresponding instruction in LLVM would produce a poison
value. Usefully tracking poison values will be more involved.
Reviewed By: ngorogiannis
Differential Revision: D17665230
fbshipit-source-id: 59fb25042
Summary:
Revise program expressions based on the changed constraints now that
Term is separate from Exp. In particular:
- Add types to all application, indicating how the operation
interprets its arguments
- Change to a simpler uncurried form
- Remove now-unneeded normalizations
Reviewed By: bennostein
Differential Revision: D17665236
fbshipit-source-id: 1bcf2efd6
Summary:
Boolean and bitwise negation of `e` is represented using `-1 xor
e`. Since Equality can only maintain and propagate equality
constraints, Boolean negation `-1 xor b` is normalized to `b =
false`. This diff delays this normalization from being part of
expression construction to part of symbolic heap formula
construction. This makes the normalization done as part of expression
construction independent of the distinction between bitwise and
boolean operations.
Reviewed By: bennostein
Differential Revision: D17665254
fbshipit-source-id: 0a0722865
Summary:
Splat, Memory, and Concat expressions are never used. Only the term
forms are needed.
Reviewed By: bennostein
Differential Revision: D17665259
fbshipit-source-id: cbfd7650d
Summary:
There are a number if issues with using the same type for expressions
in code and in formulas. One is that the type systems of the two
should be different. Another is that conflating the two compromises
the ability of Llair to correctly express aspects such as integer
overflow, floating point rounding, etc. Also, it could be beneficial
to have more source locations for program expressions than makes sense
for terms.
This diff simply unshares Exp, leading to a copy named Term. Likewise,
Reg is now a copy of Var. Simplifications to come.
Reviewed By: bennostein
Differential Revision: D17665250
fbshipit-source-id: 4359a80d5
Summary:
The generation of names for the function formal return and throw
parameters is not central to LLAIR, but a detail of the frontend,
since they are generated only because LLVM does not already have such
names.
Reviewed By: ngorogiannis
Differential Revision: D17665240
fbshipit-source-id: 684cbae92
Summary:
Using a type of keys richer than strings, which are the unique symbol
names at the C/LLVM level, is unnecessary.
Reviewed By: ngorogiannis
Differential Revision: D17665262
fbshipit-source-id: 6b8c31146
Summary:
The convenience wrappers for operations on signed 1-bit integers
represented by Z.t are not specific to Exp.
Reviewed By: ngorogiannis
Differential Revision: D17665252
fbshipit-source-id: d4b58e2a6
Summary:
Now that the relation domain construction is factored out and
generalized.
Reviewed By: ngorogiannis
Differential Revision: D17665253
fbshipit-source-id: eb156ce6b
Summary:
This diff allows domains to specify which abstract states can or can't
be merged together by the worklist. In particular, this is needed for
relational domains to ensure that Hoare triples are joined only when
they share a precondition.
Reviewed By: jberdine
Differential Revision: D17571148
fbshipit-source-id: d9345fdc9
Summary:
This diff adds a "-prenalyze-globals" flag to all analyze targets
which, when set, computes used-globals sets for all reachable
functions and then uses that information to track only relevant
global variables at calls in the main analysis.
Reviewed By: jberdine, jvillard
Differential Revision: D17526746
fbshipit-source-id: 1a114285c
Summary:
Fixes a bug in Llair.Frontend.xlate_value where the l-val register
of LLVM instruction calls was being marked as global.
Reviewed By: jberdine
Differential Revision: D17570458
fbshipit-source-id: e1b5924e2
Summary:
Fixes a bug where are all calls are treated as intrinsics in used
globals analysis, since exec_intrinsic is invoked at _all_ calls
to determine which are intrinsic, not only at call sites known to
target intrinsics.
Reviewed By: jberdine
Differential Revision: D17499406
fbshipit-source-id: 41f7621f2
Summary:
While the symbolic heap analysis ends its search upon hitting the
bound on recursion depth, the used-globals analysis should instead
simply skip recursive calls beyond the depth. Note that this is
unsound for arbitrary abstract domains, however, and the flag
controlling this feature should be used with caution.
Note that procedure calls are still not handled correctly, since
Used_globals.exec_intrinsic does not properly check whether callees
are intrinsic. A forthcoming commit will fix that, as well.
Reviewed By: jberdine
Differential Revision: D17479753
fbshipit-source-id: aa92e0ef3
Summary:
Include global variables used in function callees in used globals
analysis. Also adds support for arbitrary changes to symbolic
state while resolving callees in other analyses.
Reviewed By: jberdine
Differential Revision: D17479352
fbshipit-source-id: e3cd9f179
Summary:
Replace custom version reporting support using a shell script with
code using dune's Build_info API.
Note that after this diff, the executables under _build/<context> are
not version-stamped, but those under _build/_install are. The symlinks
in bin point to the latter, stamped, exes.
Reviewed By: bennostein
Differential Revision: D16985446
fbshipit-source-id: 7afac87be
Summary:
Adds an abstract domain to track global variable usages, as well as supporting
changes to the frontend, IR and CLI. This analysis will support optimizations
to the main symbolic-heap analysis, but for now can be invoked independently
through the `-domain` flag on `analyze` targets of the Sledge executable.
Reviewed By: jberdine
Differential Revision: D17422212
fbshipit-source-id: 74bed0a76
Summary:
Generalize the lifting from State_domain (i.e. symbolic heaps) to Sh_domain (i.e. relations over symbolic heaps).
Also, extract abstract-domain-related code into its own module/directory.
Reviewed By: jberdine
Differential Revision: D17319007
fbshipit-source-id: cefbd1393
Summary: Add support for future development of new abstract domains by eliminating hard-wired dependencies from the worklist into the symbolic heap domain. Also includes an implementation of a trivial unit domain and a CLI flag to enable its use, for debugging purposes.
Reviewed By: jberdine
Differential Revision: D17281681
fbshipit-source-id: 5858fd420
Summary:
In some cases inlining pure expressions into their use sites causes
code blowup. This diff changes the frontend to inline expressions only
if there is a single use, and otherwise adds a move instruction.
Reviewed By: ngorogiannis
Differential Revision: D17071770
fbshipit-source-id: d866a0622
Summary:
This has been out of date since arithmetic was changed from a purely
uninterpreted treatment to having a solver.
Reviewed By: jvillard
Differential Revision: D16985159
fbshipit-source-id: 39e42069c
Summary:
While SSA can be useful for code transformation purposes, it offers
little for semantic static analyses. Essentially, such analyses
explore the dynamic semantics of code, and the *static* single
assignment property does not buy much. For example, once an execution
visits a loop body that assigns a variable, there are multiple
assignments that the analysis must deal with. This leads to the need
to treat blocks as if they assign all their local variables, renaming
to avoid name clashes a la Floyd's assignment axiom. That is fine, but
it makes it much more involved to implement a version that is
economical with respect to renaming only when necessary. Additionally
the scoping constraints of SSA are cumbersome and significantly
complicate interprocedural analysis (where there is a long history of
incorrect proof rules for procedures, and SSA pushes the
interprocedural analysis away from being able to use known-good
ones). So this diff changes Llair from a functional SSA form to a
traditional imperative language.
Reviewed By: jvillard
Differential Revision: D16905898
fbshipit-source-id: 0fd835220
Summary:
Before this diff symbolic execution of instructions assumed that
assigned variables were unconstrained in the precondition. This is
ensured by symbolic execution of control flow, which renames all local
variables of a block when it is entered.
This diff changes symbolic execution of instructions to rename
modified variables that appear in the precondition when necessary, and
accounts for the modified variable occurrence condition on the frame
rule. This will enable more economically renaming variables, as most
of the time it is not needed.
Reviewed By: jvillard
Differential Revision: D16905893
fbshipit-source-id: 3a53525d7
Summary:
Currently bitcode produced with `sledge buck link` can have missing
symbols that are clearly defined in the source. For example consider a
symbol `awesome_function` that is defined in the libraries linked in but
not in the produced binary (despite being reachable from main).
`llvm-nm` of the bitcode produced by `llvm-link` might look like:
```
U awesome_function
t awesome_function.1892
```
Some our `awesome_function` is undefined and its definition is called
`awsome_function.1892` for some reason and is local. I think this is because symbol get internalized too early and then they get renamed and somehow lost. Not sure why `llvm-link` behaves this way sometimes.
This patch removes internalization from `llvm-link` and puts it into `opt`, where it doesn't cause problems.
Reviewed By: jvillard
Differential Revision: D16494153
fbshipit-source-id: aad9053a4
Summary:
`__llair_alloc` is meant to be a drop-in non-failing replacement for
`mallco`. Currently `__llair_alloc(1)` allocates 8 bytes instead of 1 as
`malloc(1)` would. This is because handling of `__llair_alloc` was
merged with handling of `new`. This patch reverts changes to handling of
`new` in D15778817 and adds a new case for `__llair_alloc`.
Reviewed By: jvillard
Differential Revision: D16356865
fbshipit-source-id: 3878d87c3
Summary:
When using summaries we first garbage collect the precondition and then
ask the solver to infer the frame of the precondition with respect to
grabage-collected footprint.
Currently if the solver fails to show the frame, we just give it an
empty frame. This is bad, because if grabage collection removed some
segments, they don't get added back on.
This patch throws an exception instead to be very explicit when the
solver cannot show the frame in this case.
Reviewed By: ngorogiannis
Differential Revision: D16339587
fbshipit-source-id: b88d0689c
Summary:
The actual implementation of folly::usingJEMalloc() tests if malloc is
jemalloc using internal knowledge of the jemalloc implemenation of
malloc. This internal behavior is not reflected in the analyzer's
spec, so the detection fails.
Additionally, folly::usingJEMalloc is implemented using mallctl to
query internal state of jemalloc. Depending on the key string passed
to mallctl, it might return a pointer to jemalloc internal state, or a
scalar, which means that the spec needs to essentially allocate that
state in those cases.
Since the jemalloc detection fails, and the analyzer is not always
able to reason precisely about string equality, this diff models
folly::usingJEMalloc directly (as nondet).
Reviewed By: kren1
Differential Revision: D16059776
fbshipit-source-id: 7e7156d7d
Summary:
It seems that functions internalized by llvm no longer have valid
mangled names, and instead have a `.<int>` suffix. This diff removes
these unpredictable suffixes when checking if a called function is a
specified/modeled intrinsic.
Reviewed By: kren1
Differential Revision: D16059781
fbshipit-source-id: a4b9f6c73
Summary:
A frame inference query `Minuend ⊢ ∃xs. Subtrahend` returns a
`∃zs. Remainder` formula such that `Minuend ⊢ ∃xs. Subtrahend *
∃zs. Remainder` when successful. Currently if the subtrahend is itself
existentially quantified, its existentials are treated trivially: they
must witness themselves. This diff allows the solver to find witnesses
as the `xs`. They are still existentially quantified in the remainder,
so clients that need to constrain them should still name them before
calling the solver.
Reviewed By: kren1
Differential Revision: D16269630
fbshipit-source-id: 65136edd1
Summary:
Add a global merge pass that merges globals into a single big global. It
replaces the uses of globals merged, with offsets into the big global.
Function summarisationis a big benefactor of this as it greatly reduces
the number of implicit formals (ie. globals).
Reviewed By: jvillard
Differential Revision: D16260098
fbshipit-source-id: 1b936f02f
Summary:
Fix a bug where summaries would be created even if summarisation option
is disabled.
Reviewed By: jvillard
Differential Revision: D16259761
fbshipit-source-id: f7319ef03
Summary:
If function summaries are enabled calling a function first tries to
apply a summary, if succesful, it directly jumps to the return site of
the call. Otherwise it proceeds as before.
Reviewed By: jvillard
Differential Revision: D16201251
fbshipit-source-id: cec52e0e5
Summary:
Define a new function summary type and compute it on function return.
As an intermediary step also apply the just computed summary to function
pre so it can be compared to what was actually computed.
Reviewed By: jvillard
Differential Revision: D16149833
fbshipit-source-id: b826c17e8
Summary:
Fix a crash that occurs when subtrahend has an existential variable that
was renamed as in the test.
The crash is due to an assertion in `Sh.exists` that says only variables
in the vocabulary can be existentialy quantifed out.
The problem was `Sh.exists` call in Solver.ml:611. Where `ws`
(existentials of the subthrehend) are not present in the vocabulary of
the remainder. This is because remainder "inheirts" the vocabulary of
the minued.
This fix simply extends the vocabulary of minued with `ws`, which
means the remaainder has the correct vocabulary. This should have no
externally visible effect as `ws` are then existentialed out.
Another option would be to try to change all the `excise_seg` functions,
to keep the vocabulary, but that looked annoying to implement.
Reviewed By: jvillard
Differential Revision: D16201423
fbshipit-source-id: b88c3abc4
Summary:
Add a `-color` option to sledge, that prints variable that are
existentially bound as bold.
Reviewed By: ngorogiannis
Differential Revision: D16088750
fbshipit-source-id: bd21cb8a0
Summary:
This fixes two bugs:
* All local variables would get existentially quantified out, that means
the the local variables of the caller couldn't be restored properly
* Frame was added back on after the formals were killed. Which meant
that if frame talked about formals (in pure for example), those
formals would remain to be free variables.
Reviewed By: ngorogiannis
Differential Revision: D16091157
fbshipit-source-id: dfe12ed82
Summary:
This fixes two issues with function summarization when calling a
function multiple times.
* Previously on return, the actuals wouldn't get added back in, so
their name would be "lost" (that is existentially quantified out),
this patch adds the formals to actuals equalities back on return,
before quantifying the formals out.
* Previously the entry state of the function would be lost if there were
multiple calls to other functions.
Reviewed By: jberdine
Differential Revision: D16071656
fbshipit-source-id: 9df7b1d4b
Summary:
Currently alarms are reported to stdout while the debug trace is
written to stderr. This makes synchronizing the two difficult. With
this diff, the alarm reports can also be included in the debug trace,
and analysis can be stopped when an alarm is encountered by tracing
the `Stop` module, e.g.:
```
sledge -trace Report+Stop.on_invalid_access
```
Reviewed By: kren1
Differential Revision: D16072611
fbshipit-source-id: 32c3639a2
Summary:
Each call to __cxa_allocate_exception, in practice, is shortly
followed by raising an exception. With -skip-throw, execution will not
proceed past the throw. Since the concrete implementation of
__cxa_allocate_exception and the following initialization of the
exception object is very low-level code that plays tricks, the
analyzer has trouble with it. So model __cxa_allocate_exception as
unreachable to avoid (needlessly) executing that code and potentially
failing spuriously.
Reviewed By: kren1
Differential Revision: D16069451
fbshipit-source-id: bea1dae09
Summary:
Allow intrinsics to return an inconsistent state, to specify that they
do not return.
Reviewed By: kren1
Differential Revision: D16069453
fbshipit-source-id: deb5d2a22
Summary:
This adds an optimized debug build mode, which is compiled with
optimizations, and without assertions, but still has tracing enabled.
Reviewed By: kren1
Differential Revision: D16069452
fbshipit-source-id: 445cfa329
Summary:
The report output got disturbed by the change from predicate to
relational Domain, and the tricky control of printing simplified
states. After this diff by default states are printed in full, and in
simplified form with `-t State_domain.pp_simp`.
Also includes some minor output improvements.
Reviewed By: kren1
Differential Revision: D16059780
fbshipit-source-id: b33289887
Summary:
Trivial renamings to use the standard "libFuzzer" name instead of "lib
fuzzer".
Reviewed By: kren1
Differential Revision: D16067881
fbshipit-source-id: 3ff2a8f86
Summary:
On function return add the computed summary (pre/post) condition to a
hashtable.
Reviewed By: jberdine
Differential Revision: D16052136
fbshipit-source-id: 0c5c9bafb
Summary:
Outputting the list of bitcode inputs when no output flag is ok for
`sledge buck bitcode` but does not make sense when it is composed as
part of other commands. So only output to stdout if `-` is given as
the output file name.
Reviewed By: kren1
Differential Revision: D16059782
fbshipit-source-id: abac9c36f
Summary:
To easily monitor and track changes to the help generated by the
command line interface, generate it in full and add it to the repo.
Reviewed By: kren1
Differential Revision: D16059783
fbshipit-source-id: be15f9943
Summary:
This diff enhances `-function-summaries` to remember the frame computed by
the solver and actually execute the function using the summary. Upon
return the frame is added back on the computed post condition.
Reviewed By: ngorogiannis
Differential Revision: D15900318
fbshipit-source-id: 8bb56b771
Summary:
This diff is preparation for function summarization and focuses on
function calls and function summary precondition computation.
It introduces `-function-summaries` flag behind most of functionality is
hidden, when enabled on each call
* A function summary is computed by quantifying all the non-formal/global variables
and removing all the segments that are not reachable from them
* `pre` and `foot` are computed from function summary and the calling context
by replacing formals with actuals again.
* A solver is asked if `pre` entails `foot` and a frame is printed if it
does
Currently this only works for formulas without disjunctions, so when
function summaries are enabled, that state is first moved to dnf and then
the call is done for each disjunct.
Reviewed By: ngorogiannis
Differential Revision: D15898928
fbshipit-source-id: 49d32504c
Summary: For buck targets that contain at least one of the substrings in `buck-target-pattern` option in config, change the buck target to add `_sledge` suffix.
Reviewed By: jberdine
Differential Revision: D15920018
fbshipit-source-id: 44c242e99
Summary:
Simplify all conversions between castable types to the identity. The
backend treats castable types as equal, so distinguishing conversions
between them is incomplete.
Reviewed By: kren1
Differential Revision: D15972427
fbshipit-source-id: fa09859ac
Josh Berdine
Benno Stein
Timotej Kapus