964 Commits (15943b1ea1c8a42ec743164fabe61c46acd36fa7)

Author SHA1 Message Date
Josh Berdine e2eb6d094a [sledge] Fix context name in test/Makefile
5 years ago
Josh Berdine b9dedea099 [sledge] Add fmt_all target to reformat no matter what dune thinks
5 years ago
Josh Berdine 209fef2256 [sledge] Optimize conjoining fresh equalities
5 years ago
Josh Berdine 53822697f9 [sledge] Rename contexts/profiles to be more conventional
5 years ago
Josh Berdine de20da4fb6 [sledge] Rename lib to src
5 years ago
Josh Berdine 8b59dc58fc [sledge] Remove dead llmodule field from frontend translation context
5 years ago
Scott Owens d30b0959a1 [sledge sem] Add a README
5 years ago
Jules Villard 7a888170e7 [pudge] it's alive!
5 years ago
Scott Owens 49d95f40a2 [sledge sem] Adds a theorem about block processing order
5 years ago
Scott Owens 8d49b8d6ef [sledge sem] Remove some proof cheats
5 years ago
Scott Owens 9327f41880 [sledge sem] Organise the tranlation corectness proof
5 years ago
Scott Owens 2a6ababa99 [sledge sem] Rework emap invariant
5 years ago
Josh Berdine 6e4a729ab6 [sledge] Do not add simple constants to Equality relation representation
5 years ago
Josh Berdine 1b5302b4d2 [sledge] Simplify remainder of a rational by an integer
5 years ago
Josh Berdine fcd0e41ee6 [sledge] Return early for == args in Term compare and equal
5 years ago
Josh Berdine 76695690b8 [sledge] Do not simplify Mul and Div terms
5 years ago
Josh Berdine a3a6a5a6fe [sledge] Do not solve for Integer constants
5 years ago
Josh Berdine 32c5fb2837 [sledge] Do not represent Equality rep sparsely on constants
5 years ago
Josh Berdine de1689ac87 [sledge] Change And and Or terms from binary to flattened n-ary
5 years ago
Josh Berdine 87c8eb7c3a [sledge] Strengthen normalization of division
5 years ago
Josh Berdine cd72d3a82e [sledge] Simplify Term.Sum.to_term
5 years ago
Josh Berdine 2fc8bc1f84 [sledge] Export Term.map_rec_pre and add Term.fold_map_rec_pre
5 years ago
Josh Berdine 548928a839 [sledge] Strengthen Equality invariant to ensure carrier closed under subterms
5 years ago
Josh Berdine 2124be1c71 [sledge] Remove the "simplified" intermediate between interpreted and uninterpreted
5 years ago
Josh Berdine ee595f2ebf [sledge] Strengthen Equality.close to handle rep being sparse on constants
5 years ago
Josh Berdine 2f4f9801ed [sledge] Add Term.is_constant
5 years ago
Josh Berdine c91e09031f [sledge] Strengthen Equality normalization
5 years ago
Josh Berdine 0f50d3c248 [sledge] Do not solve polynomials for Mul or Div terms
5 years ago
Josh Berdine eb750ba6f9 [sledge] Avoid cyclic solutions to polynomial equations
5 years ago
Josh Berdine 1b20f02052 [sledge] Strengthen normalization of division, avoiding non-reals
5 years ago
Josh Berdine 4ea9eced05 [sledge] Improve Term.Sum.to_term
5 years ago
Josh Berdine 1a34e7eed2 [sledge] Add rational constants
5 years ago
Josh Berdine 7b33996072 [sledge] Use term height to avoid "pumpable" cyclic equations in Equality
5 years ago
Josh Berdine 6c03d88cf7 [sledge] Move Term.agg_size
5 years ago
Josh Berdine 0cee03aaa1 [sledge] Simplify identity type conversions only at initial construction
5 years ago
Josh Berdine 7e4673cbeb [sledge] Improve Equality invariant checking and debugging support
5 years ago
Josh Berdine 3c0924cf01 [sledge] Minor code improvement
5 years ago
Josh Berdine 60df5d6f3a [sledge] Fix Equality.Subst.compose to preserve physical equality
5 years ago
Josh Berdine 013b948dc4 [sledge] Rename extend to compose1 to avoid potential shadowing confusion
5 years ago
Josh Berdine fddb2fa991 [sledge] Add Map.map_endo
5 years ago
Josh Berdine ef63683a16 [sledge] Add Term.fold_map
5 years ago
Josh Berdine b35e3d30e0 [sledge] Add Map.fold_until
5 years ago
Josh Berdine b09f3774a4 [sledge] Add Qset.is_empty
5 years ago
Josh Berdine 165454e17d [sledge] Add Map and Qset operations to access top of underlying tree
5 years ago
Josh Berdine 7fdd3cccbb [sledge] Add Option.or_else
5 years ago
Josh Berdine 2aacc03880 [sledge] Remove eliminated existentials from equality relations
5 years ago
Josh Berdine 30c23f8cd6 [sledge] Fix term ordering bug between monomials and vars
5 years ago
Josh Berdine e7217ac5fe [sledge] Check equality of logical variables by id only
5 years ago
Josh Berdine c8e75e3b82 [sledge] Dump perf diagnostics and replays for slow queries to stderr
5 years ago
Josh Berdine a4e523b5b6 [sledge] Rename `*_preserves_phys_equal` to `*_endo` and clarify docs
5 years ago
Josh Berdine ec52259d31 [sledge] Substitute out alias of option when including Monad_syntax
5 years ago
Josh Berdine 1ae192dc0e [sledge] Use __LOC__ for Not_found_s
5 years ago
Josh Berdine ef0dfe0d70 [sledge] Fix doc of List.remove_exn
5 years ago
Josh Berdine d1de5db6c8 [sledge] Document Equality variable context handling
5 years ago
Josh Berdine 31dd2884f6 [sledge] Use a cookie instead of env var to enable ppx_trace
5 years ago
Josh Berdine 1ce5eb8033 [sledge] Suppress warning on dune build_info compilation
5 years ago
Josh Berdine 1364eccf18 [sledge] No longer need to Marshal with Closures support
5 years ago
Josh Berdine 461f88756d [sledge] Name the sledge library `sledge`
5 years ago
Josh Berdine ed82bca4a5 [sledge] Document that integer division and remainder use truncation semantics
5 years ago
Josh Berdine 3b4b2f3999 [sledge] Add replay debugging for Equality
5 years ago
Josh Berdine e83c6170e5 [sledge] Improve tracing in unit tests
5 years ago
Josh Berdine 9414cb4fb3 [sledge] Implement 'a iarray as ('a, immutable) Array.Permissioned.t
5 years ago
Josh Berdine fe62eeadab [sledge] Cleanup of Import
5 years ago
Josh Berdine 7ab19955bb [sledge] Implement Qset using Import.Map
5 years ago
Josh Berdine d5fe9aa11d [sledge] Define Map as a functor over the Tree underlying Core.Map
5 years ago
Josh Berdine ae3c059fe9 [sledge] Define Set as a functor over the Tree underlying Core.Set
5 years ago
Jules Villard 4e9f34efea [sledge] fix for `Equality.and_term`
5 years ago
Josh Berdine 6504f12029 [sledge] Rename Var.global to Var.is_global
5 years ago
Josh Berdine 9382b8120b [sledge] Improve IArray.map_adjacent
5 years ago
Josh Berdine 2fa0948e8d [sledge] Only fmt one (dbg) context, and suppress diff output
5 years ago
Josh Berdine fe09969a53 [sledge] Move basic function and tuple operations to Import0
5 years ago
Josh Berdine 8d6911416d [sledge] Add util for local exception to return early idiom
5 years ago
Josh Berdine 2ca98c80ff [sledge] Rename vector to iarray
5 years ago
Josh Berdine 2a5e0f692b [sledge] Move dep on Core to just bin
5 years ago
Josh Berdine 4d86832d7a [sledge] Do not open Base globally
5 years ago
Josh Berdine 06e4a2c08c [sledge] Dedup Qset interface
5 years ago
Josh Berdine 434c40e646 [sledge] Do not use Base.Map to implement Qset
5 years ago
Josh Berdine 152cc38e9b [sledge] Dedup Map signature
5 years ago
Josh Berdine 5dbb4a6fc2 [sledge] Dedup Set signature
5 years ago
Josh Berdine 42a8f774fd [sledge] Move Import.Map to separate module
5 years ago
Josh Berdine 252060ac7a [sledge] Remove unused ppx_custom_printf
5 years ago
Josh Berdine 93a9c823fc [sledge] Move Import.Set to separate module
5 years ago
Josh Berdine a4613f001d [sledge] Move Vector.pp out of Import.Vector wrapper
5 years ago
Josh Berdine c47881e664 [sledge] Remove dead Result.pp function
5 years ago
Josh Berdine 04df3ca460 [sledge] Move Import.List to separate module
5 years ago
Josh Berdine 24a26c8a23 [sledge] Move Import.Option to separate module
5 years ago
Josh Berdine 9c77d7b2a4 [sledge] Move some general type definitions from Import to Import0
5 years ago
Josh Berdine 124a1fed20 [sledge] Do not use Base.Set
5 years ago
Josh Berdine 57a8748e9f [sledge] Do not use Base.Map
5 years ago
Josh Berdine 134f9f930e [sledge] Adjust build system to allow building as a vendored dependency
5 years ago
Josh Berdine 8337097cf0 [sledge] Move Domain_itv and dependency on APRON from lib to bin
5 years ago
Josh Berdine 27f93b60da [sledge] Move ctypes dep from lib to bin
5 years ago
Josh Berdine 1c9bafc2a9 [sledge] Add beginnings of HACKING docs
5 years ago
Josh Berdine f5ab894675 [sledge] Dedup preprocess entries in dune files
5 years ago
Josh Berdine 0c7249b992 [sledge] Change build system to not generate dune files
5 years ago
Josh Berdine fff3a491bf [sledge] Bump version of dune language used, and format dune files
5 years ago
Josh Berdine 1798725632 [sledge] Add support to ppx_trace enable via environment variable
5 years ago
Josh Berdine c47199e31c [sledge] Simplify build for models
5 years ago
Josh Berdine 8880dd48eb [sledge] Remove base dep from ppx_trace
5 years ago
Josh Berdine b6ddd8fe8e [sledge] Rearrange into CLI binary and LLVM-independent library
5 years ago
Josh Berdine d5158f0787 [sledge] Move Reg.demangle to frontend
5 years ago
Josh Berdine 5eebe1c733 [sledge] Add entry-points config to Control.exec_opts
5 years ago
Josh Berdine dd026745af [sledge] Remove sledge/bin symlinks
5 years ago
Josh Berdine e6ccd3e497 [sledge] Minor tracing improvements
5 years ago
Josh Berdine 556739e17c [sledge] Minor optimization of Sh.bind_exists
5 years ago
Josh Berdine f80e0977cd [sledge] Make Sh.and_cong robust wrt conjoining to an unsat formula
5 years ago
Josh Berdine 37ddf95a49 [sledge] Strengthen and simplify canonizer for Extract terms
5 years ago
Josh Berdine f8a490d477 [sledge] Enforce variable context conditions in solver goals
5 years ago
Josh Berdine f8f47c0755 [sledge] Fix a few existential context fumbles
5 years ago
Josh Berdine 991c0c66e8 [sledge] Remove unnecessary vocabulary updates
5 years ago
Josh Berdine 8b8e156f83 [sledge] Make Solver.judgment a private type
5 years ago
Josh Berdine 9488a404ff [sledge] Compare logical variables by id only
5 years ago
Josh Berdine 0f1db1bd8b [sledge] Fix potential name clash when executing memmov
5 years ago
Josh Berdine 24c62fd39b [sledge] Strengthen canonizer of Extract terms
5 years ago
Josh Berdine 6a17078bec [sledge] Make context handling in Sh.or_ more robust
5 years ago
Josh Berdine 5d429ea075 [sledge] Improve Equality.extend
5 years ago
Josh Berdine f7707ff4be [sledge] Comments
5 years ago
Josh Berdine c8e2c3f895 [sledge] Detect inconsistent pure constraints during Sh simplification
5 years ago
Josh Berdine fa23e85bb4 [sledge] Dedup equality classes when printing
5 years ago
Josh Berdine 8383dcebb8 [sledge] Simplify states during symbolic execution
5 years ago
Josh Berdine b16e85d10d [sledge] Eliminate redundant existential quantifiers
5 years ago
Josh Berdine e520e8507d [sledge] Update Equality test results
5 years ago
Josh Berdine 9d97507e09 [sledge] Update and add Sh tests
5 years ago
Josh Berdine 33e702cd8b [sledge] Improve Sh printing for Sh-internal tracing
5 years ago
Josh Berdine a6f948c2c3 [sledge] Strengthen handling of existential segments
5 years ago
Josh Berdine b3cdac76e4 [sledge] Remove hacky treatment of tautologous existential equalities
5 years ago
Josh Berdine 80afaaee1b [sledge] Detect unsat subtrahend when subtracting pure terms
5 years ago
Josh Berdine b81fb893ea [sledge] Factor out Sh.and_subst
5 years ago
Josh Berdine fc2dbdd2fc [sledge] Strengthen existential witnessing for memory theory
5 years ago
Josh Berdine 0b88d99c79 [sledge] Strengthen quantifier witnessing
5 years ago
Josh Berdine ae8cd953f8 [sledge] Fix potential unsyncing of var contexts in solver
5 years ago
Josh Berdine a52085a718 [sledge] Fix Equality.canon to handle changing term classification
5 years ago
Josh Berdine 13aa772b68 [sledge] Strengthen normalization of equality between Concats
5 years ago
Josh Berdine 3369b27cf1 [sledge] Reorder Term definitions
5 years ago
Josh Berdine 2be566a09b [sledge] Fix Solver tracing
5 years ago
Josh Berdine 2a0eca669d [sledge] Move mediation between Term and Equality APIs from Sh to Equality
5 years ago
Josh Berdine 29eb8fa876 [sledge] Replace solution substitution trimming with partitioning
5 years ago
Josh Berdine 92b942e4ee [sledge] Simplify terminology from solvable to non-interpreted
5 years ago
Josh Berdine a34236bacd [sledge] Distinguish star and or when computing variable strength
5 years ago
Josh Berdine 63b8db2f8c [sledge] Reformat after promoting tests
5 years ago
Josh Berdine a8200b4957 [sledge] Don't need staged_pps anymore
5 years ago
Josh Berdine 9d3898044d [sledge] Canonize e / -1 to -1×e
5 years ago
Josh Berdine 65f38d68cc [sledge] Refactor to allow more recursion between arithmetic canonizer cases
5 years ago
Josh Berdine 99e6e9494b [sledge] Conditionally ignore equality relation when computing free variables
5 years ago
Scott Owens 8d95ef7e3c [sledge sem] Fix global variables
5 years ago
Josh Berdine 9d12f6502f [sledge] Make aggregate sizes explicit when constructing equalities
5 years ago
Josh Berdine 77cc835199 [sledge] Strengthen Equality.solve_for_vars to concatenate extracts
5 years ago
Josh Berdine f1d94d58b0 [sledge] Strengthen Equality.solve_for_vars for vars under Memory
5 years ago
Josh Berdine 54a3982b1d [sledge] Simplify variable occurrence checking in Equality.solve
5 years ago
Josh Berdine c8ed6dae63 [sledge] Optimize and simplify Equality.solve_interp_eqs
5 years ago
Josh Berdine ffdb429f5e [sledge] Factor solve_poly_eq out of solve_interp_eq
5 years ago
Josh Berdine f3f41fbdf2 [sledge] Filter out trivial pure constraints in Sh.map
5 years ago
Josh Berdine 1e32743312 [sledge] Add Shostak solver for aggregate theory
5 years ago
Josh Berdine 232372f083 [sledge] Factor orient out of solve
5 years ago
Josh Berdine a75f2701c3 [sledge] Lambda-lift Equality.solve_
5 years ago
Josh Berdine a7b0d68574 [sledge] Support Equality.solve generating fresh variables
5 years ago
Josh Berdine 79a74f07c5 [sledge] Pass universal context to Equality.solve
5 years ago
Josh Berdine 06fcb210c9 [sledge] Add Shostak canonizer for aggregate theory
5 years ago
Josh Berdine 7bb1ec073a [sledge] Strengthen Term.invariant on aggregates
5 years ago
Josh Berdine 539b4a0b46 [sledge] Add term to Extract a slice out of an aggregate value
5 years ago
Josh Berdine 8af2a4644a [sledge] Refine dropping of tautologous existential constraints
5 years ago
Josh Berdine 65cff68ae8 [sledge] Strengthen Solver's treatment of existentials using Equality
5 years ago
Josh Berdine 200091fc78 [sledge] Add Equality.Subst.trim
5 years ago
Josh Berdine f0a660792e [sledge] Add Equality.solve_for_vars
5 years ago
Josh Berdine 1afd4f55ba [sledge] Classify Memory and Concat terms as Simplified
5 years ago
Josh Berdine 173a5c0653 [sledge] Exclude equality relation from Sh.fold_vars
5 years ago
Josh Berdine 003479dcc1 [sledge] Factor primitive map function out of Sh.apply_subst
5 years ago
Josh Berdine de52574caf [sledge] Generalize Term.solve_zero_eq to specify solved-for subterm
5 years ago
Josh Berdine c52421bb6f [sledge] Refactor pp_diff from Equality to Map and List
5 years ago
Josh Berdine 5132a46c69 [sledge] Add Map.pp and use it for Var. and Equality.Subst.pp
5 years ago
Josh Berdine 66080d4b44 [sledge] Improve consistency of naming Equality pp functions
5 years ago
Josh Berdine 9b1ff9c012 [sledge] Factor solution substitutions into Equality.Subst
5 years ago
Josh Berdine f7a860401b [sledge] Move Term.solve to Equality
5 years ago
Josh Berdine 0b35328eb0 [sledge] Factor out solving polynomial = 0 equalities from solve
5 years ago
Josh Berdine 62dc914de7 [sledge] Use a defined variant type for Term.classify
5 years ago
Josh Berdine fad59b4dc4 [sledge] Add some missing Vector operations
5 years ago
Josh Berdine 2f0a0cf288 [sledge] Replace Memory and Concat Term constructors with eq_concat
5 years ago
Josh Berdine 0137186fe5 [sledge] Improve Solver tracing
5 years ago
Josh Berdine 18fd68f60a [sledge] Add Trace.infok
5 years ago
Josh Berdine ff65bcce1c [sledge] Minor simplification in Term.map
5 years ago
Josh Berdine 7f727df119 [sledge] Remove size of Splat exps and terms
5 years ago
Josh Berdine 2aa73f9946 [sledge] Use Int.sign instead of non-exhaustive matches
5 years ago
Josh Berdine b17cfd7db6 [sledge] Printing and tracing improvements
5 years ago
Josh Berdine 1ad2c9025a [sledge] Improve Sh docs
5 years ago
Josh Berdine 65f0b691a9 [sledge] Remove redundant `open`
5 years ago
Josh Berdine 84bb409412 [sledge] Sort arguments of Eq terms
5 years ago
Josh Berdine 9338bf1adb [sledge] Minor optimization of nop Var.Subst.freshen
5 years ago
Josh Berdine 914cd06e4d [sledge] Close Equality.classes under one-step congruence
5 years ago
Josh Berdine adb1e48467 [sledge] Simplify printing of symbolic heaps
5 years ago
Josh Berdine 960a9f76a0 [sledge] Remove some fragile patterns
5 years ago
Josh Berdine c52b49e6c0 [sledge] Add Term.Map and Var.Map
5 years ago
Josh Berdine 83c59dc795 [sledge] Simplify Sh.fold_terms to fold_vars
5 years ago
Josh Berdine 01825598f7 [sledge] Equality.and_eq is part of the exposed interface
5 years ago
Josh Berdine 6e01fa91d5 [sledge] Replace Set.inter_diff with clearer diff_inter
5 years ago
Josh Berdine b8833b76b8 [sledge] Add classic equality tests for arithmetic and congruence
5 years ago
Josh Berdine 8fb0632aba [sledge] Add test Makefile targets for generating Llair code
5 years ago
Josh Berdine c9a0b06be2 [sledge] Update expected test results
5 years ago
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
6 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