Extract llvm bitcode

.github/actions/NSym/action.yml

@@ -0,0 +1,8 @@
+# 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 verify AWS-LC against Cryptol specs'
+runs:
+  using: 'docker'
+  image: '../../../Dockerfile.nsym'

.github/workflows/main.yml

@@ -62,5 +62,5 @@ jobs:
 
     # Runs the formal verification action
     - name: NSym Proofs
-      uses: ./NSym/
+      uses: ./.github/actions/NSym
 

NSym/scripts/build_aarch64.sh

@@ -7,7 +7,7 @@ set -ex
 
 BUILD_TYPE=$1
 MICRO_ARCH=$2
-TARGET="aarch64-none-linux-gnu"
+TARGET="aarch64-unknown-linux-gnu"
 
 mkdir -p build_src/aarch64
 cd build_src/aarch64
@@ -16,9 +16,9 @@ cmake -DCMAKE_BUILD_TYPE=$BUILD_TYPE \
       -DKEEP_ASM_LOCAL_SYMBOLS=1 \
       -DBUILD_LIBSSL=OFF \
       -DCMAKE_TOOLCHAIN_FILE=../../scripts/build_aarch64.cmake \
-      -DCMAKE_C_FLAGS="-mcpu="$MICRO_ARCH \
-      -DCMAKE_CXX_FLAGS="-mcpu="$MICRO_ARCH \
-      -DCMAKE_ASM_FLAGS="-mcpu="$MICRO_ARCH \
+      -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 \

NSym/scripts/build_llvm.cmake

@@ -0,0 +1,24 @@
+# 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)
+
+# which compilers to use for C and C++
+set(CMAKE_C_COMPILER   wllvm)
+set(CMAKE_CXX_COMPILER wllvm++)
+
+# ------------
+# 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)
+# set(CMAKE_FIND_ROOT_PATH_MODE_PACKAGE ONLY)
+# ------------
+# set(CMAKE_SYSTEM_INCLUDE_PATH /usr/aarch64-linux-gnu/include)

NSym/scripts/build_llvm.sh

@@ -0,0 +1,34 @@
+#!/bin/sh
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+set -ex
+
+BUILD_TYPE=$1
+TARGET="aarch64-unknown-linux-gnu"
+
+mkdir -p build_src/llvm
+cd build_src/llvm
+export LDFLAGS="-fuse-ld=lld"
+
+export LLVM_COMPILER=clang
+export BINUTILS_TARGET_PREFIX=aarch64-linux-gnu
+export LLVM_COMPILER_PATH=/usr/lib/llvm-14/bin
+wllvm-sanity-checker
+
+cmake -DCMAKE_BUILD_TYPE=$BUILD_TYPE \
+      -DKEEP_ASM_LOCAL_SYMBOLS=1 \
+      -DBUILD_LIBSSL=OFF \
+      -DCMAKE_TOOLCHAIN_FILE=../../scripts/build_llvm.cmake \
+      -DCMAKE_C_COMPILER_TARGET=$TARGET \
+      -DCMAKE_CXX_COMPILER_TARGET=$TARGET \
+      -DCMAKE_ASM_COMPILER_TARGET=$TARGET \
+      ../../../src
+
+# -DCMAKE_C_FLAGS="-L/usr/lib/gcc-cross/aarch64-linux-gnu/11" \
+# -DCMAKE_CXX_FLAGS="-L/usr/lib/gcc-cross/aarch64-linux-gnu/11" \
+# -DCMAKE_ASM_FLAGS="-L/usr/lib/gcc-cross/aarch64-linux-gnu/11" \
+
+NUM_CPU_THREADS=$(grep -c ^processor /proc/cpuinfo)
+make -j $NUM_CPU_THREADS VERBOSE=1

NSym/scripts/docker_entrypoint.sh

@@ -3,5 +3,4 @@
 # 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"
+(cd NSym && ./scripts/entrypoint_check.sh)

NSym/scripts/entrypoint_check.sh

@@ -0,0 +1,10 @@
+#!/bin/sh
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+set -ex
+
+./scripts/build_aarch64.sh "Release" "neoverse-n1"
+./scripts/build_llvm.sh "Release"
+./scripts/post_build.sh

NSym/scripts/post_build.sh

@@ -0,0 +1,14 @@
+#!/bin/sh
+
+# Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# SPDX-License-Identifier: Apache-2.0
+
+
+set -ex
+
+export BINUTILS_TARGET_PREFIX=aarch64-linux-gnu
+
+mkdir -p build/llvm/crypto build/aarch64/crypto
+cp build_src/llvm/crypto/crypto_test build/llvm/crypto/crypto_test
+cp build_src/aarch64/crypto/crypto_test build/aarch64/crypto/crypto_test
+extract-bc build/llvm/crypto/crypto_test