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
Josh Berdine
Scott Owens
Benno Stein
Jules Villard