Skip to content

Commit

Permalink
Merge pull request #325 from ftsrg/fix-memloc
Browse files Browse the repository at this point in the history 
Fix memloc
  • Loading branch information
@leventeBajczi
leventeBajczi authored Nov 27, 2024
2 parents f8e0617 + 04ee836 commit bd69e1c
Show file tree
Hide file tree
Showing 26 changed files with 691 additions and 6,606 deletions.
8 changes: 6 additions & 2 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 @@ -60,7 +64,7 @@ runs:
pwd
tasks=($(cat xml/theta.xml | awk '/rundefinition name="${{ inputs.rundef }}"/,/<\/rundefinition>/' | grep 'tasks name=' | grep -oP '(?<=").*(?=")'))
tasks_num=$(wc -w <<< ${tasks[@]})
timeout=$((900 / tasks_num))
timeout=$((${{inputs.timeout}} / tasks_num))
for task in ${tasks[@]}
do
echo "Starting benchmark on rundefinition '${{ inputs.rundef }}', task set '$task'"
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="40 s" hardtimelimit="60 s">
<benchmark tool="theta" timelimit="600 s" hardtimelimit="900 s">

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

Expand Down
Loading

0 comments on commit bd69e1c

Please sign in to comment.