717 Commits (f02f7b379e4dae8b602c22c669bd6c401de01cb1)

Author SHA1 Message Date
Scott Owens 1ddeacee50 [sledge sem] Rework phi instructions
5 years ago
Josh Berdine 3c6e2469de [ocamlformat] Enable parsing and reformatting docstrings
5 years ago
Josh Berdine 517b99e673 [sledge] Avoid infix monad operators in non-pipeline code
5 years ago
Josh Berdine c9449cce77 [sledge] Some simplifications using let+
5 years ago
Josh Berdine f60ce32125 [sledge] Undeprecate Not_found in the implementation of Import
5 years ago
Josh Berdine 0999d202ad [sledge] Remove dead List.remove
5 years ago
Josh Berdine 661db9db76 [sledge] Implement Map.find_and_remove more directly
5 years ago
Josh Berdine 30aa8aa3b9 [sledge] Basic definitions for monadic binding operators
5 years ago
Josh Berdine cfbbacf9f1 [sledge] Improve using extended open
5 years ago
Josh Berdine 7ed8a6a260 [sledge] Simplify and improve using local subst in sigs
5 years ago
Josh Berdine b22d8b4151 [sledge] Simplify using shadowing of modules from includes
5 years ago
Josh Berdine b1a6928a50 [sledge] Avoid wildcard exception handler
5 years ago
Josh Berdine f2be1cbed0 [sledge] Hashtbl.Key has been deprecated in favor of Hashtbl.Key.S
5 years ago
Josh Berdine b5915db605 [sledge] Clear terminal between builds in watch mode
5 years ago
Josh Berdine 48fd99d48f [sledge] Avoid matching on Not_found
5 years ago
Josh Berdine e201e517c9 [sledge][NFC] Refactor to avoid an unused open warning
5 years ago
Josh Berdine 6c5d9d4acb [sledge] Remove dependency on ppx_import
5 years ago
Josh Berdine 9d7580b5cd [sledge] Remove ocamlformat from dev-tools.opam
5 years ago
Josh Berdine e3734d3d2c [sledge] Fix bug in Term.solve
5 years ago
Josh Berdine 28e4c74426 [sledge] Fix bug in Equality.or_
5 years ago
Josh Berdine 8d20e4d64d [ocamlformat] Upgrade ocamlformat version
5 years ago
Josh Berdine 52380b017c [sledge][NFC] Simplify Term rec module
5 years ago
Josh Berdine 1f64634093 [sledge] Simplify type conversions
5 years ago
Josh Berdine e6d93dcf94 [sledge][NFC] Simplify term tests
5 years ago
Scott Owens 1bd290634b [sledge sem] Update integer conversions to new LLAIR
5 years ago
Scott Owens f68258ca73 [sledge sem] Update sanity proof for LLAIR convert
5 years ago
Benno Stein beb99932c3 [sledge] Handle more LLAIR expressions in APRON interval analysis
5 years ago
Josh Berdine 752b8ab56a [sledge] Fix normalization of Convert terms
5 years ago
Scott Owens 5caa19990b [sledge sem] Improve a comment
5 years ago
Scott Owens a4f0d6dbb7 [sledge sem] Complete (nearly) proof for phi instrs
5 years ago
Benno Stein 50b60bc049 [sledge] Add APRON-backed Interval abstract domain
5 years ago
Scott Owens 9f0fdd3bfe [sledge sem] Add proof of bit cast implementation
5 years ago
Scott Owens e9296d31b6 [sledge sem] Implement and verify cast expressions
5 years ago
Scott Owens 86024892e1 [sledge sem] Refactor inductive definitions a bit
5 years ago
Scott Owens 573f0d8aed [sledge sem] Make proof progress on phi instructions
5 years ago
Scott Owens 0a35b1da35 [sledge sem] Prove the Load and Store cases (mostly)
5 years ago
Josh Berdine c0c96b5235 [sledge] Refactor Used globals analysis results type and query
5 years ago
Josh Berdine 429fbddeda [sledge] Refine inlining heuristic to allow casts
5 years ago
Josh Berdine d6d65a785a [sledge] Remove left-over SSA assertion
5 years ago
Josh Berdine 7105d85281 [sledge][NFC] Minor code cleanup
5 years ago
Josh Berdine 081455278d [sledge] Do not explore exceptional control flow by default
5 years ago
Josh Berdine 9acfb65ba0 [sledge][NFC] Update TODO
5 years ago
Josh Berdine bc858fad2e [sledge][NFC] Rename Term.call's func arg to callee to match type
5 years ago
Josh Berdine 6399c59861 [sledge] Do not represent function CFGs explicitly
5 years ago
Josh Berdine 2331e8d68a [sledge] Fix frontend bug in trampoline creation
5 years ago
Josh Berdine cf5097a8b4 [sledge] Add report-summary test make target
5 years ago
Josh Berdine 995de071ed [sledge] Revise Sh_domain handling of function call and return
5 years ago
Josh Berdine df26b9b1a5 [sledge][NFC] Minor code simplification
5 years ago
Josh Berdine 65e963a162 [sledge] Add Sh.subst implemented ito and and exists
5 years ago
Josh Berdine 1595fb7c60 [sledge] Fix potential name clash in Sh.rename
5 years ago
Josh Berdine 799b21761f [sledge] Translate ExtractElement and InsertElement despite being vector
5 years ago
Scott Owens 3080fba8fa [sledge sem] Update LLVM and LLAIR sem for consistent stuckness
5 years ago
Scott Owens 14a8ae34b9 [sledge sem] Improve and unify treatment of Exit
5 years ago
Scott Owens 5312b3d10c [sledge sem] Fix trans. invariant for llair expressions
5 years ago
Scott Owens 9f2f14b34c [sledge sem] Sketch out translation correctness
5 years ago
Jules Villard 42470d8809 [hmm] sexp_{option,list} -> {option,list}
5 years ago
Josh Berdine ef78ba83cf [sledge] Report the number of alarms
5 years ago
Josh Berdine ec52c05c30 [sledge][NFC] Minor simplification for singleton sets
5 years ago
Josh Berdine 239d906ab6 [sledge] Improve tracing and debugging support
5 years ago
Josh Berdine 3f5adecdcf [sledge] Exec.exec_specs missed vocabulary extension
5 years ago
Josh Berdine 9ac854c970 [sledge] Exec.kill should preserve vocabulary
5 years ago
Josh Berdine 8097f1a6df [sledge] Adjust tests to match harnesses
5 years ago
Josh Berdine b2f90a3994 [sledge] Treat freturn directly in Dom.call
5 years ago
Josh Berdine fbf0fe2f1a [sledge][NFC] Rename args to actuals
5 years ago
Josh Berdine d3d0c4b36e [sledge][NFC] Rename params to formals
5 years ago
Josh Berdine 69c29ab3d8 [sledge][NFC] Label args of Domain.call
5 years ago
Josh Berdine 47766a0e6e [sledge] Drop globals with appending linkage and size 0
5 years ago
Josh Berdine 1efd0df035 [sledge] Avoid potential name clash between trampolines
5 years ago
Josh Berdine ebee451f1c [sledge] Improve test scripts
5 years ago
Josh Berdine 38cab376f6 [sledge] Keep BitCasts and similar in expressions
5 years ago
Josh Berdine b632d4f283 [sledge] Check the input datalayout agrees with assumptions
5 years ago
Josh Berdine 6328a6ce40 [sledge] Do not store size of globals separately
5 years ago
Josh Berdine ca95fc098f [sledge] Keep size in both bits and bytes for each type
5 years ago
Josh Berdine d3bad1ce44 [sledge] Add sizes to types
5 years ago
Josh Berdine 6120b7d098 [sledge] Use the configured margin when formatting failure messages
5 years ago
Josh Berdine a386b36616 [sledge] Re-add Splat expression for zero-initialized aggregates
5 years ago
Josh Berdine 727385d853 [sledge] Relax Typ.is_sized to allow opaque types
5 years ago
Josh Berdine f804220cd2 [sledge] Revise order of Term constructors for polynomial normalization
5 years ago
Josh Berdine 1ef390ffca [sledge] Relax Exp type-checking to be modulo-casting
5 years ago
Josh Berdine fb184a6a1d [sledge] Introduce the notion of types having the same semantics
5 years ago
Josh Berdine 917cc62e28 [sledge] Fix type of functions called using a cast
5 years ago
Josh Berdine ce3252c348 [sledge] Allow global variables as function names
5 years ago
Josh Berdine 785928c77e [sledge] Error reporting improvements
5 years ago
Josh Berdine ffeef16aae [sledge] Add a flag to disable internalization
5 years ago
Josh Berdine 6ca09b14fd [sledge] Add flag to disable linking in the models
5 years ago
Josh Berdine f699c9b9a8 [sledge] Simplify ¬¬e to e
5 years ago
Josh Berdine 06f2863dd8 [sledge] Simplify `e xor e` to `0`
5 years ago
Josh Berdine 6f84787b19 [sledge] Change exec_inst to return an option instead of a result
5 years ago
Josh Berdine 2840eb4781 [sledge] Refactor dispatch on instruction from Exec to Sh_domain
5 years ago
Josh Berdine c6d7886fd8 [sledge] Make type of exec_move consistent with move instruction
5 years ago
Josh Berdine 162f027249 [sledge] Make type argument of Exp constructors optional where computable
5 years ago
Josh Berdine ad5d5dd89e [sledge] Add Exp.true_ and Exp.false_
5 years ago
Josh Berdine 37d1904bd3 [sledge] Move check for whether a variable is global from Reg to Var
5 years ago
Josh Berdine 3003a8e646 [sledge] NFC minor cleanups
5 years ago
Josh Berdine 8ee0c67d1f [sledge] Precompute the Term form of each Exp, and add it to Exp.t
5 years ago
Josh Berdine 9ddfae4e89 [sledge] Change Term.rename to preserve sharing in cyclic records
5 years ago
Josh Berdine 7ecd091ff3 [sledge] Change Struct_rec to a generic n-ary recursive application
5 years ago
Josh Berdine 356b4f0b4e [sledge] Uncurry Record term constructor
5 years ago
Josh Berdine 99b60d191a [sledge] Fix sorting of heap block subformulas when printing
5 years ago
Josh Berdine 1228c8e31b [sledge] Uncurry Update term constructor, and specialize index to int
5 years ago
Josh Berdine 09daac754c [sledge] Uncurry Select term constructor, and specialize index to int
5 years ago
Josh Berdine 5eaae07043 [sledge] Change Concat term contructor to a generic n-ary application
5 years ago
Josh Berdine 6cd82475f1 [sledge] Use generic binary application for Splat and Memory term constructors
5 years ago
Josh Berdine 6805da9557 [sledge] Uncurry ternary term constructors
5 years ago
Josh Berdine 167e489e24 [sledge] Uncurry binary term constructors
5 years ago
Josh Berdine 8b9d4ba066 [sledge] Uncurry unary term constructors
5 years ago
Josh Berdine e87a0533be [sledge] Minor simplification of polynomial representation
5 years ago
Josh Berdine 3bbb05216f [sledge] Remove the redundancy of both < and >= terms
5 years ago
Josh Berdine a3506f995c [sledge] Simplify arithmetic terms due to not needing type
5 years ago
Josh Berdine 471d296266 [sledge] Fix check for range of representable integers
5 years ago
Josh Berdine c440c4fc28 [sledge] Remove unsigned Term operations except Extract
5 years ago
Josh Berdine e84f3fcf0f [sledge] Add Extract term
5 years ago
Josh Berdine 5753f9b26a [sledge] Rename clamp to extract
5 years ago
Josh Berdine d7ef03cf02 [sledge] Revise and fix unsigned conversions
5 years ago
Josh Berdine 7f2165484b [sledge] Do not special case boolean vs bitwise operations
5 years ago
Josh Berdine 8abfcfb504 [sledge] Simplify normalization of shift operations
5 years ago
Josh Berdine e3f0ba8c54 [sledge] Revise program expressions
5 years ago
Josh Berdine 00639e15bb [sledge] Delay normalization of xor to equality
5 years ago
Josh Berdine 0e4110fc5c [sledge] Normalize xor and equality based on type instead of bitwidth
5 years ago
Josh Berdine 0903355a0e [sledge] Remove unused Exp constructors for memory exps
5 years ago
Josh Berdine 3b03022b5e [sledge] Remove redundant Reg.id
5 years ago
Josh Berdine 310d00f380 [sledge] Remove dead code in Exp and Term
5 years ago
Josh Berdine 442c8e92f4 [sledge] Distinguish program expressions and formula terms
5 years ago
Josh Berdine 13c06e4dd3 [sledge] Move generation of formal return and throw parameters to frontend
5 years ago
Josh Berdine 0c04ecc9aa [sledge] Change Llair representation of functions to a String map
5 years ago
Josh Berdine 6aaeaba104 [sledge] Move ops on signed 1-bit Z integers to import
5 years ago
Josh Berdine ed733f0247 [sledge] Add missing import of trace into symbheap
5 years ago
Josh Berdine 1fdc76d163 [sledge] Rename State_domain back to Sh_domain
5 years ago
Josh Berdine c6b8b4688b [sledge] Move llvm build and install dirs out of llvm source tree
5 years ago
Scott Owens 5b7931e71a [sledge sem] Add a rudimentary theory of SSA
5 years ago
Scott Owens 71aa4816d6 [sledge sem] Fix the semantics and trans. of If
5 years ago
Scott Owens ab7233c5b8 [sledge sem] Refactor the way LLVM sem. does phis
5 years ago
Scott Owens 17b3c7a49f [sledge sem] Add top-level llair semantics
5 years ago
Scott Owens 30c301a3e8 [sledge sem] Add a more llair-like LLVM semantics
5 years ago
Benno Stein 7ec2830d92 [sledge] Only merge worklist states that share a calling context
5 years ago
Benno Stein e44827b892 [sledge] Add option to apply used-globals as pre-analysis
5 years ago
Benno Stein 1ab8359bc0 [sledge] fix bug spuriously marking a register as global variable
5 years ago
Benno Stein 637fff5247 [sledge] Check for intrinsic calls in used-globals analysis
5 years ago
Benno Stein 6592eb609f [sledge] Add option to skip recursive calls at depth bound
5 years ago
Benno Stein 00a5d3dd64 [sledge] Account for callees in used-globals analysis
5 years ago
Josh Berdine c131e2e669 [sledge] Use dune's Build_info for version reporting
5 years ago
Benno Stein 47f314c00e [sledge] Add used-globals abstract domain and transfer functions
5 years ago
Benno Stein 3dc0c5938f [sledge] Extract relational logic from Sh_domain, create "domain" module
5 years ago
Benno Stein 2acb1c3dee [sledge] Functorize worklist, separate out domain-specific logic
5 years ago
Scott Owens f298d728c5 [sledge sem] Start sketching translation correctness
5 years ago
Josh Berdine 72946c3be3 [sledge] Update dependencies
5 years ago
Scott Owens d864fb2c89 [sledge semantics] Add a rough draft llair semantics
5 years ago
Scott Owens 32983e129b [sledge semantics] Update expr transl. for cross-block
5 years ago
Scott Owens 9f44bbc264 [sledge semantics] Refactor the memory model
5 years ago
Josh Berdine 13fb57ec62 [sledge] Revise llvm to llair translation to avoid code duplication
5 years ago
Josh Berdine ed4aac4f66 [sledge] Update stale comment
5 years ago
Josh Berdine 0667edf418 [sledge] Remove unused Llair.ignore_result
5 years ago
Josh Berdine 3f8d5ace6e [sledge] Eliminate SSA
5 years ago
Josh Berdine b6eab89504 [sledge] Remove dead from_call.actuals_to_formals field
5 years ago
Josh Berdine 8d9b8962c7 [sledge] Add Move instruction
5 years ago
Josh Berdine 2c9fce0bf2 [sledge] Add Vector.unzip
5 years ago
Josh Berdine 0790a64763 [sledge] Change symbolic execution of instructions to not rely on SSA
5 years ago
Scott Owens 808a61623f Add types to the variable syntax in llair
5 years ago
Scott Owens 85243ada62 Update for improved HOL syntax for Datatypes
5 years ago
Scott Owens 84883127af Add a skeleton of an approach to llvm->llair
5 years ago
Scott Owens 6eab69d0d1 Definie a prelim. AST for llair's semantics
5 years ago
Josh Berdine 7efc9285cb [sledge] Fix type of Exp.rename
5 years ago
Josh Berdine 0895246e4f [sledge] Remove label on ~opts args in Control
5 years ago
Scott Owens 742ab9089d Change a type name
5 years ago
Scott Owens a635aff1bc Finish proving sanity checking property
5 years ago
Scott Owens 89c3da4510 Prove that Ret preserves the invariant
5 years ago
Scott Owens df5f20956f Define a simple initial state that inits the globals
5 years ago
Scott Owens 97eb280cb5 Add initial mini-LLVM semantics written in HOL4
5 years ago
Timotej Kapus afb6a4fd11 [sledge] Fix internalization
5 years ago
Timotej Kapus c8d1da1e0d [sledge] Fix __llair_alloc
5 years ago
Timotej Kapus 6c9e4e52c6 [sledge][summaries] Fix unsoundes due to missing frame
5 years ago
Josh Berdine 7f423f7fa1 [sledge] Model `folly::usingJEMalloc()`
5 years ago
Josh Berdine 4bbe05698e [sledge] Remove `.<int>` suffix when looking up modeled function names
5 years ago
Josh Berdine 0126b64d16 [sledge] Explicate output flag of disassemble command
5 years ago
Josh Berdine 9865bc0f74 [sledge] [solver] Strengthen handling of existential subtrahends
5 years ago
Timotej Kapus b5dea36c5e [sledge] Add global merge pass
5 years ago
Timotej Kapus 5882c49d7d [sledge] Disable creating of summaries when summaries disabled
5 years ago
Timotej Kapus ba6e6bf369 [sledge] Actually use function summaries
5 years ago
Timotej Kapus c0c6d65d45 [sledge] Generate and apply summaries
5 years ago
Timotej Kapus 8173eedf1f [sledge] Fix solver crash
6 years ago
Timotej Kapus b5b8259ea7 [sledge] Add printing of some variables in bold
6 years ago
Timotej Kapus c5f261e977 [sledge] [summaries] Fix variable naming bugs
6 years ago
Timotej Kapus b25f735c6e [sledge] Fix Exp.map and garbage_collect
6 years ago
Timotej Kapus 38e66d6f91 [sledge] [summaries] Fix issues with multiple calls
6 years ago
Josh Berdine 1908077aa9 [sledge] Include alarms in debug trace
6 years ago
Josh Berdine e27af1f184 [sledge] Build models without threads support
6 years ago
Josh Berdine b8065e9b62 [sledge] Model __cxa_allocate_exception as unreachable with -skip-throw
6 years ago
Josh Berdine bcc6e1ecc9 [sledge] Support intrinsics which do not return
6 years ago
Josh Berdine 8f765bf742 [sledge] Add -margin flag for debug tracing output
6 years ago
Josh Berdine d42908a5ff [sledge] Add dbg-opt build mode
6 years ago
Josh Berdine ddc1a028c4 [sledge] Manually set exception backtrace recording
6 years ago
Josh Berdine 8be5dbec0b [sledge] Revise Report printing
6 years ago
Josh Berdine 4c6ea0c887 [sledge] Use standard "libFuzzer" name
6 years ago
Timotej Kapus e15a1d36a5 [sledge] Add data structure to hold summaries
6 years ago
Josh Berdine 03e338b2b9 [sledge] Give more specific names to `-output` flags
6 years ago
Josh Berdine 39fe848146 [sledge] Define `sledge buck link` in terms of `sledge buck bitcode`
6 years ago
Josh Berdine 26a34bc33c [sledge] Do not always output list of bitcode inputs
6 years ago
Josh Berdine b8bd639ad8 [sledge] Generate and commit cli help
6 years ago
Timotej Kapus fc6aee2d06 [sledge] Function summarisation: maybe summaries
6 years ago
Timotej Kapus 5df12c7725 [sledge] Add lib-fuzzer to buck analyze
6 years ago
Timotej Kapus 0ab1223d3d [sledge] Function summarization: solver can show pre
6 years ago
Timotej Kapus 4ac252120b [sledge] special case buck-target-patterns
6 years ago
Josh Berdine 0f5ae186b3 [sledge] Add test for use-after-destroy of a temp
6 years ago
Josh Berdine a58bc25aa5 [sledge] Strengthen simplification of convert Exps
6 years ago
Josh Berdine cc1f88a747 [sledge] Fix macos build of models
6 years ago
Timotej Kapus 6949a5ee68 [sledge] Add a todo for calls with inttoptr
6 years ago
Josh Berdine b14580d88b [sledge] Move locals from blocks to functions
6 years ago
Timotej Kapus 86e12cb1a3 [sledge] Add missing llvm passes to frontend.ml
6 years ago
Josh Berdine 330b266d28 [sledge] Rework function return value passing
6 years ago
Timotej Kapus 01e6c5c558 [sledge] [solver] add handling of trivial equality
6 years ago
Timotej Kapus a75a50215b [sledge] Add LLVM passes that reduce bitcode size
6 years ago
Timotej Kapus 1614f78f6d [sledge] Add a harness for lionhead fuzzers
6 years ago
Timotej Kapus 46f5667823 [sledge] Relax call instruction arguments
6 years ago
Timotej Kapus 551a03c4c9 [sledge] Simplify the printed symbolic heaps
6 years ago
Josh Berdine cfc1c8be36 [copyright] Remove years
6 years ago
Timotej Kapus 5a92171b26 [sledge] Print pre/post on function return
6 years ago
Timotej Kapus 0f61a97feb [sledge] Add non-failling alloc intrinsic
6 years ago
Timotej Kapus d2ee43e818 [sledge] Remove --auto-promote from CI builds
6 years ago
Timotej Kapus ad035a4cc7 [sledge] Fix handling of bitcasts in call instr
6 years ago
Timotej Kapus 8e31b136d0 [sledge] CI install script
6 years ago
Josh Berdine 12bab4b16b [sledge] Add formal parameters to functions for return values
6 years ago
Josh Berdine 2440ee69ae [sledge] Preserve sharing of Func.parent
6 years ago
Timotej Kapus 2d69e17d51 [sledge] Add CL option to disable exceptions
6 years ago
Josh Berdine caef28f49e [sledge] Revise test scripts
6 years ago
Josh Berdine f119154a41 [sledge] Add cxa_default_handlers to models
6 years ago
Josh Berdine a0949495c1 [sledge] Translate `invoke abort` to `abort`
6 years ago
Josh Berdine f3bee3f513 [sledge] Print locations of globals in textual LLAIR
6 years ago
Josh Berdine d104f5e518 [sledge] Extend Exp.typ to binary and ternary ops
6 years ago
Timotej Kapus 65f3b10c99 [sledge] Fix crashing frontned
6 years ago
Timotej Kapus 9ef992394c [sledge] Put all the entry points in the config
6 years ago
Timotej Kapus b9ba97a2fd [sledge] Add globalopt pass to remove globals
6 years ago
Josh Berdine 4ea2cf9814 [sledge] Improve uncaught exceptions
6 years ago
Josh Berdine 6a2da2acc4 [sledge] Rework command line interface
6 years ago
Josh Berdine 9c277e9732 [sledge] Simplify Llair.pp
6 years ago
Timotej Kapus c8b063fb50 [sledge] Fix ~predicate label
6 years ago
Timotej Kapus cdd444b901 [sledge] Update internalize to handle other mains
6 years ago
Timotej Kapus e45a05a574 [sledge] fix LLVM assertion failure in xlate_global
6 years ago
Timotej Kapus 881a4d10af [sledge] Fix bound not bounding recursion
6 years ago
Josh Berdine 1e7b13bdcd [sledge] Add printers for some LLVM enums
6 years ago
Josh Berdine babe25fd29 [sledge] Fix translation of global initializers
6 years ago
Josh Berdine 00c5e1b9fe [sledge] Fix size in translation of global variables
6 years ago
Josh Berdine 62a3187f5d [sledge] Don't call Llvm.dispose_context as it leads to crashes in GC
6 years ago
Josh Berdine 14a15931f7 [sledge] Combine name and loc tables into one
6 years ago
Josh Berdine ccd2a92ba5 [sledge] Avoid Format in non-debug code
6 years ago
Josh Berdine d5c2468007 [sledge] Combine scan_locs and scan_names into a single pass
6 years ago
Josh Berdine 4d5970f693 [sledge] Only call Llvm_analysis.verify_module in debug mode
6 years ago
Josh Berdine da097679bd [sledge] Fix crash when trying to warn
6 years ago
Josh Berdine 611fb57d3a [sledge] Treat .bc or .ll input files as pre-linked bitcode
6 years ago
Josh Berdine 7ac04fa46a [sledge] Optimize finding functions by name
6 years ago
Timotej Kapus d37374dd8c [sledge] change input format
6 years ago
Josh Berdine 139a3d3e00 [sledge] Avoid calling Llvm.string_of_llvalue on instructions
6 years ago
Josh Berdine a3e7107969 [sledge] Optimize variable renaming in symbolic heaps
6 years ago
Josh Berdine e391a8a9b2 [sledge] Simplify Equality.map_exps
6 years ago
Josh Berdine c4707621ea [sledge] Make execution bound part of the work queue
6 years ago
Josh Berdine dda922b6ad [sledge] Add command line option for execution bound
6 years ago
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