Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Optimize and refactor "Hoare" domains #809

Merged
merged 81 commits into from
Sep 20, 2022
Merged

Optimize and refactor "Hoare" domains #809

merged 81 commits into from
Sep 20, 2022

Commits on Jul 29, 2022

  1. Add tests to show buggy Hoare domain usage

    @sim642
    sim642 committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    768b4fb View commit details
    Browse the repository at this point in the history

  2. Attempt to reimplement AddressDomain using projective hoare domain

    @sim642
    sim642 committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    ec013be View commit details
    Browse the repository at this point in the history

  3. Attempt to reimplement AddressDomain using pairwise hoare domain

    @sim642
    sim642 committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    7ad1c08 View commit details
    Browse the repository at this point in the history

  4. Fix projective AddressDomain by wrapping pairwise

    @sim642
    sim642 committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    bda314f View commit details
    Browse the repository at this point in the history

  5. Use more precise AddressDomain projection

    @sim642
    sim642 committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    1925e6c View commit details
    Browse the repository at this point in the history

  6. Add example for old hash-based AddressDomain projection

    @sim642
    sim642 committed Jul 29, 2022
    Configuration menu
    Copy the full SHA
    1896076 View commit details
    Browse the repository at this point in the history

Commits on Aug 1, 2022

  1. Deprecate HoareDomain.HoarePO

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    82fb030 View commit details
    Browse the repository at this point in the history

  2. Add joined set abstraction

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    61690ed View commit details
    Browse the repository at this point in the history

  3. Attempt to use Hoare domain for AddressDomain buckets

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    ca0f3d8 View commit details
    Browse the repository at this point in the history

  4. Fix HoareDomain.Pairwise narrow

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    a0555e7 View commit details
    Browse the repository at this point in the history

  5. Fix ValueDomain.widen calling AddressDomain.widen incorrectly

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    c5f6698 View commit details
    Browse the repository at this point in the history

  6. Revert to projective AddressDomain

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    74fafef View commit details
    Browse the repository at this point in the history

  7. Use HoareDomain.Pairwise for PathSensitive2

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    58dd22a View commit details
    Browse the repository at this point in the history

  8. Fix Lval.Offset joinability transitivity

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    ff03d1c View commit details
    Browse the repository at this point in the history

  9. Add asserts about s1_match cardinality in HoareDomain.Pairwise

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    288c1ea View commit details
    Browse the repository at this point in the history

  10. Remove is_element from HoareDomains

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    9f9ccbd View commit details
    Browse the repository at this point in the history

  11. Optimize and refactor HoareDomain.Projective

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    7438b26 View commit details
    Browse the repository at this point in the history

  12. Optimize and refactor HoareDomain.Pairwise

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    cd50cd9 View commit details
    Browse the repository at this point in the history

  13. Replace module E with type elt in HoareDomain.NewS

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    e2b3048 View commit details
    Browse the repository at this point in the history

  14. Rename should_join -> cong in HoareDomain

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    14cfb4d View commit details
    Browse the repository at this point in the history

  15. Make HoareDomain.Pairwise asserts exact

    @sim642
    sim642 committed Aug 1, 2022
    Configuration menu
    Copy the full SHA
    fd93942 View commit details
    Browse the repository at this point in the history

Commits on Aug 2, 2022

  1. Update LvalTest

    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    6bc127e View commit details
    Browse the repository at this point in the history

  2. Extract SensitiveDomains

    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    da9c786 View commit details
    Browse the repository at this point in the history

  3. Move HoareDomain.Joined -> SetDomain.Joined

    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    41e39fb View commit details
    Browse the repository at this point in the history

  4. Remove SensitiveDomain.NewS

    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    1113247 View commit details
    Browse the repository at this point in the history

  5. Rename SensitiveDomain.Equivalence -> Congruence

    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    77792bd View commit details
    Browse the repository at this point in the history

  6. Add SensitiveDomain.Combined

    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    1e006d6 View commit details
    Browse the repository at this point in the history

  7. Weaken SensitiveDomain E argument signatures

    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    b792000 View commit details
    Browse the repository at this point in the history

  8. Fix MapDomainTest

    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    6f88615 View commit details
    Browse the repository at this point in the history

  9. Rename Q -> C in Sensitive.Pairwise

    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    fed13ae View commit details
    Browse the repository at this point in the history

  10. Implement missing SetDomain.Joined operations 

    remove/diff is needed when using Joined with AddressDomain
    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    868519f View commit details
    Browse the repository at this point in the history

  11. Handle Lattice.BotValue in SensitiveDomain

    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    3db120e View commit details
    Browse the repository at this point in the history

  12. Make SensitiveDomain.Congruence over elt not t in Combined

    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    d77e476 View commit details
    Browse the repository at this point in the history

  13. Clean up AddressDomain construction

    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    d012f03 View commit details
    Browse the repository at this point in the history

  14. Clean up PathSensitive2 construction

    @sim642
    sim642 committed Aug 2, 2022
    Configuration menu
    Copy the full SHA
    8d6b8cf View commit details
    Browse the repository at this point in the history

