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

Lithium: a Rust-native back end #1321

Open
wants to merge 55 commits into
base: master
Choose a base branch
from
Open

Lithium: a Rust-native back end #1321

wants to merge 55 commits into from

Commits on Oct 22, 2023

  1. Add Lithium back end

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    0928308 View commit details
    Browse the repository at this point in the history

  2. Add Lithium to VerificationBackend enum

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    6821cff View commit details
    Browse the repository at this point in the history

  3. Fix simple branching (if-statements in low vir)

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    eb4c416 View commit details
    Browse the repository at this point in the history

  4. Wonky way of reporting offending positions

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    daceb78 View commit details
    Browse the repository at this point in the history

  5. Fix branching assumptions for switchInt

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    35843ff View commit details
    Browse the repository at this point in the history

  6. Fix "otherwise" branch of switchInt statements

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    74b090f View commit details
    Browse the repository at this point in the history

  7. Fix after rebase

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    f6e7e11 View commit details
    Browse the repository at this point in the history

  8. Add tests for loops, remove empty Conditional statements

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    33fe480 View commit details
    Browse the repository at this point in the history

  9. Fix mod operator

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    e3cb301 View commit details
    Browse the repository at this point in the history

  10. Add initial F32 and F64 support

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    c68d489 View commit details
    Browse the repository at this point in the history

  11. Use FP operators, choose correct type declaration

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    9caacd3 View commit details
    Browse the repository at this point in the history

  12. Tests for floating-point support

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    412772f View commit details
    Browse the repository at this point in the history

  13. Add preamble for CVC5, split fp.neq into 32 and 64-bit variants

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    9f3b962 View commit details
    Browse the repository at this point in the history

  14. Fixes after merge

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    f69cb0b View commit details
    Browse the repository at this point in the history

  15. Quantifiers to snapshots, fix unsized type bound checking bug

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    62f4a9b View commit details
    Browse the repository at this point in the history

  16. Hack quantifier generation for complex types

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    08c1e9e View commit details
    Browse the repository at this point in the history

  17. Fix after rebase

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    d195597 View commit details
    Browse the repository at this point in the history

  18. Fix lowering for quantifiers that use closures over function arguments

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    ada6736 View commit details
    Browse the repository at this point in the history

  19. Add sum-of-primes test file

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    6370a93 View commit details
    Browse the repository at this point in the history

  20. Add super sale test case

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    64d8cd2 View commit details
    Browse the repository at this point in the history

  21. Update test cases

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    fda0031 View commit details
    Browse the repository at this point in the history

  22. Add Euclid test case, fix quantifiers type mismatch

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    15579d1 View commit details
    Browse the repository at this point in the history

  23. Optimization module

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    fcfeda2 View commit details
    Browse the repository at this point in the history

  24. Correct reporting of failure reason positions

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    9a6c479 View commit details
    Browse the repository at this point in the history

  25. Remove redundant reasons for failure if the same as failing place

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    4585665 View commit details
    Browse the repository at this point in the history

  26. FP != for Viper

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    4b5e026 View commit details
    Browse the repository at this point in the history

  27. Passing FP test case

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    ddddb3a View commit details
    Browse the repository at this point in the history

  28. Remove main.rs from Lithium

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    c36a25d View commit details
    Browse the repository at this point in the history

  29. Commit the config

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    9b08400 View commit details
    Browse the repository at this point in the history

  30. Use files, not stdio, fix negative int encoding

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    c8a4d51 View commit details
    Browse the repository at this point in the history

  31. Make clippy happy

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    4e368ac View commit details
    Browse the repository at this point in the history

  32. cargo fmt

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    9ad4f34 View commit details
    Browse the repository at this point in the history

  33. More cargo fmt

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    614ebc1 View commit details
    Browse the repository at this point in the history

  34. Increase SMT timeout, comment out problematic code in error_manager

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    fc2e056 View commit details
    Browse the repository at this point in the history

  35. Fix abs(i32::MIN) overflowing

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    41bbaaa View commit details
    Browse the repository at this point in the history

  36. Refactor encoding of Statement::Conditional

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    6f3ffcc View commit details
    Browse the repository at this point in the history

  37. Fix invalid file paths when emitting SMT files

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    25ee57b View commit details
    Browse the repository at this point in the history

  38. Fix quantifier optimization rules

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    6fedb19 View commit details
    Browse the repository at this point in the history

  39. Various bugfixes

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    56c0678 View commit details
    Browse the repository at this point in the history

  40. Make sure positions are preserved by the optimizer

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    f7bec36 View commit details
    Browse the repository at this point in the history

  41. Add bisect test case

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    bc085e4 View commit details
    Browse the repository at this point in the history

  42. Remove overcomplicated tests

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    1ad0fbe View commit details
    Browse the repository at this point in the history

  43. Fix test error placement

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    d97b664 View commit details
    Browse the repository at this point in the history

  44. Clean up SMT preambles, fix modulo operator encoding

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    8e18928 View commit details
    Browse the repository at this point in the history

  45. Add Lithium test coverage script 

    To be removed when we want to merge this into Prusti. Committing for now since it's relevant to my thesis.
    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    6a216fe View commit details
    Browse the repository at this point in the history

  46. Fixes after merging master

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    18db007 View commit details
    Browse the repository at this point in the history

  47. Make clippy happy

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    dce49bb View commit details
    Browse the repository at this point in the history

  48. Fix test compilation error

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    9ba703d View commit details
    Browse the repository at this point in the history

  49. Restore config

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    18bc02f View commit details
    Browse the repository at this point in the history

  50. Fixes after rebase

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    9aed8af View commit details
    Browse the repository at this point in the history

  51. Clippy

    @JakuJ
    JakuJ committed Oct 22, 2023
    Configuration menu
    Copy the full SHA
    8372022 View commit details
    Browse the repository at this point in the history

Commits on Oct 27, 2023

  1. Fix stopwatch getting released immediately

    @JakuJ
    JakuJ committed Oct 27, 2023
    Configuration menu
    Copy the full SHA
    000c701 View commit details
    Browse the repository at this point in the history

  2. Merge branch 'master' into lithium

    @JakuJ
    JakuJ committed Oct 27, 2023
    Configuration menu
    Copy the full SHA
    cb38222 View commit details
    Browse the repository at this point in the history

  3. Add PRUSTI_NATIVE_VERIFIER env variable

    @JakuJ
    JakuJ committed Oct 27, 2023
    Configuration menu
    Copy the full SHA
    09066e1 View commit details
    Browse the repository at this point in the history

  4. Restore test case unrelated to Lithium

    @JakuJ
    JakuJ committed Oct 27, 2023
    Configuration menu
    Copy the full SHA
    7664629 View commit details
    Browse the repository at this point in the history