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:
This diff adds a formal parameter to each non-void-returning function
to name the return value, and similarly a formal parameter for the
thrown exception value. These are interpreted as call-by-reference
parameters, so that they can be constrained in formulas to e.g. be
equal to the return value, and are still in scope when the function
returns, and so can be passed to the return block. Prior to
summarizing functions, this means that these formals need to be
tracked on the analyzer's control stack.
This will be needed to express function specs/summaries in terms of
formals, and fixes a bug where in some cases return values were not
tracked correctly.
Reviewed By: kren1
Differential Revision: D15738026
fbshipit-source-id: fff2d107c
Summary:
Change command line interface to include buck and llvm integration as
separate subcommands.
Reviewed By: kren1
Differential Revision: D15614567
fbshipit-source-id: b7618571b
Summary:
Require a final `()` argument to explicitly indicate the end of the
arguments to the printf-like functions. For `warn` this is not
any safer because the return type is `unit` anyhow, but for `fail` the
return type is polymorphic so the final `()` prevents unintentionally
forgetting an argument.
Reviewed By: ngorogiannis
Differential Revision: D15403367
fbshipit-source-id: ce3fe4035
Summary:
- Change representation of Concat expressions from curried binary
operator to an nary one. This enables normalizing Concat expressions
with respect to associativity.
- Generalize Exp.solve to return a map rather than a pair of exps, to
enable expressing cases where solving an equation yields multiple
equations.
- Strengthen solver with implied equalities between sums of sizes of
concatenations of byte arrays.
Reviewed By: ngorogiannis
Differential Revision: D14297865
fbshipit-source-id: b40871559
Summary:
This patch adds an embarrassingly inefficient implementation of a
decision procedure for equality in the theories of uninterpreted
functions and linear arithmetic. A Shostak-style approach, where a
single congruence closure structure is shared by all theories, is
used. This is mostly based on the corrected variant of Shostak's
algorithm from:
Harald Rueβ and Natarajan Shankar. 2001. Deconstructing Shostak. In
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer
Science (LICS '01).
Reviewed By: jvillard
Differential Revision: D14251655
fbshipit-source-id: 8a080145f
Summary:
- Add nary expressions implemented using a form of multisets which
support any integer multiplicity
- Reimplement polynomials using new nary expressions
- Move the decomposition of exps into "base plus offset" form into
Exp, to enforce simplification invariants
- Revise expression simplification to cooperate with congruence
closure (mainly: simplification should not invent new
subexpressions)
- Reimplement congruence closure plus integer offsets to
+ cope with new representation of polynomials using nary expression forms
+ be diligent about maintaining which expressions are in the relation
+ add lots of invariant checking for the correlations between the
componnents of the congruence closure data structures
Reviewed By: jvillard
Differential Revision: D14075512
fbshipit-source-id: 2dbaf3d11
Summary:
Even pretty-printed congruence relations are verbose, and most
operations do not change much of the relation. So on return, print
only the symmetric difference between input and output relations.
Reviewed By: mbouaziz
Differential Revision: D14075513
fbshipit-source-id: b1f0ae6d0
Summary:
`sledge -c foo.bc` generates a binary file `foo.bc.llair` which can be
analyzed with `sledge foo.bc.llair`, and converted to textual form
with `sledge -c foo.bc.llair -o foo.llair`. Binary files are not
compatible between debug and release builds.
Reviewed By: mbouaziz
Differential Revision: D10389473
fbshipit-source-id: dfcabf33b
Summary:
Change the license of the source code from BSD + PATENTS to MIT.
Change `checkCopyright` to reflect the new license and learn some new file
types.
Generated with:
```
git grep BSD | xargs -n 1 ./scripts/checkCopyright -i
```
Reviewed By: jeremydubreil, mbouaziz, jberdine
Differential Revision: D8071249
fbshipit-source-id: 97ca23a
Summary:
Upgrade ocamlformat, and base which needs to be done in sync in order to build
ocamlformat, and the other deps can come for the ride.
Reviewed By: jvillard
Differential Revision: D7663537
fbshipit-source-id: 3e90970
Josh Berdine
Mehdi Bouaziz
Jules Villard