397 Commits (4a81a69fb31ed66ec8dab161785a9426ff9cb7f8)

Author SHA1 Message Date
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
6 years ago
Josh Berdine 429fbddeda [sledge] Refine inlining heuristic to allow casts
6 years ago
Josh Berdine d6d65a785a [sledge] Remove left-over SSA assertion
6 years ago
Josh Berdine 7105d85281 [sledge][NFC] Minor code cleanup
6 years ago
Josh Berdine 081455278d [sledge] Do not explore exceptional control flow by default
6 years ago
Josh Berdine 9acfb65ba0 [sledge][NFC] Update TODO
6 years ago
Josh Berdine bc858fad2e [sledge][NFC] Rename Term.call's func arg to callee to match type
6 years ago
Josh Berdine 6399c59861 [sledge] Do not represent function CFGs explicitly
6 years ago
Josh Berdine 2331e8d68a [sledge] Fix frontend bug in trampoline creation
6 years ago
Josh Berdine cf5097a8b4 [sledge] Add report-summary test make target
6 years ago
Josh Berdine 995de071ed [sledge] Revise Sh_domain handling of function call and return
6 years ago
Josh Berdine df26b9b1a5 [sledge][NFC] Minor code simplification
6 years ago
Josh Berdine 65e963a162 [sledge] Add Sh.subst implemented ito and and exists
6 years ago
Josh Berdine 1595fb7c60 [sledge] Fix potential name clash in Sh.rename
6 years ago
Josh Berdine 799b21761f [sledge] Translate ExtractElement and InsertElement despite being vector
6 years ago
Scott Owens 3080fba8fa [sledge sem] Update LLVM and LLAIR sem for consistent stuckness
6 years ago
Scott Owens 14a8ae34b9 [sledge sem] Improve and unify treatment of Exit
6 years ago
Scott Owens 5312b3d10c [sledge sem] Fix trans. invariant for llair expressions
6 years ago
Scott Owens 9f2f14b34c [sledge sem] Sketch out translation correctness
6 years ago
Jules Villard 42470d8809 [hmm] sexp_{option,list} -> {option,list}
6 years ago
Josh Berdine ef78ba83cf [sledge] Report the number of alarms
6 years ago
Josh Berdine ec52c05c30 [sledge][NFC] Minor simplification for singleton sets
6 years ago
Josh Berdine 239d906ab6 [sledge] Improve tracing and debugging support
6 years ago
Josh Berdine 3f5adecdcf [sledge] Exec.exec_specs missed vocabulary extension
6 years ago
Josh Berdine 9ac854c970 [sledge] Exec.kill should preserve vocabulary
6 years ago
Josh Berdine 8097f1a6df [sledge] Adjust tests to match harnesses
6 years ago
Josh Berdine b2f90a3994 [sledge] Treat freturn directly in Dom.call
6 years ago
Josh Berdine fbf0fe2f1a [sledge][NFC] Rename args to actuals
6 years ago
Josh Berdine d3d0c4b36e [sledge][NFC] Rename params to formals
6 years ago
Josh Berdine 69c29ab3d8 [sledge][NFC] Label args of Domain.call
6 years ago
Josh Berdine 47766a0e6e [sledge] Drop globals with appending linkage and size 0
6 years ago
Josh Berdine 1efd0df035 [sledge] Avoid potential name clash between trampolines
6 years ago
Josh Berdine ebee451f1c [sledge] Improve test scripts
6 years ago
Josh Berdine 38cab376f6 [sledge] Keep BitCasts and similar in expressions
6 years ago