Commits on Aug 3, 2022

  1. Add assert to 00-sanity/34-hoare-over-addrs

    @sim642
    sim642 committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    fdcb8c4 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'hoare-use-bugs' into hoaredomain-new

    @sim642
    sim642 committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    32f8567 View commit details
    Browse the repository at this point in the history

  3. Expand descriptions of hoare-over tests

    @sim642
    sim642 committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    51c8c01 View commit details
    Browse the repository at this point in the history

  4. Merge branch 'master' into hoaredomain-new

    @sim642
    sim642 committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    5f4d3e1 View commit details
    Browse the repository at this point in the history

  5. Switch AddressDomain back to Joined for StrPtr compatibility

    @sim642
    sim642 committed Aug 3, 2022
    Configuration menu
    Copy the full SHA
    5625a63 View commit details
    Browse the repository at this point in the history

Commits on Aug 4, 2022

  1. Implement Map versions of SensitiveDomain for WitnessConstraints

    @sim642
    sim642 committed Aug 4, 2022
    Configuration menu
    Copy the full SHA
    e3bbd31 View commit details
    Browse the repository at this point in the history

  2. Use PairwiseMap for PathSensitive.Sync

    @sim642
    sim642 committed Aug 4, 2022
    Configuration menu
    Copy the full SHA
    ae50c20 View commit details
    Browse the repository at this point in the history

Commits on Aug 5, 2022

  1. Add physical equality short-circuiting to AddressDomain

    @sim642
    sim642 committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    d04cd22 View commit details
    Browse the repository at this point in the history

  2. Add value output to PairwiseMap

    @sim642
    sim642 committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    b261e20 View commit details
    Browse the repository at this point in the history

  3. Use normal sets for WitnessConstraints ranges

    @sim642
    sim642 committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    bc1527f View commit details
    Browse the repository at this point in the history

  4. Remove commented out sensitive map code

    @sim642
    sim642 committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    24a2fd1 View commit details
    Browse the repository at this point in the history

  5. Use MapDomain.S for PairwiseMap

    @sim642
    sim642 committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    421cf57 View commit details
    Browse the repository at this point in the history

  6. Add Set suffix to SensitiveDomain sets

    @sim642
    sim642 committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    13ec33e View commit details
    Browse the repository at this point in the history

  7. Reuse Set and Map printing for SensitiveDomain

    @sim642
    sim642 committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    e39c3fc View commit details
    Browse the repository at this point in the history

  8. Implement pretty_diff for SensitiveDomains

    @sim642
    sim642 committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    8a7b601 View commit details
    Browse the repository at this point in the history

  9. Remove Node and Edge modules from WitnessConstraints

    @sim642
    sim642 committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    9ded167 View commit details
    Browse the repository at this point in the history

  10. Merge branch 'hoaredomain-new-map' into hoaredomain-new

    @sim642
    sim642 committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    47d2bec View commit details
    Browse the repository at this point in the history

  11. Deprecate HoareDomain.MapBot and SetDomain.SensitiveConf

    @sim642
    sim642 committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    7e109cc View commit details
    Browse the repository at this point in the history

  12. Document sensitive domains and related

    @sim642
    sim642 committed Aug 5, 2022
    Configuration menu
    Copy the full SHA
    4782ccd View commit details
    Browse the repository at this point in the history

Commits on Aug 8, 2022

  1. Debug PathSensitive3 sync Not_found crash

    @sim642
    sim642 committed Aug 8, 2022
    Configuration menu
    Copy the full SHA
    3c35b20 View commit details
    Browse the repository at this point in the history

  2. Work around old LibraryFunctions spawning even with sem.unknown_funct… 

    …ion.spawn disabled
    @sim642
    sim642 committed Aug 8, 2022
    Configuration menu
    Copy the full SHA
    e5799bc View commit details
    Browse the repository at this point in the history

  3. Fix GraphML witnesses with threadspawn

    @sim642
    sim642 committed Aug 8, 2022
    Configuration menu
    Copy the full SHA
    dd0c0fe View commit details
    Browse the repository at this point in the history

  4. Add witness lifter fixpoint not reached test from sv-benchmarks

    @sim642
    sim642 committed Aug 8, 2022
    Configuration menu
    Copy the full SHA
    1afc8f3 View commit details
    Browse the repository at this point in the history

  5. Fix fixpoint not reached error in sv-benchmarks

    @sim642
    sim642 committed Aug 8, 2022
    Configuration menu
    Copy the full SHA
    cde436f View commit details
    Browse the repository at this point in the history

