Summary:
This warning (68) triggers when a function argument pattern depends on
mutable state, which prevents the remaining arguments from being
uncurried, causing additional closure allocations.
Reviewed By: jvillard
Differential Revision: D27188311
fbshipit-source-id: a43354e15
Summary:
Not all types of exceptions allowed by LLVM are currently
supported. The types of Resume args and LandingPad params must be
compatible, and so it only makes sense to check they the same
way.
Reviewed By: jvillard
Differential Revision: D27188307
fbshipit-source-id: c88cc46d0
Summary:
It is possible for the filename of a source location to be the empty
string. Fpath.v asserts when passed an empty string.
Reviewed By: jvillard
Differential Revision: D27188304
fbshipit-source-id: a7d73444b
Summary:
This script interoperates with the gllvm wrapper for clang that embeds
bitcode into native object files to support linking closed bitcode for
executables built with gllvm, also linking in the bitcode of needed
dynamic libraries.
Reviewed By: ngorogiannis
Differential Revision: D26903126
fbshipit-source-id: d4b95809a
Summary:
The only difference between `program` and `identified` variables is
terminology, technically they are redundant.
Reviewed By: jvillard
Differential Revision: D26451308
fbshipit-source-id: eb4e7be43
Summary:
Negating the ids of program variables leads to inverting the order on
them. This is logically fine, the order is still a valid total order.
But it can lead to choosing younger variables as equality class
representatives over older variables, and thereby lead to more churn
as adding an equality is more likely to cause a change of
representative, and hence additional normalizing rewrites.
Reviewed By: jvillard
Differential Revision: D26451304
fbshipit-source-id: eb20d1901
Summary:
It is not necessary to clear tables and sets that do not contain any
pointers to LLVM values.
Reviewed By: jvillard
Differential Revision: D26451306
fbshipit-source-id: 403c588fb
Summary:
Theory.solved is a list of pairs of terms representing solved
equalities. The order of the pairs is very important, which is not
apparent from the type. This diff introduces an oriented_equality type
to make this more clear.
Reviewed By: jvillard
Differential Revision: D26451303
fbshipit-source-id: 56a49e601
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:
The normalization and then extension of the carrier can be combined
into one pass. This weakens the property that this normalization needs
to achieve, which yields a small simplification, and combining the
passes is a minor optimization.
Reviewed By: jvillard
Differential Revision: D26400406
fbshipit-source-id: 8a3cbb2de
Summary:
An invariant of `And` and `Or` formulas is that they are flattened,
that is, `And` formulas do not have positive immediate subformulas of
form `And` nor negative immediate subformulas of form `Or`, and
similarly for `Or`. This invariant is ensured by the formula
constructors, which scan the immediate subformulas for cases that need
to be flattened.
When mapping over formulas, this repeated scanning is a performance
bottleneck. Most of the work of flattening is wasted since the input
formulas are necessarily already in flattened form, and the common
case is that the transformation preserves the flattened form. This
diff optimizes this case by detecting violations of flattening during
the transformation, performing the needed flattening, and avoiding the
general constructor that scans for flattening violations.
Reviewed By: jvillard
Differential Revision: D26338014
fbshipit-source-id: 9f15cca58
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:
Similarly to terms, use the Comparar interface of Sets to defined
formulas using recursive types instead of recursive modules.
Reviewed By: jvillard
Differential Revision: D26250512
fbshipit-source-id: 84f0ae8c0
Summary: No functional change, just to make the interface easier to read
Reviewed By: jvillard
Differential Revision: D26250513
fbshipit-source-id: f3b07bccc
Summary:
Terms include Arithmetic terms, which are polynomials over terms
themselves. Monomials are represented as maps from
terms (multiplicative factors) to integers (their powers). Polynomials
are represented as maps from monomials (indeterminates) to
rationals (coefficients). In particular, terms are represented using
maps whose keys are terms themselves. This is currently implemented
using recursive modules.
This diff uses the Comparer-based interface of Maps to express this
cycle as recursive *types* rather than recursive *modules*, see the
very beginning of trm.ml. The rest of the changes are driven by the
need to expose the Arithmetic.t type at toplevel, outside the functor
that defines the arithmetic operations, and changes to stage the
definition of term and polynomial operations to remove unnecessary
recursion.
One might hope that these changes are just moving code around, but due
to how recursive modules are implemented, this refactoring is
motivated by performance profiling. In every cycle between recursive
modules, at least one of the modules must be "safe". A "safe" module
is one where all exposed values have function type. This allows the
compiler to initialize that module with functions that immediately
raise an exception, define the other modules using it, and then tie
the recursive knot by backpatching the safe module with the actual
functions at the end. This implementation works, but has the
consequence that the compiler must treat calls to functions of safe
recursive modules as indirect calls to unknown functions. This means
that they are not inlined or even called by symbol, and instead
calling them involves spilling registers if needed, loading their
address from memory, calling them by address, and restoring any
spilled registers. For operations like Trm.compare that are a handful
of instructions on the hot path, this is a significant
difference. Since terms are the keys of maps and sets in the core of
the first-order equality solver, those map operations are very very
hot.
Reviewed By: jvillard
Differential Revision: D26250533
fbshipit-source-id: f79334c68
Summary:
No functional change, apart from a minor change in invariant checking
for core constructors. Only to reduce diffs of upcoming changes.
Reviewed By: jvillard
Differential Revision: D26250518
fbshipit-source-id: a731e4fd6
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: `make debug` should not be the same as `make release`
Reviewed By: ngorogiannis
Differential Revision: D26451307
fbshipit-source-id: 1bf924f92
Summary: No functional change, just to reduce diffs of upcoming changes.
Reviewed By: ngorogiannis
Differential Revision: D26250543
fbshipit-source-id: a14b6f4b0
Summary:
Currently there is a direct cycle of dependencies Var -> Trm ->
Var. Inside Trm, these two modules are defined as mutually recursive
modules, so at some level this is ok. Due to internals of how
recursive modules are compiled, recursive modules that are
"unsafe" (that is, export some value of non-function type) are
compiled more efficiently. This diff moves Var from being defined
recursively with Trm to being a submodule of Trm. This eliminates that
Var -> Trm -> Var cycle and enables making Trm an "unsafe"
module. (Trm is still mutually recursive with Arith (and Arith0), but
they are "safe".)
The difference between how "safe" and "unsafe" recursive modules are
compiled, in this context, is that the safe ones are first initialized
to a block containing dummy function closures that immediately raise,
then the unsafe ones are initialized as normal modules, and then the
safe ones are back-patched. A consequence of this is that calls to
functions in safe recursive modules are "unknown" calls, and they are
implemented as loading from a pointer to a closure and calling the
generic caml_apply function. In contrast, calls to functions in normal
or "unsafe" modules can be known, and get compiled to direct assembly
calls to the statically resolved callee. The second case is
faster. Additionally, in the indirect case, the callee is unknown, and
so some register spilling and restoring is also potentially
involved. Normally (I guess), this difference in performance is not
significant, but it can be significant for e.g. compare or hash
functions of modules used as container keys / elements, where the
container data structure is very hot.
Reviewed By: ngorogiannis
Differential Revision: D26250517
fbshipit-source-id: ecef49b32
Summary:
Variable ids are currently unique non-negative integers, and register
ids are unique positive integers, so using register ids negated as
variable ids yields a situation where all variable ids are unique.
Reviewed By: jvillard
Differential Revision: D26250544
fbshipit-source-id: 9e47e9776
Summary:
The names of instructions that produce void results, other than Call
instructions, are not used. So do not consume ids for them.
There are actually very many of these, so the saved work during
translation can be significant.
Reviewed By: jvillard
Differential Revision: D26250529
fbshipit-source-id: f9eea5684
Summary:
The source block name is normally visible in the LLAIR code, while the
name of e.g. a branch instruction is some internal number. This change
only makes the output LLAIR code slightly easier to read.
Reviewed By: jvillard
Differential Revision: D26250521
fbshipit-source-id: 4723a58f7
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:
`Sh.and_ b q` normalizes `b` using the equality context of `q` and
then conjoins the result to `q`. This is incorrect in case normalizing
`b` results in expressing it using existentials of `q`, which takes
the existentials out of their scope. So this diff changes from
essentially
`(∃x.Q) ∧ B = (∃x.Q) ∧ (∃x.Bρ)`
to
`(∃x.Q) ∧ B = (∃x'.Q[x'/x] ∧ Bρ)`
where `ρ` is the substitution that normalizes with respect to the
equality context.
Reviewed By: jvillard
Differential Revision: D26250536
fbshipit-source-id: 05f5c48c0
Summary:
Add assertion to detect if the variable a function call modifies
appears in the actual parameters. In this case, the implementation is
incomplete.
Reviewed By: jvillard
Differential Revision: D26250527
fbshipit-source-id: d2e81a467
Summary:
Instructions and terminators are not themselves unique, there can be
two instructions that compare equal in distinct blocks, and likewise
for terminators. Such clashes make the coverage statistics report
incorrectly low coverage. This diff fixes this by also considering the
parent blocks.
Reviewed By: jvillard
Differential Revision: D26250514
fbshipit-source-id: 93f916eab
Summary:
Instead of passing the Var.strength across interfaces, pass the Trm.pp
partially applied to the Var.strength. This hides the type of
Var.strength, and thereby removes the need for `Arithmetic.S.var`.
Reviewed By: jvillard
Differential Revision: D26250516
fbshipit-source-id: 64dbd3870
Summary: The wrapper functions do not get inlined enough to avoid excess allocations.
Reviewed By: jvillard
Differential Revision: D25946110
fbshipit-source-id: 8dc3d8259
Summary:
This diff replaces Fml.fold_dnf, which eagerly enumerates a
disjunctive-normal form expansion, with iter_dnf which can be iterated
lazily. Fml.iter_dnf is then used in Context.dnf. This means that the
full DNF expansion does not need to be allocated by
e.g. Smtlib.check_sat, which yields huge peak memory savings.
Reviewed By: jvillard
Differential Revision: D25946111
fbshipit-source-id: e6d179e9f
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:
Context.solve_uninterp_eqs uses `not Theory.is_interpreted` where
`Theory.is_noninterpreted` is more correct, since it operates on terms
that are class elements, which cannot be `Z _ | Q _ | Concat [||]`.
Reviewed By: jvillard
Differential Revision: D25883732
fbshipit-source-id: 5d060b338
Summary:
Currently `not Theory.is_interpreted` is used to terms should be added
to classes, or delayed to pending equations. This diff changes this to
use `Theory.is_noninterpreted` instead. They only differ on `Z _ | Q _
| Concat [||]`, which do not make it to this test, and
`is_noninterpreted` is more correct since classes may only contain
solvables.
Reviewed By: jvillard
Differential Revision: D25883706
fbshipit-source-id: 3b7b94065
Summary:
Use Theory.solvable_trms for a minor strengthening and simplification
of Context.is_valid_eq.
Reviewed By: jvillard
Differential Revision: D25883735
fbshipit-source-id: 3d0f3fcfe
Summary:
The current Context.max_solvables differs from Theory.solvables in
that it incorrectly includes `Z _ | Q _ | Concat [||]` terms.
Reviewed By: jvillard
Differential Revision: D25883728
fbshipit-source-id: f39f67622
Summary:
Currently when Arith.map encounters a noninterpreted polynomial, it
does not descend to its subterms. This diff fixes this bug, and
documents that the `map` and `trms` operations agree on the set of
subterms.
Reviewed By: jvillard
Differential Revision: D25883725
fbshipit-source-id: 1dc06f1fc
Summary:
For arithmetic terms that are a single monomial, Arith.trms is
currently the singleton iterator containing the term itself. In
particular, Arith.trms is not the *sub*terms in this case. In this
case the principal constructor is multiplication. This diff fixes
these cases and defines Arith.trms to contain the factors of a
singleton monomial.
Reviewed By: jvillard
Differential Revision: D25883719
fbshipit-source-id: a88611bba
Summary:
No functional change. Mostly reorder definitions. Add some
tracing. Some documentation improvement. Remove a few unneeded
identifiers in patterns.
Reviewed By: jvillard
Differential Revision: D25883712
fbshipit-source-id: 1449a7f54
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:
The solver for single equations no longer needs access to the internal
representation of the context.
Reviewed By: jvillard
Differential Revision: D25883722
fbshipit-source-id: 4ccd97674
Summary:
When `no_fresh` is true, then no fresh variables will be generated
while solving. So it is not necessary to provide a set with respect to
which variables must be generated fresh.
Reviewed By: jvillard
Differential Revision: D25883724
fbshipit-source-id: fd886067f
Summary:
Currently when solving an equation requires solving one or more other
equations, they are handled recursively. This diff reworks the solver
to instead queue pending equations in a list rather than eagerly
solving them eagerly. The pending list will be needed when changing
the Context.t representation since some equations will need to be
delayed until representation invariants are re-established.
Additionally, the solution is accumulated as an association list
rather than being eagerly incorporated into the context
representation. This enables the uses in equality solving and
quantifier elimination to use different representations.
Reviewed By: jvillard
Differential Revision: D25883727
fbshipit-source-id: 2f6b5efa3
Summary:
When used by the first-order solver, solve_extract may generate fresh
variables to express the solution substitutions, but when used by
quantifier elimination via solve_for_vars, fresh variables should not
be generated. This diff makes the difference between these use cases
simpler and clearer by replacing the obscure filter predicate argument
that is passed eventually to compose1 with a boolean indicating
whether fresh variables may be generated.
Reviewed By: jvillard
Differential Revision: D25756562
fbshipit-source-id: 53a35b71c
Summary:
Context.solve_for_vars returns a solution substitution consisting of
oriented equalities that are implied by the given context. It is
logically valid to express these equations using terms that are
normalized with respect to the solution substitution itself. This diff
normalizes uninterpreted terms with the solution substitution when
extending it. This preserves the logical strength of the solutions,
and strengthens other purely syntactic operations on the substitution,
such as Context.Subst.is_valid_eq.
Reviewed By: jvillard
Differential Revision: D25756582
fbshipit-source-id: cd997c46b
Summary:
- Fix clamping of percentage change of memory quantities
- Improve sorting of coverage changes relative to unchanged error
results
- Filter out results for invalid LLVM code
- Fix printing multiple status values
- Fix passing args to sledge, different subcommands need different
args
- Fix cleaning commands
- Add an unknown error status to the report if sledge exits without
producing a status in the report
- Internalize globals for tests, as otherwise C++ tests are unreadable
due to the runtime system models
Reviewed By: jvillard
Differential Revision: D25756567
fbshipit-source-id: 3b4c003f4
Summary:
The ~20% hit in compilation time is dominated by the time saved
running the tests. This also makes the memory allocation numbers more
robust to inconsequential changes. Note that `make check` is still
fast.
Note that normally dune passes `-g` to ocamlopt itself, but not if the
build profile includes an `ocamlopt_flags` entry. So add it explicitly
to ensure that compilation includes debug symbols.
(Also remove `-error-style short` that was missed in 9c4f263.)
Reviewed By: jvillard
Differential Revision: D25756570
fbshipit-source-id: 94d18bac2
Summary:
When a stem has an occurrence of an existential, say x, and x is
substituted out by different witnesses, say a and b, in two disjuncts,
then the connection to other occurrences of a and b are lost.
This diff fixes this problem by propagating the solved variables that
survive normalization down to subformulas, and not removing those
variables from subformulas.
Reviewed By: jvillard
Differential Revision: D25756583
fbshipit-source-id: dabda743f
Summary:
Trade a bit more code for lowering complexity from linear to
logarithmic.
Reviewed By: jvillard
Differential Revision: D25756569
fbshipit-source-id: 83ad575fe
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 overall operation of the quantifier elimination algorithm in
Sh.simplify is to first descend through the disjunctive structure of a
symbolic heap formula, process the leaves, and then proceed back up
the formula. At each point on the way back up, the first-order solver
is used to compute a solution substitution representing witnesses of
existential variables. This substitution is then used to normalize the
entire subformula at that point. Note that this results in
substituting and normalizing each subformula a number of times
proportional to its depth in the disjunctive structure.
This diff removes this redundancy and substitutes through each
subformula once. This is done by changing from an overall bottom-up to
top-down algorithm, and involves composing solution substitutions
rather than substituting multiple times. This change also heavily
relies on the strengthened Context.apply_and_elim operation, where the
bottom-up many-substitutions approach relies on the internal details
of repeated substitutions.
Reviewed By: jvillard
Differential Revision: D25756549
fbshipit-source-id: ca7cd814a
Summary:
The current implementation of quantifier elimination in Sh.simplify is
tightly coupled with the details of what the Context operations
support. In particular, successfully eliminating variables with
Context.elim effectively relies on being given a context that has been
transformed by Context.apply_subst. These operations are sound
independently, but achieving the desired result is delicate.
To simplify this situation, this diff refactors the tightly coupled
usage into a Context.apply_and_elim operation that hides the details
of the interaction inside the Context module. This enables an accurate
specification of apply_and_elim to be given much more simply than can
be done for the separate operations. This also simplifies the
implementation of Sh.simplify.
Reviewed By: jvillard
Differential Revision: D25756577
fbshipit-source-id: b344b3da6
Summary:
The implementation of quantifier elimination in Sh.simplify currently
relies on a subtle implementation detail of Context.apply_subst to
remove some identity mappings. Now that Context.elim has been
strengthened and generalized, it can be used to to give a much clearer
implementation, that is also more robust to representation changes in
Context.
Reviewed By: jvillard
Differential Revision: D25756554
fbshipit-source-id: 6be0de2f3
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:
Context.fold_uses_of should enumerate the transitive subterms of a
term rather than only the immediate subterms.
Reviewed By: jvillard
Differential Revision: D25756553
fbshipit-source-id: a3911d9f5
Summary:
Previously Sh had a representation invariant which ensured that
existentials of a subformula did not shadow universals of its
superformulas. The current implementation of Sh.freshen_nested_xs
mistakenly still assumes this invariant, but it no longer holds. This
diff fixes freshen_nested_xs to freshen nested existentials with
respect to not only ancestor universals in addition to existentials.
Reviewed By: jvillard
Differential Revision: D25756551
fbshipit-source-id: 54c48b067
Summary:
Sh.simplify propagates first-order constraints over the formula's
propositional structure, and can reveal inconsistency. It is therefore
sometimes beneficial to check consistency after simplifying rather
than before.
Reviewed By: jvillard
Differential Revision: D25756585
fbshipit-source-id: 2a205c965
Summary:
Simplifying a symbolic heap can reveal inconsistencies, either of
individual disjuncts or (therefore) of toplevel formulas. This is due
to the first-order contexts being propagated from a formula to its
descendents, and for the intersection of the contexts of disjunctions
being propagated to their parent. The later stages of eliminating
redundant quantifiers, etc. do not reveal further
inconsistencies. Therefore this diff moves the inconsistency detection
earlier, to just after the contexts are strengthened. This is clearer,
and also a minor optimization.
Reviewed By: jvillard
Differential Revision: D25756564
fbshipit-source-id: d3acf875b
Summary:
Sh operations usually detect inconsistency where needed. But some
operations such as Context.inter must treat the unsat case
specially. This diff increases robustness by not relying on Sh to
detect inconsistency in order to get the correct context or pure
constraints, or to use the fast-paths through Context or Formula
operations.
Reviewed By: jvillard
Differential Revision: D25756550
fbshipit-source-id: 091439ff6
Summary:
Sh.is_false checks if the pure constraints are inconsistent with the
first-order consequences of the spatial constraints. This involves
some, though not very expensive, logical reasoning. But is it not
checking only testing for the representation of Sh.false_, which one
might expect from its name. This renaming also makes room for the
operation that does test for the representation of Sh.false_.
Reviewed By: jvillard
Differential Revision: D25756580
fbshipit-source-id: 30510f45a
Summary:
Context.apply_subst erroneously resets everything in the
representation of a context except the solution substitution when
applying a substitution.
Reviewed By: jvillard
Differential Revision: D25756548
fbshipit-source-id: 949a34ced
Summary:
This is a simple CFG transformation that compresses jumps to jumps
into jumps to the final destination. LLVM's simplifycfg pass seemingly
should have eliminated these, but does not.
Reviewed By: jvillard
Differential Revision: D25196728
fbshipit-source-id: 3288dbd8d
Summary:
Currently the symbolic execution options, obtained from the command
line flags and preanalysis, are passed to the Control entry points as
a record, and then passed around within Control as needed. This diff
simplifies the code in Control by replacing the record mechanism with
an additional functor parameter containing the options. The main
benefit is that the bound option no longer needs to be part of the
analysis state.
This change does make the code in Sledge_cli slightly more
complicated, as it now performs a functor application using a
first-class module computed from the command line flags.
Reviewed By: jvillard
Differential Revision: D25196735
fbshipit-source-id: 80e5d5d62
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:
The first-order solver sometimes needs to generate fresh variables to
express the solution of equations. It needs to ensure that these
generated variables do not clash. Before this diff, there was a
confusion where new variables were fresh with respect to only the
current set of "universal" variables. This is wrong, and this diff
adds the full set of variables instead.
Reviewed By: jvillard
Differential Revision: D25196732
fbshipit-source-id: afc56834a
Summary:
It can happen that the actual return variable, which is the name of
the variable in the caller's scope that receives the returned value,
clashes with the formals of the callee. The scope of the return
formula was wrong in this case, as the actual return was outscoped via
existential quantification with the rest of the formals after the
return values was passed.
Reviewed By: jvillard
Differential Revision: D25196727
fbshipit-source-id: 94cf25418
Summary:
A context with valid but extraneous equations was being kept. The
extra equations are valid, but might violate vocabulary invariants.
Reviewed By: jvillard
Differential Revision: D25196734
fbshipit-source-id: a8001a075
Summary:
Currently there is a symbolic execution option to ignore exceptional
control flow. This hack does not fit well, and it is unclear how much
backend functionality should take it into consideration. This diff
removes this option and replaces it with an option during model
compilation. This has the advantage of clarifying and simplifying the
backend, with the disadvantage of no longer supporting switching
between exceptions and no-exceptions modes at analysis time. Since the
possibility of ignoring exceptional control flow is due to it not being
ready yet, this is a good trade to make.
Reviewed By: jvillard
Differential Revision: D25146148
fbshipit-source-id: 1f1299ee1
Summary:
Use the equality class information in the symbolic state to resolve
callees of indirect calls.
Reviewed By: jvillard
Differential Revision: D25146160
fbshipit-source-id: a1c39bbe1
Summary:
The callee function of a Call can often be resolved
statically. Currently this is resolution is only done dynamically
during symbolic execution by checking if the callee expression is a
function name and looking up the function in the program. This is
wasted and redundant work. Also, the static resolution code is
duplicated in all the domains.
This diff resolves this by resolving known callees statically at
translation time. This involves:
- add an ICall terminator that is the same as Call is currently
- change Call to use a func callee instead of Exp.t
- make callee field mutable since recursive calls can create cycles
- change the Llair.Term.call constructor to return a thunk to perform
the backpatching once the callee has been translated
- modify the Frontend
+ to determine whether to emit Call or ICall depending on whether
the callee in LLVM is already a Function
+ to record the LLVM function -- backpatch thunk pairs encountered during translation
+ record the mapping of LLVM to LLAIR functions during translation
+ to enumerate the calls to backpatch after all functions have been
translated, and find the LLAIR function corresponding to each LLVM
function and backpatch the call to use it as the callee
+ to handle direct calls to undefined functions, when backpatching
translate such function declarations into undefined functions
Reviewed By: jvillard
Differential Revision: D25146152
fbshipit-source-id: 47d2ca1ff
Summary:
Current code partially tries to handle Invoke, but incorrectly, and
these names are only needed for Call. So this diff revises this to be
slightly simpler and less confusing.
Reviewed By: jvillard
Differential Revision: D25146157
fbshipit-source-id: ead4f6f31
Josh Berdine