Skip to content

Commit

Permalink
Merged, removed gen folder, formatted
Browse files Browse the repository at this point in the history
  • Loading branch information
@leventeBajczi
leventeBajczi committed Dec 2, 2024
2 parents ec1a632 + bd69e1c commit a520e15
Show file tree
Hide file tree
Showing 163 changed files with 8,120 additions and 24,957 deletions.
6 changes: 3 additions & 3 deletions .github/actions/benchexec-report/action.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -40,11 +40,11 @@ runs:
all=0
for txt in *.txt
do
new_correct=$(tail -n9 $txt | grep ' correct:' | awk ' { print $2 } ')
new_correct=$(tail -n9 $txt | grep ' correct:' | awk ' { print $2 } ' || echo 0)
correct=$((correct + new_correct))
new_incorrect=$(tail -n9 $txt | grep ' incorrect:' | awk ' { print $2 } ')
new_incorrect=$(tail -n9 $txt | grep ' incorrect:' | awk ' { print $2 } ' || echo 0)
incorrect=$((incorrect + new_incorrect))
new_all=$(tail -n9 $txt | grep 'Statistics:' | awk ' { print $2 } ')
new_all=$(tail -n9 $txt | grep 'Statistics:' | awk ' { print $2 } ' || echo 0)
all=$((all + new_all))
echo "Found $new_correct correct and $new_incorrect incorrect results out of $new_all tasks in $txt"
done
Expand Down
15 changes: 11 additions & 4 deletions .github/actions/benchexec-test/action.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,10 @@ inputs:
required: true
tool:
required: true
timeout:
required: true
xml:
required: true
runs:
using: "composite"
steps:
Expand All @@ -21,7 +25,7 @@ runs:
shell: bash
run: |
mkdir -p xml
cp $GITHUB_ACTION_PATH/theta.xml xml/
cp $GITHUB_ACTION_PATH/${{ inputs.xml }} xml/theta.xml
- name: Get sv-benchmarks (retry max. 3 times)
uses: nick-fields/retry@7152eba30c6575329ac0576536151aca5a72780e # v3.0.0
with:
Expand Down Expand Up @@ -58,11 +62,14 @@ runs:
folder=$(dirname $(find . -name "theta.jar" | head -n1))
echo $folder
pwd
for task in $(cat xml/theta.xml | grep 'tasks name=' | grep -oP '(?<=").*(?=")')
tasks=($(cat xml/theta.xml | awk '/rundefinition name="${{ inputs.rundef }}"/,/<\/rundefinition>/' | grep 'tasks name=' | grep -oP '(?<=").*(?=")'))
tasks_num=$(wc -w <<< ${tasks[@]})
timeout=$((${{inputs.timeout}} / tasks_num))
for task in ${tasks[@]}
do
echo "Starting benchmark on rundefinition '${{ inputs.rundef }}', task set '$task'"
echo "timeout 60 benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true"
timeout 60 benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true
echo "timeout --kill-after 15 $timeout benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true"
timeout --kill-after 15 $timeout benchexec xml/theta.xml -n 2 --no-container --tool-directory $folder -r ${{ inputs.rundef }} -t "$task" || true
done
- name: Upload results
uses: actions/upload-artifact@b4b15b8c7c6ac21ea08fcf65892d2ee8f75cf882 # v3.1.2
Expand Down
202 changes: 202 additions & 0 deletions .github/actions/benchexec-test/theta-short.xml
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,202 @@
<?xml version="1.0"?>
<!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-2.3.dtd">
<benchmark tool="theta" timelimit="40 s" hardtimelimit="60 s">

<resultfiles>**/witness.*</resultfiles>

<option name="--svcomp"/>
<option name="--portfolio">STABLE</option>
<option name="--loglevel">RESULT</option>


<rundefinition name="SV-COMP25_unreach-call">
<tasks name="ReachSafety-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/BitVectors.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-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/ECA.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-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/Heap.set</includesfile>
<includesfile>../sv-benchmarks/c/LinkedLists.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-Loops">
<includesfile>../sv-benchmarks/c/Loops.set</includesfile>
<includesfile>../sv-benchmarks/c/VerifyThis-Loops.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-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/Recursive.set</includesfile>
<includesfile>../sv-benchmarks/c/VerifyThis-Recursive.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-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/XCSP.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-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/Hardware.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>
<tasks name="ReachSafety-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/Fuzzle.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/unreach-call.prp</propertyfile>
</tasks>

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

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

<rundefinition name="SV-COMP25_valid-memcleanup">
<tasks name="MemSafety-MemCleanup">
<includesfile>../sv-benchmarks/c/Heap.set</includesfile>
<includesfile>../sv-benchmarks/c/Juliet.set</includesfile>
<includesfile>../sv-benchmarks/c/LinkedLists.set</includesfile>
<includesfile>../sv-benchmarks/c/VerifyThis-Loops.set</includesfile>
<includesfile>../sv-benchmarks/c/VerifyThis-Recursive.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/valid-memcleanup.prp</propertyfile>
</tasks>
</rundefinition>

