diff --git a/scripts/perf-test/codebuild-glucose.yaml b/scripts/perf-test/codebuild-glucose.yaml deleted file mode 100644 index 7cb1b8d1c73..00000000000 --- a/scripts/perf-test/codebuild-glucose.yaml +++ /dev/null @@ -1,129 +0,0 @@ ---- -AWSTemplateFormatVersion: 2010-09-09 - -Parameters: - S3Bucket: - Type: String - - PerfTestId: - Type: String - - RepoType: - Type: String - - Repository: - Type: String - -Resources: - CodeBuildRole: - Type: "AWS::IAM::Role" - Properties: - AssumeRolePolicyDocument: - Version: 2012-10-17 - Statement: - Effect: Allow - Principal: - Service: codebuild.amazonaws.com - Action: "sts:AssumeRole" - RoleName: !Sub "CR-${PerfTestId}" - Policies: - - PolicyName: !Sub "CP-${PerfTestId}" - PolicyDocument: - Version: 2012-10-17 - Statement: - - Action: - - "s3:PutObject" - Effect: Allow - Resource: !Join ["/", [!Sub "arn:aws:s3:::${S3Bucket}", "*"]] - - Action: - - "logs:CreateLogGroup" - - "logs:CreateLogStream" - - "logs:PutLogEvents" - Effect: Allow - Resource: !Sub 'arn:aws:logs:${AWS::Region}:${AWS::AccountId}:log-group:/aws/codebuild/*' - - ReleaseBuild: - Type: "AWS::CodeBuild::Project" - Properties: - Artifacts: - Type: S3 - Location: !Ref S3Bucket - Path: !Ref PerfTestId - Name: release - Environment: - ComputeType: BUILD_GENERAL1_LARGE - Image: aws/codebuild/ubuntu-base:14.04 - Type: LINUX_CONTAINER - Name: !Sub "perf-test-release-build-${PerfTestId}" - ServiceRole: !Ref CodeBuildRole - Source: - BuildSpec: !Sub | - version: 0.2 - phases: - install: - commands: - - apt-get update -y - - apt-get install -y software-properties-common - - add-apt-repository ppa:ubuntu-toolchain-r/test - - apt-get update -y - - apt-get install -y libwww-perl g++-5 flex bison git openjdk-7-jdk - - update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1 - - update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 1 - build: - commands: - - echo ${Repository} > COMMIT_INFO - - git rev-parse --short HEAD >> COMMIT_INFO - - git log HEAD^..HEAD >> COMMIT_INFO - - make -C src minisat2-download glucose-download - - sed -i 's/-Wno-error=misleading-indentation//' src/config.inc - - make -C src -j8 - artifacts: - files: - - src/cbmc/cbmc - - COMMIT_INFO - discard-paths: yes - Type: !Ref RepoType - Location: !Ref Repository - - ProfilingBuild: - Type: "AWS::CodeBuild::Project" - Properties: - Artifacts: - Type: S3 - Location: !Ref S3Bucket - Path: !Ref PerfTestId - Name: profiling - Environment: - ComputeType: BUILD_GENERAL1_LARGE - Image: aws/codebuild/ubuntu-base:14.04 - Type: LINUX_CONTAINER - Name: !Sub "perf-test-profiling-build-${PerfTestId}" - ServiceRole: !Ref CodeBuildRole - Source: - BuildSpec: !Sub | - version: 0.2 - phases: - install: - commands: - - apt-get update -y - - apt-get install -y software-properties-common - - add-apt-repository ppa:ubuntu-toolchain-r/test - - apt-get update -y - - apt-get install -y libwww-perl g++-5 flex bison git openjdk-7-jdk - - update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1 - - update-alternatives --install /usr/bin/g++ g++ /usr/bin/g++-5 1 - build: - commands: - - echo ${Repository} > COMMIT_INFO - - git rev-parse --short HEAD >> COMMIT_INFO - - git log HEAD^..HEAD >> COMMIT_INFO - - make -C src minisat2-download glucose-download - - sed -i 's/-Wno-error=misleading-indentation//' src/config.inc - - make -C src -j8 CXXFLAGS="-O2 -pg -g -finline-limit=4" LINKFLAGS="-pg" - artifacts: - files: - - src/cbmc/cbmc - - COMMIT_INFO - discard-paths: yes - Type: !Ref RepoType - Location: !Ref Repository diff --git a/scripts/perf-test/codebuild.yaml b/scripts/perf-test/codebuild.yaml index a0dab340246..01daf9ce93f 100644 --- a/scripts/perf-test/codebuild.yaml +++ b/scripts/perf-test/codebuild.yaml @@ -62,9 +62,8 @@ Resources: phases: install: commands: - - apt-get update -y - - apt-get install -y software-properties-common - - add-apt-repository ppa:ubuntu-toolchain-r/test + - echo "deb http://ppa.launchpad.net/ubuntu-toolchain-r/test/ubuntu trusty main" > /etc/apt/sources.list.d/toolchain.list + - apt-key adv --keyserver keyserver.ubuntu.com --recv-keys BA9EF27F - apt-get update -y - apt-get install -y libwww-perl g++-5 flex bison git openjdk-7-jdk - update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1 @@ -74,11 +73,12 @@ Resources: - echo ${Repository} > COMMIT_INFO - git rev-parse --short HEAD >> COMMIT_INFO - git log HEAD^..HEAD >> COMMIT_INFO - - make -C src minisat2-download glucose-download + - make -C src minisat2-download glucose-download cadical-download - make -C src -j8 artifacts: files: - src/cbmc/cbmc + - src/goto-cc/goto-cc - COMMIT_INFO discard-paths: yes Type: !Ref RepoType @@ -104,9 +104,8 @@ Resources: phases: install: commands: - - apt-get update -y - - apt-get install -y software-properties-common - - add-apt-repository ppa:ubuntu-toolchain-r/test + - echo "deb http://ppa.launchpad.net/ubuntu-toolchain-r/test/ubuntu trusty main" > /etc/apt/sources.list.d/toolchain.list + - apt-key adv --keyserver keyserver.ubuntu.com --recv-keys BA9EF27F - apt-get update -y - apt-get install -y libwww-perl g++-5 flex bison git openjdk-7-jdk - update-alternatives --install /usr/bin/gcc gcc /usr/bin/gcc-5 1 @@ -116,11 +115,12 @@ Resources: - echo ${Repository} > COMMIT_INFO - git rev-parse --short HEAD >> COMMIT_INFO - git log HEAD^..HEAD >> COMMIT_INFO - - make -C src minisat2-download glucose-download + - make -C src minisat2-download glucose-download cadical-download - make -C src -j8 CXXFLAGS="-O2 -pg -g -finline-limit=4" LINKFLAGS="-pg" artifacts: files: - src/cbmc/cbmc + - src/goto-cc/goto-cc - COMMIT_INFO discard-paths: yes Type: !Ref RepoType diff --git a/scripts/perf-test/ebs.yaml b/scripts/perf-test/ebs.yaml index e76a7497880..ce3a96f4792 100644 --- a/scripts/perf-test/ebs.yaml +++ b/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: diff --git a/scripts/perf-test/ec2.yaml b/scripts/perf-test/ec2.yaml index 47b8e1628cc..0f113d4ce3d 100644 --- a/scripts/perf-test/ec2.yaml +++ b/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/' @@ -212,7 +216,7 @@ Resources: cd /mnt cd cprover-sv-comp git pull - mkdir -p src/cbmc/ + mkdir -p src/cbmc src/goto-cc touch LICENSE cd .. mkdir -p run @@ -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) @@ -292,10 +317,12 @@ Resources: --receipt-handle $msg cd /mnt/cprover-sv-comp - rm -f src/cbmc/cbmc + rm -f src/cbmc/cbmc src/goto-cc/goto-cc aws s3 cp s3://${S3Bucket}/${PerfTestId}/$cfg/cbmc \ src/cbmc/cbmc - chmod a+x src/cbmc/cbmc + aws s3 cp s3://${S3Bucket}/${PerfTestId}/$cfg/goto-cc \ + src/goto-cc/goto-cc + chmod a+x src/cbmc/cbmc src/goto-cc/goto-cc make CBMC=. cbmc.zip cd ../run unzip ../cprover-sv-comp/cbmc.zip @@ -332,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/^(/dev/null 2>&1 then - gprof --sum ./cbmc-binary *.gmon.out.* + gprof --sum ./cbmc-binary cbmc*.gmon.out.* gprof ./cbmc-binary gmon.sum > sum.profile-$t + rm -f gmon.sum + gprof --sum ./goto-cc goto-cc*.gmon.out.* + gprof ./goto-cc gmon.sum > sum.goto-cc-profile-$t rm -f gmon.sum gmon.out *.gmon.out.* aws s3 cp sum.profile-$t \ s3://${S3Bucket}/${PerfTestId}/$cfg/sum.profile-$t + aws s3 cp sum.goto-cc-profile-$t \ + s3://${S3Bucket}/${PerfTestId}/$cfg/sum.goto-cc-profile-$t fi fi rm -rf logs-$t sum.profile-$t diff --git a/scripts/perf-test/perf_test.py b/scripts/perf-test/perf_test.py index 303bf25b712..1af45b85665 100755 --- a/scripts/perf-test/perf_test.py +++ b/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() @@ -265,24 +267,25 @@ def select_region(session, mode, region, instance_type): min_region, min_az, min_price)) # http://aws-ubuntu.herokuapp.com/ - # 20170919 - Ubuntu 16.04 LTS (xenial) - hvm:ebs-ssd + # 20180306 - Ubuntu 16.04 LTS (xenial) - hvm:ebs-ssd AMI_ids = { "Mappings": { "RegionMap": { - "ap-northeast-1": {"64": "ami-8422ebe2"}, - "ap-northeast-2": {"64": "ami-0f6fb461"}, - "ap-south-1": {"64": "ami-08a5e367"}, - "ap-southeast-1": {"64": "ami-e6d3a585"}, - "ap-southeast-2": {"64": "ami-391ff95b"}, - "ca-central-1": {"64": "ami-e59c2581"}, - "eu-central-1": {"64": "ami-5a922335"}, - "eu-west-1": {"64": "ami-17d11e6e"}, - "eu-west-2": {"64": "ami-e1f2e185"}, - "sa-east-1": {"64": "ami-a3e39ecf"}, - "us-east-1": {"64": "ami-d651b8ac"}, - "us-east-2": {"64": "ami-9686a4f3"}, - "us-west-1": {"64": "ami-2d5c6d4d"}, - "us-west-2": {"64": "ami-ecc63a94"} + "ap-northeast-1": { "64": "ami-0d74386b" }, + "ap-northeast-2": { "64": "ami-a414b9ca" }, + "ap-south-1": { "64": "ami-0189d76e" }, + "ap-southeast-1": { "64": "ami-52d4802e" }, + "ap-southeast-2": { "64": "ami-d38a4ab1" }, + "ca-central-1": { "64": "ami-ae55d2ca" }, + "eu-central-1": { "64": "ami-7c412f13" }, + "eu-west-1": { "64": "ami-f90a4880" }, + "eu-west-2": { "64": "ami-f4f21593" }, + "eu-west-3": { "64": "ami-0e55e373" }, + "sa-east-1": { "64": "ami-423d772e" }, + "us-east-1": { "64": "ami-43a15f3e" }, + "us-east-2": { "64": "ami-916f59f4" }, + "us-west-1": { "64": "ami-925144f2" }, + "us-west-2": { "64": "ami-4e79ed36" } } } } @@ -503,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') @@ -571,6 +574,10 @@ def run_perf_test( { 'ParameterKey': 'SSHKeyName', 'ParameterValue': ssh_key_name + }, + { + 'ParameterKey': 'WitnessCheck', + 'ParameterValue': str(witness_check) } ], Capabilities=['CAPABILITY_NAMED_IAM']) @@ -667,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