158 Commits (d47824fe37633eba325814f64261e61d139b8359)

Author SHA1 Message Date
Josh Berdine 69c9dbad9c [sledge] Improve simplification of negated booleans
6 years ago
Josh Berdine 48e947883d [sledge] Normalize arithmetic exps to polynomials
6 years ago
Josh Berdine fb746f65d0 [sledge] Refactor to remove unnecessary recursion in simp_and and simp_or
6 years ago
Josh Berdine 2a70b36140 [sledge] Obtain bitwidth and type from same arg of binop exps
6 years ago
Josh Berdine 42fefadc38 [sledge] Strengthen type-checking of arithmetic exps
6 years ago
Josh Berdine 6c108fa68e [sledge] Make Typ.ptr and Typ.siz inter-castable
6 years ago
Josh Berdine 718aa27c8d [sledge] Add typ of Add and Mul expressions
6 years ago
Josh Berdine c7f4ed65ce [sledge] Remove Exp.Sub, express x - y as x + -1y
6 years ago
Josh Berdine 2876ab5034 [sledge] Add result type to Exp.{add,sub,mul}
6 years ago
Josh Berdine 59ee539dce [sledge] Represent null pointer as zero integer of pointer type
6 years ago
Josh Berdine f1de054a39 [sledge] Add `-v` alias for `--trace-all`
6 years ago
Josh Berdine 2f5ed3e554 [sledge] Clamp result of binary Z ops to bitwidth
6 years ago
Josh Berdine 11bf7d9a39 [sledge] Build system support inline tests in all libraries
6 years ago
Josh Berdine 10c8b02a8d [sledge] Clean test coverage data before `make coverage`
6 years ago
Josh Berdine 6df666b87b [sledge] Return dbg and opt build targets
6 years ago
Josh Berdine 172b804838 [sledge] Update tests
6 years ago
Mehdi Bouaziz ecedb27d77 Add missing FB copyrights
6 years ago
Josh Berdine 1500745b03 [sledge] Add typ of integer constants
6 years ago
Josh Berdine 71fe6602ef [sledge] Change Switch cases from Z.t to Exp.t
6 years ago
Josh Berdine e73e6c6448 [sledge] Add Llair.Term.branch wrapper for Switch
6 years ago
Josh Berdine 0e5239682d [sledge] Add Llair.Term.goto wrapper for Switch
6 years ago
Josh Berdine 8074eea927 [sledge] Distinguish signed and unsigned integer comparisons
6 years ago
Josh Berdine 9e724842f6 [sledge] Update todo
6 years ago
Josh Berdine 889f7abc6f [sledge] Dump program to file between frontend and backend
6 years ago
Josh Berdine 080c843856 [sledge] Add maybe-alloc instruction that may fail
6 years ago
Josh Berdine f3d25d3a23 [sledge] Refactor issue reporting to Report module
6 years ago
Josh Berdine 1b11a0df0e [sledge] Improve debug tracing
6 years ago
Josh Berdine cf2a985073 [sledge] Add Trace.{printf,fprintf,kprintf}
6 years ago
Josh Berdine da89fc8f95 [sledge] Warn of each uninterpreted intrinsic only once
6 years ago
Josh Berdine 452e240e67 [sledge] Simplify CLI implementation using ppx_deriving_cmdliner
6 years ago
Josh Berdine 85d9e5bdb0 [sledge] Add `make check` using `dune build @check`
6 years ago
Josh Berdine d5a83894b0 [sledge] Run executables from dune install dir
6 years ago
Josh Berdine a9cdf69010 [sledge] Use dune ocamlformat integration for `make fmt`
6 years ago
Josh Berdine e71ea9f0ed [sledge] Switch from Llvm.demangle to __cxa_demangle via Ctypes
6 years ago
Josh Berdine 27f08ab53a [sledge] Update entry point and command line interface
6 years ago
Josh Berdine b712a57bf9 [sledge] Add analysis based on iterative bounded exploration
6 years ago
Josh Berdine 0a09581431 [sledge] Add abstract domain interface
6 years ago
Josh Berdine 4633419b1c [sledge] Add symbolic execution
6 years ago
Josh Berdine e397a43f80 [sledge] Add frame inference solver over symbolic heaps
6 years ago
Josh Berdine 83eff4c734 [sledge] Add symbolic heap formulas
6 years ago
Josh Berdine a32890a1e3 [sledge] Add congruence closure with integer offsets
6 years ago
Josh Berdine f7a9a0c323 [sledge] Update frontend
6 years ago
Josh Berdine 2c116474e5 [sledge] Update llair
6 years ago
Josh Berdine 8e7eeb8d1f [sledge] Update global
6 years ago
Josh Berdine 2b53e53504 [sledge] Update loc
6 years ago
Josh Berdine 392f596b02 [sledge] Update exp
6 years ago
Josh Berdine 742b181282 [sledge] Update typ
6 years ago
Josh Berdine 6a7c21e7c9 [sledge] Update trace and ppx_trace
6 years ago
Josh Berdine 91888c4c41 [sledge] Update import, vector
6 years ago
Josh Berdine f6ba0c8137 [sledge] Update build system, etc.
6 years ago
Josh Berdine e1d4aad487 [ocamlformat] upgrade ocamlformat to 0.8
6 years ago
Josh Berdine 40ab73037e [ocamlformat] upgrade to ocamlformat 0.7
6 years ago
Jules Villard 83a4a8fa5b [dune] jbuilder -> dune
6 years ago
Jules Villard 8b882ac1df Change license to MIT
7 years ago
Josh Berdine 16988b0a7a [ocamlformat] Upgrade to ocamlformat 0.5
7 years ago
Josh Berdine dcc0f646fe Add demo LLAIR client
7 years ago
Josh Berdine 446ac6d87c Add initial version of LLAIR and LLVM to LLAIR translation
7 years ago
Josh Berdine d61b93b1d2 Create sledge directory
7 years ago