From cbece4fbafdf662aefbe3fd503df48e4cfc31392 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 15 Dec 2023 12:18:36 +0200 Subject: [PATCH] Remove outdated my-bench-sv-comp --- sv-comp/my-bench-sv-comp/.gitignore | 1 - sv-comp/my-bench-sv-comp/README.md | 46 ------------ .../cpa-validate-correctness.xml | 25 ------- .../cpa-validate-violation.xml | 30 -------- sv-comp/my-bench-sv-comp/goblint-all-fast.sh | 26 ------- sv-comp/my-bench-sv-comp/goblint-all-fast.xml | 74 ------------------- sv-comp/my-bench-sv-comp/goblint-data-race.sh | 26 ------- .../my-bench-sv-comp/goblint-data-race.xml | 17 ----- sv-comp/my-bench-sv-comp/goblint-lint.sh | 42 ----------- sv-comp/my-bench-sv-comp/goblint-lint.xml | 68 ----------------- sv-comp/my-bench-sv-comp/goblint.sh | 63 ---------------- sv-comp/my-bench-sv-comp/goblint.xml | 38 ---------- .../table-generator-all-fast.xml | 17 ----- .../table-generator-data-race.xml | 13 ---- .../my-bench-sv-comp/table-generator-lint.xml | 16 ---- .../table-generator-witness.xml | 20 ----- .../uautomizer-validate-correctness.xml | 33 --------- .../uautomizer-validate-violation.xml | 32 -------- .../my-bench-sv-comp/witnesslint-validate.xml | 17 ----- .../witnesslint-validate2.xml | 31 -------- 20 files changed, 635 deletions(-) delete mode 100644 sv-comp/my-bench-sv-comp/.gitignore delete mode 100644 sv-comp/my-bench-sv-comp/README.md delete mode 100644 sv-comp/my-bench-sv-comp/cpa-validate-correctness.xml delete mode 100644 sv-comp/my-bench-sv-comp/cpa-validate-violation.xml delete mode 100755 sv-comp/my-bench-sv-comp/goblint-all-fast.sh delete mode 100644 sv-comp/my-bench-sv-comp/goblint-all-fast.xml delete mode 100755 sv-comp/my-bench-sv-comp/goblint-data-race.sh delete mode 100644 sv-comp/my-bench-sv-comp/goblint-data-race.xml delete mode 100755 sv-comp/my-bench-sv-comp/goblint-lint.sh delete mode 100644 sv-comp/my-bench-sv-comp/goblint-lint.xml delete mode 100755 sv-comp/my-bench-sv-comp/goblint.sh delete mode 100644 sv-comp/my-bench-sv-comp/goblint.xml delete mode 100644 sv-comp/my-bench-sv-comp/table-generator-all-fast.xml delete mode 100644 sv-comp/my-bench-sv-comp/table-generator-data-race.xml delete mode 100644 sv-comp/my-bench-sv-comp/table-generator-lint.xml delete mode 100644 sv-comp/my-bench-sv-comp/table-generator-witness.xml delete mode 100644 sv-comp/my-bench-sv-comp/uautomizer-validate-correctness.xml delete mode 100644 sv-comp/my-bench-sv-comp/uautomizer-validate-violation.xml delete mode 100644 sv-comp/my-bench-sv-comp/witnesslint-validate.xml delete mode 100644 sv-comp/my-bench-sv-comp/witnesslint-validate2.xml diff --git a/sv-comp/my-bench-sv-comp/.gitignore b/sv-comp/my-bench-sv-comp/.gitignore deleted file mode 100644 index 2eb047c8d6..0000000000 --- a/sv-comp/my-bench-sv-comp/.gitignore +++ /dev/null @@ -1 +0,0 @@ -*-tmp.xml diff --git a/sv-comp/my-bench-sv-comp/README.md b/sv-comp/my-bench-sv-comp/README.md deleted file mode 100644 index b401a1898c..0000000000 --- a/sv-comp/my-bench-sv-comp/README.md +++ /dev/null @@ -1,46 +0,0 @@ -# my-bench-sv-comp -This directory contains BenchExec benchmark and table definitions for a number of use cases and shell scripts for running them. - -## goblint-all-fast -Run Goblint on a large number of reachability benchmarks with decreased timeout. - -Files: -* `goblint-all-fast.sh` -* `goblint-all-fast.xml` -* `table-generator-all-fast.xml` - - -## goblint-data-race -Run Goblint on data-race benchmarks. - -Files: -* `goblint-data-race.sh` -* `goblint-data-race.xml` -* `table-generator-data-race.xml` - - -## goblint-lint -Run Goblint and validate witnesses using witnesslinter. - -Files: -* `goblint-lint.sh` -* `goblint-lint.xml` -* `table-generator-lint.xml` -* `witnesslint-validate.xml` - - -## goblint -Run Goblint and validate witnesses using: -* CPAChecker, -* Ultimate Automizer, -* witnesslinter. - -Files: -* `cpa-validate-correctness.xml` -* `cpa-validate-violation.xml` -* `goblint.sh` -* `goblint.xml` -* `table-generator-witness.xml` -* `uautomizer-validate-correctness.xml` -* `uautomizer-validate-violation.xml` -* `witnesslint-validate2.xml` diff --git a/sv-comp/my-bench-sv-comp/cpa-validate-correctness.xml b/sv-comp/my-bench-sv-comp/cpa-validate-correctness.xml deleted file mode 100644 index dca5c52c6d..0000000000 --- a/sv-comp/my-bench-sv-comp/cpa-validate-correctness.xml +++ /dev/null @@ -1,25 +0,0 @@ - - - - - - **.graphml - - - - - - - RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.graphml - - - - /home/simmo/benchexec/sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64-ReachSafety.set - /home/simmo/benchexec/sv-benchmarks/c/properties/unreach-call.prp - - - - diff --git a/sv-comp/my-bench-sv-comp/cpa-validate-violation.xml b/sv-comp/my-bench-sv-comp/cpa-validate-violation.xml deleted file mode 100644 index 8fcffd7321..0000000000 --- a/sv-comp/my-bench-sv-comp/cpa-validate-violation.xml +++ /dev/null @@ -1,30 +0,0 @@ - - - - - - **.graphml - - - - - - - - - - - - RESULTSDIR/LOGDIR/${rundefinition_name}/${taskdef_name}/witness.graphml - - - - /home/simmo/benchexec/sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64-ReachSafety.set - /home/simmo/benchexec/sv-benchmarks/c/properties/unreach-call.prp - - - - diff --git a/sv-comp/my-bench-sv-comp/goblint-all-fast.sh b/sv-comp/my-bench-sv-comp/goblint-all-fast.sh deleted file mode 100755 index c47ff10141..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint-all-fast.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/usr/bin/env bash - -shopt -s extglob - -MYBENCHDIR=/mnt/goblint-svcomp/benchexec/my-bench-sv-comp -RESULTSDIR=/mnt/goblint-svcomp/benchexec/results/70-all-fast-no-interval -GOBLINTPARALLEL=14 - -mkdir $RESULTSDIR - -# Run verification -cd /mnt/goblint-svcomp/sv-comp/goblint -# read-only and overlay dirs for Value too large for defined data type workaround -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $GOBLINTPARALLEL $MYBENCHDIR/goblint-all-fast.xml - -# Extract witness directory -cd $RESULTSDIR -LOGDIR=`echo goblint*.files` -echo $LOGDIR - -# Generate table with merged results and witness validation results -sed -e "s/LOGDIR/$LOGDIR/" $MYBENCHDIR/table-generator-all-fast.xml > table-generator.xml -table-generator -x table-generator.xml - -# Decompress all tool outputs for table HTML links -unzip -o goblint*.logfiles.zip \ No newline at end of file diff --git a/sv-comp/my-bench-sv-comp/goblint-all-fast.xml b/sv-comp/my-bench-sv-comp/goblint-all-fast.xml deleted file mode 100644 index 6d4bb8fc3c..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint-all-fast.xml +++ /dev/null @@ -1,74 +0,0 @@ - - - - - - - - - - - - - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/ConcurrencySafety-Main.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-wmm/* - - - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64-ReachSafety.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64Large-ReachSafety.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp - - - - diff --git a/sv-comp/my-bench-sv-comp/goblint-data-race.sh b/sv-comp/my-bench-sv-comp/goblint-data-race.sh deleted file mode 100755 index b42e69d5ce..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint-data-race.sh +++ /dev/null @@ -1,26 +0,0 @@ -#!/usr/bin/env bash - -shopt -s extglob - -MYBENCHDIR=/mnt/goblint-svcomp/benchexec/my-bench-sv-comp -RESULTSDIR=/mnt/goblint-svcomp/benchexec/results/data-race-results21-concurrencysafety-new -GOBLINTPARALLEL=14 - -mkdir $RESULTSDIR - -# Run verification -cd /mnt/goblint-svcomp/sv-comp/goblint -# read-only and overlay dirs for Value too large for defined data type workaround -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $GOBLINTPARALLEL $MYBENCHDIR/goblint-data-race.xml - -# Extract witness directory -cd $RESULTSDIR -LOGDIR=`echo goblint*.files` -echo $LOGDIR - -# Generate table with merged results and witness validation results -sed -e "s/LOGDIR/$LOGDIR/" $MYBENCHDIR/table-generator-data-race.xml > table-generator.xml -table-generator -x table-generator.xml - -# Decompress all tool outputs for table HTML links -unzip -o goblint*.logfiles.zip \ No newline at end of file diff --git a/sv-comp/my-bench-sv-comp/goblint-data-race.xml b/sv-comp/my-bench-sv-comp/goblint-data-race.xml deleted file mode 100644 index f8c00b582a..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint-data-race.xml +++ /dev/null @@ -1,17 +0,0 @@ - - - - - - - - - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/NoDataRace-ConcurrencySafety.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-data-race.prp - - - - diff --git a/sv-comp/my-bench-sv-comp/goblint-lint.sh b/sv-comp/my-bench-sv-comp/goblint-lint.sh deleted file mode 100755 index bbd1270a31..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint-lint.sh +++ /dev/null @@ -1,42 +0,0 @@ -#!/bin/bash - -shopt -s extglob - -MYBENCHDIR=/mnt/goblint-svcomp/benchexec/my-bench-sv-comp -RESULTSDIR=/mnt/goblint-svcomp/benchexec/results/new-results28-all-fast-systems-witness-linter -GOBLINTPARALLEL=15 -VALIDATEPARALLEL=15 - -mkdir $RESULTSDIR - -# Run verification -cd /mnt/goblint-svcomp/sv-comp/goblint -# read-only and overlay dirs for Value too large for defined data type workaround -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $GOBLINTPARALLEL $MYBENCHDIR/goblint-lint.xml - -# Extract witness directory -cd $RESULTSDIR -LOGDIR=`echo goblint*.files` -echo $LOGDIR - -# Construct validation XMLs -cd $MYBENCHDIR -# witnesslint -sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" witnesslint-validate.xml > witnesslint-validate-tmp.xml - -# Run validation -# witnesslint -cd /mnt/goblint-svcomp/benchexec/tools/witnesslint -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/witnesslint-validate-tmp.xml - -# Merge witness validation results -cd $RESULTSDIR -python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py goblint*.results.!(*merged*).xml.bz2 witnesslint-validate-tmp.*.results.*.xml.bz2 - -# Generate table with merged results and witness validation results -sed -e "s/LOGDIR/$LOGDIR/" $MYBENCHDIR/table-generator-lint.xml > table-generator.xml -table-generator -x table-generator.xml - -# Decompress all tool outputs for table HTML links -unzip -o goblint*.logfiles.zip -unzip -o witnesslint-validate-tmp.*.logfiles.zip \ No newline at end of file diff --git a/sv-comp/my-bench-sv-comp/goblint-lint.xml b/sv-comp/my-bench-sv-comp/goblint-lint.xml deleted file mode 100644 index 8cae0a2c69..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint-lint.xml +++ /dev/null @@ -1,68 +0,0 @@ - - - - - - **.graphml - - - - - - - - - - - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/SoftwareSystems-DeviceDriversLinux64-ReachSafety.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp - - - - diff --git a/sv-comp/my-bench-sv-comp/goblint.sh b/sv-comp/my-bench-sv-comp/goblint.sh deleted file mode 100755 index eaf74350de..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint.sh +++ /dev/null @@ -1,63 +0,0 @@ -#!/bin/bash - -shopt -s extglob - -MYBENCHDIR=/mnt/goblint-svcomp/benchexec/my-bench-sv-comp -RESULTSDIR=/mnt/goblint-svcomp/benchexec/results/new-results32-overflow -GOBLINTPARALLEL=15 -VALIDATEPARALLEL=4 # not enough memory for more - -mkdir $RESULTSDIR - -# Run verification -cd /mnt/goblint-svcomp/sv-comp/goblint -# read-only and overlay dirs for Value too large for defined data type workaround -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $GOBLINTPARALLEL $MYBENCHDIR/goblint.xml - -# Extract witness directory -cd $RESULTSDIR -LOGDIR=`echo goblint.*.files` -echo $LOGDIR - -# Construct validation XMLs -cd $MYBENCHDIR -# witnesslint -sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" witnesslint-validate2.xml > witnesslint-validate2-tmp.xml -# CPAChecker -# sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" cpa-validate-correctness.xml > cpa-validate-correctness-tmp.xml -# sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" cpa-validate-violation.xml > cpa-validate-violation-tmp.xml -# Ultimate -sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" uautomizer-validate-correctness.xml > uautomizer-validate-correctness-tmp.xml -sed -e "s|RESULTSDIR|$RESULTSDIR|" -e "s/LOGDIR/$LOGDIR/" uautomizer-validate-violation.xml > uautomizer-validate-violation-tmp.xml - -# Run validation -# witnesslint -cd /mnt/goblint-svcomp/benchexec/tools/witnesslint -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/witnesslint-validate2-tmp.xml -# CPAChecker -# cd /home/simmo/benchexec/tools/CPAchecker-1.9-unix -# benchexec --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/cpa-validate-correctness-tmp.xml -# benchexec --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/cpa-validate-violation-tmp.xml -# Ultimate -cd /mnt/goblint-svcomp/benchexec/tools/UAutomizer-linux -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/uautomizer-validate-correctness-tmp.xml -benchexec --read-only-dir / --overlay-dir . --hidden-dir /home --outputpath $RESULTSDIR --numOfThreads $VALIDATEPARALLEL $MYBENCHDIR/uautomizer-validate-violation-tmp.xml - -# Merge witness validation results -cd $RESULTSDIR -# python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py goblint.*.results.!(*merged*).xml.bz2 cpa-validate-correctness-tmp.*.results.*.xml.bz2 cpa-validate-violation-tmp.*.results.*.xml.bz2 uautomizer-validate-correctness-tmp.*.results.*.xml.bz2 uautomizer-validate-violation-tmp.*.results.*.xml.bz2 -# python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py goblint.*.results.!(*merged*).xml.bz2 uautomizer-validate-correctness-tmp.*.results.*.xml.bz2 uautomizer-validate-violation-tmp.*.results.*.xml.bz2 witnesslint-validate2-tmp.*.results.*.xml.bz2 -python3 /mnt/goblint-svcomp/benchexec/benchexec/contrib/mergeBenchmarkSets.py goblint.*.results.*no-overflow.xml.bz2 uautomizer-validate-correctness-tmp.*.results.*no-overflow.xml.bz2 uautomizer-validate-violation-tmp.*.results.*no-overflow.xml.bz2 witnesslint-validate2-tmp.*.results.*no-overflow.xml.bz2 - -# Generate table with merged results and witness validation results -# table-generator goblint.*.results.*.xml.bz2.merged.xml.bz2 cpa-validate-correctness-tmp.*.results.*.xml.bz2 cpa-validate-violation-tmp.*.results.*.xml.bz2 uautomizer-validate-correctness-tmp.*.results.*.xml.bz2 uautomizer-validate-violation-tmp.*.results.*.xml.bz2 -sed -e "s/LOGDIR/$LOGDIR/" $MYBENCHDIR/table-generator-witness.xml > table-generator.xml -table-generator -x table-generator.xml - -# Decompress all tool outputs for table HTML links -unzip -o goblint.*.logfiles.zip -# unzip -o cpa-validate-correctness-tmp.*.logfiles.zip -# unzip -o cpa-validate-violation-tmp.*.logfiles.zip -unzip -o uautomizer-validate-correctness-tmp.*.logfiles.zip -unzip -o uautomizer-validate-violation-tmp.*.logfiles.zip -unzip -o witnesslint-validate2-tmp.*.logfiles.zip \ No newline at end of file diff --git a/sv-comp/my-bench-sv-comp/goblint.xml b/sv-comp/my-bench-sv-comp/goblint.xml deleted file mode 100644 index c5773f3569..0000000000 --- a/sv-comp/my-bench-sv-comp/goblint.xml +++ /dev/null @@ -1,38 +0,0 @@ - - - - - - **.graphml - - - - - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/NoOverflows-BitVectors.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/NoOverflows-Other.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp - - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/SoftwareSystems-BusyBox-NoOverflows.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp - - - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/SoftwareSystems-uthash-NoOverflows.set - /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp - - - - - diff --git a/sv-comp/my-bench-sv-comp/table-generator-all-fast.xml b/sv-comp/my-bench-sv-comp/table-generator-all-fast.xml deleted file mode 100644 index c9b9932390..0000000000 --- a/sv-comp/my-bench-sv-comp/table-generator-all-fast.xml +++ /dev/null @@ -1,17 +0,0 @@ - - - - - - - - - - - - - - - - -
diff --git a/sv-comp/my-bench-sv-comp/table-generator-data-race.xml b/sv-comp/my-bench-sv-comp/table-generator-data-race.xml deleted file mode 100644 index 28410d1805..0000000000 --- a/sv-comp/my-bench-sv-comp/table-generator-data-race.xml +++ /dev/null @@ -1,13 +0,0 @@ - - - - - - - - - - - - -
diff --git a/sv-comp/my-bench-sv-comp/table-generator-lint.xml b/sv-comp/my-bench-sv-comp/table-generator-lint.xml deleted file mode 100644 index 6ca64dc84e..0000000000 --- a/sv-comp/my-bench-sv-comp/table-generator-lint.xml +++ /dev/null @@ -1,16 +0,0 @@ - - - - - - - - - witness - - - - - - -
diff --git a/sv-comp/my-bench-sv-comp/table-generator-witness.xml b/sv-comp/my-bench-sv-comp/table-generator-witness.xml deleted file mode 100644 index 876c08d392..0000000000 --- a/sv-comp/my-bench-sv-comp/table-generator-witness.xml +++ /dev/null @@ -1,20 +0,0 @@ - - - - - - - - - witness - - - - - - - - - - -
diff --git a/sv-comp/my-bench-sv-comp/uautomizer-validate-correctness.xml b/sv-comp/my-bench-sv-comp/uautomizer-validate-correctness.xml deleted file mode 100644 index efb0861775..0000000000 --- a/sv-comp/my-bench-sv-comp/uautomizer-validate-correctness.xml +++ /dev/null @@ -1,33 +0,0 @@ - - - - - **.graphml - - diff --git a/sv-comp/my-bench-sv-comp/uautomizer-validate-violation.xml b/sv-comp/my-bench-sv-comp/uautomizer-validate-violation.xml deleted file mode 100644 index fdf61b1bab..0000000000 --- a/sv-comp/my-bench-sv-comp/uautomizer-validate-violation.xml +++ /dev/null @@ -1,32 +0,0 @@ - - - - - **.graphml - - diff --git a/sv-comp/my-bench-sv-comp/witnesslint-validate.xml b/sv-comp/my-bench-sv-comp/witnesslint-validate.xml deleted file mode 100644 index 96a41ef731..0000000000 --- a/sv-comp/my-bench-sv-comp/witnesslint-validate.xml +++ /dev/null @@ -1,17 +0,0 @@ - - - - - diff --git a/sv-comp/my-bench-sv-comp/witnesslint-validate2.xml b/sv-comp/my-bench-sv-comp/witnesslint-validate2.xml deleted file mode 100644 index 475bc9846e..0000000000 --- a/sv-comp/my-bench-sv-comp/witnesslint-validate2.xml +++ /dev/null @@ -1,31 +0,0 @@ - - - - -