Re-enable CI, switch to ui_test (#63)

* fix tests compilation * reenable CI, switch to ui_test * fix encoding of overflowing binops * switch test annotations to ui_test syntax * address clippy lints * reformat * ignore reformat in blame * port cargo tests to ui_test * only Linux on CI, fix stable toolchain contracts
Aurel300 · Oct 31, 2024 · 9f76604 · 9f76604
1 parent fc23fce
commit 9f76604
Show file tree

Hide file tree

Showing 305 changed files with 2,733 additions and 2,399 deletions.
diff --git a/.git-blame-ignore-revs b/.git-blame-ignore-revs
@@ -0,0 +1,3 @@
+# hashes of reformat commits
+7353a97cb8211e480ee7e740c7f0b7aa74f334ba
+
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -2,10 +2,10 @@ name: Test
 
 on:
   push:
-    branches: [master, staging, trying]
+    branches: [master, rewrite-2023, staging, trying]
     paths-ignore: 'docs/**'
   pull_request:
-    branches: [master]
+    branches: [master, rewrite-2023]
     paths-ignore: 'docs/**'
 
 # Cancel previous runs in a PR when pushing new commits
@@ -85,130 +85,34 @@ jobs:
   # Run a subset of the tests that used to fail often.
   # The goal here is to fail fast and give quick feedback to the developers.
   # This job intentionally doesn't use the verification cache.
-  quick-tests:
-    runs-on: ubuntu-latest
-    env:
-      PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin
-    steps:
-      - name: Check out the repo
-        uses: actions/checkout@v2
-      - name: Set up Java
-        uses: actions/setup-java@v1
-        with:
-          java-version: '15'
-      - name: Set up the environment
-        run: python x.py setup
-      - name: Cache cargo
-        uses: Swatinem/rust-cache@v2
-        with:
-          shared-key: "shared"
-      - name: Build with cargo
-        run: python x.py build --all
-      - name: Run quick tests
-        run: python x.py test --all quick
-
-  # Run a subset of the tests with the purification optimization enabled
-  # to ensure that we do not introduce regressions.
-  purification-tests:
-    needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests]
-    runs-on: ubuntu-latest
-    env:
-      PRUSTI_ENABLE_PURIFICATION_OPTIMIZATION: true
-      PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin
-    steps:
-      - name: Check out the repo
-        uses: actions/checkout@v2
-      - name: Set up Java
-        uses: actions/setup-java@v1
-        with:
-          java-version: '15'
-      - name: Set up the environment
-        run: python x.py setup
-      - name: Cache cargo
-        uses: Swatinem/rust-cache@v2
-        with:
-          shared-key: "shared"
-      - name: Prepare verification cache keys
-        shell: bash
-        run: |
-          VER_CACHE_KEY_SHARED=prusti-cache-$(cat viper-toolchain)-$(date +%Y-%m)
-          echo "VER_CACHE_KEY_SHARED=$VER_CACHE_KEY_SHARED" >> $GITHUB_ENV
-          echo "VER_CACHE_KEY_UNIQUE=$VER_CACHE_KEY_SHARED-${RANDOM}${RANDOM}" >> $GITHUB_ENV
-      - name: Load verification cache
-        uses: actions/cache@v3
-        with:
-          path: ${{ env.PRUSTI_CACHE_PATH }}
-          # Use a unique key, so that the job will always store the cache at the end of the run
-          key: ${{ env.VER_CACHE_KEY_UNIQUE }}
-          # Restore from the most recent cache that matches a shared prefix of the key
-          restore-keys: ${{ env.VER_CACHE_KEY_SHARED }}
-      - name: Build with cargo
-        run: python x.py build --all
-      - name: Run quick tests
-        run: |
-          python x.py verify-test prusti-tests/tests/verify/pass/rosetta/Knuth_shuffle.rs
-          # python x.py test --all pass/rosetta/Binary_search_shared.rs
-          # python x.py test --all pass/demos/account.rs
-          # python x.py test --all pass/rosetta/Knights_tour.rs
-          # python x.py test --all pass/quick/fold-unfold.rs
-          # python x.py test --all pass/quick/moves.rs
-          # python x.py test --all pass/quick/mut-borrows.rs
-          # python x.py test --all pass/quick/shared-borrows.rs
-          # python x.py test --all pass/quick/trait-contracts-refinement.rs
-          # python x.py test --all pass/quick/fibonacci.rs
-          # python x.py test --all pass/pure-fn/len-lookup.rs
-          # python x.py test --all pass/pure-fn/quantifiers.rs
-          # python x.py test --all pass/pure-fn/recursive-pure-fn.rs
-          # python x.py test --all pass/pure-fn/ref-mut-arg.rs
-          # python x.py test --all pass/rosetta/Ackermann_function.rs
-          # python x.py test --all pass/rosetta/Heapsort.rs
-      - name: Run with purification.
-        env:
-          PRUSTI_VIPER_BACKEND: silicon
-          PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: silicon
-          PRUSTI_VERIFY_CORE_PROOF: true
-          PRUSTI_VERIFY_SPECIFICATIONS: true
-          PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: false
-          PRUSTI_INLINE_CALLER_FOR: false
-        run: |
-          python x.py test core_proof
-      - name: Run with purification with Carbon.
-        env:
-          PRUSTI_VIPER_BACKEND: silicon
-          PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: carbon
-          PRUSTI_VERIFY_CORE_PROOF: true
-          PRUSTI_VERIFY_SPECIFICATIONS: true
-          PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: false
-          PRUSTI_INLINE_CALLER_FOR: false
-        run: |
-          python x.py test core_proof
-      - name: Run without purification.
-        env:
-          PRUSTI_VIPER_BACKEND: silicon
-          PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: silicon
-          PRUSTI_VERIFY_CORE_PROOF: true
-          PRUSTI_VERIFY_SPECIFICATIONS: true
-          PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: true
-          PRUSTI_INLINE_CALLER_FOR: false
-        run: |
-          python x.py test core_proof
-      - name: Inline caller for functions
-        env:
-          PRUSTI_VIPER_BACKEND: silicon
-          PRUSTI_VERIFY_SPECIFICATIONS_BACKEND: silicon
-          PRUSTI_VERIFY_CORE_PROOF: true
-          PRUSTI_VERIFY_SPECIFICATIONS: true
-          PRUSTI_VERIFY_SPECIFICATIONS_WITH_CORE_PROOF: false
-          PRUSTI_INLINE_CALLER_FOR: true
-        run: |
-          python x.py test core_proof
+  #quick-tests:
+  #  runs-on: ubuntu-latest
+  #  env:
+  #    PRUSTI_CACHE_PATH: ${{ github.workspace }}/prusti_cache.bin
+  #  steps:
+  #    - name: Check out the repo
+  #      uses: actions/checkout@v2
+  #    - name: Set up Java
+  #      uses: actions/setup-java@v1
+  #      with:
+  #        java-version: '15'
+  #    - name: Set up the environment
+  #      run: python x.py setup
+  #    - name: Cache cargo
+  #      uses: Swatinem/rust-cache@v2
+  #      with:
+  #        shared-key: "shared"
+  #    - name: Build with cargo
+  #      run: python x.py build --all
+  #    - name: Run quick tests
+  #      run: python x.py test --all quick
 
   # Run all the tests.
   all-tests:
