From efa54772802c9d22160eb51a1c9c676ac85567f4 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Wed, 1 Nov 2023 04:38:39 +0000 Subject: [PATCH] Update to use Ubuntu22.04 with newer clang --- .github/workflows/main.yml | 15 +++++++++++++++ Dockerfile.nsym | 28 ++++++++++++++++++++++++++++ NSym/action.yml | 9 +++++++++ NSym/scripts/build_aarch64.cmake | 24 +++++++++++++++--------- NSym/scripts/build_aarch64.sh | 16 +++++++++------- NSym/scripts/docker_entrypoint.sh | 7 +++++++ src | 2 +- 7 files changed, 84 insertions(+), 17 deletions(-) create mode 100644 Dockerfile.nsym create mode 100644 NSym/action.yml create mode 100755 NSym/scripts/docker_entrypoint.sh diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index b31b613d..6ea3f13e 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -48,4 +48,19 @@ jobs: # Runs the formal verification action - name: Coq Proofs uses: ./.github/actions/Coq + nsym: + # The type of runner that the job will run on + runs-on: aws-lc-verification_ubuntu-latest_16-core + + # Steps represent a sequence of tasks that will be executed as part of the job + steps: + # Check out main repo and submodules. + - uses: actions/checkout@v2 + name: check out top-level repository and all submodules + with: + submodules: true + + # Runs the formal verification action + - name: NSym Proofs + uses: ./NSym/ diff --git a/Dockerfile.nsym b/Dockerfile.nsym new file mode 100644 index 00000000..03d5a08d --- /dev/null +++ b/Dockerfile.nsym @@ -0,0 +1,28 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + + +FROM ubuntu:22.04 +ENV GOROOT=/usr/local/go +ENV PATH="$GOROOT/bin:$PATH" +ARG GO_VERSION=1.20.1 +ARG GO_ARCHIVE="go${GO_VERSION}.linux-amd64.tar.gz" +RUN echo 'debconf debconf/frontend select Noninteractive' | debconf-set-selections +RUN apt-get update +RUN apt-get install -y wget unzip git cmake clang llvm python3-pip libncurses5 opam libgmp-dev cabal-install +RUN apt-get install -y g++-aarch64-linux-gnu lld + +RUN wget "https://dl.google.com/go/${GO_ARCHIVE}" && tar -xvf $GO_ARCHIVE && \ + mkdir $GOROOT && mv go/* $GOROOT && rm $GO_ARCHIVE +RUN pip3 install wllvm +RUN pip3 install psutil + +ADD ./SAW/scripts /lc/scripts +RUN /lc/scripts/docker_install.sh +ENV CRYPTOLPATH="../../../cryptol-specs:../../spec" + +# This container expects all files in the directory to be mounted or copied. +# The GitHub action will mount the workspace and set the working directory of the container. +# Another way to mount the files is: docker run -v `pwd`:`pwd` -w `pwd` + +ENTRYPOINT ["./NSym/scripts/docker_entrypoint.sh"] diff --git a/NSym/action.yml b/NSym/action.yml new file mode 100644 index 00000000..dd6ac45a --- /dev/null +++ b/NSym/action.yml @@ -0,0 +1,9 @@ +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +name: 'AWS-LC Formal Verification NSym Proofs' +description: 'Check NSym proofs to validate some specifications used in AWS-LC' +runs: + using: 'docker' + image: '../Dockerfile.nsym' + entrypoint: 'NSym/scripts/docker_entrypoint.sh' diff --git a/NSym/scripts/build_aarch64.cmake b/NSym/scripts/build_aarch64.cmake index 5117ee99..8f191cb5 100644 --- a/NSym/scripts/build_aarch64.cmake +++ b/NSym/scripts/build_aarch64.cmake @@ -1,4 +1,5 @@ # https://cmake.org/cmake/help/book/mastering-cmake/chapter/Cross%20Compiling%20With%20CMake.html + # the name of the target operating system set(CMAKE_SYSTEM_NAME Linux) set(CMAKE_SYSTEM_PROCESSOR aarch64) @@ -7,13 +8,18 @@ set(CMAKE_SYSTEM_PROCESSOR aarch64) set(CMAKE_C_COMPILER clang) set(CMAKE_CXX_COMPILER clang++) -# where is the target environment located -set(CMAKE_FIND_ROOT_PATH /usr/aarch64-linux-gnu) -set(CMAKE_SYSROOT /usr/aarch64-linux-gnu) +# The following settings are needed on Ubuntu20.04 with Clang-10, +# but not on Ubuntu22.04 with Clang-14 for some reason +# ------------ +# # where is the target environment located +# # set(CMAKE_FIND_ROOT_PATH /usr/aarch64-linux-gnu) +# # set(CMAKE_SYSROOT /usr/aarch64-linux-gnu) -# adjust the default behavior of the FIND_XXX() commands: -# search programs in the host environment -set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM NEVER) -# search headers and libraries in the target environment -set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY ONLY) -set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE ONLY) +# # adjust the default behavior of the FIND_XXX() commands: +# # search programs in the host environment +# set(CMAKE_FIND_ROOT_PATH_MODE_PROGRAM NEVER) +# # search headers and libraries in the target environment +# set(CMAKE_FIND_ROOT_PATH_MODE_LIBRARY ONLY) +# set(CMAKE_FIND_ROOT_PATH_MODE_INCLUDE ONLY) +# set(CMAKE_FIND_ROOT_PATH_MODE_PACKAGE ONLY) +# ------------ diff --git a/NSym/scripts/build_aarch64.sh b/NSym/scripts/build_aarch64.sh index 822104f2..4e6d9ab1 100755 --- a/NSym/scripts/build_aarch64.sh +++ b/NSym/scripts/build_aarch64.sh @@ -6,20 +6,22 @@ set -ex BUILD_TYPE=$1 +MICRO_ARCH=$2 +TARGET="aarch64-none-linux-gnu" mkdir -p build_src/aarch64 cd build_src/aarch64 export LDFLAGS="-fuse-ld=lld" cmake -DCMAKE_BUILD_TYPE=$BUILD_TYPE \ - -DKEEP_LOCAL_SYMBOLS=1 \ + -DKEEP_ASM_LOCAL_SYMBOLS=1 \ -DBUILD_LIBSSL=OFF \ -DCMAKE_TOOLCHAIN_FILE=../../scripts/build_aarch64.cmake \ - -DCMAKE_C_FLAGS="-mcpu=neoverse-n1 -I/usr/aarch64-linux-gnu/include/c++/9/aarch64-linux-gnu" \ - -DCMAKE_CXX_FLAGS="-mcpu=neoverse-n1 -I/usr/aarch64-linux-gnu/include/c++/9/aarch64-linux-gnu" \ - -DCMAKE_ASM_FLAGS="-mcpu=neoverse-n1 -I/usr/aarch64-linux-gnu/include/c++/9/aarch64-linux-gnu" \ - -DCMAKE_C_COMPILER_TARGET="aarch64-none-linux-gnu" \ - -DCMAKE_CXX_COMPILER_TARGET="aarch64-none-linux-gnu" \ - -DCMAKE_ASM_COMPILER_TARGET="aarch64-none-linux-gnu" \ + -DCMAKE_C_FLAGS="-mcpu="$MICRO_ARCH \ + -DCMAKE_CXX_FLAGS="-mcpu="$MICRO_ARCH \ + -DCMAKE_ASM_FLAGS="-mcpu="$MICRO_ARCH \ + -DCMAKE_C_COMPILER_TARGET=$TARGET \ + -DCMAKE_CXX_COMPILER_TARGET=$TARGET \ + -DCMAKE_ASM_COMPILER_TARGET=$TARGET \ ../../../src NUM_CPU_THREADS=$(grep -c ^processor /proc/cpuinfo) diff --git a/NSym/scripts/docker_entrypoint.sh b/NSym/scripts/docker_entrypoint.sh new file mode 100755 index 00000000..4fe8c997 --- /dev/null +++ b/NSym/scripts/docker_entrypoint.sh @@ -0,0 +1,7 @@ +#!/bin/sh -ex + +# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved. +# SPDX-License-Identifier: Apache-2.0 + +cd NSym +./scripts/build_aarch64.sh "Release" "neoverse-n1" diff --git a/src b/src index ed4e08f6..88367484 160000 --- a/src +++ b/src @@ -1 +1 @@ -Subproject commit ed4e08f6de2ad2684f3ee6b80236169cf87793b5 +Subproject commit 88367484cb1ec40f2696fe2b792a0c0436d51f4d