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

Split Class into ByReferenceClass and ByValueClass #1227

Closed
wants to merge 28 commits into from
Closed

Split Class into ByReferenceClass and ByValueClass #1227

wants to merge 28 commits into from

Commits on May 31, 2024

  1. Create separate classes for by reference and by value classes

    @superaxander
    superaxander committed May 31, 2024
    Configuration menu
    Copy the full SHA
    d52394f View commit details
    Browse the repository at this point in the history

Commits on Jun 11, 2024

  1. Use ADT encoding for ByValueClasses

    @superaxander
    superaxander committed Jun 11, 2024
    Configuration menu
    Copy the full SHA
    b01df4d View commit details
    Browse the repository at this point in the history

Commits on Jun 17, 2024

  1. Add some axioms that speed up pointer verification

    @superaxander
    superaxander committed Jun 17, 2024
    Configuration menu
    Copy the full SHA
    1666b35 View commit details
    Browse the repository at this point in the history

Commits on Jun 18, 2024

  1. Do no copy in expressions which do not yield TByValueClass

    @superaxander
    superaxander committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    0dfde7c View commit details
    Browse the repository at this point in the history

  2. Enable use of methods on by-value classes

    @superaxander
    superaxander committed Jun 18, 2024
    Configuration menu
    Copy the full SHA
    be64b27 View commit details
    Browse the repository at this point in the history

Commits on Jun 19, 2024

  1. Set --useOldAxiomatization to test which test failures are because of… 

    … me and which aren't
    @superaxander
    superaxander committed Jun 19, 2024
    Configuration menu
    Copy the full SHA
    aed3ba6 View commit details
    Browse the repository at this point in the history

Commits on Jul 18, 2024

  1. Improve struct encoding, rewrite tests for new permission syntax

    @superaxander
    superaxander committed Jul 18, 2024
    Configuration menu
    Copy the full SHA
    53f19a8 View commit details
    Browse the repository at this point in the history

Commits on Jul 19, 2024

  1. Make the pointer for struct fields implicit simplifying most locations 

    in the transformations stages
    @superaxander
    superaxander committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    7b50ef3 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/dev' into class-by-value

    @superaxander
    superaxander committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    28eaee6 View commit details
    Browse the repository at this point in the history

  3. Fix the type numbers

    @superaxander
    superaxander committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    1a31edd View commit details
    Browse the repository at this point in the history

  4. Replaced type numbers with constants for ByValueClass

    @superaxander
    superaxander committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    3f9f02b View commit details
    Browse the repository at this point in the history

  5. Temporarily set a fork of silicon in build.sc to test in CI

    @superaxander
    superaxander committed Jul 19, 2024
    Configuration menu
    Copy the full SHA
    bcd96b5 View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2024

  1. Update silver, clean up unused ByValueClass axioms

    @superaxander
    superaxander committed Jul 23, 2024
    Configuration menu
    Copy the full SHA
    24197b8 View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2024

  1. First working version pointer casts

    @superaxander
    superaxander committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    653cd5f View commit details
    Browse the repository at this point in the history

  2. Also get rid of casts from Object to another class

    @superaxander
    superaxander committed Jul 24, 2024
    Configuration menu
    Copy the full SHA
    88305b8 View commit details
    Browse the repository at this point in the history

Commits on Jul 25, 2024

  1. Ignore quantifier in SimplifyNestedQuantifiers if it has a trigger an… 

    …d clean up ClassToRef
    @superaxander
    superaxander committed Jul 25, 2024
    Configuration menu
    Copy the full SHA
    d736fdd View commit details
    Browse the repository at this point in the history

  2. Fix compilation error

    @superaxander
    superaxander committed Jul 25, 2024
    Configuration menu
    Copy the full SHA
    2615361 View commit details
    Browse the repository at this point in the history

  3. Reduce code duplication in adtPointer, remove all non-pointer casts i… 

    …n classToRef
    @superaxander
    superaxander committed Jul 25, 2024
    Configuration menu
    Copy the full SHA
    6c8be0a View commit details
    Browse the repository at this point in the history

  4. Fix duplicate OptGet and add asType function to primitive pointer arrays

    @superaxander
    superaxander committed Jul 25, 2024
    Configuration menu
    Copy the full SHA
    e141bcf View commit details
    Browse the repository at this point in the history

  5. Get rid of more 'unknown' names in the C frontend

    @superaxander
    superaxander committed Jul 25, 2024
    Configuration menu
    Copy the full SHA
    401c3d9 View commit details
    Browse the repository at this point in the history

  6. Remove Viper field access from trigger with top-level PointerSubscrip… 

    …t or DerefPointer

* Gives a 12% performance improvement on Silicon for examples/concepts/c/structs.c
    @superaxander
    superaxander committed Jul 25, 2024
    Configuration menu
    Copy the full SHA
    a1773b7 View commit details
    Browse the repository at this point in the history

Commits on Aug 19, 2024

  1. Merge remote-tracking branch 'origin/dev' into class-by-value

    @superaxander
    superaxander committed Aug 19, 2024
    Configuration menu
    Copy the full SHA
    98dde38 View commit details
    Browse the repository at this point in the history

Commits on Aug 21, 2024

  1. Implement basic pointer casts

    @superaxander
    superaxander committed Aug 21, 2024
    Configuration menu
    Copy the full SHA
    42aca99 View commit details
    Browse the repository at this point in the history

Commits on Aug 22, 2024

  1. Add pointer cast helpers in loops

    @superaxander
    superaxander committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    9b96b33 View commit details
    Browse the repository at this point in the history

  2. Add type checking for pointer casts

    @superaxander
    superaxander committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    800f1dd View commit details
    Browse the repository at this point in the history

  3. Add back blame erroneously removed by the previous commit

    @superaxander
    superaxander committed Aug 22, 2024
    Configuration menu
    Copy the full SHA
    c7a723e View commit details
    Browse the repository at this point in the history

Commits on Aug 26, 2024

  1. Fix unsupported cast test

    @superaxander
    superaxander committed Aug 26, 2024
    Configuration menu
    Copy the full SHA
    f025706 View commit details
    Browse the repository at this point in the history

Commits on Sep 13, 2024

  1. Fix unsoundness in pointer cast encoding

    @superaxander
    superaxander committed Sep 13, 2024
    Configuration menu
    Copy the full SHA
    d85b6b4 View commit details
    Browse the repository at this point in the history