-    needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests]
+    needs: [fmt-check, clippy-check, check-deps, smir-check] # , quick-tests]
     strategy:
       matrix:
-        os: [ubuntu-latest, windows-latest, macos-latest]
+        os: [ubuntu-latest] # , windows-latest, macos-latest]
       fail-fast: false
     runs-on: ${{ matrix.os }}
     env:
@@ -247,83 +151,50 @@ jobs:
       - name: Build with cargo
         run: python x.py build --all
       - name: Run cargo tests
-        run: python x.py test --all
-      - name: Run a subset of tests with Carbon
-        run: |
-            python x.py test pass/no-annotation --all --verbose
-        env:
-          PRUSTI_VIPER_BACKEND: carbon
+        run: python x.py test -p prusti-tests
+        #run: python x.py test --all
       - name: Check prusti-contracts
         run: |
           cd prusti-contracts/prusti-contracts-test/
           cargo +stable build
 
-  # Run Prusti on itself.
-  # Disabled because of a bug when compiling jni-gen
-  test-on-prusti:
-    needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests]
-    runs-on: ubuntu-latest
-    if: false
-    steps:
-      - name: Check out the repo
-        uses: actions/checkout@v2
-      - name: Set up Java
-        uses: actions/setup-java@v1
-        with:
-          java-version: '15'
-      - name: Set up the environment
-        run: python x.py setup
-      - name: Cache cargo
-        uses: Swatinem/rust-cache@v2
-        with:
-          shared-key: "shared"
-      - name: Build with cargo
-        run: python x.py build --release --all
-      - name: Run cargo-prusti on Prusti
-        run: python x.py exec target/release/cargo-prusti
-        env:
-          PRUSTI_SKIP_UNSUPPORTED_FEATURES: true
-          PRUSTI_FULL_COMPILATION: true
-          PRUSTI_CHECK_PANICS: false
-          PRUSTI_CHECK_OVERFLOWS: false
-          PRUSTI_INTERNAL_ERRORS_AS_WARNINGS: true
-
   # Test cargo-prusti on a collection of crates.
