Summary:
Generalize the existing find_or_add and find_and_remove operations to
find_update. Slightly simplify the interfaces of change, update,
find_or_add, and find_and_remove, reducing the gap to the natural
underlying functionality.
Reviewed By: jvillard
Differential Revision: D26451305
fbshipit-source-id: 89f67c84d
Summary:
Update the first-order equality solver for the sequence theory to
avoid searching the whole representation now that the super-term index
is maintained.
Reviewed By: jvillard
Differential Revision: D26338015
fbshipit-source-id: 24a9a19b6
Summary:
Inline functor applications, principally those involved in the
representation of (arithmetic) terms. This enables direct calls to
functions in the result of functor applications, instead of indirect
via an offset from the start of the module block resulting from the
functor appication. This also then enables further inlining
opportunities.
Reviewed By: jvillard
Differential Revision: D26338016
fbshipit-source-id: 27b770fa3
Summary: Also add support for deriving compare, equal, and sexp.
Reviewed By: ngorogiannis
Differential Revision: D26250524
fbshipit-source-id: b47787a9c
Summary:
A comparer `('a, 'compare_a) t` for type `'a` is a "compare" function
of type `'a -> 'a -> int` tagged with a phantom type `'compare_a`
acting as a singleton type denoting an individual compare function.
The point of these is to enable writing type definitions of containers
that depend on a compare function prior to applying a functor. For
example, a type of sorted lists could be exposed as:
```
type elt
type (elt, 'compare_elt) t = private elt list
```
and the operations manipulating sorted lists would be defined by a
functor that accepts a `Comparer.S` and implements the operations
using
```
let compare = (comparer :> elt -> elt -> int)
```
Reviewed By: ngorogiannis
Differential Revision: D26250528
fbshipit-source-id: ea61844ec
Summary: No functional change, just to reduce diffs of upcoming changes.
Reviewed By: ngorogiannis
Differential Revision: D26250543
fbshipit-source-id: a14b6f4b0
Summary:
Sometimes symbols are added to the symbol table multiple times during
translation from LLVM to LLAIR. For example, this happens when a
`llvm.dbg.declare` instruction is encountered that attaches a debug
location to a symbol. Currently when this happens, the symbol name is
regenerated unnecessarily. This is not economical, and since counters
are used in some cases to avoid clashes, this can cause visible
changes to names.
This diff fixes this, and also makes the location update more robust
by not relying on the location added last being the best.
Reviewed By: jvillard
Differential Revision: D26250542
fbshipit-source-id: 5d52ce193
Summary:
Currently detection and propagation of consequences of newly added
equality constraints is implemented using some operations that
traverse the entire representation of the equality relation. This
implementation strategy makes it relatively easy and robust to ensure
that the consequences of constraints are treated in a sound and
complete way. It does have the drawback that adding a constraint
involves work that is proportional (nonlinearly even) to the number of
all constraints. This can become a performance bottleneck.
This diff reimplements the core operations using an additional data
structure that essentially tracks the "super-term" relation between
terms, which can be used to look up the existing constraints that
might be involved in deriving new consequences when adding
equalities. This means that adding new equalities no longer takes time
proportional to the size of the entire equality context
representation, but only to the number of existing constraints that
might interact with the new constraint. Also, rewriting terms
into canonical form no longer takes time proportional to size of the
whole context, but only performs table lookups on the subterms of the
term to canonize.
Reviewed By: jvillard
Differential Revision: D25883705
fbshipit-source-id: b3f266533
Summary:
This diff changes Context.extend to not only add terms and their
subterms to the carrier, but to simultaneously normalize the added
term. The normalized form is currently ignored, but it will be needed
when adding use lists.
Reviewed By: jvillard
Differential Revision: D25883709
fbshipit-source-id: bfe06f2a8
Summary:
Currently the equality classes are computed from the representatives
solution substitution when needed. This diff instead maintains them as
part of the representation of the context. By itself this does not
make a huge difference, but it is necessary to make other operations
incremental.
Reviewed By: jvillard
Differential Revision: D25883715
fbshipit-source-id: 1b444a0dc
Summary:
Composing two substitutions does not need to require that their
domains are disjoint.
Leave disjointness check for composing a single mapping just to check
expected usage.
Reviewed By: jvillard
Differential Revision: D25756557
fbshipit-source-id: 04e92b864
Summary:
The current implementation of Context.elim crudely removes oriented
equations from terms involving the given variables. This is easy to
use in a way that violates the representation invariants of Context,
as well as destroys completeness. This diff resolves this by making
Context.elim remove the desired variables by rearranging the existing
equality classes, in particular promoting a new representative term
when the existing representative is to be removed. Also, since this
basic approach is incomplete for interpreted terms, they are detected
and not removed. As a result, the interface changes to return the set
of variables that have been removed.
Reviewed By: jvillard
Differential Revision: D25756573
fbshipit-source-id: 0eead9281
Summary:
Revise the control-flow exploration scheduling algorithm to fix
several issues. The main difference is to change the priority queue to
keep the control edges on the frontier of exploration in sync with the
states that are waiting to be propagated. This fixes several sorts of
issue where the decision of which control and state joins to perform
was unexpected / wrong. Part of keeping the frontier edges and waiting
states in sync is that the waiting states are associated not only with
a destination block, but the stack of that block. This fixes several
issues.
Combined, these changes lead to the algorithm only attempting joins
for which the pointwise max join on depth maps is correct (with the
caveat of no mathematical proof yet).
Reviewed By: jvillard
Differential Revision: D25196733
fbshipit-source-id: db007fe1f
Summary:
Previously, when LLAIR was in SSA form, blocks took parameters just
like functions, and it was sometimes necessary to partially apply a
block to some of the parameters. For example, blocks to which function
calls return would need to accept the return value as an argument, and
sometimes immediately jump to another block passing the rest of the
arguments as well. These "trampoline" blocks were partial applications
of the eventual block to all but the final, return value,
argument.
This partial application mechanism meant that function parameters and
arguments were represented as a stack, with the first argument at the
bottom, that is, in reverse order.
Now that LLAIR is free of SSA, this confusion is no longer needed, and
this diff changes the representation of function formal parameters and
actual arguments to be in the natural order. This also brings Call
instructions in line with Intrinsic instructions, which will make
changing the handling of intrinsics from Calls to Intrinsic less
error-prone.
Reviewed By: jvillard
Differential Revision: D25146163
fbshipit-source-id: d3ed07a45
Summary:
These are not simply handled by `@deriving` since:
- These types are recursive and so some fields need to be ignored
- Some are uniquely identified by one of their fields
- Some fields are mutable, but set only during construction, and need
to be considered by compare, equal, hash, but ppx_hash refuses.
Reviewed By: jvillard
Differential Revision: D24989064
fbshipit-source-id: 7f8d699e5
Summary:
The use of realpath on paths obtained from debug info and the current
working directory is application-usage-specific behavior that does not
belong in the backend library. This diff moves these uses to the
frontend and cli, respectively. Also, the use of realpath in the
frontend is memoized along the same lines as the other frontend
translation functions.
This was also the last use of `core` in the `sledge` library, so the
dependency is moved to `sledge_cli` and `sledge_report`.
Reviewed By: ngorogiannis
Differential Revision: D24989070
fbshipit-source-id: c21b275f5
Summary:
This information is needed to mediate between index-based
operations (such as on records) and offset-based operations (such as
load/store). Since it is fragile to recompute, the approach here is to
query llvm during translation and store the result.
Reviewed By: jvillard
Differential Revision: D24772954
fbshipit-source-id: ad22c3ecf
Summary:
When exceptions are used due to the lack of goto, use `raise_notrace`
instead of `raise` to avoid the overhead of populating the backtrace.
Reviewed By: ngorogiannis
Differential Revision: D24630525
fbshipit-source-id: c5051d9c4
Summary:
Operations over the core representation are more useful in the core
representation modules.
Reviewed By: ngorogiannis
Differential Revision: D24532340
fbshipit-source-id: f1eab822d
Summary:
And add Monad.Make to implement the full interface from return and
bind.
Reviewed By: ngorogiannis
Differential Revision: D24532341
fbshipit-source-id: 5740ba1c2
Summary: Simplify output of arithmetic terms, and omit trivial pure part of Sh.
Reviewed By: jvillard
Differential Revision: D24371082
fbshipit-source-id: 91f2117d3
Summary:
Change the type of `fold` functions to enable them to compose
better. The guiding reasoning behind using types such as:
```
val fold : 'a t -> 's -> f:('a -> 's -> 's) -> 's
```
is:
1. The function argument should be labeled. This is so that it can be
reordered relative to the others, since it is often a multi-line
`fun` expression.
2. The function argument should come last. This enables its
arguments (which are often polymorphic) to benefit from type-based
disambiguation information determined by the types of the other
arguments at the call sites.
3. The function argument's type should produce an
accumulator-transformer when partially-applied. That is,
`f x : 's -> 's`. This composes well with other functions designed
to produce transformers/endofunctions when partially applied, and
in particular improves the common case of composing folds into
"state-passing style" code.
4. The fold function itself should produce an accumulator-transformer
when partially applied. So `'a t -> 's -> f:_ -> 's` rather than
`'s -> 'a t -> f:_ -> 's` or `'a t -> init:'s -> f:_ -> 's` etc.
Reviewed By: jvillard
Differential Revision: D24306063
fbshipit-source-id: 13bd8bbee
Summary:
The changes in set_intf.ml dictate the rest. The previous API
minimized changes when changing the backing implementation. But that
API is hostile toward composition, partial application, and
state-passing style code.
Reviewed By: jvillard
Differential Revision: D24306089
fbshipit-source-id: 00a09f486
Josh Berdine