Update to use Ubuntu22.04 with newer clang

.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/
 

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` <name>
+
+ENTRYPOINT ["./NSym/scripts/docker_entrypoint.sh"]

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'

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)
+# ------------

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)

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"