Summary:
Trace.infok is like Trace.info but accepts a polymorphic printf
continuation instead of directly taking a format string and its
args. This is useful to write wrappers such as:
```
let trace k = [%Trace.infok k]
```
Reviewed By: ngorogiannis
Differential Revision: D19221883
fbshipit-source-id: 88e939b26
Summary:
The size of Splats is redundant, as they always appear as subterms of
a Memory chunk or a heap segment, both of which are sized.
Reviewed By: ngorogiannis
Differential Revision: D19221870
fbshipit-source-id: 74044d1ad
Summary:
Now that they are uncurried, congruence closure does not need the
order of subterms to be preserved. Sorting them reduces redundancy in
case the same equality in different orders is encountered, and
improved printing.
Reviewed By: ngorogiannis
Differential Revision: D19221875
fbshipit-source-id: c6bf4ccad
Summary:
Equality.classes was assuming a simpler representation, and was
incomplete as a result.
The 'representative' map is not kept in a normalized form, where
subterms are necessarily representatives. Therefore, applying the
representative map to subterms of terms in a class can reveal new
elements of the class. This mirrors how the `lookup` function in
`normalize` works.
Reviewed By: ngorogiannis
Differential Revision: D19221868
fbshipit-source-id: 4a2ed6d3f
Summary:
Reduce redundancy by printing adjacent segments as if they had been
concatenated together.
Reviewed By: ngorogiannis
Differential Revision: D19221881
fbshipit-source-id: 613105864
Summary:
Also, previous code was sometimes inconsistent regarding whether to
enumerate all subterms or only toplevel terms.
Reviewed By: ngorogiannis
Differential Revision: D19221873
fbshipit-source-id: e8644098b
Summary: It is easier to understand the order of args with diff_inter.
Reviewed By: ngorogiannis
Differential Revision: D19221869
fbshipit-source-id: b29ac83c8
Summary:
Add some test cases from Reuss and Shankar for equality that are
mishandled by Shostak's original algorithm.
Reviewed By: ngorogiannis
Differential Revision: D19221880
fbshipit-source-id: a6f9d51e3
Summary:
This diff enables parsing and auto-formatting documentation
comments (aka docstrings).
I have looked at this entire diff and manually made some changes to
improve the formatting. In some cases it looked like it would take too
much time, or benefit from someone more familiar with the code doing
it, and I instead disabled auto-formatting docstrings in those files.
Also, there are some source files where the docstrings are invalid,
and some where the structure detected by the parser appears not to
match what was intended. Auto-formatting has been disabled for these
files.
Reviewed By: ezgicicek
Differential Revision: D18755888
fbshipit-source-id: 68d72465d
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
Josh Berdine
Scott Owens
Benno Stein