612 Commits (fa13577695350a7e44f8baff9770cf65716082d7)

Author SHA1 Message Date
Josh Berdine 3a87a0e2f3 [sledge] Unignore model/cxxabi.bc
6 years ago
Josh Berdine 889b874f63 [sledge] Optimize equality solver treatment of atomic exps
6 years ago
Josh Berdine 0cbcb878f9 [sledge] Classify fully-interpreted and simplified exps differently
6 years ago
Josh Berdine c690416622 [sledge][NFC] Simplify harness selection code
6 years ago
Timotej Kapus d47824fe37 [sledge] link in cxxabi
6 years ago
Timotej Kapus 22acf72936 [sledge] fix only-needed
6 years ago
Josh Berdine cb6d02fe32 [sledge] Add Frontend.report_undefined
6 years ago
Josh Berdine 4ece75ace9 [sledge] Add abort instruction and use it for abort and llvm.trap
6 years ago
Josh Berdine 8f0c88cc68 [sledge] Translate aligned operator new and delete
6 years ago
Josh Berdine b33e32941a [sledge] Revise plans for variadic functions and stack allocation
6 years ago
Josh Berdine f64fc6e32e [sledge] Improve frontend warnings
6 years ago
Josh Berdine c8943f946c [sledge] Change type of warn to be consistent with fail
6 years ago
Josh Berdine ce7a947be5 [sledge] Refactor auto-formatting build
6 years ago
Josh Berdine 81909abf23 [sledge] Model llvm.trap as nop
6 years ago
Josh Berdine af766b5320 [sledge] Fix translation of Invoke retpolines
6 years ago
Josh Berdine b6d0e33dfc [sledge] Simplify build
6 years ago
Josh Berdine 9a62554322 [sledge] Fix potential divergence in Llair.sexp_of functions
6 years ago
Josh Berdine 00a93899f3 [sledge] Update roadmap
6 years ago
Josh Berdine 9c04bea9dd [sledge] Update build, setup, todo
6 years ago
Josh Berdine 109a587654 [sledge] Fix normalization of high-degree polynomials
6 years ago
Josh Berdine ffb0f4f912 [sledge] Relax 'no new subexps' invariant for Xor expressions
6 years ago
Josh Berdine 3483ec72a1 [sledge] Do not normalize shifts by enough bits to be undefined
6 years ago
Josh Berdine 8f2af62480 [sledge] Clamp rational numerator and denominator to bitwidth
6 years ago
Josh Berdine 07e8ac2d6a [sledge] Avoid division by zero during Exp normalization
6 years ago
Josh Berdine d2a97a6174 [sledge] Use integer or float constants as needed in Exp normalization
6 years ago
Josh Berdine 26a3058659 [sledge] Refine Convert Exp invariant
6 years ago
Josh Berdine 0d70f57c6f [sledge] Relax overly strong polynomial invariants
6 years ago
Josh Berdine 8a9cf0198a [sledge] Add assertions on Call and Invoke callee operands
6 years ago
Josh Berdine 684f12a498 [sledge] Protect against misdeclarations of operator new
6 years ago
Josh Berdine 9986d98645 [sledge] Revise invariant checking regarding opaque types
6 years ago
Josh Berdine d3f33d0b43 [sledge] Improve error message when calling null as a function
6 years ago
Josh Berdine 44076e00ff [sledge] Memoize translation of globals, and handle recursive globals
6 years ago
Josh Berdine 78b2835936 [sledge] Improve lookup of debug locations
6 years ago
Josh Berdine 564bd344fc [sledge] Update frontend to upstreamed LLVM OCaml api
6 years ago
Josh Berdine bf7ce6f117 [sledge] Revert "Do not auto-promote test results"
6 years ago
Josh Berdine 4acad5ca90 [ocamlformat] upgrade ocamlformat to 0.9
6 years ago
Josh Berdine 79dbb950c1 [sledge] Compare stack component of edges as a inlined code location
6 years ago
Josh Berdine c5224737c3 [sledge] Fix stack popping
6 years ago
Josh Berdine a0a8c6320d [sledge] Hoist conditional exps above boolean exps
6 years ago
Josh Berdine 7595b05f39 [sledge] Classify Eq and Dq exps as Interpreted
6 years ago
Josh Berdine 3a01feb9ba [sledge] Strengthen simplification of Convert exps
6 years ago
Josh Berdine ff9d3aca5a [sledge] Add rough models for mallctl functions
6 years ago
Josh Berdine 077b4d3da7 [sledge] Add Solver tests demonstrating incompleteness
6 years ago
Josh Berdine 3beb1ba2b2 [sledge] Add Exp.size_of
6 years ago
Josh Berdine ae1f14044c [sledge] Add Typ.int
6 years ago
Josh Berdine 455ea495fb [sledge] Strengthen Sh re null cannot be allocated
6 years ago
Josh Berdine 7567432afb [sledge] Revise Sh.dnf to handle nested existentials
6 years ago
Josh Berdine 15300403a5 [sledge] Improve debug tracing
6 years ago
Josh Berdine 0bef279ed1 [sledge] Fix bug in quantifier handling during Sh.or simplification
6 years ago
Josh Berdine 681711c4d2 [sledge] Improve Set.union to preserve ==
6 years ago
Josh Berdine 0a97615da2 [sledge] Strengthen byte-array solver with derived length constraints
6 years ago
Josh Berdine 6e1ab66945 [sledge] Add intrinsics to model jemalloc.h functions
6 years ago
Josh Berdine f3dd99ef00 [sledge] Refactor frontend to cleanup handling intrinsics slightly
6 years ago
Josh Berdine 6e41cab422 [sledge] Change strlen from an instruction to an intrinsic
6 years ago
Josh Berdine 1c2ce2344f [sledge] Skeleton for symbolic execution of unsafe intrinsics
6 years ago
Josh Berdine 94fedd9cf0 [sledge] Minor simplification of Exec implementation
6 years ago
Josh Berdine a7367a7cbd [sledge] Improve fresh variable handling in spec construction
6 years ago
Josh Berdine 2376fd3e51 [sledge] Refactor to clean up instruction ordering
6 years ago
Josh Berdine 95b9702d40 [sledge] Remove unused Domain.bottom
6 years ago
Josh Berdine 3c992a832a [sledge] Support Invoke on functions translated as intrinsic exps
6 years ago
Josh Berdine fe60b75ea0 [sledge] Ignore llvm.invariant.{start,end} instructions
6 years ago
Josh Berdine d10d30c5f0 [sledge] Fix typo llvm.memmove
6 years ago
Josh Berdine b59f444023 [sledge] Extend cxxabi model
6 years ago
Josh Berdine 2f55acf8e1 [sledge] Improve build of model/cxxabi.bc
6 years ago
Josh Berdine 2896ff15f1 [sledge] Include all function locals in entry block
6 years ago
Josh Berdine d769718192 [sledge] Add missing i32 to i64 conversion for gep indices
6 years ago
Josh Berdine 0af0d3b210 [sledge] Revise Equality carrier-closure invariant
6 years ago
Josh Berdine efbd816dff [sledge] Sort numeric constants last
6 years ago
Josh Berdine 591d60e20a [sledge] Prefer simple exps over applications as class reps
6 years ago
Josh Berdine 71694c874f [sledge] Prefer constants as class reps
6 years ago
Josh Berdine a4a9d5682e [sledge] Fix "iterator invalidation" bug
6 years ago
Josh Berdine 0578064a7f [sledge] Revise solver existential instantiation
6 years ago
Josh Berdine 29f7f30b1a [sledge] Add simple frame inference solver tests
6 years ago
Josh Berdine 0ff3925ea6 [sledge] Do not auto-promote test results
6 years ago
Josh Berdine 89e2e30fb2 [sledge] Use more standard interface for Trace.parse
6 years ago
Josh Berdine 41fff4fbf7 [sledge] Remove previous Congruence implementation
6 years ago
Josh Berdine 34e7e1a83b [sledge] Strengthen solver with implied sizes of concatenated byte arrays
6 years ago
Josh Berdine d7f5611b32 [sledge] Use ppx_compare to define equal functions
6 years ago
Josh Berdine 113df8b756 [sledge] Upgrade base to v0.12
6 years ago
Josh Berdine cd63204dba [sledge] Initial Shostak-style treatment of UIF+LIA
6 years ago
Josh Berdine e56646674f [sledge] Strengthen simplification of division exps
6 years ago
Josh Berdine 07d48fa7d8 [sledge] Make simplification subexp check more precise
6 years ago
Josh Berdine 8fa2f86b7e [sledge] Fix order of Exp.fold args
6 years ago
Josh Berdine 55540d3500 [sledge] Remove Trace.report in favor of Trace.fail
6 years ago
Josh Berdine 0ecee6a848 [sledge] Change polynomial coefficients and powers to rationals
6 years ago
Josh Berdine d01de4b0dd [sledge] Simplify representation of Add and Mul exps
6 years ago
Josh Berdine 22578089c3 [sledge] Reimplement arithmetic and congruence closure
6 years ago
Josh Berdine 06d169c440 [sledge] Add Trace.fail
6 years ago
Josh Berdine f8fda2e378 [sledge] Trace using symmetric differences between congruence relations
6 years ago
Josh Berdine 875a6a6f8e [sledge] Strengthen treatment of existentials in pure constraints
6 years ago
Josh Berdine 270b6003de [sledge] Revise excision of segments to witness existential size
6 years ago
Josh Berdine 23f2d3a08e [sledge] Fix order of args in simp_div
6 years ago
Josh Berdine 95f94537d7 [sledge] Use Typ.prim_bit_size_of instead of Integer {bits}
6 years ago
Josh Berdine 49c9b3aec4 [sledge] Strengthen Exp.invariant
6 years ago
Josh Berdine 0177549315 [sledge] Improve exp tests
6 years ago
Josh Berdine 909b341e8a [sledge] Add missing `make test` dependency
6 years ago
Josh Berdine 610a641b45 [sledge] Sort congruence classes when printing
6 years ago
Josh Berdine 616be32b5b [sledge] Merge Config.trace_all into Config.trace
6 years ago
Josh Berdine 65c446f0fb [sledge] Protect Trace.parse from invalid user input
6 years ago
Josh Berdine 5a3718a098 [sledge] Move parsing of trace specs from Config to Trace
6 years ago
Josh Berdine 83607ace5e [sledge] Add Trace.all
6 years ago
Josh Berdine 730cbac6c1 [sledge] Make --trace option optional
6 years ago
Josh Berdine 7f630097f9 [sledge] Improve debug tracing
6 years ago
Josh Berdine 10e1ef1ca6 [sledge] Update TODO
6 years ago
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