Update SV-COMP performance testing tool to 2020/2021

- Use EC2 instead of CodeBuild to avoid Docker throttling.
- Use a VPC for compatibility with current EC2 spot offerings.
- Add profiling using Linux perf as gprof doesn't seem to be working
anymore.

Author: tautschnig

scripts/perf-test/build.yaml

@@ -0,0 +1,194 @@
+---
+AWSTemplateFormatVersion: 2010-09-09
+
+Parameters:
+    Ami:
+        Type: String
+
+    AvailabilityZone:
+        Type: String
+
+    Subnet:
+        Type: String
+
+    S3Bucket:
+        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
+            AvailabilityZone: !Ref AvailabilityZone
+            SubnetId: !Ref Subnet
+            IamInstanceProfile: !Ref EC2InstanceProfile
+            BlockDeviceMappings:
+              - DeviceName: /dev/xvda
+                Ebs:
+                  VolumeType: gp2
+                  VolumeSize: '30'
+                  DeleteOnTermination: 'true'
+            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
+            AvailabilityZone: !Ref AvailabilityZone
+            SubnetId: !Ref Subnet
+            IamInstanceProfile: !Ref EC2InstanceProfile
+            BlockDeviceMappings:
+              - DeviceName: /dev/xvda
+                Ebs:
+                  VolumeType: gp2
+                  VolumeSize: '30'
+                  DeleteOnTermination: 'true'
+            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