Commits on Aug 10, 2022

  1. Merge branch 'master' into hoaredomain-new

    @sim642
    sim642 committed Aug 10, 2022
    Configuration menu
    Copy the full SHA
    5cb2778 View commit details
    Browse the repository at this point in the history

Commits on Aug 11, 2022

  1. Revert "Fix Lval.Offset joinability transitivity" 

    This reverts commit ff03d1c.
    @sim642
    sim642 committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    4d4c045 View commit details
    Browse the repository at this point in the history

  2. Remove index 0 and first field handling attempt from AddressDomain bu… 

    …ckets
    @sim642
    sim642 committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    881ad37 View commit details
    Browse the repository at this point in the history

  3. Remove PairwiseSet from AddressDomain

    @sim642
    sim642 committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    224a4b6 View commit details
    Browse the repository at this point in the history

  4. Remove unused trace_enabled from MapDomain.PMap

    @sim642
    sim642 committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    bd0bc27 View commit details
    Browse the repository at this point in the history

  5. Revert "Update LvalTest" 

    This reverts commit 6bc127e.
    @sim642
    sim642 committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    a0a375a View commit details
    Browse the repository at this point in the history

  6. Merge branch 'hoaredomain-new-ad-proj' into hoaredomain-new

    @sim642
    sim642 committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    8d78694 View commit details
    Browse the repository at this point in the history

  7. Document Lval special cases not used by AddressDomain splitting any more

    @sim642
    sim642 committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    c19a345 View commit details
    Browse the repository at this point in the history

  8. Rename SensitiveDomain -> DisjointDomain

    @sim642
    sim642 committed Aug 11, 2022
    Configuration menu
    Copy the full SHA
    4e2057e View commit details
    Browse the repository at this point in the history

Commits on Aug 22, 2022

  1. Add witness lifter path sensitive unsound branch test

    @sim642
    sim642 committed Aug 22, 2022
    Configuration menu
    Copy the full SHA
    3a2a226 View commit details
    Browse the repository at this point in the history

  2. Fix witness lifter mishandling Deadcode exceptions

    @sim642
    sim642 committed Aug 22, 2022
    Configuration menu
    Copy the full SHA
    9e52524 View commit details
    Browse the repository at this point in the history

Commits on Aug 24, 2022

  1. Move commented-out add code in MapDomain

    @sim642
    sim642 committed Aug 24, 2022
    Configuration menu
    Copy the full SHA
    256fa17 View commit details
    Browse the repository at this point in the history

  2. Improve HoareDomain and DisjointDomain documentation

    @sim642
    sim642 committed Aug 24, 2022
    Configuration menu
    Copy the full SHA
    236c76e View commit details
    Browse the repository at this point in the history

  3. Rename HoareDomain.Set2 -> SetEM

    @sim642
    sim642 committed Aug 24, 2022
    Configuration menu
    Copy the full SHA
    b16700a View commit details
    Browse the repository at this point in the history

  4. Move and document Lval bucket representatives

    @sim642
    sim642 committed Aug 24, 2022
    Configuration menu
    Copy the full SHA
    2946dcd View commit details
    Browse the repository at this point in the history

  5. Use SetDomain.Print for AddressDomain

    @sim642
    sim642 committed Aug 24, 2022
    Configuration menu
    Copy the full SHA
    a2d0cea View commit details
    Browse the repository at this point in the history

Commits on Sep 2, 2022

  1. Fix comment typo in AddressDomain 

    Co-authored-by: Michael Schwarz <michael.schwarz93@gmail.com>
    @sim642 @michael-schwarz
    sim642 and michael-schwarz committed Sep 2, 2022
    Configuration menu
    Copy the full SHA
    901a709 View commit details
    Browse the repository at this point in the history

  2. Document SetDomain strong removal

    @sim642
    sim642 committed Sep 2, 2022
    Configuration menu
    Copy the full SHA
    41bfdba View commit details
    Browse the repository at this point in the history

  3. Document abstract SetDomain element-wise operations

    @sim642
    sim642 committed Sep 2, 2022
    Configuration menu
    Copy the full SHA
    f630ebf View commit details
    Browse the repository at this point in the history

  4. Use physical equality short-circuit for AddressDomain.leq

    @sim642
    sim642 committed Sep 2, 2022
    Configuration menu
    Copy the full SHA
    c975d09 View commit details
    Browse the repository at this point in the history

  5. Merge branch 'master' into hoaredomain-new

    @sim642
    sim642 committed Sep 2, 2022
    Configuration menu
    Copy the full SHA
    cafb5fa View commit details
    Browse the repository at this point in the history

  6. Add address domain first field and zero index tests

    @sim642
    sim642 committed Sep 2, 2022
    Configuration menu
    Copy the full SHA
    af734d8 View commit details
    Browse the repository at this point in the history