Skip to content

Commit

Permalink
Merge branch 'master' into trace-generation
Browse files Browse the repository at this point in the history
  • Loading branch information
AdamZsofi committed Oct 26, 2024
2 parents aabe64e + 529352a commit 8cc79dc
Show file tree
Hide file tree
Showing 103 changed files with 6,190 additions and 4,471 deletions.
4 changes: 2 additions & 2 deletions .github/actions/benchexec-report/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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'
Expand Down
22 changes: 10 additions & 12 deletions .github/actions/benchexec-test/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
72 changes: 36 additions & 36 deletions .github/actions/benchexec-test/theta.xml
Original file line number Diff line number Diff line change
Expand Up @@ -11,90 +11,90 @@
<option name="--loglevel">INFO</option>

<rundefinition name="SV-COMP24_unreach-call">
<tasks name="ReachSafety-Arrays">
<includesfile>../sv-benchmarks/c/ReachSafety-Arrays.set</includesfile>
<tasks name="Arrays">
<includesfile>../sv-benchmarks/c/Arrays.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-BitVectors">
<includesfile>../sv-benchmarks/c/ReachSafety-BitVectors.set</includesfile>
<tasks name="BitVectors">
<includesfile>../sv-benchmarks/c/BitVectors.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-ControlFlow">
<includesfile>../sv-benchmarks/c/ReachSafety-ControlFlow.set</includesfile>
<tasks name="ControlFlow">
<includesfile>../sv-benchmarks/c/ControlFlow.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-ECA">
<includesfile>../sv-benchmarks/c/ReachSafety-ECA.set</includesfile>
<tasks name="ECA">
<includesfile>../sv-benchmarks/c/ECA.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-Floats">
<includesfile>../sv-benchmarks/c/ReachSafety-Floats.set</includesfile>
<tasks name="Floats">
<includesfile>../sv-benchmarks/c/Floats.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-Heap">
<includesfile>../sv-benchmarks/c/ReachSafety-Heap.set</includesfile>
<tasks name="Heap">
<includesfile>../sv-benchmarks/c/Heap.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-Loops">
<includesfile>../sv-benchmarks/c/ReachSafety-Loops.set</includesfile>
<tasks name="Loops">
<includesfile>../sv-benchmarks/c/Loops.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-ProductLines">
<includesfile>../sv-benchmarks/c/ReachSafety-ProductLines.set</includesfile>
<tasks name="ProductLines">
<includesfile>../sv-benchmarks/c/ProductLines.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-Recursive">
<includesfile>../sv-benchmarks/c/ReachSafety-Recursive.set</includesfile>
<tasks name="Recursive">
<includesfile>../sv-benchmarks/c/Recursive.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-Sequentialized">
<includesfile>../sv-benchmarks/c/ReachSafety-Sequentialized.set</includesfile>
<tasks name="Sequentialized">
<includesfile>../sv-benchmarks/c/Sequentialized.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-XCSP">
<includesfile>../sv-benchmarks/c/ReachSafety-XCSP.set</includesfile>
<tasks name="XCSP">
<includesfile>../sv-benchmarks/c/XCSP.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-Combinations">
<includesfile>../sv-benchmarks/c/ReachSafety-Combinations.set</includesfile>
<tasks name="Combinations">
<includesfile>../sv-benchmarks/c/Combinations.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-Hardware">
<includesfile>../sv-benchmarks/c/ReachSafety-Hardware.set</includesfile>
<tasks name="Hardware">
<includesfile>../sv-benchmarks/c/Hardware.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-Hardness">
<includesfile>../sv-benchmarks/c/ReachSafety-Hardness.set</includesfile>
<tasks name="Hardness">
<includesfile>../sv-benchmarks/c/Hardness.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-Fuzzle">
<includesfile>../sv-benchmarks/c/ReachSafety-Fuzzle.set</includesfile>
<tasks name="Fuzzle">
<includesfile>../sv-benchmarks/c/Fuzzle.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>

<tasks name="ConcurrencySafety-Main">
<includesfile>../sv-benchmarks/c/ConcurrencySafety-Main.set</includesfile>
<tasks name="Concurrency">
<includesfile>../sv-benchmarks/c/Concurrency.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
</rundefinition>

<rundefinition name="SV-COMP24_no-data-race">
<tasks name="NoDataRace-Main">
<includesfile>../sv-benchmarks/c/NoDataRace-Main.set</includesfile>
<tasks name="NoDataRace">
<includesfile>../sv-benchmarks/c/Concurrency.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/no-data-race.prp</propertyfile>
</tasks>
</rundefinition>

<rundefinition name="SV-COMP24_no-overflow">
<tasks name="ConcurrencySafety-NoOverflows">
<includesfile>../sv-benchmarks/c/ConcurrencySafety-NoOverflows.set</includesfile>
<includesfile>../sv-benchmarks/c/Concurrency.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/no-overflow.prp</propertyfile>
</tasks>
</rundefinition>

<rundefinition name="SV-COMP24_valid-memsafety">
<tasks name="ConcurrencySafety-MemSafety">
<includesfile>../sv-benchmarks/c/ConcurrencySafety-MemSafety.set</includesfile>
<includesfile>../sv-benchmarks/c/ConcurrencySafety.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile>
</tasks>
</rundefinition>
Expand Down
11 changes: 4 additions & 7 deletions .github/actions/cache-build/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down
6 changes: 2 additions & 4 deletions .github/actions/check-formatting/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,6 @@ runs:
- name: Checkout code
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Check for formatting
uses: leventeBajczi/[email protected]
uses: ./.github/actions/cache-build
with:
settings-file: "./.idea/codeStyles/Project.xml"
file-mask: "*.java,*.kt"
additional-options: "-dry"
arguments: spotlessCheck
21 changes: 19 additions & 2 deletions .github/workflows/check-copyright.yml
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ on:
permissions: write-all

concurrency:
group: copyright-${{ github.head_ref }}
group: copyright-${{ github.ref }}
cancel-in-progress: true

jobs:
Expand All @@ -17,4 +17,21 @@ jobs:
- name: Checkout repository
uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
- name: Check copyright
uses: ./.github/actions/check-copyright
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'
26 changes: 24 additions & 2 deletions .github/workflows/check-formatting.yml
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ on:
permissions: write-all

concurrency:
group: formatting-${{ github.head_ref }}
group: formatting-${{ github.ref }}
cancel-in-progress: true

jobs:
Expand All @@ -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
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'
21 changes: 19 additions & 2 deletions .github/workflows/check-version.yml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ on:
types: [opened, synchronize, reopened]

concurrency:
group: version-${{ github.head_ref }}
group: version-${{ github.ref }}
cancel-in-progress: true

jobs:
Expand Down Expand Up @@ -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
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'
26 changes: 24 additions & 2 deletions .github/workflows/linux-build-test-deploy.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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:
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/mac-build-test.yml
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ on:
permissions: write-all

concurrency:
group: mac-${{ github.head_ref }}
group: mac-${{ github.ref }}
cancel-in-progress: true

jobs:
Expand Down
Loading

0 comments on commit 8cc79dc

Please sign in to comment.