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

Update VCLLVM (now Pallas) to LLVM 17, update to newest VerCors version, and convert more instructions to COL #1159

Merged
merged 53 commits into from
Oct 15, 2024
Merged

Update VCLLVM (now Pallas) to LLVM 17, update to newest VerCors version, and convert more instructions to COL #1159

merged 53 commits into from
Oct 15, 2024

Commits on May 30, 2024

  1. Rename VCLLVM to Pallas, Update to LLVM 17, Implement Stack Allocation

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

  2. Fixed the LLVM tests, add a blame for LLVM generated nodes, add 

    formatting hook with clang-format
    @superaxander
    superaxander committed May 30, 2024
    Configuration menu
    Copy the full SHA
    5cb4a2e View commit details
    Browse the repository at this point in the history

Commits on May 31, 2024

  1. Use absolute path for finding Pallas shared library

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

  2. Remove pallas binary from output jar

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

  3. 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

  2. Merge branch 'class-by-value' into pallas

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

  3. Make the LLVM file verify again

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

Commits on Aug 28, 2024

  1. Implement basic pointer type inference for LLVM

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

Commits on Aug 29, 2024

  1. Pass-through debug locations from LLVM

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

Commits on Sep 2, 2024

  1. Improved pointer type inference

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

  2. Fix crash when transforming fib.ll

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

Commits on Sep 4, 2024

  1. Convert LLVM loops into COL

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

  2. Fix broken test with LLVM pure functions

    @superaxander
    superaxander committed Sep 4, 2024
    Configuration menu
    Copy the full SHA
    55b69e3 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
    72cb421 View commit details
    Browse the repository at this point in the history

Commits on Sep 17, 2024

  1. Allow casting back up to "greater" type

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

Commits on Sep 30, 2024

  1. Move PointerAdd logic for PointerLocations to ImportPointer

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

Commits on Oct 1, 2024

  1. Merge remote-tracking branch 'origin/dev' into pallas

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

  2. Add pointer post condition in attempt to fix injectivity issue

    @superaxander
    superaxander committed Oct 1, 2024
    Configuration menu
    Copy the full SHA
    82b53fe View commit details
    Browse the repository at this point in the history

Commits on Oct 4, 2024

  1. Make all but one HaliVer example verify again with the new struct enc… 

    …oding
    @superaxander
    superaxander committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    e2ce374 View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/dev' into pallas

    @superaxander
    superaxander committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    5f32f5b View commit details
    Browse the repository at this point in the history

  3. Merge PointerArray fallibility and nullability

    @superaxander
    superaxander committed Oct 4, 2024
    Configuration menu
    Copy the full SHA
    dee46c0 View commit details
    Browse the repository at this point in the history

Commits on Oct 7, 2024

  1. Clean up the PR

    @superaxander
    superaxander committed Oct 7, 2024
    Configuration menu
    Copy the full SHA
    8566c4b View commit details
    Browse the repository at this point in the history

Commits on Oct 9, 2024

  1. Integrate Bob's feedback

    @superaxander
    superaxander committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    60b419d View commit details
    Browse the repository at this point in the history

  2. Merge remote-tracking branch 'origin/dev' into pallas

    @superaxander
    superaxander committed Oct 9, 2024
    Configuration menu
    Copy the full SHA
    283fb6f View commit details
    Browse the repository at this point in the history

Commits on Oct 10, 2024

  1. Revert some changes which caused tests to fail

    @superaxander
    superaxander committed Oct 10, 2024
    Configuration menu
    Copy the full SHA
    ea45b98 View commit details
    Browse the repository at this point in the history

Commits on Oct 11, 2024

  1. Remove supports from ByValueClass and remove useless LLVM coercions

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

Commits on Oct 15, 2024

  1. Incorporate last remaining feedback from Bob

    @superaxander
    superaxander committed Oct 15, 2024
    Configuration menu
    Copy the full SHA
    bbe95cc View commit details
    Browse the repository at this point in the history