perf-test: add -W/--witness-check to validate SV-COMP witness checking

Author: tautschnig

scripts/perf-test/ebs.yaml

@@ -36,6 +36,8 @@ Resources:
                         https://github.com/sosy-lab/cpachecker.git
                 git clone --depth 1 \
                         https://github.com/diffblue/cprover-sv-comp.git
+                git clone --depth 1 \
+                        https://github.com/tautschnig/fshell-w2t.git
                 halt
 
     BaseVolume:

scripts/perf-test/ec2.yaml

@@ -38,6 +38,9 @@ Parameters:
     SSHKeyName:
         Type: String
 
+    WitnessCheck:
+        Type: String
+
 Conditions:
     UseSpot: !Not [!Equals [!Ref MaxPrice, ""]]
 
@@ -153,6 +156,7 @@ Resources:
                     apt-get install -y git time wget binutils awscli make jq
                     apt-get install -y zip unzip
                     apt-get install -y gcc libc6-dev-i386
+                    apt-get install -y ant python3-tempita python
 
                     # cgroup set up for benchexec
                     chmod o+wt '/sys/fs/cgroup/cpuset/'
@@ -223,6 +227,27 @@ Resources:
                     mkdir -p tmp
                     export TMPDIR=/mnt/tmp
 
+                    if [ x${WitnessCheck} = xTrue ]
+                    then
+                        cd cpachecker
+                        ant
+
+                        cd ../run
+                        for def in \
+                          cpa-seq-validate-correctness-witnesses \
+                          cpa-seq-validate-violation-witnesses \
+                          fshell-witness2test-validate-violation-witnesses
+                        do
+                            wget -O $def.xml https://raw.githubusercontent.com/sosy-lab/sv-comp/master/benchmark-defs/$def.xml
+                            sed -i 's#[\./]*/results-verified/LOGDIR/sv-comp18.\${!inputfile_name}.files/witness.graphml#witnesses/sv-comp18.${!inputfile_name}-witness.graphml#' $def.xml
+                        done
+
+                        ln -s ../cpachecker/scripts/cpa.sh cpa.sh
+                        ln -s ../cpachecker/config/ config
+
+                        cp ../fshell-w2t/* .
+                    fi
+
                     # reduce the likelihood of multiple hosts processing the
                     # same message (in addition to SQS's message hiding)
                     sleep $(expr $RANDOM % 30)
@@ -334,11 +359,26 @@ Resources:
                                 tar czf witnesses.tar.gz cbmc.*.logfiles
                                 rm -rf cbmc.*.logfiles
                                 cd ..
+
+                                if [ x${WitnessCheck} = xTrue ]
+                                then
+                                    for wc in *-witnesses.xml
+                                    do
+                                        wcp=$(echo $wc | sed 's/-witnesses.xml$//')
+                                        mkdir witnesses
+                                        tar -C witnesses --strip-components=1 -xzf \
+                                          logs-$t/witnesses.tar.gz
+                                        ../benchexec/bin/benchexec --no-container \
+                                          $wc --task $t -T 90s -M 15GB \
+                                          -o $wcp-logs-$t/ -N $max_par -c 1
+                                        rm -rf witnesses
+                                    done
+                                fi
                             fi
-                            if [ -f logs-$t/*.xml.bz2 ]
-                            then
-                                start_date="$(echo ${PerfTestId} | cut -f1-3 -d-) $(echo ${PerfTestId} | cut -f4-6 -d- | sed 's/-/:/g')"
-                                cd logs-$t
+                            start_date="$(echo ${PerfTestId} | cut -f1-3 -d-) $(echo ${PerfTestId} | cut -f4-6 -d- | sed 's/-/:/g')"
+                            for l in *logs-$t/*.xml.bz2
+                            do
+                                cd $(dirname $l)
                                 bunzip2 *.xml.bz2
                                 perl -p -i -e \
                                   "s/^(<result.*version=\"[^\"]*)/\$1:${PerfTestId}/" *.xml
@@ -348,10 +388,28 @@ Resources:
                                   "s/^(<result.*date=)\"[^\"]*/\$1\"$start_date/" *.xml
                                 bzip2 *.xml
                                 cd ..
+                            done
+
+                            if [ x${WitnessCheck} = xTrue ]
+                            then
+                                ../benchexec/bin/table-generator \
+                                  logs-$t/*xml.bz2 *-logs-$t/*.xml.bz2 -o logs-$t/
+                            else
+                                ../benchexec/bin/table-generator \
+                                  logs-$t/*xml.bz2 -o logs-$t/
                             fi
                             aws s3 cp logs-$t \
                                 s3://${S3Bucket}/${PerfTestId}/$cfg/logs-$t/ \
                                 --recursive
+                            for wc in *-witnesses.xml
+                            do
+                                [ -s $wc ] || break
+                                wcp=$(echo $wc | sed 's/-witnesses.xml$//')
+                                rm -rf $wcp-logs-$t/*.logfiles
+                                aws s3 cp $wcp-logs-$t \
+                                    s3://${S3Bucket}/${PerfTestId}/$cfg/$wcp-logs-$t/ \
+                                    --recursive
+                            done
                         else
                             rm -f gmon.sum gmon.out *.gmon.out.*
                             ../benchexec/bin/benchexec cbmc.xml --no-container \

scripts/perf-test/perf_test.py

@@ -70,6 +70,8 @@ def parse_args():
     parser.add_argument('-B', '--code-build', type=str,
                         default=same_dir('codebuild.yaml'),
                         help='Non-default CodeBuild template to use')
+    parser.add_argument('-W', '--witness-check', action='store_true',
+                        help='Run witness checks after benchmarking')
 
     args = parser.parse_args()
 
@@ -504,7 +506,7 @@ def seed_queue(session, region, queue, task_set):
 def run_perf_test(
         session, mode, region, az, ami, instance_type, sqs_arn, sqs_url,
         parallel, snapshot_id, instance_terminated_arn, bucket_name,
-        perf_test_id, price, ssh_key_name):
+        perf_test_id, price, ssh_key_name, witness_check):
     # create an EC2 instance and trigger benchmarking
     logger = logging.getLogger('perf_test')
 
@@ -572,6 +574,10 @@ def run_perf_test(
                 {
                     'ParameterKey': 'SSHKeyName',
                     'ParameterValue': ssh_key_name
+                },
+                {
+                    'ParameterKey': 'WitnessCheck',
+                    'ParameterValue': str(witness_check)
                 }
             ],
             Capabilities=['CAPABILITY_NAMED_IAM'])
@@ -668,7 +674,7 @@ def main():
             session, args.mode, region, az, ami, args.instance_type,
             sqs_arn, sqs_url, args.parallel, snapshot_id,
             instance_terminated_arn, bucket_name, perf_test_id, price,
-            args.ssh_key_name)
+            args.ssh_key_name, args.witness_check)
 
     return 0