-  test-crates:
-    needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests]
-    runs-on: ubuntu-22.04
-    strategy:
-      matrix:
-        shard_index: [0, 1, 2, 3]
-    steps:
-      - name: Check out the repo
-        uses: actions/checkout@v2
-      - name: Setup Python 3
-        uses: actions/setup-python@v2
-        with:
-          python-version: '3.x'
-      - name: Set up Java
-        uses: actions/setup-java@v1
-        with:
-          java-version: '15'
-      - name: Set up the environment
-        run: python x.py setup
-      - name: Cache cargo
-        uses: Swatinem/rust-cache@v2
-        with:
-          shared-key: "shared"
-      - name: Build with cargo --release
-        run: |
-          python x.py build --release -p prusti
-          python x.py build --release -p prusti-launch
-          python x.py build --release -p test-crates
-      - name: Test Prusti on a collection of crates
-        run: ./target/release/test-crates --fail-fast --num-shards=4 --shard-index=${{ matrix.shard_index }}
+  #test-crates:
+  #  needs: [fmt-check, clippy-check, check-deps, smir-check, quick-tests]
+  #  runs-on: ubuntu-22.04
+  #  if: false # disabled for v2 for now
+  #  strategy:
+  #    matrix:
+  #      shard_index: [0, 1, 2, 3]
+  #  steps:
+  #    - name: Check out the repo
+  #      uses: actions/checkout@v2
+  #    - name: Setup Python 3
+  #      uses: actions/setup-python@v2
+  #      with:
+  #        python-version: '3.x'
+  #    - name: Set up Java
+  #      uses: actions/setup-java@v1
+  #      with:
+  #        java-version: '15'
+  #    - name: Set up the environment
+  #      run: python x.py setup
+  #    - name: Cache cargo
+  #      uses: Swatinem/rust-cache@v2
+  #      with:
+  #        shared-key: "shared"
+  #    - name: Build with cargo --release
+  #      run: |
+  #        python x.py build --release -p prusti
+  #        python x.py build --release -p prusti-launch
+  #        python x.py build --release -p test-crates
+  #    - name: Test Prusti on a collection of crates
+  #      run: ./target/release/test-crates --fail-fast --num-shards=4 --shard-index=${{ matrix.shard_index }}
 
   # Dummy job to specify the jobs that must pass before merging on master
   can-merge:
     runs-on: ubuntu-latest
-    needs: [all-tests, purification-tests, test-crates]
+    needs: [all-tests] #, test-crates]
     # Always run, even if the workflow was cancelled
     if: ${{ always() }}
     steps:
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		# hashes of reformat commits
		7353a97cb8211e480ee7e740c7f0b7aa74f334ba