diff --git a/.github/workflows/coverage.yaml b/.github/workflows/coverage.yaml index 9b549598846..6eca4c58201 100644 --- a/.github/workflows/coverage.yaml +++ b/.github/workflows/coverage.yaml @@ -5,7 +5,7 @@ on: pull_request: branches: [ develop ] env: - cvc5-version: "1.1.2" + cvc5-version: "1.2.0" linux-vcpus: 4 windows-vcpus: 4 @@ -36,9 +36,9 @@ jobs: run: z3 --version - name: Download cvc-5 from the releases page and make sure it can be deployed run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5 - rm cvc5-Linux-static.zip + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 + rm cvc5-Linux-x86_64-static.zip cvc5 --version - name: Prepare ccache uses: actions/cache@v4 diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 8ab4a9e7e86..8704d6bc78f 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -5,7 +5,7 @@ on: pull_request: branches: [ develop ] env: - cvc5-version: "1.1.2" + cvc5-version: "1.2.0" linux-vcpus: 4 windows-vcpus: 4 @@ -29,9 +29,9 @@ jobs: run: z3 --version - name: Download cvc-5 from the releases page and make sure it can be deployed run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5 - rm cvc5-Linux-static.zip + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 + rm cvc5-Linux-x86_64-static.zip cvc5 --version - name: Prepare ccache uses: actions/cache@v4 @@ -115,9 +115,9 @@ jobs: run: z3 --version - name: Download cvc-5 from the releases page and make sure it can be deployed run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5 - rm cvc5-Linux-static.zip + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 + rm cvc5-Linux-x86_64-static.zip cvc5 --version - name: Prepare ccache uses: actions/cache@v4 @@ -225,9 +225,9 @@ jobs: run: z3 --version - name: Download cvc-5 from the releases page and make sure it can be deployed run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5 - rm cvc5-Linux-static.zip + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 + rm cvc5-Linux-x86_64-static.zip cvc5 --version - name: Prepare ccache uses: actions/cache@v4 @@ -297,9 +297,9 @@ jobs: run: z3 --version - name: Download cvc-5 from the releases page and make sure it can be deployed run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5 - rm cvc5-Linux-static.zip + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 + rm cvc5-Linux-x86_64-static.zip cvc5 --version - name: Prepare ccache uses: actions/cache@v4 @@ -363,9 +363,9 @@ jobs: run: z3 --version - name: Download cvc-5 from the releases page and make sure it can be deployed run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5 - rm cvc5-Linux-static.zip + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 + rm cvc5-Linux-x86_64-static.zip cvc5 --version - name: Prepare ccache uses: actions/cache@v4 @@ -423,9 +423,9 @@ jobs: run: z3 --version - name: Download cvc-5 from the releases page and make sure it can be deployed run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5 - rm cvc5-Linux-static.zip + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 + rm cvc5-Linux-x86_64-static.zip cvc5 --version - name: Prepare ccache uses: actions/cache@v4 @@ -451,6 +451,60 @@ jobs: - name: Run tests run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}} + # This job takes approximately 17 to 41 minutes + check-ubuntu-24_04-arm-cmake-gcc: + runs-on: ubuntu-24.04-arm + steps: + - uses: actions/checkout@v4 + with: + submodules: recursive + - name: Fetch dependencies + env: + # This is needed in addition to -yq to prevent apt-get from asking for + # user input + DEBIAN_FRONTEND: noninteractive + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils dpkg-dev ccache doxygen graphviz z3 + - name: Confirm z3 solver is available and log the version installed + run: z3 --version + - name: Download cvc-5 from the releases page and make sure it can be deployed + run: | + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-arm64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-arm64-static.zip cvc5-Linux-arm64-static/bin/cvc5 + rm cvc5-Linux-arm64-static.zip + cvc5 --version + - name: Prepare ccache + uses: actions/cache@v4 + with: + save-always: true + path: .ccache + key: ${{ runner.os }}-24.04-Arm-Release-${{ github.ref }}-${{ github.sha }}-PR + restore-keys: | + ${{ runner.os }}-24.04-Arm-Release-${{ github.ref }} + ${{ runner.os }}-24.04-Arm-Release + - name: ccache environment + run: | + echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV + echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV + - name: Configure using CMake + run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" + - name: Check that doc task works + run: ninja -C build doc + - name: Zero ccache stats and limit in size + run: ccache -z --max-size=500M + - name: Build with Ninja + run: ninja -C build -j${{env.linux-vcpus}} + - name: Print ccache stats + run: ccache -s + - name: Check if package building works + run: | + cd build + ninja package + ls *.deb + - name: Run tests + run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}} + # This job takes approximately 14 to 60 minutes check-ubuntu-22_04-cmake-gcc-32bit: runs-on: ubuntu-22.04 @@ -470,9 +524,9 @@ jobs: run: z3 --version - name: Download cvc-5 from the releases page and make sure it can be deployed run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5 - rm cvc5-Linux-static.zip + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 + rm cvc5-Linux-x86_64-static.zip cvc5 --version - name: Prepare ccache uses: actions/cache@v4 @@ -600,9 +654,9 @@ jobs: run: z3 --version - name: Download cvc5 binary and make sure it can be deployed run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS-static.zip - unzip -j -d /usr/local/bin cvc5-macOS-static.zip cvc5-macOS-static/bin/cvc5 - rm cvc5-macOS-static.zip + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-macOS-x86_64-static.zip cvc5-macOS-x86_64-static/bin/cvc5 + rm cvc5-macOS-x86_64-static.zip cvc5 --version - name: Prepare ccache uses: actions/cache@v4 @@ -652,9 +706,9 @@ jobs: run: z3 --version - name: Download cvc5 binary and make sure it can be deployed run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS-static.zip - unzip -j -d /usr/local/bin cvc5-macOS-static.zip cvc5-macOS-static/bin/cvc5 - rm cvc5-macOS-static.zip + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-macOS-arm64-static.zip + unzip -j -d /usr/local/bin cvc5-macOS-arm64-static.zip cvc5-macOS-arm64-static/bin/cvc5 + rm cvc5-macOS-arm64-static.zip cvc5 --version - name: Prepare ccache uses: actions/cache@v4 @@ -708,9 +762,9 @@ jobs: Expand-Archive -LiteralPath '.\z3.Zip' -DestinationPath C:\tools echo "c:\tools\z3-4.8.10-x64-win\bin;" >> $env:GITHUB_PATH New-Item -ItemType directory "C:\tools\cvc5" - Invoke-WebRequest -Uri https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Win64-static.zip -OutFile .\cvc5-Win64-static.zip - Expand-Archive -LiteralPath '.\cvc5-Win64-static.Zip' - Move-Item -Path .\cvc5-Win64-static\cvc5-Win64-static\bin\cvc5.exe c:\tools\cvc5\cvc5.exe + Invoke-WebRequest -Uri https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Win64-x86_64-static.zip -OutFile .\cvc5-Win64-x86_64-static.zip + Expand-Archive -LiteralPath '.\cvc5-Win64-x86_64-static.Zip' + Move-Item -Path .\cvc5-Win64-x86_64-static\cvc5-Win64-x86_64-static\bin\cvc5.exe c:\tools\cvc5\cvc5.exe echo "c:\tools\cvc5;" >> $env:GITHUB_PATH - name: Confirm z3 solver is available and log the version installed run: z3 --version @@ -771,9 +825,9 @@ jobs: Expand-Archive -LiteralPath '.\z3.Zip' -DestinationPath C:\tools echo "c:\tools\z3-4.8.10-x64-win\bin;" >> $env:GITHUB_PATH New-Item -ItemType directory "C:\tools\cvc5" - Invoke-WebRequest -Uri https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Win64-static.zip -OutFile .\cvc5-Win64-static.zip - Expand-Archive -LiteralPath '.\cvc5-Win64-static.Zip' - Move-Item -Path .\cvc5-Win64-static\cvc5-Win64-static\bin\cvc5.exe c:\tools\cvc5\cvc5.exe + Invoke-WebRequest -Uri https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Win64-x86_64-static.zip -OutFile .\cvc5-Win64-x86_64-static.zip + Expand-Archive -LiteralPath '.\cvc5-Win64-x86_64-static.Zip' + Move-Item -Path .\cvc5-Win64-x86_64-static\cvc5-Win64-x86_64-static\bin\cvc5.exe c:\tools\cvc5\cvc5.exe echo "c:\tools\cvc5;" >> $env:GITHUB_PATH New-Item -ItemType directory "C:\tools\parallel" wget.exe -O c:\tools\parallel\parallel https://git.savannah.gnu.org/cgit/parallel.git/plain/src/parallel diff --git a/.github/workflows/release-packages.yaml b/.github/workflows/release-packages.yaml index 0e7fab7e1b3..e9687f766b1 100644 --- a/.github/workflows/release-packages.yaml +++ b/.github/workflows/release-packages.yaml @@ -2,7 +2,7 @@ on: release: types: [created] env: - cvc5-version: "1.1.2" + cvc5-version: "1.2.0" name: Upload additional release assets jobs: @@ -22,9 +22,9 @@ jobs: run: z3 --version - name: Download cvc-5 from the releases page and make sure it can be deployed run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5 - rm cvc5-Linux-static.zip + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 + rm cvc5-Linux-x86_64-static.zip cvc5 --version - name: Prepare ccache uses: actions/cache@v4 @@ -77,6 +77,77 @@ jobs: SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }} SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 24.04 package built and uploaded successfully' || 'Ubuntu 24.04 package build failed' }}" + ubuntu-24_04-arm-package: + runs-on: ubuntu-24.04-arm + env: + GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }} + steps: + - uses: actions/checkout@v4 + with: + submodules: recursive + - name: Fetch dependencies + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -y g++ gdb flex bison cmake ninja-build maven jq libxml2-utils dpkg-dev ccache z3 + - name: Confirm z3 solver is available and log the version installed + run: z3 --version + - name: Download cvc-5 from the releases page and make sure it can be deployed + run: | + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-arm64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-arm64-static.zip cvc5-Linux-arm64-static/bin/cvc5 + rm cvc5-Linux-arm64-static.zip + cvc5 --version + - name: Prepare ccache + uses: actions/cache@v4 + with: + save-always: true + path: .ccache + key: ${{ runner.os }}-24.04-Arm-Release-${{ github.ref }}-${{ github.sha }}-RELEASEPKG + restore-keys: + ${{ runner.os }}-24.04-Arm-Release-${{ github.ref }} + ${{ runner.os }}-24.04-Arm-Release + - name: ccache environment + run: | + echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV + echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV + - name: Configure CMake + run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" + - name: Zero ccache stats and limit in size + run: ccache -z --max-size=500M + - name: Build using Ninja + run: ninja -C build -j4 + - name: Print ccache stats + run: ccache -s + - name: Run CTest + run: cd build; ctest . -V -L CORE -C Release -j4 + - name: Create packages + id: create_packages + run: | + cd build + ninja package + deb_package_name="$(ls *.deb)" + echo "deb_package=./build/$deb_package_name" >> $GITHUB_OUTPUT + echo "deb_package_name=ubuntu-24.04-arm64-$deb_package_name" >> $GITHUB_OUTPUT + - name: Get release info + id: get_release_info + uses: bruceadams/get-release@v1.3.2 + - name: Upload binary packages + uses: actions/upload-release-asset@v1 + with: + upload_url: ${{ steps.get_release_info.outputs.upload_url }} + asset_path: ${{ steps.create_packages.outputs.deb_package }} + asset_name: ${{ steps.create_packages.outputs.deb_package_name }} + asset_content_type: application/x-deb + - name: Slack notification of CI status + uses: rtCamp/action-slack-notify@v2 + if: success() || failure() + env: + SLACK_CHANNEL: aws-cbmc + SLACK_COLOR: ${{ job.status }} + SLACK_USERNAME: Github Actions CI bot + SLACK_WEBHOOK: ${{ secrets.SLACK_WEBHOOK }} + SLACK_MESSAGE: "${{ job.status == 'success' && 'Ubuntu 24.04 Arm package built and uploaded successfully' || 'Ubuntu 24.04 Arm package build failed' }}" + ubuntu-22_04-package: runs-on: ubuntu-22.04 env: @@ -93,9 +164,9 @@ jobs: run: z3 --version - name: Download cvc-5 from the releases page and make sure it can be deployed run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5 - rm cvc5-Linux-static.zip + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 + rm cvc5-Linux-x86_64-static.zip cvc5 --version - name: Prepare ccache uses: actions/cache@v4 @@ -164,9 +235,9 @@ jobs: run: z3 --version - name: Download cvc-5 from the releases page and make sure it can be deployed run: | - wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-static.zip - unzip -j -d /usr/local/bin cvc5-Linux-static.zip cvc5-Linux-static/bin/cvc5 - rm cvc5-Linux-static.zip + wget https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux-x86_64-static.zip + unzip -j -d /usr/local/bin cvc5-Linux-x86_64-static.zip cvc5-Linux-x86_64-static/bin/cvc5 + rm cvc5-Linux-x86_64-static.zip cvc5 --version - name: Prepare ccache uses: actions/cache@v4 diff --git a/regression/cbmc-concurrency/memory_barrier2/msvc.desc b/regression/cbmc-concurrency/memory_barrier2/msvc.desc index 9327f8de9a5..91f366f8aeb 100644 --- a/regression/cbmc-concurrency/memory_barrier2/msvc.desc +++ b/regression/cbmc-concurrency/memory_barrier2/msvc.desc @@ -1,5 +1,5 @@ CORE -msvc.c +msvc.i --mm tso --winx64 ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-concurrency/memory_barrier2/msvc.c b/regression/cbmc-concurrency/memory_barrier2/msvc.i similarity index 83% rename from regression/cbmc-concurrency/memory_barrier2/msvc.c rename to regression/cbmc-concurrency/memory_barrier2/msvc.i index b36e9a1be00..89ef92d50ed 100644 --- a/regression/cbmc-concurrency/memory_barrier2/msvc.c +++ b/regression/cbmc-concurrency/memory_barrier2/msvc.i @@ -1,3 +1,8 @@ +void __asm_mfence(void) +{ + __CPROVER_fence("WWfence", "RRfence", "RWfence", "WRfence"); +} + volatile int turn; int x; volatile int flag1 = 0, flag2 = 0; diff --git a/regression/cbmc-library/__asm_fstcw-01/msvc.desc b/regression/cbmc-library/__asm_fstcw-01/msvc.desc index 0275139a2df..780e6502916 100644 --- a/regression/cbmc-library/__asm_fstcw-01/msvc.desc +++ b/regression/cbmc-library/__asm_fstcw-01/msvc.desc @@ -1,5 +1,5 @@ CORE -msvc.c +msvc.i --pointer-check --bounds-check --winx64 ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc-library/__asm_fstcw-01/msvc.c b/regression/cbmc-library/__asm_fstcw-01/msvc.i similarity index 64% rename from regression/cbmc-library/__asm_fstcw-01/msvc.c rename to regression/cbmc-library/__asm_fstcw-01/msvc.i index 11c1cf19932..28f83895e82 100644 --- a/regression/cbmc-library/__asm_fstcw-01/msvc.c +++ b/regression/cbmc-library/__asm_fstcw-01/msvc.i @@ -1,9 +1,15 @@ +extern int __CPROVER_rounding_mode; + +void __asm_fstcw(void *dest) +{ + *(unsigned short *)dest = __CPROVER_rounding_mode << 10; +} + int main() { unsigned short cw; __asm { fstcw cw; } __CPROVER_assert((cw & 0xc00) == 0, "default rounding mode"); - // fesetround(FE_UPWARD); __CPROVER_rounding_mode = 2; __asm { fstcw cw; } __CPROVER_assert((cw & 0xc00) == 0x800, "round upwards"); diff --git a/regression/cbmc/Quantifiers-type2/main.c b/regression/cbmc/Quantifiers-type2/main.c index 73bd1913906..bdc3fd74cc9 100644 --- a/regression/cbmc/Quantifiers-type2/main.c +++ b/regression/cbmc/Quantifiers-type2/main.c @@ -5,7 +5,7 @@ int main() // clang-format off // clang-format would rewrite the "==>" as "== >" - __CPROVER_assume( __CPROVER_forall { char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } ); + __CPROVER_assume( __CPROVER_forall { signed char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } ); __CPROVER_assume( __CPROVER_forall { unsigned i; (i>=0 && i<2) ==> c[i]>=10 && c[i]<=10 } ); // clang-format on diff --git a/regression/cbmc/Quantifiers-type2/unsigned-char.c b/regression/cbmc/Quantifiers-type2/unsigned-char.c new file mode 100644 index 00000000000..186c763950b --- /dev/null +++ b/regression/cbmc/Quantifiers-type2/unsigned-char.c @@ -0,0 +1,16 @@ +int main() +{ + int b[2]; + int c[2]; + + // clang-format off + // clang-format would rewrite the "==>" as "== >" + __CPROVER_assume( __CPROVER_forall { unsigned char i; (i>=0 && i<2) ==> b[i]>=10 && b[i]<=10 } ); + __CPROVER_assume( __CPROVER_forall { unsigned i; (i>=0 && i<2) ==> c[i]>=10 && c[i]<=10 } ); + // clang-format on + + assert(b[0] == 10 && b[1] == 10); + assert(c[0] == 10 && c[1] == 10); + + return 0; +} diff --git a/regression/cbmc/Quantifiers-type2/unsigned-char.desc b/regression/cbmc/Quantifiers-type2/unsigned-char.desc new file mode 100644 index 00000000000..603f48f7a32 --- /dev/null +++ b/regression/cbmc/Quantifiers-type2/unsigned-char.desc @@ -0,0 +1,11 @@ +CORE no-new-smt +unsigned-char.c + +^\*\* Results:$ +^\[main.assertion.1\] line 12 assertion b\[.*0\] == 10 && b\[.*1\] == 10: SUCCESS$ +^\[main.assertion.2\] line 13 assertion c\[.*0\] == 10 && c\[.*1\] == 10: SUCCESS$ +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 915aa6b58d6..0f0e11c759a 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -286,6 +286,23 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type) code+="typedef signed __int128 __int128_t;\n" "typedef unsigned __int128 __uint128_t;\n"; } + + if( + config.ansi_c.arch == "arm64" && + config.ansi_c.os != configt::ansi_ct::ost::OS_MACOS) + { + code += "typedef struct __va_list {"; + code += "void *__stack;"; + code += "void *__gr_top;"; + code += "void *__vr_top;"; + code += "int __gr_offs;"; + code += "int __vr_offs;"; + code += " } __builtin_va_list;\n"; + } + else + { + code += "typedef void ** __builtin_va_list;\n"; + } } // this is Visual C/C++ only diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp index dea0fdc1b1d..fe67a0e6a29 100644 --- a/src/ansi-c/c_typecheck_expr.cpp +++ b/src/ansi-c/c_typecheck_expr.cpp @@ -541,12 +541,20 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr) typet arg_type=expr.type(); typecheck_type(arg_type); + const symbolt *symbol_ptr; + if(lookup("__builtin_va_list", symbol_ptr)) + { + error().source_location = expr.source_location(); + error() << "failed to find typedef name __builtin_va_list" << eom; + throw 0; + } + const code_typet new_type( - {code_typet::parametert(pointer_type(void_type()))}, std::move(arg_type)); + {code_typet::parametert(symbol_ptr->type)}, std::move(arg_type)); exprt arg = to_unary_expr(expr).op(); - implicit_typecast(arg, pointer_type(void_type())); + implicit_typecast(arg, new_type.parameters().front().type()); symbol_exprt function(ID_gcc_builtin_va_arg, new_type); function.add_source_location() = expr.source_location(); diff --git a/src/ansi-c/compiler_headers/gcc_builtin_headers_generic.h b/src/ansi-c/compiler_headers/gcc_builtin_headers_generic.h index 3039474ba81..84250411b6e 100644 --- a/src/ansi-c/compiler_headers/gcc_builtin_headers_generic.h +++ b/src/ansi-c/compiler_headers/gcc_builtin_headers_generic.h @@ -2,14 +2,14 @@ // stdarg void* __builtin_apply_args(); void* __builtin_apply(void (*)(), void*, __CPROVER_size_t); -void __builtin_ms_va_end(void *ap); -void __builtin_ms_va_start(void *ap, ...); +void __builtin_ms_va_end(__builtin_ms_va_list ap); +void __builtin_ms_va_start(__builtin_ms_va_list ap, ...); void* __builtin_next_arg(); int __builtin_va_arg_pack(); int __builtin_va_arg_pack_len(); void __builtin_va_copy(__builtin_va_list dest, __builtin_va_list src); -void __builtin_va_end(void *ap); -void __builtin_va_start(void *ap, ...); +void __builtin_va_end(__builtin_va_list ap); +void __builtin_va_start(__builtin_va_list ap, ...); // stdlib void __builtin__Exit(int); diff --git a/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h b/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h index 8920a952f1d..d9b61827aca 100644 --- a/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h +++ b/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h @@ -1,5 +1,4 @@ // clang-format off -typedef void ** __builtin_va_list; typedef void ** __builtin_ms_va_list; typedef int __gcc_m64 __attribute__ ((__vector_size__ (8), __may_alias__)); @@ -45,4 +44,13 @@ enum __gcc_atomic_memmodels { }; typedef unsigned char __tile __attribute__ ((__vector_size__ (1024))); + +// GCC and Clang use the following on ARM: +typedef float __Float32x4_t __attribute__ ((__vector_size__ (16))); +typedef double __Float64x2_t __attribute__ ((__vector_size__ (16))); +// The following ARM (scalable vector) extensions define vectors the size of +// which is not known at compile time. +typedef float *__SVFloat32_t; +typedef double *__SVFloat64_t; +typedef __CPROVER_bool *__SVBool_t; // clang-format on diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp index bf864fcdb1e..c6aadc337bd 100644 --- a/src/ansi-c/goto-conversion/builtin_functions.cpp +++ b/src/ansi-c/goto-conversion/builtin_functions.cpp @@ -593,8 +593,20 @@ void goto_convertt::do_array_op( copy(array_op_statement, OTHER, dest); } -exprt make_va_list(const exprt &expr) +static exprt make_va_list(const exprt &expr, const namespacet &ns) { + if( + auto struct_tag_type = type_try_dynamic_cast(expr.type())) + { + // aarch64 ABI mandates that va_list has struct type with member names as + // specified + const auto &components = ns.follow_tag(*struct_tag_type).components(); + DATA_INVARIANT( + components.size() == 5, + "va_list struct type expected to have 5 components"); + return member_exprt{expr, components.front()}; + } + exprt result = skip_typecast(expr); // if it's an address of an lvalue, we take that @@ -1296,14 +1308,15 @@ void goto_convertt::do_function_call_symbol( throw 0; } - exprt list_arg = make_va_list(arguments[0]); + exprt list_arg = make_va_list(arguments[0], ns); + const bool va_list_is_void_ptr = + list_arg.type().id() == ID_pointer && + to_pointer_type(list_arg.type()).base_type().id() == ID_empty; if(lhs.is_not_nil()) { exprt list_arg_cast = list_arg; - if( - list_arg.type().id() == ID_pointer && - to_pointer_type(list_arg.type()).base_type().id() == ID_empty) + if(va_list_is_void_ptr) { list_arg_cast = typecast_exprt{list_arg, pointer_type(pointer_type(empty_typet{}))}; @@ -1317,8 +1330,14 @@ void goto_convertt::do_function_call_symbol( goto_programt::make_assignment(lhs, rhs, function.source_location())); } - code_assignt assign{ - list_arg, plus_exprt{list_arg, from_integer(1, pointer_diff_type())}}; + exprt list_arg_ptr_arithmetic = typecast_exprt::conditional_cast( + plus_exprt{ + (va_list_is_void_ptr + ? typecast_exprt{list_arg, pointer_type(pointer_type(empty_typet{}))} + : list_arg), + from_integer(1, pointer_diff_type())}, + list_arg.type()); + code_assignt assign{list_arg, std::move(list_arg_ptr_arithmetic)}; assign.rhs().set( ID_C_va_arg_type, to_code_type(function.type()).return_type()); dest.add(goto_programt::make_assignment( @@ -1333,7 +1352,7 @@ void goto_convertt::do_function_call_symbol( throw 0; } - exprt dest_expr = make_va_list(arguments[0]); + exprt dest_expr = make_va_list(arguments[0], ns); const typecast_exprt src_expr(arguments[1], dest_expr.type()); if(!is_assignable(dest_expr)) @@ -1357,7 +1376,7 @@ void goto_convertt::do_function_call_symbol( throw 0; } - exprt dest_expr = make_va_list(arguments[0]); + exprt dest_expr = make_va_list(arguments[0], ns); if(!is_assignable(dest_expr)) { @@ -1392,7 +1411,7 @@ void goto_convertt::do_function_call_symbol( throw 0; } - exprt dest_expr = make_va_list(arguments[0]); + exprt dest_expr = make_va_list(arguments[0], ns); if(!is_assignable(dest_expr)) { diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp index 4c7992282e6..d8c862206a2 100644 --- a/src/cpp/cpp_internal_additions.cpp +++ b/src/cpp/cpp_internal_additions.cpp @@ -155,6 +155,23 @@ void cpp_internal_additions(std::ostream &out) out << "typedef signed __int128 __int128_t;" << '\n'; out << "typedef unsigned __int128 __uint128_t;" << '\n'; } + + if( + config.ansi_c.arch == "arm64" && + config.ansi_c.os != configt::ansi_ct::ost::OS_MACOS) + { + out << "typedef struct __va_list {"; + out << "void *__stack;"; + out << "void *__gr_top;"; + out << "void *__vr_top;"; + out << "int __gr_offs;"; + out << "int __vr_offs;"; + out << " } __builtin_va_list;" << '\n'; + } + else + { + out << "typedef void ** __builtin_va_list;" << '\n'; + } } // this is Visual C/C++ only diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp index 1eaa54a4dea..a0eb1b9dd89 100644 --- a/src/util/simplify_expr.cpp +++ b/src/util/simplify_expr.cpp @@ -975,6 +975,52 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr) else if(op_id==ID_ashr || op_id==ID_lshr || op_id==ID_shl) { } + else if(op_id == ID_zero_extend) + { + const exprt &zero_extended_op = to_zero_extend_expr(expr.op()); + if( + auto bv_type = + type_try_dynamic_cast(zero_extended_op.type())) + { + auto new_expr = expr; + if( + bv_type->id() == ID_signedbv && + bv_type->get_width() < to_bitvector_type(expr_type).get_width()) + { + new_expr.op() = + simplify_typecast( + typecast_exprt{ + zero_extended_op, unsignedbv_typet{bv_type->get_width()}}) + .expr; + } + else + new_expr.op() = zero_extended_op; + return changed(simplify_typecast(new_expr)); // rec. call + } + } + else if(op_id == ID_concatenation) + { + const auto &operands = expr.op().operands(); + if( + operands.size() == 2 && operands.front().is_constant() && + to_constant_expr(operands.front()).value_is_zero_string()) + { + auto new_expr = expr; + const bitvector_typet &bv_type = + to_bitvector_type(operands.back().type()); + if(bv_type.id() == ID_signedbv) + { + new_expr.op() = + simplify_typecast( + typecast_exprt{ + operands.back(), unsignedbv_typet{bv_type.get_width()}}) + .expr; + } + else + new_expr.op() = operands.back(); + return changed(simplify_typecast(new_expr)); // rec. call + } + } } }