<rundefinition name="SV-COMP25_valid-memsafety">
<tasks name="MemSafety-Arrays">
<includesfile>../sv-benchmarks/c/Arrays.set</includesfile>
<includesfile>../sv-benchmarks/c/Heap-Termination.set</includesfile>
<includesfile>../sv-benchmarks/c/VerifyThis-Loops.set</includesfile>
<includesfile>../sv-benchmarks/c/VerifyThis-Recursive.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile>
</tasks>
<tasks name="MemSafety-Heap">
<includesfile>../sv-benchmarks/c/Heap.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile>
</tasks>
<tasks name="MemSafety-LinkedLists">
<includesfile>../sv-benchmarks/c/LinkedLists.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile>
</tasks>
<tasks name="MemSafety-Other">
<includesfile>../sv-benchmarks/c/Loops.set</includesfile>
<includesfile>../sv-benchmarks/c/ControlFlow.set</includesfile>
<includesfile>../sv-benchmarks/c/ControlFlow-Termination.set</includesfile>
<includesfile>../sv-benchmarks/c/Recursive.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile>
</tasks>
<tasks name="MemSafety-Juliet">
<includesfile>../sv-benchmarks/c/Juliet.set</includesfile>
<!-- Exclude Juliet_test unsafe memsafety tasks without subproperty from competition. Originally excluded in commit 024bdad652 by @versokova -->
<exclude>../sv-benchmarks/c/Juliet_Test/*_bad.yml</exclude>
<propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile>
</tasks>

<tasks name="ConcurrencySafety-MemSafety">
<includesfile>../sv-benchmarks/c/Concurrency.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/valid-memsafety.prp</propertyfile>
</tasks>
</rundefinition>

<rundefinition name="SV-COMP25_no-overflow">
<tasks name="NoOverflows-Main">
<includesfile>../sv-benchmarks/c/Arrays.set</includesfile>
<includesfile>../sv-benchmarks/c/BitVectors.set</includesfile>
<includesfile>../sv-benchmarks/c/BitVectors-Termination.set</includesfile>
<includesfile>../sv-benchmarks/c/ControlFlow.set</includesfile>
<includesfile>../sv-benchmarks/c/ControlFlow-Termination.set</includesfile>
<includesfile>../sv-benchmarks/c/ECA.set</includesfile>
<includesfile>../sv-benchmarks/c/Floats.set</includesfile>
<includesfile>../sv-benchmarks/c/Heap.set</includesfile>
<includesfile>../sv-benchmarks/c/Heap-Termination.set</includesfile>
<includesfile>../sv-benchmarks/c/LinkedLists.set</includesfile>
<includesfile>../sv-benchmarks/c/Loops.set</includesfile>
<includesfile>../sv-benchmarks/c/Recursive.set</includesfile>
<includesfile>../sv-benchmarks/c/Sequentialized.set</includesfile>
<includesfile>../sv-benchmarks/c/VerifyThis-Loops.set</includesfile>
<includesfile>../sv-benchmarks/c/VerifyThis-Recursive.set</includesfile>
<includesfile>../sv-benchmarks/c/XCSP.set</includesfile>
<includesfile>../sv-benchmarks/c/SoftwareSystems-AWS-C-Common.set</includesfile>
<includesfile>../sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/no-overflow.prp</propertyfile>
</tasks>
<tasks name="NoOverflows-Juliet">
<includesfile>../sv-benchmarks/c/Juliet.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/no-overflow.prp</propertyfile>
</tasks>

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

<rundefinition name="SV-COMP25_termination">
<tasks name="Termination-BitVectors">
<includesfile>../sv-benchmarks/c/BitVectors-Termination.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/termination.prp</propertyfile>
</tasks>
<tasks name="Termination-MainControlFlow">
<includesfile>../sv-benchmarks/c/ControlFlow-Termination.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/termination.prp</propertyfile>
</tasks>
<tasks name="Termination-MainHeap">
<includesfile>../sv-benchmarks/c/Heap-Termination.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/termination.prp</propertyfile>
</tasks>
<tasks name="Termination-Other">
<includesfile>../sv-benchmarks/c/Arrays.set</includesfile>
<includesfile>../sv-benchmarks/c/BitVectors.set</includesfile>
<includesfile>../sv-benchmarks/c/ControlFlow.set</includesfile>
<includesfile>../sv-benchmarks/c/ECA.set</includesfile>
<includesfile>../sv-benchmarks/c/Floats.set</includesfile>
<includesfile>../sv-benchmarks/c/Heap.set</includesfile>
<includesfile>../sv-benchmarks/c/Loops.set</includesfile>
<includesfile>../sv-benchmarks/c/ProductLines.set</includesfile>
<includesfile>../sv-benchmarks/c/Recursive.set</includesfile>
<includesfile>../sv-benchmarks/c/Sequentialized.set</includesfile>
<includesfile>../sv-benchmarks/c/SoftwareSystems-uthash.set</includesfile>
<propertyfile>../sv-benchmarks/c/properties/termination.prp</propertyfile>
</tasks>

</rundefinition>



</benchmark>
2 changes: 1 addition & 1 deletion .github/actions/benchexec-test/theta.xml
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
<?xml version="1.0"?>
<!DOCTYPE benchmark PUBLIC "+//IDN sosy-lab.org//DTD BenchExec benchmark 1.9//EN" "https://www.sosy-lab.org/benchexec/benchmark-2.3.dtd">
<benchmark tool="theta" timelimit="20 s" hardtimelimit="30 s">
<benchmark tool="theta" timelimit="600 s" hardtimelimit="900 s">

<resultfiles>**/witness.*</resultfiles>

Expand Down
Loading

0 comments on commit a520e15

Please sign in to comment.