Summary:
OCaml 4.08 supports a form of signature-local bindings, to that a type
can be defined in order to be used in other definitions, without
being part of the signature itself.
Reviewed By: ngorogiannis, jvillard
Differential Revision: D18736380
fbshipit-source-id: 0bb043de6
Summary:
Otherwise it is difficult to tell the difference between compilation
errors from previous versus current builds.
Reviewed By: ngorogiannis
Differential Revision: D18736376
fbshipit-source-id: 2e583f4ba
Summary:
OCaml 4.08 has a new warning (66) on unused `open!` statements. This
has a suboptimal interaction with `ppx_let`'s `let%map_open` which
leads to triggering the warning if any of a group of such let bindings
does not need the open.
In this case, the refactor is easy.
But, warning 66 is very dubious, so also just switch it off.
Reviewed By: jvillard
Differential Revision: D18708466
fbshipit-source-id: 77618ab6e
Summary:
It seems to be effectively unmaintained, as it still doesn't support
4.08.
Reviewed By: jvillard
Differential Revision: D18708467
fbshipit-source-id: dcb3361fc
Summary:
Term.solve makes the assumption that all distinct normalized constants
denote distinct values. This is fragile at best, and it is better to
enumerate the cases where solve discovers inconsistency.
Reviewed By: jvillard
Differential Revision: D18459619
fbshipit-source-id: 71f52557c
Summary:
Equality.or_ assumed a simpler representation of equality relations,
and was incomplete as a result.
Reviewed By: jvillard
Differential Revision: D18298138
fbshipit-source-id: cf91229f6
Summary:
The treatment of type conversions is too complicated, non-uniform,
etc. This diff attempts to simplify things by separating integer to
integer conversions, which are interpreted, from others, which are
essentially just uninterpreted functions. Integer conversions are now
handled using two expression and term forms: Signed and
Unsigned. These each interpret their argument as either a signed or
unsigned number of a given bitwidth:
```
| Signed of {bits: int}
(** [Ap1 (Signed {bits= n}, dst, arg)] is [arg] interpreted as an
[n]-bit signed integer and injected into the [dst] type. That is,
it two's-complement--decodes the low [n] bits of the infinite
two's-complement encoding of [arg]. The injection into [dst] is a
no-op, so [dst] must be an integer type with bitwidth at least
[n]. *)
| Unsigned of {bits: int}
(** [Ap1 (Unsigned {bits= n}, dst, arg)] is [arg] interpreted as an
[n]-bit unsigned integer and injected into the [dst] type. That
is, it unsigned-binary--decodes the low [n] bits of the infinite
two's-complement encoding of [arg]. The injection into [dst] is a
no-op, so [dst] must be an integer type with bitwidth greater than
[n]. *)
| Convert of {src: Typ.t}
(** [Ap1 (Convert {src}, dst, arg)] is [arg] converted from type [src]
to type [dst], possibly with loss of information. The [src] and
[dst] types must be [Typ.convertible] and must not both be
[Integer] types. *)
```
Reviewed By: ngorogiannis
Differential Revision: D18298140
fbshipit-source-id: 690f065b4
Summary:
LLAIR changed how it represents integer-to-integer conversions, and this
updates the semantics and proofs to show that the new way is correct.
Reviewed By: jberdine
Differential Revision: D18448616
fbshipit-source-id: b657fcd20
Summary:
The old version of simp_convert in LLAIR had a bug, but the sanity
theorem didn't catch it because it didn't enforce that the result fit
into the size it should have. This updates to newer version of
simp_convert and adds a theorem that the result fits.
Reviewed By: jberdine
Differential Revision: D18346833
fbshipit-source-id: 533c836bf
Summary:
Extend the APRON-backed interval analysis to handle a wider range
of LLAIR expressions.
Reviewed By: jvillard
Differential Revision: D17858072
fbshipit-source-id: c50f5bf20
Summary:
In some cases the result of an integer conversion needs to be
truncated by a bit.
Differential Revision: D18271179
fbshipit-source-id: e80740045
Summary:
Improve the invariants to show that phi instructions are correctly
translated. It remains to show that the invariants can be established
when jumping to the start of a block
Reviewed By: jberdine
Differential Revision: D18228272
fbshipit-source-id: 4330b4781
Summary:
Add a new interval abstract domain. This domain uses the APRON
numerical analysis library to keep track of the range of values held
by llair variables where possible. This works by translating LLAIR
expressions into APRON tree expressions, so only handles the
subset of the LLAIR expression language that can be embedded.
Note also that function summarization is not yet implemented.
Future commits will add summarization and improve coverage of
LLAIR's expression language.
Reviewed By: jberdine
Differential Revision: D17763517
fbshipit-source-id: 826ce4cc5
Summary:
Add some theorems establishing the correspondence between the
implementation of the Convert operation in OCaml and the definition of
Convert in the semantics. Essentially, the OCaml version is in terms of
extracting certain ranges of bits, whereas the semantics is in terms of
integer arithmetic (addition, modulus, and exponentiation)
Reviewed By: jberdine
Differential Revision: D18113878
fbshipit-source-id: c318596d0
Summary:
This commit adds truncation, sign extension and zero extension to LLVM
and the Convert instruction to LLAIR.
The LLVM instructions use HOL's build-in word/int and word/num
conversions. Sanity-checking theorems prove that zero-extending leaves
the value of the word unchanged when considered as an unsigned value,
and that sign-extending leaves the value unchanged when considered as a
signed value.
The llair semantics for Convert uses the truncate_2comp function which
converts an integer to another integer as though they were represented
in 2's complement. e.g. truncate_2comp 255 16 = 255, truncate_2comp
255 8 = -1, truncate_2comp -3 2 = 1
Reviewed By: jberdine
Differential Revision: D18058833
fbshipit-source-id: df9de480c
Summary:
The old syntactic invariant in prog_ok was in the wrong direction,
saying that all labels in a phi instruction have to exist, rather than
saying that when we jump to a new block, the label of the block we came
from must be in all of the phi instructions.
Reviewed By: jberdine
Differential Revision: D18058832
fbshipit-source-id: d2ad33b04
Summary:
This required some minor tweaks to how the semantics encode values into
and out of byte lists. The remaining problems have to do with how LLVM
globals are translated into llair. At the moment, llair semantic's state
keeps a mapping for globals to their addresses, following the LLVM
semantics. However, it is not used because the translation (following
the code in frontend.ml) translates LLVM globals into llair locals,
which the llair semantics isn't set up to handle.
Reviewed By: jberdine
Differential Revision: D17930787
fbshipit-source-id: 06c6368e0
Summary:
The Used globals (pre-)analysis produces results queried by
Control. This diff adds a type definition for these and moves the
query into the Used_globals module.
Reviewed By: bennostein
Differential Revision: D17856879
fbshipit-source-id: 0211b82d7
Summary:
To avoid code explosion, the frontend emits move instructions for
expressions with more than one use. This diff relaxes this slightly by
allowing duplication of casts.
Reviewed By: bennostein
Differential Revision: D17856384
fbshipit-source-id: 6f6c496ef
Summary:
The frontend translation of exceptional control flow is untrusted
enough that it makes sense to disable it by default.
Reviewed By: bennostein
Differential Revision: D16061018
fbshipit-source-id: 65dca36ae
Summary:
The CFG of a function is implicit in the blocks themselves, so it is
possible to remove the explicit represention as a vector of
blocks. The only uses are fold or iter, and since the cycles are
detected during construction, these can be simple depth-first
traversals.
Reviewed By: bennostein
Differential Revision: D17821845
fbshipit-source-id: fc7a02151
Summary:
Fix a bug where the actual return variable was not scoped correctly in
cases where its name clashed with a local or formal of the
callee. Also comment and simplify to attempt to make more
understandable.
Reviewed By: bennostein
Differential Revision: D17801944
fbshipit-source-id: 286739241
Summary:
Some code that is otherwise benignly scalar still uses the
ExtractElement and InsertElement vector operations, so translate them
as if they were array operations.
Reviewed By: ngorogiannis
Differential Revision: D17801949
fbshipit-source-id: 89f3666bd
Summary:
Previously, the LLVM semantics could be stuck where the LLAIR semantics
was not yet stuck, but would become stuck (at the same place) after
taking a step. This was due to LLVM using the traditional definition of
stuck states: any state from which there are no transitions. However,
LLAIR cannot do that because it might get stuck in the middle of a block
that contains several visible stores. We don't want to consider the
whole block stuck, nor can we finish it. Thus, the LLAIR definition of
stuckness is when the state has the stuck flag set which happens when
stopping in the middle of a block after encountering a stuck
instruction. Now LLVM takes the same approach.
Reviewed By: jberdine
Differential Revision: D17855085
fbshipit-source-id: a094d25d5
Summary:
Add an argument to the Exit instruction. Update the LLVM semantics to
execute the Exit instruction and store the result in an "exited"
component of the state. (Previously it just noticed that it was stuck
about to do an Exit.)
With exiting treated uniformly, now in the proof that for every LLVM
trace, there is a llair trace that simulates it, all of the cheats
except for 1 are just cases that I haven't got to yet. However, the last
cheat is for the situation where the LLVM program gets stuck and the
llair program doesn't. For example, the following two line LLVM program
gets stuck because r2 is not assigned (ignoring for the moment the static
restriction that LLVM is in SSA form).
r1 := r2
Exit(0)
The compilation to llair omits the assignment and so we get a llair
program that doesn't get stuck:
Exit(0)
The key question is whether the static restrictions are sufficient to
ensure that no expression that might be omitted can get stuck.
Reviewed By: jberdine
Differential Revision: D17737589
fbshipit-source-id: bc6c01a1b
Summary:
If the LLVM to llair translation keeps a mapping from register r to
expression e, then for each register r' mentioned in e, there must be an
assignment to r' that dominates the entire live range of r. Thus, where
ever r might be replaced by e, the value of r' will be the same as it
was when the initial assignment to r occurred. Maintaining this
invariant relies on the LLVM being in SSA form.
Reviewed By: jberdine
Differential Revision: D17710288
fbshipit-source-id: fd3eaa57d
Summary:
This is work in progress; many of the cheats aren't true. In particular,
the definition of stuck/complete/partial traces in LLVM and llair don't
quite match up and need some modification. Also, the state relation
isn't strong enough; it will need to include information about registers
used in the expressions of the LLVM register to llair expression
mapping. But the overall shape of the proof is ok and so it can be
used to poke at various local aspects of the translation, such as
individual instructions.
Reviewed By: jberdine
Differential Revision: D17631604
fbshipit-source-id: 743b5d64d
Summary:
By some unfortunate logic, OCaml often decides to use
`sexp_list`/`sexp_option` instead of just `list`/`option`. Sometimes
these get copy/pasted in interface files.
It would be good to tell OCaml not to do that in the first place but in
the meantime: this diff.
Reviewed By: ngorogiannis
Differential Revision: D17907938
fbshipit-source-id: 7546834a2
Summary:
For test scripting purposes, when the analysis finishes successfully,
report the number of alarms.
Reviewed By: ngorogiannis
Differential Revision: D17801947
fbshipit-source-id: 1660866df
Summary:
In a spec, it currently may be that foot.us does not contain xs. So
exec_specs needs to extend the vocabulary of foot before existentially
quantifying out xs.
Reviewed By: ngorogiannis
Differential Revision: D17801933
fbshipit-source-id: 7b4b9262a
Summary:
Previously it was added to the locals before calling Dom.call, but
this results in the scope of freturn ending too early.
Reviewed By: ngorogiannis
Differential Revision: D17801939
fbshipit-source-id: 739ec8981
Summary:
Some globals have 'appending' linkage, where linking modules results
in appending the arrays from each module. These can appear even when
empty, leading to useless and somewhat troublesome 0-length arrays. So
drop them.
Reviewed By: ngorogiannis
Differential Revision: D17801927
fbshipit-source-id: d2dc180d7
Summary:
While BitCasts are the identity function on the bitwise
representation, they are not necessarily so in the semantics or the
logical representation. So be more conservative about eliding them in
the Exp language. Those that are actually semantic identities are
still omitted in the Term language.
Reviewed By: ngorogiannis
Differential Revision: D17801950
fbshipit-source-id: bf9ae57b5
Summary:
The analyzer (currently) hard-codes some assumptions about sizes of
basic types such as Typ.bool, Typ.siz, etc. Check that these
assumptions are satisfied by the input llvm datalayout, and give
reasonable error messages otherwise.
Reviewed By: ngorogiannis
Differential Revision: D17801941
fbshipit-source-id: 4fe484ee0
Summary:
Now that expression types and type sizes can be computed, it is not
necessary to store the sizes of globals separately.
Reviewed By: ngorogiannis
Differential Revision: D17801932
fbshipit-source-id: f746e506b
Summary:
- The `Llvm_target.DataLayout.size_in_bits` needs to be used for checking casts
e.g. it is ok to `bitcast <16 x i1> to i16`: they both have 16 bits, but they have sizes 16 vs 2 bytes
- The `Llvm_target.DataLayout.abi_size` needs to be used for the size of memory blocks containing values
e.g. for the size of memory segments containing the initial values of globals
- The example above shows that we can't compute the byte size from the bit size without knowing the target specific datalayout
- So we need both in each sized type
- Also add checks that Convert exps and terms are not no-ops
- Simplifications of size manipulating code
Reviewed By: ngorogiannis
Differential Revision: D17801928
fbshipit-source-id: 8c8ce6128
Summary:
In order to type-check casts, it is necessary to have the size of each
sized type. This size information is also useful in a few other places.
Reviewed By: bennostein
Differential Revision: D17801931
fbshipit-source-id: f8ef53276
Summary:
This is needed since expressions distinguish between the integer or
pointer zero value and zero-initialized array/tuple/struct aggregates
based on type, and the backend distinguishes them semantically.
Reviewed By: bennostein
Differential Revision: D17801938
fbshipit-source-id: ac8665e65
Summary:
Linking can lead to opaque types becoming identified with a known
types. Assertions in various places that types should be sized can be
triggered by such opaque types. Until there is a distinction between
processing fully-linked versus incomplete code, these checks need to
be relaxed to permit opaque types where sized ones are expected.
Reviewed By: bennostein
Differential Revision: D17801929
fbshipit-source-id: c5e62f7c8
Summary: Integer terms need to compare higher than any monomial.
Reviewed By: bennostein
Differential Revision: D17725607
fbshipit-source-id: c64fd52d5
Summary:
Also weaken definition of Typ.castable to permit casting between
floats and ints of the same size.
Reviewed By: bennostein
Differential Revision: D17725611
fbshipit-source-id: 5e8114e26
Summary:
Typ.equivalent is currently defined the same as Typ.castable, but
conceptually they are different and castable needs to be
weakened. They are different since for example it is possible to cast
from an i64 to a f64, but those types denote different sets of values
in the semantics, and the bitcast is modeled using a conversion
function.
Reviewed By: bennostein
Differential Revision: D17725615
fbshipit-source-id: 973574f2a
Summary:
For function calls where the callee is a cast expression, previous the
wrong type would be used for the callee. This could lead to crashes in
llvm, or asserting in sledge.
Reviewed By: bennostein
Differential Revision: D17725610
fbshipit-source-id: 938b49a49
Summary:
Some called functions are represented in llvm as a global variable
with e.g. external linkage, and so they do not appear as
'functions'. It is still valid to call such functions, though the
analyzer does not know their definitions.
Reviewed By: bennostein
Differential Revision: D17725609
fbshipit-source-id: 333d19c0d
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:
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:
Since the correcteness of the mapping from LLVM to llair depends on
LLVM being SSA, we need to formalise what that means. We also prove that
the domination relation is a strict partial order, which will probably
be helpful when reasoning about the translation.
Reviewed By: jberdine
Differential Revision: D17631456
fbshipit-source-id: a00eb3f87
Summary:
The LLVM semantics and translation was not consistently treating the
1-bit word value condition as signed or unsigned.
Reviewed By: jberdine
Differential Revision: D17605766
fbshipit-source-id: 77edf63b7
Summary:
Previously the LLVM semantics did the phi instructions at the head of a
block as part of executing the branch into that block. This looked a bit
weird, but had the advantage that the semantics knew which block was
being jumped from, which is necessary to run the phi instructions.
However, it meant that the rules for doing phi instructions would need
to show up with each branching construct. It was also annoying for the
LLVM->llair proof, since the phis are removed and their effect happens as
a distinct step from the branch.
Here we add a distinct Phi_ip instruction pointer to indicate that the
phi instructions at the start of the block should execute next, and then
be incremented to the usual numeric instruction pointer that points to
the non-phi instructions. The Phi_ip contains the identity of the
previous block.
Reviewed By: jberdine
Differential Revision: D17452416
fbshipit-source-id: 78fef7cca
Summary:
Give the llair semantics observable side effects (writes to global
variables) and a semantic function mirroring the LLVM semantics. Start
sketching out the LLVM/llair translation equivalence proof in a top-down
way from the obvious statement of equality of the semantics.
Reviewed By: jberdine
Differential Revision: D17399654
fbshipit-source-id: 2170678a8
Summary:
The simple LLVM semantics steps one instruction at a time, but the
generated llair does whole blocks at a time, since many individual LLVM
instructions can become a single llair expression. We add a bigger-step
LLVM semantics that does whole blocks at a time (except that it also
stops at function calls, since those end blocks in llair). The steps in
this bigger-step semantics should be at the same granularity as the
llair steps, making it easier to verify the translation.
We add a notion of observation to the LLVM semantics (right now, just
global variable writes) and use that to define two top-level semantic
functions, which we prove to be equivalent.
Reviewed By: jberdine
Differential Revision: D17396016
fbshipit-source-id: ee632fb92
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:
This includes a few changes and corrections to the semantics, to support
the translation. This initial attempt to reason about LLVM -> llair
showed three things that needed repair in the semantics, in addition to
various bugs. We address them as follows.
Refactor llair semantics to have only a single kind of flat value:
integers that fit into specified bit widths. Operations on size values
(e.g., offsets, indices and the like) can just take an integer and
ignore its number of bits. Pointers can just be considered integers that
fit into a certain size given by the constant pointer_size. Later on we
can consider making this a parameter to the model.
Change the generic memory model interface to use numbers rather than
words as the generic encoding of a large value. This makes it more
useful for llair where words are not used.
Pay more careful attention to signed/unsigned issues. Neither LLVM nor
llair have a concept of signed vs unsigned value. Instead individual
operations interpret bit patterns in various ways, some of which are
ambiguous in the LLVM manual. For example, since getelementpointer's
indices are explicitly said to be interpreted as signed 2's complement,
we should probably do the same for insertvalue and extractvalue. However
it is not clear how the argument to alloca is to be interpreted. For now
we assume signed.
Reviewed By: jberdine
Differential Revision: D17164133
fbshipit-source-id: 31a8af635
Summary:
Not everything is here yet, and there is some confusion on what to do
about the size values. However, the semantics has the right general
shape and will be a nice starting point for thinking about the details.
Reviewed By: jberdine
Differential Revision: D17111041
fbshipit-source-id: cc75651c6
Summary:
The translation from LLVM to llair now builds expressions up across
blocks, following the implementation. This is easy to do because of the
dominance restrictions in SSA, but might be difficult to reason
about.
Reviewed By: jberdine
Differential Revision: D17111040
fbshipit-source-id: a8e99147d
Summary:
LLVM and llair have similar memory models, and we don't want to
duplicate any definitions or theorems. This adds a new memory model
theory which should be understandable in its own right. A heap is a
mapping from addresses to bytes, alongside a set of valid addresses, and
intervals that have been allocated already. Primitives are defined for
allocating and de-allocating as well as reading and writing chuncks of
bytes.
There is also a generic type of structured values, and functions for
converting them to/from byte arrays.
Reviewed By: jberdine
Differential Revision: D17074470
fbshipit-source-id: bdab6089f
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:
Each variable now contains its type, alongside its name. This is more
uniform than in LLVM, where the name is usually paired with a type, but
not always, for example, the register type of the result of an
extractvalue is left implicit.
Reviewed By: jberdine
Differential Revision: D16984630
fbshipit-source-id: 1c3bc4985
Summary:
HOL now lets us omit quotations on Datatypes and make them look more
like the other new-style HOL definitions.
Reviewed By: jberdine
Differential Revision: D16983934
fbshipit-source-id: f8ef3abb5
Summary:
This sketches out how translation can be approached. It is partially
based on the Sledge code.
For basic blocks, isn't based on the Sledge code, but just my own
thoughts as a starting point. Essentially, we are trying to build up
larger expressions, and so not assigning to temporary registers that
don't live past the end of the block. This does remove sharing, so a
fancier approach could check for multiple uses of end-of-block dead
registers, or look at the sizes of expressions. The approach should be
flexible enough to accommodate such changes.
Fix icmp syntax
Using finite maps is elegant in the semantics, but awkward for writing
the translation function. Refactor the mappings from labels to functions
and from labels to blocks to use association lists instead.
To remove phi nodes, the translation takes every edge in the control
flow graph and makes a new basic block that contains a single parallel
move instruction that corresponds to the action of the phi node of the
target block.
Reviewed By: jberdine
Differential Revision: D16831051
fbshipit-source-id: 005663e26
Summary:
The AST is not complete on expressions, but it should have most of the
important features.
The representation is in some ways very different from the OCaml
implementation, because the OCaml code uses mutation to build the CFG as
an actual pointer graph in memory, and also because the expression
representation is optimised for the backend. For the former, it should
be easy to see that the AST here is isomorphic, representing the CFG
with finite maps from block labels. The correspondence is less clear in
the latter case, but the point here is not to model or verify
implementation optimisations, but to give a semantics to llair as a
language.
Reviewed By: jberdine
Differential Revision: D16807132
fbshipit-source-id: b0f64b3ec
Summary:
Change loc_var (for local variable) to reg (for register) because
loc_var looks too much like a location tagged variable.
Reviewed By: jberdine
Differential Revision: D16827920
fbshipit-source-id: 5b11f1065
Summary:
There could very well still be bugs in the semantics, since the
invariant here doesn't say all that much, and it completely ignores
local registers. But most trivial things and typos are probably fixed.
Reviewed By: jberdine
Differential Revision: D16803281
fbshipit-source-id: 48ba2523b
Summary:
Made progress on the sanity checking lemma (that the step relation
preserves some simple invariants on the state). Proved the Ret
instruction case of the state invariant lemma. To do this, I fixed a few
bugs in the definition, and strengthened the invariants.
Reviewed By: jberdine
Differential Revision: D16786900
fbshipit-source-id: 6fa8cb170
Summary:
Global variables need allocating and initialising before the machine can
start. The definition here shouldn't constrain how and where they are
allocated. For example, they don't all need to have separate
allocations. We also tag allocated blocks so that the allocation for a
global can never be deallocated.
Start working on a sanity checking invariant on states.
Reviewed By: jberdine
Differential Revision: D16735068
fbshipit-source-id: 0d5e60e7a
Summary:
Start working on a simple model of LLVM with the ultimate goal of
handling relevant and/or tricky aspects of LLVM and LLAIR and then
formalising the translation from LLVM to LLAIR.
This is a complete initial model of everything that we are interested in
except for exceptions, which should be tricky. Also no thought has gone
into the treatment of poison and the undefined value, so the treatment
is naive, which is at least partially justified because we are
interested in the semantics of LLVM IR after the optimisation passes
have run.
Include some sanity checking theorems.
Reviewed By: jberdine
Differential Revision: D16731885
fbshipit-source-id: fd53949fe
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:
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:
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: And fix test Makefile to call the C++ compiler on .cpp files.
Reviewed By: kren1
Differential Revision: D15972426
fbshipit-source-id: 719de755f
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
Summary:
The entry block contains all locals of the entire function, as
required by the backend. This makes the manipulation of the locals of
each block redundant.
This diff moves the locals from the entry block to the function
itself, removes the Locals frames of the Control.Stack, and adds a
locals field to Return frames.
This is part cleanup and part preparation for removing the
Control.Stack.
Reviewed By: ngorogiannis
Differential Revision: D15963503
fbshipit-source-id: 523ebc260
Josh Berdine
Scott Owens
Benno Stein
Jules Villard
Timotej Kapus