diff --git a/.github/actions/benchexec-report/action.yml b/.github/actions/benchexec-report/action.yml index 2fc30c965c..ea031af136 100644 --- a/.github/actions/benchexec-report/action.yml +++ b/.github/actions/benchexec-report/action.yml @@ -48,7 +48,7 @@ runs: then printf "\n| $task | " >> $GITHUB_OUTPUT fi lasttask="$task" - printf " $emoji ($correct / $incorrect / $all) [HTML](https://theta.mit.bme.hu/benchmark-results/${{ github.head_ref }}/$i/$(ls *.html))/[CSV](https://theta.mit.bme.hu/benchmark-results/${{ github.head_ref }}/$i/$(ls *.csv)) | " >> $GITHUB_OUTPUT + printf " $emoji ($correct / $incorrect / $all) [HTML](https://theta.mit.bme.hu/benchmark-results/${{ github.ref }}/$i/$(ls *.html))/[CSV](https://theta.mit.bme.hu/benchmark-results/${{ github.ref }}/$i/$(ls *.csv)) | " >> $GITHUB_OUTPUT popd else rm -rf $i @@ -68,7 +68,7 @@ runs: with: branch: gh-pages folder: artifacts - target-folder: benchmark-results/${{ github.head_ref }}/ + target-folder: benchmark-results/${{ github.ref }}/ single-commit: true - name: Comment on PR if: github.event_name == 'pull_request' diff --git a/.github/actions/benchexec-test/action.yml b/.github/actions/benchexec-test/action.yml index d0f198ec4c..8444c92201 100644 --- a/.github/actions/benchexec-test/action.yml +++ b/.github/actions/benchexec-test/action.yml @@ -49,23 +49,21 @@ runs: run: | unzip release/Theta.zip sed -i 's/ --input \$1/ --portfolio ${{ inputs.portfolio }} --input \$1/g' Theta/theta-start.sh - - name: Cut setfile if too long - id: setfile - shell: bash - run: | - cd sv-benchmarks/c - for i in $(sed 's/#.*$//g' ${{ inputs.task }}.set); do find . -wholename ./$i; done | while read line; do grep "${line#./}" $GITHUB_ACTION_PATH/unsupported.txt >/dev/null 2>/dev/null || test -z $(yq e '.properties.[] | select(.property_file == "../properties/unreach-call.prp")' $line) >/dev/null 2>/dev/null || echo $(echo $line | sha1sum | awk ' { print $1 } ') $line ; done | sort -k1 | awk ' { $1=""; print $0 } ' | awk '{$1=$1};1' > all-files.txt - head -n${{ inputs.test_number }} all-files.txt > ${{ inputs.task }}.set - echo "length=$(cat ${{ inputs.task }}.set | wc -l)" >> "$GITHUB_OUTPUT" - cat ${{ inputs.task }}.set +# - name: Cut setfile if too long +# id: setfile +# shell: bash +# run: | +# cd sv-benchmarks/c +# for i in $(sed 's/#.*$//g' ${{ inputs.task }}.set); do find . -wholename ./$i; done | while read line; do grep "${line#./}" $GITHUB_ACTION_PATH/unsupported.txt >/dev/null 2>/dev/null || test -z $(yq e '.properties.[] | select(.property_file == "../properties/unreach-call.prp")' $line) >/dev/null 2>/dev/null || echo $(echo $line | sha1sum | awk ' { print $1 } ') $line ; done | sort -k1 | awk ' { $1=""; print $0 } ' | awk '{$1=$1};1' > all-files.txt +# head -n${{ inputs.test_number }} all-files.txt > ${{ inputs.task }}.set +# echo "length=$(cat ${{ inputs.task }}.set | wc -l)" >> "$GITHUB_OUTPUT" +# cat ${{ inputs.task }}.set - name: Run benchexec shell: bash - if: steps.setfile.outputs.length != '0' run: | - benchexec xml/theta.xml -n 2 --no-container --tool-directory Theta -t ${{ inputs.task }} + timeout 300 benchexec xml/theta.xml -n 2 --no-container --tool-directory Theta -t ${{ inputs.task }} || true - name: Upload results uses: actions/upload-artifact@0b7f8abb1508181956e8e162db84b466c27e18ce # v3.1.2 - if: steps.setfile.outputs.length != '0' with: name: BenchexecResults-${{ inputs.task }}-${{ inputs.portfolio }} path: results diff --git a/.github/actions/benchexec-test/theta.xml b/.github/actions/benchexec-test/theta.xml index 2ce7d4bc50..e2a7455cee 100644 --- a/.github/actions/benchexec-test/theta.xml +++ b/.github/actions/benchexec-test/theta.xml @@ -11,90 +11,90 @@ - - ../sv-benchmarks/c/ReachSafety-Arrays.set + + ../sv-benchmarks/c/Arrays.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-BitVectors.set + + ../sv-benchmarks/c/BitVectors.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-ControlFlow.set + + ../sv-benchmarks/c/ControlFlow.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-ECA.set + + ../sv-benchmarks/c/ECA.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-Floats.set + + ../sv-benchmarks/c/Floats.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-Heap.set + + ../sv-benchmarks/c/Heap.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-Loops.set + + ../sv-benchmarks/c/Loops.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-ProductLines.set + + ../sv-benchmarks/c/ProductLines.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-Recursive.set + + ../sv-benchmarks/c/Recursive.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-Sequentialized.set + + ../sv-benchmarks/c/Sequentialized.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-XCSP.set + + ../sv-benchmarks/c/XCSP.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-Combinations.set + + ../sv-benchmarks/c/Combinations.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-Hardware.set + + ../sv-benchmarks/c/Hardware.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-Hardness.set + + ../sv-benchmarks/c/Hardness.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ReachSafety-Fuzzle.set + + ../sv-benchmarks/c/Fuzzle.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/ConcurrencySafety-Main.set + + ../sv-benchmarks/c/Concurrency.set ../sv-benchmarks/c/properties/unreach-call.prp - - ../sv-benchmarks/c/NoDataRace-Main.set + + ../sv-benchmarks/c/Concurrency.set ../sv-benchmarks/c/properties/no-data-race.prp - ../sv-benchmarks/c/ConcurrencySafety-NoOverflows.set + ../sv-benchmarks/c/Concurrency.set ../sv-benchmarks/c/properties/no-overflow.prp - ../sv-benchmarks/c/ConcurrencySafety-MemSafety.set + ../sv-benchmarks/c/ConcurrencySafety.set ../sv-benchmarks/c/properties/valid-memsafety.prp diff --git a/.github/actions/cache-build/action.yml b/.github/actions/cache-build/action.yml index 277be1eb47..b1c7d0945d 100644 --- a/.github/actions/cache-build/action.yml +++ b/.github/actions/cache-build/action.yml @@ -6,13 +6,10 @@ inputs: runs: using: "composite" steps: -# - uses: actions/cache@88522ab9f39a2ea568f7027eddc7d8d8bc9d59c8 -# if: runner.os == 'Linux' -# id: cache -# with: -# path: . -# key: ${{ runner.os }}-${{github.sha}} - + - name: fetch + shell: bash + run: | + git fetch origin - name: build gradle uses: gradle/gradle-build-action@40b6781dcdec2762ad36556682ac74e31030cfe2 # v2.5.1 with: diff --git a/.github/actions/check-formatting/action.yml b/.github/actions/check-formatting/action.yml index 89ad28ffd8..72cf9f45cb 100644 --- a/.github/actions/check-formatting/action.yml +++ b/.github/actions/check-formatting/action.yml @@ -6,8 +6,6 @@ runs: - name: Checkout code uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3 - name: Check for formatting - uses: leventeBajczi/intellij-idea-format@v1.0 + uses: ./.github/actions/cache-build with: - settings-file: "./.idea/codeStyles/Project.xml" - file-mask: "*.java,*.kt" - additional-options: "-dry" \ No newline at end of file + arguments: spotlessCheck \ No newline at end of file diff --git a/.github/workflows/check-copyright.yml b/.github/workflows/check-copyright.yml index c441a8d667..7eb1f23215 100644 --- a/.github/workflows/check-copyright.yml +++ b/.github/workflows/check-copyright.yml @@ -7,7 +7,7 @@ on: permissions: write-all concurrency: - group: copyright-${{ github.head_ref }} + group: copyright-${{ github.ref }} cancel-in-progress: true jobs: @@ -17,4 +17,21 @@ jobs: - name: Checkout repository uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3 - name: Check copyright - uses: ./.github/actions/check-copyright \ No newline at end of file + uses: ./.github/actions/check-copyright + - name: Comment + if: failure() && github.event_name == 'pull_request' + uses: thollander/actions-comment-pull-request@dadb7667129e23f12ca3925c90dc5cd7121ab57e + continue-on-error: true # if we are in a fork, this will fail, but we don't care (tables will be missing) + with: + comment_tag: 'copyright' + mode: 'recreate' + message: | + :exclamation: Please run `./gradlew spotlessApply` on your branch to fix copyright headers. + + - name: Delete Comment + if: github.event_name == 'pull_request' + uses: thollander/actions-comment-pull-request@dadb7667129e23f12ca3925c90dc5cd7121ab57e + continue-on-error: true # if we are in a fork, this will fail, but we don't care (tables will be missing) + with: + comment_tag: 'copyright' + mode: 'delete' \ No newline at end of file diff --git a/.github/workflows/check-formatting.yml b/.github/workflows/check-formatting.yml index 213bdcb52d..02647f3a04 100644 --- a/.github/workflows/check-formatting.yml +++ b/.github/workflows/check-formatting.yml @@ -7,7 +7,7 @@ on: permissions: write-all concurrency: - group: formatting-${{ github.head_ref }} + group: formatting-${{ github.ref }} cancel-in-progress: true jobs: @@ -16,5 +16,27 @@ jobs: steps: - name: Checkout repository uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3 + - name: Setup java 17 + uses: actions/setup-java@5ffc13f4174014e2d4d4572b3d74c3fa61aeb2c2 # v3.11.0 + with: + distribution: temurin + java-version: 17 - name: Checking formatting - uses: ./.github/actions/check-formatting \ No newline at end of file + uses: ./.github/actions/check-formatting + - name: Comment + if: failure() && github.event_name == 'pull_request' + uses: thollander/actions-comment-pull-request@dadb7667129e23f12ca3925c90dc5cd7121ab57e + continue-on-error: true # if we are in a fork, this will fail, but we don't care (tables will be missing) + with: + comment_tag: 'reformat' + mode: 'recreate' + message: | + :exclamation: Please run `./gradlew spotlessApply` on your branch to fix formatting. + + - name: Delete Comment + if: github.event_name == 'pull_request' + uses: thollander/actions-comment-pull-request@dadb7667129e23f12ca3925c90dc5cd7121ab57e + continue-on-error: true # if we are in a fork, this will fail, but we don't care (tables will be missing) + with: + comment_tag: 'reformat' + mode: 'delete' \ No newline at end of file diff --git a/.github/workflows/check-version.yml b/.github/workflows/check-version.yml index 343ed50f53..83cbf94600 100644 --- a/.github/workflows/check-version.yml +++ b/.github/workflows/check-version.yml @@ -4,7 +4,7 @@ on: types: [opened, synchronize, reopened] concurrency: - group: version-${{ github.head_ref }} + group: version-${{ github.ref }} cancel-in-progress: true jobs: @@ -35,4 +35,21 @@ jobs: if: ${{ steps.new_version.outputs.version == steps.master_version.outputs.version }} run: | echo "New version ${{ steps.new_version.outputs.version }} is NOT OK" - exit 1 \ No newline at end of file + exit 1 + - name: Comment + if: failure() && github.event_name == 'pull_request' + uses: thollander/actions-comment-pull-request@dadb7667129e23f12ca3925c90dc5cd7121ab57e + continue-on-error: true # if we are in a fork, this will fail, but we don't care (tables will be missing) + with: + comment_tag: 'version' + mode: 'recreate' + message: | + :exclamation: Please modify `build.gradle.kts` to contain a later version than ${{ steps.master_version.outputs.version }}. Current version is ${{ steps.new_version.outputs.version }}. + + - name: Delete Comment + if: github.event_name == 'pull_request' + uses: thollander/actions-comment-pull-request@dadb7667129e23f12ca3925c90dc5cd7121ab57e + continue-on-error: true # if we are in a fork, this will fail, but we don't care (tables will be missing) + with: + comment_tag: 'version' + mode: 'delete' \ No newline at end of file diff --git a/.github/workflows/linux-build-test-deploy.yml b/.github/workflows/linux-build-test-deploy.yml index c670c7f497..4c101aca95 100644 --- a/.github/workflows/linux-build-test-deploy.yml +++ b/.github/workflows/linux-build-test-deploy.yml @@ -13,7 +13,7 @@ on: permissions: write-all concurrency: - group: deploy-${{ github.head_ref }}-${{ github.event_name }} + group: deploy-${{ github.ref }}-${{ github.event_name }} cancel-in-progress: true jobs: @@ -49,7 +49,24 @@ jobs: test-benchexec: strategy: matrix: - task: [ReachSafety-Arrays, ReachSafety-BitVectors, ReachSafety-ControlFlow, ReachSafety-ECA, ReachSafety-Floats, ReachSafety-Heap, ReachSafety-Loops, ReachSafety-ProductLines, ReachSafety-Recursive, ReachSafety-Sequentialized, ReachSafety-XCSP, ReachSafety-Combinations, ReachSafety-Hardware, ConcurrencySafety-Main, NoDataRace-Main, ConcurrencySafety-NoOverflows, ConcurrencySafety-MemSafety] + task: + - Arrays + - BitVectors + - ControlFlow + - ECA + - Floats + - Heap + - Loops + - ProductLines + - Recursive + - Sequentialized + - XCSP + - Combinations + - Hardware + - Concurrency + - NoDataRace + - ConcurrencySafety-NoOverflows + - ConcurrencySafety-MemSafety portfolio: [CEGAR, BOUNDED, HORN] runs-on: ubuntu-latest needs: create-archives @@ -88,6 +105,11 @@ jobs: with: name: "EmergenTheta" inputflag: "--algorithm EMERGENT" + - name: Create thorn.zip + uses: ./.github/actions/build-archive + with: + name: "Thorn" + inputflag: "--algorithm HORN" javadoc: diff --git a/.github/workflows/mac-build-test.yml b/.github/workflows/mac-build-test.yml index 4a0f2183b0..71994579a5 100644 --- a/.github/workflows/mac-build-test.yml +++ b/.github/workflows/mac-build-test.yml @@ -7,7 +7,7 @@ on: permissions: write-all concurrency: - group: mac-${{ github.head_ref }} + group: mac-${{ github.ref }} cancel-in-progress: true jobs: diff --git a/.github/workflows/reapply_copyright.yml b/.github/workflows/reapply_copyright.yml deleted file mode 100644 index 3acc9e3876..0000000000 --- a/.github/workflows/reapply_copyright.yml +++ /dev/null @@ -1,77 +0,0 @@ -name: Reapply Copyright - -on: - workflow_dispatch: - inputs: - file_mask: - description: 'File mask to reapply license header (argument to find)' - required: true - default: '-name "*.java" -o -name "*.kt" -o -name "*.kts"' - direct-commit: - type: boolean - default: false - description: Commit directly to source (instead of opening a PR) - -jobs: - copyright_checker: - runs-on: ubuntu-latest - steps: - - uses: tibdex/github-app-token@b62528385c34dbc9f38e5f4225ac829252d1ea92 - id: generate-token - with: - app_id: ${{ secrets.APP_ID }} - private_key: ${{ secrets.APP_PRIVATE_KEY }} - - - name: Checkout repository - uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3 - with: - token: ${{ steps.generate-token.outputs.token }} - - - name: Run Copyright Checker - shell: bash {0} - run: | - set +x - - for file in $(find . -type f \( ${{ inputs.file_mask }} \)); do - last_modified_year=$(git log -1 --format=%ad --date=format:%Y "$file") - echo "Checking file $file, last modified $last_modified_year" - - header_exists=$(head -n 2 "$file" | tail -n 1 | grep -c "Budapest University of Technology") - - echo "Header exists for $file: $header_exists" - - if [[ $header_exists -eq 0 ]]; then - echo "Adding copyright header to $file" - cat ./doc/copyright-header.txt "$file" > tmp_026204264 - mv tmp_026204264 "$file" - fi - - header_year=$(head -n 2 "$file" | tail -n 1 | grep -o -E '[0-9]{4}') - - echo "Header year for $file: $header_year" - - if [[ "$header_year" != "$last_modified_year" ]]; then - echo "Updating copyright year to $last_modified_year in $file (was $header_year)" - sed -i "s/Copyright [0-9]\{4\}/Copyright $last_modified_year/g" "$file" - fi - done - - - name: Create Pull Request - if: ${{ !inputs.direct-commit }} - uses: peter-evans/create-pull-request@153407881ec5c347639a548ade7d8ad1d6740e38 - with: - commit-message: "Reapplied copyright" - branch: "copyright-reapply" - title: '[AutoPR] Reaplied copyright' - token: ${{ steps.generate-token.outputs.token }} - committer: ThetaBotMaintainer[bot] <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> - author: ThetaBotMaintainer[bot] <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> - - - name: Commit changes - if: ${{ inputs.direct-commit }} - uses: stefanzweifel/git-auto-commit-action@3ea6ae190baf489ba007f7c92608f33ce20ef04a - with: - commit_message: "Reapplied copyright" - commit_user_name: ThetaBotMaintainer[bot] - commit_user_email: 139346997+ThetaBotMaintainer[bot]@users.noreply.github.com - commit_author: ThetaBotMaintainer[bot] <139346997+ThetaBotMaintainer[bot]@users.noreply.github.com> \ No newline at end of file diff --git a/.github/workflows/reformat-code.yml b/.github/workflows/reformat-code.yml index fe6fc24d9f..29411d1f37 100644 --- a/.github/workflows/reformat-code.yml +++ b/.github/workflows/reformat-code.yml @@ -3,10 +3,6 @@ name: Reformat code on: workflow_dispatch: inputs: - file_mask: - description: 'File mask to reformat' - required: true - default: '*.java,*.kts,*.kt' direct-commit: type: boolean default: false @@ -28,10 +24,9 @@ jobs: token: ${{ steps.generate-token.outputs.token }} - name: Do reformat - uses: leventeBajczi/intellij-idea-format@v1.0 + uses: ./.github/actions/cache-build with: - settings-file: "./.idea/codeStyles/Project.xml" - file-mask: ${{ inputs.file_mask }} + arguments: spotlessApply - name: Create Pull Request if: ${{ !inputs.direct-commit }} diff --git a/.github/workflows/sonar.yml b/.github/workflows/sonar.yml index c291bdc97c..c66a14c329 100644 --- a/.github/workflows/sonar.yml +++ b/.github/workflows/sonar.yml @@ -8,7 +8,7 @@ on: permissions: read-all concurrency: - group: sonar-${{ github.head_ref }} + group: sonar-${{ github.ref }} cancel-in-progress: true jobs: diff --git a/.github/workflows/win-build-test.yml b/.github/workflows/win-build-test.yml index 1288984285..7fc33a46f5 100644 --- a/.github/workflows/win-build-test.yml +++ b/.github/workflows/win-build-test.yml @@ -7,7 +7,7 @@ on: permissions: write-all concurrency: - group: win-${{ github.head_ref }} + group: win-${{ github.ref }} cancel-in-progress: true jobs: diff --git a/README.md b/README.md index 80e602f755..7044ff4049 100644 --- a/README.md +++ b/README.md @@ -20,7 +20,7 @@ [![Check formatting](https://github.com/ftsrg/theta/actions/workflows/check-formatting.yml/badge.svg)](https://github.com/ftsrg/theta/actions/workflows/check-formatting.yml) [![Apache 2.0 License](https://img.shields.io/badge/license-Apache--2-brightgreen.svg?style=flat)](https://www.apache.org/licenses/LICENSE-2.0) -![Theta logo](https://raw.githubusercontent.com/ftsrg/theta/master/doc/theta-logo.png) +Theta logo ## About diff --git a/build.gradle.kts b/build.gradle.kts index 41d6b5e9e2..b76fd9f7ff 100644 --- a/build.gradle.kts +++ b/build.gradle.kts @@ -13,6 +13,7 @@ * See the License for the specific language governing permissions and * limitations under the License. */ + plugins { base id("jacoco-common") @@ -28,7 +29,7 @@ buildscript { allprojects { group = "hu.bme.mit.theta" - version = "6.5.3" + version = "6.6.3" apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts")) } diff --git a/buildSrc/build.gradle.kts b/buildSrc/build.gradle.kts index 093b423f12..7b1e3380f6 100644 --- a/buildSrc/build.gradle.kts +++ b/buildSrc/build.gradle.kts @@ -30,6 +30,7 @@ apply(from = rootDir.resolve("../gradle/shared-with-buildSrc/mirrors.gradle.kts" val kotlinVersion: String by project val shadowVersion: String by project +val spotlessVersion: String by project // https://github.com/gradle/kotlin-dsl/issues/430#issuecomment-414768887 fun gradlePlugin(id: String, version: String): String = "$id:$id.gradle.plugin:$version" @@ -38,6 +39,7 @@ dependencies { compileOnly(gradleKotlinDsl()) implementation(kotlin("gradle-plugin", kotlinVersion)) implementation(gradlePlugin("com.github.johnrengelman.shadow", shadowVersion)) + implementation(gradlePlugin("com.diffplug.spotless", spotlessVersion)) } // Force the embeddable Kotlin compiler version to be the selected kotlinVersion. @@ -103,4 +105,4 @@ tasks { named("compileKotlin", KotlinCompile::class) { dependsOn(generateVersions) } -} +} \ No newline at end of file diff --git a/buildSrc/gradle.properties b/buildSrc/gradle.properties index e9c71bc25e..77da25281b 100644 --- a/buildSrc/gradle.properties +++ b/buildSrc/gradle.properties @@ -39,4 +39,5 @@ deltaCollectionsVersion=0.0.1 gsonVersion=2.9.1 javasmtVersion=4.1.1 sosylabVersion=0.3000-569-g89796f98 -cliktVersion=4.4.0 \ No newline at end of file +cliktVersion=4.4.0 +spotlessVersion=6.25.0 \ No newline at end of file diff --git a/buildSrc/src/main/kotlin/java-common.gradle.kts b/buildSrc/src/main/kotlin/java-common.gradle.kts index 96ffbd8ec6..838b4d4f41 100644 --- a/buildSrc/src/main/kotlin/java-common.gradle.kts +++ b/buildSrc/src/main/kotlin/java-common.gradle.kts @@ -17,6 +17,7 @@ plugins { java id("jacoco-common") id("maven-artifact") + id("com.diffplug.spotless") } dependencies { @@ -65,3 +66,46 @@ tasks { jvmArgs("-Xss5m", "-Xms512m", "-Xmx1g") } } + +spotless { + ratchetFrom("origin/master") + + isEnforceCheck = false + + val year = "\$YEAR" // you can't escape $ in raw strings.. + val licenseHeader = """ /* + * Copyright $year Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */""".trimIndent() + + + java { + importOrder("java|javax", "hu.bme.", "") + removeUnusedImports() + googleJavaFormat("1.24.0").aosp().reflowLongStrings() + formatAnnotations() + + licenseHeader(licenseHeader) + } + kotlin { + ktfmt("0.51").googleStyle() + + licenseHeader(licenseHeader) + } + kotlinGradle { + target("*.gradle.kts") // default target for kotlinGradle + + ktlint() + } +} \ No newline at end of file diff --git a/doc/theta-logo.svg b/doc/theta-logo.svg new file mode 100644 index 0000000000..8705b0a3b4 --- /dev/null +++ b/doc/theta-logo.svg @@ -0,0 +1,50 @@ + + + + + + + + + + + diff --git a/subprojects/frontends/c-frontend/src/main/antlr/C.g4 b/subprojects/frontends/c-frontend/src/main/antlr/C.g4 index af6b7ccd1c..386d294c42 100644 --- a/subprojects/frontends/c-frontend/src/main/antlr/C.g4 +++ b/subprojects/frontends/c-frontend/src/main/antlr/C.g4 @@ -173,7 +173,7 @@ logicalOrExpression ; conditionalExpression - : logicalOrExpression ('?' expression ':' conditionalExpression)? + : logicalOrExpression ('?' ifTrue=expression ':' ifFalse=expression)? ; assignmentExpression diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/UnsupportedFrontendElementException.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/UnsupportedFrontendElementException.java new file mode 100644 index 0000000000..e3bef460e0 --- /dev/null +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/UnsupportedFrontendElementException.java @@ -0,0 +1,23 @@ +/* + * Copyright 2024 Budapest University of Technology and Economics + * + * Licensed under the Apache License, Version 2.0 (the "License"); + * you may not use this file except in compliance with the License. + * You may obtain a copy of the License at + * + * http://www.apache.org/licenses/LICENSE-2.0 + * + * Unless required by applicable law or agreed to in writing, software + * distributed under the License is distributed on an "AS IS" BASIS, + * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + * See the License for the specific language governing permissions and + * limitations under the License. + */ + +package hu.bme.mit.theta.frontend; + +public class UnsupportedFrontendElementException extends RuntimeException { + public UnsupportedFrontendElementException(String message) { + super(message); + } +} diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java index 60a7ff7609..609518ea3e 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/ExpressionVisitor.java @@ -18,13 +18,7 @@ import hu.bme.mit.theta.c.frontend.dsl.gen.CBaseVisitor; import hu.bme.mit.theta.c.frontend.dsl.gen.CParser; -import hu.bme.mit.theta.c.frontend.dsl.gen.CParser.PostfixExpressionAccessContext; -import hu.bme.mit.theta.c.frontend.dsl.gen.CParser.PostfixExpressionBracesContext; -import hu.bme.mit.theta.c.frontend.dsl.gen.CParser.PostfixExpressionBracketsContext; -import hu.bme.mit.theta.c.frontend.dsl.gen.CParser.PostfixExpressionDecrementContext; -import hu.bme.mit.theta.c.frontend.dsl.gen.CParser.PostfixExpressionIncrementContext; -import hu.bme.mit.theta.c.frontend.dsl.gen.CParser.PostfixExpressionMemberAccessContext; -import hu.bme.mit.theta.c.frontend.dsl.gen.CParser.PostfixExpressionPtrMemberAccessContext; +import hu.bme.mit.theta.c.frontend.dsl.gen.CParser.*; import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.Logger.Level; @@ -35,23 +29,16 @@ import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs; import hu.bme.mit.theta.core.type.abstracttype.DivExpr; import hu.bme.mit.theta.core.type.abstracttype.ModExpr; -import hu.bme.mit.theta.core.type.anytype.Dereference; -import hu.bme.mit.theta.core.type.anytype.Exprs; -import hu.bme.mit.theta.core.type.anytype.IteExpr; -import hu.bme.mit.theta.core.type.anytype.RefExpr; -import hu.bme.mit.theta.core.type.anytype.Reference; +import hu.bme.mit.theta.core.type.anytype.*; import hu.bme.mit.theta.core.type.booltype.BoolExprs; import hu.bme.mit.theta.core.type.booltype.BoolType; -import hu.bme.mit.theta.core.type.bvtype.BvAndExpr; -import hu.bme.mit.theta.core.type.bvtype.BvExprs; -import hu.bme.mit.theta.core.type.bvtype.BvOrExpr; -import hu.bme.mit.theta.core.type.bvtype.BvType; -import hu.bme.mit.theta.core.type.bvtype.BvXorExpr; +import hu.bme.mit.theta.core.type.bvtype.*; import hu.bme.mit.theta.core.type.fptype.FpLitExpr; import hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.core.utils.BvUtils; import hu.bme.mit.theta.core.utils.FpUtils; import hu.bme.mit.theta.frontend.ParseContext; +import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException; import hu.bme.mit.theta.frontend.transformation.ArchitectureConfig; import hu.bme.mit.theta.frontend.transformation.grammar.function.FunctionVisitor; import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.TypedefVisitor; @@ -59,7 +46,6 @@ import hu.bme.mit.theta.frontend.transformation.model.declaration.CDeclaration; import hu.bme.mit.theta.frontend.transformation.model.statements.CAssignment; import hu.bme.mit.theta.frontend.transformation.model.statements.CCall; -import hu.bme.mit.theta.frontend.transformation.model.statements.CCompound; import hu.bme.mit.theta.frontend.transformation.model.statements.CExpr; import hu.bme.mit.theta.frontend.transformation.model.statements.CStatement; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType; @@ -70,23 +56,14 @@ import org.kframework.mpfr.BinaryMathContext; import java.math.BigInteger; -import java.util.ArrayList; -import java.util.Deque; -import java.util.List; -import java.util.Map; -import java.util.Optional; +import java.util.*; import java.util.function.Function; import java.util.stream.Collectors; import static com.google.common.base.Preconditions.checkState; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Add; import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Div; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Geq; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Ite; import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Mod; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Neq; -import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Sub; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.*; import static hu.bme.mit.theta.core.type.anytype.Exprs.Reference; import static hu.bme.mit.theta.core.type.fptype.FpExprs.FpType; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; @@ -136,38 +113,6 @@ public List getPreStatements() { return preStatements; } - @Override - public Expr visitConditionalExpression(CParser.ConditionalExpressionContext ctx) { - if (ctx.expression() != null) { - CStatement ifTrue = ctx.expression().accept(functionVisitor); - addPreStatements(ifTrue); - if (ifTrue instanceof CAssignment) { - preStatements.add(ifTrue); - } - Expr expr = ctx.logicalOrExpression().accept(this); - Expr lhs = ifTrue.getExpression(); - Expr rhs = ctx.conditionalExpression().accept(this); - CComplexType smallestCommonType = CComplexType.getSmallestCommonType(List.of(CComplexType.getType(lhs, parseContext), CComplexType.getType(rhs, parseContext)), parseContext); - IteExpr ite = Ite( - AbstractExprs.Neq(CComplexType.getType(expr, parseContext).getNullValue(), expr), - smallestCommonType.castTo(lhs), - smallestCommonType.castTo(rhs) - ); - parseContext.getMetadata().create(ite, "cType", smallestCommonType); - return ite; - } else return ctx.logicalOrExpression().accept(this); - } - - private void addPreStatements(CStatement ifTrue) { - if (ifTrue instanceof CCompound) { - if (ifTrue.getPreStatements() != null) preStatements.add(ifTrue.getPreStatements()); - if (ifTrue.getPostStatements() != null) postStatements.add(ifTrue.getPostStatements()); - for (CStatement cStatement : ((CCompound) ifTrue).getcStatementList()) { - addPreStatements(cStatement); - } - } - } - @Override public Expr visitLogicalOrExpression(CParser.LogicalOrExpressionContext ctx) { if (ctx.logicalAndExpression().size() > 1) { @@ -310,7 +255,7 @@ public Expr visitRelationalExpression(CParser.RelationalExpressionContext ctx guard = AbstractExprs.Geq(leftExpr, rightExpr); break; default: - throw new IllegalStateException("Unexpected value: " + ctx.signs.get(i).getText()); + throw new UnsupportedFrontendElementException("Unexpected relational expression sign: " + ctx.signs.get(i).getText()); } // MaxEnumAnalyzer.instance.consume(guard); TODO: handle circular dependency CComplexType signedInt = CComplexType.getSignedInt(parseContext); @@ -415,7 +360,7 @@ public Expr visitMultiplicativeExpression(CParser.MultiplicativeExpressionCon } break; default: - throw new IllegalStateException("Unexpected value: " + ctx.signs.get(i).getText()); + throw new UnsupportedFrontendElementException("Unexpected multiplicative expression sign: " + ctx.signs.get(i).getText()); } parseContext.getMetadata().create(expr, "cType", smallestCommonType); expr = smallestCommonType.castTo(expr); @@ -665,9 +610,9 @@ public Expr visitPrimaryExpressionConstant(CParser.PrimaryExpressionConstantC BigFloat bigFloat; if (text.startsWith("0x")) { - throw new UnsupportedOperationException("Hexadecimal FP constants are not yet supported!"); + throw new UnsupportedFrontendElementException("Hexadecimal FP constants are not yet supported!"); } else if (text.startsWith("0b")) { - throw new UnsupportedOperationException("Binary FP constants are not yet supported!"); + throw new UnsupportedFrontendElementException("Binary FP constants are not yet supported!"); } else { bigFloat = new BigFloat(text, new BinaryMathContext(significand - 1, exponent)); } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/UnsupportedInitializer.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/UnsupportedInitializer.java index 121f0a9bba..b11b230c07 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/UnsupportedInitializer.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/expression/UnsupportedInitializer.java @@ -20,6 +20,7 @@ import hu.bme.mit.theta.core.type.LitExpr; import hu.bme.mit.theta.core.type.NullaryExpr; import hu.bme.mit.theta.core.type.inttype.IntType; +import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException; import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; @@ -32,7 +33,7 @@ public IntType getType() { @Override public LitExpr eval(Valuation val) { - throw new UnsupportedOperationException("UnsupportedInitializer expressions are not supported."); + throw new UnsupportedFrontendElementException("UnsupportedInitializer expressions are not supported."); } @Override diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java index eb98d8d707..4f9041fa08 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/function/FunctionVisitor.java @@ -26,7 +26,9 @@ import hu.bme.mit.theta.core.stmt.AssumeStmt; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs; import hu.bme.mit.theta.core.type.anytype.Exprs; +import hu.bme.mit.theta.core.type.anytype.IteExpr; import hu.bme.mit.theta.core.type.arraytype.ArrayType; import hu.bme.mit.theta.core.type.booltype.BoolType; import hu.bme.mit.theta.frontend.ParseContext; @@ -40,26 +42,7 @@ import hu.bme.mit.theta.frontend.transformation.grammar.type.DeclarationVisitor; import hu.bme.mit.theta.frontend.transformation.grammar.type.TypeVisitor; import hu.bme.mit.theta.frontend.transformation.model.declaration.CDeclaration; -import hu.bme.mit.theta.frontend.transformation.model.statements.CAssignment; -import hu.bme.mit.theta.frontend.transformation.model.statements.CAssume; -import hu.bme.mit.theta.frontend.transformation.model.statements.CBreak; -import hu.bme.mit.theta.frontend.transformation.model.statements.CCase; -import hu.bme.mit.theta.frontend.transformation.model.statements.CCompound; -import hu.bme.mit.theta.frontend.transformation.model.statements.CContinue; -import hu.bme.mit.theta.frontend.transformation.model.statements.CDecls; -import hu.bme.mit.theta.frontend.transformation.model.statements.CDefault; -import hu.bme.mit.theta.frontend.transformation.model.statements.CDoWhile; -import hu.bme.mit.theta.frontend.transformation.model.statements.CExpr; -import hu.bme.mit.theta.frontend.transformation.model.statements.CFor; -import hu.bme.mit.theta.frontend.transformation.model.statements.CFunction; -import hu.bme.mit.theta.frontend.transformation.model.statements.CGoto; -import hu.bme.mit.theta.frontend.transformation.model.statements.CIf; -import hu.bme.mit.theta.frontend.transformation.model.statements.CInitializerList; -import hu.bme.mit.theta.frontend.transformation.model.statements.CProgram; -import hu.bme.mit.theta.frontend.transformation.model.statements.CRet; -import hu.bme.mit.theta.frontend.transformation.model.statements.CStatement; -import hu.bme.mit.theta.frontend.transformation.model.statements.CSwitch; -import hu.bme.mit.theta.frontend.transformation.model.statements.CWhile; +import hu.bme.mit.theta.frontend.transformation.model.statements.*; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CVoid; import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleType; @@ -67,20 +50,13 @@ import org.antlr.v4.runtime.ParserRuleContext; import org.antlr.v4.runtime.Token; -import java.util.ArrayDeque; -import java.util.ArrayList; -import java.util.Deque; -import java.util.Iterator; -import java.util.LinkedHashMap; -import java.util.List; -import java.util.Map; -import java.util.Optional; -import java.util.Set; -import java.util.StringJoiner; +import java.util.*; +import java.util.stream.Stream; import static com.google.common.base.Preconditions.checkState; import static hu.bme.mit.theta.core.decl.Decls.Var; import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Add; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Ite; import static hu.bme.mit.theta.core.utils.TypeUtils.cast; import static hu.bme.mit.theta.grammar.UtilsKt.textWithWS; @@ -456,14 +432,19 @@ public CStatement visitBodyDeclaration(CParser.BodyDeclarationContext ctx) { createVars(declaration); if (declaration.getType() instanceof Struct) { checkState(declaration.getInitExpr() instanceof CInitializerList, "Struct can only be initialized via an initializer list!"); + final var initializerList = (CInitializerList) declaration.getInitExpr(); List> varDecls = declaration.getVarDecls(); - for (int i = 0; i < varDecls.size(); i++) { - VarDecl varDecl = varDecls.get(i); - Tuple2, CStatement> initializer = ((CInitializerList) declaration.getInitExpr()).getStatements().get(i); - - CAssignment cAssignment = new CAssignment(varDecl.getRef(), initializer.get2(), "=", parseContext); + VarDecl varDecl = varDecls.get(0); + final var ptrType = CComplexType.getUnsignedLong(parseContext); + LitExpr currentValue = ptrType.getNullValue(); + LitExpr unitValue = ptrType.getUnitValue(); + for (Tuple2, CStatement> statement : initializerList.getStatements()) { + final var expr = statement.get2().getExpression(); + final var deref = Exprs.Dereference(cast(varDecl.getRef(), currentValue.getType()), cast(currentValue, currentValue.getType()), expr.getType()); + CAssignment cAssignment = new CAssignment(deref, statement.get2(), "=", parseContext); recordMetadata(ctx, cAssignment); compound.getcStatementList().add(cAssignment); + currentValue = Add(currentValue, unitValue).eval(ImmutableValuation.empty()); } } else { checkState(declaration.getVarDecls().size() == 1, "non-struct declarations shall only have one variable!"); @@ -484,6 +465,18 @@ public CStatement visitBodyDeclaration(CParser.BodyDeclarationContext ctx) { CAssignment cAssignment = new CAssignment(declaration.getVarDecls().get(0).getRef(), declaration.getInitExpr(), "=", parseContext); recordMetadata(ctx, cAssignment); compound.getcStatementList().add(cAssignment); + if (declaration.getInitExpr() instanceof CCompound compoundInitExpr) { + final var preCompound = new CCompound(parseContext); + final var postCompound = new CCompound(parseContext); + final var preStatements = collectPreStatements(compoundInitExpr); + preCompound.getcStatementList().addAll(preStatements); + final var postStatements = collectPostStatements(compoundInitExpr); + postCompound.getcStatementList().addAll(postStatements); + resetPreStatements(compoundInitExpr); + resetPostStatements(compoundInitExpr); + compound.setPreStatements(preCompound); + compound.setPostStatements(postCompound); + } } } } else { @@ -528,7 +521,16 @@ public CStatement visitAssignmentExpressionAssignmentExpression(CParser.Assignme CCompound preStatements = new CCompound(parseContext); CCompound postStatements = new CCompound(parseContext); Expr ret = ctx.unaryExpression().accept(expressionVisitor); - CAssignment cAssignment = new CAssignment(ret, ctx.assignmentExpression().accept(this), ctx.assignmentOperator().getText(), parseContext); + CStatement rhs = ctx.assignmentExpression().accept(this); + if (rhs instanceof CCompound compoundInitExpr) { + final var preStatementList = collectPreStatements(compoundInitExpr); + preStatements.getcStatementList().addAll(preStatementList); + final var postStatementList = collectPostStatements(compoundInitExpr); + postStatements.getcStatementList().addAll(postStatementList); + resetPreStatements(compoundInitExpr); + resetPostStatements(compoundInitExpr); + } + CAssignment cAssignment = new CAssignment(ret, rhs, ctx.assignmentOperator().getText(), parseContext); compound.getcStatementList().add(cAssignment); preStatements.getcStatementList().addAll(expressionVisitor.getPreStatements()); compound.setPreStatements(preStatements); @@ -541,18 +543,146 @@ public CStatement visitAssignmentExpressionAssignmentExpression(CParser.Assignme @Override public CStatement visitAssignmentExpressionConditionalExpression(CParser.AssignmentExpressionConditionalExpressionContext ctx) { - ExpressionVisitor expressionVisitor = new ExpressionVisitor(parseContext, this, variables, functions, typedefVisitor, typeVisitor, uniqueWarningLogger); + return ctx.conditionalExpression().accept(this); + } + + private void resetPreStatements(CStatement statement) { + if (statement instanceof CCompound compound) { + compound.setPreStatements(null); + for (CStatement cStatement : compound.getcStatementList()) { + resetPreStatements(cStatement); + } + } + } + + private void resetPostStatements(CStatement statement) { + if (statement instanceof CCompound compound) { + compound.setPostStatements(null); + for (CStatement cStatement : compound.getcStatementList()) { + resetPostStatements(cStatement); + } + } + } + + private List getStatementList(CStatement statement) { + if (statement instanceof CCompound compound) { + return compound.getcStatementList().stream().flatMap(i -> getStatementList(i).stream()).toList(); + } else if (statement != null) { + return List.of(statement); + } else { + return List.of(); + } + } + + /* + This collects the following: + - the current compound's pre-statement + - all pre-statements of the pre-statement (before the pre-statement) + - all the pre-statement of every cStatement + */ + private List collectPreStatements(CStatement cStatement) { + if (cStatement instanceof CCompound) { + return Stream.concat( + Stream.concat( + collectPreStatements(cStatement.getPreStatements()).stream(), + getStatementList(cStatement.getPreStatements()).stream()), + ((CCompound) cStatement).getcStatementList().stream().flatMap(cStatement1 -> collectPreStatements(cStatement1).stream()) + ).filter(i -> !(i instanceof CExpr)).toList(); + } else return List.of(); + } + + /* + This collects the following: + - all the post-statements of every cStatement + - the current compound's post-statement + - all post-statements of the post-statement (after the post-statement) + */ + private List collectPostStatements(CStatement cStatement) { + if (cStatement instanceof CCompound) { + return Stream.concat( + ((CCompound) cStatement).getcStatementList().stream().flatMap(cStatement1 -> collectPostStatements(cStatement1).stream()), + Stream.concat( + getStatementList(cStatement.getPostStatements()).stream(), + collectPostStatements(cStatement.getPostStatements()).stream()) + ).filter(i -> !(i instanceof CExpr)).toList(); + } else return List.of(); + } + + // This is in the function visitor, not in the expression visitor, because + // cond ? f1() : f2() + // will only call either f1 or f2 (it can be used for branching) + @Override + public CStatement visitConditionalExpression(CParser.ConditionalExpressionContext ctx) { CCompound compound = new CCompound(parseContext); CCompound preStatements = new CCompound(parseContext); CCompound postStatements = new CCompound(parseContext); - Expr ret = ctx.conditionalExpression().accept(expressionVisitor); - CExpr cexpr = new CExpr(ret, parseContext); + + ExpressionVisitor expressionVisitor = new ExpressionVisitor(parseContext, this, variables, functions, typedefVisitor, typeVisitor, uniqueWarningLogger); + + Expr iteExpr; + if (!ctx.expression().isEmpty()) { + CStatement ifTrue = ctx.ifTrue.accept(this); + CStatement ifFalse = ctx.ifFalse.accept(this); + + Expr expr = ctx.logicalOrExpression().accept(expressionVisitor); + Expr lhs = ifTrue.getExpression(); + Expr rhs = ifFalse.getExpression(); + + CCompound guardCompound = new CCompound(parseContext); + guardCompound.getcStatementList().add(new CExpr(expr, parseContext)); + guardCompound.setPostStatements(new CCompound(parseContext)); + guardCompound.setPreStatements(new CCompound(parseContext)); + + + CCompound ifTruePre = new CCompound(parseContext); + List ifTruePreList = collectPreStatements(ifTrue); + ifTruePre.getcStatementList().addAll(ifTruePreList); + ifTruePre.setPostStatements(new CCompound(parseContext)); + ifTruePre.setPreStatements(new CCompound(parseContext)); + CCompound ifFalsePre = new CCompound(parseContext); + List ifFalsePreList = collectPreStatements(ifFalse); + ifFalsePre.getcStatementList().addAll(ifFalsePreList); + ifFalsePre.setPostStatements(new CCompound(parseContext)); + ifFalsePre.setPreStatements(new CCompound(parseContext)); + + CCompound ifTruePost = new CCompound(parseContext); + List ifTruePostList = collectPostStatements(ifTrue); + ifTruePost.getcStatementList().addAll(ifTruePostList); + ifTruePost.setPostStatements(new CCompound(parseContext)); + ifTruePost.setPreStatements(new CCompound(parseContext)); + CCompound ifFalsePost = new CCompound(parseContext); + List ifFalsePostList = collectPostStatements(ifFalse); + ifFalsePost.getcStatementList().addAll(ifFalsePostList); + ifFalsePost.setPostStatements(new CCompound(parseContext)); + ifFalsePost.setPreStatements(new CCompound(parseContext)); + + + if (!ifTruePreList.isEmpty() || !ifFalsePreList.isEmpty()) { + preStatements.getcStatementList().add(new CIf(guardCompound, ifTruePre, ifFalsePre, parseContext)); + } + if (!ifTruePostList.isEmpty() || !ifFalsePostList.isEmpty()) { + postStatements.getcStatementList().add(new CIf(guardCompound, ifTruePost, ifFalsePost, parseContext)); + } + + CComplexType smallestCommonType = CComplexType.getSmallestCommonType(List.of(CComplexType.getType(lhs, parseContext), CComplexType.getType(rhs, parseContext)), parseContext); + IteExpr ite = Ite( + AbstractExprs.Neq(CComplexType.getType(expr, parseContext).getNullValue(), expr), + smallestCommonType.castTo(lhs), + smallestCommonType.castTo(rhs) + ); + parseContext.getMetadata().create(ite, "cType", smallestCommonType); + iteExpr = ite; + } else { + iteExpr = ctx.logicalOrExpression().accept(expressionVisitor); + } + + CExpr cexpr = new CExpr(iteExpr, parseContext); compound.getcStatementList().add(cexpr); - preStatements.getcStatementList().addAll(expressionVisitor.getPreStatements()); + preStatements.getcStatementList().addAll(0, expressionVisitor.getPreStatements()); compound.setPreStatements(preStatements); recordMetadata(ctx, compound); - postStatements.getcStatementList().addAll(expressionVisitor.getPostStatements()); compound.setPostStatements(postStatements); + postStatements.getcStatementList().addAll(expressionVisitor.getPostStatements()); recordMetadata(ctx, compound); return compound; } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java index f752eb7ef8..84be79414d 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/DeclarationVisitor.java @@ -22,6 +22,7 @@ import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.frontend.ParseContext; +import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException; import hu.bme.mit.theta.frontend.transformation.grammar.expression.UnsupportedInitializer; import hu.bme.mit.theta.frontend.transformation.grammar.function.FunctionVisitor; import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.TypedefVisitor; @@ -140,7 +141,7 @@ public CDeclaration visitStructDeclaratorSimple(CParser.StructDeclaratorSimpleCo @Override public CDeclaration visitStructDeclaratorConstant(CParser.StructDeclaratorConstantContext ctx) { - throw new UnsupportedOperationException("Not yet supported!"); + throw new UnsupportedFrontendElementException("Not yet supported!"); } @Override @@ -191,17 +192,17 @@ public CDeclaration visitDirectDeclaratorArray1(CParser.DirectDeclaratorArray1Co @Override public CDeclaration visitDirectDeclaratorArray2(CParser.DirectDeclaratorArray2Context ctx) { - throw new UnsupportedOperationException("Not yet implemented!"); + throw new UnsupportedFrontendElementException("Not yet implemented!"); } @Override public CDeclaration visitDirectDeclaratorArray3(CParser.DirectDeclaratorArray3Context ctx) { - throw new UnsupportedOperationException("Not yet implemented!"); + throw new UnsupportedFrontendElementException("Not yet implemented!"); } @Override public CDeclaration visitDirectDeclaratorArray4(CParser.DirectDeclaratorArray4Context ctx) { - throw new UnsupportedOperationException("Not yet implemented!"); + throw new UnsupportedFrontendElementException("Not yet implemented!"); } @Override diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/TypeVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/TypeVisitor.java index 83acdef4b6..8fad36f961 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/TypeVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/grammar/type/TypeVisitor.java @@ -25,35 +25,19 @@ import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.frontend.ParseContext; +import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException; import hu.bme.mit.theta.frontend.transformation.grammar.preprocess.TypedefVisitor; import hu.bme.mit.theta.frontend.transformation.model.declaration.CDeclaration; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType; -import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleType; -import hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory; -import hu.bme.mit.theta.frontend.transformation.model.types.simple.DeclaredName; import hu.bme.mit.theta.frontend.transformation.model.types.simple.Enum; -import hu.bme.mit.theta.frontend.transformation.model.types.simple.NamedType; -import hu.bme.mit.theta.frontend.transformation.model.types.simple.Struct; +import hu.bme.mit.theta.frontend.transformation.model.types.simple.*; import org.antlr.v4.runtime.Token; import org.antlr.v4.runtime.tree.ParseTree; -import java.util.ArrayList; -import java.util.LinkedHashMap; -import java.util.List; -import java.util.Map; -import java.util.Optional; +import java.util.*; import java.util.stream.Collectors; -import static hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory.Atomic; -import static hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory.DeclaredName; -import static hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory.Enum; -import static hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory.Extern; -import static hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory.NamedType; -import static hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory.Signed; -import static hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory.ThreadLocal; -import static hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory.Typedef; -import static hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory.Unsigned; -import static hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory.Volatile; +import static hu.bme.mit.theta.frontend.transformation.model.types.simple.CSimpleTypeFactory.*; public class TypeVisitor extends CBaseVisitor { private final DeclarationVisitor declarationVisitor; @@ -211,15 +195,15 @@ public CSimpleType visitStorageClassSpecifier(CParser.StorageClassSpecifierConte case "auto": case "register": case "_Thread_local": - throw new UnsupportedOperationException("Not yet implemented"); + throw new UnsupportedFrontendElementException("Not yet implemented (" + ctx.getText() + ")"); } - throw new UnsupportedOperationException( + throw new UnsupportedFrontendElementException( "Storage class specifier not expected: " + ctx.getText()); } @Override public CSimpleType visitTypeSpecifierAtomic(CParser.TypeSpecifierAtomicContext ctx) { - throw new UnsupportedOperationException("Not yet implemented"); + throw new UnsupportedFrontendElementException("Not yet implemented"); } @Override @@ -229,7 +213,7 @@ public CSimpleType visitTypeSpecifierCompound(CParser.TypeSpecifierCompoundConte @Override public CSimpleType visitTypeSpecifierFunctionPointer(CParser.TypeSpecifierFunctionPointerContext ctx) { - throw new UnsupportedOperationException("Function pointers not yet implemented"); + throw new UnsupportedFrontendElementException("Function pointers not yet implemented"); } @Override @@ -245,13 +229,17 @@ public CSimpleType visitCompoundDefinition(CParser.CompoundDefinitionContext ctx CParser.SpecifierQualifierListContext specifierQualifierListContext = structDeclarationContext.specifierQualifierList(); CSimpleType cSimpleType = specifierQualifierListContext.accept(this); if (structDeclarationContext.structDeclaratorList() == null) { - struct.addField(cSimpleType.getAssociatedName(), cSimpleType); + final var decl = new CDeclaration(cSimpleType); + struct.addField(decl); } else { for (CParser.StructDeclaratorContext structDeclaratorContext : structDeclarationContext.structDeclaratorList() .structDeclarator()) { CDeclaration declaration = structDeclaratorContext.accept( declarationVisitor); - struct.addField(declaration.getName(), cSimpleType); + if (declaration.getType() == null) { + declaration.setType(cSimpleType); + } + struct.addField(declaration); } } } @@ -298,7 +286,7 @@ public CSimpleType visitEnumUsage(CParser.EnumUsageContext ctx) { @Override public CSimpleType visitTypeSpecifierExtension(CParser.TypeSpecifierExtensionContext ctx) { - throw new UnsupportedOperationException("Not yet implemented"); + throw new UnsupportedFrontendElementException("Not yet implemented typeSpecifierExtension"); } @Override @@ -361,7 +349,7 @@ public CSimpleType visitTypeSpecifierTypedefName(CParser.TypeSpecifierTypedefNam @Override public CSimpleType visitTypeSpecifierTypeof(CParser.TypeSpecifierTypeofContext ctx) { - throw new UnsupportedOperationException("Not yet implemented"); + throw new UnsupportedFrontendElementException("Not yet implemented typeSpecifierTypeof"); } @Override @@ -370,13 +358,13 @@ public CSimpleType visitTypeQualifier(CParser.TypeQualifierContext ctx) { case "const": return null; case "restrict": - throw new UnsupportedOperationException("Not yet implemented!"); + throw new UnsupportedFrontendElementException("Not yet implemented 'restrict'!"); case "volatile": return Volatile(); case "_Atomic": return Atomic(); } - throw new UnsupportedOperationException( + throw new UnsupportedFrontendElementException( "Type qualifier " + ctx.getText() + " not expected!"); } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/declaration/CDeclaration.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/declaration/CDeclaration.java index 7c8ce9b585..7242590d40 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/declaration/CDeclaration.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/declaration/CDeclaration.java @@ -25,6 +25,8 @@ import java.util.ArrayList; import java.util.List; +import static com.google.common.base.Preconditions.checkNotNull; + public class CDeclaration { private CSimpleType type; @@ -37,7 +39,7 @@ public class CDeclaration { private CStatement initExpr; public CDeclaration(CSimpleType cSimpleType) { - this.name = null; + this.name = checkNotNull(cSimpleType).getAssociatedName(); this.type = cSimpleType; this.derefCounter = cSimpleType.getPointerLevel(); this.varDecls = new ArrayList<>(); diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CAssignment.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CAssignment.java index 748b919252..8d285f2d04 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CAssignment.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CAssignment.java @@ -21,6 +21,7 @@ import hu.bme.mit.theta.core.type.bvtype.BvExprs; import hu.bme.mit.theta.core.type.bvtype.BvType; import hu.bme.mit.theta.frontend.ParseContext; +import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType; import java.util.List; @@ -99,7 +100,7 @@ public Expr getrExpression() { ret = BvExprs.Or(List.of((Expr) type.castTo(lValue), (Expr) type.castTo(rExpression))); break; default: - throw new RuntimeException("Bad operator: " + operator); + throw new UnsupportedFrontendElementException("Unsupported operator: " + operator); } parseContext.getMetadata().create(ret, "cType", CComplexType.getType(lValue, parseContext)); ret = CComplexType.getType(lValue, parseContext).castTo(ret); diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CInitializerList.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CInitializerList.java index 4d7670b096..d12151fe4b 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CInitializerList.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CInitializerList.java @@ -19,6 +19,7 @@ import hu.bme.mit.theta.common.Tuple2; import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.frontend.ParseContext; +import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType; import java.util.ArrayList; @@ -38,7 +39,7 @@ public CInitializerList(CComplexType type, ParseContext parseContext) { @Override public Expr getExpression() { - throw new UnsupportedOperationException("Cannot create expression of initializer list."); + throw new UnsupportedFrontendElementException("Cannot create expression of initializer list."); } @Override diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CStatement.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CStatement.java index 44f8087a79..93a2199239 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CStatement.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/statements/CStatement.java @@ -18,6 +18,7 @@ import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.frontend.ParseContext; +import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException; /** * Every Program, Function and Statement is a subclass of this base class. @@ -60,7 +61,7 @@ public void setId(String id) { * @return The expression associated with the statement. */ public Expr getExpression() { - throw new RuntimeException("Cannot get expression!"); + throw new UnsupportedFrontendElementException("Cannot get expression!"); } public CStatement getPostStatements() { @@ -68,7 +69,7 @@ public CStatement getPostStatements() { } public void setPostStatements(CStatement postStatements) { - throw new UnsupportedOperationException("Only CCompounds shall currently have pre- and post statements!"); + throw new UnsupportedFrontendElementException("Only CCompounds shall currently have pre- and post statements!"); } public CStatement getPreStatements() { @@ -76,7 +77,7 @@ public CStatement getPreStatements() { } public void setPreStatements(CStatement preStatements) { - throw new UnsupportedOperationException("Only CCompounds shall currently have pre- and post statements!"); + throw new UnsupportedFrontendElementException("Only CCompounds shall currently have pre- and post statements!"); } public abstract R accept(CStatementVisitor visitor, P param); diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java index 32b8c4b0e4..1f54441d28 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CComplexType.java @@ -26,11 +26,8 @@ import hu.bme.mit.theta.core.type.fptype.FpType; import hu.bme.mit.theta.core.type.inttype.IntType; import hu.bme.mit.theta.frontend.ParseContext; -import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CArray; -import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CCompound; -import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CFunction; -import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPointer; -import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CStruct; +import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException; +import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.*; import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.CInteger; import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.Fitsall; import hu.bme.mit.theta.frontend.transformation.model.types.complex.integer.c128.C128; @@ -62,12 +59,7 @@ import java.util.Map.Entry; import java.util.Optional; -import static hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.getCastVisitor; -import static hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.getLimitVisitor; -import static hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.getNullValueVisitor; -import static hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.getTypeVisitor; -import static hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.getUnitValueVisitor; -import static hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.getValueVisitor; +import static hu.bme.mit.theta.frontend.transformation.ArchitectureConfig.*; public abstract class CComplexType { private final CSimpleType origin; @@ -208,7 +200,7 @@ private static CComplexType getType(Type type, ParseContext parseContext) { if (longDoubleType.equals(type)) { return new CFloat(null, parseContext); } - throw new RuntimeException("No suitable size found for type: " + type); + throw new UnsupportedFrontendElementException("No suitable size found for type: " + type); } else if (type instanceof BvType) { for (Entry entry : parseContext.getArchitecture().standardTypeSizes.entrySet()) { String s = entry.getKey(); @@ -230,9 +222,9 @@ private static CComplexType getType(Type type, ParseContext parseContext) { } } } - throw new RuntimeException("No suitable width found for type: " + type); + throw new UnsupportedFrontendElementException("No suitable width found for type: " + type); } else { - throw new RuntimeException("Not yet implemented for type: " + type); + throw new UnsupportedFrontendElementException("Not yet implemented for type: " + type); } } @@ -307,7 +299,7 @@ public R accept(CComplexTypeVisitor visitor, T param) { public static class CComplexTypeVisitor { public R visit(CComplexType type, T param) { - throw new UnsupportedOperationException("Not (yet) implemented (" + type.getClass().getSimpleName() + " in " + this.getClass().getName() + ")"); + throw new UnsupportedFrontendElementException("Not (yet) implemented (" + type.getClass().getSimpleName() + " in " + this.getClass().getName() + ")"); } public R visit(CVoid type, T param) { diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CVoid.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CVoid.java index 4d9d121d1e..353ca2cc9a 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CVoid.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/CVoid.java @@ -29,6 +29,11 @@ public R accept(CComplexTypeVisitor visitor, T param) { return visitor.visit(this, param); } + @Override + public CComplexType getSmallestCommonType(CComplexType type) { + return type; + } + @Override public String getTypeName() { return "void"; diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/integer/Fitsall.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/integer/Fitsall.java index 6550e48040..8cb56130a7 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/integer/Fitsall.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/integer/Fitsall.java @@ -41,7 +41,7 @@ public String getTypeName() { @Override public CInteger getSignedVersion() { - throw new RuntimeException("Bool does not have a signed version!"); + throw new RuntimeException("Fitsall does not have a signed version!"); } @Override diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/visitors/bitvector/CastVisitor.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/visitors/bitvector/CastVisitor.java index ab2fd3faa7..6187ff3391 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/visitors/bitvector/CastVisitor.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/complex/visitors/bitvector/CastVisitor.java @@ -25,6 +25,7 @@ import hu.bme.mit.theta.core.type.fptype.FpRoundingMode; import hu.bme.mit.theta.core.type.fptype.FpType; import hu.bme.mit.theta.frontend.ParseContext; +import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CVoid; import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPointer; @@ -89,7 +90,7 @@ private Expr handleSignedConversion(CInteger type, Expr param } } } else { - throw new IllegalStateException("Compound types are not directly supported!"); + throw new UnsupportedFrontendElementException("Compound types are not directly supported!"); } } @@ -119,7 +120,7 @@ private Expr handleUnsignedConversion(CInteger type, Expr par } } } else { - throw new IllegalStateException("Compound types are not directly supported!"); + throw new UnsupportedFrontendElementException("Compound types are not directly supported!"); } } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/NamedType.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/NamedType.java index 2cbc83220d..2ff2c5fdb0 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/NamedType.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/NamedType.java @@ -19,6 +19,7 @@ import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.frontend.ParseContext; +import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CVoid; import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPointer; @@ -169,7 +170,7 @@ protected void patch(CSimpleType cSimpleType) { break; default: if (!cSimpleType.isTypedef()) { - throw new RuntimeException( + throw new UnsupportedFrontendElementException( "namedType should be short or long or type specifier, instead it is " + namedType); } diff --git a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/Struct.java b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/Struct.java index eb3d8ad12f..a7b55db04d 100644 --- a/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/Struct.java +++ b/subprojects/frontends/c-frontend/src/main/java/hu/bme/mit/theta/frontend/transformation/model/types/simple/Struct.java @@ -20,7 +20,9 @@ import hu.bme.mit.theta.common.logging.Logger; import hu.bme.mit.theta.common.logging.Logger.Level; import hu.bme.mit.theta.frontend.ParseContext; +import hu.bme.mit.theta.frontend.transformation.model.declaration.CDeclaration; import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType; +import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CPointer; import hu.bme.mit.theta.frontend.transformation.model.types.complex.compound.CStruct; import java.util.ArrayList; @@ -28,9 +30,11 @@ import java.util.List; import java.util.Map; +import static com.google.common.base.Preconditions.checkNotNull; + public class Struct extends NamedType { - private final Map fields; + private final Map fields; private final String name; private final Logger uniqueWarningLogger; @@ -52,8 +56,8 @@ public static Struct getByName(String name) { currentlyBeingBuilt = false; } - public void addField(String name, CSimpleType type) { - fields.put(name, type); + public void addField(CDeclaration decl) { + fields.put(checkNotNull(decl.getName()), checkNotNull(decl)); } @Override @@ -64,9 +68,16 @@ public CComplexType getActualType() { } currentlyBeingBuilt = true; List> actualFields = new ArrayList<>(); - fields.forEach((s, cSimpleType) -> actualFields.add(Tuple2.of(s, cSimpleType.getActualType()))); + fields.forEach((s, cDeclaration) -> actualFields.add(Tuple2.of(s, cDeclaration.getActualType()))); currentlyBeingBuilt = false; - return new CStruct(this, actualFields, parseContext); + + CComplexType type = new CStruct(this, actualFields, parseContext); + + for (int i = 0; i < getPointerLevel(); i++) { + type = new CPointer(this, type, parseContext); + } + + return type; } @Override diff --git a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt index 6dccaaa36c..d82a92fa4a 100644 --- a/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt +++ b/subprojects/xcfa/c2xcfa/src/main/java/hu/bme/mit/theta/c2xcfa/FrontendXcfaBuilder.kt @@ -94,7 +94,9 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo continue } if (type is CStruct) { - error("Not handling init expression of struct array ${globalDeclaration.get1()}") + uniqueWarningLogger.write( + Logger.Level.INFO, "Not handling init expression of struct array ${globalDeclaration.get1()}" + ) } builder.addVar(XcfaGlobalVar(globalDeclaration.get2(), type.nullValue)) if (type is CArray) { @@ -190,7 +192,7 @@ class FrontendXcfaBuilder(val parseContext: ParseContext, val checkOverflow: Boo for (flatVariable in flatVariables) { builder.addVar(flatVariable) val type = CComplexType.getType(flatVariable.ref, parseContext) - if (type is CArray && builder.getParams().none { it.first == flatVariable }) { + if ((type is CArray || type is CStruct) && builder.getParams().none { it.first == flatVariable }) { initStmtList.add(StmtLabel( Stmts.Assign(cast(flatVariable, flatVariable.type), cast(type.getValue("$ptrCnt"), flatVariable.type)) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt index f5257effa4..54e2c0d406 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/XcfaCli.kt @@ -41,6 +41,9 @@ class XcfaCli(private val args: Array) { @Parameter(names = ["--help", "-h"], help = true) private var help = false + @Parameter(names = ["--svcomp"]) + private var svcomp = false + @Parameter var remainingFlags: MutableList = ArrayList() @@ -55,6 +58,18 @@ class XcfaCli(private val args: Array) { } else { config = XcfaConfig() } + if (svcomp) { + remainingFlags.addAll( + listOf( + "--enable-output", + "--disable-xcfa-serialization", + "--disable-arg-generation", + "--disable-chc-serialization", + "--disable-c-serialization", + "--only-svcomp-witness" + ) + ) + } while (remainingFlags.isNotEmpty()) { val nextArgs = remainingFlags.toTypedArray() remainingFlags.clear() diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt index 563a7abaa3..1ecf5e665a 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt @@ -18,6 +18,7 @@ package hu.bme.mit.theta.xcfa.cli.params import com.microsoft.z3.Z3Exception import hu.bme.mit.theta.common.exception.NotSolvableException +import hu.bme.mit.theta.frontend.UnsupportedFrontendElementException import hu.bme.mit.theta.solver.UnknownSolverStatusException import hu.bme.mit.theta.solver.javasmt.JavaSMTSolverException import hu.bme.mit.theta.solver.smtlib.solver.SmtLibSolverException @@ -32,6 +33,7 @@ enum class ExitCodes(val code: Int) { SERVER_ERROR(202), PORTFOLIO_ERROR(203), + UNSUPPORTED_ELEMENT(209), FRONTEND_FAILED(210), INVALID_PARAM(211), @@ -59,6 +61,9 @@ fun exitOnError(stacktrace: Boolean, throwDontExit: Boolean, body: () -> T): } catch (e: ErrorCodeException) { e.printStackTrace() exitProcess(throwDontExit, e, e.code) + } catch (e: UnsupportedFrontendElementException) { + e.printCauseAndTrace(stacktrace) + exitProcess(throwDontExit, e, ExitCodes.UNSUPPORTED_ELEMENT.code) } catch (e: SmtLibSolverException) { e.printCauseAndTrace(stacktrace) exitProcess(throwDontExit, e, ExitCodes.SOLVER_ERROR.code)