Skip to content

Update SV-COMP performance testing tool to 2020/2021 #6117

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
May 19, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
189 changes: 189 additions & 0 deletions scripts/perf-test/build.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,189 @@
---
AWSTemplateFormatVersion: 2010-09-09

Parameters:
Ami:
Type: String

S3Bucket:
Type: String

Subnet:
Type: String

PerfTestId:
Type: String

Repository:
Type: String

CommitId:
Type: String

UsePerf:
Type: String

Resources:
EC2Role:
Type: "AWS::IAM::Role"
Properties:
AssumeRolePolicyDocument:
Version: 2012-10-17
Statement:
Effect: Allow
Principal:
Service: ec2.amazonaws.com
Action: "sts:AssumeRole"
RoleName: !Sub "BR-${PerfTestId}"
Policies:
- PolicyName: !Sub "BP-${PerfTestId}"
PolicyDocument:
Version: 2012-10-17
Statement:
- Action:
- "s3:PutObject"
- "s3:GetObject"
Effect: Allow
Resource: !Join ["/", [!Sub "arn:aws:s3:::${S3Bucket}", "*"]]
- Action:
- "s3:ListBucket"
Effect: Allow
Resource: !Sub "arn:aws:s3:::${S3Bucket}"

EC2InstanceProfile:
Type: "AWS::IAM::InstanceProfile"
Properties:
Roles:
- !Ref EC2Role

ReleaseInstance:
Type: "AWS::EC2::Instance"
Properties:
InstanceType: c5.2xlarge
ImageId: !Ref Ami
IamInstanceProfile: !Ref EC2InstanceProfile
BlockDeviceMappings:
- DeviceName: /dev/xvda
Ebs:
VolumeType: gp2
VolumeSize: '30'
DeleteOnTermination: 'true'
SubnetId: !Ref Subnet
UserData:
Fn::Base64: !Sub |
#!/bin/bash
set -x -e

sed -i 's#/archive.ubuntu.com#/${AWS::Region}.ec2.archive.ubuntu.com#g' /etc/apt/sources.list
export DEBIAN_FRONTEND=noninteractive
apt-get update
apt-get install -y awscli

# AWS Sig-v4 access
aws configure set s3.signature_version s3v4

aws s3 cp s3://${S3Bucket}/ec2-terminate.sh /etc/init.d/ec2-terminate
sed -i '25,31d' /etc/init.d/ec2-terminate
sed -i 's/#S3BUCKET#/${S3Bucket}/g' /etc/init.d/ec2-terminate
sed -i 's/#PERFTESTID#/${PerfTestId}/g' /etc/init.d/ec2-terminate
chmod a+x /etc/init.d/ec2-terminate
update-rc.d ec2-terminate defaults
systemctl start ec2-terminate

trap poweroff EXIT

apt-get install -y build-essential flex bison git curl ccache zip

cd /root/
aws s3 cp s3://${S3Bucket}/release-build-cache/ccache.zip ccache.zip || true
unzip ccache.zip || true
rm -f ccache.zip
ccache -z --max-size=1G
git clone --depth 3 --branch ${CommitId} ${Repository} cbmc.git
cd cbmc.git
echo ${Repository} > COMMIT_INFO
git rev-parse --short HEAD >> COMMIT_INFO
git log HEAD^..HEAD >> COMMIT_INFO
make -C src minisat2-download glucose-download cadical-download
export CCACHE_NOHASHDIR=1
make -C src CXX="ccache g++" -j8
ccache -s

aws s3 cp src/cbmc/cbmc s3://${S3Bucket}/${PerfTestId}/release/cbmc
aws s3 cp src/goto-cc/goto-cc s3://${S3Bucket}/${PerfTestId}/release/goto-cc
aws s3 cp COMMIT_INFO s3://${S3Bucket}/${PerfTestId}/release/COMMIT_INFO
cd /root/
zip -r ccache.zip .ccache
aws s3 cp ccache.zip s3://${S3Bucket}/release-build-cache/ccache.zip

ProfilingInstance:
Type: "AWS::EC2::Instance"
Properties:
InstanceType: c5.2xlarge
ImageId: !Ref Ami
IamInstanceProfile: !Ref EC2InstanceProfile
BlockDeviceMappings:
- DeviceName: /dev/xvda
Ebs:
VolumeType: gp2
VolumeSize: '30'
DeleteOnTermination: 'true'
SubnetId: !Ref Subnet
UserData:
Fn::Base64: !Sub |
#!/bin/bash
set -x -e

sed -i 's#/archive.ubuntu.com#/${AWS::Region}.ec2.archive.ubuntu.com#g' /etc/apt/sources.list
export DEBIAN_FRONTEND=noninteractive
apt-get update
apt-get install -y awscli

# AWS Sig-v4 access
aws configure set s3.signature_version s3v4

aws s3 cp s3://${S3Bucket}/ec2-terminate.sh /etc/init.d/ec2-terminate
sed -i '25,31d' /etc/init.d/ec2-terminate
sed -i 's/#S3BUCKET#/${S3Bucket}/g' /etc/init.d/ec2-terminate
sed -i 's/#PERFTESTID#/${PerfTestId}/g' /etc/init.d/ec2-terminate
chmod a+x /etc/init.d/ec2-terminate
update-rc.d ec2-terminate defaults
systemctl start ec2-terminate

trap poweroff EXIT

apt-get install -y build-essential flex bison git curl ccache zip

cd /root/
aws s3 cp s3://${S3Bucket}/profiling-build-cache/ccache.zip ccache.zip || true
unzip ccache.zip || true
rm -f ccache.zip
ccache -z --max-size=1G
git clone --depth 3 --branch ${CommitId} ${Repository} cbmc.git
cd cbmc.git
echo ${Repository} > COMMIT_INFO
git rev-parse --short HEAD >> COMMIT_INFO
git log HEAD^..HEAD >> COMMIT_INFO
make -C src minisat2-download glucose-download cadical-download
export CCACHE_NOHASHDIR=1
if [ x${UsePerf} = xTrue ]
then
make -C src CXX="ccache g++" -j8 CXXFLAGS="-O2 -g -Wno-deprecated -fno-omit-frame-pointer"
else
make -C src CXX="ccache g++" -j8 CXXFLAGS="-O2 -pg -g -finline-limit=4 -Wno-deprecated" LINKFLAGS="-pg"
fi
ccache -s

aws s3 cp src/cbmc/cbmc s3://${S3Bucket}/${PerfTestId}/profiling/cbmc
aws s3 cp src/goto-cc/goto-cc s3://${S3Bucket}/${PerfTestId}/profiling/goto-cc
aws s3 cp COMMIT_INFO s3://${S3Bucket}/${PerfTestId}/profiling/COMMIT_INFO
cd /root/
df -h
zip -r ccache.zip .ccache
aws s3 cp ccache.zip s3://${S3Bucket}/profiling-build-cache/ccache.zip

Outputs:
ReleaseInstanceId:
Value: !Ref ReleaseInstance
ProfilingInstanceId:
Value: !Ref ProfilingInstance
172 changes: 0 additions & 172 deletions scripts/perf-test/codebuild.yaml

This file was deleted.

Loading