From 5d8acf247c2ec68d3e22ce7baf907c1071f26fc1 Mon Sep 17 00:00:00 2001 From: Yan Peng Date: Wed, 1 Nov 2023 06:49:17 +0000 Subject: [PATCH] Extract llvm bitcode --- .github/actions/NSym/action.yml | 8 ++++++++ .github/workflows/main.yml | 2 +- NSym/scripts/build_aarch64.sh | 8 ++++---- NSym/scripts/build_llvm.cmake | 24 ++++++++++++++++++++++ NSym/scripts/build_llvm.sh | 34 +++++++++++++++++++++++++++++++ NSym/scripts/docker_entrypoint.sh | 3 +-- NSym/scripts/entrypoint_check.sh | 10 +++++++++ NSym/scripts/post_build.sh | 14 +++++++++++++ 8 files changed, 96 insertions(+), 7 deletions(-) create mode 100644 .github/actions/NSym/action.yml create mode 100644 NSym/scripts/build_llvm.cmake create mode 100755 NSym/scripts/build_llvm.sh create mode 100755 NSym/scripts/entrypoint_check.sh create mode 100755 NSym/scripts/post_build.sh diff --git a/.github/actions/NSym/action.yml b/.github/actions/NSym/action.yml new file mode 100644 index 00000000..75c20059 --- /dev/null +++ b/.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' diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 6ea3f13e..025aa444 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -62,5 +62,5 @@ jobs: # Runs the formal verification action - name: NSym Proofs - uses: ./NSym/ + uses: ./.github/actions/NSym diff --git a/NSym/scripts/build_aarch64.sh b/NSym/scripts/build_aarch64.sh index 4e6d9ab1..26e70f16 100755 --- a/NSym/scripts/build_aarch64.sh +++ b/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 \ diff --git a/NSym/scripts/build_llvm.cmake b/NSym/scripts/build_llvm.cmake new file mode 100644 index 00000000..0ab59ac9 --- /dev/null +++ b/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) diff --git a/NSym/scripts/build_llvm.sh b/NSym/scripts/build_llvm.sh new file mode 100755 index 00000000..34aa1c9a --- /dev/null +++ b/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 diff --git a/NSym/scripts/docker_entrypoint.sh b/NSym/scripts/docker_entrypoint.sh index 4fe8c997..6e7661a4 100755 --- a/NSym/scripts/docker_entrypoint.sh +++ b/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) diff --git a/NSym/scripts/entrypoint_check.sh b/NSym/scripts/entrypoint_check.sh new file mode 100755 index 00000000..ad74f50f --- /dev/null +++ b/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 diff --git a/NSym/scripts/post_build.sh b/NSym/scripts/post_build.sh new file mode 100755 index 00000000..9f09f8a1 --- /dev/null +++ b/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